cprover
Loading...
Searching...
No Matches
smt2_parser.cpp
Go to the documentation of this file.
1/*******************************************************************\
2
3Module:
4
5Author: Daniel Kroening, kroening@kroening.com
6
7\*******************************************************************/
8
9#include "smt2_parser.h"
10
11#include "smt2_format.h"
12
13#include <util/arith_tools.h>
14#include <util/bitvector_expr.h>
16#include <util/floatbv_expr.h>
17#include <util/ieee_float.h>
18#include <util/invariant.h>
20#include <util/prefix.h>
21#include <util/range.h>
22
23#include <numeric>
24
26{
27 const auto token = smt2_tokenizer.next_token();
28
29 if(token == smt2_tokenizert::OPEN)
31 else if(token == smt2_tokenizert::CLOSE)
33
34 return token;
35}
36
38{
39 while(parenthesis_level > 0)
40 if(next_token() == smt2_tokenizert::END_OF_FILE)
41 return;
42}
43
45{
46 exit=false;
47
48 while(!exit)
49 {
50 if(smt2_tokenizer.peek() == smt2_tokenizert::END_OF_FILE)
51 {
52 exit = true;
53 return;
54 }
55
56 if(next_token() != smt2_tokenizert::OPEN)
57 throw error("command must start with '('");
58
59 if(next_token() != smt2_tokenizert::SYMBOL)
60 {
62 throw error("expected symbol as command");
63 }
64
66
67 switch(next_token())
68 {
69 case smt2_tokenizert::END_OF_FILE:
70 throw error(
71 "expected closing parenthesis at end of command,"
72 " but got EOF");
73
74 case smt2_tokenizert::CLOSE:
75 // what we expect
76 break;
77
78 case smt2_tokenizert::OPEN:
79 case smt2_tokenizert::SYMBOL:
80 case smt2_tokenizert::NUMERAL:
81 case smt2_tokenizert::STRING_LITERAL:
82 case smt2_tokenizert::NONE:
83 case smt2_tokenizert::KEYWORD:
84 throw error("expected ')' at end of command");
85 }
86 }
87}
88
90{
91 std::size_t parentheses=0;
92 while(true)
93 {
94 switch(smt2_tokenizer.peek())
95 {
96 case smt2_tokenizert::OPEN:
97 next_token();
99 break;
100
101 case smt2_tokenizert::CLOSE:
102 if(parentheses==0)
103 return; // done
104
105 next_token();
106 parentheses--;
107 break;
108
109 case smt2_tokenizert::END_OF_FILE:
110 throw error("unexpected EOF in command");
111
112 case smt2_tokenizert::SYMBOL:
113 case smt2_tokenizert::NUMERAL:
114 case smt2_tokenizert::STRING_LITERAL:
115 case smt2_tokenizert::NONE:
116 case smt2_tokenizert::KEYWORD:
117 next_token();
118 }
119 }
120}
121
123{
124 exprt::operandst result;
125
126 while(smt2_tokenizer.peek() != smt2_tokenizert::CLOSE)
127 result.push_back(expression());
128
129 next_token(); // eat the ')'
130
131 return result;
132}
133
135{
136 if(!id_map
137 .emplace(
138 std::piecewise_construct,
139 std::forward_as_tuple(id),
140 std::forward_as_tuple(idt::VARIABLE, std::move(expr)))
141 .second)
142 {
143 // id already used
144 throw error() << "identifier '" << id << "' defined twice";
145 }
146}
147
149{
150 if(next_token() != smt2_tokenizert::OPEN)
151 throw error("expected bindings after let");
152
153 std::vector<std::pair<irep_idt, exprt>> bindings;
154
155 while(smt2_tokenizer.peek() == smt2_tokenizert::OPEN)
156 {
157 next_token();
158
159 if(next_token() != smt2_tokenizert::SYMBOL)
160 throw error("expected symbol in binding");
161
162 irep_idt identifier = smt2_tokenizer.get_buffer();
163
164 // note that the previous bindings are _not_ visible yet
165 exprt value=expression();
166
167 if(next_token() != smt2_tokenizert::CLOSE)
168 throw error("expected ')' after value in binding");
169
170 bindings.push_back(
171 std::pair<irep_idt, exprt>(identifier, value));
172 }
173
174 if(next_token() != smt2_tokenizert::CLOSE)
175 throw error("expected ')' at end of bindings");
176
177 // we may hide identifiers in outer scopes
178 std::vector<std::pair<irep_idt, idt>> saved_ids;
179
180 // add the bindings to the id_map
181 for(auto &b : bindings)
182 {
183 auto insert_result = id_map.insert({b.first, idt{idt::BINDING, b.second}});
184 if(!insert_result.second) // already there
185 {
186 auto &id_entry = *insert_result.first;
187 saved_ids.emplace_back(id_entry.first, std::move(id_entry.second));
188 id_entry.second = idt{idt::BINDING, b.second};
189 }
190 }
191
192 // now parse, with bindings in place
193 exprt where = expression();
194
195 if(next_token() != smt2_tokenizert::CLOSE)
196 throw error("expected ')' after let");
197
199 exprt::operandst values;
200
201 for(const auto &b : bindings)
202 {
203 variables.push_back(symbol_exprt(b.first, b.second.type()));
204 values.push_back(b.second);
205 }
206
207 // delete the bindings from the id_map
208 for(const auto &binding : bindings)
209 id_map.erase(binding.first);
210
211 // restore any previous ids
212 for(auto &saved_id : saved_ids)
213 id_map.insert(std::move(saved_id));
214
215 return let_exprt(variables, values, where);
216}
217
218std::pair<binding_exprt::variablest, exprt> smt2_parsert::binding(irep_idt id)
219{
220 if(next_token() != smt2_tokenizert::OPEN)
221 throw error() << "expected bindings after " << id;
222
224
225 while(smt2_tokenizer.peek() == smt2_tokenizert::OPEN)
226 {
227 next_token();
228
229 if(next_token() != smt2_tokenizert::SYMBOL)
230 throw error("expected symbol in binding");
231
232 irep_idt identifier = smt2_tokenizer.get_buffer();
233
234 typet type=sort();
235
236 if(next_token() != smt2_tokenizert::CLOSE)
237 throw error("expected ')' after sort in binding");
238
239 bindings.push_back(symbol_exprt(identifier, type));
240 }
241
242 if(next_token() != smt2_tokenizert::CLOSE)
243 throw error("expected ')' at end of bindings");
244
245 // we may hide identifiers in outer scopes
246 std::vector<std::pair<irep_idt, idt>> saved_ids;
247
248 // add the bindings to the id_map
249 for(auto &b : bindings)
250 {
251 auto insert_result =
252 id_map.insert({b.get_identifier(), idt{idt::BINDING, b.type()}});
253 if(!insert_result.second) // already there
254 {
255 auto &id_entry = *insert_result.first;
256 saved_ids.emplace_back(id_entry.first, std::move(id_entry.second));
257 id_entry.second = idt{idt::BINDING, b.type()};
258 }
259 }
260
261 // now parse, with bindings in place
262 exprt expr=expression();
263
264 if(next_token() != smt2_tokenizert::CLOSE)
265 throw error() << "expected ')' after " << id;
266
267 // remove bindings from id_map
268 for(const auto &b : bindings)
269 id_map.erase(b.get_identifier());
270
271 // restore any previous ids
272 for(auto &saved_id : saved_ids)
273 id_map.insert(std::move(saved_id));
274
275 return {std::move(bindings), std::move(expr)};
276}
277
279{
280 auto binding = this->binding(ID_lambda);
281 return lambda_exprt(binding.first, binding.second);
282}
283
285{
286 auto binding = this->binding(id);
287
288 if(!binding.second.is_boolean())
289 throw error() << id << " expects a boolean term";
290
291 return quantifier_exprt(id, binding.first, binding.second);
292}
293
295 const symbol_exprt &function,
296 const exprt::operandst &op)
297{
298 const auto &function_type = to_mathematical_function_type(function.type());
299
300 // check the arguments
301 if(op.size() != function_type.domain().size())
302 throw error("wrong number of arguments for function");
303
304 for(std::size_t i=0; i<op.size(); i++)
305 {
306 if(op[i].type() != function_type.domain()[i])
307 throw error("wrong type for arguments for function");
308 }
309
310 return function_application_exprt(function, op);
311}
312
314{
315 exprt::operandst result = op;
316
317 for(auto &expr : result)
318 {
319 if(expr.type().id() == ID_signedbv) // no need to cast
320 {
321 }
322 else if(expr.type().id() != ID_unsignedbv)
323 {
324 throw error("expected unsigned bitvector");
325 }
326 else
327 {
328 const auto width = to_unsignedbv_type(expr.type()).get_width();
329 expr = typecast_exprt(expr, signedbv_typet(width));
330 }
331 }
332
333 return result;
334}
335
337{
338 if(expr.type().id()==ID_unsignedbv) // no need to cast
339 return expr;
340
341 if(expr.type().id()!=ID_signedbv)
342 throw error("expected signed bitvector");
343
344 const auto width=to_signedbv_type(expr.type()).get_width();
345 return typecast_exprt(expr, unsignedbv_typet(width));
346}
347
349 const exprt::operandst &op) const
350{
351 for(std::size_t i = 1; i < op.size(); i++)
352 {
353 if(op[i].type() != op[0].type())
354 {
355 throw error() << "expression must have operands with matching types,"
356 " but got '"
357 << smt2_format(op[0].type()) << "' and '"
358 << smt2_format(op[i].type()) << '\'';
359 }
360 }
361}
362
364{
365 if(op.empty())
366 throw error("expression must have at least one operand");
367
369
370 exprt result(id, op[0].type());
371 result.operands() = op;
372 return result;
373}
374
376{
377 if(op.size()!=2)
378 throw error("expression must have two operands");
379
381
382 return binary_predicate_exprt(op[0], id, op[1]);
383}
384
386{
387 if(op.size()!=1)
388 throw error("expression must have one operand");
389
390 return unary_exprt(id, op[0], op[0].type());
391}
392
394{
395 if(op.size()!=2)
396 throw error("expression must have two operands");
397
399
400 return binary_exprt(op[0], id, op[1], op[0].type());
401}
402
404 const exprt::operandst &op)
405{
406 if(op.size() != 2)
407 throw error() << "FloatingPoint equality takes two operands";
408
409 if(op[0].type().id() != ID_floatbv || op[1].type().id() != ID_floatbv)
410 throw error() << "FloatingPoint equality takes FloatingPoint operands";
411
412 if(op[0].type() != op[1].type())
413 {
414 throw error() << "FloatingPoint equality takes FloatingPoint operands with "
415 << "matching sort, but got " << smt2_format(op[0].type())
416 << " vs " << smt2_format(op[1].type());
417 }
418
419 return ieee_float_equal_exprt(op[0], op[1]);
420}
421
423 const irep_idt &id,
424 const exprt::operandst &op)
425{
426 if(op.size() != 3)
427 throw error() << id << " takes three operands";
428
429 if(op[1].type().id() != ID_floatbv || op[2].type().id() != ID_floatbv)
430 throw error() << id << " takes FloatingPoint operands";
431
432 if(op[1].type() != op[2].type())
433 {
434 throw error() << id << " takes FloatingPoint operands with matching sort, "
435 << "but got " << smt2_format(op[1].type()) << " vs "
436 << smt2_format(op[2].type());
437 }
438
439 // clang-format off
440 const irep_idt expr_id =
441 id == "fp.add" ? ID_floatbv_plus :
442 id == "fp.sub" ? ID_floatbv_minus :
443 id == "fp.mul" ? ID_floatbv_mult :
444 id == "fp.div" ? ID_floatbv_div :
445 throw error("unsupported floating-point operation");
446 // clang-format on
447
448 return ieee_float_op_exprt(op[1], expr_id, op[2], op[0]);
449}
450
452{
453 // floating-point from bit-vectors
454 if(op.size() != 3)
455 throw error("fp takes three operands");
456
457 if(op[0].type().id() != ID_unsignedbv)
458 throw error("fp takes BitVec as first operand");
459
460 if(op[1].type().id() != ID_unsignedbv)
461 throw error("fp takes BitVec as second operand");
462
463 if(op[2].type().id() != ID_unsignedbv)
464 throw error("fp takes BitVec as third operand");
465
466 if(to_unsignedbv_type(op[0].type()).get_width() != 1)
467 throw error("fp takes BitVec of size 1 as first operand");
468
469 const auto width_e = to_unsignedbv_type(op[1].type()).get_width();
470 const auto width_f = to_unsignedbv_type(op[2].type()).get_width();
471
472 // stitch the bits together
473 const auto concat_type = unsignedbv_typet(width_f + width_e + 1);
474
475 // We need a bitvector type without numerical interpretation
476 // to do this conversion.
477 const auto bv_type = bv_typet(concat_type.get_width());
478
479 // The target type
481
482 return typecast_exprt(
485 fp_type);
486}
487
489{
490 switch(next_token())
491 {
492 case smt2_tokenizert::SYMBOL:
493 if(smt2_tokenizer.get_buffer() == "_") // indexed identifier
494 {
495 // indexed identifier
496 if(next_token() != smt2_tokenizert::SYMBOL)
497 throw error("expected symbol after '_'");
498
499 // copy, the reference won't be stable
500 const auto id = smt2_tokenizer.get_buffer();
501
502 if(has_prefix(id, "bv"))
503 {
505 std::string(smt2_tokenizer.get_buffer(), 2, std::string::npos));
506
507 if(next_token() != smt2_tokenizert::NUMERAL)
508 throw error("expected numeral as bitvector literal width");
509
510 auto width = std::stoll(smt2_tokenizer.get_buffer());
511
512 if(next_token() != smt2_tokenizert::CLOSE)
513 throw error("expected ')' after bitvector literal");
514
515 return from_integer(i, unsignedbv_typet(width));
516 }
517 else if(id == "+oo" || id == "-oo" || id == "NaN")
518 {
519 // These are the "plus infinity", "minus infinity" and NaN
520 // floating-point literals.
521 if(next_token() != smt2_tokenizert::NUMERAL)
522 throw error() << "expected number after " << id;
523
524 auto width_e = std::stoll(smt2_tokenizer.get_buffer());
525
526 if(next_token() != smt2_tokenizert::NUMERAL)
527 throw error() << "expected second number after " << id;
528
529 auto width_f = std::stoll(smt2_tokenizer.get_buffer());
530
531 if(next_token() != smt2_tokenizert::CLOSE)
532 throw error() << "expected ')' after " << id;
533
534 // width_f *includes* the hidden bit
535 const ieee_float_spect spec(width_f - 1, width_e);
536
537 if(id == "+oo")
538 return ieee_floatt::plus_infinity(spec).to_expr();
539 else if(id == "-oo")
540 return ieee_floatt::minus_infinity(spec).to_expr();
541 else // NaN
542 return ieee_floatt::NaN(spec).to_expr();
543 }
544 else
545 {
546 throw error() << "unknown indexed identifier " << id;
547 }
548 }
549 else if(smt2_tokenizer.get_buffer() == "!")
550 {
551 // these are "term attributes"
552 const auto term = expression();
553
554 while(smt2_tokenizer.peek() == smt2_tokenizert::KEYWORD)
555 {
556 next_token(); // eat the keyword
557 if(smt2_tokenizer.get_buffer() == "named")
558 {
559 // 'named terms' must be Boolean
560 if(!term.is_boolean())
561 throw error("named terms must be Boolean");
562
563 if(next_token() == smt2_tokenizert::SYMBOL)
564 {
565 const symbol_exprt symbol_expr(
567 named_terms.emplace(
568 symbol_expr.get_identifier(), named_termt(term, symbol_expr));
569 }
570 else
571 throw error("invalid name attribute, expected symbol");
572 }
573 else
574 throw error("unknown term attribute");
575 }
576
577 if(next_token() != smt2_tokenizert::CLOSE)
578 throw error("expected ')' at end of term attribute");
579 else
580 return term;
581 }
582 else
583 {
584 // non-indexed symbol, look up in expression table
585 const auto id = smt2_tokenizer.get_buffer();
586 const auto e_it = expressions.find(id);
587 if(e_it != expressions.end())
588 return e_it->second();
589
590 // get the operands
591 auto op = operands();
592
593 // rummage through id_map
594 auto id_it = id_map.find(id);
595 if(id_it != id_map.end())
596 {
597 if(id_it->second.type.id() == ID_mathematical_function)
598 {
599 return function_application(symbol_exprt(id, id_it->second.type), op);
600 }
601 else
602 return symbol_exprt(id, id_it->second.type);
603 }
604 else
605 throw error() << "unknown function symbol '" << id << '\'';
606 }
607 break;
608
609 case smt2_tokenizert::OPEN: // likely indexed identifier
610 if(smt2_tokenizer.peek() == smt2_tokenizert::SYMBOL)
611 {
612 next_token(); // eat symbol
613 if(smt2_tokenizer.get_buffer() == "_")
614 {
615 // indexed identifier
616 if(next_token() != smt2_tokenizert::SYMBOL)
617 throw error("expected symbol after '_'");
618
619 irep_idt id = smt2_tokenizer.get_buffer(); // hash it
620
621 if(id=="extract")
622 {
623 if(next_token() != smt2_tokenizert::NUMERAL)
624 throw error("expected numeral after extract");
625
626 auto upper = std::stoll(smt2_tokenizer.get_buffer());
627
628 if(next_token() != smt2_tokenizert::NUMERAL)
629 throw error("expected two numerals after extract");
630
631 auto lower = std::stoll(smt2_tokenizer.get_buffer());
632
633 if(next_token() != smt2_tokenizert::CLOSE)
634 throw error("expected ')' after extract");
635
636 auto op=operands();
637
638 if(op.size()!=1)
639 throw error("extract takes one operand");
640
641 auto upper_e=from_integer(upper, integer_typet());
642 auto lower_e=from_integer(lower, integer_typet());
643
644 if(upper<lower)
645 throw error("extract got bad indices");
646
647 unsignedbv_typet t(upper-lower+1);
648
649 return extractbits_exprt(op[0], upper_e, lower_e, t);
650 }
651 else if(id=="rotate_left" ||
652 id=="rotate_right" ||
653 id == ID_repeat ||
654 id=="sign_extend" ||
655 id=="zero_extend")
656 {
657 if(next_token() != smt2_tokenizert::NUMERAL)
658 throw error() << "expected numeral after " << id;
659
660 auto index = std::stoll(smt2_tokenizer.get_buffer());
661
662 if(next_token() != smt2_tokenizert::CLOSE)
663 throw error() << "expected ')' after " << id << " index";
664
665 auto op=operands();
666
667 if(op.size()!=1)
668 throw error() << id << " takes one operand";
669
670 if(id=="rotate_left")
671 {
672 auto dist=from_integer(index, integer_typet());
673 return binary_exprt(op[0], ID_rol, dist, op[0].type());
674 }
675 else if(id=="rotate_right")
676 {
677 auto dist=from_integer(index, integer_typet());
678 return binary_exprt(op[0], ID_ror, dist, op[0].type());
679 }
680 else if(id=="sign_extend")
681 {
682 // we first convert to a signed type of the original width,
683 // then extend to the new width, and then go to unsigned
684 const auto width = to_unsignedbv_type(op[0].type()).get_width();
686 const signedbv_typet large_signed_type(width + index);
687 const unsignedbv_typet unsigned_type(width + index);
688
689 return typecast_exprt(
693 }
694 else if(id=="zero_extend")
695 {
696 auto width=to_unsignedbv_type(op[0].type()).get_width();
697 unsignedbv_typet unsigned_type(width+index);
698
699 return typecast_exprt(op[0], unsigned_type);
700 }
701 else if(id == ID_repeat)
702 {
703 auto i = from_integer(index, integer_typet());
704 auto width = to_unsignedbv_type(op[0].type()).get_width() * index;
705 return replication_exprt(i, op[0], unsignedbv_typet(width));
706 }
707 else
708 return nil_exprt();
709 }
710 else if(id == "to_fp")
711 {
712 if(next_token() != smt2_tokenizert::NUMERAL)
713 throw error("expected number after to_fp");
714
715 auto width_e = std::stoll(smt2_tokenizer.get_buffer());
716
717 if(next_token() != smt2_tokenizert::NUMERAL)
718 throw error("expected second number after to_fp");
719
720 auto width_f = std::stoll(smt2_tokenizer.get_buffer());
721
722 if(next_token() != smt2_tokenizert::CLOSE)
723 throw error("expected ')' after to_fp");
724
725 // width_f *includes* the hidden bit
726 const ieee_float_spect spec(width_f - 1, width_e);
727
728 auto rounding_mode = expression();
729
730 auto source_op = expression();
731
732 if(next_token() != smt2_tokenizert::CLOSE)
733 throw error("expected ')' at the end of to_fp");
734
735 // There are several options for the source operand:
736 // 1) real or integer
737 // 2) bit-vector, which is interpreted as signed 2's complement
738 // 3) another floating-point format
739 if(
740 source_op.type().id() == ID_real ||
741 source_op.type().id() == ID_integer)
742 {
743 // For now, we can only do this when
744 // the source operand is a constant.
745 if(source_op.is_constant())
746 {
747 mp_integer significand, exponent;
748
749 const auto &real_number =
751 auto dot_pos = real_number.find('.');
752 if(dot_pos == std::string::npos)
753 {
754 exponent = 0;
755 significand = string2integer(real_number);
756 }
757 else
758 {
759 // remove the '.'
760 std::string significand_str;
761 significand_str.reserve(real_number.size());
762 for(auto ch : real_number)
763 {
764 if(ch != '.')
766 }
767
768 exponent =
770 significand = string2integer(significand_str);
771 }
772
774 spec,
775 static_cast<ieee_floatt::rounding_modet>(
776 numeric_cast_v<int>(to_constant_expr(rounding_mode))));
777 a.from_base10(significand, exponent);
778 return a.to_expr();
779 }
780 else
781 throw error()
782 << "to_fp for non-constant real expressions is not implemented";
783 }
784 else if(source_op.type().id() == ID_unsignedbv)
785 {
786 // The operand is hard-wired to be interpreted as a signed number.
789 source_op,
791 to_unsignedbv_type(source_op.type()).get_width())),
792 rounding_mode,
793 spec.to_type());
794 }
795 else if(source_op.type().id() == ID_floatbv)
796 {
798 source_op, rounding_mode, spec.to_type());
799 }
800 else
801 throw error() << "unexpected sort given as operand to to_fp";
802 }
803 else if(id == "to_fp_unsigned")
804 {
805 if(next_token() != smt2_tokenizert::NUMERAL)
806 throw error("expected number after to_fp_unsigned");
807
808 auto width_e = std::stoll(smt2_tokenizer.get_buffer());
809
810 if(next_token() != smt2_tokenizert::NUMERAL)
811 throw error("expected second number after to_fp_unsigned");
812
813 auto width_f = std::stoll(smt2_tokenizer.get_buffer());
814
815 if(next_token() != smt2_tokenizert::CLOSE)
816 throw error("expected ')' after to_fp_unsigned");
817
818 // width_f *includes* the hidden bit
819 const ieee_float_spect spec(width_f - 1, width_e);
820
821 auto rounding_mode = expression();
822
823 auto source_op = expression();
824
825 if(next_token() != smt2_tokenizert::CLOSE)
826 throw error("expected ')' at the end of to_fp_unsigned");
827
828 if(source_op.type().id() == ID_unsignedbv)
829 {
830 // The operand is hard-wired to be interpreted
831 // as an unsigned number.
833 source_op, rounding_mode, spec.to_type());
834 }
835 else
836 throw error()
837 << "unexpected sort given as operand to to_fp_unsigned";
838 }
839 else if(id == "fp.to_sbv" || id == "fp.to_ubv")
840 {
841 // These are indexed by the number of bits of the result.
842 if(next_token() != smt2_tokenizert::NUMERAL)
843 throw error() << "expected number after " << id;
844
845 auto width = std::stoll(smt2_tokenizer.get_buffer());
846
847 if(next_token() != smt2_tokenizert::CLOSE)
848 throw error() << "expected ')' after " << id;
849
850 auto op = operands();
851
852 if(op.size() != 2)
853 throw error() << id << " takes two operands";
854
855 if(op[1].type().id() != ID_floatbv)
856 throw error() << id << " takes a FloatingPoint operand";
857
858 if(id == "fp.to_sbv")
859 return typecast_exprt(
860 floatbv_typecast_exprt(op[1], op[0], signedbv_typet(width)),
861 unsignedbv_typet(width));
862 else
864 op[1], op[0], unsignedbv_typet(width));
865 }
866 else
867 {
868 throw error() << "unknown indexed identifier '"
869 << smt2_tokenizer.get_buffer() << '\'';
870 }
871 }
872 else if(smt2_tokenizer.get_buffer() == "as")
873 {
874 // This is an extension understood by Z3 and CVC4.
875 if(
876 smt2_tokenizer.peek() == smt2_tokenizert::SYMBOL &&
877 smt2_tokenizer.get_buffer() == "const")
878 {
879 next_token(); // eat the "const"
880 auto sort = this->sort();
881
882 if(sort.id() != ID_array)
883 {
884 throw error()
885 << "unexpected 'as const' expression expects array type";
886 }
887
888 const auto &array_sort = to_array_type(sort);
889
890 if(smt2_tokenizer.next_token() != smt2_tokenizert::CLOSE)
891 throw error() << "expecting ')' after sort in 'as const'";
892
893 auto value = expression();
894
895 if(value.type() != array_sort.element_type())
896 throw error() << "unexpected 'as const' with wrong element type";
897
898 if(smt2_tokenizer.next_token() != smt2_tokenizert::CLOSE)
899 throw error() << "expecting ')' at the end of 'as const'";
900
901 return array_of_exprt(value, array_sort);
902 }
903 else
904 throw error() << "unexpected 'as' expression";
905 }
906 else
907 {
908 // just double parentheses
910
911 if(
912 next_token() != smt2_tokenizert::CLOSE &&
913 next_token() != smt2_tokenizert::CLOSE)
914 {
915 throw error("mismatched parentheses in an expression");
916 }
917
918 return tmp;
919 }
920 }
921 else
922 {
923 // just double parentheses
925
926 if(
927 next_token() != smt2_tokenizert::CLOSE &&
928 next_token() != smt2_tokenizert::CLOSE)
929 {
930 throw error("mismatched parentheses in an expression");
931 }
932
933 return tmp;
934 }
935 break;
936
937 case smt2_tokenizert::CLOSE:
938 case smt2_tokenizert::NUMERAL:
939 case smt2_tokenizert::STRING_LITERAL:
940 case smt2_tokenizert::END_OF_FILE:
941 case smt2_tokenizert::NONE:
942 case smt2_tokenizert::KEYWORD:
943 // just parentheses
945 if(next_token() != smt2_tokenizert::CLOSE)
946 throw error("mismatched parentheses in an expression");
947
948 return tmp;
949 }
950
952}
953
955 const exprt::operandst &operands,
956 bool is_signed)
957{
958 if(operands.size() != 2)
959 throw error() << "bitvector division expects two operands";
960
961 // SMT-LIB2 defines the result of division by 0 to be 1....1
962 auto divisor = symbol_exprt("divisor", operands[1].type());
963 auto divisor_is_zero = equal_exprt(divisor, from_integer(0, divisor.type()));
964 auto all_ones = to_unsignedbv_type(operands[0].type()).largest_expr();
965
967
968 if(is_signed)
969 {
970 auto signed_operands = cast_bv_to_signed({operands[0], divisor});
973 }
974 else
975 division_result = div_exprt(operands[0], divisor);
976
977 return let_exprt(
978 {divisor},
979 operands[1],
981}
982
984{
985 if(operands.size() != 2)
986 throw error() << "bitvector modulo expects two operands";
987
988 // SMT-LIB2 defines the result of "lhs modulo 0" to be "lhs"
989 auto dividend = symbol_exprt("dividend", operands[0].type());
990 auto divisor = symbol_exprt("divisor", operands[1].type());
991 auto divisor_is_zero = equal_exprt(divisor, from_integer(0, divisor.type()));
992
994
995 // bvurem and bvsrem match our mod_exprt.
996 // bvsmod doesn't.
997 if(is_signed)
998 {
999 auto signed_operands = cast_bv_to_signed({dividend, divisor});
1000 mod_result =
1002 }
1003 else
1004 mod_result = mod_exprt(dividend, divisor);
1005
1006 return let_exprt(
1007 {dividend, divisor},
1008 {operands[0], operands[1]},
1009 if_exprt(divisor_is_zero, dividend, mod_result));
1010}
1011
1013{
1014 switch(next_token())
1015 {
1016 case smt2_tokenizert::SYMBOL:
1017 {
1018 const auto &identifier = smt2_tokenizer.get_buffer();
1019
1020 // in the expression table?
1021 const auto e_it = expressions.find(identifier);
1022 if(e_it != expressions.end())
1023 return e_it->second();
1024
1025 // rummage through id_map
1026 auto id_it = id_map.find(identifier);
1027 if(id_it != id_map.end())
1028 {
1029 symbol_exprt symbol_expr(identifier, id_it->second.type);
1031 symbol_expr.set(ID_C_quoted, true);
1032 return std::move(symbol_expr);
1033 }
1034
1035 // don't know, give up
1036 throw error() << "unknown expression '" << identifier << '\'';
1037 }
1038
1039 case smt2_tokenizert::NUMERAL:
1040 {
1041 const std::string &buffer = smt2_tokenizer.get_buffer();
1042 if(buffer.size() >= 2 && buffer[0] == '#' && buffer[1] == 'x')
1043 {
1044 mp_integer value =
1045 string2integer(std::string(buffer, 2, std::string::npos), 16);
1046 const std::size_t width = 4 * (buffer.size() - 2);
1047 CHECK_RETURN(width != 0 && width % 4 == 0);
1048 unsignedbv_typet type(width);
1049 return from_integer(value, type);
1050 }
1051 else if(buffer.size() >= 2 && buffer[0] == '#' && buffer[1] == 'b')
1052 {
1053 mp_integer value =
1054 string2integer(std::string(buffer, 2, std::string::npos), 2);
1055 const std::size_t width = buffer.size() - 2;
1056 CHECK_RETURN(width != 0);
1057 unsignedbv_typet type(width);
1058 return from_integer(value, type);
1059 }
1060 else
1061 {
1062 return constant_exprt(buffer, integer_typet());
1063 }
1064 }
1065
1066 case smt2_tokenizert::OPEN: // function application
1067 return function_application();
1068
1069 case smt2_tokenizert::END_OF_FILE:
1070 throw error("EOF in an expression");
1071
1072 case smt2_tokenizert::CLOSE:
1073 case smt2_tokenizert::STRING_LITERAL:
1074 case smt2_tokenizert::NONE:
1075 case smt2_tokenizert::KEYWORD:
1076 throw error("unexpected token in an expression");
1077 }
1078
1080}
1081
1083{
1084 expressions["true"] = [] { return true_exprt(); };
1085 expressions["false"] = [] { return false_exprt(); };
1086
1087 expressions["roundNearestTiesToEven"] = [] {
1088 // we encode as 32-bit unsignedbv
1090 };
1091
1092 expressions["roundNearestTiesToAway"] = [this]() -> exprt {
1093 throw error("unsupported rounding mode");
1094 };
1095
1096 expressions["roundTowardPositive"] = [] {
1097 // we encode as 32-bit unsignedbv
1099 };
1100
1101 expressions["roundTowardNegative"] = [] {
1102 // we encode as 32-bit unsignedbv
1104 };
1105
1106 expressions["roundTowardZero"] = [] {
1107 // we encode as 32-bit unsignedbv
1109 };
1110
1111 expressions["lambda"] = [this] { return lambda_expression(); };
1112 expressions["let"] = [this] { return let_expression(); };
1113 expressions["exists"] = [this] { return quantifier_expression(ID_exists); };
1114 expressions["forall"] = [this] { return quantifier_expression(ID_forall); };
1115 expressions["and"] = [this] { return multi_ary(ID_and, operands()); };
1116 expressions["or"] = [this] { return multi_ary(ID_or, operands()); };
1117 expressions["xor"] = [this] { return multi_ary(ID_xor, operands()); };
1118 expressions["not"] = [this] { return unary(ID_not, operands()); };
1119 expressions["="] = [this] { return binary_predicate(ID_equal, operands()); };
1120 expressions["<="] = [this] { return binary_predicate(ID_le, operands()); };
1121 expressions[">="] = [this] { return binary_predicate(ID_ge, operands()); };
1122 expressions["<"] = [this] { return binary_predicate(ID_lt, operands()); };
1123 expressions[">"] = [this] { return binary_predicate(ID_gt, operands()); };
1124
1125 expressions["bvule"] = [this] { return binary_predicate(ID_le, operands()); };
1126
1127 expressions["bvsle"] = [this] {
1129 };
1130
1131 expressions["bvuge"] = [this] { return binary_predicate(ID_ge, operands()); };
1132
1133 expressions["bvsge"] = [this] {
1135 };
1136
1137 expressions["bvult"] = [this] { return binary_predicate(ID_lt, operands()); };
1138
1139 expressions["bvslt"] = [this] {
1141 };
1142
1143 expressions["bvugt"] = [this] { return binary_predicate(ID_gt, operands()); };
1144
1145 expressions["bvsgt"] = [this] {
1147 };
1148
1149 expressions["bvcomp"] = [this] {
1150 auto b0 = from_integer(0, unsignedbv_typet(1));
1151 auto b1 = from_integer(1, unsignedbv_typet(1));
1153 };
1154
1155 expressions["bvashr"] = [this] {
1157 };
1158
1159 expressions["bvlshr"] = [this] { return binary(ID_lshr, operands()); };
1160 expressions["bvshr"] = [this] { return binary(ID_lshr, operands()); };
1161 expressions["bvlshl"] = [this] { return binary(ID_shl, operands()); };
1162 expressions["bvashl"] = [this] { return binary(ID_shl, operands()); };
1163 expressions["bvshl"] = [this] { return binary(ID_shl, operands()); };
1164 expressions["bvand"] = [this] { return multi_ary(ID_bitand, operands()); };
1165 expressions["bvnand"] = [this] { return multi_ary(ID_bitnand, operands()); };
1166 expressions["bvor"] = [this] { return multi_ary(ID_bitor, operands()); };
1167 expressions["bvnor"] = [this] { return multi_ary(ID_bitnor, operands()); };
1168 expressions["bvxor"] = [this] { return multi_ary(ID_bitxor, operands()); };
1169 expressions["bvxnor"] = [this] { return multi_ary(ID_bitxnor, operands()); };
1170 expressions["bvnot"] = [this] { return unary(ID_bitnot, operands()); };
1171 expressions["bvneg"] = [this] { return unary(ID_unary_minus, operands()); };
1172 expressions["bvadd"] = [this] { return multi_ary(ID_plus, operands()); };
1173 expressions["+"] = [this] { return multi_ary(ID_plus, operands()); };
1174 expressions["bvsub"] = [this] { return binary(ID_minus, operands()); };
1175 expressions["bvmul"] = [this] { return multi_ary(ID_mult, operands()); };
1176 expressions["*"] = [this] { return multi_ary(ID_mult, operands()); };
1177
1178 expressions["-"] = [this] {
1179 auto op = operands();
1180 if(op.size() == 1)
1181 return unary(ID_unary_minus, op);
1182 else
1183 return binary(ID_minus, op);
1184 };
1185
1186 expressions["bvsdiv"] = [this] { return bv_division(operands(), true); };
1187 expressions["bvudiv"] = [this] { return bv_division(operands(), false); };
1188 expressions["/"] = [this] { return binary(ID_div, operands()); };
1189 expressions["div"] = [this] { return binary(ID_div, operands()); };
1190
1191 expressions["bvsrem"] = [this] { return bv_mod(operands(), true); };
1192 expressions["bvurem"] = [this] { return bv_mod(operands(), false); };
1193
1194 // 2's complement signed remainder (sign follows divisor)
1195 // We don't have that.
1196 expressions["bvsmod"] = [this] { return bv_mod(operands(), true); };
1197
1198 expressions["mod"] = [this] {
1199 // SMT-LIB2 uses Boute's Euclidean definition for mod,
1200 // which is never negative and undefined when the second
1201 // argument is zero.
1202 return binary(ID_euclidean_mod, operands());
1203 };
1204
1205 expressions["concat"] = [this] {
1206 auto op = operands();
1207
1208 // add the widths
1209 auto op_width = make_range(op).map(
1210 [](const exprt &o) { return to_bitvector_type(o.type()).get_width(); });
1211
1212 const std::size_t total_width =
1213 std::accumulate(op_width.begin(), op_width.end(), 0);
1214
1215 return concatenation_exprt(std::move(op), unsignedbv_typet(total_width));
1216 };
1217
1218 expressions["distinct"] = [this] {
1219 // pair-wise different constraint, multi-ary
1220 auto op = operands();
1221 if(op.size() == 2)
1222 return binary_predicate(ID_notequal, op);
1223 else
1224 {
1225 std::vector<exprt> pairwise_constraints;
1226 for(std::size_t i = 0; i < op.size(); i++)
1227 {
1228 for(std::size_t j = i; j < op.size(); j++)
1229 {
1230 if(i != j)
1231 pairwise_constraints.push_back(
1232 binary_exprt(op[i], ID_notequal, op[j], bool_typet()));
1233 }
1234 }
1236 }
1237 };
1238
1239 expressions["ite"] = [this] {
1240 auto op = operands();
1241
1242 if(op.size() != 3)
1243 throw error("ite takes three operands");
1244
1245 if(!op[0].is_boolean())
1246 throw error("ite takes a boolean as first operand");
1247
1248 if(op[1].type() != op[2].type())
1249 throw error("ite needs matching types");
1250
1251 return if_exprt(op[0], op[1], op[2]);
1252 };
1253
1254 expressions["implies"] = [this] { return binary(ID_implies, operands()); };
1255
1256 expressions["=>"] = [this] { return binary(ID_implies, operands()); };
1257
1258 expressions["select"] = [this] {
1259 auto op = operands();
1260
1261 // array index
1262 if(op.size() != 2)
1263 throw error("select takes two operands");
1264
1265 if(op[0].type().id() != ID_array)
1266 throw error("select expects array operand");
1267
1268 return index_exprt(op[0], op[1]);
1269 };
1270
1271 expressions["store"] = [this] {
1272 auto op = operands();
1273
1274 // array update
1275 if(op.size() != 3)
1276 throw error("store takes three operands");
1277
1278 if(op[0].type().id() != ID_array)
1279 throw error("store expects array operand");
1280
1281 if(to_array_type(op[0].type()).element_type() != op[2].type())
1282 throw error("store expects value that matches array element type");
1283
1284 return with_exprt(op[0], op[1], op[2]);
1285 };
1286
1287 expressions["fp.abs"] = [this] {
1288 auto op = operands();
1289
1290 if(op.size() != 1)
1291 throw error("fp.abs takes one operand");
1292
1293 if(op[0].type().id() != ID_floatbv)
1294 throw error("fp.abs takes FloatingPoint operand");
1295
1296 return abs_exprt(op[0]);
1297 };
1298
1299 expressions["fp.isNaN"] = [this] {
1300 auto op = operands();
1301
1302 if(op.size() != 1)
1303 throw error("fp.isNaN takes one operand");
1304
1305 if(op[0].type().id() != ID_floatbv)
1306 throw error("fp.isNaN takes FloatingPoint operand");
1307
1308 return unary_predicate_exprt(ID_isnan, op[0]);
1309 };
1310
1311 expressions["fp.isInfinite"] = [this] {
1312 auto op = operands();
1313
1314 if(op.size() != 1)
1315 throw error("fp.isInfinite takes one operand");
1316
1317 if(op[0].type().id() != ID_floatbv)
1318 throw error("fp.isInfinite takes FloatingPoint operand");
1319
1320 return unary_predicate_exprt(ID_isinf, op[0]);
1321 };
1322
1323 expressions["fp.isNormal"] = [this] {
1324 auto op = operands();
1325
1326 if(op.size() != 1)
1327 throw error("fp.isNormal takes one operand");
1328
1329 if(op[0].type().id() != ID_floatbv)
1330 throw error("fp.isNormal takes FloatingPoint operand");
1331
1332 return isnormal_exprt(op[0]);
1333 };
1334
1335 expressions["fp.isZero"] = [this] {
1336 auto op = operands();
1337
1338 if(op.size() != 1)
1339 throw error("fp.isZero takes one operand");
1340
1341 if(op[0].type().id() != ID_floatbv)
1342 throw error("fp.isZero takes FloatingPoint operand");
1343
1344 return not_exprt(typecast_exprt(op[0], bool_typet()));
1345 };
1346
1347 expressions["fp"] = [this] { return function_application_fp(operands()); };
1348
1349 expressions["fp.add"] = [this] {
1350 return function_application_ieee_float_op("fp.add", operands());
1351 };
1352
1353 expressions["fp.mul"] = [this] {
1354 return function_application_ieee_float_op("fp.mul", operands());
1355 };
1356
1357 expressions["fp.sub"] = [this] {
1358 return function_application_ieee_float_op("fp.sub", operands());
1359 };
1360
1361 expressions["fp.div"] = [this] {
1362 return function_application_ieee_float_op("fp.div", operands());
1363 };
1364
1365 expressions["fp.rem"] = [this] {
1366 auto op = operands();
1367
1368 // Note that these do not have a rounding mode.
1369 if(op.size() != 2)
1370 throw error() << "fp.rem takes three operands";
1371
1372 if(op[0].type().id() != ID_floatbv || op[1].type().id() != ID_floatbv)
1373 throw error() << "fp.rem takes FloatingPoint operands";
1374
1375 if(op[0].type() != op[1].type())
1376 {
1377 throw error()
1378 << "fp.rem takes FloatingPoint operands with matching sort, "
1379 << "but got " << smt2_format(op[0].type()) << " vs "
1380 << smt2_format(op[1].type());
1381 }
1382
1383 return binary_exprt(op[0], ID_floatbv_rem, op[1]);
1384 };
1385
1386 expressions["fp.eq"] = [this] {
1388 };
1389
1390 expressions["fp.leq"] = [this] {
1391 return binary_predicate(ID_le, operands());
1392 };
1393
1394 expressions["fp.lt"] = [this] { return binary_predicate(ID_lt, operands()); };
1395
1396 expressions["fp.geq"] = [this] {
1397 return binary_predicate(ID_ge, operands());
1398 };
1399
1400 expressions["fp.gt"] = [this] { return binary_predicate(ID_gt, operands()); };
1401
1402 expressions["fp.neg"] = [this] { return unary(ID_unary_minus, operands()); };
1403}
1404
1406{
1407 std::vector<typet> sorts;
1408
1409 // (-> sort+ sort)
1410 // The last sort is the co-domain.
1411
1412 while(smt2_tokenizer.peek() != smt2_tokenizert::CLOSE)
1413 {
1414 if(smt2_tokenizer.peek() == smt2_tokenizert::END_OF_FILE)
1415 throw error() << "unexpected end-of-file in a function sort";
1416
1417 sorts.push_back(sort()); // recursive call
1418 }
1419
1420 next_token(); // eat the ')'
1421
1422 if(sorts.size() < 2)
1423 throw error() << "expected function sort to have at least 2 type arguments";
1424
1425 auto codomain = std::move(sorts.back());
1426 sorts.pop_back();
1427
1428 return mathematical_function_typet(std::move(sorts), std::move(codomain));
1429}
1430
1432{
1433 // a sort is one of the following three cases:
1434 // SYMBOL
1435 // ( _ SYMBOL ...
1436 // ( SYMBOL ...
1437 switch(next_token())
1438 {
1439 case smt2_tokenizert::SYMBOL:
1440 break;
1441
1442 case smt2_tokenizert::OPEN:
1443 if(smt2_tokenizer.next_token() != smt2_tokenizert::SYMBOL)
1444 throw error("expected symbol after '(' in a sort ");
1445
1446 if(smt2_tokenizer.get_buffer() == "_")
1447 {
1448 if(next_token() != smt2_tokenizert::SYMBOL)
1449 throw error("expected symbol after '_' in a sort");
1450 }
1451 break;
1452
1453 case smt2_tokenizert::CLOSE:
1454 case smt2_tokenizert::NUMERAL:
1455 case smt2_tokenizert::STRING_LITERAL:
1456 case smt2_tokenizert::NONE:
1457 case smt2_tokenizert::KEYWORD:
1458 throw error() << "unexpected token in a sort: '"
1459 << smt2_tokenizer.get_buffer() << '\'';
1460
1461 case smt2_tokenizert::END_OF_FILE:
1462 throw error() << "unexpected end-of-file in a sort";
1463 }
1464
1465 // now we have a SYMBOL
1466 const auto &token = smt2_tokenizer.get_buffer();
1467
1468 const auto s_it = sorts.find(token);
1469
1470 if(s_it == sorts.end())
1471 throw error() << "unexpected sort: '" << token << '\'';
1472
1473 return s_it->second();
1474}
1475
1477{
1478 sorts["Bool"] = [] { return bool_typet(); };
1479 sorts["Int"] = [] { return integer_typet(); };
1480 sorts["Real"] = [] { return real_typet(); };
1481
1482 sorts["Float16"] = [] {
1483 return ieee_float_spect::half_precision().to_type();
1484 };
1485 sorts["Float32"] = [] {
1486 return ieee_float_spect::single_precision().to_type();
1487 };
1488 sorts["Float64"] = [] {
1489 return ieee_float_spect::double_precision().to_type();
1490 };
1491 sorts["Float128"] = [] {
1492 return ieee_float_spect::quadruple_precision().to_type();
1493 };
1494
1495 sorts["BitVec"] = [this] {
1496 if(next_token() != smt2_tokenizert::NUMERAL)
1497 throw error("expected numeral as bit-width");
1498
1499 auto width = std::stoll(smt2_tokenizer.get_buffer());
1500
1501 // eat the ')'
1502 if(next_token() != smt2_tokenizert::CLOSE)
1503 throw error("expected ')' at end of sort");
1504
1505 return unsignedbv_typet(width);
1506 };
1507
1508 sorts["FloatingPoint"] = [this] {
1509 if(next_token() != smt2_tokenizert::NUMERAL)
1510 throw error("expected numeral as bit-width");
1511
1512 const auto width_e = std::stoll(smt2_tokenizer.get_buffer());
1513
1514 if(next_token() != smt2_tokenizert::NUMERAL)
1515 throw error("expected numeral as bit-width");
1516
1517 const auto width_f = std::stoll(smt2_tokenizer.get_buffer());
1518
1519 // consume the ')'
1520 if(next_token() != smt2_tokenizert::CLOSE)
1521 throw error("expected ')' at end of sort");
1522
1523 return ieee_float_spect(width_f - 1, width_e).to_type();
1524 };
1525
1526 sorts["Array"] = [this] {
1527 // this gets two sorts as arguments, domain and range
1528 auto domain = sort();
1529 auto range = sort();
1530
1531 // eat the ')'
1532 if(next_token() != smt2_tokenizert::CLOSE)
1533 throw error("expected ')' at end of Array sort");
1534
1535 // we can turn arrays that map an unsigned bitvector type
1536 // to something else into our 'array_typet'
1537 if(domain.id() == ID_unsignedbv)
1538 return array_typet(range, infinity_exprt(domain));
1539 else
1540 throw error("unsupported array sort");
1541 };
1542
1543 sorts["->"] = [this] { return function_sort(); };
1544}
1545
1548{
1549 if(next_token() != smt2_tokenizert::OPEN)
1550 throw error("expected '(' at beginning of signature");
1551
1552 if(smt2_tokenizer.peek() == smt2_tokenizert::CLOSE)
1553 {
1554 // no parameters
1555 next_token(); // eat the ')'
1557 }
1558
1560 std::vector<irep_idt> parameters;
1561
1562 while(smt2_tokenizer.peek() != smt2_tokenizert::CLOSE)
1563 {
1564 if(next_token() != smt2_tokenizert::OPEN)
1565 throw error("expected '(' at beginning of parameter");
1566
1567 if(next_token() != smt2_tokenizert::SYMBOL)
1568 throw error("expected symbol in parameter");
1569
1571 domain.push_back(sort());
1572 parameters.push_back(id);
1573
1574 if(next_token() != smt2_tokenizert::CLOSE)
1575 throw error("expected ')' at end of parameter");
1576 }
1577
1578 next_token(); // eat the ')'
1579
1580 typet codomain = sort();
1581
1583 mathematical_function_typet(domain, codomain), parameters);
1584}
1585
1587{
1588 if(next_token() != smt2_tokenizert::OPEN)
1589 throw error("expected '(' at beginning of signature");
1590
1591 if(smt2_tokenizer.peek() == smt2_tokenizert::CLOSE)
1592 {
1593 next_token(); // eat the ')'
1594 return sort();
1595 }
1596
1598
1599 while(smt2_tokenizer.peek() != smt2_tokenizert::CLOSE)
1600 domain.push_back(sort());
1601
1602 next_token(); // eat the ')'
1603
1604 typet codomain = sort();
1605
1606 return mathematical_function_typet(domain, codomain);
1607}
1608
1609void smt2_parsert::command(const std::string &c)
1610{
1611 auto c_it = commands.find(c);
1612 if(c_it == commands.end())
1613 {
1614 // silently ignore
1616 }
1617 else
1618 c_it->second();
1619}
1620
1622{
1623 commands["declare-const"] = [this]() {
1624 const auto s = smt2_tokenizer.get_buffer();
1625
1626 if(next_token() != smt2_tokenizert::SYMBOL)
1627 throw error() << "expected a symbol after " << s;
1628
1630 auto type = sort();
1631
1632 add_unique_id(id, exprt(ID_nil, type));
1633 };
1634
1635 // declare-var appears to be a synonym for declare-const that is
1636 // accepted by Z3 and CVC4
1637 commands["declare-var"] = commands["declare-const"];
1638
1639 commands["declare-fun"] = [this]() {
1640 if(next_token() != smt2_tokenizert::SYMBOL)
1641 throw error("expected a symbol after declare-fun");
1642
1644 auto type = function_signature_declaration();
1645
1646 add_unique_id(id, exprt(ID_nil, type));
1647 };
1648
1649 commands["define-const"] = [this]() {
1650 if(next_token() != smt2_tokenizert::SYMBOL)
1651 throw error("expected a symbol after define-const");
1652
1653 const irep_idt id = smt2_tokenizer.get_buffer();
1654
1655 const auto type = sort();
1656 const auto value = expression();
1657
1658 // check type of value
1659 if(value.type() != type)
1660 {
1661 throw error() << "type mismatch in constant definition: expected '"
1662 << smt2_format(type) << "' but got '"
1663 << smt2_format(value.type()) << '\'';
1664 }
1665
1666 // create the entry
1667 add_unique_id(id, value);
1668 };
1669
1670 commands["define-fun"] = [this]() {
1671 if(next_token() != smt2_tokenizert::SYMBOL)
1672 throw error("expected a symbol after define-fun");
1673
1674 const irep_idt id = smt2_tokenizer.get_buffer();
1675
1676 const auto signature = function_signature_definition();
1677
1678 // put the parameters into the scope and take care of hiding
1679 std::vector<std::pair<irep_idt, idt>> hidden_ids;
1680
1681 for(const auto &pair : signature.ids_and_types())
1682 {
1683 auto insert_result =
1684 id_map.insert({pair.first, idt{idt::PARAMETER, pair.second}});
1685 if(!insert_result.second) // already there
1686 {
1687 auto &id_entry = *insert_result.first;
1688 hidden_ids.emplace_back(id_entry.first, std::move(id_entry.second));
1689 id_entry.second = idt{idt::PARAMETER, pair.second};
1690 }
1691 }
1692
1693 // now parse body with parameter ids in place
1694 auto body = expression();
1695
1696 // remove the parameter ids
1697 for(auto &id : signature.parameters)
1698 id_map.erase(id);
1699
1700 // restore the hidden ids, if any
1701 for(auto &hidden_id : hidden_ids)
1702 id_map.insert(std::move(hidden_id));
1703
1704 // check type of body
1705 if(signature.type.id() == ID_mathematical_function)
1706 {
1707 const auto &f_signature = to_mathematical_function_type(signature.type);
1708 if(body.type() != f_signature.codomain())
1709 {
1710 throw error() << "type mismatch in function definition: expected '"
1711 << smt2_format(f_signature.codomain()) << "' but got '"
1712 << smt2_format(body.type()) << '\'';
1713 }
1714 }
1715 else if(body.type() != signature.type)
1716 {
1717 throw error() << "type mismatch in function definition: expected '"
1718 << smt2_format(signature.type) << "' but got '"
1719 << smt2_format(body.type()) << '\'';
1720 }
1721
1722 // if there are parameters, this is a lambda
1723 if(!signature.parameters.empty())
1724 body = lambda_exprt(signature.binding_variables(), body);
1725
1726 // create the entry
1727 add_unique_id(id, std::move(body));
1728 };
1729
1730 commands["exit"] = [this]() { exit = true; };
1731}
constant_exprt from_integer(const mp_integer &int_value, const typet &type)
API to expression classes for bitvectors.
Pre-defined bitvector types.
const bitvector_typet & to_bitvector_type(const typet &type)
Cast a typet to a bitvector_typet.
const unsignedbv_typet & to_unsignedbv_type(const typet &type)
Cast a typet to an unsignedbv_typet.
const signedbv_typet & to_signedbv_type(const typet &type)
Cast a typet to a signedbv_typet.
Absolute value.
Definition std_expr.h:379
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
Definition ai.h:563
Array constructor from single element.
Definition std_expr.h:1498
Arrays with given size.
Definition std_types.h:763
A base class for binary expressions.
Definition std_expr.h:583
A base class for expressions that are predicates, i.e., Boolean-typed, and that take exactly two argu...
Definition std_expr.h:676
std::vector< symbol_exprt > variablest
Definition std_expr.h:3054
The Boolean type.
Definition std_types.h:36
Fixed-width bit-vector without numerical interpretation.
Concatenation of bit-vector operands.
A constant literal expression.
Definition std_expr.h:2942
Division.
Definition std_expr.h:1097
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition dstring.h:39
Equality.
Definition std_expr.h:1306
Base class for all expressions.
Definition expr.h:56
std::vector< exprt > operandst
Definition expr.h:58
typet & type()
Return the type of the expression.
Definition expr.h:84
operandst & operands()
Definition expr.h:94
Extracts a sub-range of a bit-vector operand.
The Boolean constant false.
Definition std_expr.h:3017
Semantic type conversion from/to floating-point formats.
Application of (mathematical) function.
IEEE-floating-point equality.
IEEE floating-point operations These have two data operands (op0 and op1) and one rounding mode (op2)...
static ieee_float_spect half_precision()
Definition ieee_float.h:63
static ieee_float_spect single_precision()
Definition ieee_float.h:70
static ieee_float_spect quadruple_precision()
Definition ieee_float.h:82
class floatbv_typet to_type() const
static ieee_float_spect double_precision()
Definition ieee_float.h:76
static ieee_floatt plus_infinity(const ieee_float_spect &_spec)
Definition ieee_float.h:211
static ieee_floatt NaN(const ieee_float_spect &_spec)
Definition ieee_float.h:208
static ieee_floatt minus_infinity(const ieee_float_spect &_spec)
Definition ieee_float.h:214
The trinary if-then-else operator.
Definition std_expr.h:2323
Array index operator.
Definition std_expr.h:1410
An expression denoting infinity.
Definition std_expr.h:3042
Unbounded, signed integers (mathematical integers, not bitvectors)
void set(const irep_idt &name, const irep_idt &value)
Definition irep.h:420
const irep_idt & id() const
Definition irep.h:396
Evaluates to true if the operand is a normal number.
A (mathematical) lambda expression.
A let expression.
Definition std_expr.h:3149
A type for mathematical functions (do not confuse with functions/methods in code)
Modulo defined as lhs-(rhs * truncate(lhs/rhs)).
Definition std_expr.h:1168
The NIL expression.
Definition std_expr.h:3026
Boolean negation.
Definition std_expr.h:2278
A base class for quantifier expressions.
Unbounded, signed real numbers.
Bit-vector replication.
Fixed-width bit-vector with two's complement interpretation.
exprt function_application_ieee_float_op(const irep_idt &, const exprt::operandst &)
std::size_t parenthesis_level
Definition smt2_parser.h:94
void command(const std::string &)
exprt::operandst operands()
void command_sequence()
exprt bv_mod(const exprt::operandst &, bool is_signed)
exprt binary(irep_idt, const exprt::operandst &)
exprt bv_division(const exprt::operandst &, bool is_signed)
void skip_to_end_of_list()
This skips tokens until all bracketed expressions are closed.
std::unordered_map< std::string, std::function< exprt()> > expressions
exprt lambda_expression()
typet function_signature_declaration()
named_termst named_terms
Definition smt2_parser.h:74
id_mapt id_map
Definition smt2_parser.h:58
std::unordered_map< std::string, std::function< void()> > commands
exprt function_application()
void add_unique_id(irep_idt, exprt)
exprt cast_bv_to_unsigned(const exprt &)
Apply typecast to unsignedbv to given expression.
exprt::operandst cast_bv_to_signed(const exprt::operandst &)
Apply typecast to signedbv to expressions in vector.
exprt multi_ary(irep_idt, const exprt::operandst &)
void ignore_command()
exprt quantifier_expression(irep_idt)
std::pair< binding_exprt::variablest, exprt > binding(irep_idt)
exprt function_application_ieee_float_eq(const exprt::operandst &)
exprt let_expression()
void check_matching_operand_types(const exprt::operandst &) const
signature_with_parameter_idst function_signature_definition()
exprt function_application_fp(const exprt::operandst &)
typet function_sort()
smt2_tokenizert::smt2_errort error() const
Definition smt2_parser.h:83
void setup_expressions()
exprt binary_predicate(irep_idt, const exprt::operandst &)
smt2_tokenizert::tokent next_token()
std::unordered_map< std::string, std::function< typet()> > sorts
smt2_tokenizert smt2_tokenizer
Definition smt2_parser.h:92
exprt unary(irep_idt, const exprt::operandst &)
void setup_commands()
const std::string & get_buffer() const
bool token_is_quoted_symbol() const
Expression to hold a symbol (variable)
Definition std_expr.h:113
const irep_idt & get_identifier() const
Definition std_expr.h:142
The Boolean constant true.
Definition std_expr.h:3008
Semantic type conversion.
Definition std_expr.h:2017
The type of an expression, extends irept.
Definition type.h:29
Generic base class for unary expressions.
Definition std_expr.h:314
A base class for expressions that are predicates, i.e., Boolean-typed, and that take exactly one argu...
Definition std_expr.h:528
Fixed-width bit-vector with unsigned binary interpretation.
Operator to update elements in structs and arrays.
Definition std_expr.h:2424
bool has_prefix(const std::string &s, const std::string &prefix)
Definition converter.cpp:13
API to expression classes for floating-point arithmetic.
const std::string & id2string(const irep_idt &d)
Definition irep.h:47
API to expression classes for 'mathematical' expressions.
const mathematical_function_typet & to_mathematical_function_type(const typet &type)
Cast a typet to a mathematical_function_typet.
const mp_integer string2integer(const std::string &n, unsigned base)
Definition mp_arith.cpp:54
Ranges: pair of begin and end iterators, which can be initialized from containers,...
ranget< iteratort > make_range(iteratort begin, iteratort end)
Definition range.h:524
static smt2_format_containert< T > smt2_format(const T &_o)
Definition smt2_format.h:28
BigInt mp_integer
Definition smt_terms.h:18
#define CHECK_RETURN(CONDITION)
Definition invariant.h:495
#define UNREACHABLE
This should be used to mark dead code.
Definition invariant.h:525
const constant_exprt & to_constant_expr(const exprt &expr)
Cast an exprt to a constant_exprt.
Definition std_expr.h:2992
const array_typet & to_array_type(const typet &type)
Cast a typet to an array_typet.
Definition std_types.h:844
bool is_signed(const typet &t)
Convenience function – is the type signed?
Definition util.cpp:45