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 PRECONDITION(quantifier_expr.
id() == ID_or || quantifier_expr.
id() == ID_and);
38 if(quantifier_expr.
id()==ID_or)
44 for(
auto &x : quantifier_expr.
operands())
63 for(
auto &x : quantifier_expr.
operands())
67 if(
expr_eq(var_expr, x.
op0()) && x.op1().id()==ID_constant)
79 const exprt &var_expr,
80 const exprt &quantifier_expr)
82 PRECONDITION(quantifier_expr.
id() == ID_or || quantifier_expr.
id() == ID_and);
84 if(quantifier_expr.
id()==ID_or)
90 for(
auto &x : quantifier_expr.
operands())
94 if(
expr_eq(var_expr, x.
op0()) && x.op1().id()==ID_constant)
97 mp_integer over_i = numeric_cast_v<mp_integer>(over_expr);
115 for(
auto &x : quantifier_expr.
operands())
125 mp_integer over_i = numeric_cast_v<mp_integer>(over_expr);
160 mp_integer lb = numeric_cast_v<mp_integer>(min_i);
161 mp_integer ub = numeric_cast_v<mp_integer>(max_i);
166 std::vector<exprt> expr_insts;
169 exprt constraint_expr = re;
173 expr_insts.push_back(constraint_expr);
176 if(expr.
id()==ID_forall)
180 else if(expr.
id() == ID_exists)
202 quantifier.
expr = *res;
213 std::set<exprt> instances;
exprt simplify_expr(const exprt &src, const namespacet &ns)
bool is_false() const
Return whether the expression is a constant representing false.
bool is_true() const
Return whether the expression is a constant representing true.
virtual literalt convert_bool(const exprt &expr)
typet & type()
Return the type of the expression.
virtual void set_equal(literalt a, literalt b)
asserts a==b in the propositional formula
exprt conjunction(const exprt::operandst &op)
1) generates a conjunction for two or more operands 2) for one operand, returns the operand 3) return...
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.
nonstd::optional< T > optionalt
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
#define PRECONDITION(CONDITION)
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
The Boolean constant false.
exprt disjunction(const exprt::operandst &op)
1) generates a disjunction for two or more operands 2) for one operand, returns the operand 3) return...
void post_process_quantifiers()
optionalt< exprt > instantiate_quantifier(const quantifier_exprt &expr, const namespacet &ns)
Base class for all expressions.
A base class for quantifier expressions.
#define UNREACHABLE
This should be used to mark dead code.
virtual literalt convert_rest(const exprt &expr)
Expression to hold a symbol (variable)
bool expr_eq(const exprt &expr1, const exprt &expr2)
A method to detect equivalence between experts that can contain typecast.
virtual literalt convert_quantifier(const quantifier_exprt &expr)