20 #ifndef polybori_routines_pbori_algorithms_h_
21 #define polybori_routines_pbori_algorithms_h_
41 inline BoolePolynomial
49 return ( first * (prod / lead1) ) + ( second * (prod / lead2) );
52 template <
class NaviType,
class LowerIterator,
class ValueType>
55 LowerIterator lstart, LowerIterator lfinish,
59 if (lstart == lfinish){
63 if (navi.isConstant())
64 return (navi.terminalValue()? (ValueType)init.ring().one(): init);
68 ValueType result(init.ring());
69 if (*lstart > *navi) {
81 result =
BooleSet(*navi, navi.thenBranch(), reselse.navigation(),
90 result = resthen.
change(*navi);
97 template <
class UpperIterator,
class NaviType,
class ValueType>
100 NaviType navi, ValueType init) {
108 if (ustart == ufinish)
109 return init.ring().one();
111 while (*navi < *ustart)
112 navi.incrementElse();
114 NaviType navithen = navi.thenBranch();
118 if (navithen == resthen.navigation())
121 return BooleSet(*navi, resthen.navigation(), navi.elseBranch(), init.ring());
125 template <
class UpperIterator,
class NaviType,
class LowerIterator,
129 LowerIterator lstart, LowerIterator lfinish, ValueType init) {
132 if (lstart == lfinish)
135 if (ustart == ufinish)
136 return init.ring().one();
138 while (*navi < *ustart)
139 navi.incrementElse();
143 if (navi.isConstant())
148 ValueType result(init.ring());
149 if (*lstart > *navi) {
155 result =
BooleSet(*navi, resthen.navigation(), reselse.navigation(),
162 lstart, lfinish, init).diagram();
164 result = resthen.
change(*navi);
174 template <
class InputIterator,
class ValueType>
178 #ifdef PBORI_ALT_TERM_ACCUMULATE
181 first.navigation(), init) + ValueType(1);
185 last.begin(), last.end(), init);
199 PBORI_ASSERT((init.ring().ordering().isLexicographical()?
200 result == std::accumulate(first, last, init):
211 return typename ValueType::dd_type(init.ring(),
215 first.navigation(), init);
218 last.navigation(), init);
221 PBORI_ASSERT((init.ring().ordering().isLexicographical()?
222 result == std::accumulate(first, last, init):
231 template <
class CacheType,
class NaviType,
class SetType>
233 dd_mapping(
const CacheType& cache, NaviType navi, NaviType map, SetType init) {
235 if (navi.isConstant())
236 return cache.generate(navi);
238 while (*map < *navi) {
245 NaviType cached = cache.find(navi, map);
248 if (cached.isValid())
249 return SetType(cached, cache.ring());
252 SetType(*(map.elseBranch()),
253 dd_mapping(cache, navi.thenBranch(), map.thenBranch(), init),
254 dd_mapping(cache, navi.elseBranch(), map.thenBranch(), init)
259 cache.insert(navi, map, result.navigation());
265 template <
class PolyType,
class MapType>
272 return dd_mapping(cache, poly.navigation(), map.navigation(),
273 typename PolyType::set_type(poly.ring()));
277 template <
class MonomType,
class PolyType>
281 if(fromVars.isConstant()) {
286 MonomType varFrom = fromVars.firstVariable();
287 MonomType varTo = toVars.firstVariable();
293 template <
class PolyType,
class MonomType>
295 mapping(PolyType poly, MonomType fromVars, MonomType toVars) {
304 #endif // pbori_algorithms_h_