21 error() <<
"expected symbol as command" <<
eom;
33 error() <<
"expected closing parenthesis at end of command," 34 " but got EOF" <<
eom;
42 error() <<
"expected end of command" <<
eom;
47 if(
token!=END_OF_FILE)
49 error() <<
"unexpected token in command sequence" <<
eom;
55 std::size_t parentheses=0;
74 error() <<
"unexpected EOF in command" <<
eom;
96 if(
id_map[
id].type.is_nil())
128 error() <<
"expected bindings after let" <<
eom;
132 std::vector<std::pair<irep_idt, exprt>> bindings;
140 error() <<
"expected symbol in binding" <<
eom;
151 error() <<
"expected ')' after value in binding" <<
eom;
156 std::pair<irep_idt, exprt>(identifier, value));
161 error() <<
"expected ')' at end of bindings" <<
eom;
169 for(
auto &b : bindings)
173 auto &entry=
id_map[b.first];
174 entry.type=b.second.type();
175 entry.definition=b.second;
182 error() <<
"expected ')' after let" <<
eom;
189 for(
auto r_it=bindings.rbegin(); r_it!=bindings.rend(); r_it++)
193 let.
value()=r_it->second;
200 for(
const auto &b : bindings)
213 error() <<
"expected bindings after " <<
id <<
eom;
217 std::vector<symbol_exprt> bindings;
225 error() <<
"expected symbol in binding" <<
eom;
235 error() <<
"expected ')' after sort in binding" <<
eom;
244 error() <<
"expected ')' at end of bindings" <<
eom;
249 for(
const auto &b : bindings)
251 auto &entry=
id_map[b.get_identifier()];
260 error() <<
"expected ')' after " <<
id <<
eom;
267 for(
const auto &b : bindings)
268 id_map.erase(b.get_identifier());
271 for(
auto r_it=bindings.rbegin(); r_it!=bindings.rend(); r_it++)
274 quantifier.
op0()=*r_it;
287 const auto &f =
id_map[identifier];
295 if(op.size()!=f.type.variables().size())
297 error() <<
"wrong number of arguments for function" <<
eom;
301 for(std::size_t i=0; i<op.size(); i++)
303 if(op[i].type() != f.type.variables()[i].type())
305 error() <<
"wrong type for arguments for function" <<
eom;
310 result.type()=f.type.range();
322 if(expr.type().id() == ID_signedbv)
325 else if(expr.type().id() != ID_unsignedbv)
327 error() <<
"expected unsigned bitvector" <<
eom;
341 if(expr.
type().
id()==ID_unsignedbv)
344 if(expr.
type().
id()!=ID_signedbv)
346 error() <<
"expected signed bitvector" <<
eom;
358 error() <<
"expression must have at least one operand" <<
eom;
363 for(std::size_t i=1; i<op.size(); i++)
365 if(op[i].type()!=op[0].type())
367 error() <<
"expression must have operands with matching types," 369 << op[0].type().pretty()
370 <<
"' and `" << op[i].type().pretty() <<
'\'' <<
eom;
385 error() <<
"expression must have two operands" <<
eom;
390 if(op[0].type()!=op[1].type())
392 error() <<
"expression must have operands with matching types," 394 << op[0].type().pretty()
395 <<
"' and `" << op[1].type().pretty() <<
'\'' <<
eom;
407 error() <<
"expression must have one operand" <<
eom;
418 error() <<
"expression must have two operands" <<
eom;
423 if(op[0].type()!=op[1].type())
425 error() <<
"expression must have operands with matching types" <<
eom;
443 error() <<
"expected symbol after '_'" <<
eom;
453 error() <<
"expected numeral as bitvector literal width" <<
eom;
457 auto width=std::stoll(
buffer);
461 error() <<
"expected ')' after bitvector literal" <<
eom;
480 else if(
id==ID_forall ||
id==ID_exists)
493 return unary(
id, op);
495 else if(
id==ID_equal ||
535 else if(
id==
"bvashr")
539 else if(
id==
"bvlshr" ||
id==
"bvshr")
541 return binary(ID_lshr, op);
543 else if(
id==
"bvlshr" ||
id==
"bvashl" ||
id==
"bvshl")
545 return binary(ID_shl, op);
551 else if(
id==
"bvnand")
567 else if(
id==
"bvxnor")
573 return unary(ID_bitnot, op);
577 return unary(ID_unary_minus, op);
587 else if(
id==
"bvsub" ||
id==
"-")
589 return binary(ID_minus, op);
591 else if(
id==
"bvmul" ||
id==
"*")
593 return binary(ID_mult, op);
595 else if(
id==
"bvsdiv")
599 else if(
id==
"bvudiv")
601 return binary(ID_div, op);
603 else if(
id==
"/" ||
id==
"div")
605 return binary(ID_div, op);
607 else if(
id==
"bvsrem")
613 else if(
id==
"bvsmod")
619 else if(
id==
"bvurem" ||
id==
"%")
621 return binary(ID_mod, op);
623 else if(
id==
"concat")
627 error() <<
"concat takes two operands " << op.size() <<
eom;
638 else if(
id==
"distinct")
647 error() <<
"ite takes three operands" <<
eom;
651 if(op[0].type().
id()!=ID_bool)
653 error() <<
"ite takes a boolean as first operand" <<
eom;
657 if(op[1].type()!=op[2].type())
659 error() <<
"ite needs matching types" <<
eom;
663 return if_exprt(op[0], op[1], op[2]);
665 else if(
id==
"=>" ||
id==
"implies")
667 return binary(ID_implies, op);
673 auto id_it=
id_map.find(final_id);
676 if(id_it->second.type.id()==ID_mathematical_function)
689 error() <<
"2 unknown symbol " <<
id <<
eom;
704 error() <<
"expected symbol after '_'" <<
eom;
714 error() <<
"expected numeral after extract" <<
eom;
718 auto upper=std::stoll(
buffer);
722 error() <<
"expected two numerals after extract" <<
eom;
726 auto lower=std::stoll(
buffer);
730 error() <<
"expected ')' after extract" <<
eom;
738 error() <<
"extract takes one operand" <<
eom;
747 error() <<
"extract got bad indices" <<
eom;
755 else if(
id==
"rotate_left" ||
756 id==
"rotate_right" ||
763 error() <<
"expected numeral after " <<
id <<
eom;
767 auto index=std::stoll(
buffer);
771 error() <<
"expected ')' after " <<
id <<
" index" <<
eom;
779 error() <<
id <<
" takes one operand" <<
eom;
783 if(
id==
"rotate_left")
788 else if(
id==
"rotate_right")
793 else if(
id==
"sign_extend")
802 else if(
id==
"zero_extend")
809 else if(
id == ID_repeat)
825 error() <<
"expected symbol or indexed identifier " 826 "after '(' in an expression" <<
eom;
831 error() <<
"mismatched parentheses in an expression" <<
eom;
839 error() <<
"expected symbol or indexed identifier " 840 "after '(' in an expression" <<
eom;
845 error() <<
"mismatched parentheses in an expression" <<
eom;
853 error() <<
"expected symbol or indexed identifier " 854 "after '(' in an expression" <<
eom;
858 error() <<
"mismatched parentheses in an expression" <<
eom;
873 if(identifier==ID_true)
875 else if(identifier==ID_false)
881 auto id_it=
id_map.find(final_id);
885 error() <<
"1 unknown symbol " << identifier <<
eom;
895 const std::size_t width = 4*(
buffer.size() - 2);
904 const std::size_t width =
buffer.size() - 2;
918 error() <<
"EOF in an expression" <<
eom;
922 error() <<
"unexpected token in an expression" <<
eom;
947 error() <<
"expected symbol after '(' in a sort " <<
eom;
956 error() <<
"expected symbol after '_' in a sort" <<
eom;
964 error() <<
"expected numeral as bit-width" <<
eom;
968 auto width=std::stoll(
buffer);
973 error() <<
"expected ')' at end of sort" <<
eom;
1001 error() <<
"expected '(' at beginning of signature" <<
eom;
1017 error() <<
"expected '(' at beginning of parameter" <<
eom;
1023 error() <<
"expected symbol in parameter" <<
eom;
1031 domain.push_back(var);
1034 entry.type=var.
type();
1039 error() <<
"expected ')' at end of parameter" <<
eom;
1055 error() <<
"expected '(' at beginning of signature" <<
eom;
1071 error() <<
"expected '(' at beginning of parameter" <<
eom;
1077 error() <<
"expected symbol in parameter" <<
eom;
1083 domain.push_back(var);
1087 error() <<
"expected ')' at end of parameter" <<
eom;
1101 if(c==
"declare-const")
1105 error() <<
"expected a symbol after declare-const" <<
eom;
1114 error() <<
"identifier `" <<
id <<
"' defined twice" <<
eom;
1123 else if(c==
"declare-fun")
1127 error() <<
"expected a symbol after declare-fun" <<
eom;
1136 error() <<
"identifier `" <<
id <<
"' defined twice" <<
eom;
1145 else if(c==
"define-fun")
1149 error() <<
"expected a symbol after define-fun" <<
eom;
1158 error() <<
"identifier `" <<
id <<
"' defined twice" <<
eom;
1171 entry.type=signature;
1172 entry.definition=body;
The type of an expression.
Fixed-width bit-vector with unsigned binary interpretation.
const std::string & id2string(const irep_idt &d)
application of (mathematical) function
const mp_integer string2integer(const std::string &n, unsigned base)
const signedbv_typet & to_signedbv_type(const typet &type)
Cast a generic typet to a signedbv_typet.
renaming_mapt renaming_map
typet function_signature_declaration()
exprt quantifier_expression(irep_idt)
irep_idt get_fresh_id(const irep_idt &)
std::vector< variablet > domaint
The trinary if-then-else operator.
A constant literal expression.
#define CHECK_RETURN(CONDITION)
static mstreamt & eom(mstreamt &m)
exprt cast_bv_to_unsigned(const exprt &)
Apply typecast to unsignedbv to given expression.
exprt::operandst operands()
const irep_idt & id() const
renaming_counterst renaming_counters
exprt binary_predicate(irep_idt, const exprt::operandst &)
The boolean constant true.
A generic base class for binary expressions.
A type for mathematical functions (do not confuse with functions/methods in code) ...
Fixed-width bit-vector with two's complement interpretation.
void set_identifier(const irep_idt &identifier)
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
dstringt has one field, an unsigned integer no which is an index into a static table of strings...
typet function_signature_definition()
The boolean constant false.
std::size_t get_width() const
symbol_exprt & function()
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 generic typet to an unsignedbv_typet.
Unbounded, signed integers.
virtual void command(const std::string &)
mstreamt & result() const
Unbounded, signed real numbers.
exprt binary(irep_idt, const exprt::operandst &)
Base class for all expressions.
std::string to_string(const string_constraintt &expr)
Used for debug printing.
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 generic base class for expressions that are predicates, i.e., boolean-typed, and that take exactly ...
const mathematical_function_typet & to_mathematical_function_type(const typet &type)
Cast a generic typet to a mathematical_function_typet.