26static std::optional<constant_exprt>
29 if(quantifier_expr.
id()==ID_or)
35 for(
auto &x : quantifier_expr.
operands())
43 if(
expr_eq(var_expr, y_binary.lhs()) && y_binary.rhs().is_constant())
49 if(var_expr.
type().
id() == ID_unsignedbv)
52 else if(quantifier_expr.
id() == ID_and)
58 for(
auto &x : quantifier_expr.
operands())
60 if(x.id() != ID_ge && x.id() != ID_equal)
63 if(
expr_eq(var_expr, x_binary.lhs()) && x_binary.rhs().is_constant())
69 if(var_expr.
type().
id() == ID_unsignedbv)
78static std::optional<constant_exprt>
81 if(quantifier_expr.
id()==ID_or)
87 for(
auto &x : quantifier_expr.
operands())
92 if(
expr_eq(var_expr, x_binary.lhs()) && x_binary.rhs().is_constant())
115 for(
auto &x : quantifier_expr.
operands())
123 if(
expr_eq(var_expr, y_binary.lhs()) && y_binary.rhs().is_constant())
131 else if(x.id() == ID_equal)
134 if(
expr_eq(var_expr, y_binary.lhs()) && y_binary.rhs().is_constant())
161 new_variables.pop_back();
180 (var_expr.
type().
id() == ID_integer ||
181 var_expr.
type().
id() == ID_rational || var_expr.
type().
id() == ID_real ||
182 var_expr.
type().
id() == ID_bool ||
186 return where_simplified;
193 if(expr.
id() == ID_forall)
199 else if(expr.
id() == ID_exists)
209 const std::optional<constant_exprt> min_i =
211 const std::optional<constant_exprt> max_i =
214 if(!min_i.has_value() || !max_i.has_value())
223 auto expr_simplified =
226 std::vector<exprt> expr_insts;
229 exprt constraint_expr =
231 expr_insts.push_back(constraint_expr);
234 if(expr.
id() == ID_forall)
239 if(where_simplified.
id() == ID_and)
249 else if(expr.
id() == ID_exists)
254 if(where_simplified.
id() == ID_or)
276 auto where_replaced = src.
instantiate(fresh_symbols);
Pre-defined bitvector types.
const bitvector_typet & to_bitvector_type(const typet &type)
Cast a typet to a bitvector_typet.
static bool expr_eq(const exprt &expr1, const exprt &expr2)
A method to detect equivalence between experts that can contain typecast.
static std::optional< 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.
static std::optional< exprt > eager_quantifier_instantiation(const quantifier_exprt &expr, const namespacet &ns)
static std::optional< 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.
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
void finish_eager_conversion_quantifiers()
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
A constant literal expression.
Base class for all expressions.
bool is_true() const
Return whether the expression is a constant representing true.
bool is_boolean() const
Return whether the expression represents a Boolean.
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)
A base class for quantifier expressions.
Expression to hold a symbol (variable)
bool can_cast_type(const typet &base)
Check whether a reference to a generic typet is of a specific derived class.
const exprt & skip_typecast(const exprt &expr)
find the expression nested inside typecasts, if any
Deprecated expression utility functions.
exprt simplify_expr(exprt src, const namespacet &ns)
#define UNREACHABLE
This should be used to mark dead code.
#define PRECONDITION(CONDITION)
exprt disjunction(const exprt::operandst &op)
1) generates a disjunction for two or more operands 2) for one operand, returns the operand 3) return...
exprt conjunction(exprt a, exprt b)
Conjunction of two expressions.
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.
const not_exprt & to_not_expr(const exprt &expr)
Cast an exprt to an not_exprt.