00001
00002
00018
00019
00020 #ifndef polybori_routines_pbori_algorithms_h_
00021 #define polybori_routines_pbori_algorithms_h_
00022
00023
00024 #include <numeric>
00025
00026
00027 #include <polybori/pbori_defs.h>
00028
00029
00030 #include "pbori_algo.h"
00031
00032
00033 #include <polybori/BoolePolynomial.h>
00034 #include <polybori/BooleMonomial.h>
00035 #include <polybori/iterators/CGenericIter.h>
00036
00037
00038 BEGIN_NAMESPACE_PBORI
00039
00041 inline BoolePolynomial
00042 spoly(const BoolePolynomial& first, const BoolePolynomial& second){
00043
00044 BooleMonomial lead1(first.lead()), lead2(second.lead());
00045
00046 BooleMonomial prod = lead1;
00047 prod *= lead2;
00048
00049 return ( first * (prod / lead1) ) + ( second * (prod / lead2) );
00050 }
00051
00052 template <class NaviType, class LowerIterator, class ValueType>
00053 ValueType
00054 lower_term_accumulate(NaviType navi,
00055 LowerIterator lstart, LowerIterator lfinish,
00056 ValueType init) {
00057 PBORI_ASSERT(init.isZero());
00059 if (lstart == lfinish){
00060 return init;
00061 }
00062
00063 if (navi.isConstant())
00064 return (navi.terminalValue()? (ValueType)init.ring().one(): init);
00065
00066 PBORI_ASSERT(*lstart >= *navi);
00067
00068 ValueType result(init.ring());
00069 if (*lstart > *navi) {
00070
00071 ValueType reselse =
00072 lower_term_accumulate(navi.elseBranch(), lstart, lfinish, init);
00073
00074
00075
00076
00077
00078
00079
00080
00081 result = BooleSet(*navi, navi.thenBranch(), reselse.navigation(),
00082 init.ring());
00083 }
00084 else {
00085 PBORI_ASSERT(*lstart == *navi);
00086 ++lstart;
00087 BooleSet resthen =
00088 lower_term_accumulate(navi.thenBranch(), lstart, lfinish, init).diagram();
00089
00090 result = resthen.change(*navi);
00091 }
00092
00093 return result;
00094 }
00095
00096
00097 template <class UpperIterator, class NaviType, class ValueType>
00098 ValueType
00099 upper_term_accumulate(UpperIterator ustart, UpperIterator ufinish,
00100 NaviType navi, ValueType init) {
00101
00102
00103
00104
00105
00106
00107
00108 if (ustart == ufinish)
00109 return init.ring().one();
00110
00111 while (*navi < *ustart)
00112 navi.incrementElse();
00113 ++ustart;
00114 NaviType navithen = navi.thenBranch();
00115 ValueType resthen = upper_term_accumulate(ustart, ufinish, navithen, init);
00116
00117
00118 if (navithen == resthen.navigation())
00119 return BooleSet(navi, init.ring());
00120
00121 return BooleSet(*navi, resthen.navigation(), navi.elseBranch(), init.ring());
00122 }
00123
00124
00125 template <class UpperIterator, class NaviType, class LowerIterator,
00126 class ValueType>
00127 ValueType
00128 term_accumulate(UpperIterator ustart, UpperIterator ufinish, NaviType navi,
00129 LowerIterator lstart, LowerIterator lfinish, ValueType init) {
00130
00131
00132 if (lstart == lfinish)
00133 return upper_term_accumulate(ustart, ufinish, navi, init);
00134
00135 if (ustart == ufinish)
00136 return init.ring().one();
00137
00138 while (*navi < *ustart)
00139 navi.incrementElse();
00140 ++ustart;
00141
00142
00143 if (navi.isConstant())
00144 return BooleSet(navi, init.ring());
00145
00146 PBORI_ASSERT(*lstart >= *navi);
00147
00148 ValueType result(init.ring());
00149 if (*lstart > *navi) {
00150 ValueType resthen =
00151 upper_term_accumulate(ustart, ufinish, navi.thenBranch(), init);
00152 ValueType reselse =
00153 lower_term_accumulate(navi.elseBranch(), lstart, lfinish, init);
00154
00155 result = BooleSet(*navi, resthen.navigation(), reselse.navigation(),
00156 init.ring());
00157 }
00158 else {
00159 PBORI_ASSERT(*lstart == *navi);
00160 ++lstart;
00161 BooleSet resthen = term_accumulate(ustart, ufinish, navi.thenBranch(),
00162 lstart, lfinish, init).diagram();
00163
00164 result = resthen.change(*navi);
00165 }
00166
00167 return result;
00168 }
00169
00170
00171
00172
00174 template <class InputIterator, class ValueType>
00175 ValueType
00176 term_accumulate(InputIterator first, InputIterator last, ValueType init) {
00177
00178 #ifdef PBORI_ALT_TERM_ACCUMULATE
00179 if(last.isOne())
00180 return upper_term_accumulate(first.begin(), first.end(),
00181 first.navigation(), init) + ValueType(1);
00182
00183 ValueType result = term_accumulate(first.begin(), first.end(),
00184 first.navigation(),
00185 last.begin(), last.end(), init);
00186
00187
00188
00189
00190
00191
00192
00193
00194
00195
00196
00197
00198
00199 PBORI_ASSERT((init.ring().ordering().isLexicographical()?
00200 result == std::accumulate(first, last, init):
00201 true) );
00202
00203
00204 return result;
00205
00206 #else
00207
00210 if(first.isZero())
00211 return typename ValueType::dd_type(init.ring(),
00212 first.navigation());
00213
00214 ValueType result = upper_term_accumulate(first.begin(), first.end(),
00215 first.navigation(), init);
00216 if(!last.isZero())
00217 result += upper_term_accumulate(last.begin(), last.end(),
00218 last.navigation(), init);
00219
00220
00221 PBORI_ASSERT((init.ring().ordering().isLexicographical()?
00222 result == std::accumulate(first, last, init):
00223 true) );
00224
00225 return result;
00226 #endif
00227 }
00228
00229
00230
00231 template <class CacheType, class NaviType, class SetType>
00232 SetType
00233 dd_mapping(const CacheType& cache, NaviType navi, NaviType map, SetType init) {
00234
00235 if (navi.isConstant())
00236 return cache.generate(navi);
00237
00238 while (*map < *navi) {
00239 PBORI_ASSERT(!map.isConstant());
00240 map.incrementThen();
00241 }
00242
00243 PBORI_ASSERT(*navi == *map);
00244
00245 NaviType cached = cache.find(navi, map);
00246
00247
00248 if (cached.isValid())
00249 return SetType(cached, cache.ring());
00250
00251 SetType result =
00252 SetType(*(map.elseBranch()),
00253 dd_mapping(cache, navi.thenBranch(), map.thenBranch(), init),
00254 dd_mapping(cache, navi.elseBranch(), map.thenBranch(), init)
00255 );
00256
00257
00258
00259 cache.insert(navi, map, result.navigation());
00260
00261 return result;
00262 }
00263
00264
00265 template <class PolyType, class MapType>
00266 PolyType
00267 apply_mapping(const PolyType& poly, const MapType& map) {
00268
00269 CCacheManagement<typename PolyType::ring_type, typename CCacheTypes::mapping>
00270 cache(poly.ring());
00271
00272 return dd_mapping(cache, poly.navigation(), map.navigation(),
00273 typename PolyType::set_type(poly.ring()));
00274 }
00275
00276
00277 template <class MonomType, class PolyType>
00278 PolyType
00279 generate_mapping(MonomType& fromVars, MonomType& toVars, PolyType init) {
00280
00281 if(fromVars.isConstant()) {
00282 PBORI_ASSERT(fromVars.isOne() && toVars.isOne());
00283 return fromVars;
00284 }
00285
00286 MonomType varFrom = fromVars.firstVariable();
00287 MonomType varTo = toVars.firstVariable();
00288 fromVars.popFirst();
00289 toVars.popFirst();
00290 return (varFrom * generate_mapping(fromVars, toVars, init)) + varTo;
00291 }
00292
00293 template <class PolyType, class MonomType>
00294 PolyType
00295 mapping(PolyType poly, MonomType fromVars, MonomType toVars) {
00296
00297 return apply_mapping(poly, generate_mapping(fromVars, toVars, PolyType(poly.ring())) );
00298 }
00299
00300
00301
00302 END_NAMESPACE_PBORI
00303
00304 #endif // pbori_algorithms_h_