CBMC
All Classes Namespaces Files Functions Variables Typedefs Enumerations Enumerator Friends Macros Modules Pages
bdd_miniBDD.h
Go to the documentation of this file.
1/*******************************************************************\
2
3Module: Binary Decision Diagrams
4
5Author: Romain Brenguier, romain.brenguier@diffblue.com
6
7\*******************************************************************/
8
14
15#ifndef CPROVER_SOLVERS_BDD_BDD_MINIBDD_H
16#define CPROVER_SOLVERS_BDD_BDD_MINIBDD_H
17
18#include <unordered_map>
19
21
22class bdd_managert;
23class bddt;
24class bdd_nodet;
25
27class bdd_nodet
28{
29public:
32 bool is_constant() const
33 {
34 return node->node_number <= 1;
35 }
36
37 bool is_complement() const
38 {
39 return node->node_number == 0;
40 }
41
43 using indext = std::size_t;
44
46 indext index() const
47 {
48 return bdd_var_to_index.at(node->var);
49 }
50
52 {
53 return bdd_nodet(node->high.node, bdd_var_to_index);
54 }
55
57 {
58 return bdd_nodet(node->low.node, bdd_var_to_index);
59 }
60
63
65 idt id() const
66 {
67 return node;
68 }
69
70private:
72
73 // Should be owned by the BDD manager
74 const std::unordered_map<std::size_t, std::size_t> &bdd_var_to_index;
75
76 explicit bdd_nodet(
78 const std::unordered_map<std::size_t, std::size_t> &bdd_var_to_index)
80 {
81 }
82
83 friend class bdd_managert;
84};
85
87class bddt : private mini_bddt
88{
89public:
90 bool equals(const bddt &other) const
91 {
92 return node == other.node;
93 }
94
95 bool is_true() const
96 {
97 return mini_bddt::is_true();
98 }
99
100 bool is_false() const
101 {
102 return mini_bddt::is_false();
103 }
104
105 bddt bdd_not() const
106 {
107 return bddt(!(*this));
108 }
109
110 bddt bdd_or(const bddt &other) const
111 {
112 return bddt(*this | other);
113 }
114
115 bddt bdd_and(const bddt &other) const
116 {
117 return bddt(*this & other);
118 }
119
120 bddt bdd_xor(const bddt &other) const
121 {
122 return bddt(*this ^ other);
123 }
124
125 static bddt bdd_ite(const bddt &i, const bddt &t, const bddt &e)
126 {
127 return i.bdd_and(t).bdd_or(i.bdd_not().bdd_and(e));
128 }
129
130 bddt constrain(const bddt &other)
131 {
132 // This is correct, though not very useful
133 return bddt(*this);
134 }
135
136 bddt &operator=(const bddt &other)
137 {
138 if(this != &other)
140 return *this;
141 }
142
143private:
144 friend class bdd_managert;
145 explicit bddt(const mini_bddt &bdd) : mini_bddt(bdd)
146 {
147 }
148};
149
151class bdd_managert : private mini_bdd_mgrt
152{
153public:
155 {
156 return bddt(True());
157 }
158
160 {
161 return bddt(False());
162 }
163
165 {
166 auto it = index_to_bdd.find(index);
167 if(it != index_to_bdd.end())
168 return it->second;
169 auto var = Var(std::to_string(index));
170 auto emplace_result = index_to_bdd.emplace(index, bddt(var));
171 bdd_var_to_index[var.var()] = index;
172 return emplace_result.first->second;
173 }
174
175 bdd_nodet bdd_node(const bddt &bdd) const
176 {
177 return bdd_nodet(bdd.node, bdd_var_to_index);
178 }
179
180 bdd_managert(const bdd_managert &) = delete;
181 bdd_managert() = default;
182
183private:
184 std::unordered_map<std::size_t, bddt> index_to_bdd;
185 std::unordered_map<std::size_t, std::size_t> bdd_var_to_index;
186};
187
188#endif // CPROVER_SOLVERS_BDD_BDD_MINIBDD_H
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
Definition ai.h:562
Manager for BDD creation.
Definition bdd_cudd.h:137
bddt bdd_false()
bddt bdd_true()
bdd_nodet bdd_node(const bddt &bdd) const
std::unordered_map< std::size_t, std::size_t > bdd_var_to_index
bdd_managert(const bdd_managert &)=delete
bdd_managert()=default
bddt bdd_variable(bdd_nodet::indext index)
std::unordered_map< std::size_t, bddt > index_to_bdd
Low level access to the structure of the BDD, read-only.
Definition bdd_cudd.h:28
const std::unordered_map< std::size_t, std::size_t > & bdd_var_to_index
Definition bdd_miniBDD.h:74
indext index() const
Label on the node, corresponds to the index of a Boolean variable.
Definition bdd_miniBDD.h:46
bool is_complement() const
Definition bdd_miniBDD.h:37
bdd_nodet(mini_bdd_nodet *node, const std::unordered_map< std::size_t, std::size_t > &bdd_var_to_index)
Definition bdd_miniBDD.h:76
idt id() const
Unique identifier of the node.
Definition bdd_miniBDD.h:65
mini_bdd_nodet * node
Definition bdd_miniBDD.h:71
bool is_constant() const
is_constant has to be true for true and false and to distinguish between the two, is_complement has t...
Definition bdd_miniBDD.h:32
bdd_nodet then_branch() const
Definition bdd_miniBDD.h:51
DdNode * node
Definition bdd_cudd.h:69
bdd_nodet else_branch() const
Definition bdd_miniBDD.h:56
Logical operations on BDDs.
Definition bdd_cudd.h:78
bool equals(const bddt &other) const
Definition bdd_miniBDD.h:90
bddt bdd_xor(const bddt &other) const
bddt & operator=(const bddt &other)
bddt constrain(const bddt &other)
static bddt bdd_ite(const bddt &i, const bddt &t, const bddt &e)
bddt bdd_or(const bddt &other) const
bddt bdd_not() const
bool is_true() const
Definition bdd_miniBDD.h:95
bddt(const mini_bddt &bdd)
bddt bdd_and(const bddt &other) const
bool is_false() const
BDD bdd
Definition bdd_cudd.h:128
mini_bddt Var(const std::string &label)
Definition miniBDD.cpp:37
const mini_bddt & False() const
const mini_bddt & True() const
mini_bddt & operator=(const mini_bddt &)
bool is_false() const
bool is_true() const
class mini_bdd_nodet * node
Definition miniBDD.h:64
A minimalistic BDD library, following Bryant's original paper and Andersen's lecture notes.