PolyBoRi
pbori_algorithms.h
Go to the documentation of this file.
00001 // -*- c++ -*-
00002 //*****************************************************************************
00018 //*****************************************************************************
00019 
00020 #ifndef pbori_algorithms_h_
00021 #define pbori_algorithms_h_
00022 
00023 // include standard headers
00024 #include <numeric>
00025 
00026 // include basic definitions
00027 #include "pbori_defs.h"
00028 
00029 // include PolyBoRi algorithm, which do not depend on PolyBoRi classes
00030 #include "pbori_algo.h"
00031 
00032 // include PolyBoRi class definitions, which are used here
00033 #include "BoolePolynomial.h"
00034 #include "BooleMonomial.h"
00035 #include "CGenericIter.h"
00036 
00037 
00038 BEGIN_NAMESPACE_PBORI
00039 
00041 inline BoolePolynomial 
00042 spoly(const BoolePolynomial& first, const BoolePolynomial& second){
00043 
00044    BooleMonomial lead1(first.lead()), lead2(second.lead());
00045 
00046    BooleMonomial prod = lead1;
00047    prod *= lead2;
00048 
00049    return ( first * (prod / lead1) ) + ( second * (prod / lead2) );
00050 }
00051 
00052 template <class NaviType, class LowerIterator, class ValueType>
00053 ValueType 
00054 lower_term_accumulate(NaviType navi, 
00055                       LowerIterator lstart, LowerIterator lfinish, 
00056                       ValueType init) {
00057   assert(init.isZero());
00059   if (lstart == lfinish){
00060     return init;
00061   }
00062   
00063   if (navi.isConstant())
00064     return (navi.terminalValue()? (ValueType)init.ring().one(): init);
00065   
00066   assert(*lstart >= *navi);
00067 
00068   ValueType result;
00069   if (*lstart > *navi) {
00070 
00071     ValueType reselse = 
00072       lower_term_accumulate(navi.elseBranch(), lstart, lfinish, init);
00073 
00074 //     if(reselse.isZero())
00075 //       return BooleSet(navi.thenBranch()).change(*navi);
00076 
00077     // Note: result == BooleSet(navi) holds only in trivial cases, so testing
00078     // reselse.navigation() == navi.elseBranch() is almost always false
00079     // Hence, checking reselse.navigation() == navi.elseBranch() for returning
00080     // navi, instead of result yields too much overhead.
00081     result = BooleSet(*navi, navi.thenBranch(), reselse.navigation(), 
00082                       init.ring());
00083   }
00084   else  {
00085     assert(*lstart == *navi);
00086     ++lstart;
00087     BooleSet resthen = 
00088       lower_term_accumulate(navi.thenBranch(), lstart, lfinish, init).diagram();
00089 
00090     result = resthen.change(*navi);
00091   }
00092 
00093   return  result;
00094 }
00095 
00096 
00097 template <class UpperIterator, class NaviType, class ValueType>
00098 ValueType 
00099 upper_term_accumulate(UpperIterator ustart, UpperIterator ufinish,
00100                       NaviType navi, ValueType init) {
00101 
00102   // Note: Recursive caching, wrt. a navigator representing the term
00103   // corresponding to ustart .. ufinish cannot be efficient here, because
00104   // dereferencing the term is as expensive as this procedure in whole. (Maybe
00105   // the generation of the BooleSet in the final line could be cached somehow.)
00106 
00107   // assuming (ustart .. ufinish) never means zero
00108   if (ustart == ufinish)
00109     return init.ring().one();
00110   
00111   while (*navi < *ustart)
00112     navi.incrementElse();
00113   ++ustart;
00114   NaviType navithen = navi.thenBranch();
00115   ValueType resthen = upper_term_accumulate(ustart, ufinish, navithen, init);
00116 
00117   // The following condition holds quite often, so computation time may be saved
00118   if (navithen == resthen.navigation())
00119     return BooleSet(navi, init.ring());
00120 
00121   return BooleSet(*navi, resthen.navigation(), navi.elseBranch(), init.ring());
00122 }
00123 
00124 // assuming lstart .. lfinish *not* marking the term one
00125 template <class UpperIterator, class NaviType, class LowerIterator, 
00126           class ValueType>
00127 ValueType 
00128 term_accumulate(UpperIterator ustart, UpperIterator ufinish, NaviType navi, 
00129                 LowerIterator lstart, LowerIterator lfinish, ValueType init) {
00130 
00131 
00132   if (lstart == lfinish)
00133     return upper_term_accumulate(ustart, ufinish, navi, init);
00134 
00135   if (ustart == ufinish)
00136     return init.ring().one();
00137 
00138   while (*navi < *ustart)
00139     navi.incrementElse();
00140   ++ustart;
00141 
00142   
00143   if (navi.isConstant())
00144     return BooleSet(navi, init.ring());
00145 
00146   assert(*lstart >= *navi);
00147 
00148   ValueType result;
00149   if (*lstart > *navi) {
00150     ValueType resthen = 
00151       upper_term_accumulate(ustart, ufinish, navi.thenBranch(), init);
00152     ValueType reselse = 
00153       lower_term_accumulate(navi.elseBranch(), lstart, lfinish, init);
00154 
00155     result = BooleSet(*navi, resthen.navigation(), reselse.navigation(),
00156                       init.ring());
00157   }
00158   else  {
00159     assert(*lstart == *navi);
00160     ++lstart;
00161      BooleSet resthen = term_accumulate(ustart, ufinish,  navi.thenBranch(),
00162                                         lstart, lfinish, init).diagram();
00163  
00164     result = resthen.change(*navi);
00165   }
00166 
00167   return result;
00168 }
00169 
00170 
00171 
00172 
00174 template <class InputIterator, class ValueType>
00175 ValueType 
00176 term_accumulate(InputIterator first, InputIterator last, ValueType init) {
00177 
00178 #ifdef PBORI_ALT_TERM_ACCUMULATE
00179   if(last.isOne())
00180     return upper_term_accumulate(first.begin(), first.end(), 
00181                                  first.navigation(), init) + ValueType(1);
00182   
00183   ValueType result = term_accumulate(first.begin(), first.end(), 
00184                                      first.navigation(),
00185                                      last.begin(), last.end(), init);
00186 
00187   
00188   // alternative
00189   /*  ValueType result = upper_term_accumulate(first.begin(), first.end(), 
00190                                            first.navigation(), init);
00191 
00192 
00193   result = lower_term_accumulate(result.navigation(),
00194                                  last.begin(), last.end(), init);
00195 
00196   */
00197 
00198   assert(result == std::accumulate(first, last, init) ); 
00199 
00200   return result;
00201 
00202 #else
00203 
00206   if(first.isZero())
00207     return typename ValueType::dd_type(init.ring(),
00208                                        first.navigation());
00209 
00210   ValueType result = upper_term_accumulate(first.begin(), first.end(), 
00211                                            first.navigation(), init);
00212   if(!last.isZero())
00213     result += upper_term_accumulate(last.begin(), last.end(), 
00214                                     last.navigation(), init);
00215 
00216   assert(result == std::accumulate(first, last, init) ); 
00217 
00218   return result;
00219 #endif
00220 }
00221 
00222 
00223 // determine the part of a polynomials of a given degree
00224 template <class CacheType, class NaviType, class SetType>
00225 SetType
00226 dd_mapping(const CacheType& cache, NaviType navi, NaviType map, SetType init) {
00227 
00228   if (navi.isConstant())
00229     return cache.generate(navi);
00230 
00231   while (*map < *navi) {
00232     assert(!map.isConstant());
00233     map.incrementThen();
00234   }
00235 
00236   assert(*navi == *map);
00237 
00238   NaviType cached = cache.find(navi, map);
00239 
00240   // look whether computation was done before
00241   if (cached.isValid())
00242     return SetType(cached, cache.ring());
00243 
00244   SetType result = 
00245     SetType(*(map.elseBranch()),  
00246             dd_mapping(cache, navi.thenBranch(), map.thenBranch(), init),
00247             dd_mapping(cache, navi.elseBranch(), map.thenBranch(), init)
00248             );
00249 
00250 
00251   // store result for later reuse
00252   cache.insert(navi, map, result.navigation());
00253 
00254   return result;
00255 }
00256 
00257 
00258 template <class PolyType, class MapType>
00259 PolyType
00260 apply_mapping(const PolyType& poly, const MapType& map) {
00261 
00262   CCacheManagement<typename PolyType::ring_type, typename CCacheTypes::mapping> 
00263     cache(poly.ring());
00264 
00265   return dd_mapping(cache, poly.navigation(), map.navigation(), 
00266                     typename PolyType::set_type()); 
00267 }
00268 
00269 
00270 template <class MonomType, class PolyType>
00271 PolyType
00272 generate_mapping(MonomType& fromVars, MonomType& toVars, PolyType init) {
00273 
00274   if(fromVars.isConstant()) {
00275     assert(fromVars.isOne() && toVars.isOne());
00276     return fromVars;
00277   }
00278 
00279   MonomType varFrom = fromVars.firstVariable();
00280   MonomType varTo = toVars.firstVariable();
00281   fromVars.popFirst();
00282   toVars.popFirst();
00283   return (varFrom * generate_mapping(fromVars, toVars, init)) + varTo;
00284 }
00285 
00286 template <class PolyType, class MonomType>
00287 PolyType
00288 mapping(PolyType poly, MonomType fromVars, MonomType toVars) {
00289 
00290   return apply_mapping(poly, generate_mapping(fromVars, toVars, PolyType()) );
00291 }
00292 
00293 
00294 
00295 END_NAMESPACE_PBORI
00296 
00297 #endif // pbori_algorithms_h_