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