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