TdZdd  1.1
A top-down/breadth-first decision diagram manipulation framework
SapporoZdd.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 <ostream>
29 
30 #ifndef B_64
31 #if __SIZEOF_POINTER__ == 8
32 #define B_64
33 #endif
34 #endif
35 #include <ZBDD.h>
36 
37 #include "../DdSpec.hpp"
38 
39 namespace tdzdd {
40 
46 class SapporoZdd: public tdzdd::DdSpec<SapporoZdd,ZBDD,2> {
47  ZBDD const root;
48  int const offset;
49 
50  int var2level(int var) const {
51  return BDD_LevOfVar(var) - offset;
52  }
53 
54  int level2var(int level) const {
55  return BDD_VarOfLev(level + offset);
56  }
57 
58 public:
59  SapporoZdd(ZBDD const& f, int offset = 0)
60  : root(f), offset(offset) {
61  }
62 
63  int getRoot(ZBDD& f) const {
64  f = root;
65 
66  int level = BDD_LevOfVar(f.Top()) - offset;
67  if (level >= 1) return level;
68 
69  while (BDD_LevOfVar(f.Top()) >= 1) {
70  f = f.OffSet(BDD_VarOfLev(f.Top()));
71  }
72  return (f == 1) ? -1 : 0;
73  }
74 
75  int getChild(ZBDD& f, int level, int take) const {
76  int var = BDD_VarOfLev(level + offset);
77  f = take ? f.OnSet0(var) : f.OffSet(var);
78 
79  int nextLevel = BDD_LevOfVar(f.Top()) - offset;
80  assert(nextLevel < level);
81  if (nextLevel >= 1) return nextLevel;
82 
83  while (BDD_LevOfVar(f.Top()) >= 1) {
84  f = f.OffSet(BDD_VarOfLev(f.Top()));
85  }
86  return (f == 1) ? -1 : 0;
87  }
88 
89  size_t hashCode(ZBDD const& f) const {
90  return const_cast<ZBDD*>(&f)->GetID();
91  }
92 };
93 
94 } // namespace tdzdd
ZBDD wrapper.
Definition: SapporoZdd.hpp:46
Abstract class of DD specifications using scalar states.
Definition: DdSpec.hpp:257