1 // -*- c++ -*-
2 //*****************************************************************************
3 /** @file pbori_algo.h
4 *
5 * @author Alexander Dreyer
6 * @date 2006-04-07
7 *
8 * This file includes some templates of simple transformations and similar
9 * procedures.
10 *
11 * @note This file carries pure template routines. Algorithms, which make
12 * explicite use of PolyBoRi classes can be found in pbori_algorithms.h
13 *
14 * @par Copyright:
15 * (c) 2006 by The PolyBoRi Team
16 **/
17 //*****************************************************************************
18
19 #ifndef polybori_routines_pbori_algo_h_
20 #define polybori_routines_pbori_algo_h_
21
22 // include polybori's definitions
23 #include <polybori/pbori_defs.h>
24
25 // get polybori's functionals
26 #include "pbori_func.h"
27 #include <polybori/common/traits.h>
28
29 // temporarily
30 #include <polybori/cudd/cudd.h>
31 #include <polybori/ring/CCuddInterface.h>
32
33 BEGIN_NAMESPACE_PBORI
34
35
36 /// Function templates for transforming decision diagrams
37 template< class NaviType, class TermType,
38 class TernaryOperator,
39 class TerminalOperator >
40 TermType
dd_backward_transform(NaviType navi,TermType init,TernaryOperator newNode,TerminalOperator terminate)41 dd_backward_transform( NaviType navi, TermType init, TernaryOperator newNode,
42 TerminalOperator terminate ) {
43
44 TermType result = init;
45
46 if (navi.isConstant()) { // Reached end of path
47 if (navi.terminalValue()){ // Case of a valid path
48 result = terminate();
49 }
50 }
51 else {
52 result = dd_backward_transform(navi.thenBranch(), init, newNode, terminate);
53 result = newNode(*navi, result,
54 dd_backward_transform(navi.elseBranch(), init, newNode,
55 terminate) );
56 }
57 return result;
58 }
59
60
61 /// Function templates for transforming decision diagrams
62 template< class NaviType, class TermType, class OutIterator,
63 class ThenBinaryOperator, class ElseBinaryOperator,
64 class TerminalOperator >
65 OutIterator
dd_transform(NaviType navi,TermType init,OutIterator result,ThenBinaryOperator then_binop,ElseBinaryOperator else_binop,TerminalOperator terminate)66 dd_transform( NaviType navi, TermType init, OutIterator result,
67 ThenBinaryOperator then_binop, ElseBinaryOperator else_binop,
68 TerminalOperator terminate ) {
69
70
71 if (navi.isConstant()) { // Reached end of path
72 if (navi.terminalValue()){ // Case of a valid path
73 *result = terminate(init);
74 ++result;
75 }
76 }
77 else {
78 result = dd_transform(navi.thenBranch(), then_binop(init, *navi), result,
79 then_binop, else_binop, terminate);
80 result = dd_transform(navi.elseBranch(), else_binop(init, *navi), result,
81 then_binop, else_binop, terminate);
82 }
83 return result;
84 }
85
86 /// Function templates for transforming decision diagrams
87 /// with special treatment of the leading term
88 template< class NaviType, class TermType, class OutIterator,
89 class ThenBinaryOperator, class ElseBinaryOperator,
90 class TerminalOperator, class FirstTermOp >
91 OutIterator
dd_transform(NaviType navi,TermType init,OutIterator result,ThenBinaryOperator then_binop,ElseBinaryOperator else_binop,TerminalOperator terminate,FirstTermOp terminate_first)92 dd_transform( NaviType navi, TermType init, OutIterator result,
93 ThenBinaryOperator then_binop, ElseBinaryOperator else_binop,
94 TerminalOperator terminate, FirstTermOp terminate_first ) {
95
96 if (navi.isConstant()) { // Reached end of path
97 if (navi.terminalValue()){ // Case of a valid path - here leading term
98 *result = terminate_first(init);
99 ++result;
100 }
101 }
102 else {
103 result = dd_transform(navi.thenBranch(), then_binop(init, *navi), result,
104 then_binop, else_binop, terminate, terminate_first);
105 result = dd_transform(navi.elseBranch(), else_binop(init, *navi), result,
106 then_binop, else_binop, terminate);
107 }
108 return result;
109 }
110
111 /// Function templates for transforming decision diagrams
112 template< class NaviType, class TermType, class OutIterator,
113 class ThenBinaryOperator, class ElseBinaryOperator >
114 void
dd_transform(const NaviType & navi,const TermType & init,const OutIterator & result,const ThenBinaryOperator & then_binop,const ElseBinaryOperator & else_binop)115 dd_transform( const NaviType& navi, const TermType& init,
116 const OutIterator& result,
117 const ThenBinaryOperator& then_binop,
118 const ElseBinaryOperator& else_binop ) {
119
120 dd_transform(navi, init, result, then_binop, else_binop,
121 project_ith<1>() );
122 }
123
124 /// Function templates for transforming decision diagrams
125 template< class NaviType, class TermType, class OutIterator,
126 class ThenBinaryOperator >
127 void
dd_transform(const NaviType & navi,const TermType & init,const OutIterator & result,const ThenBinaryOperator & then_binop)128 dd_transform( const NaviType& navi, const TermType& init,
129 const OutIterator& result,
130 const ThenBinaryOperator& then_binop ) {
131
132 dd_transform(navi, init, result, then_binop,
133 project_ith<1, 2>(),
134 project_ith<1>() );
135 }
136
137
138 template <class InputIterator, class OutputIterator,
139 class FirstFunction, class UnaryFunction>
140 OutputIterator
special_first_transform(InputIterator first,InputIterator last,OutputIterator result,UnaryFunction op,FirstFunction firstop)141 special_first_transform(InputIterator first, InputIterator last,
142 OutputIterator result,
143 UnaryFunction op, FirstFunction firstop) {
144 InputIterator second(first);
145 if (second != last) {
146 ++second;
147 result = std::transform(first, second, result, firstop);
148 }
149 return std::transform(second, last, result, op);
150 }
151
152
153 /// Function templates doing a reversed copy using intermediate storage
154 template <class InputIterator, class Intermediate, class OutputIterator>
155 OutputIterator
reversed_inter_copy(InputIterator start,InputIterator finish,Intermediate & inter,OutputIterator output)156 reversed_inter_copy( InputIterator start, InputIterator finish,
157 Intermediate& inter, OutputIterator output ) {
158
159 std::copy(start, finish, inter.begin());
160 // force constant
161 return std::copy( const_cast<const Intermediate&>(inter).rbegin(),
162 const_cast<const Intermediate&>(inter).rend(),
163 output );
164 }
165
166 /// Function templates for checking whether a given decision diagram node is on
167 /// path
168 template <class NaviType>
169 bool
dd_on_path(NaviType navi)170 dd_on_path(NaviType navi) {
171
172 if (navi.isConstant())
173 return navi.terminalValue();
174
175 return dd_on_path(navi.thenBranch()) || dd_on_path(navi.elseBranch());
176 }
177
178 /// Function templates for checking whether a given decision diagram contains
179 /// paths with indices only in range [start, finish)
180 template <class NaviType, class OrderedIterator>
181 bool
dd_owns_term_of_indices(NaviType navi,OrderedIterator start,OrderedIterator finish)182 dd_owns_term_of_indices(NaviType navi,
183 OrderedIterator start, OrderedIterator finish) {
184
185 if (!navi.isConstant()) { // Not at end of path
186 bool not_at_end;
187
188 while( (not_at_end = (start != finish)) && (*start < *navi) )
189 ++start;
190
191 NaviType elsenode = navi.elseBranch();
192
193 if (elsenode.isConstant() && elsenode.terminalValue())
194 return true;
195
196
197 if (not_at_end){
198
199 if ( (*start == *navi) &&
200 dd_owns_term_of_indices(navi.thenBranch(), start, finish))
201 return true;
202 else
203 return dd_owns_term_of_indices(elsenode, start, finish);
204 }
205 else {
206
207 while(!elsenode.isConstant())
208 elsenode.incrementElse();
209 return elsenode.terminalValue();
210 }
211
212 }
213 return navi.terminalValue();
214 }
215
216 /// Function templates extracting the terms of a given decision diagram contain
217 /// which contains only indices from the range [start, finish)
218 /// Note: Returns incremented node
219 template <class NaviType, class OrderedIterator, class NodeOperation>
220 NaviType
dd_intersect_some_index(NaviType navi,OrderedIterator start,OrderedIterator finish,NodeOperation newNode)221 dd_intersect_some_index(NaviType navi,
222 OrderedIterator start, OrderedIterator finish,
223 NodeOperation newNode ) {
224
225 if (!navi.isConstant()) { // Not at end of path
226 bool not_at_end;
227 while( (not_at_end = (start != finish)) && (*start < *navi) )
228 ++start;
229
230 if (not_at_end) {
231 NaviType elseNode =
232 dd_intersect_some_index(navi.elseBranch(), start, finish,
233 newNode);
234
235 if (*start == *navi) {
236
237 NaviType thenNode =
238 dd_intersect_some_index(navi.thenBranch(), start, finish,
239 newNode);
240
241 return newNode(*start, navi, thenNode, elseNode);
242 }
243 else
244 return elseNode;
245 }
246 else { // if the start == finish, we only check
247 // validity of the else-only branch
248 while(!navi.isConstant())
249 navi = navi.elseBranch();
250 return newNode(navi);
251 }
252
253 }
254
255 return newNode(navi);
256 }
257
258
259
260 /// Function templates for debugging, prints dd indices and reference counts
261 template <class NaviType>
262 void
dd_print(NaviType navi)263 dd_print(NaviType navi) {
264
265 if (!navi.isConstant()) { // Not at end of path
266
267 std::cout << std::endl<< "idx " << *navi <<" addr "<<
268 ((DdNode*)navi)<<" ref "<<
269 int(PBORI_PREFIX(Cudd_Regular)((DdNode*)navi)->ref) << std::endl;
270
271 dd_print(navi.thenBranch());
272 dd_print(navi.elseBranch());
273
274 }
275 else {
276 std::cout << "const isvalid? "<<navi.isValid()<<" addr "
277 <<((DdNode*)navi)<<" ref "<<
278 int(PBORI_PREFIX(Cudd_Regular)((DdNode*)navi)->ref)<<std::endl;
279
280 }
281 }
282
283 // Determinine the minimum of the distance between two iterators and limit
284 template <class IteratorType, class SizeType>
285 SizeType
limited_distance(IteratorType start,IteratorType finish,SizeType limit)286 limited_distance(IteratorType start, IteratorType finish, SizeType limit) {
287
288 SizeType result = 0;
289
290 while ((result < limit) && (start != finish)) {
291 ++start, ++result;
292 }
293
294 return result;
295 }
296
297 #if 0
298 // Forward declaration of CTermIter template
299 template <class, class, class, class, class, class> class CTermIter;
300
301 // Determinine the minimum of the number of terms and limit
302 template <class NaviType, class SizeType>
303 SizeType
304 limited_length(NaviType navi, SizeType limit) {
305
306
307 typedef CTermIter<dummy_iterator, NaviType,
308 project_ith<1>, project_ith<1>, project_ith<1, 2>,
309 project_ith<1> >
310 iterator;
311
312 return limited_distance(iterator(navi), iterator(), limit);
313 }
314 #endif
315
316 /// Test whether the empty set is included
317 template <class NaviType>
owns_one(NaviType navi)318 bool owns_one(NaviType navi) {
319 while (!navi.isConstant() )
320 navi.incrementElse();
321
322 return navi.terminalValue();
323 }
324
325 template <class CacheMgr, class NaviType, class SetType>
326 SetType
dd_modulo_monomials(const CacheMgr & cache_mgr,NaviType navi,NaviType rhs,const SetType & init)327 dd_modulo_monomials(const CacheMgr& cache_mgr,
328 NaviType navi, NaviType rhs, const SetType& init){
329
330 // Managing trivial cases
331 if (owns_one(rhs)) return cache_mgr.zero();
332
333 if (navi.isConstant())
334 return cache_mgr.generate(navi);
335
336 typename SetType::idx_type index = *navi;
337 while(*rhs < index )
338 rhs.incrementElse();
339
340 if (rhs.isConstant())
341 return cache_mgr.generate(navi);
342
343 if (rhs == navi)
344 return cache_mgr.zero();
345
346 // Cache look-up
347 NaviType cached = cache_mgr.find(navi, rhs);
348 if (cached.isValid())
349 return cache_mgr.generate(cached);
350
351 // Actual computations
352 SetType result(cache_mgr.zero());
353 if (index == *rhs){
354
355 NaviType rhselse = rhs.elseBranch();
356 SetType thenres =
357 dd_modulo_monomials(cache_mgr, navi.thenBranch(), rhs.thenBranch(), init);
358
359 result =
360 SetType(index,
361 dd_modulo_monomials(cache_mgr,
362 thenres.navigation(), rhselse, init),
363 dd_modulo_monomials(cache_mgr,
364 navi.elseBranch(), rhselse, init)
365 );
366
367 }
368 else {
369 PBORI_ASSERT(*rhs > index);
370 result =
371 SetType(index,
372 dd_modulo_monomials(cache_mgr, navi.thenBranch(), rhs, init),
373 dd_modulo_monomials(cache_mgr, navi.elseBranch(), rhs, init)
374 );
375 }
376 cache_mgr.insert(navi, rhs, result.navigation());
377 return result;
378 }
379
380 /// Get minimal elements with respect to inclusion
381 template <class CacheMgr, class ModMonCacheMgr, class NaviType, class SetType>
382 SetType
dd_minimal_elements(const CacheMgr & cache_mgr,const ModMonCacheMgr & modmon_mgr,NaviType navi,const SetType & init)383 dd_minimal_elements(const CacheMgr& cache_mgr, const ModMonCacheMgr& modmon_mgr,
384 NaviType navi, const SetType& init){
385
386 // Trivial Cases
387 if (navi.isEmpty())
388 return cache_mgr.generate(navi);
389
390 if (owns_one(navi)) return cache_mgr.one();
391
392 NaviType ms0 = navi.elseBranch();
393 NaviType ms1 = navi.thenBranch();
394
395 // Cache look-up
396 NaviType cached = cache_mgr.find(navi);
397 if (cached.isValid())
398 return cache_mgr.generate(cached);
399
400 SetType minimal_else = dd_minimal_elements(cache_mgr, modmon_mgr, ms0, init);
401 SetType minimal_then =
402 dd_minimal_elements(cache_mgr, modmon_mgr,
403 dd_modulo_monomials(modmon_mgr, ms1,
404 minimal_else.navigation(),
405 init).navigation(),
406 init);
407 SetType result(cache_mgr.zero());
408 if ( (minimal_else.navigation() == ms0)
409 && (minimal_then.navigation() == ms1) )
410 result = cache_mgr.generate(navi);
411 else
412 result = SetType(*navi, minimal_then, minimal_else);
413
414 cache_mgr.insert(navi, result.navigation());
415 return result;
416 }
417
418
419 /// A first version
420 /// Function templates extracting minimal elements of dd wrt. inclusion
421 /// Assumption, navi is navigator of dd
422 template <class NaviType, class DDType>
423 DDType
dd_minimal_elements(NaviType navi,DDType dd,DDType & multiples)424 dd_minimal_elements(NaviType navi, DDType dd, DDType& multiples) {
425
426
427 if (!navi.isConstant()) { // Not at end of path
428
429 DDType elsedd = dd.subset0(*navi);
430
431
432 DDType elseMultiples;
433 elsedd = dd_minimal_elements(navi.elseBranch(), elsedd, elseMultiples);
434
435 // short cut if else and then branche equal or else contains 1
436 if((navi.elseBranch() == navi.thenBranch()) || elsedd.blankness()){
437 multiples = elseMultiples;
438 return elsedd;
439 }
440
441 NaviType elseNavi = elseMultiples.navigation();
442
443 int nmax;
444 if (elseNavi.isConstant()){
445 if (elseNavi.terminalValue())
446 nmax = dd.nVariables();
447 else
448 nmax = *navi;
449 }
450 else
451 nmax = *elseNavi;
452
453
454 for(int i = nmax-1; i > *navi; --i){
455 elseMultiples.uniteAssign(elseMultiples.change(i));
456 }
457
458
459 DDType thendd = dd.subset1(*navi);
460 thendd = thendd.diff(elseMultiples);
461
462 DDType thenMultiples;
463 thendd = dd_minimal_elements(navi.thenBranch(), thendd, thenMultiples);
464
465 NaviType thenNavi = thenMultiples.navigation();
466
467
468 if (thenNavi.isConstant()){
469 if (thenNavi.terminalValue())
470 nmax = dd.nVariables();
471 else
472 nmax = *navi;
473 }
474 else
475 nmax = *thenNavi;
476
477
478 for(int i = nmax-1; i > *navi; --i){
479 thenMultiples.uniteAssign(thenMultiples.change(i));
480 }
481
482
483 thenMultiples = thenMultiples.unite(elseMultiples);
484 thenMultiples = thenMultiples.change(*navi);
485
486
487 multiples = thenMultiples.unite(elseMultiples);
488 thendd = thendd.change(*navi);
489
490 DDType result = thendd.unite(elsedd);
491
492 return result;
493
494 }
495
496 multiples = dd;
497 return dd;
498 }
499
500 template <class MgrType>
501 inline const MgrType&
get_mgr_core(const MgrType & rhs)502 get_mgr_core(const MgrType& rhs) {
503 return rhs;
504 }
505
506
507 ///@todo merge with extract_manager
508 // inline CCuddInterface::mgrcore_ptr
509 // get_mgr_core(const CCuddInterface& mgr) {
510 // return mgr.managerCore();
511 // }
512
513 /// temporarily (needs to be more generic) (similar fct in CCuddDDFacade.h)
514 template<class ManagerType, class ReverseIterator, class MultReverseIterator,
515 class DDBase>
516 inline DDBase
cudd_generate_multiples(const ManagerType & mgr,ReverseIterator start,ReverseIterator finish,MultReverseIterator multStart,MultReverseIterator multFinish,type_tag<DDBase>)517 cudd_generate_multiples(const ManagerType& mgr,
518 ReverseIterator start, ReverseIterator finish,
519 MultReverseIterator multStart,
520 MultReverseIterator multFinish, type_tag<DDBase> ) {
521
522 DdNode* prev( (mgr.getManager())->one );
523
524 DdNode* zeroNode( (mgr.getManager())->zero );
525
526 PBORI_PREFIX(Cudd_Ref)(prev);
527 while(start != finish) {
528
529 while((multStart != multFinish) && (*start < *multStart)) {
530
531 DdNode* result = PBORI_PREFIX(cuddUniqueInterZdd)( mgr.getManager(), *multStart,
532 prev, prev );
533
534 PBORI_PREFIX(Cudd_Ref)(result);
535 PBORI_PREFIX(Cudd_RecursiveDerefZdd)(mgr.getManager(), prev);
536
537 prev = result;
538 ++multStart;
539
540 };
541
542 DdNode* result = PBORI_PREFIX(cuddUniqueInterZdd)( mgr.getManager(), *start,
543 prev, zeroNode );
544
545 PBORI_PREFIX(Cudd_Ref)(result);
546 PBORI_PREFIX(Cudd_RecursiveDerefZdd)(mgr.getManager(), prev);
547
548 prev = result;
549
550
551 if((multStart != multFinish) && (*start == *multStart))
552 ++multStart;
553
554
555 ++start;
556 }
557
558 while(multStart != multFinish) {
559
560 DdNode* result = PBORI_PREFIX(cuddUniqueInterZdd)( mgr.getManager(), *multStart,
561 prev, prev );
562
563 PBORI_PREFIX(Cudd_Ref)(result);
564 PBORI_PREFIX(Cudd_RecursiveDerefZdd)(mgr.getManager(), prev);
565
566 prev = result;
567 ++multStart;
568
569 };
570
571 PBORI_PREFIX(Cudd_Deref)(prev);
572
573 typedef DDBase dd_base;
574 return dd_base(mgr, prev);
575 }
576
577
578
579 /// temporarily (needs to be more generic) (similar fct in CCuddDDFacade.h)
580 template<class ManagerType, class ReverseIterator, class DDBase>
581 DDBase
cudd_generate_divisors(const ManagerType & mgr,ReverseIterator start,ReverseIterator finish,type_tag<DDBase>)582 cudd_generate_divisors(const ManagerType& mgr,
583 ReverseIterator start, ReverseIterator finish, type_tag<DDBase>) {
584
585
586 DdNode* prev= (mgr.getManager())->one;
587
588 PBORI_PREFIX(Cudd_Ref)(prev);
589 while(start != finish) {
590
591 DdNode* result = PBORI_PREFIX(cuddUniqueInterZdd)( mgr.getManager(), *start,
592 prev, prev);
593
594 PBORI_PREFIX(Cudd_Ref)(result);
595 PBORI_PREFIX(Cudd_RecursiveDerefZdd)(mgr.getManager(), prev);
596
597 prev = result;
598 ++start;
599 }
600
601 PBORI_PREFIX(Cudd_Deref)(prev);
602 ///@todo Next line needs generalization
603 return DDBase(mgr, prev);
604
605 }
606
607
608 template<class Iterator, class SizeType>
609 Iterator
bounded_max_element(Iterator start,Iterator finish,SizeType bound)610 bounded_max_element(Iterator start, Iterator finish, SizeType bound){
611
612 if (*start >= bound)
613 return start;
614
615 Iterator result(start);
616 if (start != finish)
617 ++start;
618
619 while (start != finish) {
620 if(*start >= bound)
621 return start;
622 if(*start > *result)
623 result = start;
624 ++start;
625 }
626
627 return result;
628 }
629
630 /// defines lexicographic comparison for variable indices
631 template <class LhsType, class RhsType, class BinaryPredicate>
632 CTypes::comp_type
generic_compare_3way(const LhsType & lhs,const RhsType & rhs,BinaryPredicate comp)633 generic_compare_3way(const LhsType& lhs, const RhsType& rhs, BinaryPredicate comp) {
634
635 if (lhs == rhs)
636 return CTypes::equality;
637
638 return (comp(lhs, rhs)? CTypes::greater_than: CTypes::less_than);
639 }
640
641
642
643 template <class IteratorLike, class ForwardIteratorTag>
644 IteratorLike
increment_iteratorlike(IteratorLike iter,ForwardIteratorTag)645 increment_iteratorlike(IteratorLike iter, ForwardIteratorTag) {
646
647 return ++iter;
648 }
649
650 template <class IteratorLike>
651 IteratorLike
increment_iteratorlike(IteratorLike iter,navigator_tag)652 increment_iteratorlike(IteratorLike iter, navigator_tag) {
653
654 return iter.thenBranch();
655 }
656
657
658 template <class IteratorLike>
659 IteratorLike
increment_iteratorlike(IteratorLike iter)660 increment_iteratorlike(IteratorLike iter) {
661
662 typedef typename std::iterator_traits<IteratorLike>::iterator_category
663 iterator_category;
664
665 return increment_iteratorlike(iter, iterator_category());
666 }
667
668 #ifdef PBORI_LOWLEVEL_XOR
669
670 // dummy for PBORI_PREFIX(cuddcache) (implemented in pbori_routines.cc)
671 DdNode*
672 pboriCuddZddUnionXor__(DdManager *, DdNode *, DdNode *);
673
674
675 /// The following should be made more generic
676 /// @todo This is still Cudd-like style, should be rewritten with PolyBoRi's
677 /// cache wrapper, which would the dependency on PBORI_PREFIX(cuddInt.h)
678 template <class MgrType, class NodeType>
679 NodeType
pboriCuddZddUnionXor(MgrType zdd,NodeType P,NodeType Q)680 pboriCuddZddUnionXor(MgrType zdd, NodeType P, NodeType Q) {
681
682 int p_top, q_top;
683 NodeType empty = DD_ZERO(zdd), t, e, res;
684 MgrType table = zdd;
685
686 statLine(zdd);
687
688 if (P == empty)
689 return(Q);
690 if (Q == empty)
691 return(P);
692 if (P == Q)
693 return(empty);
694
695 /* Check cache */
696 res = PBORI_PREFIX(cuddCacheLookup2Zdd)(table, pboriCuddZddUnionXor__, P, Q);
697 if (res != NULL)
698 return(res);
699
700 if (PBORI_PREFIX(cuddIsConstant)(P))
701 p_top = P->index;
702 else
703 p_top = P->index;/* zdd->permZ[P->index]; */
704 if (PBORI_PREFIX(cuddIsConstant)(Q))
705 q_top = Q->index;
706 else
707 q_top = Q->index; /* zdd->permZ[Q->index]; */
708 if (p_top < q_top) {
709 e = pboriCuddZddUnionXor(zdd, PBORI_PREFIX(cuddE)(P), Q);
710 if (e == NULL) return (NULL);
711 PBORI_PREFIX(Cudd_Ref)(e);
712 res = PBORI_PREFIX(cuddZddGetNode)(zdd, P->index, PBORI_PREFIX(cuddT)(P), e);
713 if (res == NULL) {
714 PBORI_PREFIX(Cudd_RecursiveDerefZdd)(table, e);
715 return(NULL);
716 }
717 PBORI_PREFIX(Cudd_Deref)(e);
718 } else if (p_top > q_top) {
719 e = pboriCuddZddUnionXor(zdd, P, PBORI_PREFIX(cuddE)(Q));
720 if (e == NULL) return(NULL);
721 PBORI_PREFIX(Cudd_Ref)(e);
722 res = PBORI_PREFIX(cuddZddGetNode)(zdd, Q->index, PBORI_PREFIX(cuddT)(Q), e);
723 if (res == NULL) {
724 PBORI_PREFIX(Cudd_RecursiveDerefZdd)(table, e);
725 return(NULL);
726 }
727 PBORI_PREFIX(Cudd_Deref)(e);
728 } else {
729 t = pboriCuddZddUnionXor(zdd, PBORI_PREFIX(cuddT)(P), PBORI_PREFIX(cuddT)(Q));
730 if (t == NULL) return(NULL);
731 PBORI_PREFIX(Cudd_Ref)(t);
732 e = pboriCuddZddUnionXor(zdd, PBORI_PREFIX(cuddE)(P), PBORI_PREFIX(cuddE)(Q));
733 if (e == NULL) {
734 PBORI_PREFIX(Cudd_RecursiveDerefZdd)(table, t);
735 return(NULL);
736 }
737 PBORI_PREFIX(Cudd_Ref)(e);
738 res = PBORI_PREFIX(cuddZddGetNode)(zdd, P->index, t, e);
739 if (res == NULL) {
740 PBORI_PREFIX(Cudd_RecursiveDerefZdd)(table, t);
741 PBORI_PREFIX(Cudd_RecursiveDerefZdd)(table, e);
742 return(NULL);
743 }
744 PBORI_PREFIX(Cudd_Deref)(t);
745 PBORI_PREFIX(Cudd_Deref)(e);
746 }
747
748 PBORI_PREFIX(cuddCacheInsert2)(table, pboriCuddZddUnionXor__, P, Q, res);
749
750 return(res);
751 } /* end of pboriCuddZddUnionXor */
752
753 template <class MgrType, class NodeType>
754 NodeType
pboriCudd_zddUnionXor(MgrType dd,NodeType P,NodeType Q)755 pboriCudd_zddUnionXor(MgrType dd, NodeType P, NodeType Q) {
756
757 NodeType res;
758 do {
759 dd->reordered = 0;
760 res = pboriCuddZddUnionXor(dd, P, Q);
761 } while (dd->reordered == 1);
762 return(res);
763 }
764
765 #endif // PBORI_LOWLEVEL_XOR
766
767
768 template <class NaviType>
769 bool
dd_is_singleton(NaviType navi)770 dd_is_singleton(NaviType navi) {
771
772 while(!navi.isConstant()) {
773 if (!navi.elseBranch().isEmpty())
774 return false;
775 navi.incrementThen();
776 }
777 return true;
778 }
779
780 template <class NaviType, class BooleConstant>
781 BooleConstant
dd_pair_check(NaviType navi,BooleConstant allowSingleton)782 dd_pair_check(NaviType navi, BooleConstant allowSingleton) {
783
784 while(!navi.isConstant()) {
785
786 if (!navi.elseBranch().isEmpty())
787 return dd_is_singleton(navi.elseBranch()) &&
788 dd_is_singleton(navi.thenBranch());
789
790 navi.incrementThen();
791 }
792 return allowSingleton;//();
793 }
794
795
796 template <class NaviType>
797 bool
dd_is_singleton_or_pair(NaviType navi)798 dd_is_singleton_or_pair(NaviType navi) {
799
800 return dd_pair_check(navi, true);
801 }
802
803 template <class NaviType>
804 bool
dd_is_pair(NaviType navi)805 dd_is_pair(NaviType navi) {
806
807 return dd_pair_check(navi, false);
808 }
809
810
811
812 template <class SetType>
combine_sizes(const SetType & bset,double & init)813 void combine_sizes(const SetType& bset, double& init) {
814 init += bset.sizeDouble();
815 }
816
817 template <class SetType>
combine_sizes(const SetType & bset,typename SetType::size_type & init)818 void combine_sizes(const SetType& bset,
819 typename SetType::size_type& init) {
820 init += bset.size();
821 }
822
823
824 template <class SizeType, class IdxType, class NaviType, class SetType>
825 SizeType&
count_index(SizeType & size,IdxType idx,NaviType navi,const SetType & init)826 count_index(SizeType& size, IdxType idx, NaviType navi, const SetType& init) {
827
828 if (*navi == idx)
829 combine_sizes(SetType(navi.incrementThen(), init.ring()), size);
830
831 if (*navi < idx) {
832 count_index(size, idx, navi.thenBranch(), init);
833 count_index(size, idx, navi.elseBranch(), init);
834 }
835 return size;
836 }
837
838
839 template <class SizeType, class IdxType, class SetType>
840 SizeType&
count_index(SizeType & size,IdxType idx,const SetType & bset)841 count_index(SizeType& size, IdxType idx, const SetType& bset) {
842
843 return count_index(size, idx, bset.navigation(), SetType(bset.ring()));
844 }
845
846
847 template <class InIter, class OutIter, class Object, class MemberFuncPtr>
848 inline OutIter
transform(InIter start,InIter finish,OutIter result,Object & obj,MemberFuncPtr func)849 transform(InIter start, InIter finish, OutIter result, Object& obj,
850 MemberFuncPtr func) {
851 for(; start != finish; ++start, ++result)
852 *result = (obj .* func)(*start);
853 }
854
855 template <class InIter, class Object, class MemberFuncPtr>
856 inline void
for_each(InIter start,InIter finish,Object & obj,MemberFuncPtr func)857 for_each(InIter start, InIter finish, Object& obj, MemberFuncPtr func) {
858 for(; start != finish; ++start)
859 (obj .* func)(*start);
860 }
861
862 template <class InIter, class Object, class MemberFuncPtr>
863 inline void
for_each(InIter start,InIter finish,const Object & obj,MemberFuncPtr func)864 for_each(InIter start, InIter finish, const Object& obj, MemberFuncPtr func) {
865 for(; start != finish; ++start)
866 (obj .* func)(*start);
867 }
868 template <class Type, class Type1>
869 const Type&
which(bool condition,const Type1 & value1,const Type & value)870 which(bool condition, const Type1& value1, const Type& value) {
871 if (condition)
872 return value1;
873 return value;
874 }
875
876 template <class Type, class Type1, class Type2>
877 const Type&
which(bool cond1,const Type1 & value1,bool cond2,const Type2 & value2,const Type & value)878 which(bool cond1, const Type1& value1,
879 bool cond2, const Type2& value2, const Type& value) {
880 return which(cond1, value1, which(cond2, value2, value) );
881 }
882
883 template <class Type, class Type1, class Type2, class Type3>
884 const Type&
which(bool cond1,const Type1 & value1,bool cond2,const Type2 & value2,bool cond3,const Type3 & value3,const Type & value)885 which(bool cond1, const Type1& value1,
886 bool cond2, const Type2& value2,
887 bool cond3, const Type3& value3, const Type& value ) {
888 return which(cond1, value1, cond2, value2, which(cond3, value3, value) );
889 }
890
891
892
893
894 template <class IDType, class Iterator>
same_rings(const IDType & id,Iterator start,Iterator finish)895 bool same_rings(const IDType& id, Iterator start, Iterator finish) {
896
897 while ((start != finish) && (start->ring().id() == id)) { ++start; }
898 return (start == finish);
899 }
900
901 template <class Iterator>
same_rings(Iterator start,Iterator finish)902 bool same_rings(Iterator start, Iterator finish) {
903
904 return (start == finish) || same_rings(start->ring().id(), start, finish);
905 }
906
907 END_NAMESPACE_PBORI
908
909 #endif
910