TdZdd  1.1
A top-down/breadth-first decision diagram manipulation framework
BinaryOperation.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 
30 #include "../DdSpec.hpp"
31 
32 namespace tdzdd {
33 
34 template<typename S, typename S1, typename S2>
35 class BinaryOperation: public PodArrayDdSpec<S,size_t,2> {
36 protected:
37  typedef S1 Spec1;
38  typedef S2 Spec2;
39  typedef size_t Word;
40 
41  static size_t const levelWords = (sizeof(int[2]) + sizeof(Word) - 1)
42  / sizeof(Word);
43 
44  Spec1 spec1;
45  Spec2 spec2;
46  int const stateWords1;
47  int const stateWords2;
48 
49  static int wordSize(int size) {
50  return (size + sizeof(Word) - 1) / sizeof(Word);
51  }
52 
53  void setLevel1(void* p, int level) const {
54  static_cast<int*>(p)[0] = level;
55  }
56 
57  int level1(void const* p) const {
58  return static_cast<int const*>(p)[0];
59  }
60 
61  void setLevel2(void* p, int level) const {
62  static_cast<int*>(p)[1] = level;
63  }
64 
65  int level2(void const* p) const {
66  return static_cast<int const*>(p)[1];
67  }
68 
69  void* state1(void* p) const {
70  return static_cast<Word*>(p) + levelWords;
71  }
72 
73  void const* state1(void const* p) const {
74  return static_cast<Word const*>(p) + levelWords;
75  }
76 
77  void* state2(void* p) const {
78  return static_cast<Word*>(p) + levelWords + stateWords1;
79  }
80 
81  void const* state2(void const* p) const {
82  return static_cast<Word const*>(p) + levelWords + stateWords1;
83  }
84 
85 public:
86  BinaryOperation(S1 const& s1, S2 const& s2) :
87  spec1(s1),
88  spec2(s2),
89  stateWords1(wordSize(spec1.datasize())),
90  stateWords2(wordSize(spec2.datasize())) {
91  BinaryOperation::setArraySize(levelWords + stateWords1 + stateWords2);
92  }
93 
94  void get_copy(void* to, void const* from) {
95  setLevel1(to, level1(from));
96  setLevel2(to, level2(from));
97  spec1.get_copy(state1(to), state1(from));
98  spec2.get_copy(state2(to), state2(from));
99  }
100 
101  int merge_states(void* p1, void* p2) {
102  return spec1.merge_states(state1(p1), state1(p2))
103  | spec2.merge_states(state2(p1), state2(p2));
104  }
105 
106  void destruct(void* p) {
107  spec1.destruct(state1(p));
108  spec2.destruct(state2(p));
109  }
110 
111  void destructLevel(int level) {
112  spec1.destructLevel(level);
113  spec2.destructLevel(level);
114  }
115 
116  size_t hash_code(void const* p, int level) const {
117  size_t h = size_t(level1(p)) * 314159257
118  + size_t(level2(p)) * 271828171;
119  if (level1(p) > 0)
120  h += spec1.hash_code(state1(p), level1(p)) * 171828143;
121  if (level2(p) > 0)
122  h += spec2.hash_code(state2(p), level2(p)) * 141421333;
123  return h;
124  }
125 
126  bool equal_to(void const* p, void const* q, int level) const {
127  if (level1(p) != level1(q)) return false;
128  if (level2(p) != level2(q)) return false;
129  if (level1(p) > 0 && !spec1.equal_to(state1(p), state1(q), level1(p)))
130  return false;
131  if (level2(p) > 0 && !spec2.equal_to(state2(p), state2(q), level2(p)))
132  return false;
133  return true;
134  }
135 };
136 
137 #if __cplusplus >= 201103L
138 template<typename ... SS> struct BddAnd;
139 
140 template<typename S, typename S1, typename ... SS>
141 struct BddAnd_: public BddAnd_<S,S1,BddAnd<SS...>> {
142  typedef BddAnd_<S,S1,BddAnd<SS...>> base;
143  typedef typename base::Word Word;
144 
145  BddAnd_(S1 const& s1, SS const&... ss) :
146  base(s1, BddAnd<SS...>(ss...)) {
147  }
148 
149  void print_state(std::ostream& os, void const* p, int level) const {
150  Word const* q = static_cast<Word const*>(p);
151  os << "<" << base::level1(q) << ",";
152  base::spec1.print_state(os, base::state1(q), level);
153  os << ">∧";
154  base::spec2.print_state(os, base::state2(q), level);
155  }
156 };
157 #endif
158 
159 template<typename S, typename S1, typename S2>
160 struct BddAnd_
161 #if __cplusplus >= 201103L
162 <S,S1,S2>
163 #endif
164  : public BinaryOperation<S,S1,S2> {
165  typedef BinaryOperation<S,S1,S2> base;
166  typedef typename base::Word Word;
167 
168  BddAnd_(S1 const& s1, S2 const& s2) :
169  base(s1, s2) {
170  }
171 
172  int getRoot(Word* p) {
173  int i1 = base::spec1.get_root(base::state1(p));
174  if (i1 == 0) return 0;
175  int i2 = base::spec2.get_root(base::state2(p));
176  if (i2 == 0) return 0;
177  base::setLevel1(p, i1);
178  base::setLevel2(p, i2);
179  return std::max(base::level1(p), base::level2(p));
180  }
181 
182  int getChild(Word* p, int level, int take) {
183  assert(base::level1(p) <= level && base::level2(p) <= level);
184  if (base::level1(p) == level) {
185  int i1 = base::spec1.get_child(base::state1(p), level, take);
186  if (i1 == 0) return 0;
187  base::setLevel1(p, i1);
188  }
189  if (base::level2(p) == level) {
190  int i2 = base::spec2.get_child(base::state2(p), level, take);
191  if (i2 == 0) return 0;
192  base::setLevel2(p, i2);
193  }
194  return std::max(base::level1(p), base::level2(p));
195  }
196 
197  void print_state(std::ostream& os, void const* p, int level) const {
198  Word const* q = static_cast<Word const*>(p);
199  os << "<" << base::level1(q) << ",";
200  base::spec1.print_state(os, base::state1(q), level);
201  os << ">∧<" << base::level2(q) << ",";
202  base::spec2.print_state(os, base::state2(q), level);
203  os << ">";
204  }
205 };
206 
207 #if __cplusplus >= 201103L
208 template<typename ... SS> struct BddOr;
209 
210 template<typename S, typename S1, typename ... SS>
211 struct BddOr_: public BddOr_<S,S1,BddOr<SS...>> {
212  typedef BddOr_<S,S1,BddOr<SS...>> base;
213  typedef typename base::Word Word;
214 
215  BddOr_(S1 const& s1, SS const&... ss) :
216  base(s1, BddOr<SS...>(ss...)) {
217  }
218 
219  void print_state(std::ostream& os, void const* p, int level) const {
220  Word const* q = static_cast<Word const*>(p);
221  os << "<" << base::level1(q) << ",";
222  base::spec1.print_state(os, base::state1(q), level);
223  os << ">∨";
224  base::spec2.print_state(os, base::state2(q), level);
225  }
226 };
227 #endif
228 
229 template<typename S, typename S1, typename S2>
230 struct BddOr_
231 #if __cplusplus >= 201103L
232 <S,S1,S2>
233 #endif
234  : public BinaryOperation<S,S1,S2> {
235  typedef BinaryOperation<S,S1,S2> base;
236  typedef typename base::Word Word;
237 
238  BddOr_(S1 const& s1, S2 const& s2) :
239  base(s1, s2) {
240  }
241 
242  int getRoot(Word* p) {
243  int i1 = base::spec1.get_root(base::state1(p));
244  if (i1 < 0) return -1;
245  int i2 = base::spec2.get_root(base::state2(p));
246  if (i2 < 0) return -1;
247  base::setLevel1(p, i1);
248  base::setLevel2(p, i2);
249  return std::max(base::level1(p), base::level2(p));
250  }
251 
252  int getChild(Word* p, int level, int take) {
253  assert(base::level1(p) <= level && base::level2(p) <= level);
254 
255  if (base::level1(p) == level) {
256  int i1 = base::spec1.get_child(base::state1(p), level, take);
257  if (i1 < 0) return -1;
258  base::setLevel1(p, i1);
259  }
260 
261  if (base::level2(p) == level) {
262  int i2 = base::spec2.get_child(base::state2(p), level, take);
263  if (i2 < 0) return -1;
264  base::setLevel2(p, i2);
265  }
266 
267  return std::max(base::level1(p), base::level2(p));
268  }
269 
270  void print_state(std::ostream& os, void const* p, int level) const {
271  Word const* q = static_cast<Word const*>(p);
272  os << "<" << base::level1(q) << ",";
273  base::spec1.print_state(os, base::state1(q), level);
274  os << ">∨<" << base::level2(q) << ",";
275  base::spec2.print_state(os, base::state2(q), level);
276  os << ">";
277  }
278 };
279 
280 #if __cplusplus >= 201103L
281 template<typename ... SS> struct ZddIntersection;
282 
283 template<typename S, typename S1, typename ... SS>
284 struct ZddIntersection_: public ZddIntersection_<S,S1,ZddIntersection<SS...>> {
285  typedef ZddIntersection_<S,S1,ZddIntersection<SS...>> base;
286  typedef typename base::Word Word;
287 
288  ZddIntersection_(S1 const& s1, SS const&... ss) :
289  base(s1, ZddIntersection<SS...>(ss...)) {
290  }
291 
292  void print_state(std::ostream& os, void const* p, int level) const {
293  Word const* q = static_cast<Word const*>(p);
294  os << "<" << base::level1(q) << ",";
295  base::spec1.print_state(os, base::state1(q), level);
296  os << ">∩";
297  base::spec2.print_state(os, base::state2(q), level);
298  }
299 };
300 #endif
301 
302 template<typename S, typename S1, typename S2>
303 struct ZddIntersection_
304 #if __cplusplus >= 201103L
305 <S,S1,S2>
306 #endif
307  : public PodArrayDdSpec<S,size_t,2> {
308  typedef S1 Spec1;
309  typedef S2 Spec2;
310  typedef size_t Word;
311 
312  Spec1 spec1;
313  Spec2 spec2;
314  int const stateWords1;
315  int const stateWords2;
316 
317  static int wordSize(int size) {
318  return (size + sizeof(Word) - 1) / sizeof(Word);
319  }
320 
321  void* state1(void* p) const {
322  return p;
323  }
324 
325  void const* state1(void const* p) const {
326  return p;
327  }
328 
329  void* state2(void* p) const {
330  return static_cast<Word*>(p) + stateWords1;
331  }
332 
333  void const* state2(void const* p) const {
334  return static_cast<Word const*>(p) + stateWords1;
335  }
336 
337 public:
338  ZddIntersection_(S1 const& s1, S2 const& s2) :
339  spec1(s1),
340  spec2(s2),
341  stateWords1(wordSize(spec1.datasize())),
342  stateWords2(wordSize(spec2.datasize())) {
343  ZddIntersection_::setArraySize(stateWords1 + stateWords2);
344  }
345 
346  int getRoot(Word* p) {
347  int i1 = spec1.get_root(state1(p));
348  if (i1 == 0) return 0;
349  int i2 = spec2.get_root(state2(p));
350  if (i2 == 0) return 0;
351 
352  while (i1 != i2) {
353  if (i1 > i2) {
354  i1 = spec1.get_child(state1(p), i1, 0);
355  if (i1 == 0) return 0;
356  }
357  else {
358  i2 = spec2.get_child(state2(p), i2, 0);
359  if (i2 == 0) return 0;
360  }
361  }
362 
363  return i1;
364  }
365 
366  int getChild(Word* p, int level, int take) {
367  int i1 = spec1.get_child(state1(p), level, take);
368  if (i1 == 0) return 0;
369  int i2 = spec2.get_child(state2(p), level, take);
370  if (i2 == 0) return 0;
371 
372  while (i1 != i2) {
373  if (i1 > i2) {
374  i1 = spec1.get_child(state1(p), i1, 0);
375  if (i1 == 0) return 0;
376  }
377  else {
378  i2 = spec2.get_child(state2(p), i2, 0);
379  if (i2 == 0) return 0;
380  }
381  }
382 
383  return i1;
384  }
385 
386  void get_copy(void* to, void const* from) {
387  spec1.get_copy(state1(to), state1(from));
388  spec2.get_copy(state2(to), state2(from));
389  }
390 
391  int merge_states(void* p1, void* p2) {
392  return spec1.merge_states(state1(p1), state1(p2))
393  | spec2.merge_states(state2(p1), state2(p2));
394  }
395 
396  void destruct(void* p) {
397  spec1.destruct(state1(p));
398  spec2.destruct(state2(p));
399  }
400 
401  void destructLevel(int level) {
402  spec1.destructLevel(level);
403  spec2.destructLevel(level);
404  }
405 
406  size_t hash_code(void const* p, int level) const {
407  return spec1.hash_code(state1(p), level) * 314159257
408  + spec2.hash_code(state2(p), level) * 271828171;
409  }
410 
411  bool equal_to(void const* p, void const* q, int level) const {
412  return spec1.equal_to(state1(p), state1(q), level)
413  && spec2.equal_to(state2(p), state2(q), level);
414  }
415 
416  void print_state(std::ostream& os, void const* p, int level) const {
417  Word const* q = static_cast<Word const*>(p);
418  os << "<";
419  spec1.print_state(os, state1(q), level);
420  os << ">∩<";
421  spec2.print_state(os, state2(q), level);
422  os << ">";
423  }
424 };
425 
426 #if __cplusplus >= 201103L
427 template<typename ... SS> struct ZddUnion;
428 
429 template<typename S, typename S1, typename ... SS>
430 struct ZddUnion_: public ZddUnion_<S,S1,ZddUnion<SS...>> {
431  typedef ZddUnion_<S,S1,ZddUnion<SS...>> base;
432  typedef typename base::Word Word;
433 
434  ZddUnion_(S1 const& s1, SS const&... ss) :
435  base(s1, ZddUnion<SS...>(ss...)) {
436  }
437 
438  void print_state(std::ostream& os, void const* p, int level) const {
439  Word const* q = static_cast<Word const*>(p);
440  os << "<" << base::level1(q) << ",";
441  base::spec1.print_state(os, base::state1(q), level);
442  os << ">∪";
443  base::spec2.print_state(os, base::state2(q), level);
444  }
445 };
446 #endif
447 
448 template<typename S, typename S1, typename S2>
449 struct ZddUnion_
450 #if __cplusplus >= 201103L
451 <S,S1,S2>
452 #endif
453  : public BinaryOperation<S,S1,S2> {
454  typedef BinaryOperation<S,S1,S2> base;
455  typedef typename base::Word Word;
456 
457  ZddUnion_(S1 const& s1, S2 const& s2) :
458  base(s1, s2) {
459  }
460 
461  int getRoot(Word* p) {
462  int i1 = base::spec1.get_root(base::state1(p));
463  int i2 = base::spec2.get_root(base::state2(p));
464  if (i1 == 0 && i2 == 0) return 0;
465  if (i1 <= 0 && i2 <= 0) return -1;
466  base::setLevel1(p, i1);
467  base::setLevel2(p, i2);
468  return std::max(base::level1(p), base::level2(p));
469  }
470 
471  int getChild(Word* p, int level, int take) {
472  assert(base::level1(p) <= level && base::level2(p) <= level);
473 
474  if (base::level1(p) == level) {
475  int i1 = base::spec1.get_child(base::state1(p), level, take);
476  base::setLevel1(p, i1);
477  }
478  else if (take) {
479  base::setLevel1(p, 0);
480  }
481 
482  if (base::level2(p) == level) {
483  int i2 = base::spec2.get_child(base::state2(p), level, take);
484  base::setLevel2(p, i2);
485  }
486  else if (take) {
487  base::setLevel2(p, 0);
488  }
489 
490  if (base::level1(p) == 0 && base::level2(p) == 0) return 0;
491  if (base::level1(p) <= 0 && base::level2(p) <= 0) return -1;
492  return std::max(base::level1(p), base::level2(p));
493  }
494 
495  void print_state(std::ostream& os, void const* p, int level) const {
496  Word const* q = static_cast<Word const*>(p);
497  os << "<" << base::level1(q) << ",";
498  base::spec1.print_state(os, base::state1(q), level);
499  os << ">∪<" << base::level2(q) << ",";
500  base::spec2.print_state(os, base::state2(q), level);
501  os << ">";
502  }
503 };
504 
505 #if __cplusplus >= 201103L
506 template<typename ... SS>
507 struct BddAnd: public BddAnd_<BddAnd<SS...>,SS...> {
508  BddAnd(SS const&... ss) :
509  BddAnd_<BddAnd,SS...>(ss...) {
510  }
511 };
512 
513 template<typename ... SS>
514 struct BddOr: public BddOr_<BddOr<SS...>,SS...> {
515  BddOr(SS const&... ss) :
516  BddOr_<BddOr,SS...>(ss...) {
517  }
518 };
519 
520 template<typename ... SS>
521 struct ZddIntersection: public ZddIntersection_<ZddIntersection<SS...>,SS...> {
522  ZddIntersection(SS const&... ss) :
523  ZddIntersection_<ZddIntersection,SS...>(ss...) {
524  }
525 };
526 
527 template<typename ... SS>
528 struct ZddUnion: public ZddUnion_<ZddUnion<SS...>,SS...> {
529  ZddUnion(SS const&... ss) :
530  ZddUnion_<ZddUnion,SS...>(ss...) {
531  }
532 };
533 
534 #else
535 
536 template<typename S1, typename S2>
537 struct BddAnd: public BddAnd_<BddAnd<S1,S2>,S1,S2> {
538  BddAnd(S1 const& s1, S2 const& s2) :
539  BddAnd_<BddAnd,S1,S2>(s1, s2) {
540  }
541 };
542 
543 template<typename S1, typename S2>
544 struct BddOr: public BddOr_<BddOr<S1,S2>,S1,S2> {
545  BddOr(S1 const& s1, S2 const& s2) :
546  BddOr_<BddOr,S1,S2>(s1, s2) {
547  }
548 };
549 
550 template<typename S1, typename S2>
551 struct ZddIntersection: public ZddIntersection_<ZddIntersection<S1,S2>,S1,S2> {
552  ZddIntersection(S1 const& s1, S2 const& s2) :
553  ZddIntersection_<ZddIntersection,S1,S2>(s1, s2) {
554  }
555 };
556 
557 template<typename S1, typename S2>
558 struct ZddUnion: public ZddUnion_<ZddUnion<S1,S2>,S1,S2> {
559  ZddUnion(S1 const& s1, S2 const& s2) :
560  ZddUnion_<ZddUnion,S1,S2>(s1, s2) {
561  }
562 };
563 #endif
564 
565 }
566  // namespace tdzdd