11#include <unordered_set>
50 for(exprt::operandst::const_iterator it =
new_operands.begin();
91 return std::move(
tmp);
96 std::unordered_set<exprt, irep_hash> expr_set;
102 for(exprt::operandst::const_iterator it =
new_operands.begin();
122 !expr_set.insert(*it).second;
137 expr_set.find(
to_not_expr(op).op()) != expr_set.end())
155 return std::move(
tmp);
196 return std::move(
tmp);
202 return std::move(
tmp);
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
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.