37 #include "NodeTable.hpp" 38 #include "../util/MyHashTable.hpp" 39 #include "../util/MyList.hpp" 40 #include "../util/MyVector.hpp" 44 template<
int ARITY,
bool BDD,
bool ZDD>
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;
53 struct ReducNodeInfo {
58 return children.hash();
61 bool operator==(ReducNodeInfo
const& o)
const {
62 return children == o.children;
65 friend std::ostream& operator<<(std::ostream& os,
66 ReducNodeInfo
const& o) {
67 return os <<
"(" << o.children <<
" -> " << o.column <<
")";
72 static int const TASKS_PER_THREAD = 10;
76 MyVector<MyVector<MyList<ReducNodeInfo> > > taskMatrix;
77 MyVector<size_t> baseColumn;
80 ElapsedTimeCounter etcP1, etcP2, etcP3, etcS0, etcS1, etcS2, etcS3, etcS4;
84 bool readyForSequentialReduction;
87 DdReducer(NodeTableHandler<ARITY>& diagram,
bool useMP =
false) :
88 input(diagram.privateEntity()),
90 newDiagram(input.numRows()),
91 output(newDiagram.privateEntity()),
92 newIdTable(input.numRows()),
93 rootPtr(input.numRows()),
95 threads(omp_get_max_threads()),
96 tasks(MyHashConstant::primeSize(TASKS_PER_THREAD * threads)),
98 baseColumn(tasks + 1),
100 readyForSequentialReduction(false) {
105 mh <<
"#thread = " << threads <<
", #task = " << tasks;
110 diagram = newDiagram;
112 input.initTerminals();
113 input.makeIndex(useMP);
115 newIdTable[0].resize(2);
116 newIdTable[0][0] = 0;
117 newIdTable[0][1] = 1;
120 for (
int y = 0; y < threads; ++y) {
121 taskMatrix[y].resize(tasks);
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";
153 void makeReadyForSequentialReduction() {
154 if (readyForSequentialReduction)
return;
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();
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;
167 NodeId f0 = input.child(f, 0);
168 NodeId deletable = BDD ? f0 : 0;
171 for (
int bb = (BDD || ZDD) ? 1 : 0; bb < ARITY; ++bb) {
172 if (input.child(f, bb) != deletable) {
188 mh <<
"[#dead = " << dead <<
"]";
191 readyForSequentialReduction =
true;
199 void setRoot(NodeId& root) {
200 rootPtr[root.row()].push_back(&root);
208 void reduce(
int i,
bool useMP =
false) {
212 else if (ARITY == 2) {
225 void algorithmR(
int i) {
227 makeReadyForSequentialReduction();
228 size_t const m = input[i].size();
229 Node<ARITY>*
const tt = input[i].data();
230 NodeId
const mark(i, m);
232 MyVector<NodeId>& newId = newIdTable[i];
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];
239 if (f0.row() != 0) f0 = newIdTable[f0.row()][f0.col()];
240 if (f1.row() != 0) f1 = newIdTable[f1.row()][f1.col()];
242 if ((BDD && f1 == f0) || (ZDD && f1 == 0)) {
246 NodeId& f00 = input.child(f0, 0);
247 NodeId& f01 = input.child(f0, 1);
251 newId[j] = NodeId(i + 1, m);
256 f00 = NodeId(i + 1, j);
261 MyVector<int>
const& levels = input.lowerLevels(i);
262 for (
int const* t = levels.begin(); t != levels.end(); ++t) {
263 newIdTable[*t].clear();
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;
273 for (
size_t k = j; k < m;) {
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);
281 assert(newId[k].row() == i + 1);
282 size_t next = newId[k].col();
287 newId[k] = NodeId(i, mm++, g0.hasEmpty());
300 MyVector<int>
const& levels = input.lowerLevels(i);
301 for (
int const* t = levels.begin(); t != levels.end(); ++t) {
306 output.initRow(i, mm);
307 Node<ARITY>* nt = output[i].data();
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];
314 assert(f0.row() == i);
315 assert(newId[j] == 0);
316 newId[j] = newId[f0.col()];
318 else if ((BDD && f1 == f0) || (ZDD && f1 == 0)) {
319 assert(newId[j].row() < i);
322 assert(newId[j].row() == i);
323 size_t k = newId[j].col();
328 for (
size_t k = 0; k < rootPtr[i].size(); ++k) {
329 NodeId& root = *rootPtr[i][k];
330 root = newId[root.col()];
338 void reduce_(
int i) {
339 size_t const m = input[i].size();
340 newIdTable[i].resize(m);
346 MyHashTable<Node<ARITY>
const*> uniq(m * 2);
348 for (
size_t j = 0; j < m; ++j) {
349 Node<ARITY>*
const p0 = input[i].data();
350 Node<ARITY>& f = input[i][j];
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;
364 newIdTable[i][j] = f0;
367 Node<ARITY>
const* pp = uniq.add(&f);
370 newIdTable[i][j] = NodeId(i, jj++, f0.hasEmpty());
373 newIdTable[i][j] = newIdTable[i][pp - p0];
379 MyVector<int>
const& levels = input.lowerLevels(i);
380 for (
int const* t = levels.begin(); t != levels.end(); ++t) {
381 newIdTable[*t].clear();
384 output.initRow(i, jj);
386 for (
size_t j = 0; j < m; ++j) {
387 NodeId
const& ff = newIdTable[i][j];
389 output[i][ff.col()] = input[i][j];
395 for (
size_t k = 0; k < rootPtr[i].size(); ++k) {
396 NodeId& root = *rootPtr[i][k];
397 root = newIdTable[i][root.col()];
405 void reduceMP_(
int i) {
412 size_t const m = input[i].size();
413 newIdTable[i].resize(m);
421 int y = omp_get_thread_num();
422 MyHashTable<ReducNodeInfo const*> uniq;
424 #pragma omp for schedule(static) 425 for (
size_t j = 0; j < m; ++j) {
426 Node<ARITY>& f = input[i][j];
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;
440 newIdTable[i][j] = f0;
445 int x = f.hash() % tasks;
446 ReducNodeInfo* p = taskMatrix[y][x].alloc_front();
457 MyVector<int>
const& levels = input.lowerLevels(i);
458 for (
int const* t = levels.begin(); t != levels.end(); ++t) {
459 newIdTable[*t].clear();
467 #pragma omp for schedule(dynamic) 468 for (
int x = 0; x < tasks; ++x) {
470 for (
int yy = 0; yy < threads; ++yy) {
471 mm += taskMatrix[yy][x].size();
474 baseColumn[x + 1] = 0;
478 uniq.initialize(mm * 2);
481 for (
int yy = 0; yy < threads; ++yy) {
482 MyList<ReducNodeInfo>& taskq = taskMatrix[yy][x];
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);
490 newIdTable[i][p->column] =
493 p->children.branch[0].hasEmpty());
496 newIdTable[i][p->column] =
497 newIdTable[i][pp->column];
502 baseColumn[x + 1] = j;
505 for (
int x = 0; x < tasks; ++x) {
506 taskMatrix[y][x].clear();
515 for (
int x = 1; x < tasks; ++x) {
516 baseColumn[x + 1] += baseColumn[x];
529 output.initRow(i, baseColumn[tasks]);
536 #pragma omp for schedule(static) 537 for (
size_t j = 0; j < m; ++j) {
538 NodeId& ff = newIdTable[i][j];
541 ff.col() + baseColumn[ff.row() - i],
543 output[i][ff.col()] = input[i][j];
553 for (
size_t k = 0; k < rootPtr[i].size(); ++k) {
554 NodeId& root = *rootPtr[i][k];
555 root = newIdTable[i][root.col()];
564 void garbageCollect() {
566 for (
int i = input.numRows() - 1; i > 0; --i) {
567 size_t m = input[i].size();
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());
576 std::sort(roots.begin(), roots.end());
577 roots.resize(std::unique(roots.begin(), roots.end())
582 for (
size_t j = 0, k = 0; j < m; ++j) {
584 input.child(i, j, 0).setAttr(
true);
587 assert(j == roots[k]);
588 input.child(i, j, 0).setAttr(
false);
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);
601 for (
int b = 1; b < ARITY; ++b) {
602 NodeId& ff = input.child(i, j, b);
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);