Go to the documentation of this file.
52 else if(this->expr.
id() != ID_and)
78 exprt::operandst::iterator it1 = op1.begin();
79 for(exprt::operandst::const_iterator it2 = op2.begin(); it2 != op2.end();
82 while(it1 != op1.end() && *it1 < *it2)
84 if(it1 != op1.end() && *it1 == *it2)
97 if(
expr.
id() == ID_and && other_guard.
expr.
id() == ID_and)
137 n_op1.reserve(op1.size());
138 n_op2.reserve(op2.size());
140 exprt::operandst::iterator it1 = op1.begin();
141 for(exprt::operandst::const_iterator it2 = op2.begin(); it2 != op2.end();
144 while(it1 != op1.end() && *it1 < *it2)
146 n_op1.push_back(*it1);
147 it1 = op1.erase(it1);
149 if(it1 != op1.end() && *it1 == *it2)
152 n_op2.push_back(*it2);
154 while(it1 != op1.end())
156 n_op1.push_back(*it1);
157 it1 = op1.erase(it1);
guard_exprt & operator|=(guard_exprt &g1, const guard_exprt &g2)
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 guard_expr(exprt expr) const
Return guard => dest or a simplified variant thereof if either guard or dest are trivial.
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.
void add(const exprt &expr)
#define PRECONDITION(CONDITION)
exprt boolean_negate(const exprt &src)
negate a Boolean expression, possibly removing a not_exprt, and swapping false and true
guard_exprt & operator-=(guard_exprt &g1, const guard_exprt &g2)
bool disjunction_may_simplify(const guard_exprt &other_guard)
Returns true if operator|= with other_guard may result in a simpler expression.
const irep_idt & id() const
std::vector< exprt > operandst
static bool sort_and_join(const struct saj_tablet &saj_entry, const irep_idt &type_id)
The Boolean constant true.
API to expression classes.