PolyBoRi
|
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_ring(start->ring().id(), start, finish); 00905 } 00906 00907 END_NAMESPACE_PBORI 00908 00909 #endif