PolyBoRi
pbori_algorithms.h
Go to the documentation of this file.
1 // -*- c++ -*-
2 //*****************************************************************************
18 //*****************************************************************************
19 
20 #ifndef polybori_routines_pbori_algorithms_h_
21 #define polybori_routines_pbori_algorithms_h_
22 
23 // include standard headers
24 #include <numeric>
25 
26 // include basic definitions
27 #include <polybori/pbori_defs.h>
28 
29 // include PolyBoRi algorithm, which do not depend on PolyBoRi classes
30 #include "pbori_algo.h"
31 
32 // include PolyBoRi class definitions, which are used here
34 #include <polybori/BooleMonomial.h>
36 
37 
39 
41 inline BoolePolynomial
42 spoly(const BoolePolynomial& first, const BoolePolynomial& second){
43 
44  BooleMonomial lead1(first.lead()), lead2(second.lead());
45 
46  BooleMonomial prod = lead1;
47  prod *= lead2;
48 
49  return ( first * (prod / lead1) ) + ( second * (prod / lead2) );
50 }
51 
52 template <class NaviType, class LowerIterator, class ValueType>
53 ValueType
54 lower_term_accumulate(NaviType navi,
55  LowerIterator lstart, LowerIterator lfinish,
56  ValueType init) {
57  PBORI_ASSERT(init.isZero());
59  if (lstart == lfinish){
60  return init;
61  }
62 
63  if (navi.isConstant())
64  return (navi.terminalValue()? (ValueType)init.ring().one(): init);
65 
66  PBORI_ASSERT(*lstart >= *navi);
67 
68  ValueType result(init.ring());
69  if (*lstart > *navi) {
70 
71  ValueType reselse =
72  lower_term_accumulate(navi.elseBranch(), lstart, lfinish, init);
73 
74 // if(reselse.isZero())
75 // return BooleSet(navi.thenBranch()).change(*navi);
76 
77  // Note: result == BooleSet(navi) holds only in trivial cases, so testing
78  // reselse.navigation() == navi.elseBranch() is almost always false
79  // Hence, checking reselse.navigation() == navi.elseBranch() for returning
80  // navi, instead of result yields too much overhead.
81  result = BooleSet(*navi, navi.thenBranch(), reselse.navigation(),
82  init.ring());
83  }
84  else {
85  PBORI_ASSERT(*lstart == *navi);
86  ++lstart;
87  BooleSet resthen =
88  lower_term_accumulate(navi.thenBranch(), lstart, lfinish, init).diagram();
89 
90  result = resthen.change(*navi);
91  }
92 
93  return result;
94 }
95 
96 
97 template <class UpperIterator, class NaviType, class ValueType>
98 ValueType
99 upper_term_accumulate(UpperIterator ustart, UpperIterator ufinish,
100  NaviType navi, ValueType init) {
101 
102  // Note: Recursive caching, wrt. a navigator representing the term
103  // corresponding to ustart .. ufinish cannot be efficient here, because
104  // dereferencing the term is as expensive as this procedure in whole. (Maybe
105  // the generation of the BooleSet in the final line could be cached somehow.)
106 
107  // assuming (ustart .. ufinish) never means zero
108  if (ustart == ufinish)
109  return init.ring().one();
110 
111  while (*navi < *ustart)
112  navi.incrementElse();
113  ++ustart;
114  NaviType navithen = navi.thenBranch();
115  ValueType resthen = upper_term_accumulate(ustart, ufinish, navithen, init);
116 
117  // The following condition holds quite often, so computation time may be saved
118  if (navithen == resthen.navigation())
119  return BooleSet(navi, init.ring());
120 
121  return BooleSet(*navi, resthen.navigation(), navi.elseBranch(), init.ring());
122 }
123 
124 // assuming lstart .. lfinish *not* marking the term one
125 template <class UpperIterator, class NaviType, class LowerIterator,
126  class ValueType>
127 ValueType
128 term_accumulate(UpperIterator ustart, UpperIterator ufinish, NaviType navi,
129  LowerIterator lstart, LowerIterator lfinish, ValueType init) {
130 
131 
132  if (lstart == lfinish)
133  return upper_term_accumulate(ustart, ufinish, navi, init);
134 
135  if (ustart == ufinish)
136  return init.ring().one();
137 
138  while (*navi < *ustart)
139  navi.incrementElse();
140  ++ustart;
141 
142 
143  if (navi.isConstant())
144  return BooleSet(navi, init.ring());
145 
146  PBORI_ASSERT(*lstart >= *navi);
147 
148  ValueType result(init.ring());
149  if (*lstart > *navi) {
150  ValueType resthen =
151  upper_term_accumulate(ustart, ufinish, navi.thenBranch(), init);
152  ValueType reselse =
153  lower_term_accumulate(navi.elseBranch(), lstart, lfinish, init);
154 
155  result = BooleSet(*navi, resthen.navigation(), reselse.navigation(),
156  init.ring());
157  }
158  else {
159  PBORI_ASSERT(*lstart == *navi);
160  ++lstart;
161  BooleSet resthen = term_accumulate(ustart, ufinish, navi.thenBranch(),
162  lstart, lfinish, init).diagram();
163 
164  result = resthen.change(*navi);
165  }
166 
167  return result;
168 }
169 
170 
171 
172 
174 template <class InputIterator, class ValueType>
175 ValueType
176 term_accumulate(InputIterator first, InputIterator last, ValueType init) {
177 
178 #ifdef PBORI_ALT_TERM_ACCUMULATE
179  if(last.isOne())
180  return upper_term_accumulate(first.begin(), first.end(),
181  first.navigation(), init) + ValueType(1);
182 
183  ValueType result = term_accumulate(first.begin(), first.end(),
184  first.navigation(),
185  last.begin(), last.end(), init);
186 
187 
188  // alternative
189  /* ValueType result = upper_term_accumulate(first.begin(), first.end(),
190  first.navigation(), init);
191 
192 
193  result = lower_term_accumulate(result.navigation(),
194  last.begin(), last.end(), init);
195 
196  */
197 
198  // test for non-lex more complicated (see testsuite)
199  PBORI_ASSERT((init.ring().ordering().isLexicographical()?
200  result == std::accumulate(first, last, init):
201  true) );
202 
203 
204  return result;
205 
206 #else
207 
210  if(first.isZero())
211  return typename ValueType::dd_type(init.ring(),
212  first.navigation());
213 
214  ValueType result = upper_term_accumulate(first.begin(), first.end(),
215  first.navigation(), init);
216  if(!last.isZero())
217  result += upper_term_accumulate(last.begin(), last.end(),
218  last.navigation(), init);
219 
220  // test for non-lex more complicated (see testsuite)
221  PBORI_ASSERT((init.ring().ordering().isLexicographical()?
222  result == std::accumulate(first, last, init):
223  true) );
224 
225  return result;
226 #endif
227 }
228 
229 
230 // determine the part of a polynomials of a given degree
231 template <class CacheType, class NaviType, class SetType>
232 SetType
233 dd_mapping(const CacheType& cache, NaviType navi, NaviType map, SetType init) {
234 
235  if (navi.isConstant())
236  return cache.generate(navi);
237 
238  while (*map < *navi) {
239  PBORI_ASSERT(!map.isConstant());
240  map.incrementThen();
241  }
242 
243  PBORI_ASSERT(*navi == *map);
244 
245  NaviType cached = cache.find(navi, map);
246 
247  // look whether computation was done before
248  if (cached.isValid())
249  return SetType(cached, cache.ring());
250 
251  SetType result =
252  SetType(*(map.elseBranch()),
253  dd_mapping(cache, navi.thenBranch(), map.thenBranch(), init),
254  dd_mapping(cache, navi.elseBranch(), map.thenBranch(), init)
255  );
256 
257 
258  // store result for later reuse
259  cache.insert(navi, map, result.navigation());
260 
261  return result;
262 }
263 
264 
265 template <class PolyType, class MapType>
266 PolyType
267 apply_mapping(const PolyType& poly, const MapType& map) {
268 
270  cache(poly.ring());
271 
272  return dd_mapping(cache, poly.navigation(), map.navigation(),
273  typename PolyType::set_type(poly.ring()));
274 }
275 
276 
277 template <class MonomType, class PolyType>
278 PolyType
279 generate_mapping(MonomType& fromVars, MonomType& toVars, PolyType init) {
280 
281  if(fromVars.isConstant()) {
282  PBORI_ASSERT(fromVars.isOne() && toVars.isOne());
283  return fromVars;
284  }
285 
286  MonomType varFrom = fromVars.firstVariable();
287  MonomType varTo = toVars.firstVariable();
288  fromVars.popFirst();
289  toVars.popFirst();
290  return (varFrom * generate_mapping(fromVars, toVars, init)) + varTo;
291 }
292 
293 template <class PolyType, class MonomType>
294 PolyType
295 mapping(PolyType poly, MonomType fromVars, MonomType toVars) {
296 
297  return apply_mapping(poly, generate_mapping(fromVars, toVars, PolyType(poly.ring())) );
298 }
299 
300 
301 
303 
304 #endif // pbori_algorithms_h_