50 else if(this->expr.
id() != ID_and)
91 for(exprt::operandst::iterator it = op1.begin(); it != op1.end(); ++it)
108 exprt::operandst::iterator it1 = op1.begin();
109 for(exprt::operandst::const_iterator it2 = op2.begin(); it2 != op2.end();
112 if(it1 != op1.end() && *it1 == *it2)
113 it1 = op1.erase(it1);
127 if(
expr.
id() == ID_and && other_guard.
expr.
id() == ID_and)
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();
172 while(it1 != op1.end() && *it1 < *it2)
174 n_op1.push_back(*it1);
175 it1 = op1.erase(it1);
177 if(it1 != op1.end() && *it1 == *it2)
180 n_op2.push_back(*it2);
182 while(it1 != op1.end())
184 n_op1.push_back(*it1);
185 it1 = op1.erase(it1);
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.