CBMC
All Classes Namespaces Files Functions Variables Typedefs Enumerations Enumerator Friends Macros Modules Pages
miniBDD.cpp
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#include "miniBDD.h"
15
16#include <util/invariant.h>
17
18#include <iostream>
19
21{
23 reference_counter != 0, "all references were already removed");
24
26
27 if(reference_counter == 0 && node_number >= 2)
28 {
30 mgr->reverse_map.erase(reverse_key);
31 low.clear();
32 high.clear();
33 mgr->free.push(this);
34 }
35}
36
37mini_bddt mini_bdd_mgrt::Var(const std::string &label)
38{
39 var_table.push_back(var_table_entryt(label));
40 true_bdd.node->var = var_table.size() + 1;
41 false_bdd.node->var = var_table.size() + 1;
42 return mk(var_table.size(), false_bdd, true_bdd);
43}
44
45void mini_bdd_mgrt::DumpDot(std::ostream &out, bool suppress_zero) const
46{
47 out << "digraph BDD {\n";
48
49 out << "center = true;\n";
50
51 out << "{ rank = same; { node [style=invis]; \"T\" };\n";
52
53 if(!suppress_zero)
54 out << " { node [shape=box,fontsize=24]; \"0\"; }\n";
55
56 out << " { node [shape=box,fontsize=24]; \"1\"; }\n"
57 << "}\n\n";
58
59 for(unsigned v = 0; v < var_table.size(); v++)
60 {
61 out << "{ rank=same; "
62 "{ node [shape=plaintext,fontname=\"Times Italic\",fontsize=24] \" "
63 << var_table[v].label << " \" }; ";
64
65 for(const auto &u : nodes)
66 {
67 if(u.var == (v + 1) && u.reference_counter != 0)
68 out << '"' << u.node_number << "\"; ";
69 }
70
71 out << "}\n";
72 }
73
74 out << '\n';
75
76 out << "{ edge [style = invis];";
77
78 for(unsigned v = 0; v < var_table.size(); v++)
79 out << " \" " << var_table[v].label << " \" ->";
80
81 out << " \"T\"; }\n";
82
83 out << '\n';
84
85 for(const auto &u : nodes)
86 {
87 if(u.reference_counter == 0)
88 continue;
89 if(u.node_number <= 1)
90 continue;
91
92 if(!suppress_zero || u.high.node_number() != 0)
93 out << '"' << u.node_number << '"' << " -> " << '"'
94 << u.high.node_number() << '"'
95 << " [style=solid,arrowsize=\".75\"];\n";
96
97 if(!suppress_zero || u.low.node_number() != 0)
98 out << '"' << u.node_number << '"' << " -> " << '"' << u.low.node_number()
99 << '"' << " [style=dashed,arrowsize=\".75\"];\n";
100
101 out << '\n';
102 }
103
104 out << "}\n";
105}
106
108 std::ostream &out,
109 bool suppress_zero,
110 bool node_numbers) const
111{
112 out << "\\begin{tikzpicture}[node distance=1cm]\n";
113
114 out << " \\tikzstyle{BDDnode}=[circle,draw=black,"
115 "inner sep=0pt,minimum size=5mm]\n";
116
117 for(unsigned v = 0; v < var_table.size(); v++)
118 {
119 out << " \\node[";
120
121 if(v != 0)
122 out << "below of=v" << var_table[v - 1].label;
123
124 out << "] (v" << var_table[v].label << ") {$\\mathit{" << var_table[v].label
125 << "}$};\n";
126
127 unsigned previous = 0;
128
129 for(const auto &u : nodes)
130 {
131 if(u.var == (v + 1) && u.reference_counter != 0)
132 {
133 out << " \\node[xshift=0cm, BDDnode, ";
134
135 if(previous == 0)
136 out << "right of=v" << var_table[v].label;
137 else
138 out << "right of=n" << previous;
139
140 out << "] (n" << u.node_number << ") {";
141 if(node_numbers)
142 out << "\\small $" << u.node_number << "$";
143 out << "};\n";
144 previous = u.node_number;
145 }
146 }
147
148 out << '\n';
149 }
150
151 out << '\n';
152
153 out << " % terminals\n";
154 out << " \\node[draw=black, style=rectangle, below of=v"
155 << var_table.back().label << ", xshift=1cm] (n1) {$1$};\n";
156
157 if(!suppress_zero)
158 out << " \\node[draw=black, style=rectangle, left of=n1] (n0) {$0$};\n";
159
160 out << '\n';
161
162 out << " % edges\n";
163 out << '\n';
164
165 for(const auto &u : nodes)
166 {
167 if(u.reference_counter != 0 && u.node_number >= 2)
168 {
169 if(!suppress_zero || u.low.node_number() != 0)
170 out << " \\draw[->,dashed] (n" << u.node_number << ") -> (n"
171 << u.low.node_number() << ");\n";
172
173 if(!suppress_zero || u.high.node_number() != 0)
174 out << " \\draw[->] (n" << u.node_number << ") -> (n"
175 << u.high.node_number() << ");\n";
176 }
177 }
178
179 out << '\n';
180
181 out << "\\end{tikzpicture}\n";
182}
183
185{
186public:
187 inline explicit mini_bdd_applyt(bool (*_fkt)(bool, bool)) : fkt(_fkt)
188 {
189 }
190
192 {
193 return APP_non_rec(x, y);
194 }
195
196protected:
198 mini_bddt APP_rec(const mini_bddt &x, const mini_bddt &y);
199 mini_bddt APP_non_rec(const mini_bddt &x, const mini_bddt &y);
200
201 typedef std::map<std::pair<unsigned, unsigned>, mini_bddt> Gt;
203};
204
206{
208 x.is_initialized() && y.is_initialized(),
209 "apply can only be called on initialized BDDs");
211 x.node->mgr == y.node->mgr,
212 "apply can only be called on BDDs with the same manager");
213
214 // dynamic programming
215 std::pair<unsigned, unsigned> key(x.node_number(), y.node_number());
216 Gt::const_iterator G_it = G.find(key);
217 if(G_it != G.end())
218 return G_it->second;
219
220 mini_bdd_mgrt *mgr = x.node->mgr;
221
222 mini_bddt u;
223
224 if(x.is_constant() && y.is_constant())
225 u = mini_bddt(fkt(x.is_true(), y.is_true()) ? mgr->True() : mgr->False());
226 else if(x.var() == y.var())
227 u =
228 mgr->mk(x.var(), APP_rec(x.low(), y.low()), APP_rec(x.high(), y.high()));
229 else if(x.var() < y.var())
230 u = mgr->mk(x.var(), APP_rec(x.low(), y), APP_rec(x.high(), y));
231 else /* x.var() > y.var() */
232 u = mgr->mk(y.var(), APP_rec(x, y.low()), APP_rec(x, y.high()));
233
234 G[key] = u;
235
236 return u;
237}
238
240{
241 struct stack_elementt
242 {
244 : result(_result),
245 x(_x),
246 y(_y),
247 key(x.node_number(), y.node_number()),
248 var(0),
249 phase(phaset::INIT)
250 {
251 }
252 mini_bddt &result, x, y, lr, hr;
253 std::pair<unsigned, unsigned> key;
254 unsigned var;
255 enum class phaset
256 {
257 INIT,
258 FINISH
259 } phase;
260 };
261
262 mini_bddt u; // return value
263
264 std::stack<stack_elementt> stack;
265 stack.push(stack_elementt(u, _x, _y));
266
267 while(!stack.empty())
268 {
269 auto &t = stack.top();
270 const mini_bddt &x = t.x;
271 const mini_bddt &y = t.y;
272
273 INVARIANT(
274 x.is_initialized() && y.is_initialized(),
275 "apply can only be called on initialized BDDs");
276 INVARIANT(
277 x.node->mgr == y.node->mgr,
278 "apply can only be called on BDDs with the same manager");
279
280 switch(t.phase)
281 {
282 case stack_elementt::phaset::INIT:
283 {
284 // dynamic programming
285 Gt::const_iterator G_it = G.find(t.key);
286 if(G_it != G.end())
287 {
288 t.result = G_it->second;
289 stack.pop();
290 }
291 else
292 {
293 if(x.is_constant() && y.is_constant())
294 {
295 bool result_truth = fkt(x.is_true(), y.is_true());
296 const mini_bdd_mgrt &mgr = *x.node->mgr;
297 t.result = result_truth ? mgr.True() : mgr.False();
298 stack.pop();
299 }
300 else if(x.var() == y.var())
301 {
302 t.var = x.var();
303 t.phase = stack_elementt::phaset::FINISH;
304
305 INVARIANT(
306 x.low().var() > t.var, "applying won't break variable order");
307 INVARIANT(
308 y.low().var() > t.var, "applying won't break variable order");
309 INVARIANT(
310 x.high().var() > t.var, "applying won't break variable order");
311 INVARIANT(
312 y.high().var() > t.var, "applying won't break variable order");
313
314 stack.push(stack_elementt(t.lr, x.low(), y.low()));
315 stack.push(stack_elementt(t.hr, x.high(), y.high()));
316 }
317 else if(x.var() < y.var())
318 {
319 t.var = x.var();
320 t.phase = stack_elementt::phaset::FINISH;
321
322 INVARIANT(
323 x.low().var() > t.var, "applying won't break variable order");
324 INVARIANT(
325 x.high().var() > t.var, "applying won't break variable order");
326
327 stack.push(stack_elementt(t.lr, x.low(), y));
328 stack.push(stack_elementt(t.hr, x.high(), y));
329 }
330 else /* x.var() > y.var() */
331 {
332 t.var = y.var();
333 t.phase = stack_elementt::phaset::FINISH;
334
335 INVARIANT(
336 y.low().var() > t.var, "applying won't break variable order");
337 INVARIANT(
338 y.high().var() > t.var, "applying won't break variable order");
339
340 stack.push(stack_elementt(t.lr, x, y.low()));
341 stack.push(stack_elementt(t.hr, x, y.high()));
342 }
343 }
344 }
345 break;
346
347 case stack_elementt::phaset::FINISH:
348 {
349 mini_bdd_mgrt *mgr = x.node->mgr;
350 t.result = mgr->mk(t.var, t.lr, t.hr);
351 G[t.key] = t.result;
352 stack.pop();
353 }
354 break;
355 }
356 }
357
359 u.is_initialized(), "the resulting BDD is initialized");
360
361 return u;
362}
363
364bool equal_fkt(bool x, bool y)
365{
366 return x == y;
367}
368
370{
371 return mini_bdd_applyt(equal_fkt)(*this, other);
372}
373
374bool xor_fkt(bool x, bool y)
375{
376 return x ^ y;
377}
378
380{
381 return mini_bdd_applyt(xor_fkt)(*this, other);
382}
383
385{
387 is_initialized(), "BDD has to be initialized for negation");
388 return node->mgr->True() ^ *this;
389}
390
391bool and_fkt(bool x, bool y)
392{
393 return x && y;
394}
395
397{
398 return mini_bdd_applyt(and_fkt)(*this, other);
399}
400
401bool or_fkt(bool x, bool y)
402{
403 return x || y;
404}
405
407{
408 return mini_bdd_applyt(or_fkt)(*this, other);
409}
410
412{
413 // add true/false nodes
414 nodes.push_back(mini_bdd_nodet(this, 0, 0, mini_bddt(), mini_bddt()));
415 false_bdd = mini_bddt(&nodes.back());
416 nodes.push_back(mini_bdd_nodet(this, 1, 1, mini_bddt(), mini_bddt()));
417 true_bdd = mini_bddt(&nodes.back());
418}
419
423
425mini_bdd_mgrt::mk(unsigned var, const mini_bddt &low, const mini_bddt &high)
426{
428 var <= var_table.size(), "cannot make a BDD for an unknown variable");
430 low.var() > var, "low-edge would break variable ordering");
431 // NOLINTNEXTLINE(build/deprecated)
433 high.var() > var, "high-edge would break variable ordering");
434
435 if(low.node_number() == high.node_number())
436 return low;
437 else
438 {
439 reverse_keyt reverse_key(var, low, high);
440 reverse_mapt::const_iterator it = reverse_map.find(reverse_key);
441
442 if(it != reverse_map.end())
443 return mini_bddt(it->second);
444 else
445 {
447
448 if(free.empty())
449 {
450 unsigned new_number = nodes.back().node_number + 1;
451 nodes.push_back(mini_bdd_nodet(this, var, new_number, low, high));
452 n = &nodes.back();
453 }
454 else // reuse a node
455 {
456 n = free.top();
457 free.pop();
458 n->var = var;
459 n->low = low;
460 n->high = high;
461 }
462
464 return mini_bddt(n);
465 }
466 }
467}
468
471{
472 const reverse_keyt &x = *this;
473
474 if(x.var < y.var)
475 return true;
476 else if(x.var > y.var)
477 return false;
478 else if(x.low < y.low)
479 return true;
480 else if(x.low > y.low)
481 return false;
482 else
483 return x.high < y.high;
484}
485
486void mini_bdd_mgrt::DumpTable(std::ostream &out) const
487{
488 out << "\\# & \\mathit{var} & \\mathit{low} &"
489 " \\mathit{high} \\\\\\hline\n";
490
491 for(const auto &n : nodes)
492 {
493 out << n.node_number << " & ";
494
495 if(n.node_number == 0 || n.node_number == 1)
496 out << n.var << " & & \\\\";
497 else if(n.reference_counter == 0)
498 out << "- & - & - \\\\";
499 else
500 out << n.var << "\\," << var_table[n.var - 1].label << " & "
501 << n.low.node_number() << " & " << n.high.node_number() << " \\\\";
502
503 if(n.node_number == 1)
504 out << "\\hline";
505
506 out << " % " << n.reference_counter << '\n';
507 }
508}
509
511{
512public:
513 inline restrictt(const unsigned _var, const bool _value)
514 : var(_var), value(_value)
515 {
516 }
517
519 {
520 return RES(u);
521 }
522
523protected:
524 const unsigned var;
525 const bool value;
526
527 mini_bddt RES(const mini_bddt &u);
528};
529
531{
532 // replace 'var' in 'u' by constant 'value'
533
535 u.is_initialized(),
536 "restricting variables can only be done in initialized BDDs");
537 mini_bdd_mgrt *mgr = u.node->mgr;
538
539 mini_bddt t;
540
541 if(u.var() > var)
542 t = u;
543 else if(u.var() < var)
544 t = mgr->mk(u.var(), RES(u.low()), RES(u.high()));
545 else // u.var()==var
546 t = RES(value ? u.high() : u.low());
547
548 return t;
549}
550
551mini_bddt restrict(const mini_bddt &u, unsigned var, const bool value)
552{
553 return restrictt(var, value)(u);
554}
555
556mini_bddt exists(const mini_bddt &u, const unsigned var)
557{
558 // u[var/0] OR u[var/1]
559 return restrict(u, var, false) | restrict(u, var, true);
560}
561
562mini_bddt substitute(const mini_bddt &t, unsigned var, const mini_bddt &tp)
563{
564 // t[var/tp] =
565 // ( tp &t[var/1]) |
566 // (!tp &t[var/0])
567
568 return (tp & restrict(t, var, true)) | ((!tp) & restrict(t, var, false));
569}
570
571void cubes(const mini_bddt &u, const std::string &path, std::string &result)
572{
573 if(u.is_false())
574 return;
575 else if(u.is_true())
576 {
577 result += path;
578 result += '\n';
579 return;
580 }
581
582 mini_bdd_mgrt *mgr = u.node->mgr;
583 std::string path_low = path;
584 std::string path_high = path;
585 if(!path.empty())
586 {
587 path_low += " & ";
588 path_high += " & ";
589 }
590 path_low += '!' + mgr->var_table[u.var() - 1].label;
591 path_high += mgr->var_table[u.var() - 1].label;
592 cubes(u.low(), path_low, result);
593 cubes(u.high(), path_high, result);
594}
595
596std::string cubes(const mini_bddt &u)
597{
598 if(u.is_false())
599 return "false\n";
600 else if(u.is_true())
601 return "true\n";
602 else
603 {
604 std::string result;
605 cubes(u, "", result);
606 return result;
607 }
608}
609
610bool OneSat(const mini_bddt &v, std::map<unsigned, bool> &assignment)
611{
612 // http://www.ecs.umass.edu/ece/labs/vlsicad/ece667/reading/somenzi99bdd.pdf
613 if(v.is_true())
614 return true;
615 else if(v.is_false())
616 return false;
617 else
618 {
619 assignment[v.var()] = true;
620 if(OneSat(v.high(), assignment))
621 return true;
622 assignment[v.var()] = false;
623 return OneSat(v.low(), assignment);
624 }
625}
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
Definition ai.h:562
bool(* fkt)(bool, bool)
Definition miniBDD.cpp:197
mini_bddt operator()(const mini_bddt &x, const mini_bddt &y)
Definition miniBDD.cpp:191
std::map< std::pair< unsigned, unsigned >, mini_bddt > Gt
Definition miniBDD.cpp:201
mini_bddt APP_non_rec(const mini_bddt &x, const mini_bddt &y)
Definition miniBDD.cpp:239
mini_bddt APP_rec(const mini_bddt &x, const mini_bddt &y)
Definition miniBDD.cpp:205
mini_bdd_applyt(bool(*_fkt)(bool, bool))
Definition miniBDD.cpp:187
mini_bddt false_bdd
Definition miniBDD.h:122
mini_bddt Var(const std::string &label)
Definition miniBDD.cpp:37
const mini_bddt & False() const
nodest nodes
Definition miniBDD.h:121
void DumpTable(std::ostream &out) const
Definition miniBDD.cpp:486
void DumpDot(std::ostream &out, bool supress_zero=false) const
Definition miniBDD.cpp:45
friend class mini_bdd_nodet
Definition miniBDD.h:103
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
reverse_mapt reverse_map
Definition miniBDD.h:134
var_tablet var_table
Definition miniBDD.h:117
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_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
const mini_bddt & low() 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
class mini_bdd_nodet * node
Definition miniBDD.h:64
mini_bddt operator==(const mini_bddt &) const
Definition miniBDD.cpp:369
const bool value
Definition miniBDD.cpp:525
restrictt(const unsigned _var, const bool _value)
Definition miniBDD.cpp:513
mini_bddt operator()(const mini_bddt &u)
Definition miniBDD.cpp:518
const unsigned var
Definition miniBDD.cpp:524
mini_bddt RES(const mini_bddt &u)
Definition miniBDD.cpp:530
bool and_fkt(bool x, bool y)
Definition miniBDD.cpp:391
bool equal_fkt(bool x, bool y)
Definition miniBDD.cpp:364
bool xor_fkt(bool x, bool y)
Definition miniBDD.cpp:374
bool or_fkt(bool x, bool y)
Definition miniBDD.cpp:401
A minimalistic BDD library, following Bryant's original paper and Andersen's lecture notes.
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
#define PRECONDITION_WITH_DIAGNOSTICS(CONDITION,...)
Definition invariant.h:464
#define INVARIANT(CONDITION, REASON)
This macro uses the wrapper function 'invariant_violated_string'.
Definition invariant.h:423
#define POSTCONDITION_WITH_DIAGNOSTICS(CONDITION,...)
Definition invariant.h:480
bool operator<(const reverse_keyt &) const
Definition miniBDD.cpp:470