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.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
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.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 if(upper<lower)
642 throw error("extract got bad indices");
643
644 auto lower_e = from_integer(lower, integer_typet());
645
646 unsignedbv_typet t(upper-lower+1);
647
648 return extractbits_exprt(op[0], lower_e, t);
649 }
650 else if(id=="rotate_left" ||
651 id=="rotate_right" ||
652 id == ID_repeat ||
653 id=="sign_extend" ||
654 id=="zero_extend")
655 {
656 if(next_token() != smt2_tokenizert::NUMERAL)
657 throw error() << "expected numeral after " << id;
658
659 auto index = std::stoll(smt2_tokenizer.get_buffer());
660
661 if(next_token() != smt2_tokenizert::CLOSE)
662 throw error() << "expected ')' after " << id << " index";
663
664 auto op=operands();
665
666 if(op.size()!=1)
667 throw error() << id << " takes one operand";
668
669 if(id=="rotate_left")
670 {
671 auto dist=from_integer(index, integer_typet());
672 return binary_exprt(op[0], ID_rol, dist, op[0].type());
673 }
674 else if(id=="rotate_right")
675 {
676 auto dist=from_integer(index, integer_typet());
677 return binary_exprt(op[0], ID_ror, dist, op[0].type());
678 }
679 else if(id=="sign_extend")
680 {
681 // we first convert to a signed type of the original width,
682 // then extend to the new width, and then go to unsigned
683 const auto width = to_unsignedbv_type(op[0].type()).get_width();
684 const signedbv_typet small_signed_type(width);
685 const signedbv_typet large_signed_type(width + index);
686 const unsignedbv_typet unsigned_type(width + index);
687
688 return typecast_exprt(
690 typecast_exprt(op[0], small_signed_type), large_signed_type),
691 unsigned_type);
692 }
693 else if(id=="zero_extend")
694 {
695 auto width=to_unsignedbv_type(op[0].type()).get_width();
696 unsignedbv_typet unsigned_type(width+index);
697
698 return typecast_exprt(op[0], unsigned_type);
699 }
700 else if(id == ID_repeat)
701 {
702 auto i = from_integer(index, integer_typet());
703 auto width = to_unsignedbv_type(op[0].type()).get_width() * index;
704 return replication_exprt(i, op[0], unsignedbv_typet(width));
705 }
706 else
707 return nil_exprt();
708 }
709 else if(id == "to_fp")
710 {
711 if(next_token() != smt2_tokenizert::NUMERAL)
712 throw error("expected number after to_fp");
713
714 auto width_e = std::stoll(smt2_tokenizer.get_buffer());
715
716 if(next_token() != smt2_tokenizert::NUMERAL)
717 throw error("expected second number after to_fp");
718
719 auto width_f = std::stoll(smt2_tokenizer.get_buffer());
720
721 if(next_token() != smt2_tokenizert::CLOSE)
722 throw error("expected ')' after to_fp");
723
724 // width_f *includes* the hidden bit
725 const ieee_float_spect spec(width_f - 1, width_e);
726
727 auto rounding_mode = expression();
728
729 auto source_op = expression();
730
731 if(next_token() != smt2_tokenizert::CLOSE)
732 throw error("expected ')' at the end of to_fp");
733
734 // There are several options for the source operand:
735 // 1) real or integer
736 // 2) bit-vector, which is interpreted as signed 2's complement
737 // 3) another floating-point format
738 if(
739 source_op.type().id() == ID_real ||
740 source_op.type().id() == ID_integer)
741 {
742 // For now, we can only do this when
743 // the source operand is a constant.
744 if(source_op.is_constant())
745 {
746 mp_integer significand, exponent;
747
748 const auto &real_number =
749 id2string(to_constant_expr(source_op).get_value());
750 auto dot_pos = real_number.find('.');
751 if(dot_pos == std::string::npos)
752 {
753 exponent = 0;
754 significand = string2integer(real_number);
755 }
756 else
757 {
758 // remove the '.'
759 std::string significand_str;
760 significand_str.reserve(real_number.size());
761 for(auto ch : real_number)
762 {
763 if(ch != '.')
764 significand_str += ch;
765 }
766
767 exponent =
768 mp_integer(dot_pos) - mp_integer(real_number.size()) + 1;
769 significand = string2integer(significand_str);
770 }
771
772 ieee_floatt a(
773 spec,
774 static_cast<ieee_floatt::rounding_modet>(
775 numeric_cast_v<int>(to_constant_expr(rounding_mode))));
776 a.from_base10(significand, exponent);
777 return a.to_expr();
778 }
779 else
780 throw error()
781 << "to_fp for non-constant real expressions is not implemented";
782 }
783 else if(source_op.type().id() == ID_unsignedbv)
784 {
785 // The operand is hard-wired to be interpreted as a signed number.
788 source_op,
790 to_unsignedbv_type(source_op.type()).get_width())),
791 rounding_mode,
792 spec.to_type());
793 }
794 else if(source_op.type().id() == ID_floatbv)
795 {
797 source_op, rounding_mode, spec.to_type());
798 }
799 else
800 throw error() << "unexpected sort given as operand to to_fp";
801 }
802 else if(id == "to_fp_unsigned")
803 {
804 if(next_token() != smt2_tokenizert::NUMERAL)
805 throw error("expected number after to_fp_unsigned");
806
807 auto width_e = std::stoll(smt2_tokenizer.get_buffer());
808
809 if(next_token() != smt2_tokenizert::NUMERAL)
810 throw error("expected second number after to_fp_unsigned");
811
812 auto width_f = std::stoll(smt2_tokenizer.get_buffer());
813
814 if(next_token() != smt2_tokenizert::CLOSE)
815 throw error("expected ')' after to_fp_unsigned");
816
817 // width_f *includes* the hidden bit
818 const ieee_float_spect spec(width_f - 1, width_e);
819
820 auto rounding_mode = expression();
821
822 auto source_op = expression();
823
824 if(next_token() != smt2_tokenizert::CLOSE)
825 throw error("expected ')' at the end of to_fp_unsigned");
826
827 if(source_op.type().id() == ID_unsignedbv)
828 {
829 // The operand is hard-wired to be interpreted
830 // as an unsigned number.
832 source_op, rounding_mode, spec.to_type());
833 }
834 else
835 throw error()
836 << "unexpected sort given as operand to to_fp_unsigned";
837 }
838 else if(id == "fp.to_sbv" || id == "fp.to_ubv")
839 {
840 // These are indexed by the number of bits of the result.
841 if(next_token() != smt2_tokenizert::NUMERAL)
842 throw error() << "expected number after " << id;
843
844 auto width = std::stoll(smt2_tokenizer.get_buffer());
845
846 if(next_token() != smt2_tokenizert::CLOSE)
847 throw error() << "expected ')' after " << id;
848
849 auto op = operands();
850
851 if(op.size() != 2)
852 throw error() << id << " takes two operands";
853
854 if(op[1].type().id() != ID_floatbv)
855 throw error() << id << " takes a FloatingPoint operand";
856
857 if(id == "fp.to_sbv")
858 return typecast_exprt(
859 floatbv_typecast_exprt(op[1], op[0], signedbv_typet(width)),
860 unsignedbv_typet(width));
861 else
863 op[1], op[0], unsignedbv_typet(width));
864 }
865 else
866 {
867 throw error() << "unknown indexed identifier '"
868 << smt2_tokenizer.get_buffer() << '\'';
869 }
870 }
871 else if(smt2_tokenizer.get_buffer() == "as")
872 {
873 // This is an extension understood by Z3 and CVC4.
874 if(
875 smt2_tokenizer.peek() == smt2_tokenizert::SYMBOL &&
876 smt2_tokenizer.get_buffer() == "const")
877 {
878 next_token(); // eat the "const"
879 auto sort = this->sort();
880
881 if(sort.id() != ID_array)
882 {
883 throw error()
884 << "unexpected 'as const' expression expects array type";
885 }
886
887 const auto &array_sort = to_array_type(sort);
888
889 if(smt2_tokenizer.next_token() != smt2_tokenizert::CLOSE)
890 throw error() << "expecting ')' after sort in 'as const'";
891
892 auto value = expression();
893
894 if(value.type() != array_sort.element_type())
895 throw error() << "unexpected 'as const' with wrong element type";
896
897 if(smt2_tokenizer.next_token() != smt2_tokenizert::CLOSE)
898 throw error() << "expecting ')' at the end of 'as const'";
899
900 return array_of_exprt(value, array_sort);
901 }
902 else
903 throw error() << "unexpected 'as' expression";
904 }
905 else
906 {
907 // just double parentheses
908 exprt tmp=expression();
909
910 if(
911 next_token() != smt2_tokenizert::CLOSE &&
912 next_token() != smt2_tokenizert::CLOSE)
913 {
914 throw error("mismatched parentheses in an expression");
915 }
916
917 return tmp;
918 }
919 }
920 else
921 {
922 // just double parentheses
923 exprt tmp=expression();
924
925 if(
926 next_token() != smt2_tokenizert::CLOSE &&
927 next_token() != smt2_tokenizert::CLOSE)
928 {
929 throw error("mismatched parentheses in an expression");
930 }
931
932 return tmp;
933 }
934 break;
935
936 case smt2_tokenizert::CLOSE:
937 case smt2_tokenizert::NUMERAL:
938 case smt2_tokenizert::STRING_LITERAL:
939 case smt2_tokenizert::END_OF_FILE:
940 case smt2_tokenizert::NONE:
941 case smt2_tokenizert::KEYWORD:
942 // just parentheses
943 exprt tmp=expression();
944 if(next_token() != smt2_tokenizert::CLOSE)
945 throw error("mismatched parentheses in an expression");
946
947 return tmp;
948 }
949
951}
952
954 const exprt::operandst &operands,
955 bool is_signed)
956{
957 if(operands.size() != 2)
958 throw error() << "bitvector division expects two operands";
959
960 // SMT-LIB2 defines the result of division by 0 to be 1....1
961 auto divisor = symbol_exprt("divisor", operands[1].type());
962 auto divisor_is_zero = equal_exprt(divisor, from_integer(0, divisor.type()));
963 auto all_ones = to_unsignedbv_type(operands[0].type()).largest_expr();
964
965 exprt division_result;
966
967 if(is_signed)
968 {
969 auto signed_operands = cast_bv_to_signed({operands[0], divisor});
970 division_result =
971 cast_bv_to_unsigned(div_exprt(signed_operands[0], signed_operands[1]));
972 }
973 else
974 division_result = div_exprt(operands[0], divisor);
975
976 return let_exprt(
977 {divisor},
978 operands[1],
979 if_exprt(divisor_is_zero, all_ones, division_result));
980}
981
983{
984 if(operands.size() != 2)
985 throw error() << "bitvector modulo expects two operands";
986
987 // SMT-LIB2 defines the result of "lhs modulo 0" to be "lhs"
988 auto dividend = symbol_exprt("dividend", operands[0].type());
989 auto divisor = symbol_exprt("divisor", operands[1].type());
990 auto divisor_is_zero = equal_exprt(divisor, from_integer(0, divisor.type()));
991
992 exprt mod_result;
993
994 // bvurem and bvsrem match our mod_exprt.
995 // bvsmod doesn't.
996 if(is_signed)
997 {
998 auto signed_operands = cast_bv_to_signed({dividend, divisor});
999 mod_result =
1000 cast_bv_to_unsigned(mod_exprt(signed_operands[0], signed_operands[1]));
1001 }
1002 else
1003 mod_result = mod_exprt(dividend, divisor);
1004
1005 return let_exprt(
1006 {dividend, divisor},
1007 {operands[0], operands[1]},
1008 if_exprt(divisor_is_zero, dividend, mod_result));
1009}
1010
1012{
1013 switch(next_token())
1014 {
1015 case smt2_tokenizert::SYMBOL:
1016 {
1017 const auto &identifier = smt2_tokenizer.get_buffer();
1018
1019 // in the expression table?
1020 const auto e_it = expressions.find(identifier);
1021 if(e_it != expressions.end())
1022 return e_it->second();
1023
1024 // rummage through id_map
1025 auto id_it = id_map.find(identifier);
1026 if(id_it != id_map.end())
1027 {
1028 symbol_exprt symbol_expr(identifier, id_it->second.type);
1030 symbol_expr.set(ID_C_quoted, true);
1031 return std::move(symbol_expr);
1032 }
1033
1034 // don't know, give up
1035 throw error() << "unknown expression '" << identifier << '\'';
1036 }
1037
1038 case smt2_tokenizert::NUMERAL:
1039 {
1040 const std::string &buffer = smt2_tokenizer.get_buffer();
1041 if(buffer.size() >= 2 && buffer[0] == '#' && buffer[1] == 'x')
1042 {
1043 mp_integer value =
1044 string2integer(std::string(buffer, 2, std::string::npos), 16);
1045 const std::size_t width = 4 * (buffer.size() - 2);
1046 CHECK_RETURN(width != 0 && width % 4 == 0);
1047 unsignedbv_typet type(width);
1048 return from_integer(value, type);
1049 }
1050 else if(buffer.size() >= 2 && buffer[0] == '#' && buffer[1] == 'b')
1051 {
1052 mp_integer value =
1053 string2integer(std::string(buffer, 2, std::string::npos), 2);
1054 const std::size_t width = buffer.size() - 2;
1055 CHECK_RETURN(width != 0);
1056 unsignedbv_typet type(width);
1057 return from_integer(value, type);
1058 }
1059 else
1060 {
1061 return constant_exprt(buffer, integer_typet());
1062 }
1063 }
1064
1065 case smt2_tokenizert::OPEN: // function application
1066 return function_application();
1067
1068 case smt2_tokenizert::END_OF_FILE:
1069 throw error("EOF in an expression");
1070
1071 case smt2_tokenizert::CLOSE:
1072 case smt2_tokenizert::STRING_LITERAL:
1073 case smt2_tokenizert::NONE:
1074 case smt2_tokenizert::KEYWORD:
1075 throw error("unexpected token in an expression");
1076 }
1077
1079}
1080
1082{
1083 expressions["true"] = [] { return true_exprt(); };
1084 expressions["false"] = [] { return false_exprt(); };
1085
1086 expressions["roundNearestTiesToEven"] = [] {
1087 // we encode as 32-bit unsignedbv
1089 };
1090
1091 expressions["roundNearestTiesToAway"] = [this]() -> exprt {
1092 throw error("unsupported rounding mode");
1093 };
1094
1095 expressions["roundTowardPositive"] = [] {
1096 // we encode as 32-bit unsignedbv
1098 };
1099
1100 expressions["roundTowardNegative"] = [] {
1101 // we encode as 32-bit unsignedbv
1103 };
1104
1105 expressions["roundTowardZero"] = [] {
1106 // we encode as 32-bit unsignedbv
1108 };
1109
1110 expressions["lambda"] = [this] { return lambda_expression(); };
1111 expressions["let"] = [this] { return let_expression(); };
1112 expressions["exists"] = [this] { return quantifier_expression(ID_exists); };
1113 expressions["forall"] = [this] { return quantifier_expression(ID_forall); };
1114 expressions["and"] = [this] { return multi_ary(ID_and, operands()); };
1115 expressions["or"] = [this] { return multi_ary(ID_or, operands()); };
1116 expressions["xor"] = [this] { return multi_ary(ID_xor, operands()); };
1117 expressions["not"] = [this] { return unary(ID_not, operands()); };
1118 expressions["="] = [this] { return binary_predicate(ID_equal, operands()); };
1119 expressions["<="] = [this] { return binary_predicate(ID_le, operands()); };
1120 expressions[">="] = [this] { return binary_predicate(ID_ge, operands()); };
1121 expressions["<"] = [this] { return binary_predicate(ID_lt, operands()); };
1122 expressions[">"] = [this] { return binary_predicate(ID_gt, operands()); };
1123
1124 expressions["bvule"] = [this] { return binary_predicate(ID_le, operands()); };
1125
1126 expressions["bvsle"] = [this] {
1128 };
1129
1130 expressions["bvuge"] = [this] { return binary_predicate(ID_ge, operands()); };
1131
1132 expressions["bvsge"] = [this] {
1134 };
1135
1136 expressions["bvult"] = [this] { return binary_predicate(ID_lt, operands()); };
1137
1138 expressions["bvslt"] = [this] {
1140 };
1141
1142 expressions["bvugt"] = [this] { return binary_predicate(ID_gt, operands()); };
1143
1144 expressions["bvsgt"] = [this] {
1146 };
1147
1148 expressions["bvcomp"] = [this] {
1149 auto b0 = from_integer(0, unsignedbv_typet(1));
1150 auto b1 = from_integer(1, unsignedbv_typet(1));
1151 return if_exprt(binary_predicate(ID_equal, operands()), b1, b0);
1152 };
1153
1154 expressions["bvashr"] = [this] {
1156 };
1157
1158 expressions["bvlshr"] = [this] { return binary(ID_lshr, operands()); };
1159 expressions["bvshr"] = [this] { return binary(ID_lshr, operands()); };
1160 expressions["bvlshl"] = [this] { return binary(ID_shl, operands()); };
1161 expressions["bvashl"] = [this] { return binary(ID_shl, operands()); };
1162 expressions["bvshl"] = [this] { return binary(ID_shl, operands()); };
1163 expressions["bvand"] = [this] { return multi_ary(ID_bitand, operands()); };
1164 expressions["bvnand"] = [this] { return multi_ary(ID_bitnand, operands()); };
1165 expressions["bvor"] = [this] { return multi_ary(ID_bitor, operands()); };
1166 expressions["bvnor"] = [this] { return multi_ary(ID_bitnor, operands()); };
1167 expressions["bvxor"] = [this] { return multi_ary(ID_bitxor, operands()); };
1168 expressions["bvxnor"] = [this] { return multi_ary(ID_bitxnor, operands()); };
1169 expressions["bvnot"] = [this] { return unary(ID_bitnot, operands()); };
1170 expressions["bvneg"] = [this] { return unary(ID_unary_minus, operands()); };
1171 expressions["bvadd"] = [this] { return multi_ary(ID_plus, operands()); };
1172 expressions["+"] = [this] { return multi_ary(ID_plus, operands()); };
1173 expressions["bvsub"] = [this] { return binary(ID_minus, operands()); };
1174 expressions["bvmul"] = [this] { return multi_ary(ID_mult, operands()); };
1175 expressions["*"] = [this] { return multi_ary(ID_mult, operands()); };
1176
1177 expressions["-"] = [this] {
1178 auto op = operands();
1179 if(op.size() == 1)
1180 return unary(ID_unary_minus, op);
1181 else
1182 return binary(ID_minus, op);
1183 };
1184
1185 expressions["bvsdiv"] = [this] { return bv_division(operands(), true); };
1186 expressions["bvudiv"] = [this] { return bv_division(operands(), false); };
1187 expressions["/"] = [this] { return binary(ID_div, operands()); };
1188 expressions["div"] = [this] { return binary(ID_div, operands()); };
1189
1190 expressions["bvsrem"] = [this] { return bv_mod(operands(), true); };
1191 expressions["bvurem"] = [this] { return bv_mod(operands(), false); };
1192
1193 // 2's complement signed remainder (sign follows divisor)
1194 // We don't have that.
1195 expressions["bvsmod"] = [this] { return bv_mod(operands(), true); };
1196
1197 expressions["mod"] = [this] {
1198 // SMT-LIB2 uses Boute's Euclidean definition for mod,
1199 // which is never negative and undefined when the second
1200 // argument is zero.
1201 return binary(ID_euclidean_mod, operands());
1202 };
1203
1204 expressions["concat"] = [this] {
1205 auto op = operands();
1206
1207 // add the widths
1208 auto op_width = make_range(op).map(
1209 [](const exprt &o) { return to_bitvector_type(o.type()).get_width(); });
1210
1211 const std::size_t total_width =
1212 std::accumulate(op_width.begin(), op_width.end(), 0);
1213
1214 return concatenation_exprt(std::move(op), unsignedbv_typet(total_width));
1215 };
1216
1217 expressions["distinct"] = [this] {
1218 // pair-wise different constraint, multi-ary
1219 auto op = operands();
1220 if(op.size() == 2)
1221 return binary_predicate(ID_notequal, op);
1222 else
1223 {
1224 std::vector<exprt> pairwise_constraints;
1225 for(std::size_t i = 0; i < op.size(); i++)
1226 {
1227 for(std::size_t j = i; j < op.size(); j++)
1228 {
1229 if(i != j)
1230 pairwise_constraints.push_back(
1231 binary_exprt(op[i], ID_notequal, op[j], bool_typet()));
1232 }
1233 }
1234 return multi_ary(ID_and, pairwise_constraints);
1235 }
1236 };
1237
1238 expressions["ite"] = [this] {
1239 auto op = operands();
1240
1241 if(op.size() != 3)
1242 throw error("ite takes three operands");
1243
1244 if(!op[0].is_boolean())
1245 throw error("ite takes a boolean as first operand");
1246
1247 if(op[1].type() != op[2].type())
1248 throw error("ite needs matching types");
1249
1250 return if_exprt(op[0], op[1], op[2]);
1251 };
1252
1253 expressions["implies"] = [this] { return binary(ID_implies, operands()); };
1254
1255 expressions["=>"] = [this] { return binary(ID_implies, operands()); };
1256
1257 expressions["select"] = [this] {
1258 auto op = operands();
1259
1260 // array index
1261 if(op.size() != 2)
1262 throw error("select takes two operands");
1263
1264 if(op[0].type().id() != ID_array)
1265 throw error("select expects array operand");
1266
1267 return index_exprt(op[0], op[1]);
1268 };
1269
1270 expressions["store"] = [this] {
1271 auto op = operands();
1272
1273 // array update
1274 if(op.size() != 3)
1275 throw error("store takes three operands");
1276
1277 if(op[0].type().id() != ID_array)
1278 throw error("store expects array operand");
1279
1280 if(to_array_type(op[0].type()).element_type() != op[2].type())
1281 throw error("store expects value that matches array element type");
1282
1283 return with_exprt(op[0], op[1], op[2]);
1284 };
1285
1286 expressions["fp.abs"] = [this] {
1287 auto op = operands();
1288
1289 if(op.size() != 1)
1290 throw error("fp.abs takes one operand");
1291
1292 if(op[0].type().id() != ID_floatbv)
1293 throw error("fp.abs takes FloatingPoint operand");
1294
1295 return abs_exprt(op[0]);
1296 };
1297
1298 expressions["fp.isNaN"] = [this] {
1299 auto op = operands();
1300
1301 if(op.size() != 1)
1302 throw error("fp.isNaN takes one operand");
1303
1304 if(op[0].type().id() != ID_floatbv)
1305 throw error("fp.isNaN takes FloatingPoint operand");
1306
1307 return unary_predicate_exprt(ID_isnan, op[0]);
1308 };
1309
1310 expressions["fp.isInfinite"] = [this] {
1311 auto op = operands();
1312
1313 if(op.size() != 1)
1314 throw error("fp.isInfinite takes one operand");
1315
1316 if(op[0].type().id() != ID_floatbv)
1317 throw error("fp.isInfinite takes FloatingPoint operand");
1318
1319 return unary_predicate_exprt(ID_isinf, op[0]);
1320 };
1321
1322 expressions["fp.isNormal"] = [this] {
1323 auto op = operands();
1324
1325 if(op.size() != 1)
1326 throw error("fp.isNormal takes one operand");
1327
1328 if(op[0].type().id() != ID_floatbv)
1329 throw error("fp.isNormal takes FloatingPoint operand");
1330
1331 return isnormal_exprt(op[0]);
1332 };
1333
1334 expressions["fp.isZero"] = [this] {
1335 auto op = operands();
1336
1337 if(op.size() != 1)
1338 throw error("fp.isZero takes one operand");
1339
1340 if(op[0].type().id() != ID_floatbv)
1341 throw error("fp.isZero takes FloatingPoint operand");
1342
1343 return not_exprt(typecast_exprt(op[0], bool_typet()));
1344 };
1345
1346 expressions["fp"] = [this] { return function_application_fp(operands()); };
1347
1348 expressions["fp.add"] = [this] {
1349 return function_application_ieee_float_op("fp.add", operands());
1350 };
1351
1352 expressions["fp.mul"] = [this] {
1353 return function_application_ieee_float_op("fp.mul", operands());
1354 };
1355
1356 expressions["fp.sub"] = [this] {
1357 return function_application_ieee_float_op("fp.sub", operands());
1358 };
1359
1360 expressions["fp.div"] = [this] {
1361 return function_application_ieee_float_op("fp.div", operands());
1362 };
1363
1364 expressions["fp.rem"] = [this] {
1365 auto op = operands();
1366
1367 // Note that these do not have a rounding mode.
1368 if(op.size() != 2)
1369 throw error() << "fp.rem takes three operands";
1370
1371 if(op[0].type().id() != ID_floatbv || op[1].type().id() != ID_floatbv)
1372 throw error() << "fp.rem takes FloatingPoint operands";
1373
1374 if(op[0].type() != op[1].type())
1375 {
1376 throw error()
1377 << "fp.rem takes FloatingPoint operands with matching sort, "
1378 << "but got " << smt2_format(op[0].type()) << " vs "
1379 << smt2_format(op[1].type());
1380 }
1381
1382 return binary_exprt(op[0], ID_floatbv_rem, op[1]);
1383 };
1384
1385 expressions["fp.eq"] = [this] {
1387 };
1388
1389 expressions["fp.leq"] = [this] {
1390 return binary_predicate(ID_le, operands());
1391 };
1392
1393 expressions["fp.lt"] = [this] { return binary_predicate(ID_lt, operands()); };
1394
1395 expressions["fp.geq"] = [this] {
1396 return binary_predicate(ID_ge, operands());
1397 };
1398
1399 expressions["fp.gt"] = [this] { return binary_predicate(ID_gt, operands()); };
1400
1401 expressions["fp.neg"] = [this] { return unary(ID_unary_minus, operands()); };
1402}
1403
1405{
1406 std::vector<typet> sorts;
1407
1408 // (-> sort+ sort)
1409 // The last sort is the co-domain.
1410
1411 while(smt2_tokenizer.peek() != smt2_tokenizert::CLOSE)
1412 {
1413 if(smt2_tokenizer.peek() == smt2_tokenizert::END_OF_FILE)
1414 throw error() << "unexpected end-of-file in a function sort";
1415
1416 sorts.push_back(sort()); // recursive call
1417 }
1418
1419 next_token(); // eat the ')'
1420
1421 if(sorts.size() < 2)
1422 throw error() << "expected function sort to have at least 2 type arguments";
1423
1424 auto codomain = std::move(sorts.back());
1425 sorts.pop_back();
1426
1427 return mathematical_function_typet(std::move(sorts), std::move(codomain));
1428}
1429
1431{
1432 // a sort is one of the following three cases:
1433 // SYMBOL
1434 // ( _ SYMBOL ...
1435 // ( SYMBOL ...
1436 switch(next_token())
1437 {
1438 case smt2_tokenizert::SYMBOL:
1439 break;
1440
1441 case smt2_tokenizert::OPEN:
1442 if(smt2_tokenizer.next_token() != smt2_tokenizert::SYMBOL)
1443 throw error("expected symbol after '(' in a sort ");
1444
1445 if(smt2_tokenizer.get_buffer() == "_")
1446 {
1447 if(next_token() != smt2_tokenizert::SYMBOL)
1448 throw error("expected symbol after '_' in a sort");
1449 }
1450 break;
1451
1452 case smt2_tokenizert::CLOSE:
1453 case smt2_tokenizert::NUMERAL:
1454 case smt2_tokenizert::STRING_LITERAL:
1455 case smt2_tokenizert::NONE:
1456 case smt2_tokenizert::KEYWORD:
1457 throw error() << "unexpected token in a sort: '"
1458 << smt2_tokenizer.get_buffer() << '\'';
1459
1460 case smt2_tokenizert::END_OF_FILE:
1461 throw error() << "unexpected end-of-file in a sort";
1462 }
1463
1464 // now we have a SYMBOL
1465 const auto &token = smt2_tokenizer.get_buffer();
1466
1467 const auto s_it = sorts.find(token);
1468
1469 if(s_it == sorts.end())
1470 throw error() << "unexpected sort: '" << token << '\'';
1471
1472 return s_it->second();
1473}
1474
1476{
1477 sorts["Bool"] = [] { return bool_typet(); };
1478 sorts["Int"] = [] { return integer_typet(); };
1479 sorts["Real"] = [] { return real_typet(); };
1480
1481 sorts["Float16"] = [] {
1483 };
1484 sorts["Float32"] = [] {
1486 };
1487 sorts["Float64"] = [] {
1489 };
1490 sorts["Float128"] = [] {
1492 };
1493
1494 sorts["BitVec"] = [this] {
1495 if(next_token() != smt2_tokenizert::NUMERAL)
1496 throw error("expected numeral as bit-width");
1497
1498 auto width = std::stoll(smt2_tokenizer.get_buffer());
1499
1500 // eat the ')'
1501 if(next_token() != smt2_tokenizert::CLOSE)
1502 throw error("expected ')' at end of sort");
1503
1504 return unsignedbv_typet(width);
1505 };
1506
1507 sorts["FloatingPoint"] = [this] {
1508 if(next_token() != smt2_tokenizert::NUMERAL)
1509 throw error("expected numeral as bit-width");
1510
1511 const auto width_e = std::stoll(smt2_tokenizer.get_buffer());
1512
1513 if(next_token() != smt2_tokenizert::NUMERAL)
1514 throw error("expected numeral as bit-width");
1515
1516 const auto width_f = std::stoll(smt2_tokenizer.get_buffer());
1517
1518 // consume the ')'
1519 if(next_token() != smt2_tokenizert::CLOSE)
1520 throw error("expected ')' at end of sort");
1521
1522 return ieee_float_spect(width_f - 1, width_e).to_type();
1523 };
1524
1525 sorts["Array"] = [this] {
1526 // this gets two sorts as arguments, domain and range
1527 auto domain = sort();
1528 auto range = sort();
1529
1530 // eat the ')'
1531 if(next_token() != smt2_tokenizert::CLOSE)
1532 throw error("expected ')' at end of Array sort");
1533
1534 // we can turn arrays that map an unsigned bitvector type
1535 // to something else into our 'array_typet'
1536 if(domain.id() == ID_unsignedbv)
1537 return array_typet(range, infinity_exprt(domain));
1538 else
1539 throw error("unsupported array sort");
1540 };
1541
1542 sorts["->"] = [this] { return function_sort(); };
1543}
1544
1547{
1548 if(next_token() != smt2_tokenizert::OPEN)
1549 throw error("expected '(' at beginning of signature");
1550
1551 if(smt2_tokenizer.peek() == smt2_tokenizert::CLOSE)
1552 {
1553 // no parameters
1554 next_token(); // eat the ')'
1556 }
1557
1559 std::vector<irep_idt> parameters;
1560
1561 while(smt2_tokenizer.peek() != smt2_tokenizert::CLOSE)
1562 {
1563 if(next_token() != smt2_tokenizert::OPEN)
1564 throw error("expected '(' at beginning of parameter");
1565
1566 if(next_token() != smt2_tokenizert::SYMBOL)
1567 throw error("expected symbol in parameter");
1568
1570 domain.push_back(sort());
1571 parameters.push_back(id);
1572
1573 if(next_token() != smt2_tokenizert::CLOSE)
1574 throw error("expected ')' at end of parameter");
1575 }
1576
1577 next_token(); // eat the ')'
1578
1579 typet codomain = sort();
1580
1582 mathematical_function_typet(domain, codomain), parameters);
1583}
1584
1586{
1587 if(next_token() != smt2_tokenizert::OPEN)
1588 throw error("expected '(' at beginning of signature");
1589
1590 if(smt2_tokenizer.peek() == smt2_tokenizert::CLOSE)
1591 {
1592 next_token(); // eat the ')'
1593 return sort();
1594 }
1595
1597
1598 while(smt2_tokenizer.peek() != smt2_tokenizert::CLOSE)
1599 domain.push_back(sort());
1600
1601 next_token(); // eat the ')'
1602
1603 typet codomain = sort();
1604
1605 return mathematical_function_typet(domain, codomain);
1606}
1607
1608void smt2_parsert::command(const std::string &c)
1609{
1610 auto c_it = commands.find(c);
1611 if(c_it == commands.end())
1612 {
1613 // silently ignore
1615 }
1616 else
1617 c_it->second();
1618}
1619
1621{
1622 commands["declare-const"] = [this]() {
1623 const auto s = smt2_tokenizer.get_buffer();
1624
1625 if(next_token() != smt2_tokenizert::SYMBOL)
1626 throw error() << "expected a symbol after " << s;
1627
1629 auto type = sort();
1630
1631 add_unique_id(id, exprt(ID_nil, type));
1632 };
1633
1634 // declare-var appears to be a synonym for declare-const that is
1635 // accepted by Z3 and CVC4
1636 commands["declare-var"] = commands["declare-const"];
1637
1638 commands["declare-fun"] = [this]() {
1639 if(next_token() != smt2_tokenizert::SYMBOL)
1640 throw error("expected a symbol after declare-fun");
1641
1643 auto type = function_signature_declaration();
1644
1645 add_unique_id(id, exprt(ID_nil, type));
1646 };
1647
1648 commands["define-const"] = [this]() {
1649 if(next_token() != smt2_tokenizert::SYMBOL)
1650 throw error("expected a symbol after define-const");
1651
1652 const irep_idt id = smt2_tokenizer.get_buffer();
1653
1654 const auto type = sort();
1655 const auto value = expression();
1656
1657 // check type of value
1658 if(value.type() != type)
1659 {
1660 throw error() << "type mismatch in constant definition: expected '"
1661 << smt2_format(type) << "' but got '"
1662 << smt2_format(value.type()) << '\'';
1663 }
1664
1665 // create the entry
1666 add_unique_id(id, value);
1667 };
1668
1669 commands["define-fun"] = [this]() {
1670 if(next_token() != smt2_tokenizert::SYMBOL)
1671 throw error("expected a symbol after define-fun");
1672
1673 const irep_idt id = smt2_tokenizer.get_buffer();
1674
1675 const auto signature = function_signature_definition();
1676
1677 // put the parameters into the scope and take care of hiding
1678 std::vector<std::pair<irep_idt, idt>> hidden_ids;
1679
1680 for(const auto &pair : signature.ids_and_types())
1681 {
1682 auto insert_result =
1683 id_map.insert({pair.first, idt{idt::PARAMETER, pair.second}});
1684 if(!insert_result.second) // already there
1685 {
1686 auto &id_entry = *insert_result.first;
1687 hidden_ids.emplace_back(id_entry.first, std::move(id_entry.second));
1688 id_entry.second = idt{idt::PARAMETER, pair.second};
1689 }
1690 }
1691
1692 // now parse body with parameter ids in place
1693 auto body = expression();
1694
1695 // remove the parameter ids
1696 for(auto &id : signature.parameters)
1697 id_map.erase(id);
1698
1699 // restore the hidden ids, if any
1700 for(auto &hidden_id : hidden_ids)
1701 id_map.insert(std::move(hidden_id));
1702
1703 // check type of body
1704 if(signature.type.id() == ID_mathematical_function)
1705 {
1706 const auto &f_signature = to_mathematical_function_type(signature.type);
1707 if(body.type() != f_signature.codomain())
1708 {
1709 throw error() << "type mismatch in function definition: expected '"
1710 << smt2_format(f_signature.codomain()) << "' but got '"
1711 << smt2_format(body.type()) << '\'';
1712 }
1713 }
1714 else if(body.type() != signature.type)
1715 {
1716 throw error() << "type mismatch in function definition: expected '"
1717 << smt2_format(signature.type) << "' but got '"
1718 << smt2_format(body.type()) << '\'';
1719 }
1720
1721 // if there are parameters, this is a lambda
1722 if(!signature.parameters.empty())
1723 body = lambda_exprt(signature.binding_variables(), body);
1724
1725 // create the entry
1726 add_unique_id(id, std::move(body));
1727 };
1728
1729 commands["exit"] = [this]() { exit = true; };
1730}
constant_exprt from_integer(const mp_integer &int_value, const typet &type)
Target numeric_cast_v(const mp_integer &arg)
Convert an mp_integer to integral type Target An invariant will fail if the conversion is not possibl...
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:442
Array constructor from single element.
Definition std_expr.h:1553
Arrays with given size.
Definition std_types.h:807
A base class for binary expressions.
Definition std_expr.h:638
A base class for expressions that are predicates, i.e., Boolean-typed, and that take exactly two argu...
Definition std_expr.h:731
std::vector< symbol_exprt > variablest
Definition std_expr.h:3101
std::size_t get_width() const
Definition std_types.h:920
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:2987
Division.
Definition std_expr.h:1152
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition dstring.h:38
Equality.
Definition std_expr.h:1361
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:3064
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
constant_exprt to_expr() const
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
void from_base10(const mp_integer &exp, const mp_integer &frac)
compute f * (10^e)
The trinary if-then-else operator.
Definition std_expr.h:2370
Array index operator.
Definition std_expr.h:1465
An expression denoting infinity.
Definition std_expr.h:3089
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:412
const irep_idt & id() const
Definition irep.h:388
Evaluates to true if the operand is a normal number.
A (mathematical) lambda expression.
A let expression.
Definition std_expr.h:3196
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:1223
The NIL expression.
Definition std_expr.h:3073
Boolean negation.
Definition std_expr.h:2327
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()
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:131
const irep_idt & get_identifier() const
Definition std_expr.h:160
The Boolean constant true.
Definition std_expr.h:3055
Semantic type conversion.
Definition std_expr.h:2068
The type of an expression, extends irept.
Definition type.h:29
Generic base class for unary expressions.
Definition std_expr.h:361
A base class for expressions that are predicates, i.e., Boolean-typed, and that take exactly one argu...
Definition std_expr.h:585
Fixed-width bit-vector with unsigned binary interpretation.
Operator to update elements in structs and arrays.
Definition std_expr.h:2471
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:44
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:522
static smt2_format_containert< T > smt2_format(const T &_o)
Definition smt2_format.h:28
BigInt mp_integer
Definition smt_terms.h:17
#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:3037
const array_typet & to_array_type(const typet &type)
Cast a typet to an array_typet.
Definition std_types.h:888
bool is_signed(const typet &t)
Convenience function – is the type signed?
Definition util.cpp:45