Go to the documentation of this file.
30 if(quantifier_expr.
id()==ID_or)
36 for(
auto &x : quantifier_expr.
operands())
45 expr_eq(var_expr, y_binary.lhs()) && y_binary.rhs().id() == ID_constant)
51 else if(quantifier_expr.
id() == ID_and)
57 for(
auto &x : quantifier_expr.
operands())
63 expr_eq(var_expr, x_binary.lhs()) && x_binary.rhs().id() == ID_constant)
78 if(quantifier_expr.
id()==ID_or)
84 for(
auto &x : quantifier_expr.
operands())
90 expr_eq(var_expr, x_binary.lhs()) && x_binary.rhs().id() == ID_constant)
94 mp_integer over_i = numeric_cast_v<mp_integer>(over_expr);
112 for(
auto &x : quantifier_expr.
operands())
121 expr_eq(var_expr, y_binary.lhs()) && y_binary.rhs().id() == ID_constant)
124 mp_integer over_i = numeric_cast_v<mp_integer>(over_expr);
154 if(!min_i.has_value() || !max_i.has_value())
157 mp_integer lb = numeric_cast_v<mp_integer>(min_i.value());
158 mp_integer ub = numeric_cast_v<mp_integer>(max_i.value());
163 std::vector<exprt> expr_insts;
166 exprt constraint_expr = re;
170 expr_insts.push_back(constraint_expr);
173 if(expr.
id()==ID_forall)
178 if(re.
id() == ID_and)
187 else if(expr.
id() == ID_exists)
#define UNREACHABLE
This should be used to mark dead code.
static optionalt< constant_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.
const exprt & skip_typecast(const exprt &expr)
find the expression nested inside typecasts, if any
exprt conjunction(const exprt::operandst &op)
1) generates a conjunction for two or more operands 2) for one operand, returns the operand 3) return...
void post_process_quantifiers()
virtual literalt new_variable()=0
Base class for all expressions.
A base class for quantifier expressions.
bool is_true() const
Return whether the expression is a constant representing true.
virtual literalt convert_bool(const exprt &expr)
Expression to hold a symbol (variable)
bool is_false() const
Return whether the expression is a constant representing false.
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
typet & type()
Return the type of the expression.
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 conversion_failed(const exprt &expr, bvt &bv)
A base class for expressions that are predicates, i.e., Boolean-typed, and that take exactly two argu...
#define PRECONDITION(CONDITION)
exprt simplify_expr(exprt src, const namespacet &ns)
const irep_idt & id() const
nonstd::optional< T > optionalt
quantifier_listt quantifier_list
static optionalt< constant_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.
Deprecated expression utility functions.
static optionalt< exprt > instantiate_quantifier(const quantifier_exprt &expr, const namespacet &ns)
const not_exprt & to_not_expr(const exprt &expr)
Cast an exprt to an not_exprt.
bool replace_expr(const exprt &what, const exprt &by, exprt &dest)
virtual literalt convert_quantifier(const quantifier_exprt &expr)
static bool expr_eq(const exprt &expr1, const exprt &expr2)
A method to detect equivalence between experts that can contain typecast.
A constant literal expression.
const binary_relation_exprt & to_binary_relation_expr(const exprt &expr)
Cast an exprt to a binary_relation_exprt.
const constant_exprt & to_constant_expr(const exprt &expr)
Cast an exprt to a constant_exprt.