cprover
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 <iosfwd>
16 
17 #include <util/expr_util.h>
18 #include <util/std_expr.h>
19 
23 {
24 };
25 
27 {
28 public:
32  explicit guard_exprt(const exprt &e, guard_expr_managert &) : expr(e)
33  {
34  }
35 
37  {
38  expr = other.expr;
39  return *this;
40  }
41 
42  void add(const exprt &expr);
43 
44  void append(const guard_exprt &guard)
45  {
46  add(guard.as_expr());
47  }
48 
49  exprt as_expr() const
50  {
51  return expr;
52  }
53 
57  static constexpr bool is_always_simplified = false;
58 
61  exprt guard_expr(exprt expr) const;
62 
63  bool is_true() const
64  {
65  return expr.is_true();
66  }
67 
68  bool is_false() const
69  {
70  return expr.is_false();
71  }
72 
73  friend guard_exprt &operator-=(guard_exprt &g1, const guard_exprt &g2);
74  friend guard_exprt &operator|=(guard_exprt &g1, const guard_exprt &g2);
75 
79  bool disjunction_may_simplify(const guard_exprt &other_guard);
80 
81 private:
83 };
84 
85 #endif // CPROVER_ANALYSES_GUARD_EXPR_H
guard_exprt
Definition: guard_expr.h:26
guard_exprt::operator|=
friend guard_exprt & operator|=(guard_exprt &g1, const guard_exprt &g2)
Definition: guard_expr.cpp:104
guard_exprt::operator-=
friend guard_exprt & operator-=(guard_exprt &g1, const guard_exprt &g2)
Definition: guard_expr.cpp:66
guard_exprt::guard_expr
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:20
exprt
Base class for all expressions.
Definition: expr.h:52
guard_exprt::is_true
bool is_true() const
Definition: guard_expr.h:63
exprt::is_true
bool is_true() const
Return whether the expression is a constant representing true.
Definition: expr.cpp:92
guard_exprt::operator=
guard_exprt & operator=(const guard_exprt &other)
Definition: guard_expr.h:36
guard_exprt::expr
exprt expr
Definition: guard_expr.h:82
exprt::is_false
bool is_false() const
Return whether the expression is a constant representing false.
Definition: expr.cpp:101
guard_expr_managert
This is unused by this implementation of guards, but can be used by other implementations of the same...
Definition: guard_expr.h:22
guard_exprt::as_expr
exprt as_expr() const
Definition: guard_expr.h:49
guard_exprt::add
void add(const exprt &expr)
Definition: guard_expr.cpp:40
guard_exprt::disjunction_may_simplify
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:93
guard_exprt::guard_exprt
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:32
guard_exprt::is_false
bool is_false() const
Definition: guard_expr.h:68
expr_util.h
Deprecated expression utility functions.
guard_exprt::append
void append(const guard_exprt &guard)
Definition: guard_expr.h:44
std_expr.h
guard_exprt::is_always_simplified
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:57