PolyBoRi
|
00001 // -*- c++ -*- 00002 //***************************************************************************** 00143 //***************************************************************************** 00144 00145 // include basic definitions 00146 #include "pbori_defs.h" 00147 00148 // temprarily 00149 #include "CIdxVariable.h" 00150 00151 // temprarily 00152 #include "CacheManager.h" 00153 00154 #include "CDDOperations.h" 00155 00156 BEGIN_NAMESPACE_PBORI 00157 00158 template<class Iterator> 00159 typename Iterator::value_type 00160 index_vector_hash(Iterator start, Iterator finish){ 00161 00162 typedef typename Iterator::value_type value_type; 00163 00164 value_type vars = 0; 00165 value_type sum = 0; 00166 00167 while (start != finish){ 00168 vars++; 00169 sum += ((*start)+1) * ((*start)+1); 00170 ++start; 00171 } 00172 return sum * vars; 00173 } 00174 00177 template <class DegreeCacher, class NaviType> 00178 typename NaviType::size_type 00179 dd_cached_degree(const DegreeCacher& cache, NaviType navi) { 00180 00181 typedef typename NaviType::size_type size_type; 00182 00183 if (navi.isConstant()) // No need for caching of constant nodes' degrees 00184 return 0; 00185 00186 // Look whether result was cached before 00187 typename DegreeCacher::node_type result = cache.find(navi); 00188 if (result.isValid()) 00189 return *result; 00190 00191 // Get degree of then branch (contains at least one valid path)... 00192 size_type deg = dd_cached_degree(cache, navi.thenBranch()) + 1; 00193 00194 // ... combine with degree of else branch 00195 deg = std::max(deg, dd_cached_degree(cache, navi.elseBranch()) ); 00196 00197 // Write result to cache 00198 cache.insert(navi, deg); 00199 00200 return deg; 00201 } 00202 00207 template <class DegreeCacher, class NaviType, class SizeType> 00208 typename NaviType::size_type 00209 dd_cached_degree(const DegreeCacher& cache, NaviType navi, SizeType bound) { 00210 00211 typedef typename NaviType::size_type size_type; 00212 00213 // No need for caching of constant nodes' degrees 00214 if (bound == 0 || navi.isConstant()) 00215 return 0; 00216 00217 // Look whether result was cached before 00218 typename DegreeCacher::node_type result = cache.find(navi); 00219 if (result.isValid()) 00220 return *result; 00221 00222 // Get degree of then branch (contains at least one valid path)... 00223 size_type deg = dd_cached_degree(cache, navi.thenBranch(), bound - 1) + 1; 00224 00225 // ... combine with degree of else branch 00226 if (bound > deg) // if deg <= bound, we are already finished 00227 deg = std::max(deg, dd_cached_degree(cache, navi.elseBranch(), bound) ); 00228 00229 // Write result to cache 00230 cache.insert(navi, deg); 00231 00232 return deg; 00233 } 00234 00235 template <class Iterator, class NameGenerator, 00236 class Separator, class EmptySetType, 00237 class OStreamType> 00238 void 00239 dd_print_term(Iterator start, Iterator finish, const NameGenerator& get_name, 00240 const Separator& sep, const EmptySetType& emptyset, 00241 OStreamType& os){ 00242 00243 if (start != finish){ 00244 os << get_name(*start); 00245 ++start; 00246 } 00247 else 00248 os << emptyset(); 00249 00250 while (start != finish){ 00251 os << sep() << get_name(*start); 00252 ++start; 00253 } 00254 } 00255 00256 template <class TermType, class NameGenerator, 00257 class Separator, class EmptySetType, 00258 class OStreamType> 00259 void 00260 dd_print_term(const TermType& term, const NameGenerator& get_name, 00261 const Separator& sep, const EmptySetType& emptyset, 00262 OStreamType& os){ 00263 dd_print_term(term.begin(), term.end(), get_name, sep, emptyset, os); 00264 } 00265 00266 00267 template <class Iterator, class NameGenerator, 00268 class Separator, class InnerSeparator, 00269 class EmptySetType, class OStreamType> 00270 void 00271 dd_print_terms(Iterator start, Iterator finish, const NameGenerator& get_name, 00272 const Separator& sep, const InnerSeparator& innersep, 00273 const EmptySetType& emptyset, OStreamType& os) { 00274 00275 if (start != finish){ 00276 dd_print_term(*start, get_name, innersep, emptyset, os); 00277 ++start; 00278 } 00279 00280 while (start != finish){ 00281 os << sep(); 00282 dd_print_term(*start, get_name, innersep, emptyset, os); 00283 ++start; 00284 } 00285 00286 } 00287 00288 00289 template <class CacheType, class NaviType, class PolyType> 00290 PolyType 00291 dd_multiply_recursively(const CacheType& cache_mgr, 00292 NaviType firstNavi, NaviType secondNavi, PolyType init){ 00293 // Extract subtypes 00294 typedef typename PolyType::dd_type dd_type; 00295 typedef typename NaviType::idx_type idx_type; 00296 typedef NaviType navigator; 00297 00298 if (firstNavi.isConstant()) { 00299 if(firstNavi.terminalValue()) 00300 return cache_mgr.generate(secondNavi); 00301 else 00302 return cache_mgr.zero(); 00303 } 00304 00305 if (secondNavi.isConstant()) { 00306 if(secondNavi.terminalValue()) 00307 return cache_mgr.generate(firstNavi); 00308 else 00309 return cache_mgr.zero(); 00310 } 00311 if (firstNavi == secondNavi) 00312 return cache_mgr.generate(firstNavi); 00313 00314 // Look up, whether operation was already used 00315 navigator cached = cache_mgr.find(firstNavi, secondNavi); 00316 PolyType result = cache_mgr.zero(); 00317 00318 if (cached.isValid()) { // Cache lookup sucessful 00319 return cache_mgr.generate(cached); 00320 } 00321 else { // Cache lookup not sucessful 00322 // Get top variable's index 00323 00324 if (*secondNavi < *firstNavi) 00325 std::swap(firstNavi, secondNavi); 00326 00327 idx_type index = *firstNavi; 00328 00329 // Get then- and else-branches wrt. current indexed variable 00330 navigator as0 = firstNavi.elseBranch(); 00331 navigator as1 = firstNavi.thenBranch(); 00332 00333 navigator bs0; 00334 navigator bs1; 00335 00336 if (*secondNavi == index) { 00337 bs0 = secondNavi.elseBranch(); 00338 bs1 = secondNavi.thenBranch(); 00339 } 00340 else { 00341 bs0 = secondNavi; 00342 bs1 = result.navigation(); 00343 } 00344 00345 00346 #ifdef PBORI_FAST_MULTIPLICATION 00347 if (*firstNavi == *secondNavi) { 00348 00349 PolyType res00 = dd_multiply_recursively(cache_mgr, as0, bs0, init); 00350 00351 PolyType res10 = PolyType(cache_mgr.generate(as1)) + 00352 PolyType(cache_mgr.generate(as0)); 00353 PolyType res01 = PolyType(cache_mgr.generate(bs0)) + 00354 PolyType(cache_mgr.generate(bs1)); 00355 00356 PolyType res11 = 00357 dd_multiply_recursively(cache_mgr, 00358 res10.navigation(), res01.navigation(), 00359 init) - res00; 00360 00361 result = dd_type(index, res11.diagram(), res00.diagram()); 00362 } else 00363 #endif 00364 { 00365 bool as1_zero=false; 00366 if (as0 == as1) 00367 bs1 = result.navigation(); 00368 else if (bs0 == bs1){ 00369 as1 = result.navigation(); 00370 as1_zero=true; 00371 } 00372 // Do recursion 00373 NaviType zero_ptr = result.navigation(); 00374 00375 if (as1_zero){ 00376 result = dd_type(index, 00377 dd_multiply_recursively(cache_mgr, as0, bs1, 00378 init).diagram(), 00379 dd_multiply_recursively(cache_mgr, as0, bs0, 00380 init).diagram() ); 00381 } else{ 00382 PolyType bs01 = PolyType(cache_mgr.generate(bs0)) + 00383 PolyType(cache_mgr.generate(bs1)); 00384 result = dd_type(index, 00385 ( dd_multiply_recursively(cache_mgr, 00386 bs01.navigation(), 00387 as1, init) + 00388 dd_multiply_recursively(cache_mgr, as0, bs1, init) 00389 ).diagram(), 00390 dd_multiply_recursively(cache_mgr, 00391 as0, bs0, 00392 init).diagram() 00393 ); 00394 } 00395 00396 } 00397 // Insert in cache 00398 cache_mgr.insert(firstNavi, secondNavi, result.navigation()); 00399 } 00400 00401 return result; 00402 } 00403 00404 00405 template <class CacheType, class NaviType, class PolyType, 00406 class MonomTag> 00407 PolyType 00408 dd_multiply_recursively(const CacheType& cache_mgr, 00409 NaviType monomNavi, NaviType navi, PolyType init, 00410 MonomTag monom_tag ){ 00411 00412 // Extract subtypes 00413 typedef typename PolyType::dd_type dd_type; 00414 typedef typename NaviType::idx_type idx_type; 00415 typedef NaviType navigator; 00416 00417 if (monomNavi.isConstant()) { 00418 if(monomNavi.terminalValue()) 00419 return cache_mgr.generate(navi); 00420 else 00421 return cache_mgr.zero(); 00422 } 00423 00424 assert(monomNavi.elseBranch().isEmpty()); 00425 00426 if (navi.isConstant()) { 00427 if(navi.terminalValue()) 00428 return cache_mgr.generate(monomNavi); 00429 else 00430 return cache_mgr.zero(); 00431 } 00432 if (monomNavi == navi) 00433 return cache_mgr.generate(monomNavi); 00434 00435 // Look up, whether operation was already used 00436 navigator cached = cache_mgr.find(monomNavi, navi); 00437 00438 if (cached.isValid()) { // Cache lookup sucessful 00439 return cache_mgr.generate(cached); 00440 } 00441 00442 // Cache lookup not sucessful 00443 // Get top variables' index 00444 00445 idx_type index = *navi; 00446 idx_type monomIndex = *monomNavi; 00447 00448 if (monomIndex < index) { // Case: index may occure within monom 00449 init = dd_multiply_recursively(cache_mgr, monomNavi.thenBranch(), navi, 00450 init, monom_tag).diagram().change(monomIndex); 00451 } 00452 else if (monomIndex == index) { // Case: monom and poly start with same index 00453 00454 // Increment navigators 00455 navigator monomThen = monomNavi.thenBranch(); 00456 navigator naviThen = navi.thenBranch(); 00457 navigator naviElse = navi.elseBranch(); 00458 00459 if (naviThen != naviElse) 00460 init = (dd_multiply_recursively(cache_mgr, monomThen, naviThen, init, 00461 monom_tag) 00462 + dd_multiply_recursively(cache_mgr, monomThen, naviElse, init, 00463 monom_tag)).diagram().change(index); 00464 } 00465 else { // Case: var(index) not part of monomial 00466 00467 init = 00468 dd_type(index, 00469 dd_multiply_recursively(cache_mgr, monomNavi, navi.thenBranch(), 00470 init, monom_tag).diagram(), 00471 dd_multiply_recursively(cache_mgr, monomNavi, navi.elseBranch(), 00472 init, monom_tag).diagram() ); 00473 } 00474 00475 // Insert in cache 00476 cache_mgr.insert(monomNavi, navi, init.navigation()); 00477 00478 return init; 00479 } 00480 00481 00482 template <class DDGenerator, class Iterator, class NaviType, class PolyType> 00483 PolyType 00484 dd_multiply_recursively_exp(const DDGenerator& ddgen, 00485 Iterator start, Iterator finish, 00486 NaviType navi, PolyType init){ 00487 // Extract subtypes 00488 typedef typename NaviType::idx_type idx_type; 00489 typedef typename PolyType::dd_type dd_type; 00490 typedef NaviType navigator; 00491 00492 if (start == finish) 00493 return ddgen.generate(navi); 00494 00495 PolyType result; 00496 if (navi.isConstant()) { 00497 if(navi.terminalValue()) { 00498 00499 std::reverse_iterator<Iterator> rstart(finish), rfinish(start); 00500 result = ddgen.generate(navi); 00501 while (rstart != rfinish) { 00502 result = result.diagram().change(*rstart); 00503 ++rstart; 00504 } 00505 } 00506 else 00507 return ddgen.zero(); 00508 00509 return result; 00510 } 00511 00512 // Cache lookup not sucessful 00513 // Get top variables' index 00514 00515 idx_type index = *navi; 00516 idx_type monomIndex = *start; 00517 00518 if (monomIndex < index) { // Case: index may occure within monom 00519 00520 Iterator next(start); 00521 while( (next != finish) && (*next < index) ) 00522 ++next; 00523 00524 result = dd_multiply_recursively_exp(ddgen, next, finish, navi, init); 00525 00526 std::reverse_iterator<Iterator> rstart(next), rfinish(start); 00527 while (rstart != rfinish) { 00528 result = result.diagram().change(*rstart); 00529 ++rstart; 00530 } 00531 } 00532 else if (monomIndex == index) { // Case: monom and poly start with same index 00533 00534 // Increment navigators 00535 ++start; 00536 00537 navigator naviThen = navi.thenBranch(); 00538 navigator naviElse = navi.elseBranch(); 00539 00540 if (naviThen != naviElse) 00541 result =(dd_multiply_recursively_exp(ddgen, start, finish, naviThen, init) 00542 + dd_multiply_recursively_exp(ddgen, start, finish, naviElse, 00543 init)).diagram().change(index); 00544 } 00545 else { // Case: var(index) not part of monomial 00546 00547 result = 00548 dd_type(index, 00549 dd_multiply_recursively_exp(ddgen, start, finish, 00550 navi.thenBranch(), init).diagram(), 00551 dd_multiply_recursively_exp(ddgen, start, finish, 00552 navi.elseBranch(), init).diagram() ); 00553 } 00554 00555 return result; 00556 } 00557 00558 template<class DegCacheMgr, class NaviType, class SizeType> 00559 bool max_degree_on_then(const DegCacheMgr& deg_mgr, NaviType navi, 00560 SizeType degree, valid_tag is_descending) { 00561 navi.incrementThen(); 00562 return ((dd_cached_degree(deg_mgr, navi, degree - 1) + 1) == degree); 00563 } 00564 00565 template<class DegCacheMgr, class NaviType, class SizeType> 00566 bool max_degree_on_then(const DegCacheMgr& deg_mgr, NaviType navi, 00567 SizeType degree, invalid_tag non_descending) { 00568 navi.incrementElse(); 00569 return (dd_cached_degree(deg_mgr, navi, degree) != degree); 00570 } 00571 00572 00573 // with degree bound 00574 template <class CacheType, class DegCacheMgr, class NaviType, 00575 class TermType, class SizeType, class DescendingProperty> 00576 TermType 00577 dd_recursive_degree_lead(const CacheType& cache_mgr, const DegCacheMgr& 00578 deg_mgr, 00579 NaviType navi, TermType init, SizeType degree, 00580 DescendingProperty prop) { 00581 00582 if ((degree == 0) || navi.isConstant()) 00583 return cache_mgr.generate(navi); 00584 00585 // Check cache for previous results 00586 NaviType cached = cache_mgr.find(navi); 00587 if (cached.isValid()) 00588 return cache_mgr.generate(cached); 00589 00590 // Go to next branch 00591 if ( max_degree_on_then(deg_mgr, navi, degree, prop) ) { 00592 NaviType then_branch = navi.thenBranch(); 00593 init = dd_recursive_degree_lead(cache_mgr, deg_mgr, then_branch, 00594 init, degree - 1, prop); 00595 if ((navi.elseBranch().isEmpty()) && (init.navigation()==then_branch)) 00596 init = cache_mgr.generate(navi); 00597 else 00598 init = init.change(*navi); 00599 00600 } 00601 else { 00602 init = dd_recursive_degree_lead(cache_mgr, deg_mgr, navi.elseBranch(), 00603 init, degree, prop); 00604 } 00605 00606 NaviType resultNavi(init.navigation()); 00607 cache_mgr.insert(navi, resultNavi); 00608 deg_mgr.insert(resultNavi, degree); 00609 00610 return init; 00611 } 00612 00613 template <class CacheType, class DegCacheMgr, class NaviType, 00614 class TermType, class DescendingProperty> 00615 TermType 00616 dd_recursive_degree_lead(const CacheType& cache_mgr, const DegCacheMgr& deg_mgr, 00617 NaviType navi, TermType init, DescendingProperty prop){ 00618 00619 if (navi.isConstant()) 00620 return cache_mgr.generate(navi); 00621 00622 return dd_recursive_degree_lead(cache_mgr, deg_mgr, navi, init, 00623 dd_cached_degree(deg_mgr, navi), prop); 00624 } 00625 00626 template <class CacheType, class DegCacheMgr, class NaviType, 00627 class TermType, class SizeType, class DescendingProperty> 00628 TermType& 00629 dd_recursive_degree_leadexp(const CacheType& cache_mgr, 00630 const DegCacheMgr& deg_mgr, 00631 NaviType navi, TermType& result, 00632 SizeType degree, 00633 DescendingProperty prop) { 00634 00635 if ((degree == 0) || navi.isConstant()) 00636 return result; 00637 00638 // Check cache for previous result 00639 NaviType cached = cache_mgr.find(navi); 00640 if (cached.isValid()) 00641 return result = result.multiplyFirst(cache_mgr.generate(cached)); 00642 00643 // Prepare next branch 00644 if ( max_degree_on_then(deg_mgr, navi, degree, prop) ) { 00645 result.push_back(*navi); 00646 navi.incrementThen(); 00647 --degree; 00648 } 00649 else 00650 navi.incrementElse(); 00651 00652 return 00653 dd_recursive_degree_leadexp(cache_mgr, deg_mgr, navi, result, degree, prop); 00654 } 00655 00656 template <class CacheType, class DegCacheMgr, class NaviType, 00657 class TermType, class DescendingProperty> 00658 TermType& 00659 dd_recursive_degree_leadexp(const CacheType& cache_mgr, 00660 const DegCacheMgr& deg_mgr, 00661 NaviType navi, TermType& result, 00662 DescendingProperty prop) { 00663 00664 if (navi.isConstant()) 00665 return result; 00666 00667 return dd_recursive_degree_leadexp(cache_mgr, deg_mgr, navi, result, 00668 dd_cached_degree(deg_mgr, navi), prop); 00669 } 00670 00671 // Existential Abstraction. Given a ZDD F, and a set of variables 00672 // S, remove all occurrences of s in S from any subset in F. This can 00673 // be implemented by cofactoring F with respect to s = 1 and s = 0, 00674 // then forming the union of these results. 00675 00676 00677 template <class CacheType, class NaviType, class TermType> 00678 TermType 00679 dd_existential_abstraction(const CacheType& cache_mgr, 00680 NaviType varsNavi, NaviType navi, TermType init){ 00681 00682 typedef typename TermType::dd_type dd_type; 00683 typedef typename TermType::idx_type idx_type; 00684 00685 if (navi.isConstant()) 00686 return cache_mgr.generate(navi); 00687 00688 idx_type index(*navi); 00689 while (!varsNavi.isConstant() && ((*varsNavi) < index)) 00690 varsNavi.incrementThen(); 00691 00692 if (varsNavi.isConstant()) 00693 return cache_mgr.generate(navi); 00694 00695 // Check cache for previous result 00696 NaviType cached = cache_mgr.find(varsNavi, navi); 00697 if (cached.isValid()) 00698 return cache_mgr.generate(cached); 00699 00700 NaviType thenNavi(navi.thenBranch()), elseNavi(navi.elseBranch()); 00701 00702 TermType thenResult = 00703 dd_existential_abstraction(cache_mgr, varsNavi, thenNavi, init); 00704 00705 TermType elseResult = 00706 dd_existential_abstraction(cache_mgr, varsNavi, elseNavi, init); 00707 00708 if ((*varsNavi) == index) 00709 init = thenResult.unite(elseResult); 00710 else if ( (thenResult.navigation() == thenNavi) && 00711 (elseResult.navigation() == elseNavi) ) 00712 init = cache_mgr.generate(navi); 00713 else 00714 init = dd_type(index, thenResult, elseResult); 00715 00716 // Insert result to cache 00717 cache_mgr.insert(varsNavi, navi, init.navigation()); 00718 00719 return init; 00720 } 00721 00722 00723 00724 template <class CacheType, class NaviType, class PolyType> 00725 PolyType 00726 dd_divide_recursively(const CacheType& cache_mgr, 00727 NaviType navi, NaviType monomNavi, PolyType init){ 00728 00729 // Extract subtypes 00730 typedef typename NaviType::idx_type idx_type; 00731 typedef NaviType navigator; 00732 typedef typename PolyType::dd_type dd_type; 00733 00734 if (monomNavi.isConstant()) { 00735 if(monomNavi.terminalValue()) 00736 return cache_mgr.generate(navi); 00737 else 00738 return cache_mgr.zero(); 00739 } 00740 00741 assert(monomNavi.elseBranch().isEmpty()); 00742 00743 if (navi.isConstant()) 00744 return cache_mgr.zero(); 00745 00746 if (monomNavi == navi) 00747 return cache_mgr.one(); 00748 00749 // Look up, whether operation was already used 00750 navigator cached = cache_mgr.find(navi, monomNavi); 00751 00752 if (cached.isValid()) { // Cache lookup sucessful 00753 return cache_mgr.generate(cached); 00754 } 00755 00756 // Cache lookup not sucessful 00757 // Get top variables' index 00758 00759 idx_type index = *navi; 00760 idx_type monomIndex = *monomNavi; 00761 00762 if (monomIndex == index) { // Case: monom and poly start with same index 00763 00764 // Increment navigators 00765 navigator monomThen = monomNavi.thenBranch(); 00766 navigator naviThen = navi.thenBranch(); 00767 00768 init = dd_divide_recursively(cache_mgr, naviThen, monomThen, init); 00769 } 00770 else if (monomIndex > index) { // Case: monomIndex may occure within poly 00771 00772 init = 00773 dd_type(index, 00774 dd_divide_recursively(cache_mgr, navi.thenBranch(), monomNavi, 00775 init).diagram(), 00776 dd_divide_recursively(cache_mgr, navi.elseBranch(), monomNavi, 00777 init).diagram() ); 00778 } 00779 00780 // Insert in cache 00781 cache_mgr.insert(navi, monomNavi, init.navigation()); 00782 00783 return init; 00784 } 00785 00786 00787 00788 template <class DDGenerator, class Iterator, class NaviType, class PolyType> 00789 PolyType 00790 dd_divide_recursively_exp(const DDGenerator& ddgen, 00791 NaviType navi, Iterator start, Iterator finish, 00792 PolyType init){ 00793 00794 // Extract subtypes 00795 typedef typename NaviType::idx_type idx_type; 00796 typedef typename PolyType::dd_type dd_type; 00797 typedef NaviType navigator; 00798 00799 if (start == finish) 00800 return ddgen.generate(navi); 00801 00802 if (navi.isConstant()) 00803 return ddgen.zero(); 00804 00805 00806 // Cache lookup not sucessful 00807 // Get top variables' index 00808 00809 idx_type index = *navi; 00810 idx_type monomIndex = *start; 00811 00812 PolyType result; 00813 if (monomIndex == index) { // Case: monom and poly start with same index 00814 00815 // Increment navigators 00816 ++start; 00817 navigator naviThen = navi.thenBranch(); 00818 00819 result = dd_divide_recursively_exp(ddgen, naviThen, start, finish, init); 00820 } 00821 else if (monomIndex > index) { // Case: monomIndex may occure within poly 00822 00823 result = 00824 dd_type(index, 00825 dd_divide_recursively_exp(ddgen, navi.thenBranch(), start, finish, 00826 init).diagram(), 00827 dd_divide_recursively_exp(ddgen, navi.elseBranch(), start, finish, 00828 init).diagram() ); 00829 } 00830 else 00831 result = ddgen.zero(); 00832 00833 return result; 00834 } 00835 00838 template <class CacheType, class NaviType, class MonomType> 00839 MonomType 00840 cached_used_vars(const CacheType& cache, NaviType navi, MonomType init) { 00841 00842 if (navi.isConstant()) // No need for caching of constant nodes' degrees 00843 return init; 00844 00845 // Look whether result was cached before 00846 NaviType cached_result = cache.find(navi); 00847 00848 typedef typename MonomType::poly_type poly_type; 00849 if (cached_result.isValid()) 00850 return CDDOperations<typename MonomType::dd_type, 00851 MonomType>().getMonomial(cache.generate(cached_result)); 00852 00853 MonomType result = cached_used_vars(cache, navi.thenBranch(), init); 00854 result *= cached_used_vars(cache, navi.elseBranch(), init); 00855 00856 result.changeAssign(*navi); 00857 00858 // Write result to cache 00859 cache.insert(navi, result.diagram().navigation()); 00860 00861 return result; 00862 } 00863 00864 template <class NaviType, class Iterator> 00865 bool 00866 dd_owns(NaviType navi, Iterator start, Iterator finish) { 00867 00868 if (start == finish) { 00869 while(!navi.isConstant()) 00870 navi.incrementElse(); 00871 return navi.terminalValue(); 00872 } 00873 00874 while(!navi.isConstant() && (*start > *navi) ) 00875 navi.incrementElse(); 00876 00877 if (navi.isConstant() || (*start != *navi)) 00878 return false; 00879 00880 return dd_owns(navi.thenBranch(), ++start, finish); 00881 } 00882 00883 // determine the part of a polynomials of a given degree 00884 template <class CacheType, class NaviType, class DegType, class SetType> 00885 SetType 00886 dd_graded_part(const CacheType& cache, NaviType navi, DegType deg, 00887 SetType init) { 00888 00889 00890 if (deg == 0) { 00891 while(!navi.isConstant()) 00892 navi.incrementElse(); 00893 return cache.generate(navi); 00894 } 00895 00896 if(navi.isConstant()) 00897 return cache.zero(); 00898 00899 // Look whether result was cached before 00900 NaviType cached = cache.find(navi, deg); 00901 00902 if (cached.isValid()) 00903 return cache.generate(cached); 00904 00905 SetType result = 00906 SetType(*navi, 00907 dd_graded_part(cache, navi.thenBranch(), deg - 1, init), 00908 dd_graded_part(cache, navi.elseBranch(), deg, init) 00909 ); 00910 00911 // store result for later reuse 00912 cache.insert(navi, deg, result.navigation()); 00913 00914 return result; 00915 } 00916 00917 00922 template <class CacheManager, class NaviType, class SetType> 00923 SetType 00924 dd_first_divisors_of(CacheManager cache_mgr, NaviType navi, 00925 NaviType rhsNavi, SetType init ) { 00926 00927 typedef typename SetType::dd_type dd_type; 00928 while( (!navi.isConstant()) && (*rhsNavi != *navi) ) { 00929 00930 if ( (*rhsNavi < *navi) && (!rhsNavi.isConstant()) ) 00931 rhsNavi.incrementThen(); 00932 else 00933 navi.incrementElse(); 00934 } 00935 00936 if (navi.isConstant()) // At end of path 00937 return cache_mgr.generate(navi); 00938 00939 // Look up, whether operation was already used 00940 NaviType result = cache_mgr.find(navi, rhsNavi); 00941 00942 if (result.isValid()) // Cache lookup sucessful 00943 return cache_mgr.generate(result); 00944 00945 assert(*rhsNavi == *navi); 00946 00947 // Compute new result 00948 init = dd_type(*rhsNavi, 00949 dd_first_divisors_of(cache_mgr, navi.thenBranch(), rhsNavi, 00950 init).diagram(), 00951 dd_first_divisors_of(cache_mgr, navi.elseBranch(), rhsNavi, 00952 init).diagram() ); 00953 // Insert result to cache 00954 cache_mgr.insert(navi, rhsNavi, init.navigation()); 00955 00956 return init; 00957 } 00958 00959 template <class CacheType, class NaviType, class SetType> 00960 SetType 00961 dd_first_multiples_of(const CacheType& cache_mgr, 00962 NaviType navi, NaviType rhsNavi, SetType init){ 00963 00964 typedef typename SetType::dd_type dd_type; 00965 00966 if(rhsNavi.isConstant()) 00967 if(rhsNavi.terminalValue()) 00968 return cache_mgr.generate(navi); 00969 else 00970 return cache_mgr.generate(rhsNavi); 00971 00972 if (navi.isConstant() || (*navi > *rhsNavi)) 00973 return cache_mgr.zero(); 00974 00975 if (*navi == *rhsNavi) 00976 return dd_first_multiples_of(cache_mgr, navi.thenBranch(), 00977 rhsNavi.thenBranch(), init).change(*navi); 00978 00979 // Look up old result - if any 00980 NaviType result = cache_mgr.find(navi, rhsNavi); 00981 00982 if (result.isValid()) 00983 return cache_mgr.generate(result); 00984 00985 // Compute new result 00986 init = dd_type(*navi, 00987 dd_first_multiples_of(cache_mgr, navi.thenBranch(), 00988 rhsNavi, init).diagram(), 00989 dd_first_multiples_of(cache_mgr, navi.elseBranch(), 00990 rhsNavi, init).diagram() ); 00991 00992 // Insert new result in cache 00993 cache_mgr.insert(navi, rhsNavi, init.navigation()); 00994 00995 return init; 00996 } 00997 00998 00999 END_NAMESPACE_PBORI