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, provide useful methods such as map, filter and concat which only manipulate iterators, and can be used with ranged-for.
The NIL expression.
Definition: std_expr.h:4461
void ignore_command()
Definition: smt2_parser.cpp:78
Fixed-width bit-vector with two&#39;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