TdZdd  1.1
A top-down/breadth-first decision diagram manipulation framework
Lookahead.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 <iostream>
29 #include <vector>
30 
31 #include "../DdSpec.hpp"
32 
33 namespace tdzdd {
34 
35 template<typename S>
36 class BddLookahead: public DdSpecBase<BddLookahead<S>,S::ARITY> {
37  typedef S Spec;
38 
39  Spec spec;
40  std::vector<char> work0;
41  std::vector<char> work1;
42 
43  int lookahead(void* p, int level) {
44  while (level >= 1) {
45  spec.get_copy(work0.data(), p);
46  int level0 = spec.get_child(work0.data(), level, 0);
47 
48  for (int b = 1; b < Spec::ARITY; ++b) {
49  spec.get_copy(work1.data(), p);
50  int level1 = spec.get_child(work1.data(), level, b);
51  if (!(level0 == level1
52  && (level0 <= 0
53  || spec.equal_to(work0.data(), work1.data(),
54  level0)))) {
55  spec.destruct(work0.data());
56  spec.destruct(work1.data());
57  return level;
58  }
59  spec.destruct(work1.data());
60  }
61 
62  spec.destruct(p);
63  spec.get_copy(p, work0.data());
64  spec.destruct(work0.data());
65  level = level0;
66  }
67 
68  return level;
69  }
70 
71 public:
72  BddLookahead(S const& s)
73  : spec(s), work0(spec.datasize()), work1(spec.datasize()) {
74  }
75 
76  int datasize() const {
77  return spec.datasize();
78  }
79 
80  int get_root(void* p) {
81  return lookahead(p, spec.get_root(p));
82  }
83 
84  int get_child(void* p, int level, int b) {
85  return lookahead(p, spec.get_child(p, level, b));
86  }
87 
88  void get_copy(void* to, void const* from) {
89  spec.get_copy(to, from);
90  }
91 
92  int merge_states(void* p1, void* p2) {
93  return spec.merge_states(p1, p2);
94  }
95 
96  void destruct(void* p) {
97  spec.destruct(p);
98  }
99 
100  void destructLevel(int level) {
101  spec.destructLevel(level);
102  }
103 
104  size_t hash_code(void const* p, int level) const {
105  return spec.hash_code(p, level);
106  }
107 
108  bool equal_to(void const* p, void const* q, int level) const {
109  return spec.equal_to(p, q, level);
110  }
111 
112  void print_state(std::ostream& os, void const* p, int level) const {
113  spec.print_state(os, p, level);
114  }
115 
116  void print_level(std::ostream& os, int level) const {
117  spec.print_level(os, level);
118  }
119 };
120 
121 template<typename S>
122 class ZddLookahead: public DdSpecBase<ZddLookahead<S>,S::ARITY> {
123  typedef S Spec;
124 
125  Spec spec;
126  std::vector<char> work;
127 
128  int lookahead(void* p, int level) {
129  void* const q = work.data();
130  while (level >= 1) {
131  for (int b = 1; b < Spec::ARITY; ++b) {
132  spec.get_copy(q, p);
133  if (spec.get_child(q, level, b) != 0) {
134  spec.destruct(q);
135  return level;
136  }
137  spec.destruct(q);
138  }
139  level = spec.get_child(p, level, 0);
140  }
141 
142  return level;
143  }
144 
145 public:
146  ZddLookahead(S const& s)
147  : spec(s), work(spec.datasize()) {
148  }
149 
150  int datasize() const {
151  return spec.datasize();
152  }
153 
154  int get_root(void* p) {
155  return lookahead(p, spec.get_root(p));
156  }
157 
158  int get_child(void* p, int level, int b) {
159  return lookahead(p, spec.get_child(p, level, b));
160  }
161 
162  void get_copy(void* to, void const* from) {
163  spec.get_copy(to, from);
164  }
165 
166  int merge_states(void* p1, void* p2) {
167  return spec.merge_states(p1, p2);
168  }
169 
170  void destruct(void* p) {
171  spec.destruct(p);
172  }
173 
174  void destructLevel(int level) {
175  spec.destructLevel(level);
176  }
177 
178  size_t hash_code(void const* p, int level) const {
179  return spec.hash_code(p, level);
180  }
181 
182  bool equal_to(void const* p, void const* q, int level) const {
183  return spec.equal_to(p, q, level);
184  }
185 
186  void print_state(std::ostream& os, void const* p, int level) const {
187  spec.print_state(os, p, level);
188  }
189 
190  void print_level(std::ostream& os, int level) const {
191  spec.print_level(os, level);
192  }
193 };
194 
195 } // namespace tdzdd