28 if(token == smt2_tokenizert::OPEN)
30 else if(token == smt2_tokenizert::CLOSE)
39 if(
next_token() == smt2_tokenizert::END_OF_FILE)
56 throw error(
"command must start with '('");
61 throw error(
"expected symbol as command");
68 case smt2_tokenizert::END_OF_FILE:
70 "expected closing parenthesis at end of command,"
73 case smt2_tokenizert::CLOSE:
77 case smt2_tokenizert::OPEN:
78 case smt2_tokenizert::SYMBOL:
79 case smt2_tokenizert::NUMERAL:
80 case smt2_tokenizert::STRING_LITERAL:
81 case smt2_tokenizert::NONE:
82 case smt2_tokenizert::KEYWORD:
83 throw error(
"expected ')' at end of command");
90 std::size_t parentheses=0;
95 case smt2_tokenizert::OPEN:
100 case smt2_tokenizert::CLOSE:
108 case smt2_tokenizert::END_OF_FILE:
109 throw error(
"unexpected EOF in command");
111 case smt2_tokenizert::SYMBOL:
112 case smt2_tokenizert::NUMERAL:
113 case smt2_tokenizert::STRING_LITERAL:
114 case smt2_tokenizert::NONE:
115 case smt2_tokenizert::KEYWORD:
146 std::piecewise_construct,
147 std::forward_as_tuple(new_id),
148 std::forward_as_tuple(kind, expr))
161 std::piecewise_construct,
162 std::forward_as_tuple(
id),
163 std::forward_as_tuple(idt::VARIABLE, expr))
167 throw error() <<
"identifier '" <<
id <<
"' defined twice";
184 throw error(
"expected bindings after let");
186 std::vector<std::pair<irep_idt, exprt>> bindings;
193 throw error(
"expected symbol in binding");
201 throw error(
"expected ')' after value in binding");
204 std::pair<irep_idt, exprt>(identifier, value));
208 throw error(
"expected ')' at end of bindings");
214 for(
auto &b : bindings)
217 b.first =
add_fresh_id(b.first, idt::BINDING, b.second);
223 throw error(
"expected ')' after let");
228 for(
const auto &b : bindings)
230 variables.push_back(
symbol_exprt(b.first, b.second.type()));
231 values.push_back(b.second);
240 return let_exprt(variables, values, where);
246 throw error() <<
"expected bindings after " << id;
248 std::vector<symbol_exprt> bindings;
255 throw error(
"expected symbol in binding");
262 throw error(
"expected ')' after sort in binding");
268 throw error(
"expected ')' at end of bindings");
274 for(
auto &b : bindings)
279 b.set_identifier(
id);
285 throw error() <<
"expected ')' after " << id;
290 for(
const auto &b : bindings)
291 id_map.erase(b.get_identifier());
297 for(
auto r_it=bindings.rbegin(); r_it!=bindings.rend(); r_it++)
313 if(op.size() != function_type.domain().size())
314 throw error(
"wrong number of arguments for function");
316 for(std::size_t i=0; i<op.size(); i++)
318 if(op[i].type() != function_type.domain()[i])
319 throw error(
"wrong type for arguments for function");
329 for(
auto &expr : result)
331 if(expr.type().id() == ID_signedbv)
334 else if(expr.type().id() != ID_unsignedbv)
336 throw error(
"expected unsigned bitvector");
350 if(expr.
type().
id()==ID_unsignedbv)
353 if(expr.
type().
id()!=ID_signedbv)
354 throw error(
"expected signed bitvector");
363 throw error(
"expression must have at least one operand");
365 for(std::size_t i = 1; i < op.size(); i++)
367 if(op[i].type() != op[0].type())
369 throw error() <<
"expression must have operands with matching types,"
376 exprt result(
id, op[0].type());
384 throw error(
"expression must have two operands");
386 if(op[0].type() != op[1].type())
388 throw error() <<
"expression must have operands with matching types,"
400 throw error(
"expression must have one operand");
408 throw error(
"expression must have two operands");
410 if(op[0].type() != op[1].type())
411 throw error(
"expression must have operands with matching types");
420 throw error() <<
"FloatingPoint equality takes two operands";
422 if(op[0].type().
id() != ID_floatbv || op[1].type().
id() != ID_floatbv)
423 throw error() <<
"FloatingPoint equality takes FloatingPoint operands";
425 if(op[0].type() != op[1].type())
427 throw error() <<
"FloatingPoint equality takes FloatingPoint operands with "
428 <<
"matching sort, but got " <<
smt2_format(op[0].type())
440 throw error() <<
id <<
" takes three operands";
442 if(op[1].type().
id() != ID_floatbv || op[2].type().
id() != ID_floatbv)
443 throw error() <<
id <<
" takes FloatingPoint operands";
445 if(op[1].type() != op[2].type())
447 throw error() <<
id <<
" takes FloatingPoint operands with matching sort, "
448 <<
"but got " <<
smt2_format(op[1].type()) <<
" vs "
454 id ==
"fp.add" ? ID_floatbv_plus :
455 id ==
"fp.sub" ? ID_floatbv_minus :
456 id ==
"fp.mul" ? ID_floatbv_mult :
457 id ==
"fp.div" ? ID_floatbv_div :
458 throw error(
"unsupported floating-point operation");
468 throw error(
"fp takes three operands");
470 if(op[0].type().
id() != ID_unsignedbv)
471 throw error(
"fp takes BitVec as first operand");
473 if(op[1].type().
id() != ID_unsignedbv)
474 throw error(
"fp takes BitVec as second operand");
476 if(op[2].type().
id() != ID_unsignedbv)
477 throw error(
"fp takes BitVec as third operand");
480 throw error(
"fp takes BitVec of size 1 as first operand");
495 case smt2_tokenizert::SYMBOL:
500 throw error(
"expected symbol after '_'");
508 throw error(
"expected numeral as bitvector literal width");
513 throw error(
"expected ')' after bitvector literal");
519 throw error() <<
"unknown indexed identifier "
534 if(term.type().id() != ID_bool)
535 throw error(
"named terms must be Boolean");
545 throw error(
"invalid name attribute, expected symbol");
548 throw error(
"unknown term attribute");
552 throw error(
"expected ')' at end of term attribute");
562 return e_it->second();
569 auto id_it =
id_map.find(final_id);
572 if(id_it->second.type.id() == ID_mathematical_function)
581 throw error() <<
"unknown function symbol '" <<
id <<
'\'';
585 case smt2_tokenizert::OPEN:
593 throw error(
"expected symbol after '_'");
600 throw error(
"expected numeral after extract");
605 throw error(
"expected two numerals after extract");
610 throw error(
"expected ')' after extract");
615 throw error(
"extract takes one operand");
621 throw error(
"extract got bad indices");
627 else if(
id==
"rotate_left" ||
628 id==
"rotate_right" ||
634 throw error() <<
"expected numeral after " << id;
639 throw error() <<
"expected ')' after " <<
id <<
" index";
644 throw error() <<
id <<
" takes one operand";
646 if(
id==
"rotate_left")
651 else if(
id==
"rotate_right")
656 else if(
id==
"sign_extend")
670 else if(
id==
"zero_extend")
677 else if(
id == ID_repeat)
688 throw error() <<
"unknown indexed identifier '"
701 throw error(
"mismatched parentheses in an expression");
716 throw error(
"mismatched parentheses in an expression");
723 case smt2_tokenizert::CLOSE:
724 case smt2_tokenizert::NUMERAL:
725 case smt2_tokenizert::STRING_LITERAL:
726 case smt2_tokenizert::END_OF_FILE:
727 case smt2_tokenizert::NONE:
728 case smt2_tokenizert::KEYWORD:
732 throw error(
"mismatched parentheses in an expression");
744 case smt2_tokenizert::SYMBOL:
751 return e_it->second();
755 auto id_it =
id_map.find(final_id);
760 symbol_expr.
set(ID_C_quoted,
true);
761 return std::move(symbol_expr);
765 throw error() <<
"unknown expression '" << identifier <<
'\'';
768 case smt2_tokenizert::NUMERAL:
771 if(buffer.size() >= 2 && buffer[0] ==
'#' && buffer[1] ==
'x')
775 const std::size_t width = 4 * (buffer.size() - 2);
780 else if(buffer.size() >= 2 && buffer[0] ==
'#' && buffer[1] ==
'b')
784 const std::size_t width = buffer.size() - 2;
795 case smt2_tokenizert::OPEN:
798 case smt2_tokenizert::END_OF_FILE:
799 throw error(
"EOF in an expression");
801 case smt2_tokenizert::CLOSE:
802 case smt2_tokenizert::STRING_LITERAL:
803 case smt2_tokenizert::NONE:
804 case smt2_tokenizert::KEYWORD:
805 throw error(
"unexpected token in an expression");
822 throw error(
"unsupported rounding mode");
909 return unary(ID_unary_minus, op);
911 return binary(ID_minus, op);
945 const std::size_t total_width =
946 std::accumulate(op_width.begin(), op_width.end(), 0);
958 std::vector<exprt> pairwise_constraints;
959 for(std::size_t i = 0; i < op.size(); i++)
961 for(std::size_t j = i; j < op.size(); j++)
964 pairwise_constraints.push_back(
968 return multi_ary(ID_and, pairwise_constraints);
976 throw error(
"ite takes three operands");
978 if(op[0].type().
id() != ID_bool)
979 throw error(
"ite takes a boolean as first operand");
981 if(op[1].type() != op[2].type())
982 throw error(
"ite needs matching types");
984 return if_exprt(op[0], op[1], op[2]);
996 throw error(
"select takes two operands");
998 if(op[0].type().
id() != ID_array)
999 throw error(
"select expects array operand");
1009 throw error(
"store takes three operands");
1011 if(op[0].type().
id() != ID_array)
1012 throw error(
"store expects array operand");
1015 throw error(
"store expects value that matches array element type");
1024 throw error(
"fp.isNaN takes one operand");
1026 if(op[0].type().
id() != ID_floatbv)
1027 throw error(
"fp.isNaN takes FloatingPoint operand");
1036 throw error(
"fp.isInf takes one operand");
1038 if(op[0].type().
id() != ID_floatbv)
1039 throw error(
"fp.isInf takes FloatingPoint operand");
1048 throw error(
"fp.isNormal takes one operand");
1050 if(op[0].type().
id() != ID_floatbv)
1051 throw error(
"fp.isNormal takes FloatingPoint operand");
1101 case smt2_tokenizert::SYMBOL:
1104 case smt2_tokenizert::OPEN:
1106 throw error(
"expected symbol after '(' in a sort ");
1111 throw error(
"expected symbol after '_' in a sort");
1115 case smt2_tokenizert::CLOSE:
1116 case smt2_tokenizert::NUMERAL:
1117 case smt2_tokenizert::STRING_LITERAL:
1118 case smt2_tokenizert::NONE:
1119 case smt2_tokenizert::KEYWORD:
1120 throw error() <<
"unexpected token in a sort: '"
1123 case smt2_tokenizert::END_OF_FILE:
1124 throw error() <<
"unexpected end-of-file in a sort";
1130 const auto s_it =
sorts.find(token);
1132 if(s_it ==
sorts.end())
1133 throw error() <<
"unexpected sort: '" << token <<
'\'';
1135 return s_it->second();
1144 sorts[
"BitVec"] = [
this] {
1146 throw error(
"expected numeral as bit-width");
1152 throw error(
"expected ')' at end of sort");
1157 sorts[
"FloatingPoint"] = [
this] {
1159 throw error(
"expected numeral as bit-width");
1164 throw error(
"expected numeral as bit-width");
1170 throw error(
"expected ')' at end of sort");
1175 sorts[
"Array"] = [
this] {
1177 auto domain =
sort();
1178 auto range =
sort();
1182 throw error(
"expected ')' at end of Array sort");
1186 if(domain.id() == ID_unsignedbv)
1189 throw error(
"unsupported array sort");
1197 throw error(
"expected '(' at beginning of signature");
1207 std::vector<irep_idt> parameters;
1212 throw error(
"expected '(' at beginning of parameter");
1215 throw error(
"expected symbol in parameter");
1218 domain.push_back(
sort());
1220 parameters.push_back(
1224 throw error(
"expected ')' at end of parameter");
1238 throw error(
"expected '(' at beginning of signature");
1249 domain.push_back(
sort());
1272 commands[
"declare-const"] = [
this]() {
1276 throw error() <<
"expected a symbol after " << s;
1288 commands[
"declare-fun"] = [
this]() {
1290 throw error(
"expected a symbol after declare-fun");
1298 commands[
"define-const"] = [
this]() {
1300 throw error(
"expected a symbol after define-const");
1304 const auto type =
sort();
1308 if(value.type() != type)
1310 throw error() <<
"type mismatch in constant definition: expected '"
1319 commands[
"define-fun"] = [
this]() {
1321 throw error(
"expected a symbol after define-fun");
1335 if(signature.type.id() == ID_mathematical_function)
1338 if(body.type() != f_signature.codomain())
1340 throw error() <<
"type mismatch in function definition: expected '"
1341 <<
smt2_format(f_signature.codomain()) <<
"' but got '"
1345 else if(body.type() != signature.type)
1347 throw error() <<
"type mismatch in function definition: expected '"
1355 id_map.at(
id).type = signature.type;
1356 id_map.at(
id).parameters = signature.parameters;