TdZdd  1.1
A top-down/breadth-first decision diagram manipulation framework
NodeTable.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 <algorithm>
28 #include <cassert>
29 #include <climits>
30 #include <ostream>
31 #include <stdexcept>
32 
33 #include "Node.hpp"
34 #include "DataTable.hpp"
35 #include "../util/MyVector.hpp"
36 
37 namespace tdzdd {
38 
39 template<int ARITY>
40 class NodeTableEntity: public DataTable<Node<ARITY> > {
41  mutable MyVector<MyVector<int> > higherLevelTable;
42  mutable MyVector<MyVector<int> > lowerLevelTable;
43 
44 public:
49  NodeTableEntity(int n = 1)
50  : DataTable<Node<ARITY> >(n) {
51  assert(n >= 1);
52  initTerminals();
53  }
54 
59  void init(int n) {
60  assert(n >= 1);
61  DataTable<Node<ARITY> >::init(n);
62  initTerminals();
63  }
64 
68  void initTerminals() {
69  MyVector<Node<ARITY> >& t = (*this)[0];
70  t.resize(2);
71  for (int j = 0; j < 2; ++j) {
72  t[j] = Node<ARITY>(j, j);
73  }
74  }
75 
76 // /**
77 // * Gets the variable ID at a given level.
78 // * @param level level.
79 // * @return variable ID.
80 // */
81 // int varAtLevel(int level) const {
82 // assert(0 <= level && level <= numVars());
83 // return (level == 0) ? INT_MAX : numVars() - level;
84 // }
85 //
86 // /**
87 // * Gets the level of a variable.
88 // * @param var variable ID.
89 // * @return level.
90 // */
91 // int levelOfVar(int var) const {
92 // assert((0 <= var && var < numVars()) || var == INT_MAX);
93 // return (var == INT_MAX) ? 0 : numVars() - var;
94 // }
95 
100  size_t size() const {
101  return this->totalSize() - (*this)[0].size();
102  }
103 
108  int numVars() const {
109  return this->numRows() - 1;
110  }
111 
117  void stretchBottom(int n) {
118  int n0 = numVars();
119  int d = n - n0;
120 
121  if (d > 0) {
122  this->setNumRows(n + 1);
123 
124  for (int i = n0; i > 0; --i) {
125  size_t m = (*this)[i].size();
126  this->initRow(i + d, m);
127 
128  for (size_t j = 0; j < m; ++j) {
129  for (int b = 0; b < ARITY; ++b) {
130  NodeId ff = child(i, j, b);
131  int ii = ff.row();
132  child(i + d, j, b) =
133  (ii == 0) ? ff : NodeId(ii + d, ff.col());
134  }
135  }
136 
137  this->initRow(i, 0);
138  }
139  }
140  else if (d < 0) {
141  for (int i = 1 - d; i <= n0; ++i) {
142  size_t m = (*this)[i].size();
143  this->initRow(i + d, m);
144 
145  for (size_t j = 0; j < m; ++j) {
146  for (int b = 0; b < ARITY; ++b) {
147  NodeId ff = child(i, j, b);
148  int ii = ff.row();
149  child(i + d, j, b) =
150  (ii == 0) ? ff :
151  (ii + d <= 0) ? 1 : NodeId(ii + d, ff.col());
152  }
153  }
154 
155  this->initRow(i, 0);
156  }
157 
158  this->setNumRows(n + 1);
159  }
160  }
161 
167  Node<ARITY> const& node(NodeId f) const {
168  return (*this)[f.row()][f.col()];
169  }
170 
176  Node<ARITY>& node(NodeId f) {
177  return (*this)[f.row()][f.col()];
178  }
179 
186  NodeId child(NodeId f, int b) const {
187  return child(f.row(), f.col(), b);
188  }
189 
196  NodeId& child(NodeId f, int b) {
197  return child(f.row(), f.col(), b);
198  }
199 
207  NodeId child(int i, size_t j, int b) const {
208  assert(0 <= b && b < ARITY);
209  return (*this)[i][j].branch[b];
210  }
211 
219  NodeId& child(int i, size_t j, int b) {
220  assert(0 <= b && b < ARITY);
221  return (*this)[i][j].branch[b];
222  }
223 
230  NodeId getZeroDescendant(NodeId f, int stopLevel) const {
231  assert(0 <= stopLevel);
232  if (stopLevel == 0 && f.hasEmpty()) return 1;
233  while (f.row() > stopLevel) {
234  f = child(f, 0);
235  }
236  return f;
237  }
238 
242  void deleteIndex() {
243  higherLevelTable.clear();
244  lowerLevelTable.clear();
245  }
246 
251  void makeIndex(bool useMP = false) const {
252  int const n = this->numRows() - 1;
253  higherLevelTable.clear();
254  higherLevelTable.resize(n + 1);
255  lowerLevelTable.clear();
256  lowerLevelTable.resize(n + 1);
257  MyVector<bool> lowerMark(n + 1);
258 
259  for (int i = n; i >= 1; --i) {
260  MyVector<Node<ARITY> > const& node = (*this)[i];
261  size_t const m = node.size();
262  int lowest = i;
263  MyVector<bool> myLower(n + 1);
264 
265 #ifdef _OPENMP
266  if (useMP) {
267 #pragma omp parallel for schedule(static)
268  for (intmax_t j = 0; j < intmax_t(m); ++j) {
269  for (int b = 0; b < ARITY; ++b) {
270  int const ii = node[j].branch[b].row();
271  if (ii == 0) continue;
272  if (ii < lowest) {
273 #pragma omp critical
274  if (ii < lowest) lowest = ii;
275  }
276  if (!lowerMark[ii]) {
277  myLower[ii] = true;
278  lowerMark[ii] = true;
279  }
280  }
281  }
282  }
283  else
284 #endif
285  for (size_t j = 0; j < m; ++j) {
286  for (int b = 0; b < ARITY; ++b) {
287  int const ii = node[j].branch[b].row();
288  if (ii == 0) continue;
289  if (ii < lowest) lowest = ii;
290  if (!lowerMark[ii]) {
291  myLower[ii] = true;
292  lowerMark[ii] = true;
293  }
294  }
295  }
296 
297  higherLevelTable[lowest].push_back(i);
298  MyVector<int>& lower = lowerLevelTable[i];
299  for (int ii = lowest; ii < i; ++ii) {
300  if (myLower[ii]) lower.push_back(ii);
301  }
302  }
303  }
304 
310  MyVector<int> const& higherLevels(int level) const {
311  if (higherLevelTable.empty()) makeIndex();
312  return higherLevelTable[level];
313  }
314 
321  MyVector<int> const& lowerLevels(int level) const {
322  if (lowerLevelTable.empty()) makeIndex();
323  return lowerLevelTable[level];
324  }
325 
331  void dumpDot(std::ostream& os, std::string title = "") const {
332  os << "digraph \"" << title << "\" {\n";
333  for (int i = this->numRows() - 1; i >= 1; --i) {
334  os << " " << i << " [shape=none];\n";
335  }
336  for (int i = this->numRows() - 2; i >= 1; --i) {
337  os << " " << (i + 1) << " -> " << i << " [style=invis];\n";
338  }
339 
340  if (!title.empty()) {
341  os << " labelloc=\"t\";\n";
342  os << " label=\"" << title << "\";\n";
343  }
344 
345  bool terminal1 = false;
346 
347  for (int i = this->numRows() - 1; i > 0; --i) {
348  size_t m = (*this)[i].size();
349 
350  for (size_t j = 0; j < m; ++j) {
351  NodeId f = NodeId(i, j);
352  os << " \"" << f << "\";\n";
353 
354  for (int b = 0; b < ARITY; ++b) {
355  NodeId ff = child(i, j, b);
356  bool aa = ff.getAttr();
357  if (ff == 0) continue;
358 
359  if (ff == 1) {
360  terminal1 = true;
361  os << " \"" << f << "\" -> \"$\"";
362  }
363  else {
364  ff.setAttr(false);
365  os << " \"" << f << "\" -> \"" << ff << "\"";
366  }
367 
368  os << " [style=";
369  if (b == 0) {
370  os << "dashed";
371  }
372  else {
373  os << "solid";
374  if (ARITY > 2) {
375  os << ",color="
376  << ((b == 1) ? "blue" :
377  (b == 2) ? "red" : "green");
378  }
379  }
380  if (aa) os << ",arrowtail=dot";
381  os << "];\n";
382  }
383  }
384 
385  if (terminal1) {
386  os << " \"$\" [shape=square,label=\"⊤\"];\n";
387  }
388 
389  os << " {rank=same; " << i;
390  for (size_t j = 0; j < m; ++j) {
391  os << "; \"" << NodeId(i, j) << "\"";
392  }
393  os << "}\n";
394  }
395 
396  os << "}\n";
397  os.flush();
398  }
399 };
400 
401 template<int ARITY>
402 class NodeTableHandler {
403  struct Object {
404  unsigned refCount;
405  NodeTableEntity<ARITY> entity;
406 
407  Object(int n)
408  : refCount(1), entity(n) {
409  }
410 
411  Object(NodeTableEntity<ARITY> const& entity)
412  : refCount(1), entity(entity) {
413  }
414 
415  void ref() {
416  ++refCount;
417  if (refCount == 0) throw std::runtime_error("Too many references");
418  }
419 
420  void deref() {
421  --refCount;
422  if (refCount == 0) delete this;
423  }
424  };
425 
426  Object* pointer;
427 
428 public:
429  NodeTableHandler(int n = 1)
430  : pointer(new Object(n)) {
431  }
432 
433  NodeTableHandler(NodeTableHandler const& o)
434  : pointer(o.pointer) {
435  pointer->ref();
436  }
437 
438  NodeTableHandler& operator=(NodeTableHandler const& o) {
439  pointer->deref();
440  pointer = o.pointer;
441  pointer->ref();
442  return *this;
443  }
444 
445  ~NodeTableHandler() {
446  pointer->deref();
447  }
448 
449  NodeTableEntity<ARITY> const& operator*() const {
450  return pointer->entity;
451  }
452 
453  NodeTableEntity<ARITY> const* operator->() const {
454  return &pointer->entity;
455  }
456 
461  NodeTableEntity<ARITY>& privateEntity() {
462  if (pointer->refCount >= 2) {
463  pointer->deref();
464  pointer = new Object(pointer->entity);
465  }
466  return pointer->entity;
467  }
468 
474  NodeTableEntity<ARITY>& init(int n = 1) {
475  if (pointer->refCount == 1) {
476  pointer->entity.init(n);
477  }
478  else {
479  pointer->deref();
480  pointer = new Object(n);
481  }
482  return pointer->entity;
483  }
484 
489  void derefLevel(int i) {
490  if (pointer->refCount == 1) pointer->entity[i].clear();
491  }
492 };
493 
494 }// namespace tdzdd