103 #ifndef pbori_algorithms_h_
104 #define pbori_algorithms_h_
125 inline BoolePolynomial
133 return ( first * (prod / lead1) ) + ( second * (prod / lead2) );
136 template <
class NaviType,
class LowerIterator,
class ValueType>
139 LowerIterator lstart, LowerIterator lfinish,
141 assert(init.isZero());
143 if (lstart == lfinish){
147 if (navi.isConstant())
148 return (navi.terminalValue()? (ValueType)init.ring().one(): init);
150 assert(*lstart >= *navi);
153 if (*lstart > *navi) {
165 result =
BooleSet(*navi, navi.thenBranch(), reselse.navigation(),
169 assert(*lstart == *navi);
174 result = resthen.
change(*navi);
181 template <
class UpperIterator,
class NaviType,
class ValueType>
184 NaviType navi, ValueType init) {
192 if (ustart == ufinish)
193 return init.ring().one();
195 while (*navi < *ustart)
196 navi.incrementElse();
198 NaviType navithen = navi.thenBranch();
202 if (navithen == resthen.navigation())
205 return BooleSet(*navi, resthen.navigation(), navi.elseBranch(), init.ring());
209 template <
class UpperIterator,
class NaviType,
class LowerIterator,
213 LowerIterator lstart, LowerIterator lfinish, ValueType init) {
216 if (lstart == lfinish)
219 if (ustart == ufinish)
220 return init.ring().one();
222 while (*navi < *ustart)
223 navi.incrementElse();
227 if (navi.isConstant())
230 assert(*lstart >= *navi);
233 if (*lstart > *navi) {
239 result =
BooleSet(*navi, resthen.navigation(), reselse.navigation(),
243 assert(*lstart == *navi);
246 lstart, lfinish, init).diagram();
248 result = resthen.
change(*navi);
259 template <
class InputIterator,
class ValueType>
263 #ifdef PBORI_ALT_TERM_ACCUMULATE
266 first.navigation(), init) + ValueType(1);
270 last.begin(), last.end(), init);
283 assert(result == std::accumulate(first, last, init) );
292 return typename ValueType::dd_type(init.diagram().manager(),
296 first.navigation(), init);
299 last.navigation(), init);
301 assert(result == std::accumulate(first, last, init) );
309 template <
class CacheType,
class NaviType,
class SetType>
311 dd_mapping(
const CacheType& cache, NaviType navi, NaviType map, SetType init) {
313 if (navi.isConstant())
314 return cache.generate(navi);
316 while (*map < *navi) {
317 assert(!map.isConstant());
321 assert(*navi == *map);
323 NaviType cached = cache.find(navi, map);
326 if (cached.isValid())
327 return SetType(cached, cache.ring());
330 SetType(*(map.elseBranch()),
331 dd_mapping(cache, navi.thenBranch(), map.thenBranch(), init),
332 dd_mapping(cache, navi.elseBranch(), map.thenBranch(), init)
337 cache.insert(navi, map, result.navigation());
343 template <
class PolyType,
class MapType>
348 cache(poly.diagram().manager());
350 return dd_mapping(cache, poly.navigation(), map.navigation(),
351 typename PolyType::set_type());
355 template <
class MonomType,
class PolyType>
359 if(fromVars.isConstant()) {
360 assert(fromVars.isOne() && toVars.isOne());
364 MonomType varFrom = fromVars.firstVariable();
365 MonomType varTo = toVars.firstVariable();
371 template <
class PolyType,
class MonomType>
373 mapping(PolyType poly, MonomType fromVars, MonomType toVars) {
382 #endif // pbori_algorithms_h_