PolyBoRi
pbori_routines_misc.h
Go to the documentation of this file.
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