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