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