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