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