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:
45     /**
46      * Constructor.
47      * @param n the number of rows.
48      */
NodeTableEntity(int n=1)49     NodeTableEntity(int n = 1)
50             : DataTable<Node<ARITY> >(n) {
51         assert(n >= 1);
52         initTerminals();
53     }
54 
55     /**
56      * Clears and initializes the table.
57      * @param n the number of rows.
58      */
init(int n)59     void init(int n) {
60         assert(n >= 1);
61         DataTable<Node<ARITY> >::init(n);
62         initTerminals();
63     }
64 
65     /**
66      * Initializes the terminal nodes.
67      */
initTerminals()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 
96     /**
97      * Gets the number of nonterminal nodes.
98      * @return the number of nonterminal nodes.
99      */
size() const100     size_t size() const {
101         return this->totalSize() - (*this)[0].size();
102     }
103 
104     /**
105      * Gets the number of ZDD variables.
106      * @return the number of ZDD variables.
107      */
numVars() const108     int numVars() const {
109         return this->numRows() - 1;
110     }
111 
112     /**
113      * Changes the number of ZDD variables
114      * by shifting up/down the levels of existing variables.
115      * @param n required number of variables.
116      */
stretchBottom(int n)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 
162     /**
163      * Gets a node.
164      * @param f node ID.
165      * @return node @p f.
166      */
node(NodeId f) const167     Node<ARITY> const& node(NodeId f) const {
168         return (*this)[f.row()][f.col()];
169     }
170 
171     /**
172      * Gets a reference to a node.
173      * @param f node ID.
174      * @return node @p f.
175      */
node(NodeId f)176     Node<ARITY>& node(NodeId f) {
177         return (*this)[f.row()][f.col()];
178     }
179 
180     /**
181      * Gets a child node ID.
182      * @param f parent node ID.
183      * @param b child branch.
184      * @return the @p b-child of @p f.
185      */
child(NodeId f,int b) const186     NodeId child(NodeId f, int b) const {
187         return child(f.row(), f.col(), b);
188     }
189 
190     /**
191      * Gets a reference to a child node ID.
192      * @param f parent node ID.
193      * @param b child branch.
194      * @return the @p b-child of @p f.
195      */
child(NodeId f,int b)196     NodeId& child(NodeId f, int b) {
197         return child(f.row(), f.col(), b);
198     }
199 
200     /**
201      * Gets a child node ID.
202      * @param i parent row.
203      * @param j parent column.
204      * @param b child branch.
205      * @return the @p b-child of the parent.
206      */
child(int i,size_t j,int b) const207     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 
212     /**
213      * Gets a reference to a child node ID.
214      * @param i parent row.
215      * @param j parent column.
216      * @param b child branch.
217      * @return the @p b-child of the parent.
218      */
child(int i,size_t j,int b)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 
224     /**
225      * Gets a descendant node ID by tracing 0-edges.
226      * @param f parent node ID.
227      * @param stopLevel level to stop going down.
228      * @return reached node ID.
229      */
getZeroDescendant(NodeId f,int stopLevel) const230     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 
239     /**
240      * Deletes current index information.
241      */
deleteIndex()242     void deleteIndex() {
243         higherLevelTable.clear();
244         lowerLevelTable.clear();
245     }
246 
247     /**
248      * Makes index information.
249      * @param useMP use an algorithm for multiple processors.
250      */
makeIndex(bool useMP=false) const251     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 
305     /**
306      * Returns a collection of the higher levels that directly refers
307      * the given level and that does not refer any lower levels.
308      * @param level the level.
309      */
higherLevels(int level) const310     MyVector<int> const& higherLevels(int level) const {
311         if (higherLevelTable.empty()) makeIndex();
312         return higherLevelTable[level];
313     }
314 
315     /**
316      * Returns a collection of the lower levels that are referred
317      * by the given level and that are not referred directly by
318      * any higher levels.
319      * @param level the level.
320      */
lowerLevels(int level) const321     MyVector<int> const& lowerLevels(int level) const {
322         if (lowerLevelTable.empty()) makeIndex();
323         return lowerLevelTable[level];
324     }
325 
326     /**
327      * Dumps the node table in Graphviz (dot) format.
328      * @param os output stream.
329      * @param title title label.
330      */
dumpDot(std::ostream & os,std::string title="") const331     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 
Objecttdzdd::NodeTableHandler::Object407         Object(int n)
408                 : refCount(1), entity(n) {
409         }
410 
Objecttdzdd::NodeTableHandler::Object411         Object(NodeTableEntity<ARITY> const& entity)
412                 : refCount(1), entity(entity) {
413         }
414 
reftdzdd::NodeTableHandler::Object415         void ref() {
416             ++refCount;
417             if (refCount == 0) throw std::runtime_error("Too many references");
418         }
419 
dereftdzdd::NodeTableHandler::Object420         void deref() {
421             --refCount;
422             if (refCount == 0) delete this;
423         }
424     };
425 
426     Object* pointer;
427 
428 public:
NodeTableHandler(int n=1)429     NodeTableHandler(int n = 1)
430             : pointer(new Object(n)) {
431     }
432 
NodeTableHandler(NodeTableHandler const & o)433     NodeTableHandler(NodeTableHandler const& o)
434             : pointer(o.pointer) {
435         pointer->ref();
436     }
437 
operator =(NodeTableHandler const & o)438     NodeTableHandler& operator=(NodeTableHandler const& o) {
439         pointer->deref();
440         pointer = o.pointer;
441         pointer->ref();
442         return *this;
443     }
444 
~NodeTableHandler()445     ~NodeTableHandler() {
446         pointer->deref();
447     }
448 
operator *() const449     NodeTableEntity<ARITY> const& operator*() const {
450         return pointer->entity;
451     }
452 
operator ->() const453     NodeTableEntity<ARITY> const* operator->() const {
454         return &pointer->entity;
455     }
456 
457     /**
458      * Make the table unshared.
459      * @return writable reference to the private table.
460      */
privateEntity()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 
469     /**
470      * Clear and initialize the table.
471      * @param n the number of rows.
472      * @return writable reference to the private table.
473      */
init(int n=1)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 
485     /**
486      * Clear a row if it is not shared.
487      * @param i row index.
488      */
derefLevel(int i)489     void derefLevel(int i) {
490         if (pointer->refCount == 1) pointer->entity[i].clear();
491     }
492 };
493 
494 }// namespace tdzdd
495