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