12 #include <unordered_set> 25 if(expr.
type().
id()!=ID_bool)
28 if(expr.
id()==ID_implies)
30 if(operands.size()!=2 ||
31 operands.front().type().id()!=ID_bool ||
32 operands.back().type().id()!=ID_bool)
43 else if(expr.
id()==ID_iff)
45 if(operands.size()!=2 ||
46 operands.front().type().id()!=ID_bool ||
47 operands.back().type().id()!=ID_bool)
50 if(operands.front().is_false())
53 operands.erase(operands.begin());
56 else if(operands.front().is_true())
58 exprt tmp(operands.back());
62 else if(operands.back().is_false())
65 operands.erase(++operands.begin());
68 else if(operands.back().is_true())
70 exprt tmp(operands.front());
75 else if(expr.
id()==ID_xor)
81 for(exprt::operandst::const_iterator it=operands.begin();
84 if(it->type().id()!=ID_bool)
99 it=operands.erase(it);
111 else if(operands.size()==1)
113 exprt tmp(operands.front());
122 else if(expr.
id()==ID_and || expr.
id()==ID_or)
124 std::unordered_set<exprt, irep_hash> expr_set;
128 for(exprt::operandst::const_iterator it=operands.begin();
131 if(it->type().id()!=ID_bool)
150 !expr_set.insert(*it).second;
154 it=operands.erase(it);
162 for(
const exprt &op : operands)
163 if(op.id()==ID_not &&
164 op.operands().size()==1 &&
165 op.type().id()==ID_bool &&
166 expr_set.find(op.op0())!=expr_set.end())
177 else if(operands.size()==1)
179 exprt tmp(operands.front());
197 if(expr.
type().
id()!=ID_bool ||
221 else if(op.
id()==ID_and ||
234 expr.
id(expr.
id()==ID_and?ID_or:ID_and);
238 else if(op.
id()==ID_notequal)
246 else if(op.
id()==ID_exists)
bool is_true(const literalt &l)
bool simplify_node(exprt &expr)
void make_bool(bool 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
The boolean constant false.
std::vector< exprt > operandst
Base class for all expressions.
#define Forall_operands(it, expr)
bool simplify_not(exprt &expr)