29 if(token == smt2_tokenizert::OPEN)
31 else if(token == smt2_tokenizert::CLOSE)
40 if(
next_token() == smt2_tokenizert::END_OF_FILE)
57 throw error(
"command must start with '('");
62 throw error(
"expected symbol as command");
69 case smt2_tokenizert::END_OF_FILE:
71 "expected closing parenthesis at end of command,"
74 case smt2_tokenizert::CLOSE:
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");
91 std::size_t parentheses=0;
96 case smt2_tokenizert::OPEN:
101 case smt2_tokenizert::CLOSE:
109 case smt2_tokenizert::END_OF_FILE:
110 throw error(
"unexpected EOF in command");
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:
147 std::piecewise_construct,
148 std::forward_as_tuple(new_id),
149 std::forward_as_tuple(kind, expr))
162 std::piecewise_construct,
163 std::forward_as_tuple(
id),
164 std::forward_as_tuple(idt::VARIABLE, expr))
168 throw error() <<
"identifier '" <<
id <<
"' defined twice";
185 throw error(
"expected bindings after let");
187 std::vector<std::pair<irep_idt, exprt>> bindings;
194 throw error(
"expected symbol in binding");
202 throw error(
"expected ')' after value in binding");
205 std::pair<irep_idt, exprt>(identifier, value));
209 throw error(
"expected ')' at end of bindings");
215 for(
auto &b : bindings)
218 b.first =
add_fresh_id(b.first, idt::BINDING, b.second);
224 throw error(
"expected ')' after let");
229 for(
const auto &b : bindings)
231 variables.push_back(
symbol_exprt(b.first, b.second.type()));
232 values.push_back(b.second);
241 return let_exprt(variables, values, where);
247 throw error() <<
"expected bindings after " << id;
249 std::vector<symbol_exprt> bindings;
256 throw error(
"expected symbol in binding");
263 throw error(
"expected ')' after sort in binding");
269 throw error(
"expected ')' at end of bindings");
275 for(
auto &b : bindings)
280 b.set_identifier(
id);
286 throw error() <<
"expected ')' after " << id;
291 for(
const auto &b : bindings)
292 id_map.erase(b.get_identifier());
298 for(
auto r_it=bindings.rbegin(); r_it!=bindings.rend(); r_it++)
314 if(op.size() != function_type.domain().size())
315 throw error(
"wrong number of arguments for function");
317 for(std::size_t i=0; i<op.size(); i++)
319 if(op[i].type() != function_type.domain()[i])
320 throw error(
"wrong type for arguments for function");
330 for(
auto &expr : result)
332 if(expr.type().id() == ID_signedbv)
335 else if(expr.type().id() != ID_unsignedbv)
337 throw error(
"expected unsigned bitvector");
351 if(expr.
type().
id()==ID_unsignedbv)
354 if(expr.
type().
id()!=ID_signedbv)
355 throw error(
"expected signed bitvector");
364 throw error(
"expression must have at least one operand");
366 for(std::size_t i = 1; i < op.size(); i++)
368 if(op[i].type() != op[0].type())
370 throw error() <<
"expression must have operands with matching types,"
377 exprt result(
id, op[0].type());
385 throw error(
"expression must have two operands");
387 if(op[0].type() != op[1].type())
389 throw error() <<
"expression must have operands with matching types,"
401 throw error(
"expression must have one operand");
409 throw error(
"expression must have two operands");
411 if(op[0].type() != op[1].type())
412 throw error(
"expression must have operands with matching types");
421 throw error() <<
"FloatingPoint equality takes two operands";
423 if(op[0].type().
id() != ID_floatbv || op[1].type().
id() != ID_floatbv)
424 throw error() <<
"FloatingPoint equality takes FloatingPoint operands";
426 if(op[0].type() != op[1].type())
428 throw error() <<
"FloatingPoint equality takes FloatingPoint operands with "
429 <<
"matching sort, but got " <<
smt2_format(op[0].type())
441 throw error() <<
id <<
" takes three operands";
443 if(op[1].type().
id() != ID_floatbv || op[2].type().
id() != ID_floatbv)
444 throw error() <<
id <<
" takes FloatingPoint operands";
446 if(op[1].type() != op[2].type())
448 throw error() <<
id <<
" takes FloatingPoint operands with matching sort, "
449 <<
"but got " <<
smt2_format(op[1].type()) <<
" vs "
455 id ==
"fp.add" ? ID_floatbv_plus :
456 id ==
"fp.sub" ? ID_floatbv_minus :
457 id ==
"fp.mul" ? ID_floatbv_mult :
458 id ==
"fp.div" ? ID_floatbv_div :
459 throw error(
"unsupported floating-point operation");
469 throw error(
"fp takes three operands");
471 if(op[0].type().
id() != ID_unsignedbv)
472 throw error(
"fp takes BitVec as first operand");
474 if(op[1].type().
id() != ID_unsignedbv)
475 throw error(
"fp takes BitVec as second operand");
477 if(op[2].type().
id() != ID_unsignedbv)
478 throw error(
"fp takes BitVec as third operand");
481 throw error(
"fp takes BitVec of size 1 as first operand");
496 case smt2_tokenizert::SYMBOL:
501 throw error(
"expected symbol after '_'");
509 throw error(
"expected numeral as bitvector literal width");
514 throw error(
"expected ')' after bitvector literal");
520 throw error() <<
"unknown indexed identifier "
535 if(term.type().id() != ID_bool)
536 throw error(
"named terms must be Boolean");
546 throw error(
"invalid name attribute, expected symbol");
549 throw error(
"unknown term attribute");
553 throw error(
"expected ')' at end of term attribute");
563 return e_it->second();
570 auto id_it =
id_map.find(final_id);
573 if(id_it->second.type.id() == ID_mathematical_function)
582 throw error() <<
"unknown function symbol '" <<
id <<
'\'';
586 case smt2_tokenizert::OPEN:
594 throw error(
"expected symbol after '_'");
601 throw error(
"expected numeral after extract");
606 throw error(
"expected two numerals after extract");
611 throw error(
"expected ')' after extract");
616 throw error(
"extract takes one operand");
622 throw error(
"extract got bad indices");
628 else if(
id==
"rotate_left" ||
629 id==
"rotate_right" ||
635 throw error() <<
"expected numeral after " << id;
640 throw error() <<
"expected ')' after " <<
id <<
" index";
645 throw error() <<
id <<
" takes one operand";
647 if(
id==
"rotate_left")
652 else if(
id==
"rotate_right")
657 else if(
id==
"sign_extend")
671 else if(
id==
"zero_extend")
678 else if(
id == ID_repeat)
687 else if(
id ==
"to_fp")
690 throw error(
"expected number after to_fp");
695 throw error(
"expected second number after to_fp");
700 throw error(
"expected ')' after to_fp");
705 throw error(
"expected number after to_fp");
710 throw error(
"expected ')' at the end of to_fp");
714 auto dot_pos = real_number.find(
'.');
715 if(dot_pos == std::string::npos)
723 std::string significand_str;
724 significand_str.reserve(real_number.size());
725 for(
auto ch : real_number)
727 significand_str += ch;
743 throw error() <<
"unknown indexed identifier '"
760 <<
"unexpected 'as const' expression expects array type";
766 throw error() <<
"expecting ')' after sort in 'as const'";
770 if(value.type() != array_sort.subtype())
771 throw error() <<
"unexpected 'as const' with wrong element type";
774 throw error() <<
"expecting ')' at the end of 'as const'";
779 throw error() <<
"unexpected 'as' expression";
790 throw error(
"mismatched parentheses in an expression");
805 throw error(
"mismatched parentheses in an expression");
812 case smt2_tokenizert::CLOSE:
813 case smt2_tokenizert::NUMERAL:
814 case smt2_tokenizert::STRING_LITERAL:
815 case smt2_tokenizert::END_OF_FILE:
816 case smt2_tokenizert::NONE:
817 case smt2_tokenizert::KEYWORD:
821 throw error(
"mismatched parentheses in an expression");
833 case smt2_tokenizert::SYMBOL:
840 return e_it->second();
844 auto id_it =
id_map.find(final_id);
849 symbol_expr.
set(ID_C_quoted,
true);
850 return std::move(symbol_expr);
854 throw error() <<
"unknown expression '" << identifier <<
'\'';
857 case smt2_tokenizert::NUMERAL:
860 if(buffer.size() >= 2 && buffer[0] ==
'#' && buffer[1] ==
'x')
864 const std::size_t width = 4 * (buffer.size() - 2);
869 else if(buffer.size() >= 2 && buffer[0] ==
'#' && buffer[1] ==
'b')
873 const std::size_t width = buffer.size() - 2;
884 case smt2_tokenizert::OPEN:
887 case smt2_tokenizert::END_OF_FILE:
888 throw error(
"EOF in an expression");
890 case smt2_tokenizert::CLOSE:
891 case smt2_tokenizert::STRING_LITERAL:
892 case smt2_tokenizert::NONE:
893 case smt2_tokenizert::KEYWORD:
894 throw error(
"unexpected token in an expression");
911 throw error(
"unsupported rounding mode");
998 return unary(ID_unary_minus, op);
1000 return binary(ID_minus, op);
1034 const std::size_t total_width =
1035 std::accumulate(op_width.begin(), op_width.end(), 0);
1047 std::vector<exprt> pairwise_constraints;
1048 for(std::size_t i = 0; i < op.size(); i++)
1050 for(std::size_t j = i; j < op.size(); j++)
1053 pairwise_constraints.push_back(
1057 return multi_ary(ID_and, pairwise_constraints);
1065 throw error(
"ite takes three operands");
1067 if(op[0].type().
id() != ID_bool)
1068 throw error(
"ite takes a boolean as first operand");
1070 if(op[1].type() != op[2].type())
1071 throw error(
"ite needs matching types");
1073 return if_exprt(op[0], op[1], op[2]);
1085 throw error(
"select takes two operands");
1087 if(op[0].type().
id() != ID_array)
1088 throw error(
"select expects array operand");
1098 throw error(
"store takes three operands");
1100 if(op[0].type().
id() != ID_array)
1101 throw error(
"store expects array operand");
1104 throw error(
"store expects value that matches array element type");
1113 throw error(
"fp.isNaN takes one operand");
1115 if(op[0].type().
id() != ID_floatbv)
1116 throw error(
"fp.isNaN takes FloatingPoint operand");
1125 throw error(
"fp.isInf takes one operand");
1127 if(op[0].type().
id() != ID_floatbv)
1128 throw error(
"fp.isInf takes FloatingPoint operand");
1137 throw error(
"fp.isNormal takes one operand");
1139 if(op[0].type().
id() != ID_floatbv)
1140 throw error(
"fp.isNormal takes FloatingPoint operand");
1190 case smt2_tokenizert::SYMBOL:
1193 case smt2_tokenizert::OPEN:
1195 throw error(
"expected symbol after '(' in a sort ");
1200 throw error(
"expected symbol after '_' in a sort");
1204 case smt2_tokenizert::CLOSE:
1205 case smt2_tokenizert::NUMERAL:
1206 case smt2_tokenizert::STRING_LITERAL:
1207 case smt2_tokenizert::NONE:
1208 case smt2_tokenizert::KEYWORD:
1209 throw error() <<
"unexpected token in a sort: '"
1212 case smt2_tokenizert::END_OF_FILE:
1213 throw error() <<
"unexpected end-of-file in a sort";
1219 const auto s_it =
sorts.find(token);
1221 if(s_it ==
sorts.end())
1222 throw error() <<
"unexpected sort: '" << token <<
'\'';
1224 return s_it->second();
1233 sorts[
"BitVec"] = [
this] {
1235 throw error(
"expected numeral as bit-width");
1241 throw error(
"expected ')' at end of sort");
1246 sorts[
"FloatingPoint"] = [
this] {
1248 throw error(
"expected numeral as bit-width");
1253 throw error(
"expected numeral as bit-width");
1259 throw error(
"expected ')' at end of sort");
1264 sorts[
"Array"] = [
this] {
1266 auto domain =
sort();
1267 auto range =
sort();
1271 throw error(
"expected ')' at end of Array sort");
1275 if(domain.id() == ID_unsignedbv)
1278 throw error(
"unsupported array sort");
1286 throw error(
"expected '(' at beginning of signature");
1296 std::vector<irep_idt> parameters;
1301 throw error(
"expected '(' at beginning of parameter");
1304 throw error(
"expected symbol in parameter");
1307 domain.push_back(
sort());
1309 parameters.push_back(
1313 throw error(
"expected ')' at end of parameter");
1327 throw error(
"expected '(' at beginning of signature");
1338 domain.push_back(
sort());
1361 commands[
"declare-const"] = [
this]() {
1365 throw error() <<
"expected a symbol after " << s;
1377 commands[
"declare-fun"] = [
this]() {
1379 throw error(
"expected a symbol after declare-fun");
1387 commands[
"define-const"] = [
this]() {
1389 throw error(
"expected a symbol after define-const");
1393 const auto type =
sort();
1397 if(value.type() != type)
1399 throw error() <<
"type mismatch in constant definition: expected '"
1408 commands[
"define-fun"] = [
this]() {
1410 throw error(
"expected a symbol after define-fun");
1424 if(signature.type.id() == ID_mathematical_function)
1427 if(body.type() != f_signature.codomain())
1429 throw error() <<
"type mismatch in function definition: expected '"
1430 <<
smt2_format(f_signature.codomain()) <<
"' but got '"
1434 else if(body.type() != signature.type)
1436 throw error() <<
"type mismatch in function definition: expected '"
1444 id_map.at(
id).type = signature.type;
1445 id_map.at(
id).parameters = signature.parameters;