70 if(
g1.expr ==
g2.expr)
75 for(
const auto &op :
g2.expr.operands())
91 for(exprt::operandst::iterator it = op1.begin(); it != op1.end(); ++it)
93 if(
g1.expr ==
g2.expr)
108 exprt::operandst::iterator
it1 = op1.begin();
109 for(exprt::operandst::const_iterator
it2 = op2.begin();
it2 != op2.end();
136 if(
g2.is_false() ||
g1.is_true())
138 if(
g1.is_false() ||
g2.is_true())
148 if(
tmp ==
g1.as_expr())
165 n_op1.reserve(op1.size());
166 n_op2.reserve(op2.size());
168 exprt::operandst::iterator
it1 = op1.begin();
169 for(exprt::operandst::const_iterator
it2 = op2.begin();
it2 != op2.end();
182 while(
it1 != op1.end())
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
Base class for all expressions.
std::vector< exprt > operandst
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.
void add(const exprt &expr)
bool disjunction_may_simplify(const guard_exprt &other_guard)
Returns true if operator|= with other_guard may result in a simpler expression.
exprt guard_expr(exprt expr) const
Return guard => dest or a simplified variant thereof if either guard or dest are trivial.
const irep_idt & id() const
The Boolean constant true.
exprt boolean_negate(const exprt &src)
negate a Boolean expression, possibly removing a not_exprt, and swapping false and true
Deprecated expression utility functions.
guard_exprt & operator|=(guard_exprt &g1, const guard_exprt &g2)
guard_exprt & operator-=(guard_exprt &g1, const guard_exprt &g2)
#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...
API to expression classes.