11 #include <unordered_set>
25 if(expr.
type().
id()!=ID_bool)
28 if(expr.
id()==ID_implies)
33 implies_expr.op0().type().id() != ID_bool ||
34 implies_expr.op1().type().id() != ID_bool)
46 else if(expr.
id()==ID_xor)
48 bool no_change =
true;
53 for(exprt::operandst::const_iterator it = new_operands.begin();
54 it != new_operands.end();)
56 if(it->type().id()!=ID_bool)
71 it = new_operands.erase(it);
78 if(new_operands.empty())
82 else if(new_operands.size() == 1)
87 return std::move(new_operands.front());
93 tmp.
operands() = std::move(new_operands);
94 return std::move(tmp);
97 else if(expr.
id()==ID_and || expr.
id()==ID_or)
99 std::unordered_set<exprt, irep_hash> expr_set;
101 bool no_change =
true;
105 for(exprt::operandst::const_iterator it = new_operands.begin();
106 it != new_operands.end();)
108 if(it->type().id()!=ID_bool)
125 !expr_set.insert(*it).second;
129 it = new_operands.erase(it);
137 for(
const exprt &op : new_operands)
139 op.id() == ID_not && op.type().id() == ID_bool &&
140 expr_set.find(
to_not_expr(op).op()) != expr_set.end())
145 if(new_operands.empty())
149 else if(new_operands.size() == 1)
151 return std::move(new_operands.front());
157 tmp.
operands() = std::move(new_operands);
158 return std::move(tmp);
169 if(expr.
type().
id()!=ID_bool ||
187 else if(op.
id()==ID_and ||
197 tmp.
id(tmp.
id() == ID_and ? ID_or : ID_and);
199 return std::move(tmp);
201 else if(op.
id()==ID_notequal)
205 return std::move(tmp);
207 else if(op.
id()==ID_exists)
211 op_as_exists.symbol(),
not_exprt(op_as_exists.where()));
213 return std::move(rewritten_op);
215 else if(op.
id() == ID_forall)
219 op_as_forall.symbol(),
not_exprt(op_as_forall.where()));
221 return std::move(rewritten_op);