74 if(g1.
id()!=ID_and || g2.
id()!=ID_and)
84 exprt::operandst::iterator it1=op1.begin();
85 for(exprt::operandst::const_iterator
90 while(it1!=op1.end() && *it1<*it2)
92 if(it1!=op1.end() && *it1==*it2)
111 if(g1.
id()!=ID_and || g2.
id()!=ID_and)
134 n_op1.reserve(op1.size());
135 n_op2.reserve(op2.size());
137 exprt::operandst::iterator it1=op1.begin();
138 for(exprt::operandst::const_iterator
143 while(it1!=op1.end() && *it1<*it2)
145 n_op1.push_back(*it1);
148 if(it1!=op1.end() && *it1==*it2)
151 n_op2.push_back(*it2);
153 while(it1!=op1.end())
155 n_op1.push_back(*it1);
void guard_expr(exprt &dest) const
Deprecated expression utility functions.
bool is_false() const
Return whether the expression is a constant representing false.
guardt & operator -=(guardt &g1, const guardt &g2)
guardt & operator|=(guardt &g1, const guardt &g2)
bool is_true() const
Return whether the expression is a constant representing true.
typet & type()
Return the type of the expression.
exprt conjunction(const exprt::operandst &op)
1) generates a conjunction for two or more operands 2) for one operand, returns the operand 3) return...
const irep_idt & id() const
The Boolean constant true.
API to expression classes.
#define PRECONDITION(CONDITION)
std::vector< exprt > operandst
Base class for all expressions.
static bool sort_and_join(const struct saj_tablet &saj_entry, const irep_idt &type_id)
exprt boolean_negate(const exprt &src)
negate a Boolean expression, possibly removing a not_exprt, and swapping false and true
void add_to_operands(const exprt &expr)
Add the given argument to the end of exprt's operands.
void add(const exprt &expr)