• Main Page
  • Related Pages
  • Namespaces
  • Classes
  • Files
  • File List
  • File Members

pbori_routines_misc.h

Go to the documentation of this file.
00001 // -*- c++ -*-
00002 //*****************************************************************************
00152 //*****************************************************************************
00153 
00154 // include basic definitions
00155 #include "pbori_defs.h"
00156 
00157 // temprarily
00158 #include "CIdxVariable.h"
00159 
00160 // temprarily
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()){ // No need for caching of constant nodes' degrees
00193     if (navi.terminalValue())
00194         return 0;
00195     else
00196         return -1;
00197   }
00198  
00199   // Look whether result was cached before
00200   typename DegreeCacher::node_type result = cache.find(navi);
00201   if (result.isValid())
00202     return *result;
00203 
00204   // Get degree of then branch (contains at least one valid path)...
00205   deg_type deg = dd_cached_degree(cache, navi.thenBranch()) + 1;
00206  
00207   // ... combine with degree of else branch
00208   deg = std::max(deg,  dd_cached_degree(cache, navi.elseBranch()) );
00209 
00210   // Write result to cache
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   // No need for caching of constant nodes' degrees
00227   if (bound == 0 || navi.isConstant())
00228     return 0;
00229  
00230   // Look whether result was cached before
00231   typename DegreeCacher::node_type result = cache.find(navi);
00232   if (result.isValid())
00233     return *result;
00234 
00235   // Get degree of then branch (contains at least one valid path)...
00236   deg_type deg = dd_cached_degree(cache, navi.thenBranch(), bound - 1) + 1;
00237 
00238   // ... combine with degree of else branch
00239   if (bound > deg)              // if deg <= bound, we are already finished
00240     deg = std::max(deg,  dd_cached_degree(cache, navi.elseBranch(), bound) );
00241 
00242   // Write result to cache
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   // Extract subtypes
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   // Look up, whether operation was already used
00328   navigator cached = cache_mgr.find(firstNavi, secondNavi);
00329   PolyType result = cache_mgr.zero();
00330 
00331   if (cached.isValid()) {       // Cache lookup sucessful
00332     return cache_mgr.generate(cached);
00333   }
00334   else {                        // Cache lookup not sucessful
00335     // Get top variable's index
00336 
00337     if (*secondNavi < *firstNavi)
00338       std::swap(firstNavi, secondNavi);
00339 
00340     idx_type index = *firstNavi;
00341 
00342     // Get then- and else-branches wrt. current indexed variable
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         // Do recursion
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     // Insert in cache
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   // Extract subtypes
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   // Look up, whether operation was already used
00449   navigator cached = cache_mgr.find(monomNavi, navi);
00450 
00451   if (cached.isValid()) {       // Cache lookup sucessful
00452     return cache_mgr.generate(cached);
00453   }
00454 
00455   // Cache lookup not sucessful
00456   // Get top variables' index
00457 
00458   idx_type index = *navi;
00459   idx_type monomIndex = *monomNavi;
00460 
00461   if (monomIndex < index) {     // Case: index may occure within monom
00462     init = dd_multiply_recursively(cache_mgr, monomNavi.thenBranch(), navi,
00463                                    init, monom_tag).diagram().change(monomIndex);
00464   }
00465   else if (monomIndex == index) { // Case: monom and poly start with same index
00466 
00467     // Increment navigators
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 {                        // Case: var(index) not part of monomial
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   // Insert in cache
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   // Extract subtypes
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   // Cache lookup not sucessful
00526   // Get top variables' index
00527 
00528   idx_type index = *navi;
00529   idx_type monomIndex = *start;
00530 
00531   if (monomIndex < index) {     // Case: index may occure within monom
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) { // Case: monom and poly start with same index
00546 
00547     // Increment navigators
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 {                        // Case: var(index) not part of monomial
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 // with degree bound
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   // Check cache for previous results
00599   NaviType cached = cache_mgr.find(navi);
00600   if (cached.isValid())
00601     return cache_mgr.generate(cached);
00602 
00603   // Go to next branch
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   // Check cache for previous result
00652   NaviType cached = cache_mgr.find(navi);
00653   if (cached.isValid())
00654     return result = result.multiplyFirst(cache_mgr.generate(cached));
00655 
00656   // Prepare next branch
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 // Existential Abstraction. Given a ZDD F, and a set of variables
00685 // S, remove all occurrences of s in S from any subset in F. This can
00686 // be implemented by cofactoring F with respect to s = 1 and s = 0,
00687 // then forming the union of these results. 
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   // Check cache for previous result
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   // Insert result to cache
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   // Extract subtypes
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   // Look up, whether operation was already used
00763   navigator cached = cache_mgr.find(navi, monomNavi);
00764 
00765   if (cached.isValid()) {       // Cache lookup sucessful
00766     return cache_mgr.generate(cached);
00767   }
00768 
00769   // Cache lookup not sucessful
00770   // Get top variables' index
00771 
00772   idx_type index = *navi;
00773   idx_type monomIndex = *monomNavi;
00774 
00775   if (monomIndex == index) {    // Case: monom and poly start with same index
00776 
00777     // Increment navigators
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) { // Case: monomIndex may occure within poly
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   // Insert in cache
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   // Extract subtypes
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   // Cache lookup not sucessful
00820   // Get top variables' index
00821 
00822   idx_type index = *navi;
00823   idx_type monomIndex = *start;
00824 
00825   PolyType result;
00826   if (monomIndex == index) {    // Case: monom and poly start with same index
00827 
00828     // Increment navigators
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) { // Case: monomIndex may occure within poly
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()) // No need for caching of constant nodes' degrees
00856     return init;
00857  
00858   // Look whether result was cached before
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   // Write result to cache
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 // determine the part of a polynomials of a given degree
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   // Look whether result was cached before
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   // store result for later reuse
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())        // At end of path
00949     return cache_mgr.generate(navi);
00950 
00951   // Look up, whether operation was already used
00952   NaviType result = cache_mgr.find(navi, rhsNavi);
00953     
00954   if (result.isValid())       // Cache lookup sucessful
00955     return  cache_mgr.generate(result);
00956   
00957   assert(*rhsNavi == *navi);
00958    
00959   // Compute new result
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   // Insert result to cache
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   // Look up old result - if any
00992   NaviType result = cache_mgr.find(navi, rhsNavi);
00993 
00994   if (result.isValid())
00995     return cache_mgr.generate(result);
00996 
00997   // Compute new result
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   // Insert new result in cache
01005   cache_mgr.insert(navi, rhsNavi, init.navigation());
01006 
01007   return init;
01008 }
01009 
01010 
01011 END_NAMESPACE_PBORI

Generated on Wed Sep 29 2010 for PolyBoRi by  doxygen 1.7.1