26 if(token == smt2_tokenizert::OPEN)
28 else if(token == smt2_tokenizert::CLOSE)
37 if(
next_token() == smt2_tokenizert::END_OF_FILE)
54 throw error(
"command must start with '('");
59 throw error(
"expected symbol as command");
66 case smt2_tokenizert::END_OF_FILE:
68 "expected closing parenthesis at end of command,"
71 case smt2_tokenizert::CLOSE:
75 case smt2_tokenizert::OPEN:
76 case smt2_tokenizert::SYMBOL:
77 case smt2_tokenizert::NUMERAL:
78 case smt2_tokenizert::STRING_LITERAL:
79 case smt2_tokenizert::NONE:
80 case smt2_tokenizert::KEYWORD:
81 throw error(
"expected ')' at end of command");
88 std::size_t parentheses=0;
93 case smt2_tokenizert::OPEN:
98 case smt2_tokenizert::CLOSE:
106 case smt2_tokenizert::END_OF_FILE:
107 throw error(
"unexpected EOF in command");
109 case smt2_tokenizert::SYMBOL:
110 case smt2_tokenizert::NUMERAL:
111 case smt2_tokenizert::STRING_LITERAL:
112 case smt2_tokenizert::NONE:
113 case smt2_tokenizert::KEYWORD:
144 std::piecewise_construct,
145 std::forward_as_tuple(new_id),
146 std::forward_as_tuple(kind, expr))
159 std::piecewise_construct,
160 std::forward_as_tuple(
id),
161 std::forward_as_tuple(idt::VARIABLE, expr))
165 throw error() <<
"identifier '" <<
id <<
"' defined twice";
182 throw error(
"expected bindings after let");
184 std::vector<std::pair<irep_idt, exprt>> bindings;
191 throw error(
"expected symbol in binding");
199 throw error(
"expected ')' after value in binding");
202 std::pair<irep_idt, exprt>(identifier, value));
206 throw error(
"expected ')' at end of bindings");
212 for(
auto &b : bindings)
215 b.first =
add_fresh_id(b.first, idt::BINDING, b.second);
221 throw error(
"expected ')' after let");
226 for(
const auto &b : bindings)
228 variables.push_back(
symbol_exprt(b.first, b.second.type()));
229 values.push_back(b.second);
238 return let_exprt(variables, values, where);
244 throw error() <<
"expected bindings after " << id;
246 std::vector<symbol_exprt> bindings;
253 throw error(
"expected symbol in binding");
260 throw error(
"expected ')' after sort in binding");
266 throw error(
"expected ')' at end of bindings");
272 for(
auto &b : bindings)
277 b.set_identifier(
id);
283 throw error() <<
"expected ')' after " << id;
288 for(
const auto &b : bindings)
289 id_map.erase(b.get_identifier());
295 for(
auto r_it=bindings.rbegin(); r_it!=bindings.rend(); r_it++)
311 if(op.size() != function_type.domain().size())
312 throw error(
"wrong number of arguments for function");
314 for(std::size_t i=0; i<op.size(); i++)
316 if(op[i].type() != function_type.domain()[i])
317 throw error(
"wrong type for arguments for function");
327 for(
auto &expr : result)
329 if(expr.type().id() == ID_signedbv)
332 else if(expr.type().id() != ID_unsignedbv)
334 throw error(
"expected unsigned bitvector");
348 if(expr.
type().
id()==ID_unsignedbv)
351 if(expr.
type().
id()!=ID_signedbv)
352 throw error(
"expected signed bitvector");
361 throw error(
"expression must have at least one operand");
363 for(std::size_t i = 1; i < op.size(); i++)
365 if(op[i].type() != op[0].type())
367 throw error() <<
"expression must have operands with matching types,"
374 exprt result(
id, op[0].type());
382 throw error(
"expression must have two operands");
384 if(op[0].type() != op[1].type())
386 throw error() <<
"expression must have operands with matching types,"
398 throw error(
"expression must have one operand");
406 throw error(
"expression must have two operands");
408 if(op[0].type() != op[1].type())
409 throw error(
"expression must have operands with matching types");
418 throw error() <<
"FloatingPoint equality takes two operands";
420 if(op[0].type().
id() != ID_floatbv || op[1].type().
id() != ID_floatbv)
421 throw error() <<
"FloatingPoint equality takes FloatingPoint operands";
423 if(op[0].type() != op[1].type())
425 throw error() <<
"FloatingPoint equality takes FloatingPoint operands with "
426 <<
"matching sort, but got " <<
smt2_format(op[0].type())
438 throw error() <<
id <<
" takes three operands";
440 if(op[1].type().
id() != ID_floatbv || op[2].type().
id() != ID_floatbv)
441 throw error() <<
id <<
" takes FloatingPoint operands";
443 if(op[1].type() != op[2].type())
445 throw error() <<
id <<
" takes FloatingPoint operands with matching sort, "
446 <<
"but got " <<
smt2_format(op[1].type()) <<
" vs "
452 id ==
"fp.add" ? ID_floatbv_plus :
453 id ==
"fp.sub" ? ID_floatbv_minus :
454 id ==
"fp.mul" ? ID_floatbv_mult :
455 id ==
"fp.div" ? ID_floatbv_div :
456 throw error(
"unsupported floating-point operation");
466 throw error(
"fp takes three operands");
468 if(op[0].type().
id() != ID_unsignedbv)
469 throw error(
"fp takes BitVec as first operand");
471 if(op[1].type().
id() != ID_unsignedbv)
472 throw error(
"fp takes BitVec as second operand");
474 if(op[2].type().
id() != ID_unsignedbv)
475 throw error(
"fp takes BitVec as third operand");
478 throw error(
"fp takes BitVec of size 1 as first operand");
493 case smt2_tokenizert::SYMBOL:
498 throw error(
"expected symbol after '_'");
506 throw error(
"expected numeral as bitvector literal width");
511 throw error(
"expected ')' after bitvector literal");
517 throw error() <<
"unknown indexed identifier "
532 if(term.type().id() != ID_bool)
533 throw error(
"named terms must be Boolean");
543 throw error(
"invalid name attribute, expected symbol");
546 throw error(
"unknown term attribute");
550 throw error(
"expected ')' at end of term attribute");
560 return e_it->second();
567 auto id_it =
id_map.find(final_id);
570 if(id_it->second.type.id() == ID_mathematical_function)
579 throw error() <<
"unknown function symbol '" <<
id <<
'\'';
583 case smt2_tokenizert::OPEN:
591 throw error(
"expected symbol after '_'");
598 throw error(
"expected numeral after extract");
603 throw error(
"expected two numerals after extract");
608 throw error(
"expected ')' after extract");
613 throw error(
"extract takes one operand");
619 throw error(
"extract got bad indices");
625 else if(
id==
"rotate_left" ||
626 id==
"rotate_right" ||
632 throw error() <<
"expected numeral after " << id;
637 throw error() <<
"expected ')' after " <<
id <<
" index";
642 throw error() <<
id <<
" takes one operand";
644 if(
id==
"rotate_left")
649 else if(
id==
"rotate_right")
654 else if(
id==
"sign_extend")
668 else if(
id==
"zero_extend")
675 else if(
id == ID_repeat)
684 throw error() <<
"unknown indexed identifier '"
697 throw error(
"mismatched parentheses in an expression");
712 throw error(
"mismatched parentheses in an expression");
719 case smt2_tokenizert::CLOSE:
720 case smt2_tokenizert::NUMERAL:
721 case smt2_tokenizert::STRING_LITERAL:
722 case smt2_tokenizert::END_OF_FILE:
723 case smt2_tokenizert::NONE:
724 case smt2_tokenizert::KEYWORD:
728 throw error(
"mismatched parentheses in an expression");
740 case smt2_tokenizert::SYMBOL:
747 return e_it->second();
751 auto id_it =
id_map.find(final_id);
756 symbol_expr.
set(ID_C_quoted,
true);
757 return std::move(symbol_expr);
761 throw error() <<
"unknown expression '" << identifier <<
'\'';
764 case smt2_tokenizert::NUMERAL:
767 if(buffer.size() >= 2 && buffer[0] ==
'#' && buffer[1] ==
'x')
771 const std::size_t width = 4 * (buffer.size() - 2);
776 else if(buffer.size() >= 2 && buffer[0] ==
'#' && buffer[1] ==
'b')
780 const std::size_t width = buffer.size() - 2;
791 case smt2_tokenizert::OPEN:
794 case smt2_tokenizert::END_OF_FILE:
795 throw error(
"EOF in an expression");
797 case smt2_tokenizert::CLOSE:
798 case smt2_tokenizert::STRING_LITERAL:
799 case smt2_tokenizert::NONE:
800 case smt2_tokenizert::KEYWORD:
801 throw error(
"unexpected token in an expression");
818 throw error(
"unsupported rounding mode");
928 const std::size_t total_width =
929 std::accumulate(op_width.begin(), op_width.end(), 0);
943 throw error(
"ite takes three operands");
945 if(op[0].type().
id() != ID_bool)
946 throw error(
"ite takes a boolean as first operand");
948 if(op[1].type() != op[2].type())
949 throw error(
"ite needs matching types");
951 return if_exprt(op[0], op[1], op[2]);
963 throw error(
"select takes two operands");
965 if(op[0].type().
id() != ID_array)
966 throw error(
"select expects array operand");
976 throw error(
"store takes three operands");
978 if(op[0].type().
id() != ID_array)
979 throw error(
"store expects array operand");
982 throw error(
"store expects value that matches array element type");
991 throw error(
"fp.isNaN takes one operand");
993 if(op[0].type().
id() != ID_floatbv)
994 throw error(
"fp.isNaN takes FloatingPoint operand");
1003 throw error(
"fp.isInf takes one operand");
1005 if(op[0].type().
id() != ID_floatbv)
1006 throw error(
"fp.isInf takes FloatingPoint operand");
1015 throw error(
"fp.isNormal takes one operand");
1017 if(op[0].type().
id() != ID_floatbv)
1018 throw error(
"fp.isNormal takes FloatingPoint operand");
1068 case smt2_tokenizert::SYMBOL:
1071 case smt2_tokenizert::OPEN:
1073 throw error(
"expected symbol after '(' in a sort ");
1078 throw error(
"expected symbol after '_' in a sort");
1082 case smt2_tokenizert::CLOSE:
1083 case smt2_tokenizert::NUMERAL:
1084 case smt2_tokenizert::STRING_LITERAL:
1085 case smt2_tokenizert::NONE:
1086 case smt2_tokenizert::KEYWORD:
1087 throw error() <<
"unexpected token in a sort: '"
1090 case smt2_tokenizert::END_OF_FILE:
1091 throw error() <<
"unexpected end-of-file in a sort";
1097 const auto s_it =
sorts.find(token);
1099 if(s_it ==
sorts.end())
1100 throw error() <<
"unexpected sort: '" << token <<
'\'';
1102 return s_it->second();
1111 sorts[
"BitVec"] = [
this] {
1113 throw error(
"expected numeral as bit-width");
1119 throw error(
"expected ')' at end of sort");
1124 sorts[
"FloatingPoint"] = [
this] {
1126 throw error(
"expected numeral as bit-width");
1131 throw error(
"expected numeral as bit-width");
1137 throw error(
"expected ')' at end of sort");
1142 sorts[
"Array"] = [
this] {
1144 auto domain =
sort();
1145 auto range =
sort();
1149 throw error(
"expected ')' at end of Array sort");
1153 if(domain.id() == ID_unsignedbv)
1156 throw error(
"unsupported array sort");
1164 throw error(
"expected '(' at beginning of signature");
1174 std::vector<irep_idt> parameters;
1179 throw error(
"expected '(' at beginning of parameter");
1182 throw error(
"expected symbol in parameter");
1185 domain.push_back(
sort());
1187 parameters.push_back(
1191 throw error(
"expected ')' at end of parameter");
1205 throw error(
"expected '(' at beginning of signature");
1218 throw error(
"expected '(' at beginning of parameter");
1221 throw error(
"expected symbol in parameter");
1223 domain.push_back(
sort());
1226 throw error(
"expected ')' at end of parameter");
1250 commands[
"declare-const"] = [
this]() {
1254 throw error() <<
"expected a symbol after " << s;
1266 commands[
"declare-fun"] = [
this]() {
1268 throw error(
"expected a symbol after declare-fun");
1276 commands[
"define-const"] = [
this]() {
1278 throw error(
"expected a symbol after define-const");
1282 const auto type =
sort();
1286 if(value.type() != type)
1288 throw error() <<
"type mismatch in constant definition: expected '"
1297 commands[
"define-fun"] = [
this]() {
1299 throw error(
"expected a symbol after define-fun");
1313 if(signature.type.id() == ID_mathematical_function)
1316 if(body.type() != f_signature.codomain())
1318 throw error() <<
"type mismatch in function definition: expected '"
1319 <<
smt2_format(f_signature.codomain()) <<
"' but got '"
1323 else if(body.type() != signature.type)
1325 throw error() <<
"type mismatch in function definition: expected '"
1333 id_map.at(
id).type = signature.type;
1334 id_map.at(
id).parameters = signature.parameters;