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
00124 inline BoolePolynomial
00125 spoly(const BoolePolynomial& first, const BoolePolynomial& second){
00126
00127 BooleMonomial lead1(first.lead()), lead2(second.lead());
00128
00129 BooleMonomial prod = lead1;
00130 prod *= lead2;
00131
00132 return ( first * (prod / lead1) ) + ( second * (prod / lead2) );
00133 }
00134
00135 template <class NaviType, class LowerIterator, class ValueType>
00136 ValueType
00137 lower_term_accumulate(NaviType navi,
00138 LowerIterator lstart, LowerIterator lfinish,
00139 ValueType init) {
00140 assert(init.isZero());
00142 if (lstart == lfinish){
00143 return init;
00144 }
00145
00146 if (navi.isConstant())
00147 return (navi.terminalValue()? (ValueType)init.ring().one(): init);
00148
00149 assert(*lstart >= *navi);
00150
00151 ValueType result;
00152 if (*lstart > *navi) {
00153
00154 ValueType reselse =
00155 lower_term_accumulate(navi.elseBranch(), lstart, lfinish, init);
00156
00157
00158
00159
00160
00161
00162
00163
00164 result = BooleSet(*navi, navi.thenBranch(), reselse.navigation(),
00165 init.ring());
00166 }
00167 else {
00168 assert(*lstart == *navi);
00169 ++lstart;
00170 BooleSet resthen =
00171 lower_term_accumulate(navi.thenBranch(), lstart, lfinish, init).diagram();
00172
00173 result = resthen.change(*navi);
00174 }
00175
00176 return result;
00177 }
00178
00179
00180 template <class UpperIterator, class NaviType, class ValueType>
00181 ValueType
00182 upper_term_accumulate(UpperIterator ustart, UpperIterator ufinish,
00183 NaviType navi, ValueType init) {
00184
00185
00186
00187
00188
00189
00190
00191 if (ustart == ufinish)
00192 return init.ring().one();
00193
00194 while (*navi < *ustart)
00195 navi.incrementElse();
00196 ++ustart;
00197 NaviType navithen = navi.thenBranch();
00198 ValueType resthen = upper_term_accumulate(ustart, ufinish, navithen, init);
00199
00200
00201 if (navithen == resthen.navigation())
00202 return BooleSet(navi, init.ring());
00203
00204 return BooleSet(*navi, resthen.navigation(), navi.elseBranch(), init.ring());
00205 }
00206
00207
00208 template <class UpperIterator, class NaviType, class LowerIterator,
00209 class ValueType>
00210 ValueType
00211 term_accumulate(UpperIterator ustart, UpperIterator ufinish, NaviType navi,
00212 LowerIterator lstart, LowerIterator lfinish, ValueType init) {
00213
00214
00215 if (lstart == lfinish)
00216 return upper_term_accumulate(ustart, ufinish, navi, init);
00217
00218 if (ustart == ufinish)
00219 return init.ring().one();
00220
00221 while (*navi < *ustart)
00222 navi.incrementElse();
00223 ++ustart;
00224
00225
00226 if (navi.isConstant())
00227 return BooleSet(navi, init.ring());
00228
00229 assert(*lstart >= *navi);
00230
00231 ValueType result;
00232 if (*lstart > *navi) {
00233 ValueType resthen =
00234 upper_term_accumulate(ustart, ufinish, navi.thenBranch(), init);
00235 ValueType reselse =
00236 lower_term_accumulate(navi.elseBranch(), lstart, lfinish, init);
00237
00238 result = BooleSet(*navi, resthen.navigation(), reselse.navigation(),
00239 init.ring());
00240 }
00241 else {
00242 assert(*lstart == *navi);
00243 ++lstart;
00244 BooleSet resthen = term_accumulate(ustart, ufinish, navi.thenBranch(),
00245 lstart, lfinish, init).diagram();
00246
00247 result = resthen.change(*navi);
00248 }
00249
00250 return result;
00251 }
00252
00253
00254
00255
00257 template <class InputIterator, class ValueType>
00258 ValueType
00259 term_accumulate(InputIterator first, InputIterator last, ValueType init) {
00260
00261 #ifdef PBORI_ALT_TERM_ACCUMULATE
00262 if(last.isOne())
00263 return upper_term_accumulate(first.begin(), first.end(),
00264 first.navigation(), init) + ValueType(1);
00265
00266 ValueType result = term_accumulate(first.begin(), first.end(),
00267 first.navigation(),
00268 last.begin(), last.end(), init);
00269
00270
00271
00272
00273
00274
00275
00276
00277
00278
00279
00280
00281 assert(result == std::accumulate(first, last, init) );
00282
00283 return result;
00284
00285 #else
00286
00289 if(first.isZero())
00290 return typename ValueType::dd_type(init.diagram().manager(),
00291 first.navigation());
00292
00293 ValueType result = upper_term_accumulate(first.begin(), first.end(),
00294 first.navigation(), init);
00295 if(!last.isZero())
00296 result += upper_term_accumulate(last.begin(), last.end(),
00297 last.navigation(), init);
00298
00299 assert(result == std::accumulate(first, last, init) );
00300
00301 return result;
00302 #endif
00303 }
00304
00305
00306
00307 template <class CacheType, class NaviType, class SetType>
00308 SetType
00309 dd_mapping(const CacheType& cache, NaviType navi, NaviType map, SetType init) {
00310
00311 if (navi.isConstant())
00312 return cache.generate(navi);
00313
00314 while (*map < *navi) {
00315 assert(!map.isConstant());
00316 map.incrementThen();
00317 }
00318
00319 assert(*navi == *map);
00320
00321 NaviType cached = cache.find(navi, map);
00322
00323
00324 if (cached.isValid())
00325 return SetType(cached, cache.ring());
00326
00327 SetType result =
00328 SetType(*(map.elseBranch()),
00329 dd_mapping(cache, navi.thenBranch(), map.thenBranch(), init),
00330 dd_mapping(cache, navi.elseBranch(), map.thenBranch(), init)
00331 );
00332
00333
00334
00335 cache.insert(navi, map, result.navigation());
00336
00337 return result;
00338 }
00339
00340
00341 template <class PolyType, class MapType>
00342 PolyType
00343 apply_mapping(const PolyType& poly, const MapType& map) {
00344
00345 CCacheManagement<typename CCacheTypes::mapping>
00346 cache(poly.diagram().manager());
00347
00348 return dd_mapping(cache, poly.navigation(), map.navigation(),
00349 typename PolyType::set_type());
00350 }
00351
00352
00353 template <class MonomType, class PolyType>
00354 PolyType
00355 generate_mapping(MonomType& fromVars, MonomType& toVars, PolyType init) {
00356
00357 if(fromVars.isConstant()) {
00358 assert(fromVars.isOne() && toVars.isOne());
00359 return fromVars;
00360 }
00361
00362 MonomType varFrom = fromVars.firstVariable();
00363 MonomType varTo = toVars.firstVariable();
00364 fromVars.popFirst();
00365 toVars.popFirst();
00366 return (varFrom * generate_mapping(fromVars, toVars, init)) + varTo;
00367 }
00368
00369 template <class PolyType, class MonomType>
00370 PolyType
00371 mapping(PolyType poly, MonomType fromVars, MonomType toVars) {
00372
00373 return apply_mapping(poly, generate_mapping(fromVars, toVars, PolyType()) );
00374 }
00375
00376
00377
00378 END_NAMESPACE_PBORI
00379
00380 #endif // pbori_algorithms_h_