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_BDD_MINIBDD_MINIBDD_H
15 #define CPROVER_SOLVERS_BDD_MINIBDD_MINIBDD_H
16 
24 #include <cassert>
25 #include <list>
26 #include <map>
27 #include <stack>
28 #include <string>
29 #include <vector>
30 
31 class mini_bddt
32 {
33 public:
35  mini_bddt(const mini_bddt &x);
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
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
59  {
60  return node != nullptr;
61  }
62 
63  // internal
64  explicit mini_bddt(class mini_bdd_nodet *_node);
66 };
67 
69 {
70 public:
74 
76  class mini_bdd_mgrt *_mgr,
77  unsigned _var,
78  unsigned _node_number,
79  const mini_bddt &_low,
80  const mini_bddt &_high);
81 
82  void add_reference();
83  void remove_reference();
84 };
85 
87 {
88 public:
89  mini_bdd_mgrt();
91 
92  mini_bddt Var(const std::string &label);
93 
94  void DumpDot(std::ostream &out, bool supress_zero = false) const;
95  void DumpTikZ(
96  std::ostream &out,
97  bool supress_zero = false,
98  bool node_numbers = true) const;
99  void DumpTable(std::ostream &out) const;
100 
101  const mini_bddt &True() const;
102  const mini_bddt &False() const;
103 
104  friend class mini_bdd_nodet;
105 
106  // create a node (consulting the reverse-map)
107  mini_bddt mk(unsigned var, const mini_bddt &low, const mini_bddt &high);
108 
109  std::size_t number_of_nodes();
110 
112  {
113  std::string label;
114  explicit var_table_entryt(const std::string &_label);
115  };
116 
117  typedef std::vector<var_table_entryt> var_tablet;
119 
120 protected:
121  typedef std::list<mini_bdd_nodet> nodest;
124 
125  // this is our reverse-map for nodes
127  {
128  unsigned var, low, high;
129  reverse_keyt(unsigned _var, const mini_bddt &_low, const mini_bddt &_high);
130 
131  bool operator<(const reverse_keyt &) const;
132  };
133 
134  typedef std::map<reverse_keyt, mini_bdd_nodet *> reverse_mapt;
136 
137  typedef std::stack<mini_bdd_nodet *> freet;
139 };
140 
141 mini_bddt restrict(const mini_bddt &u, unsigned var, const bool value);
142 mini_bddt exists(const mini_bddt &u, unsigned var);
143 mini_bddt
144 substitute(const mini_bddt &where, unsigned var, const mini_bddt &by_what);
145 std::string cubes(const mini_bddt &u);
146 bool OneSat(const mini_bddt &v, std::map<unsigned, bool> &assignment);
147 
148 // inline functions
149 #include "miniBDD.inc"
150 
151 #endif // CPROVER_SOLVERS_BDD_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:472
mini_bdd_mgrt::mk
mini_bddt mk(unsigned var, const mini_bddt &low, const mini_bddt &high)
Definition: miniBDD.cpp:427
mini_bdd_mgrt::DumpTikZ
void DumpTikZ(std::ostream &out, bool supress_zero=false, bool node_numbers=true) const
Definition: miniBDD.cpp:109
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:134
mini_bdd_mgrt::~mini_bdd_mgrt
~mini_bdd_mgrt()
Definition: miniBDD.cpp:422
mini_bdd_nodet::high
mini_bddt high
Definition: miniBDD.h:73
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:613
mini_bddt::is_false
bool is_false() const
mini_bdd_mgrt::true_bdd
mini_bddt true_bdd
Definition: miniBDD.h:123
exists
mini_bddt exists(const mini_bddt &u, unsigned var)
Definition: miniBDD.cpp:559
mini_bdd_mgrt::reverse_map
reverse_mapt reverse_map
Definition: miniBDD.h:135
mini_bddt::operator=
mini_bddt & operator=(const mini_bddt &)
mini_bdd_nodet::reference_counter
unsigned reference_counter
Definition: miniBDD.h:72
mini_bddt::operator^
mini_bddt operator^(const mini_bddt &) const
Definition: miniBDD.cpp:381
mini_bdd_mgrt::reverse_keyt::high
unsigned high
Definition: miniBDD.h:128
mini_bdd_mgrt::nodes
nodest nodes
Definition: miniBDD.h:122
mini_bddt::var
unsigned var() const
mini_bdd_mgrt::reverse_keyt
Definition: miniBDD.h:127
mini_bdd_mgrt::number_of_nodes
std::size_t number_of_nodes()
cubes
std::string cubes(const mini_bddt &u)
Definition: miniBDD.cpp:599
mini_bdd_mgrt::freet
std::stack< mini_bdd_nodet * > freet
Definition: miniBDD.h:137
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:138
mini_bdd_mgrt::nodest
std::list< mini_bdd_nodet > nodest
Definition: miniBDD.h:121
mini_bdd_nodet::node_number
unsigned node_number
Definition: miniBDD.h:72
mini_bdd_mgrt
Definition: miniBDD.h:87
mini_bddt::mini_bddt
mini_bddt(class mini_bdd_nodet *_node)
mini_bdd_nodet::low
mini_bddt low
Definition: miniBDD.h:73
mini_bddt::operator&
mini_bddt operator&(const mini_bddt &) const
Definition: miniBDD.cpp:398
mini_bdd_mgrt::var_table
var_tablet var_table
Definition: miniBDD.h:118
mini_bdd_mgrt::DumpTable
void DumpTable(std::ostream &out) const
Definition: miniBDD.cpp:488
mini_bdd_nodet::var
unsigned var
Definition: miniBDD.h:72
mini_bdd_mgrt::var_table_entryt::label
std::string label
Definition: miniBDD.h:113
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:117
mini_bdd_mgrt::False
const mini_bddt & False() const
mini_bddt::clear
void clear()
mini_bdd_nodet
Definition: miniBDD.h:69
mini_bddt::~mini_bddt
~mini_bddt()
mini_bdd_nodet::mgr
class mini_bdd_mgrt * mgr
Definition: miniBDD.h:71
mini_bddt::is_true
bool is_true() const
mini_bddt::mini_bddt
mini_bddt(const mini_bddt &x)
mini_bdd_mgrt::false_bdd
mini_bddt false_bdd
Definition: miniBDD.h:123
mini_bddt::operator|
mini_bddt operator|(const mini_bddt &) const
Definition: miniBDD.cpp:408
mini_bdd_nodet::add_reference
void add_reference()
mini_bddt::operator==
mini_bddt operator==(const mini_bddt &) const
Definition: miniBDD.cpp:371
mini_bddt
Definition: miniBDD.h:32
mini_bddt::mini_bddt
mini_bddt()
mini_bdd_mgrt::var_table_entryt
Definition: miniBDD.h:112
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:128
mini_bddt::node
class mini_bdd_nodet * node
Definition: miniBDD.h:65
restrict
mini_bddt restrict(const mini_bddt &u, unsigned var, const bool value)
Definition: miniBDD.cpp:554
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:386
mini_bddt::is_constant
bool is_constant() const
mini_bdd_mgrt::reverse_keyt::var
unsigned var
Definition: miniBDD.h:128
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:565
mini_bdd_mgrt::mini_bdd_mgrt
mini_bdd_mgrt()
Definition: miniBDD.cpp:413