12 #ifndef CPROVER_ANALYSES_GUARD_EXPR_H
13 #define CPROVER_ANALYSES_GUARD_EXPR_H
static exprt guard(const exprt::operandst &guards, exprt cond)
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.
This is unused by this implementation of guards, but can be used by other implementations of the same...