30 #include "../DdSpec.hpp" 34 template<
typename S,
typename S1,
typename S2>
35 class BinaryOperation:
public PodArrayDdSpec<S,size_t,2> {
41 static size_t const levelWords = (
sizeof(
int[2]) +
sizeof(Word) - 1)
46 int const stateWords1;
47 int const stateWords2;
49 static int wordSize(
int size) {
50 return (size +
sizeof(Word) - 1) /
sizeof(Word);
53 void setLevel1(
void* p,
int level)
const {
54 static_cast<int*
>(p)[0] = level;
57 int level1(
void const* p)
const {
58 return static_cast<int const*
>(p)[0];
61 void setLevel2(
void* p,
int level)
const {
62 static_cast<int*
>(p)[1] = level;
65 int level2(
void const* p)
const {
66 return static_cast<int const*
>(p)[1];
69 void* state1(
void* p)
const {
70 return static_cast<Word*
>(p) + levelWords;
73 void const* state1(
void const* p)
const {
74 return static_cast<Word const*
>(p) + levelWords;
77 void* state2(
void* p)
const {
78 return static_cast<Word*
>(p) + levelWords + stateWords1;
81 void const* state2(
void const* p)
const {
82 return static_cast<Word const*
>(p) + levelWords + stateWords1;
86 BinaryOperation(S1
const& s1, S2
const& s2) :
89 stateWords1(wordSize(spec1.datasize())),
90 stateWords2(wordSize(spec2.datasize())) {
91 BinaryOperation::setArraySize(levelWords + stateWords1 + stateWords2);
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));
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));
106 void destruct(
void* p) {
107 spec1.destruct(state1(p));
108 spec2.destruct(state2(p));
111 void destructLevel(
int level) {
112 spec1.destructLevel(level);
113 spec2.destructLevel(level);
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;
120 h += spec1.hash_code(state1(p), level1(p)) * 171828143;
122 h += spec2.hash_code(state2(p), level2(p)) * 141421333;
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)))
131 if (level2(p) > 0 && !spec2.equal_to(state2(p), state2(q), level2(p)))
137 #if __cplusplus >= 201103L 138 template<
typename ... SS>
struct BddAnd;
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;
145 BddAnd_(S1
const& s1, SS
const&... ss) :
146 base(s1, BddAnd<SS...>(ss...)) {
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);
154 base::spec2.print_state(os, base::state2(q), level);
159 template<
typename S,
typename S1,
typename S2>
161 #if __cplusplus >= 201103L
164 :
public BinaryOperation<S,S1,S2> {
165 typedef BinaryOperation<S,S1,S2> base;
166 typedef typename base::Word Word;
168 BddAnd_(S1
const& s1, S2
const& s2) :
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));
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);
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);
194 return std::max(base::level1(p), base::level2(p));
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);
207 #if __cplusplus >= 201103L 208 template<
typename ... SS>
struct BddOr;
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;
215 BddOr_(S1
const& s1, SS
const&... ss) :
216 base(s1, BddOr<SS...>(ss...)) {
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);
224 base::spec2.print_state(os, base::state2(q), level);
229 template<
typename S,
typename S1,
typename S2>
231 #if __cplusplus >= 201103L
234 :
public BinaryOperation<S,S1,S2> {
235 typedef BinaryOperation<S,S1,S2> base;
236 typedef typename base::Word Word;
238 BddOr_(S1
const& s1, S2
const& s2) :
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));
252 int getChild(Word* p,
int level,
int take) {
253 assert(base::level1(p) <= level && base::level2(p) <= level);
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);
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);
267 return std::max(base::level1(p), base::level2(p));
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);
280 #if __cplusplus >= 201103L 281 template<
typename ... SS>
struct ZddIntersection;
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;
288 ZddIntersection_(S1
const& s1, SS
const&... ss) :
289 base(s1, ZddIntersection<SS...>(ss...)) {
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);
297 base::spec2.print_state(os, base::state2(q), level);
302 template<
typename S,
typename S1,
typename S2>
303 struct ZddIntersection_
304 #if __cplusplus >= 201103L
307 :
public PodArrayDdSpec<S,size_t,2> {
314 int const stateWords1;
315 int const stateWords2;
317 static int wordSize(
int size) {
318 return (size +
sizeof(Word) - 1) /
sizeof(Word);
321 void* state1(
void* p)
const {
325 void const* state1(
void const* p)
const {
329 void* state2(
void* p)
const {
330 return static_cast<Word*
>(p) + stateWords1;
333 void const* state2(
void const* p)
const {
334 return static_cast<Word const*
>(p) + stateWords1;
338 ZddIntersection_(S1
const& s1, S2
const& s2) :
341 stateWords1(wordSize(spec1.datasize())),
342 stateWords2(wordSize(spec2.datasize())) {
343 ZddIntersection_::setArraySize(stateWords1 + stateWords2);
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;
354 i1 = spec1.get_child(state1(p), i1, 0);
355 if (i1 == 0)
return 0;
358 i2 = spec2.get_child(state2(p), i2, 0);
359 if (i2 == 0)
return 0;
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;
374 i1 = spec1.get_child(state1(p), i1, 0);
375 if (i1 == 0)
return 0;
378 i2 = spec2.get_child(state2(p), i2, 0);
379 if (i2 == 0)
return 0;
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));
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));
396 void destruct(
void* p) {
397 spec1.destruct(state1(p));
398 spec2.destruct(state2(p));
401 void destructLevel(
int level) {
402 spec1.destructLevel(level);
403 spec2.destructLevel(level);
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;
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);
416 void print_state(std::ostream& os,
void const* p,
int level)
const {
417 Word
const* q =
static_cast<Word const*
>(p);
419 spec1.print_state(os, state1(q), level);
421 spec2.print_state(os, state2(q), level);
426 #if __cplusplus >= 201103L 427 template<
typename ... SS>
struct ZddUnion;
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;
434 ZddUnion_(S1
const& s1, SS
const&... ss) :
435 base(s1, ZddUnion<SS...>(ss...)) {
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);
443 base::spec2.print_state(os, base::state2(q), level);
448 template<
typename S,
typename S1,
typename S2>
450 #if __cplusplus >= 201103L
453 :
public BinaryOperation<S,S1,S2> {
454 typedef BinaryOperation<S,S1,S2> base;
455 typedef typename base::Word Word;
457 ZddUnion_(S1
const& s1, S2
const& s2) :
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));
471 int getChild(Word* p,
int level,
int take) {
472 assert(base::level1(p) <= level && base::level2(p) <= level);
474 if (base::level1(p) == level) {
475 int i1 = base::spec1.get_child(base::state1(p), level, take);
476 base::setLevel1(p, i1);
479 base::setLevel1(p, 0);
482 if (base::level2(p) == level) {
483 int i2 = base::spec2.get_child(base::state2(p), level, take);
484 base::setLevel2(p, i2);
487 base::setLevel2(p, 0);
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));
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);
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...) {
513 template<
typename ... SS>
514 struct BddOr:
public BddOr_<BddOr<SS...>,SS...> {
515 BddOr(SS
const&... ss) :
516 BddOr_<BddOr,SS...>(ss...) {
520 template<
typename ... SS>
521 struct ZddIntersection:
public ZddIntersection_<ZddIntersection<SS...>,SS...> {
522 ZddIntersection(SS
const&... ss) :
523 ZddIntersection_<ZddIntersection,SS...>(ss...) {
527 template<
typename ... SS>
528 struct ZddUnion:
public ZddUnion_<ZddUnion<SS...>,SS...> {
529 ZddUnion(SS
const&... ss) :
530 ZddUnion_<ZddUnion,SS...>(ss...) {
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) {
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) {
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) {
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) {