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

pbori_algorithms.h

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

Generated on Tue Sep 14 2010 for PolyBoRi by  doxygen 1.7.1