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