PolyBoRi
|
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