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_
#define END_NAMESPACE_PBORI
Finish project's namespace.
Definition: pbori_defs.h:77
ValueType upper_term_accumulate(UpperIterator ustart, UpperIterator ufinish, NaviType navi, ValueType init)
Definition: pbori_algorithms.h:99
monom_type lead() const
Get leading term.
Definition: BoolePolynomial.cc:225
#define BEGIN_NAMESPACE_PBORI
Start project's namespace.
Definition: pbori_defs.h:74
BoolePolynomial spoly(const BoolePolynomial &first, const BoolePolynomial &second)
Compute spoly of two polynomials.
Definition: pbori_algorithms.h:42
This template class forms the base for CCommutativeCacheManagement and CacheManager. It is an interface defining find and insert on decision diagram cache.
Definition: CCacheManagement.h:455
PolyType apply_mapping(const PolyType &poly, const MapType &map)
Definition: pbori_algorithms.h:267
PolyType generate_mapping(MonomType &fromVars, MonomType &toVars, PolyType init)
Definition: pbori_algorithms.h:279
PolyType mapping(PolyType poly, MonomType fromVars, MonomType toVars)
Definition: pbori_algorithms.h:295
This class wraps the underlying decicion diagram type and defines the necessary operations.
Definition: BoolePolynomial.h:85
ValueType lower_term_accumulate(NaviType navi, LowerIterator lstart, LowerIterator lfinish, ValueType init)
Definition: pbori_algorithms.h:54
#define PBORI_ASSERT(arg)
Definition: pbori_defs.h:118
ValueType term_accumulate(InputIterator first, InputIterator last, ValueType init)
Routine for adding all terms given by iterators.
Definition: pbori_algorithms.h:176
self change(idx_type idx) const
Definition: BooleSet.h:169
Definition: BooleSet.h:57
This class is just a wrapper for using variables from cudd's decicion diagram.
Definition: BooleMonomial.h:50
SetType dd_mapping(const CacheType &cache, NaviType navi, NaviType map, SetType init)
Definition: pbori_algorithms.h:233