cprover
smt2_parser.cpp
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module:
4 
5 Author: Daniel Kroening, kroening@kroening.com
6 
7 \*******************************************************************/
8 
9 #include "smt2_parser.h"
10 
11 #include "smt2_format.h"
12 
13 #include <util/arith_tools.h>
14 #include <util/ieee_float.h>
15 #include <util/invariant.h>
16 #include <util/mathematical_expr.h>
17 #include <util/prefix.h>
18 #include <util/range.h>
19 
20 #include <numeric>
21 
23 {
24  const auto token = smt2_tokenizer.next_token();
25 
26  if(token == smt2_tokenizert::OPEN)
28  else if(token == smt2_tokenizert::CLOSE)
30 
31  return token;
32 }
33 
35 {
36  while(parenthesis_level > 0)
37  if(next_token() == smt2_tokenizert::END_OF_FILE)
38  return;
39 }
40 
42 {
43  exit=false;
44 
45  while(!exit)
46  {
47  if(smt2_tokenizer.peek() == smt2_tokenizert::END_OF_FILE)
48  {
49  exit = true;
50  return;
51  }
52 
53  if(next_token() != smt2_tokenizert::OPEN)
54  throw error("command must start with '('");
55 
56  if(next_token() != smt2_tokenizert::SYMBOL)
57  {
59  throw error("expected symbol as command");
60  }
61 
63 
64  switch(next_token())
65  {
66  case smt2_tokenizert::END_OF_FILE:
67  throw error(
68  "expected closing parenthesis at end of command,"
69  " but got EOF");
70 
71  case smt2_tokenizert::CLOSE:
72  // what we expect
73  break;
74 
75  case smt2_tokenizert::OPEN:
76  case smt2_tokenizert::SYMBOL:
77  case smt2_tokenizert::NUMERAL:
78  case smt2_tokenizert::STRING_LITERAL:
79  case smt2_tokenizert::NONE:
80  case smt2_tokenizert::KEYWORD:
81  throw error("expected ')' at end of command");
82  }
83  }
84 }
85 
87 {
88  std::size_t parentheses=0;
89  while(true)
90  {
91  switch(smt2_tokenizer.peek())
92  {
93  case smt2_tokenizert::OPEN:
94  next_token();
95  parentheses++;
96  break;
97 
98  case smt2_tokenizert::CLOSE:
99  if(parentheses==0)
100  return; // done
101 
102  next_token();
103  parentheses--;
104  break;
105 
106  case smt2_tokenizert::END_OF_FILE:
107  throw error("unexpected EOF in command");
108 
109  case smt2_tokenizert::SYMBOL:
110  case smt2_tokenizert::NUMERAL:
111  case smt2_tokenizert::STRING_LITERAL:
112  case smt2_tokenizert::NONE:
113  case smt2_tokenizert::KEYWORD:
114  next_token();
115  }
116  }
117 }
118 
120 {
121  exprt::operandst result;
122 
123  while(smt2_tokenizer.peek() != smt2_tokenizert::CLOSE)
124  result.push_back(expression());
125 
126  next_token(); // eat the ')'
127 
128  return result;
129 }
130 
132  const irep_idt &id,
133  idt::kindt kind,
134  const exprt &expr)
135 {
136  auto &count=renaming_counters[id];
137  irep_idt new_id;
138  do
139  {
140  new_id=id2string(id)+'#'+std::to_string(count);
141  count++;
142  } while(!id_map
143  .emplace(
144  std::piecewise_construct,
145  std::forward_as_tuple(new_id),
146  std::forward_as_tuple(kind, expr))
147  .second);
148 
149  // record renaming
150  renaming_map[id] = new_id;
151 
152  return new_id;
153 }
154 
155 void smt2_parsert::add_unique_id(const irep_idt &id, const exprt &expr)
156 {
157  if(!id_map
158  .emplace(
159  std::piecewise_construct,
160  std::forward_as_tuple(id),
161  std::forward_as_tuple(idt::VARIABLE, expr))
162  .second)
163  {
164  // id already used
165  throw error() << "identifier '" << id << "' defined twice";
166  }
167 }
168 
170 {
171  auto it=renaming_map.find(id);
172 
173  if(it==renaming_map.end())
174  return id;
175  else
176  return it->second;
177 }
178 
180 {
181  if(next_token() != smt2_tokenizert::OPEN)
182  throw error("expected bindings after let");
183 
184  std::vector<std::pair<irep_idt, exprt>> bindings;
185 
186  while(smt2_tokenizer.peek() == smt2_tokenizert::OPEN)
187  {
188  next_token();
189 
190  if(next_token() != smt2_tokenizert::SYMBOL)
191  throw error("expected symbol in binding");
192 
193  irep_idt identifier = smt2_tokenizer.get_buffer();
194 
195  // note that the previous bindings are _not_ visible yet
196  exprt value=expression();
197 
198  if(next_token() != smt2_tokenizert::CLOSE)
199  throw error("expected ')' after value in binding");
200 
201  bindings.push_back(
202  std::pair<irep_idt, exprt>(identifier, value));
203  }
204 
205  if(next_token() != smt2_tokenizert::CLOSE)
206  throw error("expected ')' at end of bindings");
207 
208  // save the renaming map
209  renaming_mapt old_renaming_map=renaming_map;
210 
211  // go forwards, add to id_map, renaming if need be
212  for(auto &b : bindings)
213  {
214  // get a fresh id for it
215  b.first = add_fresh_id(b.first, idt::BINDING, b.second);
216  }
217 
218  exprt where = expression();
219 
220  if(next_token() != smt2_tokenizert::CLOSE)
221  throw error("expected ')' after let");
222 
223  binding_exprt::variablest variables;
224  exprt::operandst values;
225 
226  for(const auto &b : bindings)
227  {
228  variables.push_back(symbol_exprt(b.first, b.second.type()));
229  values.push_back(b.second);
230  }
231 
232  // we keep these in the id_map in order to retain globally
233  // unique identifiers
234 
235  // restore renamings
236  renaming_map=old_renaming_map;
237 
238  return let_exprt(variables, values, where);
239 }
240 
242 {
243  if(next_token() != smt2_tokenizert::OPEN)
244  throw error() << "expected bindings after " << id;
245 
246  std::vector<symbol_exprt> bindings;
247 
248  while(smt2_tokenizer.peek() == smt2_tokenizert::OPEN)
249  {
250  next_token();
251 
252  if(next_token() != smt2_tokenizert::SYMBOL)
253  throw error("expected symbol in binding");
254 
255  irep_idt identifier = smt2_tokenizer.get_buffer();
256 
257  typet type=sort();
258 
259  if(next_token() != smt2_tokenizert::CLOSE)
260  throw error("expected ')' after sort in binding");
261 
262  bindings.push_back(symbol_exprt(identifier, type));
263  }
264 
265  if(next_token() != smt2_tokenizert::CLOSE)
266  throw error("expected ')' at end of bindings");
267 
268  // save the renaming map
269  renaming_mapt old_renaming_map = renaming_map;
270 
271  // go forwards, add to id_map, renaming if need be
272  for(auto &b : bindings)
273  {
274  const irep_idt id =
275  add_fresh_id(b.get_identifier(), idt::BINDING, exprt(ID_nil, b.type()));
276 
277  b.set_identifier(id);
278  }
279 
280  exprt expr=expression();
281 
282  if(next_token() != smt2_tokenizert::CLOSE)
283  throw error() << "expected ')' after " << id;
284 
285  exprt result=expr;
286 
287  // remove bindings from id_map
288  for(const auto &b : bindings)
289  id_map.erase(b.get_identifier());
290 
291  // restore renaming map
292  renaming_map = old_renaming_map;
293 
294  // go backwards, build quantified expression
295  for(auto r_it=bindings.rbegin(); r_it!=bindings.rend(); r_it++)
296  {
297  quantifier_exprt quantifier(id, *r_it, result);
298  result=quantifier;
299  }
300 
301  return result;
302 }
303 
305  const symbol_exprt &function,
306  const exprt::operandst &op)
307 {
308  const auto &function_type = to_mathematical_function_type(function.type());
309 
310  // check the arguments
311  if(op.size() != function_type.domain().size())
312  throw error("wrong number of arguments for function");
313 
314  for(std::size_t i=0; i<op.size(); i++)
315  {
316  if(op[i].type() != function_type.domain()[i])
317  throw error("wrong type for arguments for function");
318  }
319 
320  return function_application_exprt(function, op);
321 }
322 
324 {
325  exprt::operandst result = op;
326 
327  for(auto &expr : result)
328  {
329  if(expr.type().id() == ID_signedbv) // no need to cast
330  {
331  }
332  else if(expr.type().id() != ID_unsignedbv)
333  {
334  throw error("expected unsigned bitvector");
335  }
336  else
337  {
338  const auto width = to_unsignedbv_type(expr.type()).get_width();
339  expr = typecast_exprt(expr, signedbv_typet(width));
340  }
341  }
342 
343  return result;
344 }
345 
347 {
348  if(expr.type().id()==ID_unsignedbv) // no need to cast
349  return expr;
350 
351  if(expr.type().id()!=ID_signedbv)
352  throw error("expected signed bitvector");
353 
354  const auto width=to_signedbv_type(expr.type()).get_width();
355  return typecast_exprt(expr, unsignedbv_typet(width));
356 }
357 
359 {
360  if(op.empty())
361  throw error("expression must have at least one operand");
362 
363  for(std::size_t i = 1; i < op.size(); i++)
364  {
365  if(op[i].type() != op[0].type())
366  {
367  throw error() << "expression must have operands with matching types,"
368  " but got '"
369  << smt2_format(op[0].type()) << "' and '"
370  << smt2_format(op[i].type()) << '\'';
371  }
372  }
373 
374  exprt result(id, op[0].type());
375  result.operands() = op;
376  return result;
377 }
378 
380 {
381  if(op.size()!=2)
382  throw error("expression must have two operands");
383 
384  if(op[0].type() != op[1].type())
385  {
386  throw error() << "expression must have operands with matching types,"
387  " but got '"
388  << smt2_format(op[0].type()) << "' and '"
389  << smt2_format(op[1].type()) << '\'';
390  }
391 
392  return binary_predicate_exprt(op[0], id, op[1]);
393 }
394 
396 {
397  if(op.size()!=1)
398  throw error("expression must have one operand");
399 
400  return unary_exprt(id, op[0], op[0].type());
401 }
402 
404 {
405  if(op.size()!=2)
406  throw error("expression must have two operands");
407 
408  if(op[0].type() != op[1].type())
409  throw error("expression must have operands with matching types");
410 
411  return binary_exprt(op[0], id, op[1], op[0].type());
412 }
413 
415  const exprt::operandst &op)
416 {
417  if(op.size() != 2)
418  throw error() << "FloatingPoint equality takes two operands";
419 
420  if(op[0].type().id() != ID_floatbv || op[1].type().id() != ID_floatbv)
421  throw error() << "FloatingPoint equality takes FloatingPoint operands";
422 
423  if(op[0].type() != op[1].type())
424  {
425  throw error() << "FloatingPoint equality takes FloatingPoint operands with "
426  << "matching sort, but got " << smt2_format(op[0].type())
427  << " vs " << smt2_format(op[1].type());
428  }
429 
430  return ieee_float_equal_exprt(op[0], op[1]);
431 }
432 
434  const irep_idt &id,
435  const exprt::operandst &op)
436 {
437  if(op.size() != 3)
438  throw error() << id << " takes three operands";
439 
440  if(op[1].type().id() != ID_floatbv || op[2].type().id() != ID_floatbv)
441  throw error() << id << " takes FloatingPoint operands";
442 
443  if(op[1].type() != op[2].type())
444  {
445  throw error() << id << " takes FloatingPoint operands with matching sort, "
446  << "but got " << smt2_format(op[1].type()) << " vs "
447  << smt2_format(op[2].type());
448  }
449 
450  // clang-format off
451  const irep_idt expr_id =
452  id == "fp.add" ? ID_floatbv_plus :
453  id == "fp.sub" ? ID_floatbv_minus :
454  id == "fp.mul" ? ID_floatbv_mult :
455  id == "fp.div" ? ID_floatbv_div :
456  throw error("unsupported floating-point operation");
457  // clang-format on
458 
459  return ieee_float_op_exprt(op[1], expr_id, op[2], op[0]);
460 }
461 
463 {
464  // floating-point from bit-vectors
465  if(op.size() != 3)
466  throw error("fp takes three operands");
467 
468  if(op[0].type().id() != ID_unsignedbv)
469  throw error("fp takes BitVec as first operand");
470 
471  if(op[1].type().id() != ID_unsignedbv)
472  throw error("fp takes BitVec as second operand");
473 
474  if(op[2].type().id() != ID_unsignedbv)
475  throw error("fp takes BitVec as third operand");
476 
477  if(to_unsignedbv_type(op[0].type()).get_width() != 1)
478  throw error("fp takes BitVec of size 1 as first operand");
479 
480  const auto width_e = to_unsignedbv_type(op[1].type()).get_width();
481  const auto width_f = to_unsignedbv_type(op[2].type()).get_width();
482 
483  // stitch the bits together
484  return typecast_exprt(
485  concatenation_exprt(exprt::operandst(op), bv_typet(width_f + width_e + 1)),
486  ieee_float_spect(width_f, width_e).to_type());
487 }
488 
490 {
491  switch(next_token())
492  {
493  case smt2_tokenizert::SYMBOL:
494  if(smt2_tokenizer.get_buffer() == "_") // indexed identifier
495  {
496  // indexed identifier
497  if(next_token() != smt2_tokenizert::SYMBOL)
498  throw error("expected symbol after '_'");
499 
501  {
503  std::string(smt2_tokenizer.get_buffer(), 2, std::string::npos));
504 
505  if(next_token() != smt2_tokenizert::NUMERAL)
506  throw error("expected numeral as bitvector literal width");
507 
508  auto width = std::stoll(smt2_tokenizer.get_buffer());
509 
510  if(next_token() != smt2_tokenizert::CLOSE)
511  throw error("expected ')' after bitvector literal");
512 
513  return from_integer(i, unsignedbv_typet(width));
514  }
515  else
516  {
517  throw error() << "unknown indexed identifier "
519  }
520  }
521  else if(smt2_tokenizer.get_buffer() == "!")
522  {
523  // these are "term attributes"
524  const auto term = expression();
525 
526  while(smt2_tokenizer.peek() == smt2_tokenizert::KEYWORD)
527  {
528  next_token(); // eat the keyword
529  if(smt2_tokenizer.get_buffer() == "named")
530  {
531  // 'named terms' must be Boolean
532  if(term.type().id() != ID_bool)
533  throw error("named terms must be Boolean");
534 
535  if(next_token() == smt2_tokenizert::SYMBOL)
536  {
537  const symbol_exprt symbol_expr(
539  named_terms.emplace(
540  symbol_expr.get_identifier(), named_termt(term, symbol_expr));
541  }
542  else
543  throw error("invalid name attribute, expected symbol");
544  }
545  else
546  throw error("unknown term attribute");
547  }
548 
549  if(next_token() != smt2_tokenizert::CLOSE)
550  throw error("expected ')' at end of term attribute");
551  else
552  return term;
553  }
554  else
555  {
556  // non-indexed symbol, look up in expression table
557  const auto id = smt2_tokenizer.get_buffer();
558  const auto e_it = expressions.find(id);
559  if(e_it != expressions.end())
560  return e_it->second();
561 
562  // get the operands
563  auto op = operands();
564 
565  // rummage through id_map
566  const irep_idt final_id = rename_id(id);
567  auto id_it = id_map.find(final_id);
568  if(id_it != id_map.end())
569  {
570  if(id_it->second.type.id() == ID_mathematical_function)
571  {
572  return function_application(
573  symbol_exprt(final_id, id_it->second.type), op);
574  }
575  else
576  return symbol_exprt(final_id, id_it->second.type);
577  }
578 
579  throw error() << "unknown function symbol '" << id << '\'';
580  }
581  break;
582 
583  case smt2_tokenizert::OPEN: // likely indexed identifier
584  if(smt2_tokenizer.peek() == smt2_tokenizert::SYMBOL)
585  {
586  next_token(); // eat symbol
587  if(smt2_tokenizer.get_buffer() == "_")
588  {
589  // indexed identifier
590  if(next_token() != smt2_tokenizert::SYMBOL)
591  throw error("expected symbol after '_'");
592 
593  irep_idt id = smt2_tokenizer.get_buffer(); // hash it
594 
595  if(id=="extract")
596  {
597  if(next_token() != smt2_tokenizert::NUMERAL)
598  throw error("expected numeral after extract");
599 
600  auto upper = std::stoll(smt2_tokenizer.get_buffer());
601 
602  if(next_token() != smt2_tokenizert::NUMERAL)
603  throw error("expected two numerals after extract");
604 
605  auto lower = std::stoll(smt2_tokenizer.get_buffer());
606 
607  if(next_token() != smt2_tokenizert::CLOSE)
608  throw error("expected ')' after extract");
609 
610  auto op=operands();
611 
612  if(op.size()!=1)
613  throw error("extract takes one operand");
614 
615  auto upper_e=from_integer(upper, integer_typet());
616  auto lower_e=from_integer(lower, integer_typet());
617 
618  if(upper<lower)
619  throw error("extract got bad indices");
620 
621  unsignedbv_typet t(upper-lower+1);
622 
623  return extractbits_exprt(op[0], upper_e, lower_e, t);
624  }
625  else if(id=="rotate_left" ||
626  id=="rotate_right" ||
627  id == ID_repeat ||
628  id=="sign_extend" ||
629  id=="zero_extend")
630  {
631  if(next_token() != smt2_tokenizert::NUMERAL)
632  throw error() << "expected numeral after " << id;
633 
634  auto index = std::stoll(smt2_tokenizer.get_buffer());
635 
636  if(next_token() != smt2_tokenizert::CLOSE)
637  throw error() << "expected ')' after " << id << " index";
638 
639  auto op=operands();
640 
641  if(op.size()!=1)
642  throw error() << id << " takes one operand";
643 
644  if(id=="rotate_left")
645  {
646  auto dist=from_integer(index, integer_typet());
647  return binary_exprt(op[0], ID_rol, dist, op[0].type());
648  }
649  else if(id=="rotate_right")
650  {
651  auto dist=from_integer(index, integer_typet());
652  return binary_exprt(op[0], ID_ror, dist, op[0].type());
653  }
654  else if(id=="sign_extend")
655  {
656  // we first convert to a signed type of the original width,
657  // then extend to the new width, and then go to unsigned
658  const auto width = to_unsignedbv_type(op[0].type()).get_width();
659  const signedbv_typet small_signed_type(width);
660  const signedbv_typet large_signed_type(width + index);
661  const unsignedbv_typet unsigned_type(width + index);
662 
663  return typecast_exprt(
665  typecast_exprt(op[0], small_signed_type), large_signed_type),
666  unsigned_type);
667  }
668  else if(id=="zero_extend")
669  {
670  auto width=to_unsignedbv_type(op[0].type()).get_width();
671  unsignedbv_typet unsigned_type(width+index);
672 
673  return typecast_exprt(op[0], unsigned_type);
674  }
675  else if(id == ID_repeat)
676  {
677  return nil_exprt();
678  }
679  else
680  return nil_exprt();
681  }
682  else
683  {
684  throw error() << "unknown indexed identifier '"
685  << smt2_tokenizer.get_buffer() << '\'';
686  }
687  }
688  else
689  {
690  // just double parentheses
691  exprt tmp=expression();
692 
693  if(
694  next_token() != smt2_tokenizert::CLOSE &&
695  next_token() != smt2_tokenizert::CLOSE)
696  {
697  throw error("mismatched parentheses in an expression");
698  }
699 
700  return tmp;
701  }
702  }
703  else
704  {
705  // just double parentheses
706  exprt tmp=expression();
707 
708  if(
709  next_token() != smt2_tokenizert::CLOSE &&
710  next_token() != smt2_tokenizert::CLOSE)
711  {
712  throw error("mismatched parentheses in an expression");
713  }
714 
715  return tmp;
716  }
717  break;
718 
719  case smt2_tokenizert::CLOSE:
720  case smt2_tokenizert::NUMERAL:
721  case smt2_tokenizert::STRING_LITERAL:
722  case smt2_tokenizert::END_OF_FILE:
723  case smt2_tokenizert::NONE:
724  case smt2_tokenizert::KEYWORD:
725  // just parentheses
726  exprt tmp=expression();
727  if(next_token() != smt2_tokenizert::CLOSE)
728  throw error("mismatched parentheses in an expression");
729 
730  return tmp;
731  }
732 
733  UNREACHABLE;
734 }
735 
737 {
738  switch(next_token())
739  {
740  case smt2_tokenizert::SYMBOL:
741  {
742  const auto &identifier = smt2_tokenizer.get_buffer();
743 
744  // in the expression table?
745  const auto e_it = expressions.find(identifier);
746  if(e_it != expressions.end())
747  return e_it->second();
748 
749  // rummage through id_map
750  const irep_idt final_id = rename_id(identifier);
751  auto id_it = id_map.find(final_id);
752  if(id_it != id_map.end())
753  {
754  symbol_exprt symbol_expr(final_id, id_it->second.type);
756  symbol_expr.set(ID_C_quoted, true);
757  return std::move(symbol_expr);
758  }
759 
760  // don't know, give up
761  throw error() << "unknown expression '" << identifier << '\'';
762  }
763 
764  case smt2_tokenizert::NUMERAL:
765  {
766  const std::string &buffer = smt2_tokenizer.get_buffer();
767  if(buffer.size() >= 2 && buffer[0] == '#' && buffer[1] == 'x')
768  {
769  mp_integer value =
770  string2integer(std::string(buffer, 2, std::string::npos), 16);
771  const std::size_t width = 4 * (buffer.size() - 2);
772  CHECK_RETURN(width != 0 && width % 4 == 0);
773  unsignedbv_typet type(width);
774  return from_integer(value, type);
775  }
776  else if(buffer.size() >= 2 && buffer[0] == '#' && buffer[1] == 'b')
777  {
778  mp_integer value =
779  string2integer(std::string(buffer, 2, std::string::npos), 2);
780  const std::size_t width = buffer.size() - 2;
781  CHECK_RETURN(width != 0);
782  unsignedbv_typet type(width);
783  return from_integer(value, type);
784  }
785  else
786  {
787  return constant_exprt(buffer, integer_typet());
788  }
789  }
790 
791  case smt2_tokenizert::OPEN: // function application
792  return function_application();
793 
794  case smt2_tokenizert::END_OF_FILE:
795  throw error("EOF in an expression");
796 
797  case smt2_tokenizert::CLOSE:
798  case smt2_tokenizert::STRING_LITERAL:
799  case smt2_tokenizert::NONE:
800  case smt2_tokenizert::KEYWORD:
801  throw error("unexpected token in an expression");
802  }
803 
804  UNREACHABLE;
805 }
806 
808 {
809  expressions["true"] = [] { return true_exprt(); };
810  expressions["false"] = [] { return false_exprt(); };
811 
812  expressions["roundNearestTiesToEven"] = [] {
813  // we encode as 32-bit unsignedbv
815  };
816 
817  expressions["roundNearestTiesToAway"] = [this]() -> exprt {
818  throw error("unsupported rounding mode");
819  };
820 
821  expressions["roundTowardPositive"] = [] {
822  // we encode as 32-bit unsignedbv
824  };
825 
826  expressions["roundTowardNegative"] = [] {
827  // we encode as 32-bit unsignedbv
829  };
830 
831  expressions["roundTowardZero"] = [] {
832  // we encode as 32-bit unsignedbv
834  };
835 
836  expressions["let"] = [this] { return let_expression(); };
837  expressions["exists"] = [this] { return quantifier_expression(ID_exists); };
838  expressions["forall"] = [this] { return quantifier_expression(ID_forall); };
839  expressions["and"] = [this] { return multi_ary(ID_and, operands()); };
840  expressions["or"] = [this] { return multi_ary(ID_or, operands()); };
841  expressions["xor"] = [this] { return multi_ary(ID_xor, operands()); };
842  expressions["not"] = [this] { return unary(ID_not, operands()); };
843  expressions["="] = [this] { return binary_predicate(ID_equal, operands()); };
844  expressions["<="] = [this] { return binary_predicate(ID_le, operands()); };
845  expressions[">="] = [this] { return binary_predicate(ID_ge, operands()); };
846  expressions["<"] = [this] { return binary_predicate(ID_lt, operands()); };
847  expressions[">"] = [this] { return binary_predicate(ID_gt, operands()); };
848 
849  expressions["bvule"] = [this] { return binary_predicate(ID_le, operands()); };
850 
851  expressions["bvsle"] = [this] {
852  return binary_predicate(ID_le, cast_bv_to_signed(operands()));
853  };
854 
855  expressions["bvuge"] = [this] { return binary_predicate(ID_ge, operands()); };
856 
857  expressions["bvsge"] = [this] {
858  return binary_predicate(ID_ge, cast_bv_to_signed(operands()));
859  };
860 
861  expressions["bvult"] = [this] { return binary_predicate(ID_lt, operands()); };
862 
863  expressions["bvslt"] = [this] {
864  return binary_predicate(ID_lt, cast_bv_to_signed(operands()));
865  };
866 
867  expressions["bvugt"] = [this] { return binary_predicate(ID_gt, operands()); };
868 
869  expressions["bvsgt"] = [this] {
870  return binary_predicate(ID_gt, cast_bv_to_signed(operands()));
871  };
872 
873  expressions["bvashr"] = [this] {
875  };
876 
877  expressions["bvlshr"] = [this] { return binary(ID_lshr, operands()); };
878  expressions["bvshr"] = [this] { return binary(ID_lshr, operands()); };
879  expressions["bvlshl"] = [this] { return binary(ID_shl, operands()); };
880  expressions["bvashl"] = [this] { return binary(ID_shl, operands()); };
881  expressions["bvshl"] = [this] { return binary(ID_shl, operands()); };
882  expressions["bvand"] = [this] { return multi_ary(ID_bitand, operands()); };
883  expressions["bvnand"] = [this] { return multi_ary(ID_bitnand, operands()); };
884  expressions["bvor"] = [this] { return multi_ary(ID_bitor, operands()); };
885  expressions["bvnor"] = [this] { return multi_ary(ID_bitnor, operands()); };
886  expressions["bvxor"] = [this] { return multi_ary(ID_bitxor, operands()); };
887  expressions["bvxnor"] = [this] { return multi_ary(ID_bitxnor, operands()); };
888  expressions["bvnot"] = [this] { return unary(ID_bitnot, operands()); };
889  expressions["bvneg"] = [this] { return unary(ID_unary_minus, operands()); };
890  expressions["bvadd"] = [this] { return multi_ary(ID_plus, operands()); };
891  expressions["+"] = [this] { return multi_ary(ID_plus, operands()); };
892  expressions["bvsub"] = [this] { return binary(ID_minus, operands()); };
893  expressions["-"] = [this] { return binary(ID_minus, operands()); };
894  expressions["bvmul"] = [this] { return binary(ID_mult, operands()); };
895  expressions["*"] = [this] { return binary(ID_mult, operands()); };
896 
897  expressions["bvsdiv"] = [this] {
899  };
900 
901  expressions["bvudiv"] = [this] { return binary(ID_div, operands()); };
902  expressions["/"] = [this] { return binary(ID_div, operands()); };
903  expressions["div"] = [this] { return binary(ID_div, operands()); };
904 
905  expressions["bvsrem"] = [this] {
906  // 2's complement signed remainder (sign follows dividend)
907  // This matches our ID_mod, and what C does since C99.
909  };
910 
911  expressions["bvsmod"] = [this] {
912  // 2's complement signed remainder (sign follows divisor)
913  // We don't have that.
915  };
916 
917  expressions["bvurem"] = [this] { return binary(ID_mod, operands()); };
918 
919  expressions["%"] = [this] { return binary(ID_mod, operands()); };
920 
921  expressions["concat"] = [this] {
922  auto op = operands();
923 
924  // add the widths
925  auto op_width = make_range(op).map(
926  [](const exprt &o) { return to_unsignedbv_type(o.type()).get_width(); });
927 
928  const std::size_t total_width =
929  std::accumulate(op_width.begin(), op_width.end(), 0);
930 
931  return concatenation_exprt(std::move(op), unsignedbv_typet(total_width));
932  };
933 
934  expressions["distinct"] = [this] {
935  // pair-wise different constraint, multi-ary
936  return multi_ary("distinct", operands());
937  };
938 
939  expressions["ite"] = [this] {
940  auto op = operands();
941 
942  if(op.size() != 3)
943  throw error("ite takes three operands");
944 
945  if(op[0].type().id() != ID_bool)
946  throw error("ite takes a boolean as first operand");
947 
948  if(op[1].type() != op[2].type())
949  throw error("ite needs matching types");
950 
951  return if_exprt(op[0], op[1], op[2]);
952  };
953 
954  expressions["implies"] = [this] { return binary(ID_implies, operands()); };
955 
956  expressions["=>"] = [this] { return binary(ID_implies, operands()); };
957 
958  expressions["select"] = [this] {
959  auto op = operands();
960 
961  // array index
962  if(op.size() != 2)
963  throw error("select takes two operands");
964 
965  if(op[0].type().id() != ID_array)
966  throw error("select expects array operand");
967 
968  return index_exprt(op[0], op[1]);
969  };
970 
971  expressions["store"] = [this] {
972  auto op = operands();
973 
974  // array update
975  if(op.size() != 3)
976  throw error("store takes three operands");
977 
978  if(op[0].type().id() != ID_array)
979  throw error("store expects array operand");
980 
981  if(to_array_type(op[0].type()).subtype() != op[2].type())
982  throw error("store expects value that matches array element type");
983 
984  return with_exprt(op[0], op[1], op[2]);
985  };
986 
987  expressions["fp.isNaN"] = [this] {
988  auto op = operands();
989 
990  if(op.size() != 1)
991  throw error("fp.isNaN takes one operand");
992 
993  if(op[0].type().id() != ID_floatbv)
994  throw error("fp.isNaN takes FloatingPoint operand");
995 
996  return unary_predicate_exprt(ID_isnan, op[0]);
997  };
998 
999  expressions["fp.isInf"] = [this] {
1000  auto op = operands();
1001 
1002  if(op.size() != 1)
1003  throw error("fp.isInf takes one operand");
1004 
1005  if(op[0].type().id() != ID_floatbv)
1006  throw error("fp.isInf takes FloatingPoint operand");
1007 
1008  return unary_predicate_exprt(ID_isinf, op[0]);
1009  };
1010 
1011  expressions["fp.isNormal"] = [this] {
1012  auto op = operands();
1013 
1014  if(op.size() != 1)
1015  throw error("fp.isNormal takes one operand");
1016 
1017  if(op[0].type().id() != ID_floatbv)
1018  throw error("fp.isNormal takes FloatingPoint operand");
1019 
1020  return isnormal_exprt(op[0]);
1021  };
1022 
1023  expressions["fp"] = [this] { return function_application_fp(operands()); };
1024 
1025  expressions["fp.add"] = [this] {
1026  return function_application_ieee_float_op("fp.add", operands());
1027  };
1028 
1029  expressions["fp.mul"] = [this] {
1030  return function_application_ieee_float_op("fp.mul", operands());
1031  };
1032 
1033  expressions["fp.sub"] = [this] {
1034  return function_application_ieee_float_op("fp.sub", operands());
1035  };
1036 
1037  expressions["fp.div"] = [this] {
1038  return function_application_ieee_float_op("fp.div", operands());
1039  };
1040 
1041  expressions["fp.eq"] = [this] {
1043  };
1044 
1045  expressions["fp.leq"] = [this] {
1046  return binary_predicate(ID_le, operands());
1047  };
1048 
1049  expressions["fp.lt"] = [this] { return binary_predicate(ID_lt, operands()); };
1050 
1051  expressions["fp.geq"] = [this] {
1052  return binary_predicate(ID_ge, operands());
1053  };
1054 
1055  expressions["fp.gt"] = [this] { return binary_predicate(ID_gt, operands()); };
1056 
1057  expressions["fp.neg"] = [this] { return unary(ID_unary_minus, operands()); };
1058 }
1059 
1061 {
1062  // a sort is one of the following three cases:
1063  // SYMBOL
1064  // ( _ SYMBOL ...
1065  // ( SYMBOL ...
1066  switch(next_token())
1067  {
1068  case smt2_tokenizert::SYMBOL:
1069  break;
1070 
1071  case smt2_tokenizert::OPEN:
1072  if(smt2_tokenizer.next_token() != smt2_tokenizert::SYMBOL)
1073  throw error("expected symbol after '(' in a sort ");
1074 
1075  if(smt2_tokenizer.get_buffer() == "_")
1076  {
1077  if(next_token() != smt2_tokenizert::SYMBOL)
1078  throw error("expected symbol after '_' in a sort");
1079  }
1080  break;
1081 
1082  case smt2_tokenizert::CLOSE:
1083  case smt2_tokenizert::NUMERAL:
1084  case smt2_tokenizert::STRING_LITERAL:
1085  case smt2_tokenizert::NONE:
1086  case smt2_tokenizert::KEYWORD:
1087  throw error() << "unexpected token in a sort: '"
1088  << smt2_tokenizer.get_buffer() << '\'';
1089 
1090  case smt2_tokenizert::END_OF_FILE:
1091  throw error() << "unexpected end-of-file in a sort";
1092  }
1093 
1094  // now we have a SYMBOL
1095  const auto &token = smt2_tokenizer.get_buffer();
1096 
1097  const auto s_it = sorts.find(token);
1098 
1099  if(s_it == sorts.end())
1100  throw error() << "unexpected sort: '" << token << '\'';
1101 
1102  return s_it->second();
1103 }
1104 
1106 {
1107  sorts["Bool"] = [] { return bool_typet(); };
1108  sorts["Int"] = [] { return integer_typet(); };
1109  sorts["Real"] = [] { return real_typet(); };
1110 
1111  sorts["BitVec"] = [this] {
1112  if(next_token() != smt2_tokenizert::NUMERAL)
1113  throw error("expected numeral as bit-width");
1114 
1115  auto width = std::stoll(smt2_tokenizer.get_buffer());
1116 
1117  // eat the ')'
1118  if(next_token() != smt2_tokenizert::CLOSE)
1119  throw error("expected ')' at end of sort");
1120 
1121  return unsignedbv_typet(width);
1122  };
1123 
1124  sorts["FloatingPoint"] = [this] {
1125  if(next_token() != smt2_tokenizert::NUMERAL)
1126  throw error("expected numeral as bit-width");
1127 
1128  const auto width_e = std::stoll(smt2_tokenizer.get_buffer());
1129 
1130  if(next_token() != smt2_tokenizert::NUMERAL)
1131  throw error("expected numeral as bit-width");
1132 
1133  const auto width_f = std::stoll(smt2_tokenizer.get_buffer());
1134 
1135  // consume the ')'
1136  if(next_token() != smt2_tokenizert::CLOSE)
1137  throw error("expected ')' at end of sort");
1138 
1139  return ieee_float_spect(width_f - 1, width_e).to_type();
1140  };
1141 
1142  sorts["Array"] = [this] {
1143  // this gets two sorts as arguments, domain and range
1144  auto domain = sort();
1145  auto range = sort();
1146 
1147  // eat the ')'
1148  if(next_token() != smt2_tokenizert::CLOSE)
1149  throw error("expected ')' at end of Array sort");
1150 
1151  // we can turn arrays that map an unsigned bitvector type
1152  // to something else into our 'array_typet'
1153  if(domain.id() == ID_unsignedbv)
1154  return array_typet(range, infinity_exprt(domain));
1155  else
1156  throw error("unsupported array sort");
1157  };
1158 }
1159 
1162 {
1163  if(next_token() != smt2_tokenizert::OPEN)
1164  throw error("expected '(' at beginning of signature");
1165 
1166  if(smt2_tokenizer.peek() == smt2_tokenizert::CLOSE)
1167  {
1168  // no parameters
1169  next_token(); // eat the ')'
1171  }
1172 
1174  std::vector<irep_idt> parameters;
1175 
1176  while(smt2_tokenizer.peek() != smt2_tokenizert::CLOSE)
1177  {
1178  if(next_token() != smt2_tokenizert::OPEN)
1179  throw error("expected '(' at beginning of parameter");
1180 
1181  if(next_token() != smt2_tokenizert::SYMBOL)
1182  throw error("expected symbol in parameter");
1183 
1185  domain.push_back(sort());
1186 
1187  parameters.push_back(
1188  add_fresh_id(id, idt::PARAMETER, exprt(ID_nil, domain.back())));
1189 
1190  if(next_token() != smt2_tokenizert::CLOSE)
1191  throw error("expected ')' at end of parameter");
1192  }
1193 
1194  next_token(); // eat the ')'
1195 
1196  typet codomain = sort();
1197 
1199  mathematical_function_typet(domain, codomain), parameters);
1200 }
1201 
1203 {
1204  if(next_token() != smt2_tokenizert::OPEN)
1205  throw error("expected '(' at beginning of signature");
1206 
1207  if(smt2_tokenizer.peek() == smt2_tokenizert::CLOSE)
1208  {
1209  next_token(); // eat the ')'
1210  return sort();
1211  }
1212 
1214 
1215  while(smt2_tokenizer.peek() != smt2_tokenizert::CLOSE)
1216  {
1217  if(next_token() != smt2_tokenizert::OPEN)
1218  throw error("expected '(' at beginning of parameter");
1219 
1220  if(next_token() != smt2_tokenizert::SYMBOL)
1221  throw error("expected symbol in parameter");
1222 
1223  domain.push_back(sort());
1224 
1225  if(next_token() != smt2_tokenizert::CLOSE)
1226  throw error("expected ')' at end of parameter");
1227  }
1228 
1229  next_token(); // eat the ')'
1230 
1231  typet codomain = sort();
1232 
1233  return mathematical_function_typet(domain, codomain);
1234 }
1235 
1236 void smt2_parsert::command(const std::string &c)
1237 {
1238  auto c_it = commands.find(c);
1239  if(c_it == commands.end())
1240  {
1241  // silently ignore
1242  ignore_command();
1243  }
1244  else
1245  c_it->second();
1246 }
1247 
1249 {
1250  commands["declare-const"] = [this]() {
1251  const auto s = smt2_tokenizer.get_buffer();
1252 
1253  if(next_token() != smt2_tokenizert::SYMBOL)
1254  throw error() << "expected a symbol after " << s;
1255 
1257  auto type = sort();
1258 
1259  add_unique_id(id, exprt(ID_nil, type));
1260  };
1261 
1262  // declare-var appears to be a synonym for declare-const that is
1263  // accepted by Z3 and CVC4
1264  commands["declare-var"] = commands["declare-const"];
1265 
1266  commands["declare-fun"] = [this]() {
1267  if(next_token() != smt2_tokenizert::SYMBOL)
1268  throw error("expected a symbol after declare-fun");
1269 
1271  auto type = function_signature_declaration();
1272 
1273  add_unique_id(id, exprt(ID_nil, type));
1274  };
1275 
1276  commands["define-const"] = [this]() {
1277  if(next_token() != smt2_tokenizert::SYMBOL)
1278  throw error("expected a symbol after define-const");
1279 
1280  const irep_idt id = smt2_tokenizer.get_buffer();
1281 
1282  const auto type = sort();
1283  const auto value = expression();
1284 
1285  // check type of value
1286  if(value.type() != type)
1287  {
1288  throw error() << "type mismatch in constant definition: expected '"
1289  << smt2_format(type) << "' but got '"
1290  << smt2_format(value.type()) << '\'';
1291  }
1292 
1293  // create the entry
1294  add_unique_id(id, value);
1295  };
1296 
1297  commands["define-fun"] = [this]() {
1298  if(next_token() != smt2_tokenizert::SYMBOL)
1299  throw error("expected a symbol after define-fun");
1300 
1301  // save the renaming map
1302  renaming_mapt old_renaming_map = renaming_map;
1303 
1304  const irep_idt id = smt2_tokenizer.get_buffer();
1305 
1306  const auto signature = function_signature_definition();
1307  const auto body = expression();
1308 
1309  // restore renamings
1310  std::swap(renaming_map, old_renaming_map);
1311 
1312  // check type of body
1313  if(signature.type.id() == ID_mathematical_function)
1314  {
1315  const auto &f_signature = to_mathematical_function_type(signature.type);
1316  if(body.type() != f_signature.codomain())
1317  {
1318  throw error() << "type mismatch in function definition: expected '"
1319  << smt2_format(f_signature.codomain()) << "' but got '"
1320  << smt2_format(body.type()) << '\'';
1321  }
1322  }
1323  else if(body.type() != signature.type)
1324  {
1325  throw error() << "type mismatch in function definition: expected '"
1326  << smt2_format(signature.type) << "' but got '"
1327  << smt2_format(body.type()) << '\'';
1328  }
1329 
1330  // create the entry
1331  add_unique_id(id, body);
1332 
1333  id_map.at(id).type = signature.type;
1334  id_map.at(id).parameters = signature.parameters;
1335  };
1336 
1337  commands["exit"] = [this]() { exit = true; };
1338 }
smt2_parsert::command
void command(const std::string &)
Definition: smt2_parser.cpp:1236
with_exprt
Operator to update elements in structs and arrays.
Definition: std_expr.h:3050
smt2_parsert::quantifier_expression
exprt quantifier_expression(irep_idt)
Definition: smt2_parser.cpp:241
smt2_parsert::setup_sorts
void setup_sorts()
Definition: smt2_parser.cpp:1105
UNREACHABLE
#define UNREACHABLE
This should be used to mark dead code.
Definition: invariant.h:504
dstringt
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:37
smt2_parsert::rename_id
irep_idt rename_id(const irep_idt &) const
Definition: smt2_parser.cpp:169
smt2_parsert::setup_commands
void setup_commands()
Definition: smt2_parser.cpp:1248
smt2_parsert::renaming_counters
renaming_counterst renaming_counters
Definition: smt2_parser.h:95
arith_tools.h
smt2_parsert::error
smt2_tokenizert::smt2_errort error()
Definition: smt2_parser.h:77
CHECK_RETURN
#define CHECK_RETURN(CONDITION)
Definition: invariant.h:496
smt2_tokenizert::tokent
enum { NONE, END_OF_FILE, STRING_LITERAL, NUMERAL, SYMBOL, KEYWORD, OPEN, CLOSE } tokent
Definition: smt2_tokenizer.h:68
typet
The type of an expression, extends irept.
Definition: type.h:29
smt2_parsert::sorts
std::unordered_map< std::string, std::function< typet()> > sorts
Definition: smt2_parser.h:154
smt2_parsert::expressions
std::unordered_map< std::string, std::function< exprt()> > expressions
Definition: smt2_parser.h:123
smt2_parsert::ignore_command
void ignore_command()
Definition: smt2_parser.cpp:86
smt2_tokenizert::peek
tokent peek()
Definition: smt2_tokenizer.h:72
smt2_parsert::function_application
exprt function_application()
Definition: smt2_parser.cpp:489
mp_integer
BigInt mp_integer
Definition: mp_arith.h:19
if_exprt
The trinary if-then-else operator.
Definition: std_expr.h:2964
smt2_parsert::add_fresh_id
irep_idt add_fresh_id(const irep_idt &, idt::kindt, const exprt &)
Definition: smt2_parser.cpp:131
string2integer
const mp_integer string2integer(const std::string &n, unsigned base)
Definition: mp_arith.cpp:57
prefix.h
invariant.h
integer_typet
Unbounded, signed integers (mathematical integers, not bitvectors)
Definition: mathematical_types.h:22
smt2_parsert::binary
exprt binary(irep_idt, const exprt::operandst &)
Definition: smt2_parser.cpp:403
to_mathematical_function_type
const mathematical_function_typet & to_mathematical_function_type(const typet &type)
Cast a typet to a mathematical_function_typet.
Definition: mathematical_types.h:119
exprt
Base class for all expressions.
Definition: expr.h:53
unary_exprt
Generic base class for unary expressions.
Definition: std_expr.h:269
binary_exprt
A base class for binary expressions.
Definition: std_expr.h:601
smt2_parsert::commands
std::unordered_map< std::string, std::function< void()> > commands
Definition: smt2_parser.h:158
bool_typet
The Boolean type.
Definition: std_types.h:37
concatenation_exprt
Concatenation of bit-vector operands.
Definition: std_expr.h:4067
smt2_parsert::named_terms
named_termst named_terms
Definition: smt2_parser.h:68
quantifier_exprt
A base class for quantifier expressions.
Definition: mathematical_expr.h:271
to_string
std::string to_string(const string_not_contains_constraintt &expr)
Used for debug printing.
Definition: string_constraint.cpp:55
symbol_exprt
Expression to hold a symbol (variable)
Definition: std_expr.h:82
smt2_parsert::function_signature_definition
signature_with_parameter_idst function_signature_definition()
Definition: smt2_parser.cpp:1161
infinity_exprt
An expression denoting infinity.
Definition: std_expr.h:4111
unsignedbv_typet
Fixed-width bit-vector with unsigned binary interpretation.
Definition: std_types.h:1216
smt2_parsert::sort
typet sort()
Definition: smt2_parser.cpp:1060
smt2_parsert::exit
bool exit
Definition: smt2_parser.h:70
smt2_parsert::add_unique_id
void add_unique_id(const irep_idt &, const exprt &)
Definition: smt2_parser.cpp:155
smt2_parsert::multi_ary
exprt multi_ary(irep_idt, const exprt::operandst &)
Definition: smt2_parser.cpp:358
smt2_parsert::unary
exprt unary(irep_idt, const exprt::operandst &)
Definition: smt2_parser.cpp:395
ieee_float_spect
Definition: ieee_float.h:26
smt2_parsert::command_sequence
void command_sequence()
Definition: smt2_parser.cpp:41
exprt::type
typet & type()
Return the type of the expression.
Definition: expr.h:81
smt2_parsert::parenthesis_level
std::size_t parenthesis_level
Definition: smt2_parser.h:88
smt2_parsert::renaming_mapt
std::map< irep_idt, irep_idt > renaming_mapt
Definition: smt2_parser.h:92
smt2_parsert::function_signature_declaration
typet function_signature_declaration()
Definition: smt2_parser.cpp:1202
real_typet
Unbounded, signed real numbers.
Definition: mathematical_types.h:49
to_unsignedbv_type
const unsignedbv_typet & to_unsignedbv_type(const typet &type)
Cast a typet to an unsignedbv_typet.
Definition: std_types.h:1248
smt2_parsert::function_application_fp
exprt function_application_fp(const exprt::operandst &)
Definition: smt2_parser.cpp:462
smt2_parsert::let_expression
exprt let_expression()
Definition: smt2_parser.cpp:179
id2string
const std::string & id2string(const irep_idt &d)
Definition: irep.h:44
smt2_parser.h
smt2_parsert::setup_expressions
void setup_expressions()
Definition: smt2_parser.cpp:807
ieee_float_spect::to_type
class floatbv_typet to_type() const
Definition: ieee_float.cpp:25
binary_predicate_exprt
A base class for expressions that are predicates, i.e., Boolean-typed, and that take exactly two argu...
Definition: std_expr.h:694
smt2_parsert::binary_predicate
exprt binary_predicate(irep_idt, const exprt::operandst &)
Definition: smt2_parser.cpp:379
symbol_exprt::get_identifier
const irep_idt & get_identifier() const
Definition: std_expr.h:111
nil_exprt
The NIL expression.
Definition: std_expr.h:3973
smt2_format
static smt2_format_containert< T > smt2_format(const T &_o)
Definition: smt2_format.h:25
signedbv_typet
Fixed-width bit-vector with two's complement interpretation.
Definition: std_types.h:1265
smt2_parsert::named_termt
Definition: smt2_parser.h:55
smt2_parsert::function_application_ieee_float_op
exprt function_application_ieee_float_op(const irep_idt &, const exprt::operandst &)
Definition: smt2_parser.cpp:433
smt2_parsert::cast_bv_to_signed
exprt::operandst cast_bv_to_signed(const exprt::operandst &)
Apply typecast to signedbv to expressions in vector.
Definition: smt2_parser.cpp:323
function_application_exprt
Application of (mathematical) function.
Definition: mathematical_expr.h:191
binding_exprt::variablest
std::vector< symbol_exprt > variablest
Definition: std_expr.h:4123
mathematical_function_typet::domaint
std::vector< typet > domaint
Definition: mathematical_types.h:63
irept::id
const irep_idt & id() const
Definition: irep.h:418
range.h
Ranges: pair of begin and end iterators, which can be initialized from containers,...
exprt::operandst
std::vector< exprt > operandst
Definition: expr.h:55
false_exprt
The Boolean constant false.
Definition: std_expr.h:3964
smt2_parsert::renaming_map
renaming_mapt renaming_map
Definition: smt2_parser.h:93
smt2_parsert::signature_with_parameter_idst
Definition: smt2_parser.h:101
bitvector_typet::get_width
std::size_t get_width() const
Definition: std_types.h:1041
array_typet
Arrays with given size.
Definition: std_types.h:965
ieee_floatt::ROUND_TO_PLUS_INF
@ ROUND_TO_PLUS_INF
Definition: ieee_float.h:128
smt2_parsert::function_application_ieee_float_eq
exprt function_application_ieee_float_eq(const exprt::operandst &)
Definition: smt2_parser.cpp:414
ieee_floatt::ROUND_TO_EVEN
@ ROUND_TO_EVEN
Definition: ieee_float.h:127
smt2_parsert::expression
exprt expression()
Definition: smt2_parser.cpp:736
irept::set
void set(const irep_namet &name, const irep_idt &value)
Definition: irep.h:442
from_integer
constant_exprt from_integer(const mp_integer &int_value, const typet &type)
Definition: arith_tools.cpp:99
ieee_float.h
to_signedbv_type
const signedbv_typet & to_signedbv_type(const typet &type)
Cast a typet to a signedbv_typet.
Definition: std_types.h:1298
smt2_parsert::cast_bv_to_unsigned
exprt cast_bv_to_unsigned(const exprt &)
Apply typecast to unsignedbv to given expression.
Definition: smt2_parser.cpp:346
smt2_tokenizert::token_is_quoted_symbol
bool token_is_quoted_symbol() const
Definition: smt2_tokenizer.h:89
smt2_parsert::idt::kindt
enum { VARIABLE, BINDING, PARAMETER } kindt
Definition: smt2_parser.h:38
to_array_type
const array_typet & to_array_type(const typet &type)
Cast a typet to an array_typet.
Definition: std_types.h:1011
smt2_parsert::next_token
smt2_tokenizert::tokent next_token()
Definition: smt2_parser.cpp:22
ieee_float_op_exprt
IEEE floating-point operations These have two data operands (op0 and op1) and one rounding mode (op2)...
Definition: std_expr.h:3790
has_prefix
bool has_prefix(const std::string &s, const std::string &prefix)
Definition: converter.cpp:13
smt2_format.h
smt2_tokenizert::next_token
tokent next_token()
Definition: smt2_tokenizer.cpp:203
smt2_parsert::operands
exprt::operandst operands()
Definition: smt2_parser.cpp:119
extractbits_exprt
Extracts a sub-range of a bit-vector operand.
Definition: std_expr.h:2697
exprt::operands
operandst & operands()
Definition: expr.h:95
smt2_parsert::smt2_tokenizer
smt2_tokenizert smt2_tokenizer
Definition: smt2_parser.h:86
index_exprt
Array index operator.
Definition: std_expr.h:1293
typecast_exprt
Semantic type conversion.
Definition: std_expr.h:2013
true_exprt
The Boolean constant true.
Definition: std_expr.h:3955
constant_exprt
A constant literal expression.
Definition: std_expr.h:3906
ieee_float_equal_exprt
IEEE-floating-point equality.
Definition: std_expr.h:3689
make_range
ranget< iteratort > make_range(iteratort begin, iteratort end)
Definition: range.h:524
mathematical_function_typet
A type for mathematical functions (do not confuse with functions/methods in code)
Definition: mathematical_types.h:59
isnormal_exprt
Evaluates to true if the operand is a normal number.
Definition: std_expr.h:3644
smt2_parsert::id_map
id_mapt id_map
Definition: smt2_parser.h:52
unary_predicate_exprt
A base class for expressions that are predicates, i.e., Boolean-typed, and that take exactly one argu...
Definition: std_expr.h:546
ieee_floatt::ROUND_TO_MINUS_INF
@ ROUND_TO_MINUS_INF
Definition: ieee_float.h:127
smt2_tokenizert::get_buffer
const std::string & get_buffer() const
Definition: smt2_tokenizer.h:84
let_exprt
A let expression.
Definition: std_expr.h:4165
smt2_parsert::skip_to_end_of_list
void skip_to_end_of_list()
This skips tokens until all bracketed expressions are closed.
Definition: smt2_parser.cpp:34
ieee_floatt::ROUND_TO_ZERO
@ ROUND_TO_ZERO
Definition: ieee_float.h:128
bv_typet
Fixed-width bit-vector without numerical interpretation.
Definition: std_types.h:1106
mathematical_expr.h
API to expression classes for 'mathematical' expressions.