12 #ifndef CPROVER_ANALYSES_GUARD_EXPR_H
13 #define CPROVER_ANALYSES_GUARD_EXPR_H
Base class for all expressions.
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.
void add(const exprt &expr)
void append(const guard_exprt &guard)
guard_exprt & operator=(const guard_exprt &other)
bool disjunction_may_simplify(const guard_exprt &other_guard)
Returns true if operator|= with other_guard may result in a simpler expression.
guard_exprt(const exprt &e, guard_expr_managert &)
Construct a BDD from an expression The guard_managert parameter is not used, but we keep it for unifo...
friend guard_exprt & operator-=(guard_exprt &g1, const guard_exprt &g2)
friend guard_exprt & operator|=(guard_exprt &g1, const guard_exprt &g2)
exprt guard_expr(exprt expr) const
Return guard => dest or a simplified variant thereof if either guard or dest are trivial.
static constexpr bool is_always_simplified
The result of as_expr is not always in a simplified form and may requires some simplification.
Deprecated expression utility functions.
API to expression classes.
This is unused by this implementation of guards, but can be used by other implementations of the same...