PolyBoRi
pbori_routines_misc.h
Go to the documentation of this file.
1 // -*- c++ -*-
2 //*****************************************************************************
13 //*****************************************************************************
14 
15 #ifndef polybori_routines_pbori_routines_misc_h_
16 #define polybori_routines_pbori_routines_misc_h_
17 
18 // include basic definitions
19 #include <polybori/pbori_defs.h>
20 
21 // temprarily
23 
25 
27 
28 template<class Iterator>
29 typename Iterator::value_type
30 index_vector_hash(Iterator start, Iterator finish){
31 
32  typedef typename Iterator::value_type value_type;
33 
34  value_type vars = 0;
35  value_type sum = 0;
36 
37  while (start != finish){
38  vars++;
39  sum += ((*start)+1) * ((*start)+1);
40  ++start;
41  }
42  return sum * vars;
43 }
44 
47 template <class DegreeCacher, class NaviType>
48 typename NaviType::deg_type
49 dd_cached_degree(const DegreeCacher& cache, NaviType navi) {
50 
51  typedef typename NaviType::deg_type deg_type;
52 
53  if (navi.isConstant()){ // No need for caching of constant nodes' degrees
54  if (navi.terminalValue())
55  return 0;
56  else
57  return -1;
58  }
59 
60  // Look whether result was cached before
61  typename DegreeCacher::node_type result = cache.find(navi);
62  if (result.isValid())
63  return (*result);
64 
65  // Get degree of then branch (contains at least one valid path)...
66  deg_type deg = dd_cached_degree(cache, navi.thenBranch()) + 1;
67 
68  // ... combine with degree of else branch
69  deg = std::max(deg, dd_cached_degree(cache, navi.elseBranch()) );
70 
71  // Write result to cache
72  cache.insert(navi, deg);
73 
74  return deg;
75 }
76 
81 template <class DegreeCacher, class NaviType, class SizeType>
82 typename NaviType::deg_type
83 dd_cached_degree(const DegreeCacher& cache, NaviType navi, SizeType bound) {
84 
85  typedef typename NaviType::deg_type deg_type;
86 
87  if (bound < 0) {
88  return -1;
89  }
90 
91  // No need for caching of constant nodes' degrees
92  if (bound == 0) {
93  while(!navi.isConstant())
94  navi.incrementElse();
95  }
96  if (navi.isConstant())
97  return (navi.terminalValue()? 0: -1);
98 
99  // Look whether result was cached before
100  typename DegreeCacher::node_type result = cache.find(navi, bound);
101  if (result.isValid())
102  return *result;
103 
104  // Get degree of then branch (contains at least one valid path)...
105  deg_type deg = dd_cached_degree(cache, navi.thenBranch(), bound - 1);
106  if (deg >= 0) ++deg;
107 
108  // ... combine with degree of else branch
109  if (bound > deg) // if deg <= bound, we are already finished
110  deg = std::max(deg, dd_cached_degree(cache, navi.elseBranch(), bound) );
111 
112  // Write result to cache
113  if (deg >= 0) {
114  PBORI_ASSERT(bound >= 0);
115  cache.insert(navi, bound, deg);
116  }
117 
118  return deg;
119 }
120 
121 template <class Iterator, class NameGenerator,
122  class Separator, class EmptySetType,
123  class OStreamType>
124 void
125 dd_print_term(Iterator start, Iterator finish, const NameGenerator& get_name,
126  const Separator& sep, const EmptySetType& emptyset,
127  OStreamType& os){
128 
129  if (start != finish){
130  os << get_name(*start);
131  ++start;
132  }
133  else
134  os << emptyset();
135 
136  while (start != finish){
137  os << sep() << get_name(*start);
138  ++start;
139  }
140 }
141 
142 template <class TermType, class NameGenerator,
143  class Separator, class EmptySetType,
144  class OStreamType>
145 void
146 dd_print_term(const TermType& term, const NameGenerator& get_name,
147  const Separator& sep, const EmptySetType& emptyset,
148  OStreamType& os){
149  dd_print_term(term.begin(), term.end(), get_name, sep, emptyset, os);
150 }
151 
152 
153 template <class Iterator, class NameGenerator,
154  class Separator, class InnerSeparator,
155  class EmptySetType, class OStreamType>
156 void
157 dd_print_terms(Iterator start, Iterator finish, const NameGenerator& get_name,
158  const Separator& sep, const InnerSeparator& innersep,
159  const EmptySetType& emptyset, OStreamType& os) {
160 
161  if (start != finish){
162  dd_print_term(*start, get_name, innersep, emptyset, os);
163  ++start;
164  }
165 
166  while (start != finish){
167  os << sep();
168  dd_print_term(*start, get_name, innersep, emptyset, os);
169  ++start;
170  }
171 
172 }
173 
174 
175 template <bool use_fast,
176  class CacheType, class NaviType, class PolyType>
177 PolyType
178 dd_multiply(const CacheType& cache_mgr,
179  NaviType firstNavi, NaviType secondNavi, PolyType init){
180 
181  // Extract subtypes
182  typedef typename PolyType::dd_type dd_type;
183  typedef typename NaviType::idx_type idx_type;
184  typedef NaviType navigator;
185 
186  if (firstNavi.isConstant()) {
187  if(firstNavi.terminalValue())
188  return cache_mgr.generate(secondNavi);
189  else
190  return cache_mgr.zero();
191  }
192 
193  if (secondNavi.isConstant()) {
194  if(secondNavi.terminalValue())
195  return cache_mgr.generate(firstNavi);
196  else
197  return cache_mgr.zero();
198  }
199  if (firstNavi == secondNavi)
200  return cache_mgr.generate(firstNavi);
201 
202  // Look up, whether operation was already used
203  navigator cached = cache_mgr.find(firstNavi, secondNavi);
204  PolyType result(cache_mgr.zero());
205 
206  if (cached.isValid()) { // Cache lookup sucessful
207  return cache_mgr.generate(cached);
208  }
209  else { // Cache lookup not sucessful
210  // Get top variable's index
211 
212  if (*secondNavi < *firstNavi)
213  std::swap(firstNavi, secondNavi);
214 
215  idx_type index = *firstNavi;
216 
217  // Get then- and else-branches wrt. current indexed variable
218  navigator as0 = firstNavi.elseBranch();
219  navigator as1 = firstNavi.thenBranch();
220 
221  navigator bs0;
222  navigator bs1;
223 
224  if (*secondNavi == index) {
225  bs0 = secondNavi.elseBranch();
226  bs1 = secondNavi.thenBranch();
227  }
228  else {
229  bs0 = secondNavi;
230  bs1 = cache_mgr.zero().navigation();
231  }
232  PolyType result0 = dd_multiply<use_fast>(cache_mgr, as0, bs0, init);
233  PolyType result1(cache_mgr.zero());
234 
235  // use fast multiplication
236  if (use_fast && (*firstNavi == *secondNavi)) {
237 
238  PolyType res10 = PolyType(cache_mgr.generate(as1)) +
239  PolyType(cache_mgr.generate(as0));
240  PolyType res01 = PolyType(cache_mgr.generate(bs0)) +
241  PolyType(cache_mgr.generate(bs1));
242 
243  result1 = dd_multiply<use_fast>(cache_mgr, res10.navigation(),
244  res01.navigation(), init) - result0;
245  }
246  // not using fast multiplication
247  else if (as0 == as1) {
248  result1 = dd_multiply<use_fast>(cache_mgr, bs0, as1, init);
249 
250  }
251  else {
252  result1 = dd_multiply<use_fast>(cache_mgr, as0, bs1, init);
253  if (bs0 != bs1){
254  PolyType bs01 = PolyType(cache_mgr.generate(bs0)) +
255  PolyType(cache_mgr.generate(bs1));
256 
257  result1 +=
258  dd_multiply<use_fast>(cache_mgr, bs01.navigation(), as1, init);
259  }
260  }
261  result = dd_type(index, result1.diagram(), result0.diagram());
262 
263  // Insert in cache
264  cache_mgr.insert(firstNavi, secondNavi, result.navigation());
265  } // end of Cache lookup not sucessful
266 
267  return result;
268 }
269 
270 template <class CacheType, class NaviType, class PolyType>
271 PolyType
272 dd_multiply_recursively(const CacheType& cache_mgr,
273  NaviType firstNavi, NaviType secondNavi, PolyType init){
274 
275  enum { use_fast =
276 #ifdef PBORI_FAST_MULTIPLICATION
277  true
278 #else
279  false
280 #endif
281  };
282 
283  return dd_multiply<use_fast>(cache_mgr, firstNavi, secondNavi, init);
284 }
285 
286 template <class CacheType, class NaviType, class PolyType>
287 PolyType
288 dd_multiply_recursively_monom(const CacheType& cache_mgr,
289  NaviType monomNavi, NaviType navi, PolyType init){
290 
291  // Extract subtypes
292  typedef typename PolyType::dd_type dd_type;
293  typedef typename NaviType::idx_type idx_type;
294  typedef NaviType navigator;
295 
296  if (monomNavi.isConstant()) {
297  if(monomNavi.terminalValue())
298  return cache_mgr.generate(navi);
299  else
300  return cache_mgr.zero();
301  }
302 
303  PBORI_ASSERT(monomNavi.elseBranch().isEmpty());
304 
305  if (navi.isConstant()) {
306  if(navi.terminalValue())
307  return cache_mgr.generate(monomNavi);
308  else
309  return cache_mgr.zero();
310  }
311  if (monomNavi == navi)
312  return cache_mgr.generate(monomNavi);
313 
314  // Look up, whether operation was already used
315  navigator cached = cache_mgr.find(monomNavi, navi);
316 
317  if (cached.isValid()) { // Cache lookup sucessful
318  return cache_mgr.generate(cached);
319  }
320 
321  // Cache lookup not sucessful
322  // Get top variables' index
323 
324  idx_type index = *navi;
325  idx_type monomIndex = *monomNavi;
326 
327  if (monomIndex < index) { // Case: index may occure within monom
328  init = dd_multiply_recursively_monom(cache_mgr, monomNavi.thenBranch(), navi,
329  init).diagram().change(monomIndex);
330  }
331  else if (monomIndex == index) { // Case: monom and poly start with same index
332 
333  // Increment navigators
334  navigator monomThen = monomNavi.thenBranch();
335  navigator naviThen = navi.thenBranch();
336  navigator naviElse = navi.elseBranch();
337 
338  if (naviThen != naviElse)
339  init = (dd_multiply_recursively_monom(cache_mgr, monomThen, naviThen, init)
340  + dd_multiply_recursively_monom(cache_mgr, monomThen, naviElse,
341  init)).diagram().change(index);
342  }
343  else { // Case: var(index) not part of monomial
344 
345  init =
346  dd_type(index,
347  dd_multiply_recursively_monom(cache_mgr, monomNavi, navi.thenBranch(),
348  init).diagram(),
349  dd_multiply_recursively_monom(cache_mgr, monomNavi, navi.elseBranch(),
350  init).diagram() );
351  }
352 
353  // Insert in cache
354  cache_mgr.insert(monomNavi, navi, init.navigation());
355 
356  return init;
357 }
358 
359 
360 template <class DDGenerator, class Iterator, class NaviType, class PolyType>
361 PolyType
362 dd_multiply_recursively_exp(const DDGenerator& ddgen,
363  Iterator start, Iterator finish,
364  NaviType navi, PolyType init){
365  // Extract subtypes
366  typedef typename NaviType::idx_type idx_type;
367  typedef typename PolyType::dd_type dd_type;
368  typedef NaviType navigator;
369 
370  if (start == finish)
371  return ddgen.generate(navi);
372 
373  PolyType result(ddgen.zero());
374  if (navi.isConstant()) {
375  if(navi.terminalValue()) {
376 
377  std::reverse_iterator<Iterator> rstart(finish), rfinish(start);
378  result = ddgen.generate(navi);
379  while (rstart != rfinish) {
380  result = result.diagram().change(*rstart);
381  ++rstart;
382  }
383  }
384  else
385  return ddgen.zero();
386 
387  return result;
388  }
389 
390  // Cache lookup not sucessful
391  // Get top variables' index
392 
393  idx_type index = *navi;
394  idx_type monomIndex = *start;
395 
396  if (monomIndex < index) { // Case: index may occure within monom
397 
398  Iterator next(start);
399  while( (next != finish) && (*next < index) )
400  ++next;
401 
402  result = dd_multiply_recursively_exp(ddgen, next, finish, navi, init);
403 
404  std::reverse_iterator<Iterator> rstart(next), rfinish(start);
405  while (rstart != rfinish) {
406  result = result.diagram().change(*rstart);
407  ++rstart;
408  }
409  }
410  else if (monomIndex == index) { // Case: monom and poly start with same index
411 
412  // Increment navigators
413  ++start;
414 
415  navigator naviThen = navi.thenBranch();
416  navigator naviElse = navi.elseBranch();
417 
418  if (naviThen != naviElse)
419  result =(dd_multiply_recursively_exp(ddgen, start, finish, naviThen, init)
420  + dd_multiply_recursively_exp(ddgen, start, finish, naviElse,
421  init)).diagram().change(index);
422  }
423  else { // Case: var(index) not part of monomial
424 
425  result =
426  dd_type(index,
427  dd_multiply_recursively_exp(ddgen, start, finish,
428  navi.thenBranch(), init).diagram(),
429  dd_multiply_recursively_exp(ddgen, start, finish,
430  navi.elseBranch(), init).diagram() );
431  }
432 
433  return result;
434 }
435 
436 template<class DegCacheMgr, class NaviType, class SizeType>
437 bool max_degree_on_then(const DegCacheMgr& deg_mgr, NaviType navi,
438  SizeType degree, valid_tag is_descending) {
439 
440  navi.incrementThen();
441  return ((dd_cached_degree(deg_mgr, navi, degree - 1) + 1) == degree);
442 }
443 
444 template<class DegCacheMgr, class NaviType, class SizeType>
445 bool max_degree_on_then(const DegCacheMgr& deg_mgr, NaviType navi,
446  SizeType degree, invalid_tag non_descending) {
447 
448  navi.incrementElse();
449  return (dd_cached_degree(deg_mgr, navi, degree) != degree);
450 }
451 
452 template <class NaviType>
453 NaviType dd_get_constant(NaviType navi) {
454  while(!navi.isConstant()) {
455  navi.incrementElse();
456  }
457 
458  return navi;
459 }
460 
461 template <class T> class CIndexCacheHandle;
462 // with degree bound
463 template <class CacheType, class DegCacheMgr, class NaviType,
464  class TermType, class SizeType, class DescendingProperty>
465 TermType
466 dd_recursive_degree_lead(const CacheType& cache_mgr, const DegCacheMgr&
467  deg_mgr,
468  NaviType navi, TermType init, SizeType degree,
469  DescendingProperty prop) {
470 
471 
472  typedef CIndexCacheHandle<NaviType> deg2node;
473 
474  if PBORI_UNLIKELY(degree < 0)
475  return cache_mgr.zero();
476 
477  if (navi.isConstant())
478  return cache_mgr.generate(navi);
479 
480  if (degree == 0)
481  return cache_mgr.generate(dd_get_constant(navi));
482 
483  // Check cache for previous results
484  NaviType cached = cache_mgr.find(navi, deg2node(degree, cache_mgr.manager()));
485  if (cached.isValid())
486  return cache_mgr.generate(cached);
487 
488  // Go to next branch
489  if ( max_degree_on_then(deg_mgr, navi, degree, prop) ) {
490  NaviType then_branch = navi.thenBranch();
491  init = dd_recursive_degree_lead(cache_mgr, deg_mgr, then_branch,
492  init, degree - 1, prop);
493 
494  if ((navi.elseBranch().isEmpty()) && (init.navigation()==then_branch))
495  init = cache_mgr.generate(navi);
496  else
497  init = init.change(*navi);
498 
499  }
500  else {
501  init = dd_recursive_degree_lead(cache_mgr, deg_mgr, navi.elseBranch(),
502  init, degree, prop);
503  }
505  NaviType resultNavi(init.navigation());
506  cache_mgr.insert(navi, deg2node(degree, cache_mgr.manager()), resultNavi);
507 // if (!cache_mgr.find(resultNavi).isValid())
508 // deg_mgr.insert(resultNavi, degree, degree);
509 
510  return init;
511 }
512 
513 template <class CacheType, class DegCacheMgr, class NaviType,
514  class TermType, class DescendingProperty>
515 TermType
516 dd_recursive_degree_lead(const CacheType& cache_mgr, const DegCacheMgr& deg_mgr,
517  NaviType navi, TermType init, DescendingProperty prop){
518 
519 // if (navi.isConstant())
520 // return cache_mgr.generate(dd_get_constant(navi));
521 
522  return dd_recursive_degree_lead(cache_mgr, deg_mgr, navi, init,
523  dd_cached_degree(deg_mgr, navi), prop);
524 }
525 
526 template <class CacheType, class DegCacheMgr, class NaviType,
527  class TermType, class SizeType, class DescendingProperty>
528 TermType&
529 dd_recursive_degree_leadexp(const CacheType& cache_mgr,
530  const DegCacheMgr& deg_mgr,
531  NaviType navi, TermType& result,
532  SizeType degree,
533  DescendingProperty prop) {
534  typedef CIndexCacheHandle<NaviType> deg2node;
535  if PBORI_UNLIKELY(degree < 0) {
536  result.resize(0);
537  return result;
538  }
539  if (navi.isConstant())
540  return result;
541 
542  if (degree == 0) {
543  while (!navi.isConstant())
544  navi.incrementElse();
545  if (!navi.terminalValue())
546  result.resize(0);
547 
548  return result;
549  }
550 
551  // Check cache for previous result
552  NaviType cached = cache_mgr.find(navi, deg2node(degree, cache_mgr.manager()));
553  if (cached.isValid())
554  return result = result.multiplyFirst(cache_mgr.generate(cached));
555 
556  // Prepare next branch
557  if ( max_degree_on_then(deg_mgr, navi, degree, prop) ) {
558  result.push_back(*navi);
559  navi.incrementThen();
560  --degree;
561  }
562  else
563  navi.incrementElse();
564 
565  return
566  dd_recursive_degree_leadexp(cache_mgr, deg_mgr, navi, result, degree, prop);
567 }
568 
569 template <class CacheType, class DegCacheMgr, class NaviType,
570  class TermType, class DescendingProperty>
571 TermType&
572 dd_recursive_degree_leadexp(const CacheType& cache_mgr,
573  const DegCacheMgr& deg_mgr,
574  NaviType navi, TermType& result,
575  DescendingProperty prop) {
576 
577  if (navi.isConstant())
578  return result;
579 
580  return dd_recursive_degree_leadexp(cache_mgr, deg_mgr, navi, result,
581  dd_cached_degree(deg_mgr, navi), prop);
582 }
583 
584 // Existential Abstraction. Given a ZDD F, and a set of variables
585 // S, remove all occurrences of s in S from any subset in F. This can
586 // be implemented by cofactoring F with respect to s = 1 and s = 0,
587 // then forming the union of these results.
588 
589 
590 template <class CacheType, class NaviType, class TermType>
591 TermType
592 dd_existential_abstraction(const CacheType& cache_mgr,
593  NaviType varsNavi, NaviType navi, TermType init){
594 
595  typedef typename TermType::dd_type dd_type;
596  typedef typename TermType::idx_type idx_type;
597 
598  if (navi.isConstant())
599  return cache_mgr.generate(navi);
600 
601  idx_type index(*navi);
602  while (!varsNavi.isConstant() && ((*varsNavi) < index))
603  varsNavi.incrementThen();
604 
605  if (varsNavi.isConstant())
606  return cache_mgr.generate(navi);
607 
608  // Check cache for previous result
609  NaviType cached = cache_mgr.find(varsNavi, navi);
610  if (cached.isValid())
611  return cache_mgr.generate(cached);
612 
613  NaviType thenNavi(navi.thenBranch()), elseNavi(navi.elseBranch());
614 
615  TermType thenResult =
616  dd_existential_abstraction(cache_mgr, varsNavi, thenNavi, init);
617 
618  TermType elseResult =
619  dd_existential_abstraction(cache_mgr, varsNavi, elseNavi, init);
620 
621  if ((*varsNavi) == index)
622  init = thenResult.unite(elseResult);
623  else if ( (thenResult.navigation() == thenNavi) &&
624  (elseResult.navigation() == elseNavi) )
625  init = cache_mgr.generate(navi);
626  else
627  init = dd_type(index, thenResult, elseResult);
628 
629  // Insert result to cache
630  cache_mgr.insert(varsNavi, navi, init.navigation());
631 
632  return init;
633 }
634 
635 
636 
637 template <class CacheType, class NaviType, class PolyType>
638 PolyType
639 dd_divide_recursively(const CacheType& cache_mgr,
640  NaviType navi, NaviType monomNavi, PolyType init){
641 
642  // Extract subtypes
643  typedef typename NaviType::idx_type idx_type;
644  typedef NaviType navigator;
645  typedef typename PolyType::dd_type dd_type;
646 
647  if (monomNavi.isConstant()) {
648  PBORI_ASSERT(monomNavi.terminalValue() == true);
649  return cache_mgr.generate(navi);
650  }
651 
652  PBORI_ASSERT(monomNavi.elseBranch().isEmpty());
653 
654  if (navi.isConstant())
655  return cache_mgr.zero();
656 
657  if (monomNavi == navi)
658  return cache_mgr.one();
659 
660  // Look up, whether operation was already used
661  navigator cached = cache_mgr.find(navi, monomNavi);
662 
663  if (cached.isValid()) { // Cache lookup sucessful
664  return cache_mgr.generate(cached);
665  }
666 
667  // Cache lookup not sucessful
668  // Get top variables' index
669 
670  idx_type index = *navi;
671  idx_type monomIndex = *monomNavi;
672 
673  if (monomIndex == index) { // Case: monom and poly start with same index
674 
675  // Increment navigators
676  navigator monomThen = monomNavi.thenBranch();
677  navigator naviThen = navi.thenBranch();
678 
679  init = dd_divide_recursively(cache_mgr, naviThen, monomThen, init);
680  }
681  else if (monomIndex > index) { // Case: monomIndex may occure within poly
682 
683  init =
684  dd_type(index,
685  dd_divide_recursively(cache_mgr, navi.thenBranch(), monomNavi,
686  init).diagram(),
687  dd_divide_recursively(cache_mgr, navi.elseBranch(), monomNavi,
688  init).diagram() );
689  }
690 
691  // Insert in cache
692  cache_mgr.insert(navi, monomNavi, init.navigation());
693 
694  return init;
695 }
696 
697 
698 
699 template <class DDGenerator, class Iterator, class NaviType, class PolyType>
700 PolyType
701 dd_divide_recursively_exp(const DDGenerator& ddgen,
702  NaviType navi, Iterator start, Iterator finish,
703  PolyType init){
704 
705  // Extract subtypes
706  typedef typename NaviType::idx_type idx_type;
707  typedef typename PolyType::dd_type dd_type;
708  typedef NaviType navigator;
709 
710  if (start == finish)
711  return ddgen.generate(navi);
712 
713  if (navi.isConstant())
714  return ddgen.zero();
715 
716 
717  // Cache lookup not sucessful
718  // Get top variables' index
719 
720  idx_type index = *navi;
721  idx_type monomIndex = *start;
722 
723  PolyType result(ddgen.zero());
724  if (monomIndex == index) { // Case: monom and poly start with same index
725 
726  // Increment navigators
727  ++start;
728  navigator naviThen = navi.thenBranch();
729 
730  result = dd_divide_recursively_exp(ddgen, naviThen, start, finish, init);
731  }
732  else if (monomIndex > index) { // Case: monomIndex may occure within poly
733 
734  result =
735  dd_type(index,
736  dd_divide_recursively_exp(ddgen, navi.thenBranch(), start, finish,
737  init).diagram(),
738  dd_divide_recursively_exp(ddgen, navi.elseBranch(), start, finish,
739  init).diagram() );
740  }
741  else
742  result = ddgen.zero();
743 
744  return result;
745 }
746 
749 template <class CacheType, class NaviType, class MonomType>
750 MonomType
751 cached_used_vars(const CacheType& cache, NaviType navi, MonomType init) {
752 
753  if (navi.isConstant()) // No need for caching of constant nodes' degrees
754  return init;
755 
756  // Look whether result was cached before
757  NaviType cached_result = cache.find(navi);
758 
759  typedef typename MonomType::poly_type poly_type;
760  if (cached_result.isValid())
761  return CDDOperations<typename MonomType::dd_type,
762  MonomType>().getMonomial(cache.generate(cached_result));
763 
764  MonomType result = cached_used_vars(cache, navi.thenBranch(), init);
765  result *= cached_used_vars(cache, navi.elseBranch(), init);
766 
767  result = result.change(*navi);
768 
769  // Write result to cache
770  cache.insert(navi, result.diagram().navigation());
771 
772  return result;
773 }
774 
775 template <class NaviType, class Iterator>
776 bool
777 dd_owns(NaviType navi, Iterator start, Iterator finish) {
778 
779  if (start == finish) {
780  while(!navi.isConstant())
781  navi.incrementElse();
782  return navi.terminalValue();
783  }
784 
785  while(!navi.isConstant() && (*start > *navi) )
786  navi.incrementElse();
787 
788  if (navi.isConstant() || (*start != *navi))
789  return false;
790 
791  return dd_owns(navi.thenBranch(), ++start, finish);
792 }
793 
796 template <class NaviType, class MonomIterator>
797 bool
799  MonomIterator start, MonomIterator finish) {
800 
801  // Managing trivial cases
802 
803  if (start == finish) // divisors of monomial 1 is the empty set,
804  // which is always contained
805  return true;
806 
807  if (navi.isConstant()) { // set is empty or owns 1 only
808  if (navi.terminalValue()) // set == {1}
809  return (++start == finish); // whether monom is of degree one
810  else // empty set contains no divisors
811  return false;
812 
813  }
814 
815  // Actual computations
816 
817  if (*navi < *start)
818  return dd_contains_divs_of_dec_deg(navi.elseBranch(), start, finish);
819 
820 
821  if (*navi > *start) {
822  if (++start == finish) // if monom is of degree one
823  return owns_one(navi);
824  else
825  return false;
826  }
827 
828  // (*navi == *start) here
829  ++start;
830  return dd_owns(navi.elseBranch(), start, finish) &&
831  dd_contains_divs_of_dec_deg(navi.thenBranch(), start, finish);
832 }
833 
834 
835 
836 // determine the part of a polynomials of a given degree
837 template <class CacheType, class NaviType, class DegType, class SetType>
838 SetType
839 dd_graded_part(const CacheType& cache, NaviType navi, DegType deg,
840  SetType init) {
841 
842 
843  if (deg == 0) {
844  while(!navi.isConstant())
845  navi.incrementElse();
846  return cache.generate(navi);
847  }
848 
849  if(navi.isConstant())
850  return cache.zero();
851 
852  // Look whether result was cached before
853  NaviType cached = cache.find(navi, deg);
854 
855  if (cached.isValid())
856  return cache.generate(cached);
857 
858  SetType result =
859  SetType(*navi,
860  dd_graded_part(cache, navi.thenBranch(), deg - 1, init),
861  dd_graded_part(cache, navi.elseBranch(), deg, init)
862  );
863 
864  // store result for later reuse
865  cache.insert(navi, deg, result.navigation());
866 
867  return result;
868 }
869 
870 
874 template <class CacheManager, class NaviType, class SetType>
875 SetType
876 dd_first_divisors_of(CacheManager cache_mgr, NaviType navi,
877  NaviType rhsNavi, SetType init ) {
878 
879  typedef typename SetType::dd_type dd_type;
880  while( (!navi.isConstant()) && (*rhsNavi != *navi) ) {
881 
882  if ( (*rhsNavi < *navi) && (!rhsNavi.isConstant()) )
883  rhsNavi.incrementThen();
884  else
885  navi.incrementElse();
886  }
887 
888  if (navi.isConstant()) // At end of path
889  return cache_mgr.generate(navi);
890 
891  // Look up, whether operation was already used
892  NaviType result = cache_mgr.find(navi, rhsNavi);
893 
894  if (result.isValid()) // Cache lookup sucessful
895  return cache_mgr.generate(result);
896 
897  PBORI_ASSERT(*rhsNavi == *navi);
898 
899  // Compute new result
900  init = dd_type(*rhsNavi,
901  dd_first_divisors_of(cache_mgr, navi.thenBranch(), rhsNavi,
902  init).diagram(),
903  dd_first_divisors_of(cache_mgr, navi.elseBranch(), rhsNavi,
904  init).diagram() );
905  // Insert result to cache
906  cache_mgr.insert(navi, rhsNavi, init.navigation());
907 
908  return init;
909 }
910 
911 template <class CacheType, class NaviType, class SetType>
912 SetType
913 dd_first_multiples_of(const CacheType& cache_mgr,
914  NaviType navi, NaviType rhsNavi, SetType init){
915 
916  typedef typename SetType::dd_type dd_type;
917 
918  if(rhsNavi.isConstant()) {
919  PBORI_ASSERT(rhsNavi.terminalValue() == true);
920  return cache_mgr.generate(navi);
921  }
922 
923  if (navi.isConstant() || (*navi > *rhsNavi))
924  return cache_mgr.zero();
925 
926  if (*navi == *rhsNavi)
927  return dd_first_multiples_of(cache_mgr, navi.thenBranch(),
928  rhsNavi.thenBranch(), init).change(*navi);
929 
930  // Look up old result - if any
931  NaviType result = cache_mgr.find(navi, rhsNavi);
932 
933  if (result.isValid())
934  return cache_mgr.generate(result);
935 
936  // Compute new result
937  init = dd_type(*navi,
938  dd_first_multiples_of(cache_mgr, navi.thenBranch(),
939  rhsNavi, init).diagram(),
940  dd_first_multiples_of(cache_mgr, navi.elseBranch(),
941  rhsNavi, init).diagram() );
942 
943  // Insert new result in cache
944  cache_mgr.insert(navi, rhsNavi, init.navigation());
945 
946  return init;
947 }
948 
949 
952 template <class PolyType, class RingType, class MapType, class NaviType>
953 PolyType
954 substitute_variables__(const RingType& ring, const MapType& idx2poly, NaviType navi) {
955 
956  if (navi.isConstant())
957  return ring.constant(navi.terminalValue());
958 
959  //typename MapType::const_reference var(idx2poly[*navi]);
960  // PBORI_ASSERT(var.ring() == ring);
961  return (idx2poly[*navi] *
962  substitute_variables__<PolyType>(ring, idx2poly, navi.thenBranch())) +
963  substitute_variables__<PolyType>(ring, idx2poly, navi.elseBranch());
964 }
965 
968 template <class RingType, class MapType, class PolyType>
969 PolyType
970 substitute_variables(const RingType& ring,
971  const MapType& idx2poly, const PolyType& poly) {
972 
973  return substitute_variables__<PolyType>(ring, idx2poly, poly.navigation());
974 }
975 
976 
978 
979 #endif