cprover
guard_bdd.h
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module: Guard Data Structure
4 
5 Author: Romain Brenguier, romain.brenguier@diffblue.com
6 
7 \*******************************************************************/
8 
12 
13 #ifndef CPROVER_ANALYSES_GUARD_BDD_H
14 #define CPROVER_ANALYSES_GUARD_BDD_H
15 
16 #include <iosfwd>
17 #include <memory>
18 
19 #include <solvers/bdd/bdd.h>
20 #include <solvers/prop/bdd_expr.h>
21 #include <util/make_unique.h>
22 #include <util/std_expr.h>
23 
25 {
26 public:
27  guard_bddt(const exprt &e, bdd_exprt &manager);
28  guard_bddt(const guard_bddt &other) : manager(other.manager), bdd(other.bdd)
29  {
30  }
31 
32  guard_bddt &operator=(const guard_bddt &other);
34  guard_bddt &add(const exprt &expr);
35  guard_bddt &append(const guard_bddt &guard);
36  exprt as_expr() const;
37 
41  static constexpr bool is_always_simplified = true;
42 
45  exprt guard_expr(exprt expr) const;
46 
47  bool is_true() const
48  {
49  return bdd.is_true();
50  }
51 
52  bool is_false() const
53  {
54  return bdd.is_false();
55  }
56 
59  friend guard_bddt &operator-=(guard_bddt &g1, const guard_bddt &g2);
60 
61  friend guard_bddt &operator|=(guard_bddt &g1, const guard_bddt &g2);
62 
64  {
65  return guard_bddt(manager, bdd.bdd_not());
66  }
67 
70  bool disjunction_may_simplify(const guard_bddt &other_guard)
71  {
72  return true;
73  }
74 
75 private:
78 
80  : manager(manager), bdd(std::move(bdd))
81  {
82  }
83 };
84 
85 #endif // CPROVER_ANALYSES_GUARD_BDD_H
guard_bddt::is_true
bool is_true() const
Definition: guard_bdd.h:47
guard_bddt::append
guard_bddt & append(const guard_bddt &guard)
Definition: guard_bdd.cpp:67
guard_bddt::operator!
guard_bddt operator!() const
Definition: guard_bdd.h:63
guard_bddt::disjunction_may_simplify
bool disjunction_may_simplify(const guard_bddt &other_guard)
Returns true if operator|= with other_guard may result in a simpler expression.
Definition: guard_bdd.h:70
bddt::bdd_not
bddt bdd_not() const
Definition: bdd_cudd.h:95
guard_bddt::bdd
bddt bdd
Definition: guard_bdd.h:77
bdd.h
Choice between the different interface to BDD libraries.
exprt
Base class for all expressions.
Definition: expr.h:53
guard_bddt
Definition: guard_bdd.h:25
guard_bddt::guard_bddt
guard_bddt(bdd_exprt &manager, bddt bdd)
Definition: guard_bdd.h:79
bdd_exprt
Conversion between exprt and bbdt This encapsulate a bdd_managert, thus BDDs created with this class ...
Definition: bdd_expr.h:34
guard_bddt::add
guard_bddt & add(const exprt &expr)
Definition: guard_bdd.cpp:73
make_unique.h
guard_bddt::is_false
bool is_false() const
Definition: guard_bdd.h:52
guard_bddt::operator|=
friend guard_bddt & operator|=(guard_bddt &g1, const guard_bddt &g2)
Definition: guard_bdd.cpp:85
guard_bddt::guard_bddt
guard_bddt(const exprt &e, bdd_exprt &manager)
Definition: guard_bdd.cpp:28
guard_bddt::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_bdd.cpp:47
bdd_expr.h
Conversion between exprt and miniBDD.
guard_bddt::operator=
guard_bddt & operator=(const guard_bddt &other)
Definition: guard_bdd.cpp:33
guard_bddt::manager
bdd_exprt & manager
Definition: guard_bdd.h:76
bddt::is_true
bool is_true() const
Definition: bdd_cudd.h:85
bddt::is_false
bool is_false() const
Definition: bdd_cudd.h:90
guard_bddt::guard_bddt
guard_bddt(const guard_bddt &other)
Definition: guard_bdd.h:28
bddt
Logical operations on BDDs.
Definition: bdd_cudd.h:78
guard_bddt::is_always_simplified
static constexpr bool is_always_simplified
BDDs are always in a simplified form and thus no further simplification is required after calls to as...
Definition: guard_bdd.h:41
std_expr.h
API to expression classes.
guard_bddt::as_expr
exprt as_expr() const
Definition: guard_bdd.cpp:91
guard_bddt::operator-=
friend guard_bddt & operator-=(guard_bddt &g1, const guard_bddt &g2)
Transforms g1 into g1' such that ‘g1’ & g2 => g1 => g1'` and returns a reference to g1.
Definition: guard_bdd.cpp:79