PolyBoRi
pbori_algorithms.h
Go to the documentation of this file.
00001 // -*- c++ -*-
00002 //*****************************************************************************
00018 //*****************************************************************************
00019 
00020 #ifndef polybori_routines_pbori_algorithms_h_
00021 #define polybori_routines_pbori_algorithms_h_
00022 
00023 // include standard headers
00024 #include <numeric>
00025 
00026 // include basic definitions
00027 #include <polybori/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 <polybori/BoolePolynomial.h>
00034 #include <polybori/BooleMonomial.h>
00035 #include <polybori/iterators/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   PBORI_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   PBORI_ASSERT(*lstart >= *navi);
00067 
00068   ValueType result(init.ring());
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     PBORI_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   PBORI_ASSERT(*lstart >= *navi);
00147 
00148   ValueType result(init.ring());
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     PBORI_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   // test for non-lex more complicated (see testsuite)
00199   PBORI_ASSERT((init.ring().ordering().isLexicographical()?
00200           result == std::accumulate(first, last, init):
00201           true) ); 
00202 
00203 
00204   return result;
00205 
00206 #else
00207 
00210   if(first.isZero())
00211     return typename ValueType::dd_type(init.ring(),
00212                                        first.navigation());
00213 
00214   ValueType result = upper_term_accumulate(first.begin(), first.end(), 
00215                                            first.navigation(), init);
00216   if(!last.isZero())
00217     result += upper_term_accumulate(last.begin(), last.end(), 
00218                                     last.navigation(), init);
00219 
00220   // test for non-lex more complicated (see testsuite)
00221   PBORI_ASSERT((init.ring().ordering().isLexicographical()?
00222           result == std::accumulate(first, last, init):
00223           true) ); 
00224   
00225   return result;
00226 #endif
00227 }
00228 
00229 
00230 // determine the part of a polynomials of a given degree
00231 template <class CacheType, class NaviType, class SetType>
00232 SetType
00233 dd_mapping(const CacheType& cache, NaviType navi, NaviType map, SetType init) {
00234 
00235   if (navi.isConstant())
00236     return cache.generate(navi);
00237 
00238   while (*map < *navi) {
00239     PBORI_ASSERT(!map.isConstant());
00240     map.incrementThen();
00241   }
00242 
00243   PBORI_ASSERT(*navi == *map);
00244 
00245   NaviType cached = cache.find(navi, map);
00246 
00247   // look whether computation was done before
00248   if (cached.isValid())
00249     return SetType(cached, cache.ring());
00250 
00251   SetType result = 
00252     SetType(*(map.elseBranch()),  
00253             dd_mapping(cache, navi.thenBranch(), map.thenBranch(), init),
00254             dd_mapping(cache, navi.elseBranch(), map.thenBranch(), init)
00255             );
00256 
00257 
00258   // store result for later reuse
00259   cache.insert(navi, map, result.navigation());
00260 
00261   return result;
00262 }
00263 
00264 
00265 template <class PolyType, class MapType>
00266 PolyType
00267 apply_mapping(const PolyType& poly, const MapType& map) {
00268 
00269   CCacheManagement<typename PolyType::ring_type, typename CCacheTypes::mapping> 
00270     cache(poly.ring());
00271 
00272   return dd_mapping(cache, poly.navigation(), map.navigation(), 
00273                     typename PolyType::set_type(poly.ring())); 
00274 }
00275 
00276 
00277 template <class MonomType, class PolyType>
00278 PolyType
00279 generate_mapping(MonomType& fromVars, MonomType& toVars, PolyType init) {
00280 
00281   if(fromVars.isConstant()) {
00282     PBORI_ASSERT(fromVars.isOne() && toVars.isOne());
00283     return fromVars;
00284   }
00285 
00286   MonomType varFrom = fromVars.firstVariable();
00287   MonomType varTo = toVars.firstVariable();
00288   fromVars.popFirst();
00289   toVars.popFirst();
00290   return (varFrom * generate_mapping(fromVars, toVars, init)) + varTo;
00291 }
00292 
00293 template <class PolyType, class MonomType>
00294 PolyType
00295 mapping(PolyType poly, MonomType fromVars, MonomType toVars) {
00296 
00297   return apply_mapping(poly, generate_mapping(fromVars, toVars, PolyType(poly.ring())) );
00298 }
00299 
00300 
00301 
00302 END_NAMESPACE_PBORI
00303 
00304 #endif // pbori_algorithms_h_