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 <cassert>
17 
18 #include <iostream>
19 
20 #define forall_nodes(it) for(nodest::const_iterator it=nodes.begin(); \
21  it!=nodes.end(); it++)
22 
24 {
25  // NOLINTNEXTLINE(build/deprecated)
26  assert(reference_counter!=0);
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 {
212  // NOLINTNEXTLINE(build/deprecated)
213  assert(x.is_initialized() && y.is_initialized());
214  // NOLINTNEXTLINE(build/deprecated)
215  assert(x.node->mgr==y.node->mgr);
216 
217  // dynamic programming
218  std::pair<unsigned, unsigned> key(x.node_number(), y.node_number());
219  Gt::const_iterator G_it=G.find(key);
220  if(G_it!=G.end())
221  return G_it->second;
222 
224 
225  mini_bddt u;
226 
227  if(x.is_constant() && y.is_constant())
228  u=mini_bddt(fkt(x.is_true(), y.is_true())?mgr->True():mgr->False());
229  else if(x.var()==y.var())
230  u=mgr->mk(x.var(),
231  APP_rec(x.low(), y.low()),
232  APP_rec(x.high(), y.high()));
233  else if(x.var()<y.var())
234  u=mgr->mk(x.var(),
235  APP_rec(x.low(), y),
236  APP_rec(x.high(), y));
237  else /* x.var() > y.var() */
238  u=mgr->mk(y.var(),
239  APP_rec(x, y.low()),
240  APP_rec(x, y.high()));
241 
242  G[key]=u;
243 
244  return u;
245 }
246 
248  const mini_bddt &_x,
249  const mini_bddt &_y)
250 {
251  struct stack_elementt
252  {
253  stack_elementt(
254  mini_bddt &_result,
255  const mini_bddt &_x,
256  const mini_bddt &_y):
257  result(_result), x(_x), y(_y),
258  key(x.node_number(), y.node_number()),
259  var(0), phase(phaset::INIT) { }
260  mini_bddt &result, x, y, lr, hr;
261  std::pair<unsigned, unsigned> key;
262  unsigned var;
263  enum class phaset { INIT, FINISH } phase;
264  };
265 
266  mini_bddt u; // return value
267 
268  std::stack<stack_elementt> stack;
269  stack.push(stack_elementt(u, _x, _y));
270 
271  while(!stack.empty())
272  {
273  auto &t=stack.top();
274  const mini_bddt &x=t.x;
275  const mini_bddt &y=t.y;
276  // NOLINTNEXTLINE(build/deprecated)
277  assert(x.is_initialized() && y.is_initialized());
278  // NOLINTNEXTLINE(build/deprecated)
279  assert(x.node->mgr==y.node->mgr);
280 
281  switch(t.phase)
282  {
283  case stack_elementt::phaset::INIT:
284  {
285  // dynamic programming
286  Gt::const_iterator G_it=G.find(t.key);
287  if(G_it!=G.end())
288  {
289  t.result=G_it->second;
290  stack.pop();
291  }
292  else
293  {
294  if(x.is_constant() && y.is_constant())
295  {
296  bool result_truth=fkt(x.is_true(), y.is_true());
297  const mini_bdd_mgrt &mgr=*x.node->mgr;
298  t.result=result_truth?mgr.True():mgr.False();
299  stack.pop();
300  }
301  else if(x.var()==y.var())
302  {
303  t.var=x.var();
304  t.phase=stack_elementt::phaset::FINISH;
305  // NOLINTNEXTLINE(build/deprecated)
306  assert(x.low().var()>t.var);
307  // NOLINTNEXTLINE(build/deprecated)
308  assert(y.low().var()>t.var);
309  // NOLINTNEXTLINE(build/deprecated)
310  assert(x.high().var()>t.var);
311  // NOLINTNEXTLINE(build/deprecated)
312  assert(y.high().var()>t.var);
313  stack.push(stack_elementt(t.lr, x.low(), y.low()));
314  stack.push(stack_elementt(t.hr, x.high(), y.high()));
315  }
316  else if(x.var()<y.var())
317  {
318  t.var=x.var();
319  t.phase=stack_elementt::phaset::FINISH;
320  // NOLINTNEXTLINE(build/deprecated)
321  assert(x.low().var()>t.var);
322  // NOLINTNEXTLINE(build/deprecated)
323  assert(x.high().var()>t.var);
324  stack.push(stack_elementt(t.lr, x.low(), y));
325  stack.push(stack_elementt(t.hr, x.high(), y));
326  }
327  else /* x.var() > y.var() */
328  {
329  t.var=y.var();
330  t.phase=stack_elementt::phaset::FINISH;
331  // NOLINTNEXTLINE(build/deprecated)
332  assert(y.low().var()>t.var);
333  // NOLINTNEXTLINE(build/deprecated)
334  assert(y.high().var()>t.var);
335  stack.push(stack_elementt(t.lr, x, y.low()));
336  stack.push(stack_elementt(t.hr, x, y.high()));
337  }
338  }
339  }
340  break;
341 
342  case stack_elementt::phaset::FINISH:
343  {
345  t.result=mgr->mk(t.var, t.lr, t.hr);
346  G[t.key]=t.result;
347  stack.pop();
348  }
349  break;
350  }
351  }
352 
353  // NOLINTNEXTLINE(build/deprecated)
354  assert(u.is_initialized());
355 
356  return u;
357 }
358 
359 bool equal_fkt(bool x, bool y)
360 {
361  return x==y;
362 }
363 
365 {
366  return mini_bdd_applyt(equal_fkt)(*this, other);
367 }
368 
369 bool xor_fkt(bool x, bool y)
370 {
371  return x^y;
372 }
373 
375 {
376  return mini_bdd_applyt(xor_fkt)(*this, other);
377 }
378 
380 {
381  // NOLINTNEXTLINE(build/deprecated)
382  assert(is_initialized());
383  return node->mgr->True()^*this;
384 }
385 
386 bool and_fkt(bool x, bool y)
387 {
388  return x && y;
389 }
390 
391 mini_bddt mini_bddt::operator&(const mini_bddt &other) const
392 {
393  return mini_bdd_applyt(and_fkt)(*this, other);
394 }
395 
396 bool or_fkt(bool x, bool y)
397 {
398  return x || y;
399 }
400 
402 {
403  return mini_bdd_applyt(or_fkt)(*this, other);
404 }
405 
407 {
408  // add true/false nodes
409  nodes.push_back(mini_bdd_nodet(this, 0, 0, mini_bddt(), mini_bddt()));
410  false_bdd=mini_bddt(&nodes.back());
411  nodes.push_back(mini_bdd_nodet(this, 1, 1, mini_bddt(), mini_bddt()));
412  true_bdd=mini_bddt(&nodes.back());
413 }
414 
416 {
417 }
418 
420  unsigned var,
421  const mini_bddt &low,
422  const mini_bddt &high)
423 {
424  // NOLINTNEXTLINE(build/deprecated)
425  assert(var<=var_table.size());
426  // NOLINTNEXTLINE(build/deprecated)
427  assert(low.var()>var);
428  // NOLINTNEXTLINE(build/deprecated)
429  assert(high.var()>var);
430 
431  if(low.node_number()==high.node_number())
432  return low;
433  else
434  {
435  reverse_keyt reverse_key(var, low, high);
436  reverse_mapt::const_iterator it=reverse_map.find(reverse_key);
437 
438  if(it!=reverse_map.end())
439  return mini_bddt(it->second);
440  else
441  {
442  mini_bdd_nodet *n;
443 
444  if(free.empty())
445  {
446  unsigned new_number=nodes.back().node_number+1;
447  nodes.push_back(mini_bdd_nodet(this, var, new_number, low, high));
448  n=&nodes.back();
449  }
450  else // reuse a node
451  {
452  n=free.top();
453  free.pop();
454  n->var=var;
455  n->low=low;
456  n->high=high;
457  }
458 
459  reverse_map[reverse_key]=n;
460  return mini_bddt(n);
461  }
462  }
463 }
464 
466  const mini_bdd_mgrt::reverse_keyt &y) const
467 {
468  const reverse_keyt &x=*this;
469 
470  if(x.var<y.var)
471  return true;
472  else if(x.var>y.var)
473  return false;
474  else if(x.low<y.low)
475  return true;
476  else if(x.low>y.low)
477  return false;
478  else
479  return x.high<y.high;
480 }
481 
482 void mini_bdd_mgrt::DumpTable(std::ostream &out) const
483 {
484  out << "\\# & \\mathit{var} & \\mathit{low} &"
485  " \\mathit{high} \\\\\\hline\n";
486 
487  forall_nodes(it)
488  {
489  out << it->node_number << " & ";
490 
491  if(it->node_number==0 || it->node_number==1)
492  out << it->var << " & & \\\\";
493  else if(it->reference_counter==0)
494  out << "- & - & - \\\\";
495  else
496  out << it->var << "\\," << var_table[it->var-1].label << " & "
497  << it->low.node_number() << " & " << it->high.node_number()
498  << " \\\\";
499 
500  if(it->node_number==1)
501  out << "\\hline";
502 
503  out << " % " << it->reference_counter << '\n';
504  }
505 }
506 
508 {
509 public:
510  inline restrictt(const unsigned _var, const bool _value):
511  var(_var), value(_value)
512  {
513  }
514 
515  mini_bddt operator()(const mini_bddt &u) { return RES(u); }
516 
517 protected:
518  const unsigned var;
519  const bool value;
520 
521  mini_bddt RES(const mini_bddt &u);
522 };
523 
525 {
526  // replace 'var' in 'u' by constant 'value'
527 
528  // NOLINTNEXTLINE(build/deprecated)
529  assert(u.is_initialized());
531 
532  mini_bddt t;
533 
534  if(u.var()>var)
535  t=u;
536  else if(u.var()<var)
537  t=mgr->mk(u.var(), RES(u.low()), RES(u.high()));
538  else // u.var()==var
539  t=RES(value?u.high():u.low());
540 
541  return t;
542 }
543 
544 mini_bddt restrict(const mini_bddt &u, unsigned var, const bool value)
545 {
546  return restrictt(var, value)(u);
547 }
548 
549 mini_bddt exists(const mini_bddt &u, const unsigned var)
550 {
551  // u[var/0] OR u[var/1]
552  return restrict(u, var, false) |
553  restrict(u, var, true);
554 }
555 
556 mini_bddt substitute(const mini_bddt &t, unsigned var, const mini_bddt &tp)
557 {
558  // t[var/tp] =
559  // ( tp &t[var/1]) |
560  // (!tp &t[var/0])
561 
562  return ( tp &restrict(t, var, true)) |
563  ((!tp) &restrict(t, var, false));
564 }
565 
566 void cubes(const mini_bddt &u, const std::string &path, std::string &result)
567 {
568  if(u.is_false())
569  return;
570  else if(u.is_true())
571  {
572  result+=path;
573  result+='\n';
574  return;
575  }
576 
578  std::string path_low=path;
579  std::string path_high=path;
580  if(!path.empty())
581  {
582  path_low+=" & ";
583  path_high+=" & ";
584  }
585  path_low+='!'+mgr->var_table[u.var()-1].label;
586  path_high+=mgr->var_table[u.var()-1].label;
587  cubes(u.low(), path_low, result);
588  cubes(u.high(), path_high, result);
589 }
590 
591 std::string cubes(const mini_bddt &u)
592 {
593  if(u.is_false())
594  return "false\n";
595  else if(u.is_true())
596  return "true\n";
597  else
598  {
599  std::string result;
600  cubes(u, "", result);
601  return result;
602  }
603 }
604 
605 bool OneSat(const mini_bddt &v, std::map<unsigned, bool> &assignment)
606 {
607  // http://www.ecs.umass.edu/ece/labs/vlsicad/ece667/reading/somenzi99bdd.pdf
608  if(v.is_true())
609  return true;
610  else if(v.is_false())
611  return false;
612  else
613  {
614  assignment[v.var()]=true;
615  if(OneSat(v.high(), assignment))
616  return true;
617  assignment[v.var()]=false;
618  return OneSat(v.low(), assignment);
619  }
620 }
void clear()
freet free
Definition: miniBDD.h:134
bool or_fkt(bool x, bool y)
Definition: miniBDD.cpp:396
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
unsigned var() const
const mini_bddt & False() const
unsigned node_number() const
mini_bddt operator()(const mini_bddt &x, const mini_bddt &y)
Definition: miniBDD.cpp:196
const bool value
Definition: miniBDD.cpp:519
bool equal_fkt(bool x, bool y)
Definition: miniBDD.cpp:359
void free(void *)
mini_bddt operator!() const
Definition: miniBDD.cpp:379
bool is_initialized() const
Definition: miniBDD.h:58
void cubes(const mini_bddt &u, const std::string &path, std::string &result)
Definition: miniBDD.cpp:566
mini_bddt low
Definition: miniBDD.h:70
mini_bddt exists(const mini_bddt &u, const unsigned var)
Definition: miniBDD.cpp:549
mini_bddt substitute(const mini_bddt &t, unsigned var, const mini_bddt &tp)
Definition: miniBDD.cpp:556
unsigned node_number
Definition: miniBDD.h:69
void remove_reference()
Definition: miniBDD.cpp:23
mini_bdd_nodet(class mini_bdd_mgrt *_mgr, unsigned _var, unsigned _node_number, const mini_bddt &_low, const mini_bddt &_high)
bool is_false() const
const unsigned var
Definition: miniBDD.cpp:518
class mini_bdd_nodet * node
Definition: miniBDD.h:62
bool xor_fkt(bool x, bool y)
Definition: miniBDD.cpp:369
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:364
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:374
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:386
mini_bddt operator()(const mini_bddt &u)
Definition: miniBDD.cpp:515
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:419
mini_bddt APP_non_rec(const mini_bddt &x, const mini_bddt &y)
Definition: miniBDD.cpp:247
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:482
const mini_bddt & low() const
class mini_bdd_mgrt * mgr
Definition: miniBDD.h:68
mini_bddt operator|(const mini_bddt &) const
Definition: miniBDD.cpp:401
restrictt(const unsigned _var, const bool _value)
Definition: miniBDD.cpp:510
std::map< std::pair< unsigned, unsigned >, mini_bddt > Gt
Definition: miniBDD.cpp:206
bool operator<(const reverse_keyt &) const
Definition: miniBDD.cpp:465
bool is_true() const
mini_bddt RES(const mini_bddt &u)
Definition: miniBDD.cpp:524
bool OneSat(const mini_bddt &v, std::map< unsigned, bool > &assignment)
Definition: miniBDD.cpp:605
#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:544