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