• 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 //*****************************************************************************
00143 //*****************************************************************************
00144 
00145 // include basic definitions
00146 #include "pbori_defs.h"
00147 
00148 // temprarily
00149 #include "CIdxVariable.h"
00150 
00151 // temprarily
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()) // No need for caching of constant nodes' degrees
00184     return 0;
00185  
00186   // Look whether result was cached before
00187   typename DegreeCacher::node_type result = cache.find(navi);
00188   if (result.isValid())
00189     return *result;
00190 
00191   // Get degree of then branch (contains at least one valid path)...
00192   size_type deg = dd_cached_degree(cache, navi.thenBranch()) + 1;
00193  
00194   // ... combine with degree of else branch
00195   deg = std::max(deg,  dd_cached_degree(cache, navi.elseBranch()) );
00196 
00197   // Write result to cache
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   // No need for caching of constant nodes' degrees
00214   if (bound == 0 || navi.isConstant())
00215     return 0;
00216  
00217   // Look whether result was cached before
00218   typename DegreeCacher::node_type result = cache.find(navi);
00219   if (result.isValid())
00220     return *result;
00221 
00222   // Get degree of then branch (contains at least one valid path)...
00223   size_type deg = dd_cached_degree(cache, navi.thenBranch(), bound - 1) + 1;
00224 
00225   // ... combine with degree of else branch
00226   if (bound > deg)              // if deg <= bound, we are already finished
00227     deg = std::max(deg,  dd_cached_degree(cache, navi.elseBranch(), bound) );
00228 
00229   // Write result to cache
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   // Extract subtypes
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   // Look up, whether operation was already used
00315   navigator cached = cache_mgr.find(firstNavi, secondNavi);
00316   PolyType result = cache_mgr.zero();
00317 
00318   if (cached.isValid()) {       // Cache lookup sucessful
00319     return cache_mgr.generate(cached);
00320   }
00321   else {                        // Cache lookup not sucessful
00322     // Get top variable's index
00323 
00324     if (*secondNavi < *firstNavi)
00325       std::swap(firstNavi, secondNavi);
00326 
00327     idx_type index = *firstNavi;
00328 
00329     // Get then- and else-branches wrt. current indexed variable
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         // Do recursion
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     // Insert in cache
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   // Extract subtypes
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   // Look up, whether operation was already used
00436   navigator cached = cache_mgr.find(monomNavi, navi);
00437 
00438   if (cached.isValid()) {       // Cache lookup sucessful
00439     return cache_mgr.generate(cached);
00440   }
00441 
00442   // Cache lookup not sucessful
00443   // Get top variables' index
00444 
00445   idx_type index = *navi;
00446   idx_type monomIndex = *monomNavi;
00447 
00448   if (monomIndex < index) {     // Case: index may occure within monom
00449     init = dd_multiply_recursively(cache_mgr, monomNavi.thenBranch(), navi,
00450                                    init, monom_tag).diagram().change(monomIndex);
00451   }
00452   else if (monomIndex == index) { // Case: monom and poly start with same index
00453 
00454     // Increment navigators
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 {                        // Case: var(index) not part of monomial
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   // Insert in cache
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   // Extract subtypes
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   // Cache lookup not sucessful
00513   // Get top variables' index
00514 
00515   idx_type index = *navi;
00516   idx_type monomIndex = *start;
00517 
00518   if (monomIndex < index) {     // Case: index may occure within monom
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) { // Case: monom and poly start with same index
00533 
00534     // Increment navigators
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 {                        // Case: var(index) not part of monomial
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 // with degree bound
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   // Check cache for previous results
00586   NaviType cached = cache_mgr.find(navi);
00587   if (cached.isValid())
00588     return cache_mgr.generate(cached);
00589 
00590   // Go to next branch
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   // Check cache for previous result
00639   NaviType cached = cache_mgr.find(navi);
00640   if (cached.isValid())
00641     return result = result.multiplyFirst(cache_mgr.generate(cached));
00642 
00643   // Prepare next branch
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 // Existential Abstraction. Given a ZDD F, and a set of variables
00672 // S, remove all occurrences of s in S from any subset in F. This can
00673 // be implemented by cofactoring F with respect to s = 1 and s = 0,
00674 // then forming the union of these results. 
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   // Check cache for previous result
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   // Insert result to cache
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   // Extract subtypes
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   // Look up, whether operation was already used
00750   navigator cached = cache_mgr.find(navi, monomNavi);
00751 
00752   if (cached.isValid()) {       // Cache lookup sucessful
00753     return cache_mgr.generate(cached);
00754   }
00755 
00756   // Cache lookup not sucessful
00757   // Get top variables' index
00758 
00759   idx_type index = *navi;
00760   idx_type monomIndex = *monomNavi;
00761 
00762   if (monomIndex == index) {    // Case: monom and poly start with same index
00763 
00764     // Increment navigators
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) { // Case: monomIndex may occure within poly
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   // Insert in cache
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   // Extract subtypes
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   // Cache lookup not sucessful
00807   // Get top variables' index
00808 
00809   idx_type index = *navi;
00810   idx_type monomIndex = *start;
00811 
00812   PolyType result;
00813   if (monomIndex == index) {    // Case: monom and poly start with same index
00814 
00815     // Increment navigators
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) { // Case: monomIndex may occure within poly
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()) // No need for caching of constant nodes' degrees
00843     return init;
00844  
00845   // Look whether result was cached before
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   // Write result to cache
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 // determine the part of a polynomials of a given degree
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   // Look whether result was cached before
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   // store result for later reuse
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())        // At end of path
00937     return cache_mgr.generate(navi);
00938 
00939   // Look up, whether operation was already used
00940   NaviType result = cache_mgr.find(navi, rhsNavi);
00941     
00942   if (result.isValid())       // Cache lookup sucessful
00943     return  cache_mgr.generate(result);
00944   
00945   assert(*rhsNavi == *navi);
00946    
00947   // Compute new result
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   // Insert result to cache
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   // Look up old result - if any
00980   NaviType result = cache_mgr.find(navi, rhsNavi);
00981 
00982   if (result.isValid())
00983     return cache_mgr.generate(result);
00984 
00985   // Compute new result
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   // Insert new result in cache
00993   cache_mgr.insert(navi, rhsNavi, init.navigation());
00994 
00995   return init;
00996 }
00997 
00998 
00999 END_NAMESPACE_PBORI

Generated on Thu Oct 21 2010 02:56:33 for PolyBoRi by  doxygen 1.7.1