TdZdd  1.1
A top-down/breadth-first decision diagram manipulation framework
DdReducer.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 "Node.hpp"
37 #include "NodeTable.hpp"
38 #include "../util/MyHashTable.hpp"
39 #include "../util/MyList.hpp"
40 #include "../util/MyVector.hpp"
41 
42 namespace tdzdd {
43 
44 template<int ARITY, bool BDD, bool ZDD>
45 class DdReducer {
46  NodeTableEntity<ARITY>& input;
47  NodeTableHandler<ARITY> oldDiagram;
48  NodeTableHandler<ARITY> newDiagram;
49  NodeTableEntity<ARITY>& output;
50  MyVector<MyVector<NodeId> > newIdTable;
51  MyVector<MyVector<NodeId*> > rootPtr;
52 
53  struct ReducNodeInfo {
54  Node<ARITY> children;
55  size_t column;
56 
57  size_t hash() const {
58  return children.hash();
59  }
60 
61  bool operator==(ReducNodeInfo const& o) const {
62  return children == o.children;
63  }
64 
65  friend std::ostream& operator<<(std::ostream& os,
66  ReducNodeInfo const& o) {
67  return os << "(" << o.children << " -> " << o.column << ")";
68  }
69  };
70 
71 #ifdef _OPENMP
72  static int const TASKS_PER_THREAD = 10;
73 
74  int const threads;
75  int const tasks;
76  MyVector<MyVector<MyList<ReducNodeInfo> > > taskMatrix;
77  MyVector<size_t> baseColumn;
78 
79 #ifdef DEBUG
80  ElapsedTimeCounter etcP1, etcP2, etcP3, etcS0, etcS1, etcS2, etcS3, etcS4;
81 #endif
82 #endif
83 
84  bool readyForSequentialReduction;
85 
86 public:
87  DdReducer(NodeTableHandler<ARITY>& diagram, bool useMP = false) :
88  input(diagram.privateEntity()),
89  oldDiagram(diagram),
90  newDiagram(input.numRows()),
91  output(newDiagram.privateEntity()),
92  newIdTable(input.numRows()),
93  rootPtr(input.numRows()),
94 #ifdef _OPENMP
95  threads(omp_get_max_threads()),
96  tasks(MyHashConstant::primeSize(TASKS_PER_THREAD * threads)),
97  taskMatrix(threads),
98  baseColumn(tasks + 1),
99 #endif
100  readyForSequentialReduction(false) {
101 #ifdef _OPENMP
102 #ifdef DEBUG
103  if (useMP) {
104  MessageHandler mh;
105  mh << "#thread = " << threads << ", #task = " << tasks;
106  }
107  etcS0.start();
108 #endif
109 #endif
110  diagram = newDiagram;
111 
112  input.initTerminals();
113  input.makeIndex(useMP);
114 
115  newIdTable[0].resize(2);
116  newIdTable[0][0] = 0;
117  newIdTable[0][1] = 1;
118 
119 #ifdef _OPENMP
120  for (int y = 0; y < threads; ++y) {
121  taskMatrix[y].resize(tasks);
122  }
123 #ifdef DEBUG
124  etcS0.stop();
125 #endif
126 #endif
127  }
128 
129 #ifdef _OPENMP
130 #ifdef DEBUG
131  ~DdReducer() {
132  if (etcP1 != 0) {
133  MessageHandler mh;
134  mh << "P1: " << etcP1 << "\n";
135  mh << "P2: " << etcP2 << "\n";
136  mh << "P3: " << etcP3 << "\n";
137  mh << "S0: " << etcS0 << "\n";
138  mh << "S1: " << etcS1 << "\n";
139  mh << "S2: " << etcS2 << "\n";
140  mh << "S3: " << etcS3 << "\n";
141  mh << "S4: " << etcS4 << "\n";
142  }
143  }
144 #endif
145 #endif
146 
147 private:
153  void makeReadyForSequentialReduction() {
154  if (readyForSequentialReduction) return;
155 #ifdef DEBUG
156  size_t dead = 0;
157 #endif
158  for (int i = 2; i < input.numRows(); ++i) {
159  size_t const m = input[i].size();
160  Node<ARITY>* const tt = input[i].data();
161 
162  for (size_t j = 0; j < m; ++j) {
163  for (int b = 0; b < ARITY; ++b) {
164  NodeId& f = tt[j].branch[b];
165  if (f.row() == 0) continue;
166 
167  NodeId f0 = input.child(f, 0);
168  NodeId deletable = BDD ? f0 : 0;
169  bool del = true;
170 
171  for (int bb = (BDD || ZDD) ? 1 : 0; bb < ARITY; ++bb) {
172  if (input.child(f, bb) != deletable) {
173  del = false;
174  }
175  }
176 
177  if (del) {
178  f = f0;
179 #ifdef DEBUG
180  if (f == 0) ++dead;
181 #endif
182  }
183  }
184  }
185  }
186 #ifdef DEBUG
187  MessageHandler mh;
188  mh << "[#dead = " << dead << "]";
189 #endif
190  input.makeIndex();
191  readyForSequentialReduction = true;
192  }
193 
194 public:
199  void setRoot(NodeId& root) {
200  rootPtr[root.row()].push_back(&root);
201  }
202 
208  void reduce(int i, bool useMP = false) {
209  if (useMP) {
210  reduceMP_(i);
211  }
212  else if (ARITY == 2) {
213  algorithmR(i);
214  }
215  else {
216  reduce_(i);
217  }
218  }
219 
220 private:
225  void algorithmR(int i) {
226  assert(ARITY == 2);
227  makeReadyForSequentialReduction();
228  size_t const m = input[i].size();
229  Node<ARITY>* const tt = input[i].data();
230  NodeId const mark(i, m);
231 
232  MyVector<NodeId>& newId = newIdTable[i];
233  newId.resize(m);
234 
235  for (size_t j = m - 1; j + 1 > 0; --j) {
236  NodeId& f0 = tt[j].branch[0];
237  NodeId& f1 = tt[j].branch[1];
238 
239  if (f0.row() != 0) f0 = newIdTable[f0.row()][f0.col()];
240  if (f1.row() != 0) f1 = newIdTable[f1.row()][f1.col()];
241 
242  if ((BDD && f1 == f0) || (ZDD && f1 == 0)) {
243  newId[j] = f0;
244  }
245  else {
246  NodeId& f00 = input.child(f0, 0);
247  NodeId& f01 = input.child(f0, 1);
248 
249  if (f01 != mark) { // the first touch from this level
250  f01 = mark; // mark f0 as touched
251  newId[j] = NodeId(i + 1, m); // tail of f0-equivalent list
252  }
253  else {
254  newId[j] = f00; // next of f0-equivalent list
255  }
256  f00 = NodeId(i + 1, j); // new head of f0-equivalent list
257  }
258  }
259 
260  {
261  MyVector<int> const& levels = input.lowerLevels(i);
262  for (int const* t = levels.begin(); t != levels.end(); ++t) {
263  newIdTable[*t].clear();
264  }
265  }
266  size_t mm = 0;
267 
268  for (size_t j = 0; j < m; ++j) {
269  NodeId const f(i, j);
270  assert(newId[j].row() <= i + 1);
271  if (newId[j].row() <= i) continue;
272 
273  for (size_t k = j; k < m;) { // for each g in f0-equivalent list
274  assert(j <= k);
275  NodeId const g(i, k);
276  NodeId& g0 = tt[k].branch[0];
277  NodeId& g1 = tt[k].branch[1];
278  NodeId& g10 = input.child(g1, 0);
279  NodeId& g11 = input.child(g1, 1);
280  assert(g1 != mark);
281  assert(newId[k].row() == i + 1);
282  size_t next = newId[k].col();
283 
284  if (g11 != f) { // the first touch to g1 in f0-equivalent list
285  g11 = f; // mark g1 as touched
286  g10 = g; // record g as a canonical node for <f0,g1>
287  newId[k] = NodeId(i, mm++, g0.hasEmpty());
288  }
289  else {
290  g0 = g10; // make a forward link
291  g1 = mark; // mark g as forwarded
292  newId[k] = 0;
293  }
294 
295  k = next;
296  }
297  }
298 
299  if (!BDD) {
300  MyVector<int> const& levels = input.lowerLevels(i);
301  for (int const* t = levels.begin(); t != levels.end(); ++t) {
302  input[*t].clear();
303  }
304  }
305 
306  output.initRow(i, mm);
307  Node<ARITY>* nt = output[i].data();
308 
309  for (size_t j = 0; j < m; ++j) {
310  NodeId const& f0 = tt[j].branch[0];
311  NodeId const& f1 = tt[j].branch[1];
312 
313  if (f1 == mark) { // forwarded
314  assert(f0.row() == i);
315  assert(newId[j] == 0);
316  newId[j] = newId[f0.col()];
317  }
318  else if ((BDD && f1 == f0) || (ZDD && f1 == 0)) { // forwarded
319  assert(newId[j].row() < i);
320  }
321  else {
322  assert(newId[j].row() == i);
323  size_t k = newId[j].col();
324  nt[k] = tt[j];
325  }
326  }
327 
328  for (size_t k = 0; k < rootPtr[i].size(); ++k) {
329  NodeId& root = *rootPtr[i][k];
330  root = newId[root.col()];
331  }
332  }
333 
338  void reduce_(int i) {
339  size_t const m = input[i].size();
340  newIdTable[i].resize(m);
341  size_t jj = 0;
342 
343  {
344  //MyList<ReducNodeInfo> rni;
345  //MyHashTable<ReducNodeInfo const*> uniq(m * 2);
346  MyHashTable<Node<ARITY> const*> uniq(m * 2);
347 
348  for (size_t j = 0; j < m; ++j) {
349  Node<ARITY>* const p0 = input[i].data();
350  Node<ARITY>& f = input[i][j];
351 
352  // make f canonical
353  NodeId& f0 = f.branch[0];
354  f0 = newIdTable[f0.row()][f0.col()];
355  NodeId deletable = BDD ? f0 : 0;
356  bool del = BDD || ZDD || (f0 == 0);
357  for (int b = 1; b < ARITY; ++b) {
358  NodeId& ff = f.branch[b];
359  ff = newIdTable[ff.row()][ff.col()];
360  if (ff != deletable) del = false;
361  }
362 
363  if (del) { // f is redundant
364  newIdTable[i][j] = f0;
365  }
366  else {
367  Node<ARITY> const* pp = uniq.add(&f);
368 
369  if (pp == &f) {
370  newIdTable[i][j] = NodeId(i, jj++, f0.hasEmpty());
371  }
372  else {
373  newIdTable[i][j] = newIdTable[i][pp - p0];
374  }
375  }
376  }
377  }
378 
379  MyVector<int> const& levels = input.lowerLevels(i);
380  for (int const* t = levels.begin(); t != levels.end(); ++t) {
381  newIdTable[*t].clear();
382  }
383 
384  output.initRow(i, jj);
385 
386  for (size_t j = 0; j < m; ++j) {
387  NodeId const& ff = newIdTable[i][j];
388  if (ff.row() == i) {
389  output[i][ff.col()] = input[i][j];
390  }
391  }
392 
393  input[i].clear();
394 
395  for (size_t k = 0; k < rootPtr[i].size(); ++k) {
396  NodeId& root = *rootPtr[i][k];
397  root = newIdTable[i][root.col()];
398  }
399  }
400 
405  void reduceMP_(int i) {
406 #ifndef _OPENMP
407  reduce_(i);
408 #else
409 #ifdef DEBUG
410  etcS1.start();
411 #endif
412  size_t const m = input[i].size();
413  newIdTable[i].resize(m);
414 #ifdef DEBUG
415  etcS1.stop();
416  etcP1.start();
417 #endif
418 
419 #pragma omp parallel
420  {
421  int y = omp_get_thread_num();
422  MyHashTable<ReducNodeInfo const*> uniq;
423 
424 #pragma omp for schedule(static)
425  for (size_t j = 0; j < m; ++j) {
426  Node<ARITY>& f = input[i][j];
427 
428  // make f canonical
429  NodeId& f0 = f.branch[0];
430  f0 = newIdTable[f0.row()][f0.col()];
431  NodeId deletable = BDD ? f0 : 0;
432  bool del = BDD || ZDD || (f0 == 0);
433  for (int b = 1; b < ARITY; ++b) {
434  NodeId& ff = f.branch[b];
435  ff = newIdTable[ff.row()][ff.col()];
436  if (ff != deletable) del = false;
437  }
438 
439  if (del) { // f is redundant
440  newIdTable[i][j] = f0;
441  continue;
442  }
443 
444  // schedule a task
445  int x = f.hash() % tasks;
446  ReducNodeInfo* p = taskMatrix[y][x].alloc_front();
447  p->children = f;
448  p->column = j;
449  }
450 
451 #pragma omp single
452  {
453 #ifdef DEBUG
454  etcP1.stop();
455  etcS2.start();
456 #endif
457  MyVector<int> const& levels = input.lowerLevels(i);
458  for (int const* t = levels.begin(); t != levels.end(); ++t) {
459  newIdTable[*t].clear();
460  }
461 #ifdef DEBUG
462  etcS2.stop();
463  etcP2.start();
464 #endif
465  }
466 
467 #pragma omp for schedule(dynamic)
468  for (int x = 0; x < tasks; ++x) {
469  size_t mm = 0;
470  for (int yy = 0; yy < threads; ++yy) {
471  mm += taskMatrix[yy][x].size();
472  }
473  if (mm == 0) {
474  baseColumn[x + 1] = 0;
475  continue;
476  }
477 
478  uniq.initialize(mm * 2);
479  size_t j = 0;
480 
481  for (int yy = 0; yy < threads; ++yy) {
482  MyList<ReducNodeInfo>& taskq = taskMatrix[yy][x];
483 
484  for (typename MyList<ReducNodeInfo>::iterator t =
485  taskq.begin(); t != taskq.end(); ++t) {
486  ReducNodeInfo const* p = *t;
487  ReducNodeInfo const* pp = uniq.add(p);
488 
489  if (pp == p) {
490  newIdTable[i][p->column] =
491  NodeId(i + x,
492  j++,
493  p->children.branch[0].hasEmpty()); // row += task ID
494  }
495  else {
496  newIdTable[i][p->column] =
497  newIdTable[i][pp->column];
498  }
499  }
500  }
501 
502  baseColumn[x + 1] = j;
503  }
504 
505  for (int x = 0; x < tasks; ++x) {
506  taskMatrix[y][x].clear();
507  }
508 
509 #pragma omp single
510  {
511 #ifdef DEBUG
512  etcP2.stop();
513  etcS3.start();
514 #endif
515  for (int x = 1; x < tasks; ++x) {
516  baseColumn[x + 1] += baseColumn[x];
517  }
518 
519 // for (int k = 1; k < tasks; k <<= 1) {
520 //#pragma omp for schedule(static)
521 // for (int x = k; x < tasks; ++x) {
522 // if (x & k) {
523 // int w = (x & ~k) | (k - 1);
524 // baseColumn[x + 1] += baseColumn[w + 1];
525 // }
526 // }
527 // }
528 
529  output.initRow(i, baseColumn[tasks]);
530 #ifdef DEBUG
531  etcS3.stop();
532  etcP3.start();
533 #endif
534  }
535 
536 #pragma omp for schedule(static)
537  for (size_t j = 0; j < m; ++j) {
538  NodeId& ff = newIdTable[i][j];
539  if (ff.row() >= i) {
540  ff = NodeId(i,
541  ff.col() + baseColumn[ff.row() - i],
542  ff.getAttr());
543  output[i][ff.col()] = input[i][j];
544  }
545  }
546  }
547 #ifdef DEBUG
548  etcP3.stop();
549  etcS4.start();
550 #endif
551  input[i].clear();
552 
553  for (size_t k = 0; k < rootPtr[i].size(); ++k) {
554  NodeId& root = *rootPtr[i][k];
555  root = newIdTable[i][root.col()];
556  }
557 #ifdef DEBUG
558  etcS4.stop();
559 #endif
560 #endif // _OPENMP
561  }
562 
563 public:
564  void garbageCollect() {
565  // Initialize marks
566  for (int i = input.numRows() - 1; i > 0; --i) {
567  size_t m = input[i].size();
568 
569  size_t r = rootPtr[i].size();
570  MyVector<size_t> roots;
571  roots.reserve(r + 1);
572  for (size_t k = 0; k < r; ++k) {
573  roots.push_back(rootPtr[i][k]->col());
574  }
575  if (r >= 2) {
576  std::sort(roots.begin(), roots.end());
577  roots.resize(std::unique(roots.begin(), roots.end())
578  - roots.begin());
579  }
580  roots.push_back(m);
581 
582  for (size_t j = 0, k = 0; j < m; ++j) {
583  if (j < roots[k]) {
584  input.child(i, j, 0).setAttr(true);
585  }
586  else {
587  assert(j == roots[k]);
588  input.child(i, j, 0).setAttr(false);
589  ++k;
590  }
591  }
592  }
593 
594  // Delete unnecessary nodes
595  for (int i = input.numRows() - 1; i > 0; --i) {
596  size_t m = input[i].size();
597  for (size_t j = 0; j < m; ++j) {
598  NodeId& f0 = input.child(i, j, 0);
599  if (f0.getAttr()) {
600  f0 = 0;
601  for (int b = 1; b < ARITY; ++b) {
602  NodeId& ff = input.child(i, j, b);
603  ff = 0;
604  }
605  }
606  else {
607  input.child(f0, 0).setAttr(false);
608  for (int b = 1; b < ARITY; ++b) {
609  NodeId& ff = input.child(i, j, b);
610  input.child(ff, 0).setAttr(false);
611  }
612  }
613  }
614  }
615  }
616 };
617 
618 } // namespace tdzdd