00001
00002
00152
00153
00154
00155 #include "pbori_defs.h"
00156
00157
00158 #include "CIdxVariable.h"
00159
00160
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()){
00193 if (navi.terminalValue())
00194 return 0;
00195 else
00196 return -1;
00197 }
00198
00199
00200 typename DegreeCacher::node_type result = cache.find(navi);
00201 if (result.isValid())
00202 return *result;
00203
00204
00205 deg_type deg = dd_cached_degree(cache, navi.thenBranch()) + 1;
00206
00207
00208 deg = std::max(deg, dd_cached_degree(cache, navi.elseBranch()) );
00209
00210
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
00227 if (bound == 0 || navi.isConstant())
00228 return 0;
00229
00230
00231 typename DegreeCacher::node_type result = cache.find(navi);
00232 if (result.isValid())
00233 return *result;
00234
00235
00236 deg_type deg = dd_cached_degree(cache, navi.thenBranch(), bound - 1) + 1;
00237
00238
00239 if (bound > deg)
00240 deg = std::max(deg, dd_cached_degree(cache, navi.elseBranch(), bound) );
00241
00242
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
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
00328 navigator cached = cache_mgr.find(firstNavi, secondNavi);
00329 PolyType result = cache_mgr.zero();
00330
00331 if (cached.isValid()) {
00332 return cache_mgr.generate(cached);
00333 }
00334 else {
00335
00336
00337 if (*secondNavi < *firstNavi)
00338 std::swap(firstNavi, secondNavi);
00339
00340 idx_type index = *firstNavi;
00341
00342
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
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
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
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
00449 navigator cached = cache_mgr.find(monomNavi, navi);
00450
00451 if (cached.isValid()) {
00452 return cache_mgr.generate(cached);
00453 }
00454
00455
00456
00457
00458 idx_type index = *navi;
00459 idx_type monomIndex = *monomNavi;
00460
00461 if (monomIndex < index) {
00462 init = dd_multiply_recursively(cache_mgr, monomNavi.thenBranch(), navi,
00463 init, monom_tag).diagram().change(monomIndex);
00464 }
00465 else if (monomIndex == index) {
00466
00467
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 {
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
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
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
00526
00527
00528 idx_type index = *navi;
00529 idx_type monomIndex = *start;
00530
00531 if (monomIndex < index) {
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) {
00546
00547
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 {
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
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
00599 NaviType cached = cache_mgr.find(navi);
00600 if (cached.isValid())
00601 return cache_mgr.generate(cached);
00602
00603
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
00652 NaviType cached = cache_mgr.find(navi);
00653 if (cached.isValid())
00654 return result = result.multiplyFirst(cache_mgr.generate(cached));
00655
00656
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
00685
00686
00687
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
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
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
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
00763 navigator cached = cache_mgr.find(navi, monomNavi);
00764
00765 if (cached.isValid()) {
00766 return cache_mgr.generate(cached);
00767 }
00768
00769
00770
00771
00772 idx_type index = *navi;
00773 idx_type monomIndex = *monomNavi;
00774
00775 if (monomIndex == index) {
00776
00777
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) {
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
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
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
00820
00821
00822 idx_type index = *navi;
00823 idx_type monomIndex = *start;
00824
00825 PolyType result;
00826 if (monomIndex == index) {
00827
00828
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) {
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())
00856 return init;
00857
00858
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
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
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
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
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())
00949 return cache_mgr.generate(navi);
00950
00951
00952 NaviType result = cache_mgr.find(navi, rhsNavi);
00953
00954 if (result.isValid())
00955 return cache_mgr.generate(result);
00956
00957 assert(*rhsNavi == *navi);
00958
00959
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
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
00992 NaviType result = cache_mgr.find(navi, rhsNavi);
00993
00994 if (result.isValid())
00995 return cache_mgr.generate(result);
00996
00997
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
01005 cache_mgr.insert(navi, rhsNavi, init.navigation());
01006
01007 return init;
01008 }
01009
01010
01011 END_NAMESPACE_PBORI