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