31 if(quantifier_expr.
id()==ID_or)
37 for(
auto &x : quantifier_expr.
operands())
46 expr_eq(var_expr, y_binary.lhs()) && y_binary.rhs().id() == ID_constant)
52 else if(quantifier_expr.
id() == ID_and)
58 for(
auto &x : quantifier_expr.
operands())
64 expr_eq(var_expr, x_binary.lhs()) && x_binary.rhs().id() == ID_constant)
79 if(quantifier_expr.
id()==ID_or)
85 for(
auto &x : quantifier_expr.
operands())
91 expr_eq(var_expr, x_binary.lhs()) && x_binary.rhs().id() == ID_constant)
95 mp_integer over_i = numeric_cast_v<mp_integer>(over_expr);
113 for(
auto &x : quantifier_expr.
operands())
122 expr_eq(var_expr, y_binary.lhs()) && y_binary.rhs().id() == ID_constant)
125 mp_integer over_i = numeric_cast_v<mp_integer>(over_expr);
155 if(!min_i.has_value() || !max_i.has_value())
158 mp_integer lb = numeric_cast_v<mp_integer>(min_i.value());
159 mp_integer ub = numeric_cast_v<mp_integer>(max_i.value());
164 std::vector<exprt> expr_insts;
167 exprt constraint_expr = re;
171 expr_insts.push_back(constraint_expr);
174 if(expr.
id()==ID_forall)
179 if(re.
id() == ID_and)
188 else if(expr.
id() == ID_exists)
214 auto where_replaced = src.
instantiate(fresh_symbols);
static bool expr_eq(const exprt &expr1, const exprt &expr2)
A method to detect equivalence between experts that can contain typecast.
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.
static optionalt< exprt > instantiate_quantifier(const quantifier_exprt &expr, const namespacet &ns)
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.
A base class for expressions that are predicates, i.e., Boolean-typed, and that take exactly two argu...
exprt instantiate(const exprt::operandst &) const
substitute free occurrences of the variables in where() by the given values
binding_exprt::variablest fresh_binding(const binding_exprt &)
create new, unique variables for the given binding
virtual literalt convert_quantifier(const quantifier_exprt &expr)
bvt conversion_failed(const exprt &expr)
Print that the expression of x has failed conversion, then return a vector of x's width.
quantifier_listt quantifier_list
void post_process_quantifiers()
A constant literal expression.
Base class for all expressions.
bool is_true() const
Return whether the expression is a constant representing true.
bool is_false() const
Return whether the expression is a constant representing false.
typet & type()
Return the type of the expression.
const irep_idt & id() const
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
virtual literalt convert_bool(const exprt &expr)
virtual literalt new_variable()=0
A base class for quantifier expressions.
Expression to hold a symbol (variable)
const exprt & skip_typecast(const exprt &expr)
find the expression nested inside typecasts, if any
Deprecated expression utility functions.
nonstd::optional< T > optionalt
Ranges: pair of begin and end iterators, which can be initialized from containers,...
bool replace_expr(const exprt &what, const exprt &by, exprt &dest)
exprt simplify_expr(exprt src, const namespacet &ns)
#define UNREACHABLE
This should be used to mark dead code.
#define PRECONDITION(CONDITION)
exprt conjunction(const exprt::operandst &op)
1) generates a conjunction for two or more operands 2) for one operand, returns the operand 3) return...
exprt disjunction(const exprt::operandst &op)
1) generates a disjunction for two or more operands 2) for one operand, returns the operand 3) return...
const constant_exprt & to_constant_expr(const exprt &expr)
Cast an exprt to a constant_exprt.
const not_exprt & to_not_expr(const exprt &expr)
Cast an exprt to an not_exprt.
const binary_relation_exprt & to_binary_relation_expr(const exprt &expr)
Cast an exprt to a binary_relation_exprt.