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
mini_bddt::low
const mini_bddt & low() const
mini_bdd_mgrt::reverse_keyt::operator<
bool operator<(const reverse_keyt &) const
Definition: miniBDD.cpp:477
mini_bdd_mgrt::mk
mini_bddt mk(unsigned var, const mini_bddt &low, const mini_bddt &high)
Definition: miniBDD.cpp:430
mini_bdd_mgrt::DumpTikZ
void DumpTikZ(std::ostream &out, bool supress_zero=false, bool node_numbers=true) const
Definition: miniBDD.cpp:111
mini_bdd_mgrt::reverse_keyt::reverse_keyt
reverse_keyt(unsigned _var, const mini_bddt &_low, const mini_bddt &_high)
mini_bdd_mgrt::reverse_mapt
std::map< reverse_keyt, mini_bdd_nodet * > reverse_mapt
Definition: miniBDD.h:130
mini_bdd_mgrt::~mini_bdd_mgrt
~mini_bdd_mgrt()
Definition: miniBDD.cpp:426
mini_bdd_nodet::high
mini_bddt high
Definition: miniBDD.h:70
mini_bdd_nodet::remove_reference
void remove_reference()
Definition: miniBDD.cpp:23
mini_bdd_mgrt::True
const mini_bddt & True() const
OneSat
bool OneSat(const mini_bddt &v, std::map< unsigned, bool > &assignment)
Definition: miniBDD.cpp:618
mini_bddt::is_false
bool is_false() const
mini_bdd_mgrt::true_bdd
mini_bddt true_bdd
Definition: miniBDD.h:118
exists
mini_bddt exists(const mini_bddt &u, unsigned var)
Definition: miniBDD.cpp:562
mini_bdd_mgrt::reverse_map
reverse_mapt reverse_map
Definition: miniBDD.h:131
mini_bddt::operator=
mini_bddt & operator=(const mini_bddt &)
mini_bdd_nodet::reference_counter
unsigned reference_counter
Definition: miniBDD.h:69
mini_bddt::operator^
mini_bddt operator^(const mini_bddt &) const
Definition: miniBDD.cpp:385
mini_bdd_mgrt::reverse_keyt::high
unsigned high
Definition: miniBDD.h:123
mini_bdd_mgrt::nodes
nodest nodes
Definition: miniBDD.h:117
mini_bddt::var
unsigned var() const
mini_bdd_mgrt::reverse_keyt
Definition: miniBDD.h:121
mini_bdd_mgrt::number_of_nodes
std::size_t number_of_nodes()
cubes
std::string cubes(const mini_bddt &u)
Definition: miniBDD.cpp:604
mini_bdd_mgrt::freet
std::stack< mini_bdd_nodet * > freet
Definition: miniBDD.h:133
mini_bdd_mgrt::DumpDot
void DumpDot(std::ostream &out, bool supress_zero=false) const
Definition: miniBDD.cpp:48
mini_bdd_mgrt::free
freet free
Definition: miniBDD.h:134
mini_bdd_mgrt::nodest
std::list< mini_bdd_nodet > nodest
Definition: miniBDD.h:116
mini_bdd_nodet::node_number
unsigned node_number
Definition: miniBDD.h:69
mini_bdd_mgrt
Definition: miniBDD.h:81
mini_bdd_nodet::low
mini_bddt low
Definition: miniBDD.h:70
mini_bddt::operator&
mini_bddt operator&(const mini_bddt &) const
Definition: miniBDD.cpp:402
mini_bdd_mgrt::var_table
var_tablet var_table
Definition: miniBDD.h:113
mini_bdd_mgrt::DumpTable
void DumpTable(std::ostream &out) const
Definition: miniBDD.cpp:494
mini_bdd_nodet::var
unsigned var
Definition: miniBDD.h:69
mini_bdd_mgrt::var_table_entryt::label
std::string label
Definition: miniBDD.h:108
mini_bddt::is_initialized
bool is_initialized() const
Definition: miniBDD.h:58
mini_bdd_mgrt::var_tablet
std::vector< var_table_entryt > var_tablet
Definition: miniBDD.h:112
mini_bdd_mgrt::False
const mini_bddt & False() const
mini_bddt::clear
void clear()
mini_bdd_nodet
Definition: miniBDD.h:65
mini_bddt::~mini_bddt
~mini_bddt()
mini_bdd_nodet::mgr
class mini_bdd_mgrt * mgr
Definition: miniBDD.h:68
mini_bddt::is_true
bool is_true() const
mini_bdd_mgrt::false_bdd
mini_bddt false_bdd
Definition: miniBDD.h:118
mini_bddt::operator|
mini_bddt operator|(const mini_bddt &) const
Definition: miniBDD.cpp:412
mini_bdd_nodet::add_reference
void add_reference()
mini_bddt::operator==
mini_bddt operator==(const mini_bddt &) const
Definition: miniBDD.cpp:375
mini_bddt
Definition: miniBDD.h:31
mini_bddt::mini_bddt
mini_bddt()
mini_bdd_mgrt::var_table_entryt
Definition: miniBDD.h:106
mini_bddt::node_number
unsigned node_number() const
mini_bdd_nodet::mini_bdd_nodet
mini_bdd_nodet(class mini_bdd_mgrt *_mgr, unsigned _var, unsigned _node_number, const mini_bddt &_low, const mini_bddt &_high)
mini_bdd_mgrt::reverse_keyt::low
unsigned low
Definition: miniBDD.h:123
mini_bddt::node
class mini_bdd_nodet * node
Definition: miniBDD.h:62
restrict
mini_bddt restrict(const mini_bddt &u, unsigned var, const bool value)
Definition: miniBDD.cpp:557
mini_bddt::high
const mini_bddt & high() const
mini_bdd_mgrt::Var
mini_bddt Var(const std::string &label)
Definition: miniBDD.cpp:40
mini_bddt::operator!
mini_bddt operator!() const
Definition: miniBDD.cpp:390
mini_bddt::is_constant
bool is_constant() const
mini_bdd_mgrt::reverse_keyt::var
unsigned var
Definition: miniBDD.h:123
mini_bdd_mgrt::var_table_entryt::var_table_entryt
var_table_entryt(const std::string &_label)
substitute
mini_bddt substitute(const mini_bddt &where, unsigned var, const mini_bddt &by_what)
Definition: miniBDD.cpp:569
mini_bdd_mgrt::mini_bdd_mgrt
mini_bdd_mgrt()
Definition: miniBDD.cpp:417