CBMC
All Classes Namespaces Files Functions Variables Typedefs Enumerations Enumerator Friends Macros Modules Pages
miniBDD.h
Go to the documentation of this file.
1/*******************************************************************\
2
3Module: A minimalistic BDD library, following Bryant's original paper
4 and Andersen's lecture notes
5
6Author: 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 <list>
25#include <map>
26#include <stack>
27#include <string>
28#include <vector>
29
31{
32public:
36
37 // Boolean operators on BDDs
38 mini_bddt operator!() const;
39 mini_bddt operator^(const mini_bddt &) 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
44 // copy operator
46
47 bool is_constant() const;
48 bool is_true() const;
49 bool is_false() const;
50
51 unsigned var() const;
52 const mini_bddt &low() const;
53 const mini_bddt &high() const;
54 unsigned node_number() const;
55 void clear();
56
57 bool is_initialized() const
58 {
59 return node != nullptr;
60 }
61
62 // internal
63 explicit mini_bddt(class mini_bdd_nodet *_node);
65};
66
68{
69public:
73
75 class mini_bdd_mgrt *_mgr,
76 unsigned _var,
77 unsigned _node_number,
78 const mini_bddt &_low,
79 const mini_bddt &_high);
80
82 void remove_reference();
83};
84
86{
87public:
90
91 mini_bddt Var(const std::string &label);
92
93 void DumpDot(std::ostream &out, bool supress_zero = false) const;
94 void DumpTikZ(
95 std::ostream &out,
96 bool supress_zero = false,
97 bool node_numbers = true) const;
98 void DumpTable(std::ostream &out) const;
99
100 const mini_bddt &True() const;
101 const mini_bddt &False() const;
102
103 friend class mini_bdd_nodet;
104
105 // create a node (consulting the reverse-map)
106 mini_bddt mk(unsigned var, const mini_bddt &low, const mini_bddt &high);
107
108 std::size_t number_of_nodes();
109
111 {
112 std::string label;
113 explicit var_table_entryt(const std::string &_label);
114 };
115
116 typedef std::vector<var_table_entryt> var_tablet;
118
119protected:
120 typedef std::list<mini_bdd_nodet> nodest;
123
124 // this is our reverse-map for nodes
126 {
127 unsigned var, low, high;
128 reverse_keyt(unsigned _var, const mini_bddt &_low, const mini_bddt &_high);
129
130 bool operator<(const reverse_keyt &) const;
131 };
132
133 typedef std::map<reverse_keyt, mini_bdd_nodet *> reverse_mapt;
135
136 typedef std::stack<mini_bdd_nodet *> freet;
138};
139
140mini_bddt restrict(const mini_bddt &u, unsigned var, const bool value);
141mini_bddt exists(const mini_bddt &u, unsigned var);
143substitute(const mini_bddt &where, unsigned var, const mini_bddt &by_what);
144std::string cubes(const mini_bddt &u);
145bool OneSat(const mini_bddt &v, std::map<unsigned, bool> &assignment);
146
147// inline functions
148#include "miniBDD.inc" // IWYU pragma: keep
149
150#endif // CPROVER_SOLVERS_BDD_MINIBDD_MINIBDD_H
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
Definition ai.h:562
mini_bddt false_bdd
Definition miniBDD.h:122
mini_bddt Var(const std::string &label)
Definition miniBDD.cpp:37
std::size_t number_of_nodes()
const mini_bddt & False() const
nodest nodes
Definition miniBDD.h:121
std::list< mini_bdd_nodet > nodest
Definition miniBDD.h:120
void DumpTable(std::ostream &out) const
Definition miniBDD.cpp:486
void DumpDot(std::ostream &out, bool supress_zero=false) const
Definition miniBDD.cpp:45
void DumpTikZ(std::ostream &out, bool supress_zero=false, bool node_numbers=true) const
Definition miniBDD.cpp:107
mini_bddt mk(unsigned var, const mini_bddt &low, const mini_bddt &high)
Definition miniBDD.cpp:425
const mini_bddt & True() const
std::stack< mini_bdd_nodet * > freet
Definition miniBDD.h:136
reverse_mapt reverse_map
Definition miniBDD.h:134
std::vector< var_table_entryt > var_tablet
Definition miniBDD.h:116
var_tablet var_table
Definition miniBDD.h:117
std::map< reverse_keyt, mini_bdd_nodet * > reverse_mapt
Definition miniBDD.h:133
mini_bddt true_bdd
Definition miniBDD.h:122
unsigned node_number
Definition miniBDD.h:71
class mini_bdd_mgrt * mgr
Definition miniBDD.h:70
unsigned reference_counter
Definition miniBDD.h:71
mini_bdd_nodet(class mini_bdd_mgrt *_mgr, unsigned _var, unsigned _node_number, const mini_bddt &_low, const mini_bddt &_high)
void add_reference()
mini_bddt high
Definition miniBDD.h:72
void remove_reference()
Definition miniBDD.cpp:20
unsigned var
Definition miniBDD.h:71
mini_bddt low
Definition miniBDD.h:72
mini_bddt operator!() const
Definition miniBDD.cpp:384
const mini_bddt & high() const
bool is_initialized() const
Definition miniBDD.h:57
mini_bddt & operator=(const mini_bddt &)
mini_bddt(const mini_bddt &x)
const mini_bddt & low() const
bool is_constant() const
mini_bddt operator&(const mini_bddt &) const
Definition miniBDD.cpp:396
mini_bddt operator^(const mini_bddt &) const
Definition miniBDD.cpp:379
void clear()
bool is_false() const
mini_bddt operator|(const mini_bddt &) const
Definition miniBDD.cpp:406
unsigned var() const
unsigned node_number() const
bool is_true() const
mini_bddt(class mini_bdd_nodet *_node)
class mini_bdd_nodet * node
Definition miniBDD.h:64
mini_bddt operator==(const mini_bddt &) const
Definition miniBDD.cpp:369
mini_bddt restrict(const mini_bddt &u, unsigned var, const bool value)
Definition miniBDD.cpp:551
mini_bddt exists(const mini_bddt &u, unsigned var)
Definition miniBDD.cpp:556
std::string cubes(const mini_bddt &u)
Definition miniBDD.cpp:596
bool OneSat(const mini_bddt &v, std::map< unsigned, bool > &assignment)
Definition miniBDD.cpp:610
mini_bddt substitute(const mini_bddt &where, unsigned var, const mini_bddt &by_what)
Definition miniBDD.cpp:562
reverse_keyt(unsigned _var, const mini_bddt &_low, const mini_bddt &_high)
bool operator<(const reverse_keyt &) const
Definition miniBDD.cpp:470
var_table_entryt(const std::string &_label)