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

pbori_algorithms.h

Go to the documentation of this file.
00001 // -*- c++ -*-
00002 //*****************************************************************************
00101 //*****************************************************************************
00102 
00103 #ifndef pbori_algorithms_h_
00104 #define pbori_algorithms_h_
00105 
00106 // include standard headers
00107 #include <numeric>
00108 
00109 // include basic definitions
00110 #include "pbori_defs.h"
00111 
00112 // include PolyBoRi algorithm, which do not depend on PolyBoRi classes
00113 #include "pbori_algo.h"
00114 
00115 // include PolyBoRi class definitions, which are used here
00116 #include "BoolePolynomial.h"
00117 #include "BooleMonomial.h"
00118 #include "CGenericIter.h"
00119 
00120 
00121 BEGIN_NAMESPACE_PBORI
00122 
00125 inline BoolePolynomial 
00126 spoly(const BoolePolynomial& first, const BoolePolynomial& second){
00127 
00128    BooleMonomial lead1(first.lead()), lead2(second.lead());
00129 
00130    BooleMonomial prod = lead1;
00131    prod *= lead2;
00132 
00133    return ( first * (prod / lead1) ) + ( second * (prod / lead2) );
00134 }
00135 
00136 template <class NaviType, class LowerIterator, class ValueType>
00137 ValueType 
00138 lower_term_accumulate(NaviType navi, 
00139                       LowerIterator lstart, LowerIterator lfinish, 
00140                       ValueType init) {
00141   assert(init.isZero());
00143   if (lstart == lfinish){
00144     return init;
00145   }
00146   
00147   if (navi.isConstant())
00148     return (navi.terminalValue()? (ValueType)init.ring().one(): init);
00149   
00150   assert(*lstart >= *navi);
00151 
00152   ValueType result;
00153   if (*lstart > *navi) {
00154 
00155     ValueType reselse = 
00156       lower_term_accumulate(navi.elseBranch(), lstart, lfinish, init);
00157 
00158 //     if(reselse.isZero())
00159 //       return BooleSet(navi.thenBranch()).change(*navi);
00160 
00161     // Note: result == BooleSet(navi) holds only in trivial cases, so testing
00162     // reselse.navigation() == navi.elseBranch() is almost always false
00163     // Hence, checking reselse.navigation() == navi.elseBranch() for returning
00164     // navi, instead of result yields too much overhead.
00165     result = BooleSet(*navi, navi.thenBranch(), reselse.navigation(), 
00166                       init.ring());
00167   }
00168   else  {
00169     assert(*lstart == *navi);
00170     ++lstart;
00171     BooleSet resthen = 
00172       lower_term_accumulate(navi.thenBranch(), lstart, lfinish, init).diagram();
00173 
00174     result = resthen.change(*navi);
00175   }
00176 
00177   return  result;
00178 }
00179 
00180 
00181 template <class UpperIterator, class NaviType, class ValueType>
00182 ValueType 
00183 upper_term_accumulate(UpperIterator ustart, UpperIterator ufinish,
00184                       NaviType navi, ValueType init) {
00185 
00186   // Note: Recursive caching, wrt. a navigator representing the term
00187   // corresponding to ustart .. ufinish cannot be efficient here, because
00188   // dereferencing the term is as expensive as this procedure in whole. (Maybe
00189   // the generation of the BooleSet in the final line could be cached somehow.)
00190 
00191   // assuming (ustart .. ufinish) never means zero
00192   if (ustart == ufinish)
00193     return init.ring().one();
00194   
00195   while (*navi < *ustart)
00196     navi.incrementElse();
00197   ++ustart;
00198   NaviType navithen = navi.thenBranch();
00199   ValueType resthen = upper_term_accumulate(ustart, ufinish, navithen, init);
00200 
00201   // The following condition holds quite often, so computation time may be saved
00202   if (navithen == resthen.navigation())
00203     return BooleSet(navi, init.ring());
00204 
00205   return BooleSet(*navi, resthen.navigation(), navi.elseBranch(), init.ring());
00206 }
00207 
00209 template <class UpperIterator, class NaviType, class LowerIterator, 
00210           class ValueType>
00211 ValueType 
00212 term_accumulate(UpperIterator ustart, UpperIterator ufinish, NaviType navi, 
00213                 LowerIterator lstart, LowerIterator lfinish, ValueType init) {
00214 
00215 
00216   if (lstart == lfinish)
00217     return upper_term_accumulate(ustart, ufinish, navi, init);
00218 
00219   if (ustart == ufinish)
00220     return init.ring().one();
00221 
00222   while (*navi < *ustart)
00223     navi.incrementElse();
00224   ++ustart;
00225 
00226   
00227   if (navi.isConstant())
00228     return BooleSet(navi, init.ring());
00229 
00230   assert(*lstart >= *navi);
00231 
00232   ValueType result;
00233   if (*lstart > *navi) {
00234     ValueType resthen = 
00235       upper_term_accumulate(ustart, ufinish, navi.thenBranch(), init);
00236     ValueType reselse = 
00237       lower_term_accumulate(navi.elseBranch(), lstart, lfinish, init);
00238 
00239     result = BooleSet(*navi, resthen.navigation(), reselse.navigation(),
00240                       init.ring());
00241   }
00242   else  {
00243     assert(*lstart == *navi);
00244     ++lstart;
00245      BooleSet resthen = term_accumulate(ustart, ufinish,  navi.thenBranch(),
00246                                         lstart, lfinish, init).diagram();
00247  
00248     result = resthen.change(*navi);
00249   }
00250 
00251   return result;
00252 }
00253 
00254 
00255 
00256 
00259 template <class InputIterator, class ValueType>
00260 ValueType 
00261 term_accumulate(InputIterator first, InputIterator last, ValueType init) {
00262 
00263 #ifdef PBORI_ALT_TERM_ACCUMULATE
00264   if(last.isOne())
00265     return upper_term_accumulate(first.begin(), first.end(), 
00266                                  first.navigation(), init) + ValueType(1);
00267   
00268   ValueType result = term_accumulate(first.begin(), first.end(), 
00269                                      first.navigation(),
00270                                      last.begin(), last.end(), init);
00271 
00272   
00273   // alternative
00274   /*  ValueType result = upper_term_accumulate(first.begin(), first.end(), 
00275                                            first.navigation(), init);
00276 
00277 
00278   result = lower_term_accumulate(result.navigation(),
00279                                  last.begin(), last.end(), init);
00280 
00281   */
00282 
00283   assert(result == std::accumulate(first, last, init) ); 
00284 
00285   return result;
00286 
00287 #else
00288 
00291   if(first.isZero())
00292     return typename ValueType::dd_type(init.diagram().manager(),
00293                                        first.navigation());
00294 
00295   ValueType result = upper_term_accumulate(first.begin(), first.end(), 
00296                                            first.navigation(), init);
00297   if(!last.isZero())
00298     result += upper_term_accumulate(last.begin(), last.end(), 
00299                                     last.navigation(), init);
00300 
00301   assert(result == std::accumulate(first, last, init) ); 
00302 
00303   return result;
00304 #endif
00305 }
00306 
00307 
00308 // determine the part of a polynomials of a given degree
00309 template <class CacheType, class NaviType, class SetType>
00310 SetType
00311 dd_mapping(const CacheType& cache, NaviType navi, NaviType map, SetType init) {
00312 
00313   if (navi.isConstant())
00314     return cache.generate(navi);
00315 
00316   while (*map < *navi) {
00317     assert(!map.isConstant());
00318     map.incrementThen();
00319   }
00320 
00321   assert(*navi == *map);
00322 
00323   NaviType cached = cache.find(navi, map);
00324 
00325   // look whether computation was done before
00326   if (cached.isValid())
00327     return SetType(cached, cache.ring());
00328 
00329   SetType result = 
00330     SetType(*(map.elseBranch()),  
00331             dd_mapping(cache, navi.thenBranch(), map.thenBranch(), init),
00332             dd_mapping(cache, navi.elseBranch(), map.thenBranch(), init)
00333             );
00334 
00335 
00336   // store result for later reuse
00337   cache.insert(navi, map, result.navigation());
00338 
00339   return result;
00340 }
00341 
00342 
00343 template <class PolyType, class MapType>
00344 PolyType
00345 apply_mapping(const PolyType& poly, const MapType& map) {
00346 
00347   CCacheManagement<typename CCacheTypes::mapping> 
00348     cache(poly.diagram().manager());
00349 
00350   return dd_mapping(cache, poly.navigation(), map.navigation(), 
00351                     typename PolyType::set_type()); 
00352 }
00353 
00354 
00355 template <class MonomType, class PolyType>
00356 PolyType
00357 generate_mapping(MonomType& fromVars, MonomType& toVars, PolyType init) {
00358 
00359   if(fromVars.isConstant()) {
00360     assert(fromVars.isOne() && toVars.isOne());
00361     return fromVars;
00362   }
00363 
00364   MonomType varFrom = fromVars.firstVariable();
00365   MonomType varTo = toVars.firstVariable();
00366   fromVars.popFirst();
00367   toVars.popFirst();
00368   return (varFrom * generate_mapping(fromVars, toVars, init)) + varTo;
00369 }
00370 
00371 template <class PolyType, class MonomType>
00372 PolyType
00373 mapping(PolyType poly, MonomType fromVars, MonomType toVars) {
00374 
00375   return apply_mapping(poly, generate_mapping(fromVars, toVars, PolyType()) );
00376 }
00377 
00378 
00379 
00380 END_NAMESPACE_PBORI
00381 
00382 #endif // pbori_algorithms_h_

Generated on Thu Nov 4 2010 08:06:25 for PolyBoRi by  doxygen 1.7.1