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