11 #include <unordered_set>
22 if(expr.
type().
id()!=ID_bool)
25 if(expr.
id()==ID_implies)
30 implies_expr.op0().type().id() != ID_bool ||
31 implies_expr.op1().type().id() != ID_bool)
43 else if(expr.
id()==ID_xor)
45 bool no_change =
true;
50 for(exprt::operandst::const_iterator it = new_operands.begin();
51 it != new_operands.end();)
53 if(it->type().id()!=ID_bool)
68 it = new_operands.erase(it);
75 if(new_operands.empty())
79 else if(new_operands.size() == 1)
84 return std::move(new_operands.front());
90 tmp.
operands() = std::move(new_operands);
91 return std::move(tmp);
94 else if(expr.
id()==ID_and || expr.
id()==ID_or)
96 std::unordered_set<exprt, irep_hash> expr_set;
98 bool no_change =
true;
102 for(exprt::operandst::const_iterator it = new_operands.begin();
103 it != new_operands.end();)
105 if(it->type().id()!=ID_bool)
122 !expr_set.insert(*it).second;
126 it = new_operands.erase(it);
134 for(
const exprt &op : new_operands)
136 op.id() == ID_not && op.type().id() == ID_bool &&
137 expr_set.find(
to_not_expr(op).op()) != expr_set.end())
142 if(new_operands.empty())
146 else if(new_operands.size() == 1)
148 return std::move(new_operands.front());
154 tmp.
operands() = std::move(new_operands);
155 return std::move(tmp);
166 if(expr.
type().
id()!=ID_bool ||
184 else if(op.
id()==ID_and ||
194 tmp.
id(tmp.
id() == ID_and ? ID_or : ID_and);
196 return std::move(tmp);
198 else if(op.
id()==ID_notequal)
202 return std::move(tmp);
204 else if(op.
id()==ID_exists)
210 else if(op.
id() == ID_forall)