44 if(
peek() == END_OF_FILE)
51 throw error(
"command must start with '('");
56 throw error(
"expected symbol as command");
65 "expected closing parenthesis at end of command," 73 throw error(
"expected ')' at end of command");
80 std::size_t parentheses=0;
99 throw error(
"unexpected EOF in command");
121 if(
id_map[
id].type.is_nil())
152 throw error(
"expected bindings after let");
154 std::vector<std::pair<irep_idt, exprt>> bindings;
161 throw error(
"expected symbol in binding");
169 throw error(
"expected ')' after value in binding");
172 std::pair<irep_idt, exprt>(identifier, value));
176 throw error(
"expected ')' at end of bindings");
182 for(
auto &b : bindings)
186 auto &entry=
id_map[b.first];
187 entry.type=b.second.type();
188 entry.definition=b.second;
194 throw error(
"expected ')' after let");
199 for(
auto r_it=bindings.rbegin(); r_it!=bindings.rend(); r_it++)
209 for(
const auto &b : bindings)
221 throw error() <<
"expected bindings after " << id;
223 std::vector<symbol_exprt> bindings;
230 throw error(
"expected symbol in binding");
237 throw error(
"expected ')' after sort in binding");
243 throw error(
"expected ')' at end of bindings");
246 for(
const auto &b : bindings)
248 auto &entry=
id_map[b.get_identifier()];
256 throw error() <<
"expected ')' after " << id;
261 for(
const auto &b : bindings)
262 id_map.erase(b.get_identifier());
265 for(
auto r_it=bindings.rbegin(); r_it!=bindings.rend(); r_it++)
268 quantifier.
op0()=*r_it;
281 const auto &f =
id_map[identifier];
284 if(op.size()!=f.type.variables().size())
285 throw error(
"wrong number of arguments for function");
287 for(std::size_t i=0; i<op.size(); i++)
289 if(op[i].type() != f.type.variables()[i].type())
290 throw error(
"wrong type for arguments for function");
305 if(expr.type().id() == ID_signedbv)
308 else if(expr.type().id() != ID_unsignedbv)
310 throw error(
"expected unsigned bitvector");
324 if(expr.
type().
id()==ID_unsignedbv)
327 if(expr.
type().
id()!=ID_signedbv)
328 throw error(
"expected signed bitvector");
337 throw error(
"expression must have at least one operand");
339 for(std::size_t i = 1; i < op.size(); i++)
341 if(op[i].type() != op[0].type())
343 throw error() <<
"expression must have operands with matching types," 358 throw error(
"expression must have two operands");
360 if(op[0].type() != op[1].type())
362 throw error() <<
"expression must have operands with matching types," 374 throw error(
"expression must have one operand");
382 throw error(
"expression must have two operands");
384 if(op[0].type() != op[1].type())
385 throw error(
"expression must have operands with matching types");
395 throw error() <<
id <<
" takes three operands";
397 if(op[1].type().id() != ID_floatbv || op[2].type().id() != ID_floatbv)
398 throw error() <<
id <<
" takes FloatingPoint operands";
400 if(op[1].type() != op[2].type())
402 throw error() <<
id <<
" takes FloatingPoint operands with matching sort, " 403 <<
"but got " <<
smt2_format(op[1].type()) <<
" vs " 409 id ==
"fp.add" ? ID_floatbv_plus :
410 id ==
"fp.sub" ? ID_floatbv_minus :
411 id ==
"fp.mul" ? ID_floatbv_mult :
412 id ==
"fp.div" ? ID_floatbv_div :
413 throw error(
"unsupported floating-point operation");
423 throw error(
"fp takes three operands");
425 if(op[0].type().id() != ID_unsignedbv)
426 throw error(
"fp takes BitVec as first operand");
428 if(op[1].type().id() != ID_unsignedbv)
429 throw error(
"fp takes BitVec as second operand");
431 if(op[2].type().id() != ID_unsignedbv)
432 throw error(
"fp takes BitVec as third operand");
435 throw error(
"fp takes BitVec of size 1 as first operand");
442 c.
operands() = {op[0], op[1], op[2]};
457 throw error(
"expected symbol after '_'");
464 throw error(
"expected numeral as bitvector literal width");
466 auto width=std::stoll(
buffer);
469 throw error(
"expected ')' after bitvector literal");
475 throw error() <<
"unknown indexed identifier " <<
buffer;
483 while(
peek() == KEYWORD)
489 if(term.type().id() != ID_bool)
490 throw error(
"named terms must be Boolean");
496 named_term.term = term;
497 named_term.name = symbol_expr;
500 throw error(
"invalid name attribute, expected symbol");
503 throw error(
"unknown term attribute");
507 throw error(
"expected ')' at end of term attribute");
518 else if(
id==ID_forall ||
id==ID_exists)
531 return unary(
id, op);
533 else if(
id==ID_equal ||
573 else if(
id==
"bvashr")
577 else if(
id==
"bvlshr" ||
id==
"bvshr")
579 return binary(ID_lshr, op);
581 else if(
id==
"bvlshr" ||
id==
"bvashl" ||
id==
"bvshl")
583 return binary(ID_shl, op);
589 else if(
id==
"bvnand")
605 else if(
id==
"bvxnor")
611 return unary(ID_bitnot, op);
615 return unary(ID_unary_minus, op);
625 else if(
id==
"bvsub" ||
id==
"-")
627 return binary(ID_minus, op);
629 else if(
id==
"bvmul" ||
id==
"*")
631 return binary(ID_mult, op);
633 else if(
id==
"bvsdiv")
637 else if(
id==
"bvudiv")
639 return binary(ID_div, op);
641 else if(
id==
"/" ||
id==
"div")
643 return binary(ID_div, op);
645 else if(
id==
"bvsrem")
651 else if(
id==
"bvsmod")
657 else if(
id==
"bvurem" ||
id==
"%")
659 return binary(ID_mod, op);
661 else if(
id==
"concat")
668 const std::size_t total_width =
669 std::accumulate(op_width.begin(), op_width.end(), 0);
675 else if(
id==
"distinct")
683 throw error(
"ite takes three operands");
685 if(op[0].type().id()!=ID_bool)
686 throw error(
"ite takes a boolean as first operand");
688 if(op[1].type()!=op[2].type())
689 throw error(
"ite needs matching types");
691 return if_exprt(op[0], op[1], op[2]);
693 else if(
id==
"=>" ||
id==
"implies")
695 return binary(ID_implies, op);
697 else if(
id ==
"select")
701 throw error(
"select takes two operands");
703 if(op[0].type().id() != ID_array)
704 throw error(
"select expects array operand");
708 else if(
id ==
"store")
712 throw error(
"store takes three operands");
714 if(op[0].type().id() != ID_array)
715 throw error(
"store expects array operand");
718 throw error(
"store expects value that matches array element type");
722 else if(
id ==
"fp.isNaN")
725 throw error(
"fp.isNaN takes one operand");
727 if(op[0].type().id() != ID_floatbv)
728 throw error(
"fp.isNaN takes FloatingPoint operand");
732 else if(
id ==
"fp.isInf")
735 throw error(
"fp.isInf takes one operand");
737 if(op[0].type().id() != ID_floatbv)
738 throw error(
"fp.isInf takes FloatingPoint operand");
747 id ==
"fp.add" ||
id ==
"fp.mul" ||
id ==
"fp.sub" ||
id ==
"fp.div")
755 auto id_it=
id_map.find(final_id);
758 if(id_it->second.type.id()==ID_mathematical_function)
770 throw error() <<
"unknown function symbol `" <<
id <<
'\'';
783 throw error(
"expected symbol after '_'");
790 throw error(
"expected numeral after extract");
792 auto upper=std::stoll(
buffer);
795 throw error(
"expected two numerals after extract");
797 auto lower=std::stoll(
buffer);
800 throw error(
"expected ')' after extract");
805 throw error(
"extract takes one operand");
811 throw error(
"extract got bad indices");
817 else if(
id==
"rotate_left" ||
818 id==
"rotate_right" ||
824 throw error() <<
"expected numeral after " << id;
826 auto index=std::stoll(
buffer);
829 throw error() <<
"expected ')' after " <<
id <<
" index";
834 throw error() <<
id <<
" takes one operand";
836 if(
id==
"rotate_left")
841 else if(
id==
"rotate_right")
846 else if(
id==
"sign_extend")
860 else if(
id==
"zero_extend")
867 else if(
id == ID_repeat)
876 throw error() <<
"unknown indexed identifier `" <<
buffer <<
'\'';
885 throw error(
"mismatched parentheses in an expression");
896 throw error(
"mismatched parentheses in an expression");
906 throw error(
"mismatched parentheses in an expression");
921 if(identifier==ID_true)
923 else if(identifier==ID_false)
925 else if(identifier ==
"roundNearestTiesToEven")
930 else if(identifier ==
"roundNearestTiesToAway")
932 throw error(
"unsupported rounding mode");
934 else if(identifier ==
"roundTowardPositive")
940 else if(identifier ==
"roundTowardNegative")
946 else if(identifier ==
"roundTowardZero")
955 auto id_it=
id_map.find(final_id);
960 symbol_expr.
set(ID_C_quoted,
true);
961 return std::move(symbol_expr);
964 throw error() <<
"unknown expression `" << identifier <<
'\'';
973 const std::size_t width = 4*(
buffer.size() - 2);
982 const std::size_t width =
buffer.size() - 2;
996 throw error(
"EOF in an expression");
999 throw error(
"unexpected token in an expression");
1015 throw error() <<
"unexpected sort: `" <<
buffer <<
'\'';
1019 throw error(
"expected symbol after '(' in a sort ");
1025 throw error(
"expected symbol after '_' in a sort");
1030 throw error(
"expected numeral as bit-width");
1032 auto width=std::stoll(
buffer);
1036 throw error(
"expected ')' at end of sort");
1040 else if(
buffer ==
"FloatingPoint")
1043 throw error(
"expected numeral as bit-width");
1045 const auto width_e = std::stoll(
buffer);
1048 throw error(
"expected numeral as bit-width");
1050 const auto width_f = std::stoll(
buffer);
1054 throw error(
"expected ')' at end of sort");
1059 throw error() <<
"unexpected sort: `" <<
buffer <<
'\'';
1061 else if(
buffer ==
"Array")
1064 auto domain =
sort();
1065 auto range =
sort();
1069 throw error(
"expected ')' at end of Array sort");
1073 if(domain.id() == ID_unsignedbv)
1076 throw error(
"unsupported array sort");
1079 throw error() <<
"unexpected sort: `" <<
buffer <<
'\'';
1082 throw error() <<
"unexpected token in a sort: `" <<
buffer <<
'\'';
1090 throw error(
"expected '(' at beginning of signature");
1100 std::vector<irep_idt> parameters;
1105 throw error(
"expected '(' at beginning of parameter");
1108 throw error(
"expected symbol in parameter");
1111 parameters.push_back(
id);
1112 domain.push_back(
sort());
1115 entry.type = domain.back();
1119 throw error(
"expected ')' at end of parameter");
1133 throw error(
"expected '(' at beginning of signature");
1146 throw error(
"expected '(' at beginning of parameter");
1149 throw error(
"expected symbol in parameter");
1151 domain.push_back(
sort());
1154 throw error(
"expected ')' at end of parameter");
1166 if(c ==
"declare-const" || c ==
"declare-var")
1171 throw error() <<
"expected a symbol after `" << c <<
'\'';
1177 throw error() <<
"identifier `" <<
id <<
"' defined twice";
1179 auto &entry =
id_map[id];
1183 else if(c==
"declare-fun")
1186 throw error(
"expected a symbol after declare-fun");
1192 throw error() <<
"identifier `" <<
id <<
"' defined twice";
1194 auto &entry =
id_map[id];
1198 else if(c ==
"define-const")
1201 throw error(
"expected a symbol after define-const");
1206 throw error() <<
"identifier `" <<
id <<
"' defined twice";
1208 const auto type =
sort();
1212 if(value.type() != type)
1214 throw error() <<
"type mismatch in constant definition: expected `" 1220 auto &entry =
id_map[id];
1222 entry.definition = value;
1224 else if(c==
"define-fun")
1227 throw error(
"expected a symbol after define-fun");
1232 throw error() <<
"identifier `" <<
id <<
"' defined twice";
1238 if(signature.type.id() == ID_mathematical_function)
1241 if(body.type() != f_signature.codomain())
1243 throw error() <<
"type mismatch in function definition: expected `" 1244 <<
smt2_format(f_signature.codomain()) <<
"' but got `" 1248 else if(body.type() != signature.type)
1250 throw error() <<
"type mismatch in function definition: expected `" 1256 auto &entry =
id_map[id];
1257 entry.type = signature.type;
1258 entry.parameters = signature.parameters;
1259 entry.definition = body;
The type of an expression, extends irept.
Fixed-width bit-vector with unsigned binary interpretation.
Semantic type conversion.
A base class for expressions that are predicates, i.e., Boolean-typed, and that take exactly one argu...
const std::string & id2string(const irep_idt &d)
void skip_to_end_of_list()
This skips tokens until all bracketed expressions are closed.
Application of (mathematical) function.
const mp_integer string2integer(const std::string &n, unsigned base)
std::size_t parenthesis_level
const signedbv_typet & to_signedbv_type(const typet &type)
Cast a typet to a signedbv_typet.
renaming_mapt renaming_map
typet function_signature_declaration()
std::vector< typet > domaint
exprt quantifier_expression(irep_idt)
std::string to_string(const string_not_contains_constraintt &expr)
Used for debug printing.
irep_idt get_fresh_id(const irep_idt &)
const irep_idt & get_identifier() const
The trinary if-then-else operator.
typet & type()
Return the type of the expression.
A constant literal expression.
const mathematical_function_typet & to_mathematical_function_type(const typet &type)
Cast a typet to a mathematical_function_typet.
#define CHECK_RETURN(CONDITION)
exprt cast_bv_to_unsigned(const exprt &)
Apply typecast to unsignedbv to given expression.
class floatbv_typet to_type() const
Concatenation of bit-vector operands.
exprt::operandst operands()
const irep_idt & id() const
renaming_counterst renaming_counters
exprt binary_predicate(irep_idt, const exprt::operandst &)
An expression denoting infinity.
The Boolean constant true.
A base class for binary expressions.
exprt function_application_ieee_float_op(const irep_idt &, const exprt::operandst &)
A type for mathematical functions (do not confuse with functions/methods in code) ...
Ranges: pair of begin and end iterators, which can be initialized from containers, provide useful methods such as map, filter and concat which only manipulate iterators, and can be used with ranged-for.
Fixed-width bit-vector with two's complement interpretation.
tokent next_token() override
Generic base class for unary expressions.
std::map< irep_idt, irep_idt > renaming_mapt
bool has_prefix(const std::string &s, const std::string &prefix)
irep_idt rename_id(const irep_idt &) const
enum { NONE, END_OF_FILE, STRING_LITERAL, NUMERAL, SYMBOL, KEYWORD, OPEN, CLOSE } tokent
ranget< iteratort > make_range(iteratort begin, iteratort end)
dstringt has one field, an unsigned integer no which is an index into a static table of strings...
The Boolean constant false.
std::size_t get_width() const
std::vector< exprt > operandst
exprt multi_ary(irep_idt, const exprt::operandst &)
exprt unary(irep_idt, const exprt::operandst &)
const unsignedbv_typet & to_unsignedbv_type(const typet &type)
Cast a typet to an unsignedbv_typet.
Unbounded, signed integers (mathematical integers, not bitvectors)
typet & codomain()
Return the codomain, i.e., the set of values that the function maps to (the "target").
virtual void command(const std::string &)
mstreamt & result() const
Unbounded, signed real numbers.
exprt binary(irep_idt, const exprt::operandst &)
const array_typet & to_array_type(const typet &type)
Cast a typet to an array_typet.
Base class for all expressions.
Operator to update elements in structs and arrays.
smt2_errort error()
generate an error exception
signature_with_parameter_idst function_signature_definition()
exprt::operandst cast_bv_to_signed(const exprt::operandst &)
Apply typecast to signedbv to expressions in vector.
exprt function_application()
Expression to hold a symbol (variable)
A base class for expressions that are predicates, i.e., Boolean-typed, and that take exactly two argu...
const typet & subtype() const
Fixed-width bit-vector without numerical interpretation.
IEEE floating-point operations These have two data operands (op0 and op1) and one rounding mode (op2)...
exprt function_application_fp(const exprt::operandst &)
void set(const irep_namet &name, const irep_idt &value)
virtual tokent next_token()