cprover
miniBDD.h
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module: A minimalistic BDD library, following Bryant's original paper
4  and Andersen's lecture notes
5 
6 Author: Daniel Kroening, kroening@kroening.com
7 
8 \*******************************************************************/
9 
13 
14 #ifndef CPROVER_SOLVERS_MINIBDD_MINIBDD_H
15 #define CPROVER_SOLVERS_MINIBDD_MINIBDD_H
16 
24 #include <cassert>
25 #include <list>
26 #include <vector>
27 #include <map>
28 #include <string>
29 #include <stack>
30 
31 class mini_bddt
32 {
33 public:
34  mini_bddt();
35  mini_bddt(const mini_bddt &x);
36  ~mini_bddt();
37 
38  // Boolean operators on BDDs
39  mini_bddt operator!() const;
40  mini_bddt operator^(const mini_bddt &) const;
41  mini_bddt operator==(const mini_bddt &) const;
42  mini_bddt operator&(const mini_bddt &) const;
43  mini_bddt operator|(const mini_bddt &) const;
44 
45  // copy operator
46  mini_bddt &operator=(const mini_bddt &);
47 
48  bool is_constant() const;
49  bool is_true() const;
50  bool is_false() const;
51 
52  unsigned var() const;
53  const mini_bddt &low() const;
54  const mini_bddt &high() const;
55  unsigned node_number() const;
56  void clear();
57 
58  bool is_initialized() const { return node!=nullptr; }
59 
60  // internal
61  explicit mini_bddt(class mini_bdd_nodet *_node);
63 };
64 
66 {
67 public:
71 
73  class mini_bdd_mgrt *_mgr,
74  unsigned _var, unsigned _node_number,
75  const mini_bddt &_low, const mini_bddt &_high);
76 
77  void add_reference();
78  void remove_reference();
79 };
80 
82 {
83 public:
84  mini_bdd_mgrt();
86 
87  mini_bddt Var(const std::string &label);
88 
89  void DumpDot(std::ostream &out, bool supress_zero=false) const;
90  void DumpTikZ(
91  std::ostream &out,
92  bool supress_zero=false,
93  bool node_numbers=true) const;
94  void DumpTable(std::ostream &out) const;
95 
96  const mini_bddt &True() const;
97  const mini_bddt &False() const;
98 
99  friend class mini_bdd_nodet;
100 
101  // create a node (consulting the reverse-map)
102  mini_bddt mk(unsigned var, const mini_bddt &low, const mini_bddt &high);
103 
104  std::size_t number_of_nodes();
105 
107  {
108  std::string label;
109  explicit var_table_entryt(const std::string &_label);
110  };
111 
112  typedef std::vector<var_table_entryt> var_tablet;
114 
115 protected:
116  typedef std::list<mini_bdd_nodet> nodest;
119 
120  // this is our reverse-map for nodes
122  {
123  unsigned var, low, high;
124  reverse_keyt(
125  unsigned _var, const mini_bddt &_low, const mini_bddt &_high);
126 
127  bool operator<(const reverse_keyt &) const;
128  };
129 
130  typedef std::map<reverse_keyt, mini_bdd_nodet *> reverse_mapt;
132 
133  typedef std::stack<mini_bdd_nodet *> freet;
135 };
136 
137 mini_bddt restrict(const mini_bddt &u, unsigned var, const bool value);
138 mini_bddt exists(const mini_bddt &u, unsigned var);
140  const mini_bddt &where,
141  unsigned var,
142  const mini_bddt &by_what);
143 std::string cubes(const mini_bddt &u);
144 bool OneSat(const mini_bddt &v, std::map<unsigned, bool> &assignment);
145 
146 // inline functions
147 #include "miniBDD.inc"
148 
149 #endif // CPROVER_SOLVERS_MINIBDD_MINIBDD_H
void clear()
std::vector< var_table_entryt > var_tablet
Definition: miniBDD.h:112
mini_bddt & operator=(const mini_bddt &)
mini_bddt operator&(const mini_bddt &) const
Definition: miniBDD.cpp:402
freet free
Definition: miniBDD.h:134
void DumpTikZ(std::ostream &out, bool supress_zero=false, bool node_numbers=true) const
Definition: miniBDD.cpp:111
reverse_mapt reverse_map
Definition: miniBDD.h:131
unsigned reference_counter
Definition: miniBDD.h:69
unsigned var() const
const mini_bddt & False() const
unsigned node_number() const
std::list< mini_bdd_nodet > nodest
Definition: miniBDD.h:116
mini_bddt substitute(const mini_bddt &where, unsigned var, const mini_bddt &by_what)
Definition: miniBDD.cpp:569
mini_bddt operator!() const
Definition: miniBDD.cpp:390
bool is_initialized() const
Definition: miniBDD.h:58
mini_bddt false_bdd
Definition: miniBDD.h:118
mini_bddt low
Definition: miniBDD.h:70
mini_bddt true_bdd
Definition: miniBDD.h:118
void add_reference()
unsigned node_number
Definition: miniBDD.h:69
void remove_reference()
Definition: miniBDD.cpp:23
mini_bdd_nodet(class mini_bdd_mgrt *_mgr, unsigned _var, unsigned _node_number, const mini_bddt &_low, const mini_bddt &_high)
nodest nodes
Definition: miniBDD.h:117
mini_bddt restrict(const mini_bddt &u, unsigned var, const bool value)
Definition: miniBDD.cpp:557
bool is_false() const
class mini_bdd_nodet * node
Definition: miniBDD.h:62
bool OneSat(const mini_bddt &v, std::map< unsigned, bool > &assignment)
Definition: miniBDD.cpp:618
var_tablet var_table
Definition: miniBDD.h:113
bool is_constant() const
var_table_entryt(const std::string &_label)
std::string cubes(const mini_bddt &u)
Definition: miniBDD.cpp:604
mini_bddt high
Definition: miniBDD.h:70
unsigned var
Definition: miniBDD.h:69
mini_bddt operator==(const mini_bddt &) const
Definition: miniBDD.cpp:375
const mini_bddt & high() const
mini_bddt Var(const std::string &label)
Definition: miniBDD.cpp:40
const mini_bddt & True() const
mini_bddt operator^(const mini_bddt &) const
Definition: miniBDD.cpp:385
mini_bddt mk(unsigned var, const mini_bddt &low, const mini_bddt &high)
Definition: miniBDD.cpp:430
reverse_keyt(unsigned _var, const mini_bddt &_low, const mini_bddt &_high)
void DumpTable(std::ostream &out) const
Definition: miniBDD.cpp:494
const mini_bddt & low() const
class mini_bdd_mgrt * mgr
Definition: miniBDD.h:68
mini_bddt operator|(const mini_bddt &) const
Definition: miniBDD.cpp:412
std::stack< mini_bdd_nodet * > freet
Definition: miniBDD.h:133
std::size_t number_of_nodes()
bool operator<(const reverse_keyt &) const
Definition: miniBDD.cpp:477
bool is_true() const
mini_bddt exists(const mini_bddt &u, unsigned var)
Definition: miniBDD.cpp:562
std::map< reverse_keyt, mini_bdd_nodet * > reverse_mapt
Definition: miniBDD.h:130
void DumpDot(std::ostream &out, bool supress_zero=false) const
Definition: miniBDD.cpp:48