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();
98 parentheses++;
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.type().id() != ID_bool)
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
480 const auto fp_type = ieee_float_spect(width_f, width_e).to_type();
481
482 return typecast_exprt(
484 concatenation_exprt(exprt::operandst(op), concat_type), bv_type),
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")
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.type().id() != ID_bool)
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();
685 const signedbv_typet small_signed_type(width);
686 const signedbv_typet large_signed_type(width + index);
687 const unsignedbv_typet unsigned_type(width + index);
688
689 return typecast_exprt(
691 typecast_exprt(op[0], small_signed_type), large_signed_type),
692 unsigned_type);
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.id() == ID_constant)
746 {
747 mp_integer significand, exponent;
748
749 const auto &real_number =
750 id2string(to_constant_expr(source_op).get_value());
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 != '.')
765 significand_str += ch;
766 }
767
768 exponent =
769 mp_integer(dot_pos) - mp_integer(real_number.size()) + 1;
770 significand = string2integer(significand_str);
771 }
772
773 ieee_floatt a(
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
804 {
805 throw error() << "unknown indexed identifier '"
806 << smt2_tokenizer.get_buffer() << '\'';
807 }
808 }
809 else if(smt2_tokenizer.get_buffer() == "as")
810 {
811 // This is an extension understood by Z3 and CVC4.
812 if(
813 smt2_tokenizer.peek() == smt2_tokenizert::SYMBOL &&
814 smt2_tokenizer.get_buffer() == "const")
815 {
816 next_token(); // eat the "const"
817 auto sort = this->sort();
818
819 if(sort.id() != ID_array)
820 {
821 throw error()
822 << "unexpected 'as const' expression expects array type";
823 }
824
825 const auto &array_sort = to_array_type(sort);
826
827 if(smt2_tokenizer.next_token() != smt2_tokenizert::CLOSE)
828 throw error() << "expecting ')' after sort in 'as const'";
829
830 auto value = expression();
831
832 if(value.type() != array_sort.element_type())
833 throw error() << "unexpected 'as const' with wrong element type";
834
835 if(smt2_tokenizer.next_token() != smt2_tokenizert::CLOSE)
836 throw error() << "expecting ')' at the end of 'as const'";
837
838 return array_of_exprt(value, array_sort);
839 }
840 else
841 throw error() << "unexpected 'as' expression";
842 }
843 else
844 {
845 // just double parentheses
846 exprt tmp=expression();
847
848 if(
849 next_token() != smt2_tokenizert::CLOSE &&
850 next_token() != smt2_tokenizert::CLOSE)
851 {
852 throw error("mismatched parentheses in an expression");
853 }
854
855 return tmp;
856 }
857 }
858 else
859 {
860 // just double parentheses
861 exprt tmp=expression();
862
863 if(
864 next_token() != smt2_tokenizert::CLOSE &&
865 next_token() != smt2_tokenizert::CLOSE)
866 {
867 throw error("mismatched parentheses in an expression");
868 }
869
870 return tmp;
871 }
872 break;
873
874 case smt2_tokenizert::CLOSE:
875 case smt2_tokenizert::NUMERAL:
876 case smt2_tokenizert::STRING_LITERAL:
877 case smt2_tokenizert::END_OF_FILE:
878 case smt2_tokenizert::NONE:
879 case smt2_tokenizert::KEYWORD:
880 // just parentheses
881 exprt tmp=expression();
882 if(next_token() != smt2_tokenizert::CLOSE)
883 throw error("mismatched parentheses in an expression");
884
885 return tmp;
886 }
887
889}
890
892 const exprt::operandst &operands,
893 bool is_signed)
894{
895 if(operands.size() != 2)
896 throw error() << "bitvector division expects two operands";
897
898 // SMT-LIB2 defines the result of division by 0 to be 1....1
899 auto divisor = symbol_exprt("divisor", operands[1].type());
900 auto divisor_is_zero = equal_exprt(divisor, from_integer(0, divisor.type()));
901 auto all_ones = to_unsignedbv_type(operands[0].type()).largest_expr();
902
903 exprt division_result;
904
905 if(is_signed)
906 {
907 auto signed_operands = cast_bv_to_signed({operands[0], divisor});
908 division_result =
909 cast_bv_to_unsigned(div_exprt(signed_operands[0], signed_operands[1]));
910 }
911 else
912 division_result = div_exprt(operands[0], divisor);
913
914 return let_exprt(
915 {divisor},
916 operands[1],
917 if_exprt(divisor_is_zero, all_ones, division_result));
918}
919
921{
922 if(operands.size() != 2)
923 throw error() << "bitvector modulo expects two operands";
924
925 // SMT-LIB2 defines the result of "lhs modulo 0" to be "lhs"
926 auto dividend = symbol_exprt("dividend", operands[0].type());
927 auto divisor = symbol_exprt("divisor", operands[1].type());
928 auto divisor_is_zero = equal_exprt(divisor, from_integer(0, divisor.type()));
929
930 exprt mod_result;
931
932 // bvurem and bvsrem match our mod_exprt.
933 // bvsmod doesn't.
934 if(is_signed)
935 {
936 auto signed_operands = cast_bv_to_signed({dividend, divisor});
937 mod_result =
938 cast_bv_to_unsigned(mod_exprt(signed_operands[0], signed_operands[1]));
939 }
940 else
941 mod_result = mod_exprt(dividend, divisor);
942
943 return let_exprt(
944 {dividend, divisor},
945 {operands[0], operands[1]},
946 if_exprt(divisor_is_zero, dividend, mod_result));
947}
948
950{
951 switch(next_token())
952 {
953 case smt2_tokenizert::SYMBOL:
954 {
955 const auto &identifier = smt2_tokenizer.get_buffer();
956
957 // in the expression table?
958 const auto e_it = expressions.find(identifier);
959 if(e_it != expressions.end())
960 return e_it->second();
961
962 // rummage through id_map
963 auto id_it = id_map.find(identifier);
964 if(id_it != id_map.end())
965 {
966 symbol_exprt symbol_expr(identifier, id_it->second.type);
968 symbol_expr.set(ID_C_quoted, true);
969 return std::move(symbol_expr);
970 }
971
972 // don't know, give up
973 throw error() << "unknown expression '" << identifier << '\'';
974 }
975
976 case smt2_tokenizert::NUMERAL:
977 {
978 const std::string &buffer = smt2_tokenizer.get_buffer();
979 if(buffer.size() >= 2 && buffer[0] == '#' && buffer[1] == 'x')
980 {
981 mp_integer value =
982 string2integer(std::string(buffer, 2, std::string::npos), 16);
983 const std::size_t width = 4 * (buffer.size() - 2);
984 CHECK_RETURN(width != 0 && width % 4 == 0);
985 unsignedbv_typet type(width);
986 return from_integer(value, type);
987 }
988 else if(buffer.size() >= 2 && buffer[0] == '#' && buffer[1] == 'b')
989 {
990 mp_integer value =
991 string2integer(std::string(buffer, 2, std::string::npos), 2);
992 const std::size_t width = buffer.size() - 2;
993 CHECK_RETURN(width != 0);
994 unsignedbv_typet type(width);
995 return from_integer(value, type);
996 }
997 else
998 {
999 return constant_exprt(buffer, integer_typet());
1000 }
1001 }
1002
1003 case smt2_tokenizert::OPEN: // function application
1004 return function_application();
1005
1006 case smt2_tokenizert::END_OF_FILE:
1007 throw error("EOF in an expression");
1008
1009 case smt2_tokenizert::CLOSE:
1010 case smt2_tokenizert::STRING_LITERAL:
1011 case smt2_tokenizert::NONE:
1012 case smt2_tokenizert::KEYWORD:
1013 throw error("unexpected token in an expression");
1014 }
1015
1017}
1018
1020{
1021 expressions["true"] = [] { return true_exprt(); };
1022 expressions["false"] = [] { return false_exprt(); };
1023
1024 expressions["roundNearestTiesToEven"] = [] {
1025 // we encode as 32-bit unsignedbv
1027 };
1028
1029 expressions["roundNearestTiesToAway"] = [this]() -> exprt {
1030 throw error("unsupported rounding mode");
1031 };
1032
1033 expressions["roundTowardPositive"] = [] {
1034 // we encode as 32-bit unsignedbv
1036 };
1037
1038 expressions["roundTowardNegative"] = [] {
1039 // we encode as 32-bit unsignedbv
1041 };
1042
1043 expressions["roundTowardZero"] = [] {
1044 // we encode as 32-bit unsignedbv
1046 };
1047
1048 expressions["lambda"] = [this] { return lambda_expression(); };
1049 expressions["let"] = [this] { return let_expression(); };
1050 expressions["exists"] = [this] { return quantifier_expression(ID_exists); };
1051 expressions["forall"] = [this] { return quantifier_expression(ID_forall); };
1052 expressions["and"] = [this] { return multi_ary(ID_and, operands()); };
1053 expressions["or"] = [this] { return multi_ary(ID_or, operands()); };
1054 expressions["xor"] = [this] { return multi_ary(ID_xor, operands()); };
1055 expressions["not"] = [this] { return unary(ID_not, operands()); };
1056 expressions["="] = [this] { return binary_predicate(ID_equal, operands()); };
1057 expressions["<="] = [this] { return binary_predicate(ID_le, operands()); };
1058 expressions[">="] = [this] { return binary_predicate(ID_ge, operands()); };
1059 expressions["<"] = [this] { return binary_predicate(ID_lt, operands()); };
1060 expressions[">"] = [this] { return binary_predicate(ID_gt, operands()); };
1061
1062 expressions["bvule"] = [this] { return binary_predicate(ID_le, operands()); };
1063
1064 expressions["bvsle"] = [this] {
1066 };
1067
1068 expressions["bvuge"] = [this] { return binary_predicate(ID_ge, operands()); };
1069
1070 expressions["bvsge"] = [this] {
1072 };
1073
1074 expressions["bvult"] = [this] { return binary_predicate(ID_lt, operands()); };
1075
1076 expressions["bvslt"] = [this] {
1078 };
1079
1080 expressions["bvugt"] = [this] { return binary_predicate(ID_gt, operands()); };
1081
1082 expressions["bvsgt"] = [this] {
1084 };
1085
1086 expressions["bvcomp"] = [this] {
1087 auto b0 = from_integer(0, unsignedbv_typet(1));
1088 auto b1 = from_integer(1, unsignedbv_typet(1));
1089 return if_exprt(binary_predicate(ID_equal, operands()), b1, b0);
1090 };
1091
1092 expressions["bvashr"] = [this] {
1094 };
1095
1096 expressions["bvlshr"] = [this] { return binary(ID_lshr, operands()); };
1097 expressions["bvshr"] = [this] { return binary(ID_lshr, operands()); };
1098 expressions["bvlshl"] = [this] { return binary(ID_shl, operands()); };
1099 expressions["bvashl"] = [this] { return binary(ID_shl, operands()); };
1100 expressions["bvshl"] = [this] { return binary(ID_shl, operands()); };
1101 expressions["bvand"] = [this] { return multi_ary(ID_bitand, operands()); };
1102 expressions["bvnand"] = [this] { return multi_ary(ID_bitnand, operands()); };
1103 expressions["bvor"] = [this] { return multi_ary(ID_bitor, operands()); };
1104 expressions["bvnor"] = [this] { return multi_ary(ID_bitnor, operands()); };
1105 expressions["bvxor"] = [this] { return multi_ary(ID_bitxor, operands()); };
1106 expressions["bvxnor"] = [this] { return multi_ary(ID_bitxnor, operands()); };
1107 expressions["bvnot"] = [this] { return unary(ID_bitnot, operands()); };
1108 expressions["bvneg"] = [this] { return unary(ID_unary_minus, operands()); };
1109 expressions["bvadd"] = [this] { return multi_ary(ID_plus, operands()); };
1110 expressions["+"] = [this] { return multi_ary(ID_plus, operands()); };
1111 expressions["bvsub"] = [this] { return binary(ID_minus, operands()); };
1112 expressions["bvmul"] = [this] { return multi_ary(ID_mult, operands()); };
1113 expressions["*"] = [this] { return multi_ary(ID_mult, operands()); };
1114
1115 expressions["-"] = [this] {
1116 auto op = operands();
1117 if(op.size() == 1)
1118 return unary(ID_unary_minus, op);
1119 else
1120 return binary(ID_minus, op);
1121 };
1122
1123 expressions["bvsdiv"] = [this] { return bv_division(operands(), true); };
1124 expressions["bvudiv"] = [this] { return bv_division(operands(), false); };
1125 expressions["/"] = [this] { return binary(ID_div, operands()); };
1126 expressions["div"] = [this] { return binary(ID_div, operands()); };
1127
1128 expressions["bvsrem"] = [this] { return bv_mod(operands(), true); };
1129 expressions["bvurem"] = [this] { return bv_mod(operands(), false); };
1130
1131 // 2's complement signed remainder (sign follows divisor)
1132 // We don't have that.
1133 expressions["bvsmod"] = [this] { return bv_mod(operands(), true); };
1134
1135 expressions["mod"] = [this] {
1136 // SMT-LIB2 uses Boute's Euclidean definition for mod,
1137 // which is never negative and undefined when the second
1138 // argument is zero.
1139 return binary(ID_euclidean_mod, operands());
1140 };
1141
1142 expressions["concat"] = [this] {
1143 auto op = operands();
1144
1145 // add the widths
1146 auto op_width = make_range(op).map(
1147 [](const exprt &o) { return to_unsignedbv_type(o.type()).get_width(); });
1148
1149 const std::size_t total_width =
1150 std::accumulate(op_width.begin(), op_width.end(), 0);
1151
1152 return concatenation_exprt(std::move(op), unsignedbv_typet(total_width));
1153 };
1154
1155 expressions["distinct"] = [this] {
1156 // pair-wise different constraint, multi-ary
1157 auto op = operands();
1158 if(op.size() == 2)
1159 return binary_predicate(ID_notequal, op);
1160 else
1161 {
1162 std::vector<exprt> pairwise_constraints;
1163 for(std::size_t i = 0; i < op.size(); i++)
1164 {
1165 for(std::size_t j = i; j < op.size(); j++)
1166 {
1167 if(i != j)
1168 pairwise_constraints.push_back(
1169 binary_exprt(op[i], ID_notequal, op[j], bool_typet()));
1170 }
1171 }
1172 return multi_ary(ID_and, pairwise_constraints);
1173 }
1174 };
1175
1176 expressions["ite"] = [this] {
1177 auto op = operands();
1178
1179 if(op.size() != 3)
1180 throw error("ite takes three operands");
1181
1182 if(op[0].type().id() != ID_bool)
1183 throw error("ite takes a boolean as first operand");
1184
1185 if(op[1].type() != op[2].type())
1186 throw error("ite needs matching types");
1187
1188 return if_exprt(op[0], op[1], op[2]);
1189 };
1190
1191 expressions["implies"] = [this] { return binary(ID_implies, operands()); };
1192
1193 expressions["=>"] = [this] { return binary(ID_implies, operands()); };
1194
1195 expressions["select"] = [this] {
1196 auto op = operands();
1197
1198 // array index
1199 if(op.size() != 2)
1200 throw error("select takes two operands");
1201
1202 if(op[0].type().id() != ID_array)
1203 throw error("select expects array operand");
1204
1205 return index_exprt(op[0], op[1]);
1206 };
1207
1208 expressions["store"] = [this] {
1209 auto op = operands();
1210
1211 // array update
1212 if(op.size() != 3)
1213 throw error("store takes three operands");
1214
1215 if(op[0].type().id() != ID_array)
1216 throw error("store expects array operand");
1217
1218 if(to_array_type(op[0].type()).element_type() != op[2].type())
1219 throw error("store expects value that matches array element type");
1220
1221 return with_exprt(op[0], op[1], op[2]);
1222 };
1223
1224 expressions["fp.abs"] = [this] {
1225 auto op = operands();
1226
1227 if(op.size() != 1)
1228 throw error("fp.abs takes one operand");
1229
1230 if(op[0].type().id() != ID_floatbv)
1231 throw error("fp.abs takes FloatingPoint operand");
1232
1233 return abs_exprt(op[0]);
1234 };
1235
1236 expressions["fp.isNaN"] = [this] {
1237 auto op = operands();
1238
1239 if(op.size() != 1)
1240 throw error("fp.isNaN takes one operand");
1241
1242 if(op[0].type().id() != ID_floatbv)
1243 throw error("fp.isNaN takes FloatingPoint operand");
1244
1245 return unary_predicate_exprt(ID_isnan, op[0]);
1246 };
1247
1248 expressions["fp.isInf"] = [this] {
1249 auto op = operands();
1250
1251 if(op.size() != 1)
1252 throw error("fp.isInf takes one operand");
1253
1254 if(op[0].type().id() != ID_floatbv)
1255 throw error("fp.isInf takes FloatingPoint operand");
1256
1257 return unary_predicate_exprt(ID_isinf, op[0]);
1258 };
1259
1260 expressions["fp.isNormal"] = [this] {
1261 auto op = operands();
1262
1263 if(op.size() != 1)
1264 throw error("fp.isNormal takes one operand");
1265
1266 if(op[0].type().id() != ID_floatbv)
1267 throw error("fp.isNormal takes FloatingPoint operand");
1268
1269 return isnormal_exprt(op[0]);
1270 };
1271
1272 expressions["fp"] = [this] { return function_application_fp(operands()); };
1273
1274 expressions["fp.add"] = [this] {
1275 return function_application_ieee_float_op("fp.add", operands());
1276 };
1277
1278 expressions["fp.mul"] = [this] {
1279 return function_application_ieee_float_op("fp.mul", operands());
1280 };
1281
1282 expressions["fp.sub"] = [this] {
1283 return function_application_ieee_float_op("fp.sub", operands());
1284 };
1285
1286 expressions["fp.div"] = [this] {
1287 return function_application_ieee_float_op("fp.div", operands());
1288 };
1289
1290 expressions["fp.rem"] = [this] {
1291 auto op = operands();
1292
1293 // Note that these do not have a rounding mode.
1294 if(op.size() != 2)
1295 throw error() << "fp.rem takes three operands";
1296
1297 if(op[0].type().id() != ID_floatbv || op[1].type().id() != ID_floatbv)
1298 throw error() << "fp.rem takes FloatingPoint operands";
1299
1300 if(op[0].type() != op[1].type())
1301 {
1302 throw error()
1303 << "fp.rem takes FloatingPoint operands with matching sort, "
1304 << "but got " << smt2_format(op[0].type()) << " vs "
1305 << smt2_format(op[1].type());
1306 }
1307
1308 return binary_exprt(op[0], ID_floatbv_rem, op[1]);
1309 };
1310
1311 expressions["fp.eq"] = [this] {
1313 };
1314
1315 expressions["fp.leq"] = [this] {
1316 return binary_predicate(ID_le, operands());
1317 };
1318
1319 expressions["fp.lt"] = [this] { return binary_predicate(ID_lt, operands()); };
1320
1321 expressions["fp.geq"] = [this] {
1322 return binary_predicate(ID_ge, operands());
1323 };
1324
1325 expressions["fp.gt"] = [this] { return binary_predicate(ID_gt, operands()); };
1326
1327 expressions["fp.neg"] = [this] { return unary(ID_unary_minus, operands()); };
1328}
1329
1331{
1332 std::vector<typet> sorts;
1333
1334 // (-> sort+ sort)
1335 // The last sort is the co-domain.
1336
1337 while(smt2_tokenizer.peek() != smt2_tokenizert::CLOSE)
1338 {
1339 if(smt2_tokenizer.peek() == smt2_tokenizert::END_OF_FILE)
1340 throw error() << "unexpected end-of-file in a function sort";
1341
1342 sorts.push_back(sort()); // recursive call
1343 }
1344
1345 next_token(); // eat the ')'
1346
1347 if(sorts.size() < 2)
1348 throw error() << "expected function sort to have at least 2 type arguments";
1349
1350 auto codomain = std::move(sorts.back());
1351 sorts.pop_back();
1352
1353 return mathematical_function_typet(std::move(sorts), std::move(codomain));
1354}
1355
1357{
1358 // a sort is one of the following three cases:
1359 // SYMBOL
1360 // ( _ SYMBOL ...
1361 // ( SYMBOL ...
1362 switch(next_token())
1363 {
1364 case smt2_tokenizert::SYMBOL:
1365 break;
1366
1367 case smt2_tokenizert::OPEN:
1368 if(smt2_tokenizer.next_token() != smt2_tokenizert::SYMBOL)
1369 throw error("expected symbol after '(' in a sort ");
1370
1371 if(smt2_tokenizer.get_buffer() == "_")
1372 {
1373 if(next_token() != smt2_tokenizert::SYMBOL)
1374 throw error("expected symbol after '_' in a sort");
1375 }
1376 break;
1377
1378 case smt2_tokenizert::CLOSE:
1379 case smt2_tokenizert::NUMERAL:
1380 case smt2_tokenizert::STRING_LITERAL:
1381 case smt2_tokenizert::NONE:
1382 case smt2_tokenizert::KEYWORD:
1383 throw error() << "unexpected token in a sort: '"
1384 << smt2_tokenizer.get_buffer() << '\'';
1385
1386 case smt2_tokenizert::END_OF_FILE:
1387 throw error() << "unexpected end-of-file in a sort";
1388 }
1389
1390 // now we have a SYMBOL
1391 const auto &token = smt2_tokenizer.get_buffer();
1392
1393 const auto s_it = sorts.find(token);
1394
1395 if(s_it == sorts.end())
1396 throw error() << "unexpected sort: '" << token << '\'';
1397
1398 return s_it->second();
1399}
1400
1402{
1403 sorts["Bool"] = [] { return bool_typet(); };
1404 sorts["Int"] = [] { return integer_typet(); };
1405 sorts["Real"] = [] { return real_typet(); };
1406
1407 sorts["Float16"] = [] {
1409 };
1410 sorts["Float32"] = [] {
1412 };
1413 sorts["Float64"] = [] {
1415 };
1416 sorts["Float128"] = [] {
1418 };
1419
1420 sorts["BitVec"] = [this] {
1421 if(next_token() != smt2_tokenizert::NUMERAL)
1422 throw error("expected numeral as bit-width");
1423
1424 auto width = std::stoll(smt2_tokenizer.get_buffer());
1425
1426 // eat the ')'
1427 if(next_token() != smt2_tokenizert::CLOSE)
1428 throw error("expected ')' at end of sort");
1429
1430 return unsignedbv_typet(width);
1431 };
1432
1433 sorts["FloatingPoint"] = [this] {
1434 if(next_token() != smt2_tokenizert::NUMERAL)
1435 throw error("expected numeral as bit-width");
1436
1437 const auto width_e = std::stoll(smt2_tokenizer.get_buffer());
1438
1439 if(next_token() != smt2_tokenizert::NUMERAL)
1440 throw error("expected numeral as bit-width");
1441
1442 const auto width_f = std::stoll(smt2_tokenizer.get_buffer());
1443
1444 // consume the ')'
1445 if(next_token() != smt2_tokenizert::CLOSE)
1446 throw error("expected ')' at end of sort");
1447
1448 return ieee_float_spect(width_f - 1, width_e).to_type();
1449 };
1450
1451 sorts["Array"] = [this] {
1452 // this gets two sorts as arguments, domain and range
1453 auto domain = sort();
1454 auto range = sort();
1455
1456 // eat the ')'
1457 if(next_token() != smt2_tokenizert::CLOSE)
1458 throw error("expected ')' at end of Array sort");
1459
1460 // we can turn arrays that map an unsigned bitvector type
1461 // to something else into our 'array_typet'
1462 if(domain.id() == ID_unsignedbv)
1463 return array_typet(range, infinity_exprt(domain));
1464 else
1465 throw error("unsupported array sort");
1466 };
1467
1468 sorts["->"] = [this] { return function_sort(); };
1469}
1470
1473{
1474 if(next_token() != smt2_tokenizert::OPEN)
1475 throw error("expected '(' at beginning of signature");
1476
1477 if(smt2_tokenizer.peek() == smt2_tokenizert::CLOSE)
1478 {
1479 // no parameters
1480 next_token(); // eat the ')'
1482 }
1483
1485 std::vector<irep_idt> parameters;
1486
1487 while(smt2_tokenizer.peek() != smt2_tokenizert::CLOSE)
1488 {
1489 if(next_token() != smt2_tokenizert::OPEN)
1490 throw error("expected '(' at beginning of parameter");
1491
1492 if(next_token() != smt2_tokenizert::SYMBOL)
1493 throw error("expected symbol in parameter");
1494
1496 domain.push_back(sort());
1497 parameters.push_back(id);
1498
1499 if(next_token() != smt2_tokenizert::CLOSE)
1500 throw error("expected ')' at end of parameter");
1501 }
1502
1503 next_token(); // eat the ')'
1504
1505 typet codomain = sort();
1506
1508 mathematical_function_typet(domain, codomain), parameters);
1509}
1510
1512{
1513 if(next_token() != smt2_tokenizert::OPEN)
1514 throw error("expected '(' at beginning of signature");
1515
1516 if(smt2_tokenizer.peek() == smt2_tokenizert::CLOSE)
1517 {
1518 next_token(); // eat the ')'
1519 return sort();
1520 }
1521
1523
1524 while(smt2_tokenizer.peek() != smt2_tokenizert::CLOSE)
1525 domain.push_back(sort());
1526
1527 next_token(); // eat the ')'
1528
1529 typet codomain = sort();
1530
1531 return mathematical_function_typet(domain, codomain);
1532}
1533
1534void smt2_parsert::command(const std::string &c)
1535{
1536 auto c_it = commands.find(c);
1537 if(c_it == commands.end())
1538 {
1539 // silently ignore
1541 }
1542 else
1543 c_it->second();
1544}
1545
1547{
1548 commands["declare-const"] = [this]() {
1549 const auto s = smt2_tokenizer.get_buffer();
1550
1551 if(next_token() != smt2_tokenizert::SYMBOL)
1552 throw error() << "expected a symbol after " << s;
1553
1555 auto type = sort();
1556
1557 add_unique_id(id, exprt(ID_nil, type));
1558 };
1559
1560 // declare-var appears to be a synonym for declare-const that is
1561 // accepted by Z3 and CVC4
1562 commands["declare-var"] = commands["declare-const"];
1563
1564 commands["declare-fun"] = [this]() {
1565 if(next_token() != smt2_tokenizert::SYMBOL)
1566 throw error("expected a symbol after declare-fun");
1567
1569 auto type = function_signature_declaration();
1570
1571 add_unique_id(id, exprt(ID_nil, type));
1572 };
1573
1574 commands["define-const"] = [this]() {
1575 if(next_token() != smt2_tokenizert::SYMBOL)
1576 throw error("expected a symbol after define-const");
1577
1578 const irep_idt id = smt2_tokenizer.get_buffer();
1579
1580 const auto type = sort();
1581 const auto value = expression();
1582
1583 // check type of value
1584 if(value.type() != type)
1585 {
1586 throw error() << "type mismatch in constant definition: expected '"
1587 << smt2_format(type) << "' but got '"
1588 << smt2_format(value.type()) << '\'';
1589 }
1590
1591 // create the entry
1592 add_unique_id(id, value);
1593 };
1594
1595 commands["define-fun"] = [this]() {
1596 if(next_token() != smt2_tokenizert::SYMBOL)
1597 throw error("expected a symbol after define-fun");
1598
1599 const irep_idt id = smt2_tokenizer.get_buffer();
1600
1601 const auto signature = function_signature_definition();
1602
1603 // put the parameters into the scope and take care of hiding
1604 std::vector<std::pair<irep_idt, idt>> hidden_ids;
1605
1606 for(const auto &pair : signature.ids_and_types())
1607 {
1608 auto insert_result =
1609 id_map.insert({pair.first, idt{idt::PARAMETER, pair.second}});
1610 if(!insert_result.second) // already there
1611 {
1612 auto &id_entry = *insert_result.first;
1613 hidden_ids.emplace_back(id_entry.first, std::move(id_entry.second));
1614 id_entry.second = idt{idt::PARAMETER, pair.second};
1615 }
1616 }
1617
1618 // now parse body with parameter ids in place
1619 auto body = expression();
1620
1621 // remove the parameter ids
1622 for(auto &id : signature.parameters)
1623 id_map.erase(id);
1624
1625 // restore the hidden ids, if any
1626 for(auto &hidden_id : hidden_ids)
1627 id_map.insert(std::move(hidden_id));
1628
1629 // check type of body
1630 if(signature.type.id() == ID_mathematical_function)
1631 {
1632 const auto &f_signature = to_mathematical_function_type(signature.type);
1633 if(body.type() != f_signature.codomain())
1634 {
1635 throw error() << "type mismatch in function definition: expected '"
1636 << smt2_format(f_signature.codomain()) << "' but got '"
1637 << smt2_format(body.type()) << '\'';
1638 }
1639 }
1640 else if(body.type() != signature.type)
1641 {
1642 throw error() << "type mismatch in function definition: expected '"
1643 << smt2_format(signature.type) << "' but got '"
1644 << smt2_format(body.type()) << '\'';
1645 }
1646
1647 // if there are parameters, this is a lambda
1648 if(!signature.parameters.empty())
1649 body = lambda_exprt(signature.binding_variables(), body);
1650
1651 // create the entry
1652 add_unique_id(id, std::move(body));
1653 };
1654
1655 commands["exit"] = [this]() { exit = true; };
1656}
constant_exprt from_integer(const mp_integer &int_value, const typet &type)
Definition: arith_tools.cpp:99
API to expression classes for bitvectors.
Pre-defined bitvector types.
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:346
Array constructor from single element.
Definition: std_expr.h:1411
Arrays with given size.
Definition: std_types.h:763
A base class for binary expressions.
Definition: std_expr.h:550
A base class for expressions that are predicates, i.e., Boolean-typed, and that take exactly two argu...
Definition: std_expr.h:643
std::vector< symbol_exprt > variablest
Definition: std_expr.h:2902
std::size_t get_width() const
Definition: std_types.h:864
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:2807
Division.
Definition: std_expr.h:1064
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:37
Equality.
Definition: std_expr.h:1225
Base class for all expressions.
Definition: expr.h:54
std::vector< exprt > operandst
Definition: expr.h:56
typet & type()
Return the type of the expression.
Definition: expr.h:82
operandst & operands()
Definition: expr.h:92
Extracts a sub-range of a bit-vector operand.
The Boolean constant false.
Definition: std_expr.h:2865
Semantic type conversion from/to floating-point formats.
Definition: floatbv_expr.h:19
Application of (mathematical) function.
IEEE-floating-point equality.
Definition: floatbv_expr.h:264
IEEE floating-point operations These have two data operands (op0 and op1) and one rounding mode (op2)...
Definition: floatbv_expr.h:364
static ieee_float_spect half_precision()
Definition: ieee_float.h:64
static ieee_float_spect single_precision()
Definition: ieee_float.h:71
static ieee_float_spect quadruple_precision()
Definition: ieee_float.h:83
class floatbv_typet to_type() const
Definition: ieee_float.cpp:25
static ieee_float_spect double_precision()
Definition: ieee_float.h:77
constant_exprt to_expr() const
Definition: ieee_float.cpp:703
static ieee_floatt plus_infinity(const ieee_float_spect &_spec)
Definition: ieee_float.h:212
static ieee_floatt NaN(const ieee_float_spect &_spec)
Definition: ieee_float.h:209
static ieee_floatt minus_infinity(const ieee_float_spect &_spec)
Definition: ieee_float.h:215
@ ROUND_TO_PLUS_INF
Definition: ieee_float.h:126
@ ROUND_TO_MINUS_INF
Definition: ieee_float.h:125
void from_base10(const mp_integer &exp, const mp_integer &frac)
compute f * (10^e)
Definition: ieee_float.cpp:487
The trinary if-then-else operator.
Definition: std_expr.h:2226
Array index operator.
Definition: std_expr.h:1328
An expression denoting infinity.
Definition: std_expr.h:2890
constant_exprt largest_expr() const
Return an expression representing the largest value of this type.
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.
Definition: floatbv_expr.h:220
A (mathematical) lambda expression.
A let expression.
Definition: std_expr.h:2973
A type for mathematical functions (do not confuse with functions/methods in code)
std::vector< typet > domaint
Modulo defined as lhs-(rhs * truncate(lhs/rhs)).
Definition: std_expr.h:1135
The NIL expression.
Definition: std_expr.h:2874
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()
Definition: smt2_parser.cpp:44
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.
Definition: smt2_parser.cpp:37
std::unordered_map< std::string, std::function< exprt()> > expressions
Definition: smt2_parser.h:149
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
Definition: smt2_parser.h:190
void setup_sorts()
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()
Definition: smt2_parser.cpp:89
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()
exprt expression()
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()
Definition: smt2_parser.cpp:25
std::unordered_map< std::string, std::function< typet()> > sorts
Definition: smt2_parser.h:186
smt2_tokenizert smt2_tokenizer
Definition: smt2_parser.h:92
exprt unary(irep_idt, const exprt::operandst &)
void setup_commands()
enum { NONE, END_OF_FILE, STRING_LITERAL, NUMERAL, SYMBOL, KEYWORD, OPEN, CLOSE } tokent
const std::string & get_buffer() const
bool token_is_quoted_symbol() const
Expression to hold a symbol (variable)
Definition: std_expr.h:80
const irep_idt & get_identifier() const
Definition: std_expr.h:109
The Boolean constant true.
Definition: std_expr.h:2856
Semantic type conversion.
Definition: std_expr.h:1920
The type of an expression, extends irept.
Definition: type.h:29
Generic base class for unary expressions.
Definition: std_expr.h:281
A base class for expressions that are predicates, i.e., Boolean-typed, and that take exactly one argu...
Definition: std_expr.h:495
Fixed-width bit-vector with unsigned binary interpretation.
Operator to update elements in structs and arrays.
Definition: std_expr.h:2312
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:12
#define CHECK_RETURN(CONDITION)
Definition: invariant.h:495
#define UNREACHABLE
This should be used to mark dead code.
Definition: invariant.h:503
const constant_exprt & to_constant_expr(const exprt &expr)
Cast an exprt to a constant_exprt.
Definition: std_expr.h:2840
const array_typet & to_array_type(const typet &type)
Cast a typet to an array_typet.
Definition: std_types.h:832
bool is_signed(const typet &t)
Convenience function – is the type signed?
Definition: util.cpp:45