PolyBoRi: pbori_algo.h Source File

00001 // -*- c++ -*-
00002 //*****************************************************************************
00017 //*****************************************************************************
00018 
00019 #ifndef polybori_routines_pbori_algo_h_
00020 #define polybori_routines_pbori_algo_h_
00021 
00022 // include polybori's definitions
00023 #include <polybori/pbori_defs.h>
00024 
00025 // get polybori's functionals
00026 #include "pbori_func.h"
00027 #include <polybori/common/traits.h>
00028 
00029 // temporarily
00030 #include <polybori/cudd/cudd.h>
00031 #include <polybori/ring/CCuddInterface.h>
00032 
00033 BEGIN_NAMESPACE_PBORI
00034 
00035 
00037 template< class NaviType, class TermType, 
00038           class TernaryOperator, 
00039           class TerminalOperator >
00040 TermType
00041 dd_backward_transform( NaviType navi, TermType init, TernaryOperator newNode,
00042               TerminalOperator terminate ) {
00043  
00044   TermType result = init;
00045 
00046   if (navi.isConstant()) {      // Reached end of path
00047     if (navi.terminalValue()){   // Case of a valid path
00048       result = terminate();
00049     }
00050   }
00051   else {
00052     result = dd_backward_transform(navi.thenBranch(), init, newNode, terminate);
00053     result = newNode(*navi, result, 
00054                      dd_backward_transform(navi.elseBranch(), init, newNode,
00055                                            terminate) );
00056   }
00057   return result;
00058 }
00059 
00060 
00062 template< class NaviType, class TermType, class OutIterator,
00063           class ThenBinaryOperator, class ElseBinaryOperator, 
00064           class TerminalOperator >
00065 OutIterator
00066 dd_transform( NaviType navi, TermType init, OutIterator result, 
00067               ThenBinaryOperator then_binop, ElseBinaryOperator else_binop,
00068               TerminalOperator terminate ) {
00069  
00070 
00071   if (navi.isConstant()) {      // Reached end of path
00072     if (navi.terminalValue()){   // Case of a valid path
00073       *result = terminate(init);
00074       ++result;
00075     }
00076   }
00077   else {
00078     result = dd_transform(navi.thenBranch(), then_binop(init, *navi), result,
00079                  then_binop, else_binop, terminate);
00080     result = dd_transform(navi.elseBranch(), else_binop(init, *navi), result,
00081                  then_binop, else_binop, terminate);
00082   }
00083   return result;
00084 }
00085 
00088 template< class NaviType, class TermType, class OutIterator,
00089           class ThenBinaryOperator, class ElseBinaryOperator, 
00090           class TerminalOperator, class FirstTermOp >
00091 OutIterator
00092 dd_transform( NaviType navi, TermType init, OutIterator result, 
00093               ThenBinaryOperator then_binop, ElseBinaryOperator else_binop,
00094               TerminalOperator terminate, FirstTermOp terminate_first ) {
00095 
00096   if (navi.isConstant()) {      // Reached end of path
00097     if (navi.terminalValue()){   // Case of a valid path - here leading term
00098       *result = terminate_first(init);
00099       ++result;
00100     }
00101   }
00102   else {
00103     result = dd_transform(navi.thenBranch(), then_binop(init, *navi), result,
00104                  then_binop, else_binop, terminate, terminate_first);
00105     result = dd_transform(navi.elseBranch(), else_binop(init, *navi), result,
00106                  then_binop, else_binop, terminate);
00107   }
00108   return result;
00109 }
00110 
00112 template< class NaviType, class TermType, class OutIterator,
00113           class ThenBinaryOperator, class ElseBinaryOperator >
00114 void
00115 dd_transform( const NaviType& navi, const TermType& init, 
00116               const OutIterator& result, 
00117               const ThenBinaryOperator& then_binop, 
00118               const ElseBinaryOperator& else_binop ) {
00119 
00120   dd_transform(navi, init, result, then_binop, else_binop, 
00121                project_ith<1>() );
00122 }
00123 
00125 template< class NaviType, class TermType, class OutIterator,
00126           class ThenBinaryOperator >
00127 void
00128 dd_transform( const NaviType& navi, const TermType& init, 
00129               const OutIterator& result, 
00130               const ThenBinaryOperator& then_binop ) {
00131 
00132   dd_transform(navi, init, result, then_binop,
00133                project_ith<1, 2>(),
00134                project_ith<1>() );
00135 }
00136 
00137 
00138 template <class InputIterator, class OutputIterator, 
00139           class FirstFunction, class UnaryFunction>
00140 OutputIterator 
00141 special_first_transform(InputIterator first, InputIterator last,
00142                         OutputIterator result, 
00143                          UnaryFunction op, FirstFunction firstop) {
00144   InputIterator second(first);
00145   if (second != last) {
00146     ++second;
00147     result = std::transform(first, second, result, firstop);
00148   }
00149   return std::transform(second, last, result, op);
00150 }
00151 
00152 
00154 template <class InputIterator, class Intermediate, class OutputIterator>
00155 OutputIterator
00156 reversed_inter_copy( InputIterator start, InputIterator finish,
00157                      Intermediate& inter, OutputIterator output ) {
00158 
00159     std::copy(start, finish, inter.begin());
00160     // force constant
00161     return std::copy( const_cast<const Intermediate&>(inter).rbegin(),
00162                       const_cast<const Intermediate&>(inter).rend(), 
00163                       output );
00164 }
00165 
00168 template <class NaviType>
00169 bool
00170 dd_on_path(NaviType navi) {
00171  
00172   if (navi.isConstant()) 
00173     return navi.terminalValue();
00174 
00175   return dd_on_path(navi.thenBranch()) || dd_on_path(navi.elseBranch());
00176 }
00177 
00180 template <class NaviType, class OrderedIterator>
00181 bool
00182 dd_owns_term_of_indices(NaviType navi, 
00183                           OrderedIterator start, OrderedIterator finish) {
00184  
00185   if (!navi.isConstant()) {     // Not at end of path
00186     bool not_at_end;
00187 
00188     while( (not_at_end = (start != finish)) && (*start < *navi) )
00189       ++start;
00190 
00191     NaviType elsenode = navi.elseBranch();
00192 
00193     if (elsenode.isConstant() && elsenode.terminalValue())
00194       return true;
00195       
00196 
00197     if (not_at_end){
00198       
00199       if ( (*start == *navi) && 
00200            dd_owns_term_of_indices(navi.thenBranch(), start, finish))
00201         return true;
00202       else  
00203         return dd_owns_term_of_indices(elsenode, start, finish);
00204     }
00205     else {
00206 
00207       while(!elsenode.isConstant()) 
00208         elsenode.incrementElse();
00209       return elsenode.terminalValue();
00210     }
00211    
00212   }
00213   return navi.terminalValue();
00214 }
00215 
00219 template <class NaviType, class OrderedIterator, class NodeOperation>
00220 NaviType
00221 dd_intersect_some_index(NaviType navi, 
00222                         OrderedIterator start, OrderedIterator finish,
00223                         NodeOperation newNode ) {
00224  
00225   if (!navi.isConstant()) {     // Not at end of path
00226     bool not_at_end;
00227     while( (not_at_end = (start != finish)) && (*start < *navi) )
00228       ++start;
00229 
00230     if (not_at_end) {
00231       NaviType elseNode = 
00232         dd_intersect_some_index(navi.elseBranch(), start, finish, 
00233                                 newNode);
00234   
00235       if (*start == *navi) {
00236 
00237         NaviType thenNode = 
00238           dd_intersect_some_index(navi.thenBranch(), start, finish, 
00239                                   newNode);
00240 
00241         return newNode(*start, navi, thenNode, elseNode); 
00242       }
00243       else
00244         return elseNode;
00245     }
00246     else {                      // if the start == finish, we only check 
00247                                 // validity of the else-only branch 
00248       while(!navi.isConstant()) 
00249         navi = navi.elseBranch();
00250       return newNode(navi);
00251     }
00252 
00253   }
00254 
00255   return newNode(navi);
00256 }
00257 
00258 
00259 
00261 template <class NaviType>
00262 void
00263 dd_print(NaviType navi) {
00264  
00265   if (!navi.isConstant()) {     // Not at end of path
00266  
00267     std::cout << std::endl<< "idx " << *navi <<" addr "<<
00268       ((DdNode*)navi)<<" ref "<<
00269       int(PBORI_PREFIX(Cudd_Regular)((DdNode*)navi)->ref) << std::endl;
00270 
00271     dd_print(navi.thenBranch());
00272     dd_print(navi.elseBranch());
00273 
00274   }
00275   else {
00276     std::cout << "const isvalid? "<<navi.isValid()<<" addr "
00277               <<((DdNode*)navi)<<" ref "<<
00278       int(PBORI_PREFIX(Cudd_Regular)((DdNode*)navi)->ref)<<std::endl;
00279 
00280   }
00281 }
00282 
00283 // Determinine the minimum of the distance between two iterators and limit
00284 template <class IteratorType, class SizeType>
00285 SizeType
00286 limited_distance(IteratorType start, IteratorType finish, SizeType limit) {
00287 
00288   SizeType result = 0;
00289 
00290   while ((result < limit) && (start != finish)) {
00291     ++start, ++result;
00292   }
00293 
00294   return result;
00295 }
00296 
00297 #if 0
00298 // Forward declaration of CTermIter template
00299 template <class, class, class, class, class, class> class CTermIter;
00300 
00301 // Determinine the minimum of the number of terms and limit
00302 template <class NaviType, class SizeType>
00303 SizeType
00304 limited_length(NaviType navi, SizeType limit) {
00305 
00306 
00307   typedef CTermIter<dummy_iterator, NaviType, 
00308                     project_ith<1>, project_ith<1>, project_ith<1, 2>, 
00309     project_ith<1> >
00310   iterator;
00311 
00312   return limited_distance(iterator(navi), iterator(), limit);
00313 }
00314 #endif
00315 
00317 template <class NaviType>
00318 bool owns_one(NaviType navi) {
00319   while (!navi.isConstant() )
00320     navi.incrementElse();
00321   
00322   return navi.terminalValue();
00323 }
00324 
00325 template <class CacheMgr, class NaviType, class SetType>
00326 SetType
00327 dd_modulo_monomials(const CacheMgr& cache_mgr,  
00328                     NaviType navi, NaviType rhs, const SetType& init){
00329 
00330   // Managing trivial cases
00331   if (owns_one(rhs)) return cache_mgr.zero();
00332 
00333   if (navi.isConstant())
00334     return cache_mgr.generate(navi);
00335 
00336   typename SetType::idx_type index = *navi;
00337   while(*rhs < index )
00338     rhs.incrementElse();
00339 
00340   if (rhs.isConstant())
00341     return cache_mgr.generate(navi);
00342 
00343   if (rhs == navi)
00344     return cache_mgr.zero(); 
00345 
00346   // Cache look-up
00347   NaviType cached = cache_mgr.find(navi, rhs);
00348   if (cached.isValid()) 
00349     return cache_mgr.generate(cached);
00350 
00351   // Actual computations
00352   SetType result(cache_mgr.zero());
00353   if (index == *rhs){
00354 
00355     NaviType rhselse = rhs.elseBranch();
00356     SetType thenres =
00357       dd_modulo_monomials(cache_mgr, navi.thenBranch(), rhs.thenBranch(), init);
00358 
00359     result = 
00360       SetType(index,
00361               dd_modulo_monomials(cache_mgr, 
00362                                   thenres.navigation(), rhselse, init),
00363               dd_modulo_monomials(cache_mgr, 
00364                                   navi.elseBranch(), rhselse, init)
00365               );
00366     
00367   } 
00368   else {
00369     PBORI_ASSERT(*rhs > index);
00370     result = 
00371       SetType(index,
00372               dd_modulo_monomials(cache_mgr, navi.thenBranch(), rhs, init),
00373               dd_modulo_monomials(cache_mgr, navi.elseBranch(), rhs, init)
00374               );
00375   }
00376   cache_mgr.insert(navi, rhs, result.navigation());
00377   return result;
00378 }
00379 
00381 template <class CacheMgr, class ModMonCacheMgr, class NaviType, class SetType>
00382 SetType
00383 dd_minimal_elements(const CacheMgr& cache_mgr, const ModMonCacheMgr& modmon_mgr,
00384                     NaviType navi, const SetType& init){
00385 
00386   // Trivial Cases
00387   if (navi.isEmpty()) 
00388     return cache_mgr.generate(navi);
00389   
00390   if (owns_one(navi)) return cache_mgr.one();
00391 
00392   NaviType ms0 = navi.elseBranch();
00393   NaviType ms1 = navi.thenBranch();
00394 
00395   // Cache look-up
00396   NaviType cached = cache_mgr.find(navi);
00397   if (cached.isValid())
00398     return cache_mgr.generate(cached);
00399   
00400   SetType minimal_else = dd_minimal_elements(cache_mgr, modmon_mgr, ms0, init);
00401   SetType minimal_then = 
00402     dd_minimal_elements(cache_mgr, modmon_mgr,
00403                         dd_modulo_monomials(modmon_mgr, ms1,
00404                                             minimal_else.navigation(),
00405                                             init).navigation(),
00406                      init);
00407   SetType result(cache_mgr.zero());
00408   if ( (minimal_else.navigation() == ms0) 
00409        && (minimal_then.navigation() == ms1) )
00410     result = cache_mgr.generate(navi);
00411   else
00412     result = SetType(*navi, minimal_then, minimal_else);
00413 
00414   cache_mgr.insert(navi, result.navigation());
00415   return result;
00416 }
00417 
00418 
00422 template <class NaviType, class DDType>
00423 DDType
00424 dd_minimal_elements(NaviType navi, DDType dd, DDType& multiples) {
00425 
00426 
00427   if (!navi.isConstant()) {     // Not at end of path
00428 
00429     DDType elsedd = dd.subset0(*navi);
00430 
00431 
00432     DDType elseMultiples;
00433     elsedd = dd_minimal_elements(navi.elseBranch(), elsedd, elseMultiples);
00434 
00435     // short cut if else and then branche equal or else contains 1
00436     if((navi.elseBranch() == navi.thenBranch()) || elsedd.blankness()){
00437       multiples = elseMultiples;
00438       return elsedd;
00439     }
00440 
00441     NaviType elseNavi = elseMultiples.navigation();
00442 
00443     int nmax;
00444     if (elseNavi.isConstant()){
00445       if (elseNavi.terminalValue())
00446         nmax = dd.nVariables();
00447       else
00448         nmax = *navi;
00449     }
00450     else
00451       nmax = *elseNavi;
00452 
00453 
00454     for(int i = nmax-1; i > *navi; --i){
00455       elseMultiples.uniteAssign(elseMultiples.change(i)); 
00456     }
00457 
00458 
00459     DDType thendd = dd.subset1(*navi);
00460     thendd = thendd.diff(elseMultiples);
00461 
00462     DDType thenMultiples;
00463     thendd = dd_minimal_elements(navi.thenBranch(), thendd, thenMultiples); 
00464  
00465     NaviType thenNavi = thenMultiples.navigation();
00466 
00467 
00468     if (thenNavi.isConstant()){
00469       if (thenNavi.terminalValue())
00470         nmax =  dd.nVariables();
00471       else
00472         nmax = *navi;
00473     }
00474     else
00475       nmax = *thenNavi;
00476 
00477 
00478     for(int i = nmax-1; i > *navi; --i){
00479       thenMultiples.uniteAssign(thenMultiples.change(i)); 
00480     }
00481 
00482 
00483     thenMultiples = thenMultiples.unite(elseMultiples);
00484     thenMultiples = thenMultiples.change(*navi);
00485 
00486 
00487     multiples = thenMultiples.unite(elseMultiples);
00488     thendd = thendd.change(*navi);
00489 
00490     DDType result =  thendd.unite(elsedd);
00491 
00492     return result;
00493 
00494   }
00495 
00496   multiples = dd;
00497   return dd;
00498 }
00499 
00500 template <class MgrType>
00501 inline const MgrType&
00502 get_mgr_core(const MgrType& rhs) { 
00503   return rhs;
00504 }
00505 
00506 
00508 // inline CCuddInterface::mgrcore_ptr
00509 // get_mgr_core(const CCuddInterface& mgr) {
00510 //   return mgr.managerCore();
00511 // }
00512 
00514 template<class ManagerType, class ReverseIterator, class MultReverseIterator,
00515 class DDBase>
00516 inline DDBase
00517 cudd_generate_multiples(const ManagerType& mgr, 
00518                         ReverseIterator start, ReverseIterator finish,
00519                         MultReverseIterator multStart, 
00520                         MultReverseIterator multFinish, type_tag<DDBase> ) {
00521 
00522     DdNode* prev( (mgr.getManager())->one );
00523 
00524     DdNode* zeroNode( (mgr.getManager())->zero ); 
00525 
00526     PBORI_PREFIX(Cudd_Ref)(prev);
00527     while(start != finish) {
00528 
00529       while((multStart != multFinish) && (*start < *multStart)) {
00530 
00531         DdNode* result = PBORI_PREFIX(cuddUniqueInterZdd)( mgr.getManager(), *multStart,
00532                                              prev, prev );
00533 
00534         PBORI_PREFIX(Cudd_Ref)(result);
00535         PBORI_PREFIX(Cudd_RecursiveDerefZdd)(mgr.getManager(), prev);
00536 
00537         prev = result;
00538         ++multStart;
00539 
00540       };
00541 
00542       DdNode* result = PBORI_PREFIX(cuddUniqueInterZdd)( mgr.getManager(), *start,
00543                                            prev, zeroNode );
00544 
00545       PBORI_PREFIX(Cudd_Ref)(result);
00546       PBORI_PREFIX(Cudd_RecursiveDerefZdd)(mgr.getManager(), prev);
00547 
00548       prev = result;
00549 
00550 
00551       if((multStart != multFinish) && (*start == *multStart))
00552         ++multStart;
00553 
00554 
00555       ++start;
00556     }
00557 
00558     while(multStart != multFinish) {
00559 
00560       DdNode* result = PBORI_PREFIX(cuddUniqueInterZdd)( mgr.getManager(), *multStart,
00561                                            prev, prev );
00562 
00563       PBORI_PREFIX(Cudd_Ref)(result);
00564       PBORI_PREFIX(Cudd_RecursiveDerefZdd)(mgr.getManager(), prev);
00565 
00566       prev = result;
00567       ++multStart;
00568 
00569     };
00570 
00571     PBORI_PREFIX(Cudd_Deref)(prev);
00572 
00573     typedef DDBase dd_base;
00574     return dd_base(mgr, prev);
00575   }
00576 
00577 
00578 
00580 template<class ManagerType, class ReverseIterator, class DDBase>
00581 DDBase
00582 cudd_generate_divisors(const ManagerType& mgr, 
00583                        ReverseIterator start, ReverseIterator finish, type_tag<DDBase>) {
00584 
00585 
00586     DdNode* prev= (mgr.getManager())->one;
00587 
00588     PBORI_PREFIX(Cudd_Ref)(prev);
00589     while(start != finish) {
00590  
00591       DdNode* result = PBORI_PREFIX(cuddUniqueInterZdd)( mgr.getManager(), *start,
00592                                            prev, prev);
00593 
00594       PBORI_PREFIX(Cudd_Ref)(result);
00595       PBORI_PREFIX(Cudd_RecursiveDerefZdd)(mgr.getManager(), prev);
00596  
00597       prev = result;
00598       ++start;
00599     }
00600 
00601     PBORI_PREFIX(Cudd_Deref)(prev);
00603       return DDBase(mgr, prev);
00604 
00605 }
00606 
00607 
00608 template<class Iterator, class SizeType>
00609 Iterator
00610 bounded_max_element(Iterator start, Iterator finish, SizeType bound){
00611 
00612   if (*start >= bound)
00613     return start;
00614 
00615   Iterator result(start);
00616   if (start != finish)
00617     ++start;
00618 
00619   while (start != finish) {
00620     if(*start >= bound)
00621       return start;
00622     if(*start > *result)
00623       result = start;
00624     ++start;
00625   }
00626 
00627   return result;
00628 }
00629 
00631 template <class LhsType, class RhsType, class BinaryPredicate>
00632 CTypes::comp_type
00633 generic_compare_3way(const LhsType& lhs, const RhsType& rhs, BinaryPredicate comp) {
00634 
00635   if (lhs == rhs)
00636     return CTypes::equality;
00637 
00638   return (comp(lhs, rhs)?  CTypes::greater_than: CTypes::less_than);
00639 }
00640 
00641 
00642 
00643 template <class IteratorLike, class ForwardIteratorTag>
00644 IteratorLike 
00645 increment_iteratorlike(IteratorLike iter, ForwardIteratorTag) {
00646 
00647   return ++iter;
00648 }
00649 
00650 template <class IteratorLike>
00651 IteratorLike 
00652 increment_iteratorlike(IteratorLike iter, navigator_tag) {
00653 
00654   return iter.thenBranch();
00655 }
00656 
00657 
00658 template <class IteratorLike>
00659 IteratorLike 
00660 increment_iteratorlike(IteratorLike iter) {
00661 
00662   typedef typename std::iterator_traits<IteratorLike>::iterator_category
00663     iterator_category;
00664 
00665   return increment_iteratorlike(iter, iterator_category());
00666 }
00667 
00668 #ifdef PBORI_LOWLEVEL_XOR 
00669 
00670 // dummy for PBORI_PREFIX(cuddcache) (implemented in pbori_routines.cc)
00671 DdNode* 
00672 pboriCuddZddUnionXor__(DdManager *, DdNode *, DdNode *);
00673 
00674 
00678 template <class MgrType, class NodeType>
00679 NodeType
00680 pboriCuddZddUnionXor(MgrType zdd, NodeType P, NodeType Q) {
00681 
00682   int           p_top, q_top;
00683   NodeType empty = DD_ZERO(zdd), t, e, res;
00684   MgrType table = zdd;
00685   
00686   statLine(zdd);
00687   
00688   if (P == empty)
00689     return(Q); 
00690   if (Q == empty)
00691     return(P);
00692   if (P == Q)
00693     return(empty);
00694 
00695   /* Check cache */
00696   res = PBORI_PREFIX(cuddCacheLookup2Zdd)(table, pboriCuddZddUnionXor__, P, Q);
00697   if (res != NULL)
00698     return(res);
00699   
00700   if (PBORI_PREFIX(cuddIsConstant)(P))
00701     p_top = P->index;
00702   else
00703     p_top = P->index;/* zdd->permZ[P->index]; */
00704   if (PBORI_PREFIX(cuddIsConstant)(Q))
00705     q_top = Q->index;
00706   else
00707     q_top = Q->index; /* zdd->permZ[Q->index]; */
00708   if (p_top < q_top) {
00709     e = pboriCuddZddUnionXor(zdd, PBORI_PREFIX(cuddE)(P), Q);
00710     if (e == NULL) return (NULL);
00711     PBORI_PREFIX(Cudd_Ref)(e);
00712     res = PBORI_PREFIX(cuddZddGetNode)(zdd, P->index, PBORI_PREFIX(cuddT)(P), e);
00713     if (res == NULL) {
00714       PBORI_PREFIX(Cudd_RecursiveDerefZdd)(table, e);
00715       return(NULL);
00716     }
00717     PBORI_PREFIX(Cudd_Deref)(e);
00718   } else if (p_top > q_top) {
00719     e = pboriCuddZddUnionXor(zdd, P, PBORI_PREFIX(cuddE)(Q));
00720     if (e == NULL) return(NULL);
00721     PBORI_PREFIX(Cudd_Ref)(e);
00722     res = PBORI_PREFIX(cuddZddGetNode)(zdd, Q->index, PBORI_PREFIX(cuddT)(Q), e);
00723     if (res == NULL) {
00724       PBORI_PREFIX(Cudd_RecursiveDerefZdd)(table, e);
00725       return(NULL);
00726     }
00727     PBORI_PREFIX(Cudd_Deref)(e);
00728   } else {
00729     t = pboriCuddZddUnionXor(zdd, PBORI_PREFIX(cuddT)(P), PBORI_PREFIX(cuddT)(Q));
00730     if (t == NULL) return(NULL);
00731     PBORI_PREFIX(Cudd_Ref)(t);
00732     e = pboriCuddZddUnionXor(zdd, PBORI_PREFIX(cuddE)(P), PBORI_PREFIX(cuddE)(Q));
00733     if (e == NULL) {
00734       PBORI_PREFIX(Cudd_RecursiveDerefZdd)(table, t);
00735       return(NULL);
00736     }
00737     PBORI_PREFIX(Cudd_Ref)(e);
00738     res = PBORI_PREFIX(cuddZddGetNode)(zdd, P->index, t, e);
00739     if (res == NULL) {
00740       PBORI_PREFIX(Cudd_RecursiveDerefZdd)(table, t);
00741       PBORI_PREFIX(Cudd_RecursiveDerefZdd)(table, e);
00742       return(NULL);
00743     }
00744     PBORI_PREFIX(Cudd_Deref)(t);
00745     PBORI_PREFIX(Cudd_Deref)(e);
00746   }
00747   
00748   PBORI_PREFIX(cuddCacheInsert2)(table, pboriCuddZddUnionXor__, P, Q, res);
00749   
00750   return(res);
00751 } /* end of pboriCuddZddUnionXor */
00752 
00753 template <class MgrType, class NodeType>
00754 NodeType
00755 pboriCudd_zddUnionXor(MgrType dd, NodeType P, NodeType Q) {
00756 
00757   NodeType res;
00758   do {
00759     dd->reordered = 0;
00760     res = pboriCuddZddUnionXor(dd, P, Q);
00761     } while (dd->reordered == 1);
00762   return(res);
00763 }
00764 
00765 #endif // PBORI_LOWLEVEL_XOR 
00766 
00767 
00768 template <class NaviType>
00769 bool
00770 dd_is_singleton(NaviType navi) {
00771 
00772   while(!navi.isConstant()) {
00773     if (!navi.elseBranch().isEmpty())
00774       return false;
00775     navi.incrementThen();
00776   }
00777   return true;
00778 }
00779 
00780 template <class NaviType, class BooleConstant>
00781 BooleConstant
00782 dd_pair_check(NaviType navi, BooleConstant allowSingleton) {
00783 
00784   while(!navi.isConstant()) {
00785 
00786     if (!navi.elseBranch().isEmpty())
00787       return dd_is_singleton(navi.elseBranch()) && 
00788         dd_is_singleton(navi.thenBranch());
00789 
00790     navi.incrementThen();
00791   }
00792   return allowSingleton;//();
00793 }
00794 
00795 
00796 template <class NaviType>
00797 bool
00798 dd_is_singleton_or_pair(NaviType navi) {
00799 
00800   return dd_pair_check(navi, true);
00801 }
00802 
00803 template <class NaviType>
00804 bool
00805 dd_is_pair(NaviType navi) {
00806 
00807   return dd_pair_check(navi, false);
00808 }
00809 
00810 
00811 
00812 template <class SetType>
00813 void combine_sizes(const SetType& bset, double& init) {
00814   init += bset.sizeDouble();
00815 }
00816 
00817 template <class SetType>
00818 void combine_sizes(const SetType& bset, 
00819                    typename SetType::size_type& init) {
00820   init += bset.size();
00821 }
00822 
00823 
00824 template <class SizeType, class IdxType, class NaviType, class SetType>
00825 SizeType&
00826 count_index(SizeType& size, IdxType idx, NaviType navi, const SetType& init) {
00827 
00828   if (*navi == idx)
00829     combine_sizes(SetType(navi.incrementThen(), init.ring()), size);
00830 
00831   if (*navi < idx) {
00832     count_index(size, idx, navi.thenBranch(), init);
00833     count_index(size, idx, navi.elseBranch(), init);
00834   }
00835   return size;
00836 }
00837 
00838 
00839 template <class SizeType, class IdxType, class SetType>
00840 SizeType&
00841 count_index(SizeType& size, IdxType idx, const SetType& bset) {
00842 
00843   return count_index(size, idx, bset.navigation(), SetType(bset.ring()));
00844 }
00845 
00846 
00847 template <class InIter, class OutIter, class Object, class MemberFuncPtr>
00848 inline OutIter
00849 transform(InIter start, InIter finish, OutIter result, Object& obj,
00850           MemberFuncPtr func) {
00851   for(; start != finish; ++start, ++result)
00852     *result = (obj .* func)(*start);
00853 }
00854 
00855 template <class InIter, class Object, class MemberFuncPtr>
00856 inline void
00857 for_each(InIter start, InIter finish, Object& obj, MemberFuncPtr func) {
00858   for(; start != finish; ++start)
00859     (obj .* func)(*start);
00860 }
00861 
00862 template <class InIter, class Object, class MemberFuncPtr>
00863 inline void
00864 for_each(InIter start, InIter finish, const Object& obj, MemberFuncPtr func) {
00865   for(; start != finish; ++start)
00866     (obj .* func)(*start);
00867 }
00868 template <class Type, class Type1>
00869 const Type&
00870 which(bool condition, const Type1& value1, const Type& value) {
00871   if (condition)
00872     return value1;
00873   return  value;
00874 }
00875 
00876 template <class Type, class Type1, class Type2>
00877 const Type&
00878 which(bool cond1, const Type1& value1, 
00879       bool cond2, const Type2& value2, const Type& value) {
00880   return which(cond1, value1, which(cond2, value2, value) );
00881 }
00882 
00883 template <class Type, class Type1, class Type2, class Type3>
00884 const Type&
00885 which(bool cond1, const Type1& value1, 
00886       bool cond2, const Type2& value2, 
00887       bool cond3, const Type3& value3, const Type& value ) {
00888   return which(cond1, value1, cond2, value2, which(cond3, value3, value) );
00889 }
00890 
00891 
00892 
00893 
00894 template <class IDType, class Iterator>
00895 bool same_rings(const IDType& id, Iterator start, Iterator finish) {
00896   
00897   while ((start != finish) && (start->ring().id() == id)) {  ++start;  }
00898   return (start == finish);
00899 }
00900 
00901 template <class Iterator>
00902 bool same_rings(Iterator start, Iterator finish) {
00903 
00904   return (start == finish) || same_rings(start->ring().id(), start, finish);
00905 }
00906 
00907 END_NAMESPACE_PBORI
00908 
00909 #endif