Go to the documentation of this file.
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;
virtual void command(const std::string &)
Operator to update elements in structs and arrays.
exprt quantifier_expression(irep_idt)
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
irep_idt rename_id(const irep_idt &) const
renaming_counterst renaming_counters
enum { NONE, END_OF_FILE, STRING_LITERAL, NUMERAL, SYMBOL, KEYWORD, OPEN, CLOSE } tokent
The type of an expression, extends irept.
exprt function_application()
tokent next_token() override
The trinary if-then-else operator.
const mp_integer string2integer(const std::string &n, unsigned base)
Unbounded, signed integers (mathematical integers, not bitvectors)
exprt binary(irep_idt, const exprt::operandst &)
const mathematical_function_typet & to_mathematical_function_type(const typet &type)
Cast a typet to a mathematical_function_typet.
Base class for all expressions.
Generic base class for unary expressions.
A base class for binary expressions.
Concatenation of bit-vector operands.
std::string to_string(const string_not_contains_constraintt &expr)
Used for debug printing.
Expression to hold a symbol (variable)
signature_with_parameter_idst function_signature_definition()
An expression denoting infinity.
Fixed-width bit-vector with unsigned binary interpretation.
exprt multi_ary(irep_idt, const exprt::operandst &)
exprt unary(irep_idt, const exprt::operandst &)
typet & type()
Return the type of the expression.
std::size_t parenthesis_level
std::map< irep_idt, irep_idt > renaming_mapt
typet function_signature_declaration()
Unbounded, signed real numbers.
mstreamt & result() const
smt2_errort error()
generate an error exception
const unsignedbv_typet & to_unsignedbv_type(const typet &type)
Cast a typet to an unsignedbv_typet.
exprt function_application_fp(const exprt::operandst &)
const std::string & id2string(const irep_idt &d)
class floatbv_typet to_type() const
A base class for expressions that are predicates, i.e., Boolean-typed, and that take exactly two argu...
typet & codomain()
Return the codomain, i.e., the set of values that the function maps to (the "target").
exprt binary_predicate(irep_idt, const exprt::operandst &)
const irep_idt & get_identifier() const
Fixed-width bit-vector with two's complement interpretation.
exprt function_application_ieee_float_op(const irep_idt &, const exprt::operandst &)
exprt::operandst cast_bv_to_signed(const exprt::operandst &)
Apply typecast to signedbv to expressions in vector.
Application of (mathematical) function.
std::vector< typet > domaint
const irep_idt & id() const
std::vector< exprt > operandst
The Boolean constant false.
renaming_mapt renaming_map
irep_idt get_fresh_id(const irep_idt &)
std::size_t get_width() const
void set(const irep_namet &name, const irep_idt &value)
const signedbv_typet & to_signedbv_type(const typet &type)
Cast a typet to a signedbv_typet.
exprt cast_bv_to_unsigned(const exprt &)
Apply typecast to unsignedbv to given expression.
const array_typet & to_array_type(const typet &type)
Cast a typet to an array_typet.
IEEE floating-point operations These have two data operands (op0 and op1) and one rounding mode (op2)...
bool has_prefix(const std::string &s, const std::string &prefix)
virtual tokent next_token()
exprt::operandst operands()
Semantic type conversion.
The Boolean constant true.
A constant literal expression.
ranget< iteratort > make_range(iteratort begin, iteratort end)
A type for mathematical functions (do not confuse with functions/methods in code)
A base class for expressions that are predicates, i.e., Boolean-typed, and that take exactly one argu...
void skip_to_end_of_list()
This skips tokens until all bracketed expressions are closed.
Fixed-width bit-vector without numerical interpretation.
#define CHECK_RETURN(CONDITION)