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)
A base class for binary expressions.
Base class for all expressions.
std::vector< exprt > operandst
bool has_operands() const
Return true if there is at least one operand.
bool is_true() const
Return whether the expression is a constant representing true.
bool is_false() const
Return whether the expression is a constant representing false.
typet & type()
Return the type of the expression.
The Boolean constant false.
const irep_idt & id() const
static resultt changed(resultt<> result)
resultt simplify_boolean(const exprt &)
resultt simplify_not(const not_exprt &)
static resultt unchanged(exprt expr)
The Boolean constant true.
#define Forall_operands(it, expr)
constant_exprt make_boolean_expr(bool value)
returns true_exprt if given true and false_exprt otherwise
Deprecated expression utility functions.
bool is_false(const literalt &l)
bool is_true(const literalt &l)
API to expression classes for 'mathematical' expressions.
const exists_exprt & to_exists_expr(const exprt &expr)
const forall_exprt & to_forall_expr(const exprt &expr)
API to expression classes.
const not_exprt & to_not_expr(const exprt &expr)
Cast an exprt to an not_exprt.
const implies_exprt & to_implies_expr(const exprt &expr)
Cast an exprt to a implies_exprt.