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