20 exprt e1=expr1, e2=expr2;
21 if(expr1.
id()==ID_typecast)
23 if(expr2.
id()==ID_typecast)
32 const exprt &var_expr,
33 const exprt &quantifier_expr)
35 assert(quantifier_expr.
id()==ID_or ||
36 quantifier_expr.
id()==ID_and);
39 if(quantifier_expr.
id()==ID_or)
45 for(
auto &x : quantifier_expr.
operands())
64 for(
auto &x : quantifier_expr.
operands())
68 if(
expr_eq(var_expr, x.
op0()) && x.op1().id()==ID_constant)
80 const exprt &var_expr,
81 const exprt &quantifier_expr)
83 assert(quantifier_expr.
id()==ID_or ||
84 quantifier_expr.
id()==ID_and);
87 if(quantifier_expr.
id()==ID_or)
93 for(
auto &x : quantifier_expr.
operands())
97 if(
expr_eq(var_expr, x.
op0()) && x.op1().id()==ID_constant)
119 for(
auto &x : quantifier_expr.
operands())
143 if(!(expr.
id()==ID_forall || expr.
id()==ID_exists))
147 assert(expr.
op0().
id()==ID_symbol);
169 if(var_expr.is_false() ||
183 std::vector<exprt> expr_insts;
186 exprt constraint_expr=body_expr;
190 expr_insts.push_back(constraint_expr);
192 if(expr.
id()==ID_forall)
196 if(expr.
id()==ID_exists)
211 quantifier.
expr=expr;
222 std::set<exprt> instances;
exprt simplify_expr(const exprt &src, const namespacet &ns)
virtual literalt convert_bool(const exprt &expr)
virtual literalt convert_quantifier(const exprt &expr)
virtual void set_equal(literalt a, literalt b)
asserts a==b in the propositional formula
exprt conjunction(const exprt::operandst &op)
const irep_idt & id() const
bool replace_expr(const exprt &what, const exprt &by, exprt &dest)
virtual literalt new_variable()=0
exprt get_quantifier_var_min(const exprt &var_expr, const exprt &quantifier_expr)
To obtain the min value for the quantifier variable of the specified forall/exists operator...
exprt get_quantifier_var_max(const exprt &var_expr, const exprt &quantifier_expr)
To obtain the max value for the quantifier variable of the specified forall/exists operator...
quantifier_listt quantifier_list
exprt disjunction(const exprt::operandst &op)
void post_process_quantifiers()
Base class for all expressions.
bool instantiate_quantifier(exprt &expr, const namespacet &ns)
virtual literalt convert_rest(const exprt &expr)
bool expr_eq(const exprt &expr1, const exprt &expr2)
A method to detect equivalence between experts that can contain typecast.