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 <util/arith_tools.h>
12 
14 {
15  exit=false;
16 
17  while(next_token()==OPEN)
18  {
19  if(next_token()!=SYMBOL)
20  {
21  error() << "expected symbol as command" << eom;
22  return;
23  }
24 
25  command(buffer);
26 
27  if(exit)
28  return;
29 
30  switch(next_token())
31  {
32  case END_OF_FILE:
33  error() << "expected closing parenthesis at end of command,"
34  " but got EOF" << eom;
35  return;
36 
37  case CLOSE:
38  // what we expect
39  break;
40 
41  default:
42  error() << "expected end of command" << eom;
43  return;
44  }
45  }
46 
47  if(token!=END_OF_FILE)
48  {
49  error() << "unexpected token in command sequence" << eom;
50  }
51 }
52 
54 {
55  std::size_t parentheses=0;
56  while(true)
57  {
58  switch(peek())
59  {
60  case OPEN:
61  next_token();
62  parentheses++;
63  break;
64 
65  case CLOSE:
66  if(parentheses==0)
67  return; // done
68 
69  next_token();
70  parentheses--;
71  break;
72 
73  case END_OF_FILE:
74  error() << "unexpected EOF in command" << eom;
75  return;
76 
77  default:
78  next_token();
79  }
80  }
81 }
83 {
85 
86  while(peek()!=CLOSE)
87  result.push_back(expression());
88 
89  next_token(); // eat the ')'
90 
91  return result;
92 }
93 
95 {
96  if(id_map[id].type.is_nil())
97  return id; // id not yet used
98 
99  auto &count=renaming_counters[id];
100  irep_idt new_id;
101  do
102  {
103  new_id=id2string(id)+'#'+std::to_string(count);
104  count++;
105  }
106  while(id_map.find(new_id)!=id_map.end());
107 
108  // record renaming
109  renaming_map[id]=new_id;
110 
111  return new_id;
112 }
113 
115 {
116  auto it=renaming_map.find(id);
117 
118  if(it==renaming_map.end())
119  return id;
120  else
121  return it->second;
122 }
123 
125 {
126  if(next_token()!=OPEN)
127  {
128  error() << "expected bindings after let" << eom;
129  return nil_exprt();
130  }
131 
132  std::vector<std::pair<irep_idt, exprt>> bindings;
133 
134  while(peek()==OPEN)
135  {
136  next_token();
137 
138  if(next_token()!=SYMBOL)
139  {
140  error() << "expected symbol in binding" << eom;
141  return nil_exprt();
142  }
143 
144  irep_idt identifier=buffer;
145 
146  // note that the previous bindings are _not_ visible yet
147  exprt value=expression();
148 
149  if(next_token()!=CLOSE)
150  {
151  error() << "expected ')' after value in binding" << eom;
152  return nil_exprt();
153  }
154 
155  bindings.push_back(
156  std::pair<irep_idt, exprt>(identifier, value));
157  }
158 
159  if(next_token()!=CLOSE)
160  {
161  error() << "expected ')' at end of bindings" << eom;
162  return nil_exprt();
163  }
164 
165  // save the renaming map
166  renaming_mapt old_renaming_map=renaming_map;
167 
168  // go forwards, add to id_map, renaming if need be
169  for(auto &b : bindings)
170  {
171  // get a fresh id for it
172  b.first=get_fresh_id(b.first);
173  auto &entry=id_map[b.first];
174  entry.type=b.second.type();
175  entry.definition=b.second;
176  }
177 
178  exprt expr=expression();
179 
180  if(next_token()!=CLOSE)
181  {
182  error() << "expected ')' after let" << eom;
183  return nil_exprt();
184  }
185 
186  exprt result=expr;
187 
188  // go backwards, build let_expr
189  for(auto r_it=bindings.rbegin(); r_it!=bindings.rend(); r_it++)
190  {
191  let_exprt let;
192  let.symbol()=symbol_exprt(r_it->first, r_it->second.type());
193  let.value()=r_it->second;
194  let.type()=result.type();
195  let.where().swap(result);
196  result=let;
197  }
198 
199  // remove bindings from id_map
200  for(const auto &b : bindings)
201  id_map.erase(b.first);
202 
203  // restore renamings
204  renaming_map=old_renaming_map;
205 
206  return result;
207 }
208 
210 {
211  if(next_token()!=OPEN)
212  {
213  error() << "expected bindings after " << id << eom;
214  return nil_exprt();
215  }
216 
217  std::vector<symbol_exprt> bindings;
218 
219  while(peek()==OPEN)
220  {
221  next_token();
222 
223  if(next_token()!=SYMBOL)
224  {
225  error() << "expected symbol in binding" << eom;
226  return nil_exprt();
227  }
228 
229  irep_idt identifier=buffer;
230 
231  typet type=sort();
232 
233  if(next_token()!=CLOSE)
234  {
235  error() << "expected ')' after sort in binding" << eom;
236  return nil_exprt();
237  }
238 
239  bindings.push_back(symbol_exprt(identifier, type));
240  }
241 
242  if(next_token()!=CLOSE)
243  {
244  error() << "expected ')' at end of bindings" << eom;
245  return nil_exprt();
246  }
247 
248  // go forwards, add to id_map
249  for(const auto &b : bindings)
250  {
251  auto &entry=id_map[b.get_identifier()];
252  entry.type=b.type();
253  entry.definition=nil_exprt();
254  }
255 
256  exprt expr=expression();
257 
258  if(next_token()!=CLOSE)
259  {
260  error() << "expected ')' after " << id << eom;
261  return nil_exprt();
262  }
263 
264  exprt result=expr;
265 
266  // remove bindings from id_map
267  for(const auto &b : bindings)
268  id_map.erase(b.get_identifier());
269 
270  // go backwards, build quantified expression
271  for(auto r_it=bindings.rbegin(); r_it!=bindings.rend(); r_it++)
272  {
273  binary_predicate_exprt quantifier(id);
274  quantifier.op0()=*r_it;
275  quantifier.op1().swap(result);
276  result=quantifier;
277  }
278 
279  return result;
280 }
281 
283  const irep_idt &identifier,
284  const exprt::operandst &op)
285 {
286  #if 0
287  const auto &f = id_map[identifier];
288 
290 
291  result.function()=symbol_exprt(identifier, f.type);
292  result.arguments()=op;
293 
294  // check the arguments
295  if(op.size()!=f.type.variables().size())
296  {
297  error() << "wrong number of arguments for function" << eom;
298  return nil_exprt();
299  }
300 
301  for(std::size_t i=0; i<op.size(); i++)
302  {
303  if(op[i].type() != f.type.variables()[i].type())
304  {
305  error() << "wrong type for arguments for function" << eom;
306  return result;
307  }
308  }
309 
310  result.type()=f.type.range();
311  return result;
312  #endif
313  return nil_exprt();
314 }
315 
317 {
319 
320  for(auto &expr : result)
321  {
322  if(expr.type().id() == ID_signedbv) // no need to cast
323  {
324  }
325  else if(expr.type().id() != ID_unsignedbv)
326  {
327  error() << "expected unsigned bitvector" << eom;
328  }
329  else
330  {
331  const auto width = to_unsignedbv_type(expr.type()).get_width();
332  expr = typecast_exprt(expr, signedbv_typet(width));
333  }
334  }
335 
336  return result;
337 }
338 
340 {
341  if(expr.type().id()==ID_unsignedbv) // no need to cast
342  return expr;
343 
344  if(expr.type().id()!=ID_signedbv)
345  {
346  error() << "expected signed bitvector" << eom;
347  return expr;
348  }
349 
350  const auto width=to_signedbv_type(expr.type()).get_width();
351  return typecast_exprt(expr, unsignedbv_typet(width));
352 }
353 
355 {
356  if(op.empty())
357  {
358  error() << "expression must have at least one operand" << eom;
359  return nil_exprt();
360  }
361  else
362  {
363  for(std::size_t i=1; i<op.size(); i++)
364  {
365  if(op[i].type()!=op[0].type())
366  {
367  error() << "expression must have operands with matching types,"
368  " but got `"
369  << op[0].type().pretty()
370  << "' and `" << op[i].type().pretty() << '\'' << eom;
371  return nil_exprt();
372  }
373  }
374 
375  exprt result(id, op[0].type());
376  result.operands() = op;
377  return result;
378  }
379 }
380 
382 {
383  if(op.size()!=2)
384  {
385  error() << "expression must have two operands" << eom;
386  return nil_exprt();
387  }
388  else
389  {
390  if(op[0].type()!=op[1].type())
391  {
392  error() << "expression must have operands with matching types,"
393  " but got `"
394  << op[0].type().pretty()
395  << "' and `" << op[1].type().pretty() << '\'' << eom;
396  return nil_exprt();
397  }
398 
399  return binary_predicate_exprt(op[0], id, op[1]);
400  }
401 }
402 
404 {
405  if(op.size()!=1)
406  {
407  error() << "expression must have one operand" << eom;
408  return nil_exprt();
409  }
410  else
411  return unary_exprt(id, op[0], op[0].type());
412 }
413 
415 {
416  if(op.size()!=2)
417  {
418  error() << "expression must have two operands" << eom;
419  return nil_exprt();
420  }
421  else
422  {
423  if(op[0].type()!=op[1].type())
424  {
425  error() << "expression must have operands with matching types" << eom;
426  return nil_exprt();
427  }
428 
429  return binary_exprt(op[0], id, op[1], op[0].type());
430  }
431 }
432 
434 {
435  switch(next_token())
436  {
437  case SYMBOL:
438  if(buffer=="_") // indexed identifier
439  {
440  // indexed identifier
441  if(next_token()!=SYMBOL)
442  {
443  error() << "expected symbol after '_'" << eom;
444  return nil_exprt();
445  }
446 
447  if(has_prefix(buffer, "bv"))
448  {
449  mp_integer i=string2integer(std::string(buffer, 2, std::string::npos));
450 
451  if(next_token()!=NUMERAL)
452  {
453  error() << "expected numeral as bitvector literal width" << eom;
454  return nil_exprt();
455  }
456 
457  auto width=std::stoll(buffer);
458 
459  if(next_token()!=CLOSE)
460  {
461  error() << "expected ')' after bitvector literal" << eom;
462  return nil_exprt();
463  }
464 
465  return from_integer(i, unsignedbv_typet(width));
466  }
467  else
468  {
469  error() << "unknown indexed identifier " << buffer << eom;
470  return nil_exprt();
471  }
472  }
473  else
474  {
475  // non-indexed symbol; hash it
476  const irep_idt id=buffer;
477 
478  if(id==ID_let)
479  return let_expression();
480  else if(id==ID_forall || id==ID_exists)
481  return quantifier_expression(id);
482 
483  auto op=operands();
484 
485  if(id==ID_and ||
486  id==ID_or ||
487  id==ID_xor)
488  {
489  return multi_ary(id, op);
490  }
491  else if(id==ID_not)
492  {
493  return unary(id, op);
494  }
495  else if(id==ID_equal ||
496  id==ID_le ||
497  id==ID_ge ||
498  id==ID_lt ||
499  id==ID_gt)
500  {
501  return binary_predicate(id, op);
502  }
503  else if(id=="bvule")
504  {
505  return binary_predicate(ID_le, op);
506  }
507  else if(id=="bvsle")
508  {
509  return binary_predicate(ID_le, cast_bv_to_signed(op));
510  }
511  else if(id=="bvuge")
512  {
513  return binary_predicate(ID_ge, op);
514  }
515  else if(id=="bvsge")
516  {
517  return binary_predicate(ID_ge, cast_bv_to_signed(op));
518  }
519  else if(id=="bvult")
520  {
521  return binary_predicate(ID_lt, op);
522  }
523  else if(id=="bvslt")
524  {
525  return binary_predicate(ID_lt, cast_bv_to_signed(op));
526  }
527  else if(id=="bvugt")
528  {
529  return binary_predicate(ID_gt, op);
530  }
531  else if(id=="bvsgt")
532  {
533  return binary_predicate(ID_gt, cast_bv_to_signed(op));
534  }
535  else if(id=="bvashr")
536  {
537  return cast_bv_to_unsigned(binary(ID_ashr, cast_bv_to_signed(op)));
538  }
539  else if(id=="bvlshr" || id=="bvshr")
540  {
541  return binary(ID_lshr, op);
542  }
543  else if(id=="bvlshr" || id=="bvashl" || id=="bvshl")
544  {
545  return binary(ID_shl, op);
546  }
547  else if(id=="bvand")
548  {
549  return multi_ary(ID_bitand, op);
550  }
551  else if(id=="bvnand")
552  {
553  return multi_ary(ID_bitnand, op);
554  }
555  else if(id=="bvor")
556  {
557  return multi_ary(ID_bitor, op);
558  }
559  else if(id=="bvnor")
560  {
561  return multi_ary(ID_bitnor, op);
562  }
563  else if(id=="bvxor")
564  {
565  return multi_ary(ID_bitxor, op);
566  }
567  else if(id=="bvxnor")
568  {
569  return multi_ary(ID_bitxnor, op);
570  }
571  else if(id=="bvnot")
572  {
573  return unary(ID_bitnot, op);
574  }
575  else if(id=="bvneg")
576  {
577  return unary(ID_unary_minus, op);
578  }
579  else if(id=="bvadd")
580  {
581  return multi_ary(ID_plus, op);
582  }
583  else if(id==ID_plus)
584  {
585  return multi_ary(id, op);
586  }
587  else if(id=="bvsub" || id=="-")
588  {
589  return binary(ID_minus, op);
590  }
591  else if(id=="bvmul" || id=="*")
592  {
593  return binary(ID_mult, op);
594  }
595  else if(id=="bvsdiv")
596  {
597  return cast_bv_to_unsigned(binary(ID_div, cast_bv_to_signed(op)));
598  }
599  else if(id=="bvudiv")
600  {
601  return binary(ID_div, op);
602  }
603  else if(id=="/" || id=="div")
604  {
605  return binary(ID_div, op);
606  }
607  else if(id=="bvsrem")
608  {
609  // 2's complement signed remainder (sign follows dividend)
610  // This matches our ID_mod, and what C does since C99.
611  return cast_bv_to_unsigned(binary(ID_mod, cast_bv_to_signed(op)));
612  }
613  else if(id=="bvsmod")
614  {
615  // 2's complement signed remainder (sign follows divisor)
616  // We don't have that.
617  return cast_bv_to_unsigned(binary(ID_mod, cast_bv_to_signed(op)));
618  }
619  else if(id=="bvurem" || id=="%")
620  {
621  return binary(ID_mod, op);
622  }
623  else if(id=="concat")
624  {
625  if(op.size()!=2)
626  {
627  error() << "concat takes two operands " << op.size() << eom;
628  return nil_exprt();
629  }
630 
631  auto width0=to_unsignedbv_type(op[0].type()).get_width();
632  auto width1=to_unsignedbv_type(op[1].type()).get_width();
633 
634  unsignedbv_typet t(width0+width1);
635 
636  return binary_exprt(op[0], ID_concatenation, op[1], t);
637  }
638  else if(id=="distinct")
639  {
640  // pair-wise different constraint, multi-ary
641  return multi_ary("distinct", op);
642  }
643  else if(id=="ite")
644  {
645  if(op.size()!=3)
646  {
647  error() << "ite takes three operands" << eom;
648  return nil_exprt();
649  }
650 
651  if(op[0].type().id()!=ID_bool)
652  {
653  error() << "ite takes a boolean as first operand" << eom;
654  return nil_exprt();
655  }
656 
657  if(op[1].type()!=op[2].type())
658  {
659  error() << "ite needs matching types" << eom;
660  return nil_exprt();
661  }
662 
663  return if_exprt(op[0], op[1], op[2]);
664  }
665  else if(id=="=>" || id=="implies")
666  {
667  return binary(ID_implies, op);
668  }
669  else
670  {
671  // rummage through id_map
672  const irep_idt final_id=rename_id(id);
673  auto id_it=id_map.find(final_id);
674  if(id_it!=id_map.end())
675  {
676  if(id_it->second.type.id()==ID_mathematical_function)
677  {
679  app.function()=symbol_exprt(final_id, id_it->second.type);
680  app.arguments()=op;
682  id_it->second.type).codomain();
683  return app;
684  }
685  else
686  return symbol_exprt(final_id, id_it->second.type);
687  }
688 
689  error() << "2 unknown symbol " << id << eom;
690  return nil_exprt();
691  }
692  }
693  break;
694 
695  case OPEN: // likely indexed identifier
696  if(peek()==SYMBOL)
697  {
698  next_token(); // eat symbol
699  if(buffer=="_")
700  {
701  // indexed identifier
702  if(next_token()!=SYMBOL)
703  {
704  error() << "expected symbol after '_'" << eom;
705  return nil_exprt();
706  }
707 
708  irep_idt id=buffer; // hash it
709 
710  if(id=="extract")
711  {
712  if(next_token()!=NUMERAL)
713  {
714  error() << "expected numeral after extract" << eom;
715  return nil_exprt();
716  }
717 
718  auto upper=std::stoll(buffer);
719 
720  if(next_token()!=NUMERAL)
721  {
722  error() << "expected two numerals after extract" << eom;
723  return nil_exprt();
724  }
725 
726  auto lower=std::stoll(buffer);
727 
728  if(next_token()!=CLOSE)
729  {
730  error() << "expected ')' after extract" << eom;
731  return nil_exprt();
732  }
733 
734  auto op=operands();
735 
736  if(op.size()!=1)
737  {
738  error() << "extract takes one operand" << eom;
739  return nil_exprt();
740  }
741 
742  auto upper_e=from_integer(upper, integer_typet());
743  auto lower_e=from_integer(lower, integer_typet());
744 
745  if(upper<lower)
746  {
747  error() << "extract got bad indices" << eom;
748  return nil_exprt();
749  }
750 
751  unsignedbv_typet t(upper-lower+1);
752 
753  return extractbits_exprt(op[0], upper_e, lower_e, t);
754  }
755  else if(id=="rotate_left" ||
756  id=="rotate_right" ||
757  id == ID_repeat ||
758  id=="sign_extend" ||
759  id=="zero_extend")
760  {
761  if(next_token()!=NUMERAL)
762  {
763  error() << "expected numeral after " << id << eom;
764  return nil_exprt();
765  }
766 
767  auto index=std::stoll(buffer);
768 
769  if(next_token()!=CLOSE)
770  {
771  error() << "expected ')' after " << id << " index" << eom;
772  return nil_exprt();
773  }
774 
775  auto op=operands();
776 
777  if(op.size()!=1)
778  {
779  error() << id << " takes one operand" << eom;
780  return nil_exprt();
781  }
782 
783  if(id=="rotate_left")
784  {
785  auto dist=from_integer(index, integer_typet());
786  return binary_exprt(op[0], ID_rol, dist, op[0].type());
787  }
788  else if(id=="rotate_right")
789  {
790  auto dist=from_integer(index, integer_typet());
791  return binary_exprt(op[0], ID_ror, dist, op[0].type());
792  }
793  else if(id=="sign_extend")
794  {
795  auto width=to_unsignedbv_type(op[0].type()).get_width();
796  signedbv_typet signed_type(width+index);
797  unsignedbv_typet unsigned_type(width+index);
798 
799  return typecast_exprt(
800  typecast_exprt(op[0], signed_type), unsigned_type);
801  }
802  else if(id=="zero_extend")
803  {
804  auto width=to_unsignedbv_type(op[0].type()).get_width();
805  unsignedbv_typet unsigned_type(width+index);
806 
807  return typecast_exprt(op[0], unsigned_type);
808  }
809  else if(id == ID_repeat)
810  {
811  return nil_exprt();
812  }
813  else
814  return nil_exprt();
815  }
816  else
817  {
818  error() << "unknown indexed identifier " << buffer << eom;
819  return nil_exprt();
820  }
821  }
822  else
823  {
824  // just double parentheses
825  error() << "expected symbol or indexed identifier "
826  "after '(' in an expression" << eom;
827 
828  exprt tmp=expression();
829 
830  if(next_token()!=CLOSE && next_token()!=CLOSE)
831  error() << "mismatched parentheses in an expression" << eom;
832 
833  return tmp;
834  }
835  }
836  else
837  {
838  // just double parentheses
839  error() << "expected symbol or indexed identifier "
840  "after '(' in an expression" << eom;
841 
842  exprt tmp=expression();
843 
844  if(next_token()!=CLOSE && next_token()!=CLOSE)
845  error() << "mismatched parentheses in an expression" << eom;
846 
847  return tmp;
848  }
849  break;
850 
851  default:
852  // just parentheses
853  error() << "expected symbol or indexed identifier "
854  "after '(' in an expression" << eom;
855 
856  exprt tmp=expression();
857  if(next_token()!=CLOSE)
858  error() << "mismatched parentheses in an expression" << eom;
859 
860  return tmp;
861  }
862 }
863 
865 {
866  switch(next_token())
867  {
868  case SYMBOL:
869  {
870  // hash it
871  const irep_idt identifier=buffer;
872 
873  if(identifier==ID_true)
874  return true_exprt();
875  else if(identifier==ID_false)
876  return false_exprt();
877  else
878  {
879  // rummage through id_map
880  const irep_idt final_id=rename_id(identifier);
881  auto id_it=id_map.find(final_id);
882  if(id_it!=id_map.end())
883  return symbol_exprt(final_id, id_it->second.type);
884 
885  error() << "1 unknown symbol " << identifier << eom;
886  return nil_exprt();
887  }
888  }
889 
890  case NUMERAL:
891  if(buffer.size()>=2 && buffer[0]=='#' && buffer[1]=='x')
892  {
893  mp_integer value=
894  string2integer(std::string(buffer, 2, std::string::npos), 16);
895  const std::size_t width = 4*(buffer.size() - 2);
896  CHECK_RETURN(width!=0 && width%4==0);
897  unsignedbv_typet type(width);
898  return from_integer(value, type);
899  }
900  else if(buffer.size()>=2 && buffer[0]=='#' && buffer[1]=='b')
901  {
902  mp_integer value=
903  string2integer(std::string(buffer, 2, std::string::npos), 2);
904  const std::size_t width = buffer.size() - 2;
905  CHECK_RETURN(width!=0);
906  unsignedbv_typet type(width);
907  return from_integer(value, type);
908  }
909  else
910  {
912  }
913 
914  case OPEN: // function application
915  return function_application();
916 
917  case END_OF_FILE:
918  error() << "EOF in an expression" << eom;
919  return nil_exprt();
920 
921  default:
922  error() << "unexpected token in an expression" << eom;
923  return nil_exprt();
924  }
925 }
926 
928 {
929  switch(next_token())
930  {
931  case SYMBOL:
932  if(buffer=="Bool")
933  return bool_typet();
934  else if(buffer=="Int")
935  return integer_typet();
936  else if(buffer=="Real")
937  return real_typet();
938  else
939  {
940  error() << "unexpected sort: `" << buffer << '\'' << eom;
941  return nil_typet();
942  }
943 
944  case OPEN:
945  if(next_token()!=SYMBOL)
946  {
947  error() << "expected symbol after '(' in a sort " << eom;
948  return nil_typet();
949  }
950 
951  if(buffer=="_")
952  {
953  // indexed identifier
954  if(next_token()!=SYMBOL)
955  {
956  error() << "expected symbol after '_' in a sort" << eom;
957  return nil_typet();
958  }
959 
960  if(buffer=="BitVec")
961  {
962  if(next_token()!=NUMERAL)
963  {
964  error() << "expected numeral as bit-width" << eom;
965  return nil_typet();
966  }
967 
968  auto width=std::stoll(buffer);
969 
970  // eat the ')'
971  if(next_token()!=CLOSE)
972  {
973  error() << "expected ')' at end of sort" << eom;
974  return nil_typet();
975  }
976 
977  return unsignedbv_typet(width);
978  }
979  else
980  {
981  error() << "unexpected sort: `" << buffer << '\'' << eom;
982  return nil_typet();
983  }
984  }
985  else
986  {
987  error() << "unexpected sort: `" << buffer << '\'' << eom;
988  return nil_typet();
989  }
990 
991  default:
992  error() << "unexpected token in a sort " << buffer << eom;
993  return nil_typet();
994  }
995 }
996 
998 {
999  if(next_token()!=OPEN)
1000  {
1001  error() << "expected '(' at beginning of signature" << eom;
1002  return nil_typet();
1003  }
1004 
1005  if(peek()==CLOSE)
1006  {
1007  next_token(); // eat the ')'
1008  return sort();
1009  }
1010 
1012 
1013  while(peek()!=CLOSE)
1014  {
1015  if(next_token()!=OPEN)
1016  {
1017  error() << "expected '(' at beginning of parameter" << eom;
1018  return nil_typet();
1019  }
1020 
1021  if(next_token()!=SYMBOL)
1022  {
1023  error() << "expected symbol in parameter" << eom;
1024  return nil_typet();
1025  }
1026 
1028  std::string id=buffer;
1029  var.set_identifier(id);
1030  var.type()=sort();
1031  domain.push_back(var);
1032 
1033  auto &entry=id_map[id];
1034  entry.type=var.type();
1035  entry.definition=nil_exprt();
1036 
1037  if(next_token()!=CLOSE)
1038  {
1039  error() << "expected ')' at end of parameter" << eom;
1040  return nil_typet();
1041  }
1042  }
1043 
1044  next_token(); // eat the ')'
1045 
1046  typet codomain = sort();
1047 
1048  return mathematical_function_typet(domain, codomain);
1049 }
1050 
1052 {
1053  if(next_token()!=OPEN)
1054  {
1055  error() << "expected '(' at beginning of signature" << eom;
1056  return nil_typet();
1057  }
1058 
1059  if(peek()==CLOSE)
1060  {
1061  next_token(); // eat the ')'
1062  return sort();
1063  }
1064 
1066 
1067  while(peek()!=CLOSE)
1068  {
1069  if(next_token()!=OPEN)
1070  {
1071  error() << "expected '(' at beginning of parameter" << eom;
1072  return nil_typet();
1073  }
1074 
1075  if(next_token()!=SYMBOL)
1076  {
1077  error() << "expected symbol in parameter" << eom;
1078  return nil_typet();
1079  }
1080 
1082  var.type()=sort();
1083  domain.push_back(var);
1084 
1085  if(next_token()!=CLOSE)
1086  {
1087  error() << "expected ')' at end of parameter" << eom;
1088  return nil_typet();
1089  }
1090  }
1091 
1092  next_token(); // eat the ')'
1093 
1094  typet codomain = sort();
1095 
1096  return mathematical_function_typet(domain, codomain);
1097 }
1098 
1099 void smt2_parsert::command(const std::string &c)
1100 {
1101  if(c=="declare-const")
1102  {
1103  if(next_token()!=SYMBOL)
1104  {
1105  error() << "expected a symbol after declare-const" << eom;
1106  ignore_command();
1107  return;
1108  }
1109 
1110  irep_idt id=buffer;
1111 
1112  if(id_map.find(id)!=id_map.end())
1113  {
1114  error() << "identifier `" << id << "' defined twice" << eom;
1115  ignore_command();
1116  return;
1117  }
1118 
1119  auto &entry=id_map[id];
1120  entry.type=sort();
1121  entry.definition=nil_exprt();
1122  }
1123  else if(c=="declare-fun")
1124  {
1125  if(next_token()!=SYMBOL)
1126  {
1127  error() << "expected a symbol after declare-fun" << eom;
1128  ignore_command();
1129  return;
1130  }
1131 
1132  irep_idt id=buffer;
1133 
1134  if(id_map.find(id)!=id_map.end())
1135  {
1136  error() << "identifier `" << id << "' defined twice" << eom;
1137  ignore_command();
1138  return;
1139  }
1140 
1141  auto &entry=id_map[id];
1142  entry.type=function_signature_declaration();
1143  entry.definition=nil_exprt();
1144  }
1145  else if(c=="define-fun")
1146  {
1147  if(next_token()!=SYMBOL)
1148  {
1149  error() << "expected a symbol after define-fun" << eom;
1150  ignore_command();
1151  return;
1152  }
1153 
1154  const irep_idt id=buffer;
1155 
1156  if(id_map.find(id)!=id_map.end())
1157  {
1158  error() << "identifier `" << id << "' defined twice" << eom;
1159  ignore_command();
1160  return;
1161  }
1162 
1163  // create the entry
1164  id_map[id];
1165 
1166  auto signature=function_signature_definition();
1167  exprt body=expression();
1168 
1169  // set up the entry
1170  auto &entry=id_map[id];
1171  entry.type=signature;
1172  entry.definition=body;
1173  }
1174  else if(c=="exit")
1175  {
1176  exit=true;
1177  }
1178  else
1179  ignore_command();
1180 }
The type of an expression.
Definition: type.h:22
Fixed-width bit-vector with unsigned binary interpretation.
Definition: std_types.h:1220
semantic type conversion
Definition: std_expr.h:2111
BigInt mp_integer
Definition: mp_arith.h:22
const std::string & id2string(const irep_idt &d)
Definition: irep.h:43
application of (mathematical) function
Definition: std_expr.h:4531
const mp_integer string2integer(const std::string &n, unsigned base)
Definition: mp_arith.cpp:57
const signedbv_typet & to_signedbv_type(const typet &type)
Cast a generic typet to a signedbv_typet.
Definition: std_types.h:1287
renaming_mapt renaming_map
Definition: smt2_parser.h:54
typet function_signature_declaration()
exprt & op0()
Definition: expr.h:72
exprt quantifier_expression(irep_idt)
irep_idt get_fresh_id(const irep_idt &)
Definition: smt2_parser.cpp:94
argumentst & arguments()
Definition: std_expr.h:4564
std::vector< variablet > domaint
Definition: std_types.h:1748
The trinary if-then-else operator.
Definition: std_expr.h:3361
typet & type()
Definition: expr.h:56
The proper Booleans.
Definition: std_types.h:34
A constant literal expression.
Definition: std_expr.h:4424
#define CHECK_RETURN(CONDITION)
Definition: invariant.h:245
static mstreamt & eom(mstreamt &m)
Definition: message.h:272
exprt cast_bv_to_unsigned(const exprt &)
Apply typecast to unsignedbv to given expression.
exprt & where()
Definition: std_expr.h:4734
exprt::operandst operands()
Definition: smt2_parser.cpp:82
const irep_idt & id() const
Definition: irep.h:189
renaming_counterst renaming_counters
Definition: smt2_parser.h:56
exprt binary_predicate(irep_idt, const exprt::operandst &)
The boolean constant true.
Definition: std_expr.h:4488
A generic base class for binary expressions.
Definition: std_expr.h:649
A type for mathematical functions (do not confuse with functions/methods in code) ...
Definition: std_types.h:1718
The NIL expression.
Definition: std_expr.h:4510
void ignore_command()
Definition: smt2_parser.cpp:53
Fixed-width bit-vector with two&#39;s complement interpretation.
Definition: std_types.h:1262
void set_identifier(const irep_idt &identifier)
Definition: std_types.h:1732
Extracts a sub-range of a bit-vector operand.
Definition: std_expr.h:3072
exprt & op1()
Definition: expr.h:75
Generic base class for unary expressions.
Definition: std_expr.h:303
std::map< irep_idt, irep_idt > renaming_mapt
Definition: smt2_parser.h:53
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()
typet function_signature_definition()
The boolean constant false.
Definition: std_expr.h:4499
std::size_t get_width() const
Definition: std_types.h:1129
exprt expression()
symbol_exprt & function()
Definition: std_expr.h:4552
id_mapt id_map
Definition: smt2_parser.h:44
std::vector< exprt > operandst
Definition: expr.h:45
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 generic typet to an unsignedbv_typet.
Definition: std_types.h:1245
Unbounded, signed integers.
Definition: std_types.h:70
exprt & value()
Definition: std_expr.h:4724
virtual void command(const std::string &)
mstreamt & result() const
Definition: message.h:312
Unbounded, signed real numbers.
Definition: std_types.h:100
std::string buffer
exprt binary(irep_idt, const exprt::operandst &)
Base class for all expressions.
Definition: expr.h:42
std::string to_string(const string_constraintt &expr)
Used for debug printing.
#define CLOSE
Definition: xml_y.tab.cpp:147
The NIL type.
Definition: std_types.h:44
void swap(irept &irep)
Definition: irep.h:231
exprt::operandst cast_bv_to_signed(const exprt::operandst &)
Apply typecast to signedbv to expressions in vector.
exprt function_application()
Expression to hold a symbol (variable)
Definition: std_expr.h:90
symbol_exprt & symbol()
Definition: std_expr.h:4714
void command_sequence()
Definition: smt2_parser.cpp:13
A generic base class for expressions that are predicates, i.e., boolean-typed, and that take exactly ...
Definition: std_expr.h:730
A let expression.
Definition: std_expr.h:4705
const mathematical_function_typet & to_mathematical_function_type(const typet &type)
Cast a generic typet to a mathematical_function_typet.
Definition: std_types.h:1799
constant_exprt from_integer(const mp_integer &int_value, const typet &type)
mstreamt & error()