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