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