CBMC
All Classes Namespaces Files Functions Variables Typedefs Enumerations Enumerator Friends Macros Modules Pages
guard_expr.h
Go to the documentation of this file.
1/*******************************************************************\
2
3Module: Guard Data Structure
4
5Author: Daniel Kroening, kroening@kroening.com
6
7\*******************************************************************/
8
11
12#ifndef CPROVER_ANALYSES_GUARD_EXPR_H
13#define CPROVER_ANALYSES_GUARD_EXPR_H
14
15#include <util/expr.h>
16
20{
21};
22
24{
25public:
29 explicit guard_exprt(const exprt &e, guard_expr_managert &) : expr(e)
30 {
31 }
32
34 {
35 expr = other.expr;
36 return *this;
37 }
38
39 void add(const exprt &expr);
40
42 {
43 add(guard.as_expr());
44 }
45
46 exprt as_expr() const
47 {
48 return expr;
49 }
50
54 static constexpr bool is_always_simplified = false;
55
59
60 bool is_true() const
61 {
62 return expr.is_true();
63 }
64
65 bool is_false() const
66 {
67 return expr.is_false();
68 }
69
72
77
78private:
80};
81
82#endif // CPROVER_ANALYSES_GUARD_EXPR_H
static exprt guard(const exprt::operandst &guards, exprt cond)
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
Definition ai.h:562
Base class for all expressions.
Definition expr.h:56
bool is_true() const
Return whether the expression is a constant representing true.
Definition expr.cpp:27
bool is_false() const
Return whether the expression is a constant representing false.
Definition expr.cpp:34
guard_exprt & operator=(const guard_exprt &other)
Definition guard_expr.h:33
void add(const exprt &expr)
bool is_true() const
Definition guard_expr.h:60
void append(const guard_exprt &guard)
Definition guard_expr.h:41
bool disjunction_may_simplify(const guard_exprt &other_guard)
Returns true if operator|= with other_guard may result in a simpler expression.
exprt as_expr() const
Definition guard_expr.h:46
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...
Definition guard_expr.h:29
friend guard_exprt & operator|=(guard_exprt &g1, const guard_exprt &g2)
bool is_false() const
Definition guard_expr.h:65
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.
Definition guard_expr.h:54
This is unused by this implementation of guards, but can be used by other implementations of the same...
Definition guard_expr.h:20