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