PolyBoRi
|
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_