CBMC
guard_expr.h
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module: Guard Data Structure
4 
5 Author: 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 {
25 public:
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 
41  void append(const guard_exprt &guard)
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 
58  exprt guard_expr(exprt expr) const;
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 
70  friend guard_exprt &operator-=(guard_exprt &g1, const guard_exprt &g2);
71  friend guard_exprt &operator|=(guard_exprt &g1, const guard_exprt &g2);
72 
76  bool disjunction_may_simplify(const guard_exprt &other_guard);
77 
78 private:
80 };
81 
82 #endif // CPROVER_ANALYSES_GUARD_EXPR_H
static exprt guard(const exprt::operandst &guards, exprt cond)
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
void add(const exprt &expr)
Definition: guard_expr.cpp:38
bool is_true() const
Definition: guard_expr.h:60
void append(const guard_exprt &guard)
Definition: guard_expr.h:41
guard_exprt & operator=(const guard_exprt &other)
Definition: guard_expr.h:33
bool disjunction_may_simplify(const guard_exprt &other_guard)
Returns true if operator|= with other_guard may result in a simpler expression.
Definition: guard_expr.cpp:123
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)
Definition: guard_expr.cpp:64
bool is_false() const
Definition: guard_expr.h:65
friend guard_exprt & operator|=(guard_exprt &g1, const guard_exprt &g2)
Definition: guard_expr.cpp:134
exprt guard_expr(exprt expr) const
Return guard => dest or a simplified variant thereof if either guard or dest are trivial.
Definition: guard_expr.cpp:18
exprt expr
Definition: guard_expr.h:79
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