TdZdd  1.1
A top-down/breadth-first decision diagram manipulation framework
DdBuilder.hpp
1 /*
2  * TdZdd: a Top-down/Breadth-first Decision Diagram Manipulation Framework
3  * by Hiroaki Iwashita <iwashita@erato.ist.hokudai.ac.jp>
4  * Copyright (c) 2014 ERATO MINATO Project
5  *
6  * Permission is hereby granted, free of charge, to any person obtaining a
7  * copy of this software and associated documentation files (the "Software"),
8  * to deal in the Software without restriction, including without limitation
9  * the rights to use, copy, modify, merge, publish, distribute, sublicense,
10  * and/or sell copies of the Software, and to permit persons to whom the
11  * Software is furnished to do so, subject to the following conditions:
12  *
13  * The above copyright notice and this permission notice shall be included in
14  * all copies or substantial portions of the Software.
15  *
16  * THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR
17  * IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY,
18  * FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE
19  * AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER
20  * LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING
21  * FROM, OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER
22  * DEALINGS IN THE SOFTWARE.
23  */
24 
25 #pragma once
26 
27 #include <cassert>
28 #include <cmath>
29 #include <ostream>
30 #include <stdexcept>
31 
32 #ifdef _OPENMP
33 #include <omp.h>
34 #endif
35 
36 #include "DdSweeper.hpp"
37 #include "Node.hpp"
38 #include "NodeTable.hpp"
39 #include "../DdSpec.hpp"
40 #include "../util/MemoryPool.hpp"
41 #include "../util/MessageHandler.hpp"
42 #include "../util/MyHashTable.hpp"
43 #include "../util/MyList.hpp"
44 #include "../util/MyVector.hpp"
45 
46 namespace tdzdd {
47 
48 class DdBuilderBase {
49 protected:
50  static int const headerSize = 1;
51 
52  /* SpecNode
53  * ┌────────┬────────┬────────┬─────
54  * │ srcPtr │state[0]│state[1]│ ...
55  * │ nodeId │ │ │
56  * └────────┴────────┴────────┴─────
57  */
58  union SpecNode {
59  NodeId* srcPtr;
60  int64_t code;
61  };
62 
63  static NodeId*& srcPtr(SpecNode* p) {
64  return p[0].srcPtr;
65  }
66 
67  static int64_t& code(SpecNode* p) {
68  return p[0].code;
69  }
70 
71  static NodeId& nodeId(SpecNode* p) {
72  return *reinterpret_cast<NodeId*>(&p[0].code);
73  }
74 
75  static void* state(SpecNode* p) {
76  return p + headerSize;
77  }
78 
79  static void const* state(SpecNode const* p) {
80  return p + headerSize;
81  }
82 
83  static int getSpecNodeSize(int n) {
84  if (n < 0)
85  throw std::runtime_error("storage size is not initialized!!!");
86  return headerSize + (n + sizeof(SpecNode) - 1) / sizeof(SpecNode);
87  }
88 
89  template<typename SPEC>
90  struct Hasher {
91  SPEC const& spec;
92  int const level;
93 
94  Hasher(SPEC const& spec, int level) :
95  spec(spec), level(level) {
96  }
97 
98  size_t operator()(SpecNode const* p) const {
99  return spec.hash_code(state(p), level);
100  }
101 
102  size_t operator()(SpecNode const* p, SpecNode const* q) const {
103  return spec.equal_to(state(p), state(q), level);
104  }
105  };
106 };
107 
108 class DdBuilderMPBase {
109 protected:
110  static int const headerSize = 2;
111 
112  /* SpecNode
113  * ┌────────┬────────┬────────┬────────┬─────
114  * │ srcPtr │ nodeId │state[0]│state[1]│ ...
115  * └────────┴────────┴────────┴────────┴─────
116  */
117  union SpecNode {
118  NodeId* srcPtr;
119  int64_t code;
120  };
121 
122  static NodeId*& srcPtr(SpecNode* p) {
123  return p[0].srcPtr;
124  }
125 
126  static int64_t& code(SpecNode* p) {
127  return p[1].code;
128  }
129 
130  static NodeId& nodeId(SpecNode* p) {
131  return *reinterpret_cast<NodeId*>(&p[1].code);
132  }
133 
134  static NodeId nodeId(SpecNode const* p) {
135  return *reinterpret_cast<NodeId const*>(&p[1].code);
136  }
137 
138  static void* state(SpecNode* p) {
139  return p + headerSize;
140  }
141 
142  static void const* state(SpecNode const* p) {
143  return p + headerSize;
144  }
145 
146  static int getSpecNodeSize(int n) {
147  if (n < 0)
148  throw std::runtime_error("storage size is not initialized!!!");
149  return headerSize + (n + sizeof(SpecNode) - 1) / sizeof(SpecNode);
150  }
151 
152  template<typename SPEC>
153  struct Hasher {
154  SPEC const& spec;
155  int const level;
156 
157  Hasher(SPEC const& spec, int level) :
158  spec(spec), level(level) {
159  }
160 
161  size_t operator()(SpecNode const* p) const {
162  return spec.hash_code(state(p), level);
163  }
164 
165  size_t operator()(SpecNode const* p, SpecNode const* q) const {
166  return spec.equal_to(state(p), state(q), level);
167  }
168  };
169 };
170 
174 template<typename S>
175 class DdBuilder: DdBuilderBase {
176  typedef S Spec;
177  typedef MyHashTable<SpecNode*,Hasher<Spec>,Hasher<Spec> > UniqTable;
178  static int const AR = Spec::ARITY;
179 
180  Spec spec;
181  int const specNodeSize;
182  NodeTableEntity<AR>& output;
183  DdSweeper<AR> sweeper;
184 
185  MyVector<MyList<SpecNode> > snodeTable;
186 
187  MyVector<char> oneStorage;
188  void* const one;
189  MyVector<NodeBranchId> oneSrcPtr;
190 
191  void init(int n) {
192  snodeTable.resize(n + 1);
193  if (n >= output.numRows()) output.setNumRows(n + 1);
194  oneSrcPtr.clear();
195  }
196 
197 public:
198  DdBuilder(Spec const& spec, NodeTableHandler<AR>& output, int n = 0) :
199  spec(spec),
200  specNodeSize(getSpecNodeSize(spec.datasize())),
201  output(output.privateEntity()),
202  sweeper(this->output, oneSrcPtr),
203  oneStorage(spec.datasize()),
204  one(oneStorage.data()) {
205  if (n >= 1) init(n);
206  }
207 
208  ~DdBuilder() {
209  if (!oneSrcPtr.empty()) {
210  spec.destruct(one);
211  oneSrcPtr.clear();
212  }
213  }
214 
221  void schedule(NodeId* fp, int level, void* s) {
222  SpecNode* p0 = snodeTable[level].alloc_front(specNodeSize);
223  spec.get_copy(state(p0), s);
224  srcPtr(p0) = fp;
225  }
226 
231  int initialize(NodeId& root) {
232  sweeper.setRoot(root);
233  MyVector<char> tmp(spec.datasize());
234  void* const tmpState = tmp.data();
235  int n = spec.get_root(tmpState);
236 
237  if (n <= 0) {
238  root = n ? 1 : 0;
239  n = 0;
240  }
241  else {
242  init(n);
243  schedule(&root, n, tmpState);
244  }
245 
246  spec.destruct(tmpState);
247  if (!oneSrcPtr.empty()) {
248  spec.destruct(one);
249  oneSrcPtr.clear();
250  }
251  return n;
252  }
253 
258  void construct(int i) {
259  assert(0 < i && size_t(i) < snodeTable.size());
260 
261  MyList<SpecNode> &snodes = snodeTable[i];
262  size_t j0 = output[i].size();
263  size_t m = j0;
264  int lowestChild = i - 1;
265  size_t deadCount = 0;
266 
267  {
268  Hasher<Spec> hasher(spec, i);
269  UniqTable uniq(snodes.size() * 2, hasher, hasher);
270 
271  for (MyList<SpecNode>::iterator t = snodes.begin();
272  t != snodes.end(); ++t) {
273  SpecNode* p = *t;
274  SpecNode*& p0 = uniq.add(p);
275 
276  if (p0 == p) {
277  nodeId(p) = *srcPtr(p) = NodeId(i, m++);
278  }
279  else {
280  switch (spec.merge_states(state(p0), state(p))) {
281  case 1:
282  nodeId(p0) = 0; // forward to 0-terminal
283  nodeId(p) = *srcPtr(p) = NodeId(i, m++);
284  p0 = p;
285  break;
286  case 2:
287  *srcPtr(p) = 0;
288  nodeId(p) = 1; // unused
289  break;
290  default:
291  *srcPtr(p) = nodeId(p0);
292  nodeId(p) = 1; // unused
293  break;
294  }
295  }
296  }
297 //#ifdef DEBUG
298 // MessageHandler mh;
299 // mh << "table_size[" << i << "] = " << uniq.tableSize() << "\n";
300 //#endif
301  }
302 
303  output[i].resize(m);
304  Node<AR>* const outi = output[i].data();
305  size_t jj = j0;
306  SpecNode* pp = snodeTable[i - 1].alloc_front(specNodeSize);
307 
308  for (; !snodes.empty(); snodes.pop_front()) {
309  SpecNode* p = snodes.front();
310  Node<AR>& q = outi[jj];
311 
312  if (nodeId(p) == 1) {
313  spec.destruct(state(p));
314  continue;
315  }
316 
317  bool allZero = true;
318 
319  for (int b = 0; b < AR; ++b) {
320  if (nodeId(p) == 0) {
321  q.branch[b] = 0;
322  continue;
323  }
324 
325  spec.get_copy(state(pp), state(p));
326  int ii = spec.get_child(state(pp), i, b);
327 
328  if (ii == 0) {
329  q.branch[b] = 0;
330  spec.destruct(state(pp));
331  }
332  else if (ii < 0) {
333  if (oneSrcPtr.empty()) { // the first 1-terminal candidate
334  spec.get_copy(one, state(pp));
335  q.branch[b] = 1;
336  oneSrcPtr.push_back(NodeBranchId(i, jj, b));
337  }
338  else {
339  switch (spec.merge_states(one, state(pp))) {
340  case 1:
341  while (!oneSrcPtr.empty()) {
342  NodeBranchId const& nbi = oneSrcPtr.back();
343  assert(nbi.row >= i);
344  output[nbi.row][nbi.col].branch[nbi.val] = 0;
345  oneSrcPtr.pop_back();
346  }
347  spec.destruct(one);
348  spec.get_copy(one, state(pp));
349  q.branch[b] = 1;
350  oneSrcPtr.push_back(NodeBranchId(i, jj, b));
351  break;
352  case 2:
353  q.branch[b] = 0;
354  break;
355  default:
356  q.branch[b] = 1;
357  oneSrcPtr.push_back(NodeBranchId(i, jj, b));
358  break;
359  }
360  }
361  spec.destruct(state(pp));
362  allZero = false;
363  }
364  else if (ii == i - 1) {
365  srcPtr(pp) = &q.branch[b];
366  pp = snodeTable[ii].alloc_front(specNodeSize);
367  allZero = false;
368  }
369  else {
370  assert(ii < i - 1);
371  SpecNode* ppp = snodeTable[ii].alloc_front(specNodeSize);
372  spec.get_copy(state(ppp), state(pp));
373  spec.destruct(state(pp));
374  srcPtr(ppp) = &q.branch[b];
375  if (ii < lowestChild) lowestChild = ii;
376  allZero = false;
377  }
378  }
379 
380  spec.destruct(state(p));
381  ++jj;
382  if (allZero) ++deadCount;
383  }
384 
385  snodeTable[i - 1].pop_front();
386  spec.destructLevel(i);
387  sweeper.update(i, lowestChild, deadCount);
388  }
389 };
390 
394 template<typename S>
395 class DdBuilderMP: DdBuilderMPBase {//TODO oneStorage
396  typedef S Spec;
397  typedef MyHashTable<SpecNode*,Hasher<Spec>,Hasher<Spec> > UniqTable;
398  static int const AR = Spec::ARITY;
399  static int const TASKS_PER_THREAD = 10;
400 
401  int const threads;
402  int const tasks;
403 
404  MyVector<Spec> specs;
405  int const specNodeSize;
406  NodeTableEntity<AR>& output;
407  DdSweeper<AR> sweeper;
408 
409  MyVector<MyVector<MyVector<MyList<SpecNode> > > > snodeTables;
410 
411 #ifdef DEBUG
412  ElapsedTimeCounter etcP1, etcP2, etcS1;
413 #endif
414 
415  void init(int n) {
416  for (int y = 0; y < threads; ++y) {
417  snodeTables[y].resize(tasks);
418  for (int x = 0; x < tasks; ++x) {
419  snodeTables[y][x].resize(n + 1);
420  }
421  }
422  if (n >= output.numRows()) output.setNumRows(n + 1);
423  }
424 
425 public:
426  DdBuilderMP(Spec const& s, NodeTableHandler<AR>& output, int n = 0) :
427 #ifdef _OPENMP
428  threads(omp_get_max_threads()),
429  tasks(MyHashConstant::primeSize(TASKS_PER_THREAD * threads)),
430 #else
431  threads(1),
432  tasks(1),
433 #endif
434  specs(threads, s),
435  specNodeSize(getSpecNodeSize(s.datasize())),
436  output(output.privateEntity()),
437  sweeper(this->output),
438  snodeTables(threads) {
439  if (n >= 1) init(n);
440 #ifdef DEBUG
441  MessageHandler mh;
442  mh << "#thread = " << threads << ", #task = " << tasks;
443 #endif
444  }
445 
446 #ifdef DEBUG
447  ~DdBuilderMP() {
448  MessageHandler mh;
449  mh << "P1: " << etcP1 << "\n";
450  mh << "P2: " << etcP2 << "\n";
451  mh << "S1: " << etcS1 << "\n";
452  }
453 #endif
454 
461  void schedule(NodeId* fp, int level, void* s) {
462  SpecNode* p0 = snodeTables[0][0][level].alloc_front(specNodeSize);
463  specs[0].get_copy(state(p0), s);
464  srcPtr(p0) = fp;
465  }
466 
471  int initialize(NodeId& root) {
472  sweeper.setRoot(root);
473  MyVector<char> tmp(specs[0].datasize());
474  void* const tmpState = tmp.data();
475  int n = specs[0].get_root(tmpState);
476 
477  if (n <= 0) {
478  root = n ? 1 : 0;
479  n = 0;
480  }
481  else {
482  init(n);
483  schedule(&root, n, tmpState);
484  }
485 
486  specs[0].destruct(tmpState);
487  return n;
488  }
489 
494  void construct(int i) {
495  assert(0 < i && i < output.numRows());
496  assert(output.numRows() - snodeTables[0][0].size() == 0);
497 
498  MyVector<size_t> nodeColumn(tasks);
499  int lowestChild = i - 1;
500  size_t deadCount = 0;
501 
502 #ifdef DEBUG
503  etcP1.start();
504 #endif
505 
506 #ifdef _OPENMP
507  // OpenMP 2.0 does not support reduction(min:lowestChild)
508 #pragma omp parallel reduction(+:deadCount)
509 #endif
510  {
511 #ifdef _OPENMP
512  int yy = omp_get_thread_num();
513  //CPUAffinity().bind(yy);
514 #else
515  int yy = 0;
516 #endif
517 
518  Spec& spec = specs[yy];
519  MyVector<char> tmp(spec.datasize());
520  void* const tmpState = tmp.data();
521  Hasher<Spec> hasher(spec, i);
522  UniqTable uniq(hasher, hasher);
523  int lc = lowestChild;
524 
525 #ifdef _OPENMP
526 #pragma omp for schedule(dynamic)
527 #endif
528  for (int x = 0; x < tasks; ++x) {
529  size_t m = 0;
530  for (int y = 0; y < threads; ++y) {
531  m += snodeTables[y][x][i].size();
532  }
533  if (m == 0) continue;
534 
535  uniq.initialize(m * 2);
536  size_t j = 0;
537 
538  for (int y = 0; y < threads; ++y) {
539  MyList<SpecNode> &snodes = snodeTables[y][x][i];
540 
541  for (MyList<SpecNode>::iterator t = snodes.begin();
542  t != snodes.end(); ++t) {
543  SpecNode* p = *t;
544  SpecNode*& p0 = uniq.add(p);
545 
546  if (p0 == p) {
547  code(p) = ++j; // code(p) >= 1
548  }
549  else {
550  switch (spec.merge_states(state(p0), state(p))) {
551  case 1:
552  code(p0) = 0;
553  code(p) = ++j; // code(p) >= 1
554  p0 = p;
555  break;
556  case 2:
557  code(p) = 0;
558  break;
559  default:
560  code(p) = -code(p0);
561  break;
562  }
563  }
564  }
565  }
566 
567  nodeColumn[x] = j;
568 //#ifdef DEBUG
569 // MessageHandler mh;
570 //#ifdef _OPENMP
571 //#pragma omp critical
572 //#endif
573 // mh << "table_size[" << i << "][" << x << "] = " << uniq.tableSize() << "\n";
574 //#endif
575  }
576 
577 #ifdef _OPENMP
578 #pragma omp single
579 #endif
580  {
581 #ifdef DEBUG
582  etcP1.stop();
583  etcS1.start();
584 #endif
585  size_t m = output[i].size();
586  for (int x = 0; x < tasks; ++x) {
587  size_t j = nodeColumn[x];
588  nodeColumn[x] = (j >= 1) ? m : -1; // -1 for skip
589  m += j;
590  }
591 
592  output.initRow(i, m);
593 #ifdef DEBUG
594  etcS1.stop();
595  etcP2.start();
596 #endif
597  }
598 
599 #ifdef _OPENMP
600 #pragma omp for schedule(dynamic)
601 #endif
602  for (int x = 0; x < tasks; ++x) {
603  if (nodeColumn[x] < 0) continue; // -1 for skip
604  size_t j0 = nodeColumn[x] - 1; // code(p) >= 1
605 
606  for (int y = 0; y < threads; ++y) {
607  MyList<SpecNode> &snodes = snodeTables[y][x][i];
608 
609  for (; !snodes.empty(); snodes.pop_front()) {
610  SpecNode* p = snodes.front();
611 
612  if (code(p) <= 0) {
613  *srcPtr(p) = code(p) ? NodeId(i, j0 - code(p)) : 0;
614  spec.destruct(state(p));
615  continue;
616  }
617 
618  size_t j = j0 + code(p);
619  *srcPtr(p) = NodeId(i, j);
620 
621  Node<AR> &q = output[i][j];
622  bool allZero = true;
623  void* s = tmpState;
624 
625  for (int b = 0; b < AR; ++b) {
626  if (b < AR - 1) {
627  spec.get_copy(s, state(p));
628  }
629  else {
630  s = state(p);
631  }
632 
633  int ii = spec.get_child(s, i, b);
634 
635  if (ii <= 0) {
636  q.branch[b] = ii ? 1 : 0;
637  if (ii) allZero = false;
638  }
639  else {
640  assert(ii <= i - 1);
641  int xx = spec.hash_code(s, ii) % tasks;
642  SpecNode* pp =
643  snodeTables[yy][xx][ii].alloc_front(
644  specNodeSize);
645  spec.get_copy(state(pp), s);
646  srcPtr(pp) = &q.branch[b];
647  if (ii < lc) lc = ii;
648  allZero = false;
649  }
650 
651  spec.destruct(s);
652  }
653 
654  if (allZero) ++deadCount;
655  }
656  }
657  }
658 
659  spec.destructLevel(i);
660 
661 #ifdef _OPENMP
662 #pragma omp critical
663 #endif
664  if (lc < lowestChild) lowestChild = lc;
665  }
666 
667  sweeper.update(i, lowestChild, deadCount);
668 #ifdef DEBUG
669  etcP2.stop();
670 #endif
671  }
672 };
673 
677 template<typename S>
678 class ZddSubsetter: DdBuilderBase {
679 //typedef typename std::remove_const<typename std::remove_reference<S>::type>::type Spec;
680  typedef S Spec;
681  typedef MyHashTable<SpecNode*,Hasher<Spec>,Hasher<Spec> > UniqTable;
682  static int const AR = Spec::ARITY;
683 
684  Spec spec;
685  int const specNodeSize;
686  NodeTableEntity<AR> const& input;
687  NodeTableEntity<AR>& output;
688  DataTable<MyListOnPool<SpecNode> > work;
689  DdSweeper<AR> sweeper;
690 
691  MyVector<char> oneStorage;
692  void* const one;
693  MyVector<NodeBranchId> oneSrcPtr;
694 
695  MemoryPools pools;
696 
697 public:
698  ZddSubsetter(NodeTableHandler<AR> const& input, Spec const& s,
699  NodeTableHandler<AR>& output) :
700  spec(s),
701  specNodeSize(getSpecNodeSize(spec.datasize())),
702  input(*input),
703  output(output.privateEntity()),
704  work(input->numRows()),
705  sweeper(this->output, oneSrcPtr),
706  oneStorage(spec.datasize()),
707  one(oneStorage.data()) {
708  }
709 
710  ~ZddSubsetter() {
711  if (!oneSrcPtr.empty()) {
712  spec.destruct(one);
713  oneSrcPtr.clear();
714  }
715  }
716 
721  int initialize(NodeId& root) {
722  sweeper.setRoot(root);
723  MyVector<char> tmp(spec.datasize());
724  void* const tmpState = tmp.data();
725  int n = spec.get_root(tmpState);
726 
727  int k = (root == 1) ? -1 : root.row();
728 
729  while (n != 0 && k != 0 && n != k) {
730  if (n < k) {
731  assert(k >= 1);
732  k = downTable(root, 0, n);
733  }
734  else {
735  assert(n >= 1);
736  n = downSpec(tmpState, n, 0, k);
737  }
738  }
739 
740  if (n <= 0 || k <= 0) {
741  assert(n == 0 || k == 0 || (n == -1 && k == -1));
742  root = NodeId(0, n != 0 && k != 0);
743  n = 0;
744  }
745  else {
746  assert(n == k);
747  assert(n == root.row());
748 
749  pools.resize(n + 1);
750  work[n].resize(input[n].size());
751 
752  SpecNode* p0 = work[n][root.col()].alloc_front(pools[n],
753  specNodeSize);
754  spec.get_copy(state(p0), tmpState);
755  srcPtr(p0) = &root;
756  }
757 
758  spec.destruct(tmpState);
759  output.init(n + 1);
760  if (!oneSrcPtr.empty()) {
761  spec.destruct(one);
762  oneSrcPtr.clear();
763  }
764  return n;
765  }
766 
771  void subset(int i) {
772  assert(0 < i && i < output.numRows());
773  assert(output.numRows() - pools.size() == 0);
774 
775  Hasher<Spec> const hasher(spec, i);
776  MyVector<char> tmp(spec.datasize());
777  void* const tmpState = tmp.data();
778  size_t const m = input[i].size();
779  size_t mm = 0;
780  int lowestChild = i - 1;
781  size_t deadCount = 0;
782 
783  if (work[i].empty()) work[i].resize(m);
784  assert(work[i].size() == m);
785 
786  for (size_t j = 0; j < m; ++j) {
787  MyListOnPool<SpecNode> &list = work[i][j];
788  size_t n = list.size();
789 
790  if (n >= 2) {
791  UniqTable uniq(n * 2, hasher, hasher);
792 
793  for (MyListOnPool<SpecNode>::iterator t = list.begin();
794  t != list.end(); ++t) {
795  SpecNode* p = *t;
796  SpecNode*& p0 = uniq.add(p);
797 
798  if (p0 == p) {
799  nodeId(p) = *srcPtr(p) = NodeId(i, mm++);
800  }
801  else {
802  switch (spec.merge_states(state(p0), state(p))) {
803  case 1:
804  nodeId(p0) = 0; // forward to 0-terminal
805  nodeId(p) = *srcPtr(p) = NodeId(i, mm++);
806  p0 = p;
807  break;
808  case 2:
809  *srcPtr(p) = 0;
810  nodeId(p) = 1; // unused
811  break;
812  default:
813  *srcPtr(p) = nodeId(p0);
814  nodeId(p) = 1; // unused
815  break;
816  }
817  }
818  }
819  }
820  else if (n == 1) {
821  SpecNode* p = list.front();
822  nodeId(p) = *srcPtr(p) = NodeId(i, mm++);
823  }
824  }
825 
826  output.initRow(i, mm);
827  Node<AR>* const outi = output[i].data();
828  size_t jj = 0;
829 
830  for (size_t j = 0; j < m; ++j) {
831  MyListOnPool<SpecNode> &list = work[i][j];
832 
833  for (MyListOnPool<SpecNode>::iterator t = list.begin();
834  t != list.end(); ++t) {
835  SpecNode* p = *t;
836  Node<AR>& q = outi[jj];
837 
838  if (nodeId(p) == 1) {
839  spec.destruct(state(p));
840  continue;
841  }
842 
843  bool allZero = true;
844 
845  for (int b = 0; b < AR; ++b) {
846  if (nodeId(p) == 0) {
847  q.branch[b] = 0;
848  continue;
849  }
850 
851  NodeId f(i, j);
852  spec.get_copy(tmpState, state(p));
853  int kk = downTable(f, b, i - 1);
854  int ii = downSpec(tmpState, i, b, kk);
855 
856  while (ii != 0 && kk != 0 && ii != kk) {
857  if (ii < kk) {
858  assert(kk >= 1);
859  kk = downTable(f, 0, ii);
860  }
861  else {
862  assert(ii >= 1);
863  ii = downSpec(tmpState, ii, 0, kk);
864  }
865  }
866 
867  if (ii <= 0 || kk <= 0) {
868  if (ii == 0 || kk == 0) {
869  q.branch[b] = 0;
870  }
871  else {
872  if (oneSrcPtr.empty()) { // the first 1-terminal candidate
873  spec.get_copy(one, tmpState);
874  q.branch[b] = 1;
875  oneSrcPtr.push_back(NodeBranchId(i, jj, b));
876  }
877  else {
878  switch (spec.merge_states(one, tmpState)) {
879  case 1:
880  while (!oneSrcPtr.empty()) {
881  NodeBranchId const& nbi =
882  oneSrcPtr.back();
883  assert(nbi.row >= i);
884  output[nbi.row][nbi.col].branch[nbi.val] =
885  0;
886  oneSrcPtr.pop_back();
887  }
888  spec.destruct(one);
889  spec.get_copy(one, tmpState);
890  q.branch[b] = 1;
891  oneSrcPtr.push_back(NodeBranchId(i, jj, b));
892  break;
893  case 2:
894  q.branch[b] = 0;
895  break;
896  default:
897  q.branch[b] = 1;
898  oneSrcPtr.push_back(NodeBranchId(i, jj, b));
899  break;
900  }
901  }
902  allZero = false;
903  }
904  }
905  else {
906  assert(ii == f.row() && ii == kk && ii < i);
907  if (work[ii].empty()) work[ii].resize(input[ii].size());
908  SpecNode* pp = work[ii][f.col()].alloc_front(pools[ii],
909  specNodeSize);
910  spec.get_copy(state(pp), tmpState);
911  srcPtr(pp) = &q.branch[b];
912  if (ii < lowestChild) lowestChild = ii;
913  allZero = false;
914  }
915 
916  spec.destruct(tmpState);
917  }
918 
919  spec.destruct(state(p));
920  ++jj;
921  if (allZero) ++deadCount;
922  }
923  }
924 
925  work[i].clear();
926  pools[i].clear();
927  spec.destructLevel(i);
928  sweeper.update(i, lowestChild, deadCount);
929  }
930 
931 private:
932  int downTable(NodeId& f, int b, int zerosupLevel) const {
933  if (zerosupLevel < 0) zerosupLevel = 0;
934 
935  f = input.child(f, b);
936  while (f.row() > zerosupLevel) {
937  f = input.child(f, 0);
938  }
939  return (f == 1) ? -1 : f.row();
940  }
941 
942  int downSpec(void* p, int level, int b, int zerosupLevel) {
943  if (zerosupLevel < 0) zerosupLevel = 0;
944  assert(level > zerosupLevel);
945 
946  int i = spec.get_child(p, level, b);
947  while (i > zerosupLevel) {
948  i = spec.get_child(p, i, 0);
949  }
950  return i;
951  }
952 };
953 
957 template<typename S>
958 class ZddSubsetterMP: DdBuilderMPBase { //TODO oneStorage
959 //typedef typename std::remove_const<typename std::remove_reference<S>::type>::type Spec;
960  typedef S Spec;
961  typedef MyHashTable<SpecNode*,Hasher<Spec>,Hasher<Spec> > UniqTable;
962  static int const AR = Spec::ARITY;
963 
964  int const threads;
965 
966  MyVector<Spec> specs;
967  int const specNodeSize;
968  NodeTableEntity<AR> const& input;
969  NodeTableEntity<AR>& output;
970  DdSweeper<AR> sweeper;
971 
972  MyVector<MyVector<MyVector<MyListOnPool<SpecNode> > > > snodeTables;
973  MyVector<MemoryPools> pools;
974 
975 public:
976  ZddSubsetterMP(NodeTableHandler<AR> const& input,
977  Spec const& s,
978  NodeTableHandler<AR>& output) :
979 #ifdef _OPENMP
980  threads(omp_get_max_threads()),
981 
982 #else
983  threads(1),
984 #endif
985  specs(threads, s),
986  specNodeSize(getSpecNodeSize(s.datasize())),
987  input(*input),
988  output(output.privateEntity()),
989  sweeper(this->output),
990  snodeTables(threads),
991  pools(threads) {
992  }
993 
998  int initialize(NodeId& root) {
999  sweeper.setRoot(root);
1000  MyVector<char> tmp(specs[0].datasize());
1001  void* const tmpState = tmp.data();
1002  Spec& spec = specs[0];
1003  int n = spec.get_root(tmpState);
1004 
1005  int k = (root == 1) ? -1 : root.row();
1006 
1007  while (n != 0 && k != 0 && n != k) {
1008  if (n < k) {
1009  assert(k >= 1);
1010  k = downTable(root, 0, n);
1011  }
1012  else {
1013  assert(n >= 1);
1014  n = downSpec(spec, tmpState, n, 0, k);
1015  }
1016  }
1017 
1018  if (n <= 0 || k <= 0) {
1019  assert(n == 0 || k == 0 || (n == -1 && k == -1));
1020  root = NodeId(0, n != 0 && k != 0);
1021  n = 0;
1022  }
1023  else {
1024  assert(n == k);
1025  assert(n == root.row());
1026 
1027  for (int y = 0; y < threads; ++y) {
1028  snodeTables[y].resize(n + 1);
1029  pools[y].resize(n + 1);
1030  }
1031 
1032  snodeTables[0][n].resize(input[n].size());
1033  SpecNode* p0 = snodeTables[0][n][root.col()].alloc_front(
1034  pools[0][n], specNodeSize);
1035  spec.get_copy(state(p0), tmpState);
1036  srcPtr(p0) = &root;
1037  }
1038 
1039  spec.destruct(tmpState);
1040  output.init(n + 1);
1041  return n;
1042  }
1043 
1048  void subset(int i) {
1049  assert(0 < i && i < output.numRows());
1050  size_t const m = input[i].size();
1051 
1052  MyVector<size_t> nodeColumn(m);
1053  int lowestChild = i - 1;
1054  size_t deadCount = 0;
1055 
1056 #ifdef _OPENMP
1057  // OpenMP 2.0 does not support reduction(min:lowestChild)
1058 #pragma omp parallel reduction(+:deadCount)
1059 #endif
1060  {
1061 #ifdef _OPENMP
1062  int yy = omp_get_thread_num();
1063 #else
1064  int yy = 0;
1065 #endif
1066  Spec& spec = specs[yy];
1067  MyVector<char> tmp(spec.datasize());
1068  void* const tmpState = tmp.data();
1069  Hasher<Spec> hasher(spec, i);
1070  UniqTable uniq(hasher, hasher);
1071  int lc = lowestChild;
1072 
1073 #ifdef _OPENMP
1074 #pragma omp for schedule(dynamic)
1075 #endif
1076  for (intmax_t j = 0; j < intmax_t(m); ++j) {
1077  size_t mm = 0;
1078  for (int y = 0; y < threads; ++y) {
1079  if (snodeTables[y][i].empty()) continue;
1080  MyListOnPool<SpecNode> &snodes = snodeTables[y][i][j];
1081  mm += snodes.size();
1082  }
1083  uniq.initialize(mm * 2);
1084  size_t jj = 0;
1085 
1086  for (int y = 0; y < threads; ++y) {
1087  if (snodeTables[y][i].empty()) continue;
1088  MyListOnPool<SpecNode> &snodes = snodeTables[y][i][j];
1089 
1090  for (MyListOnPool<SpecNode>::iterator t = snodes.begin();
1091  t != snodes.end(); ++t) {
1092  SpecNode* p = *t;
1093  SpecNode* pp = uniq.add(p);
1094 
1095  if (pp == p) {
1096  code(p) = ++jj; // code(p) >= 1
1097  }
1098  else {
1099  code(p) = -code(pp);
1100  if (int prune = spec.merge_states(state(pp),
1101  state(p))) {
1102  if (prune & 1) code(pp) = 0;
1103  if (prune & 2) code(p) = 0;
1104  }
1105  }
1106  }
1107  }
1108 
1109  nodeColumn[j] = jj;
1110  }
1111 
1112 #ifdef _OPENMP
1113 #pragma omp single
1114 #endif
1115  {
1116  size_t mm = 0;
1117  for (size_t j = 0; j < m; ++j) {
1118  size_t jj = nodeColumn[j];
1119  nodeColumn[j] = mm;
1120  mm += jj;
1121  }
1122 
1123  output.initRow(i, mm);
1124  }
1125 
1126 #ifdef _OPENMP
1127 #pragma omp for schedule(dynamic)
1128 #endif
1129  for (intmax_t j = 0; j < intmax_t(m); ++j) {
1130  size_t const jj0 = nodeColumn[j] - 1; // code(p) >= 1
1131 
1132  for (int y = 0; y < threads; ++y) {
1133  if (snodeTables[y][i].empty()) continue;
1134 
1135  MyListOnPool<SpecNode> &snodes = snodeTables[y][i][j];
1136 
1137  for (MyListOnPool<SpecNode>::iterator t = snodes.begin();
1138  t != snodes.end(); ++t) {
1139  SpecNode* p = *t;
1140 
1141  if (code(p) <= 0) {
1142  *srcPtr(p) = code(p) ? NodeId(i, jj0 - code(p)) : 0;
1143  spec.destruct(state(p));
1144  continue;
1145  }
1146 
1147  size_t const jj = jj0 + code(p);
1148  *srcPtr(p) = NodeId(i, jj);
1149  Node<AR> &q = output[i][jj];
1150  bool allZero = true;
1151  void* s = tmpState;
1152 
1153  for (int b = 0; b < AR; ++b) {
1154  if (b < AR - 1) {
1155  spec.get_copy(s, state(p));
1156  }
1157  else {
1158  s = state(p);
1159  }
1160 
1161  NodeId f(i, j);
1162  int kk = downTable(f, b, i - 1);
1163  int ii = downSpec(spec, s, i, b, kk);
1164 
1165  while (ii != 0 && kk != 0 && ii != kk) {
1166  if (ii < kk) {
1167  assert(kk >= 1);
1168  kk = downTable(f, 0, ii);
1169  }
1170  else {
1171  assert(ii >= 1);
1172  ii = downSpec(spec, s, ii, 0, kk);
1173  }
1174  }
1175 
1176  if (ii <= 0 || kk <= 0) {
1177  bool val = ii != 0 && kk != 0;
1178  q.branch[b] = val;
1179  if (val) allZero = false;
1180  }
1181  else {
1182  assert(ii == f.row() && ii == kk && ii < i);
1183  size_t jj = f.col();
1184 
1185  if (snodeTables[yy][ii].empty()) {
1186  snodeTables[yy][ii].resize(
1187  input[ii].size());
1188  }
1189 
1190  SpecNode* pp =
1191  snodeTables[yy][ii][jj].alloc_front(
1192  pools[yy][ii], specNodeSize);
1193  spec.get_copy(state(pp), s);
1194  srcPtr(pp) = &q.branch[b];
1195  if (ii < lc) lc = ii;
1196  allZero = false;
1197  }
1198 
1199  spec.destruct(s);
1200  }
1201 
1202  if (allZero) ++deadCount;
1203  }
1204  }
1205  }
1206 
1207  snodeTables[yy][i].clear();
1208  pools[yy][i].clear();
1209  spec.destructLevel(i);
1210 
1211 #ifdef _OPENMP
1212 #pragma omp critical
1213 #endif
1214  if (lc < lowestChild) lowestChild = lc;
1215  }
1216 
1217  sweeper.update(i, lowestChild, deadCount);
1218  }
1219 
1220 private:
1221  int downTable(NodeId& f, int b, int zerosupLevel) const {
1222  if (zerosupLevel < 0) zerosupLevel = 0;
1223 
1224  f = input.child(f, b);
1225  while (f.row() > zerosupLevel) {
1226  f = input.child(f, 0);
1227  }
1228  return (f == 1) ? -1 : f.row();
1229  }
1230 
1231  int downSpec(Spec& spec, void* p, int level, int b, int zerosupLevel) {
1232  if (zerosupLevel < 0) zerosupLevel = 0;
1233  assert(level > zerosupLevel);
1234 
1235  int i = spec.get_child(p, level, b);
1236  while (i > zerosupLevel) {
1237  i = spec.get_child(p, i, 0);
1238  }
1239  return i;
1240  }
1241 };
1242 
1247 template<typename S>
1248 class DdDumper {
1249  typedef S Spec;
1250  static int const AR = Spec::ARITY;
1251  static int const headerSize = 1;
1252 
1253  /* SpecNode
1254  * ┌────────┬────────┬────────┬─────
1255  * │ nodeId │state[0]│state[1]│ ...
1256  * └────────┴────────┴────────┴─────
1257  */
1258  struct SpecNode {
1259  NodeId nodeId;
1260  };
1261 
1262  static NodeId& nodeId(SpecNode* p) {
1263  return p->nodeId;
1264  }
1265 
1266  static NodeId nodeId(SpecNode const* p) {
1267  return p->nodeId;
1268  }
1269 
1270  static void* state(SpecNode* p) {
1271  return p + headerSize;
1272  }
1273 
1274  static void const* state(SpecNode const* p) {
1275  return p + headerSize;
1276  }
1277 
1278  template<typename SPEC>
1279  struct Hasher {
1280  SPEC const& spec;
1281  int const level;
1282 
1283  Hasher(SPEC const& spec, int level) :
1284  spec(spec), level(level) {
1285  }
1286 
1287  size_t operator()(SpecNode const* p) const {
1288  return spec.hash_code(state(p), level);
1289  }
1290 
1291  size_t operator()(SpecNode const* p, SpecNode const* q) const {
1292  return spec.equal_to(state(p), state(q), level);
1293  }
1294  };
1295 
1296  typedef MyHashTable<SpecNode*,Hasher<Spec>,Hasher<Spec> > UniqTable;
1297 
1298  static int getSpecNodeSize(int n) {
1299  if (n < 0)
1300  throw std::runtime_error("storage size is not initialized!!!");
1301  return headerSize + (n + sizeof(SpecNode) - 1) / sizeof(SpecNode);
1302  }
1303 
1304  Spec spec;
1305  int const specNodeSize;
1306  char* oneState;
1307  NodeId oneId;
1308 
1309  MyVector<MyList<SpecNode> > snodeTable;
1310  MyVector<UniqTable> uniqTable;
1311  MyVector<Hasher<Spec> > hasher;
1312 
1313 public:
1314  DdDumper(Spec const& s) :
1315  spec(s),
1316  specNodeSize(getSpecNodeSize(spec.datasize())),
1317  oneState(0),
1318  oneId(1) {
1319  }
1320 
1321  ~DdDumper() {
1322  if (oneState) {
1323  spec.destruct(oneState);
1324  delete[] oneState;
1325  }
1326  }
1327 
1333  void dump(std::ostream& os, std::string title) {
1334  if (oneState) {
1335  spec.destruct(oneState);
1336  }
1337  else {
1338  oneState = new char[spec.datasize()];
1339  }
1340  int n = spec.get_root(oneState);
1341 
1342  os << "digraph \"" << title << "\" {\n";
1343 
1344  if (n == 0) {
1345  if (!title.empty()) {
1346  os << " labelloc=\"t\";\n";
1347  os << " label=\"" << title << "\";\n";
1348  }
1349  }
1350  else if (n < 0) {
1351  os << " \"^\" [shape=none,label=\"" << title << "\"];\n";
1352  os << " \"^\" -> \"" << oneId << "\" [style=dashed" << "];\n";
1353  os << " \"" << oneId << "\" ";
1354  os << "[shape=square,margin=0.05,width=0,label=\"T\"];\n";
1355  }
1356  else {
1357  NodeId root(n, 0);
1358 
1359  for (int i = n; i >= 1; --i) {
1360  os << " " << i << " [shape=none,label=\"";
1361  spec.printLevel(os, i);
1362  os << "\"];\n";
1363  }
1364  for (int i = n - 1; i >= 1; --i) {
1365  os << " " << (i + 1) << " -> " << i << " [style=invis];\n";
1366  }
1367 
1368  os << " \"^\" [shape=none,label=\"" << title << "\"];\n";
1369  os << " \"^\" -> \"" << root << "\" [style=dashed" << "];\n";
1370 
1371  snodeTable.init(n + 1);
1372  SpecNode* p = snodeTable[n].alloc_front(specNodeSize);
1373  spec.get_copy(state(p), oneState);
1374  nodeId(p) = root;
1375 
1376  uniqTable.clear();
1377  uniqTable.reserve(n + 1);
1378  hasher.clear();
1379  hasher.reserve(n + 1);
1380  for (int i = 0; i <= n; ++i) {
1381  hasher.push_back(Hasher<Spec>(spec, i));
1382  uniqTable.push_back(UniqTable(hasher.back(), hasher.back()));
1383  }
1384 
1385  for (int i = n; i >= 1; --i) {
1386  dumpStep(os, i);
1387  }
1388 
1389  for (size_t j = 2; j < oneId.code(); ++j) {
1390  os << " \"" << NodeId(j) << "\" ";
1391  os << "[style=invis];\n";
1392  }
1393  os << " \"" << oneId << "\" ";
1394  os << "[shape=square,margin=0.05,width=0,label=\"T\"];\n";
1395  }
1396 
1397  os << "}\n";
1398  os.flush();
1399  }
1400 
1401 private:
1402  void dumpStep(std::ostream& os, int i) {
1403  MyList<SpecNode> &snodes = snodeTable[i];
1404  size_t const m = snodes.size();
1405  MyVector<char> tmp(spec.datasize());
1406  void* const tmpState = tmp.data();
1407  MyVector<Node<AR> > nodeList(m);
1408 
1409  for (size_t j = m - 1; j + 1 > 0; --j, snodes.pop_front()) {
1410  NodeId f(i, j);
1411  assert(!snodes.empty());
1412  SpecNode* p = snodes.front();
1413 
1414  os << " \"" << f << "\" [label=\"";
1415  spec.print_state(os, state(p), i);
1416  os << "\"];\n";
1417 
1418  for (int b = 0; b < AR; ++b) {
1419  NodeId& child = nodeList[j].branch[b];
1420 
1421  if (nodeId(p) == 0) {
1422  child = 0;
1423  continue;
1424  }
1425 
1426  spec.get_copy(tmpState, state(p));
1427  int ii = spec.get_child(tmpState, i, b);
1428 
1429  if (ii == 0) {
1430  child = 0;
1431  }
1432  else if (ii < 0) {
1433  if (oneId == 1) { // the first 1-terminal candidate
1434  oneId = 2;
1435  spec.destruct(oneState);
1436  spec.get_copy(oneState, tmpState);
1437  child = oneId;
1438  }
1439  else {
1440  switch (spec.merge_states(oneState, tmpState)) {
1441  case 1:
1442  oneId = oneId.code() + 1;
1443  spec.destruct(oneState);
1444  spec.get_copy(oneState, tmpState);
1445  child = oneId;
1446  break;
1447  case 2:
1448  child = 0;
1449  break;
1450  default:
1451  child = oneId;
1452  break;
1453  }
1454  }
1455  }
1456  else {
1457  SpecNode* pp = snodeTable[ii].alloc_front(specNodeSize);
1458  size_t jj = snodeTable[ii].size() - 1;
1459  spec.get_copy(state(pp), tmpState);
1460 
1461  SpecNode*& pp0 = uniqTable[ii].add(pp);
1462  if (pp0 == pp) {
1463  nodeId(pp) = child = NodeId(ii, jj);
1464  }
1465  else {
1466  switch (spec.merge_states(state(pp0), state(pp))) {
1467  case 1:
1468  nodeId(pp0) = 0;
1469  nodeId(pp) = child = NodeId(ii, jj);
1470  pp0 = pp;
1471  break;
1472  case 2:
1473  child = 0;
1474  spec.destruct(state(pp));
1475  snodeTable[ii].pop_front();
1476  break;
1477  default:
1478  child = nodeId(pp0);
1479  spec.destruct(state(pp));
1480  snodeTable[ii].pop_front();
1481  break;
1482  }
1483  }
1484  }
1485 
1486  spec.destruct(tmpState);
1487  }
1488 
1489  spec.destruct(state(p));
1490  }
1491 
1492  for (size_t j = 0; j < m; ++j) {
1493  for (int b = 0; b < AR; ++b) {
1494  NodeId f(i, j);
1495  NodeId child = nodeList[j].branch[b];
1496  if (child == 0) continue;
1497  if (child == 1) child = oneId;
1498 
1499  os << " \"" << f << "\" -> \"" << child << "\"";
1500 
1501  os << " [style=";
1502  if (b == 0) {
1503  os << "dashed";
1504  }
1505  else {
1506  os << "solid";
1507  if (AR > 2) {
1508  os << ",color="
1509  << ((b == 1) ? "blue" : (b == 2) ? "red" : "green");
1510  }
1511  }
1512  os << "];\n";
1513  }
1514  }
1515 
1516  os << " {rank=same; " << i;
1517  for (size_t j = 0; j < m; ++j) {
1518  os << "; \"" << NodeId(i, j) << "\"";
1519  }
1520  os << "}\n";
1521 
1522  uniqTable[i - 1].clear();
1523  spec.destructLevel(i);
1524  }
1525 };
1526 
1527 } // namespace tdzdd
tdzdd::DdDumper
DD dumper.
Definition: DdBuilder.hpp:1248
tdzdd::MyHashTable
Closed hash table implementation.
Definition: MyHashTable.hpp:147
tdzdd::ZddSubsetterMP::initialize
int initialize(NodeId &root)
Initializes the builder.
Definition: DdBuilder.hpp:998
tdzdd::MyHashTable::add
Entry & add(Entry const &elem)
Insert an element if no other equivalent element is registered.
Definition: MyHashTable.hpp:336
tdzdd::DdBuilder
Basic breadth-first DD builder.
Definition: DdBuilder.hpp:175
tdzdd::ZddSubsetter
Breadth-first ZDD subset builder.
Definition: DdBuilder.hpp:678
tdzdd::ZddSubsetter::subset
void subset(int i)
Builds one level.
Definition: DdBuilder.hpp:771
tdzdd::DdBuilder::schedule
void schedule(NodeId *fp, int level, void *s)
Schedules a top-down event.
Definition: DdBuilder.hpp:221
tdzdd::DdSweeper::update
void update(int current, int child, size_t count)
Updates status and sweeps the DD if necessary.
Definition: DdSweeper.hpp:92
tdzdd::ZddSubsetterMP
Multi-threaded breadth-first ZDD subset builder.
Definition: DdBuilder.hpp:958
tdzdd::DdBuilderMP::schedule
void schedule(NodeId *fp, int level, void *s)
Schedules a top-down event.
Definition: DdBuilder.hpp:461
tdzdd::ZddSubsetterMP::subset
void subset(int i)
Builds one level.
Definition: DdBuilder.hpp:1048
tdzdd::DdBuilderMP::initialize
int initialize(NodeId &root)
Initializes the builder.
Definition: DdBuilder.hpp:471
tdzdd::MyHashTable::initialize
void initialize(size_t n)
Initialize the table to be empty.
Definition: MyHashTable.hpp:301
tdzdd::DdDumper::dump
void dump(std::ostream &os, std::string title)
Dumps the node table in Graphviz (dot) format.
Definition: DdBuilder.hpp:1333
tdzdd::DdBuilder::initialize
int initialize(NodeId &root)
Initializes the builder.
Definition: DdBuilder.hpp:231
tdzdd::DdSweeper::setRoot
void setRoot(NodeId &root)
Set the root pointer.
Definition: DdSweeper.hpp:82
tdzdd::ZddSubsetter::initialize
int initialize(NodeId &root)
Initializes the builder.
Definition: DdBuilder.hpp:721
tdzdd::DdBuilderMP::construct
void construct(int i)
Builds one level.
Definition: DdBuilder.hpp:494
tdzdd::DdBuilder::construct
void construct(int i)
Builds one level.
Definition: DdBuilder.hpp:258
tdzdd::DdBuilderMP
Multi-threaded breadth-first DD builder.
Definition: DdBuilder.hpp:395
Generated on Sat Sep 19 2020 11:22:23 for TdZdd by   doxygen 1.8.13