00001
00002
00101
00102
00103 #ifndef pbori_algorithms_h_
00104 #define pbori_algorithms_h_
00105
00106
00107 #include <numeric>
00108
00109
00110 #include "pbori_defs.h"
00111
00112
00113 #include "pbori_algo.h"
00114
00115
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
00159
00160
00161
00162
00163
00164
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
00187
00188
00189
00190
00191
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
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
00274
00275
00276
00277
00278
00279
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
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
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
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_