TdZdd  1.1
A top-down/breadth-first decision diagram manipulation framework
Node.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 <stdint.h>
29 #include <ostream>
30 
31 namespace tdzdd {
32 
33 int const NODE_ROW_BITS = 20;
34 int const NODE_ATTR_BITS = 1;
35 int const NODE_COL_BITS = 64 - NODE_ROW_BITS - NODE_ATTR_BITS;
36 
37 int const NODE_ROW_OFFSET = NODE_COL_BITS + NODE_ATTR_BITS;
38 int const NODE_ATTR_OFFSET = NODE_COL_BITS;
39 
40 uint64_t const NODE_ROW_MAX = (uint64_t(1) << NODE_ROW_BITS) - 1;
41 uint64_t const NODE_COL_MAX = (uint64_t(1) << NODE_COL_BITS) - 1;
42 
43 uint64_t const NODE_ROW_MASK = NODE_ROW_MAX << NODE_ROW_OFFSET;
44 uint64_t const NODE_ATTR_MASK = uint64_t(1) << NODE_ATTR_OFFSET;
45 
46 class NodeId {
47  uint64_t code_;
48 
49 public:
50  NodeId() { // 'code_' is not initialized in the default constructor for SPEED. @suppress("Class members should be properly initialized")
51  }
52 
53  NodeId(uint64_t code) :
54  code_(code) {
55  }
56 
57  NodeId(uint64_t row, uint64_t col) :
58  code_((row << NODE_ROW_OFFSET) | col) {
59  }
60 
61  NodeId(uint64_t row, uint64_t col, bool attr) :
62  code_((row << NODE_ROW_OFFSET) | col) {
63  setAttr(attr);
64  }
65 
66  int row() const {
67  return code_ >> NODE_ROW_OFFSET;
68  }
69 
70  size_t col() const {
71  return code_ & NODE_COL_MAX;
72  }
73 
74  void setAttr(bool val) {
75  if (val) {
76  code_ |= NODE_ATTR_MASK;
77  }
78  else {
79  code_ &= ~NODE_ATTR_MASK;
80  }
81  }
82 
83  bool getAttr() const {
84  return (code_ & NODE_ATTR_MASK) != 0;
85  }
86 
87  NodeId withoutAttr() const {
88  return code_ & ~NODE_ATTR_MASK;
89  }
90 
91  bool hasEmpty() const {
92  return code_ == 1 || getAttr();
93  }
94 
95  uint64_t code() const {
96  return code_ & ~NODE_ATTR_MASK;
97  }
98 
99  size_t hash() const {
100  return code() * 314159257;
101  }
102 
103  bool operator==(NodeId const& o) const {
104  return code() == o.code();
105  }
106 
107  bool operator!=(NodeId const& o) const {
108  return !(*this == o);
109  }
110 
111  bool operator<(NodeId const& o) const {
112  return code() < o.code();
113  }
114 
115  bool operator>=(NodeId const& o) const {
116  return !(*this < o);
117  }
118 
119  bool operator>(NodeId const& o) const {
120  return o < *this;
121  }
122 
123  bool operator<=(NodeId const& o) const {
124  return !(o < *this);
125  }
126 
127  friend std::ostream& operator<<(std::ostream& os, NodeId const& o) {
128  os << o.row() << ":" << o.col();
129  if (o.code_ & NODE_ATTR_MASK) os << "+";
130  return os;
131  }
132 };
133 
134 struct NodeBranchId {
135  size_t col;
136  int row;
137  int val;
138 
139  NodeBranchId() { // @suppress("Class members should be properly initialized")
140  }
141 
142  NodeBranchId(int row, size_t col, int val) :
143  col(col), row(row), val(val) {
144  }
145 };
146 
147 template<int ARITY>
148 struct Node {
149  NodeId branch[ARITY];
150 
151  Node() {
152  }
153 
154  Node(NodeId f0, NodeId f1) {
155  branch[0] = f0;
156  for (int i = 1; i < ARITY; ++i) {
157  branch[i] = f1;
158  }
159  }
160 
161  Node(NodeId const* f) {
162  for (int i = 0; i < ARITY; ++i) {
163  branch[i] = f[i];
164  }
165  }
166 
167  size_t hash() const {
168  size_t h = branch[0].code();
169  for (int i = 1; i < ARITY; ++i) {
170  h = h * 314159257 + branch[i].code() * 271828171;
171  }
172  return h;
173  }
174 
175  bool operator==(Node const& o) const {
176  for (int i = 0; i < ARITY; ++i) {
177  if (branch[i] != o.branch[i]) return false;
178  }
179  return true;
180  }
181 
182  bool operator!=(Node const& o) const {
183  return !operator==(o);
184  }
185 
186  friend std::ostream& operator<<(std::ostream& os, Node const& o) {
187  os << "(" << o.branch[0];
188  for (int i = 1; i < ARITY; ++i) {
189  os << "," << o.branch[i];
190  }
191  return os << ")";
192  }
193 };
194 
195 template<int ARITY>
196 struct InitializedNode: Node<ARITY> {
197  InitializedNode() :
198  Node<ARITY>(0, 0) {
199  }
200 
201  InitializedNode(NodeId f0, NodeId f1) :
202  Node<ARITY>(f0, f1) {
203  }
204 
205  InitializedNode(Node<ARITY> const& o) :
206  Node<ARITY>(o.branch) {
207  }
208 };
209 
210 } // namespace tdzdd