00001
00002
00104
00105
00106 #ifndef pbori_algorithms_h_
00107 #define pbori_algorithms_h_
00108
00109
00110 #include <numeric>
00111
00112
00113 #include "pbori_defs.h"
00114
00115
00116 #include "pbori_algo.h"
00117
00118
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
00161
00162
00163
00164
00165
00166
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
00189
00190
00191
00192
00193
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
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
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
00275
00276
00277
00278
00279
00280
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
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
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
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_