PolyBoRi
pbori_algorithms.h
Go to the documentation of this file.
1 // -*- c++ -*-
2 //*****************************************************************************
101 //*****************************************************************************
102 
103 #ifndef pbori_algorithms_h_
104 #define pbori_algorithms_h_
105 
106 // include standard headers
107 #include <numeric>
108 
109 // include basic definitions
110 #include "pbori_defs.h"
111 
112 // include PolyBoRi algorithm, which do not depend on PolyBoRi classes
113 #include "pbori_algo.h"
114 
115 // include PolyBoRi class definitions, which are used here
116 #include "BoolePolynomial.h"
117 #include "BooleMonomial.h"
118 #include "CGenericIter.h"
119 
120 
122 
125 inline BoolePolynomial
126 spoly(const BoolePolynomial& first, const BoolePolynomial& second){
127 
128  BooleMonomial lead1(first.lead()), lead2(second.lead());
129 
130  BooleMonomial prod = lead1;
131  prod *= lead2;
132 
133  return ( first * (prod / lead1) ) + ( second * (prod / lead2) );
134 }
135 
136 template <class NaviType, class LowerIterator, class ValueType>
137 ValueType
138 lower_term_accumulate(NaviType navi,
139  LowerIterator lstart, LowerIterator lfinish,
140  ValueType init) {
141  assert(init.isZero());
143  if (lstart == lfinish){
144  return init;
145  }
146 
147  if (navi.isConstant())
148  return (navi.terminalValue()? (ValueType)init.ring().one(): init);
149 
150  assert(*lstart >= *navi);
151 
152  ValueType result;
153  if (*lstart > *navi) {
154 
155  ValueType reselse =
156  lower_term_accumulate(navi.elseBranch(), lstart, lfinish, init);
157 
158 // if(reselse.isZero())
159 // return BooleSet(navi.thenBranch()).change(*navi);
160 
161  // Note: result == BooleSet(navi) holds only in trivial cases, so testing
162  // reselse.navigation() == navi.elseBranch() is almost always false
163  // Hence, checking reselse.navigation() == navi.elseBranch() for returning
164  // navi, instead of result yields too much overhead.
165  result = BooleSet(*navi, navi.thenBranch(), reselse.navigation(),
166  init.ring());
167  }
168  else {
169  assert(*lstart == *navi);
170  ++lstart;
171  BooleSet resthen =
172  lower_term_accumulate(navi.thenBranch(), lstart, lfinish, init).diagram();
173 
174  result = resthen.change(*navi);
175  }
176 
177  return result;
178 }
179 
180 
181 template <class UpperIterator, class NaviType, class ValueType>
182 ValueType
183 upper_term_accumulate(UpperIterator ustart, UpperIterator ufinish,
184  NaviType navi, ValueType init) {
185 
186  // Note: Recursive caching, wrt. a navigator representing the term
187  // corresponding to ustart .. ufinish cannot be efficient here, because
188  // dereferencing the term is as expensive as this procedure in whole. (Maybe
189  // the generation of the BooleSet in the final line could be cached somehow.)
190 
191  // assuming (ustart .. ufinish) never means zero
192  if (ustart == ufinish)
193  return init.ring().one();
194 
195  while (*navi < *ustart)
196  navi.incrementElse();
197  ++ustart;
198  NaviType navithen = navi.thenBranch();
199  ValueType resthen = upper_term_accumulate(ustart, ufinish, navithen, init);
200 
201  // The following condition holds quite often, so computation time may be saved
202  if (navithen == resthen.navigation())
203  return BooleSet(navi, init.ring());
204 
205  return BooleSet(*navi, resthen.navigation(), navi.elseBranch(), init.ring());
206 }
207 
209 template <class UpperIterator, class NaviType, class LowerIterator,
210  class ValueType>
211 ValueType
212 term_accumulate(UpperIterator ustart, UpperIterator ufinish, NaviType navi,
213  LowerIterator lstart, LowerIterator lfinish, ValueType init) {
214 
215 
216  if (lstart == lfinish)
217  return upper_term_accumulate(ustart, ufinish, navi, init);
218 
219  if (ustart == ufinish)
220  return init.ring().one();
221 
222  while (*navi < *ustart)
223  navi.incrementElse();
224  ++ustart;
225 
226 
227  if (navi.isConstant())
228  return BooleSet(navi, init.ring());
229 
230  assert(*lstart >= *navi);
231 
232  ValueType result;
233  if (*lstart > *navi) {
234  ValueType resthen =
235  upper_term_accumulate(ustart, ufinish, navi.thenBranch(), init);
236  ValueType reselse =
237  lower_term_accumulate(navi.elseBranch(), lstart, lfinish, init);
238 
239  result = BooleSet(*navi, resthen.navigation(), reselse.navigation(),
240  init.ring());
241  }
242  else {
243  assert(*lstart == *navi);
244  ++lstart;
245  BooleSet resthen = term_accumulate(ustart, ufinish, navi.thenBranch(),
246  lstart, lfinish, init).diagram();
247 
248  result = resthen.change(*navi);
249  }
250 
251  return result;
252 }
253 
254 
255 
256 
259 template <class InputIterator, class ValueType>
260 ValueType
261 term_accumulate(InputIterator first, InputIterator last, ValueType init) {
262 
263 #ifdef PBORI_ALT_TERM_ACCUMULATE
264  if(last.isOne())
265  return upper_term_accumulate(first.begin(), first.end(),
266  first.navigation(), init) + ValueType(1);
267 
268  ValueType result = term_accumulate(first.begin(), first.end(),
269  first.navigation(),
270  last.begin(), last.end(), init);
271 
272 
273  // alternative
274  /* ValueType result = upper_term_accumulate(first.begin(), first.end(),
275  first.navigation(), init);
276 
277 
278  result = lower_term_accumulate(result.navigation(),
279  last.begin(), last.end(), init);
280 
281  */
282 
283  assert(result == std::accumulate(first, last, init) );
284 
285  return result;
286 
287 #else
288 
291  if(first.isZero())
292  return typename ValueType::dd_type(init.diagram().manager(),
293  first.navigation());
294 
295  ValueType result = upper_term_accumulate(first.begin(), first.end(),
296  first.navigation(), init);
297  if(!last.isZero())
298  result += upper_term_accumulate(last.begin(), last.end(),
299  last.navigation(), init);
300 
301  assert(result == std::accumulate(first, last, init) );
302 
303  return result;
304 #endif
305 }
306 
307 
308 // determine the part of a polynomials of a given degree
309 template <class CacheType, class NaviType, class SetType>
310 SetType
311 dd_mapping(const CacheType& cache, NaviType navi, NaviType map, SetType init) {
312 
313  if (navi.isConstant())
314  return cache.generate(navi);
315 
316  while (*map < *navi) {
317  assert(!map.isConstant());
318  map.incrementThen();
319  }
320 
321  assert(*navi == *map);
322 
323  NaviType cached = cache.find(navi, map);
324 
325  // look whether computation was done before
326  if (cached.isValid())
327  return SetType(cached, cache.ring());
328 
329  SetType result =
330  SetType(*(map.elseBranch()),
331  dd_mapping(cache, navi.thenBranch(), map.thenBranch(), init),
332  dd_mapping(cache, navi.elseBranch(), map.thenBranch(), init)
333  );
334 
335 
336  // store result for later reuse
337  cache.insert(navi, map, result.navigation());
338 
339  return result;
340 }
341 
342 
343 template <class PolyType, class MapType>
344 PolyType
345 apply_mapping(const PolyType& poly, const MapType& map) {
346 
348  cache(poly.diagram().manager());
349 
350  return dd_mapping(cache, poly.navigation(), map.navigation(),
351  typename PolyType::set_type());
352 }
353 
354 
355 template <class MonomType, class PolyType>
356 PolyType
357 generate_mapping(MonomType& fromVars, MonomType& toVars, PolyType init) {
358 
359  if(fromVars.isConstant()) {
360  assert(fromVars.isOne() && toVars.isOne());
361  return fromVars;
362  }
363 
364  MonomType varFrom = fromVars.firstVariable();
365  MonomType varTo = toVars.firstVariable();
366  fromVars.popFirst();
367  toVars.popFirst();
368  return (varFrom * generate_mapping(fromVars, toVars, init)) + varTo;
369 }
370 
371 template <class PolyType, class MonomType>
372 PolyType
373 mapping(PolyType poly, MonomType fromVars, MonomType toVars) {
374 
375  return apply_mapping(poly, generate_mapping(fromVars, toVars, PolyType()) );
376 }
377 
378 
379 
381 
382 #endif // pbori_algorithms_h_