1/*******************************************************************\
5Author: Daniel Kroening, kroening@kroening.com
7\*******************************************************************/
26static std::optional<constant_exprt>
54 // The minimum variable can be of the form `var_expr >= constant`, or
55 // it can be of the form `var_expr == constant` (e.g. in the case where
56 // the interval that bounds the variable is a singleton interval (set
57 // with only one element)).
78static std::optional<constant_exprt>
110 // There are two potential forms we could come across here. The first one
111 // is `!(var_expr >= constant)` - identified by the first if branch - and
112 // the second is `var_expr == constant` - identified by the second else-if
113 // branch. The second form could be met if previous simplification has
114 // identified a singleton interval - see simplify_boolean_expr.cpp.
141 // If you need special handling for a particular expression type (say,
142 // after changes to the simplifier) you need to make sure that you add
143 // an `else if` branch above, otherwise the expression will get skipped
144 // and the constraints will not propagate correctly.
159 // Qx,y.P(x,y) is the same as Qx.Qy.P(x,y)
161 new_variables.pop_back();
192 // This grows worst-case exponentially in the quantifier nesting depth.
195 // ∀b.f(b) <===> f(0)∧f(1)
201 // ∃b.f(b) <===> f(0)∨f(1)
209 const std::optional<constant_exprt>
min_i =
211 const std::optional<constant_exprt>
max_i =
236 // maintain the domain constraint if it isn't guaranteed
237 // by the instantiations (for a disjunction the domain
238 // constraint is implied by the instantiations)
251 // maintain the domain constraint if it isn't trivially satisfied
252 // by the instantiations (for a conjunction the instantiations are
253 // stronger constraints)
272 // We first worry about the scoping of the symbols bound by the quantifier.
275 // replace in where()
278 // produce new quantifier expression
287 // we failed to instantiate here, need to pass to post-processing
298 // we do not yet have any elaborate post-processing
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.
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
Boolean AND All operands must be boolean, and the result is always boolean.
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.
const irep_idt & id() const
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Boolean OR All operands must be boolean, and the result is always boolean.
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.
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.