11 #include <unordered_set> 26 if(expr.
type().
id()!=ID_bool)
29 if(expr.
id()==ID_implies)
31 if(operands.size()!=2 ||
32 operands.front().type().id()!=ID_bool ||
33 operands.back().type().id()!=ID_bool)
44 else if(expr.
id()==ID_xor)
50 for(exprt::operandst::const_iterator it=operands.begin();
53 if(it->type().id()!=ID_bool)
68 it=operands.erase(it);
80 else if(operands.size()==1)
82 exprt tmp(operands.front());
91 else if(expr.
id()==ID_and || expr.
id()==ID_or)
93 std::unordered_set<exprt, irep_hash> expr_set;
97 for(exprt::operandst::const_iterator it=operands.begin();
100 if(it->type().id()!=ID_bool)
119 !expr_set.insert(*it).second;
123 it=operands.erase(it);
131 for(
const exprt &op : operands)
132 if(op.id()==ID_not &&
133 op.operands().size()==1 &&
134 op.type().id()==ID_bool &&
135 expr_set.find(op.op0())!=expr_set.end())
146 else if(operands.size()==1)
148 exprt tmp(operands.front());
166 if(expr.
type().
id()!=ID_bool ||
190 else if(op.
id()==ID_and ||
203 expr.
id(expr.
id()==ID_and?ID_or:ID_and);
207 else if(op.
id()==ID_notequal)
215 else if(op.
id()==ID_exists)
219 op_as_exists.symbol(),
not_exprt(op_as_exists.where()));
bool is_true(const literalt &l)
bool simplify_node(exprt &expr)
Deprecated expression utility functions.
bool is_false() const
Return whether the expression is a constant representing false.
const exists_exprt & to_exists_expr(const exprt &expr)
bool is_true() const
Return whether the expression is a constant representing true.
typet & type()
Return the type of the expression.
void make_bool(bool value)
Replace the expression by a Boolean expression representing value.
const irep_idt & id() const
bool is_false(const literalt &l)
The Boolean constant true.
bool simplify_boolean(exprt &expr)
API to expression classes.
bool has_operands() const
Return true if there is at least one operand.
The Boolean constant false.
std::vector< exprt > operandst
Base class for all expressions.
#define Forall_operands(it, expr)
bool simplify_not(exprt &expr)
exprt boolean_negate(const exprt &src)
negate a Boolean expression, possibly removing a not_exprt, and swapping false and true