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