PolyBoRi
pbori_algo.h
Go to the documentation of this file.
1 // -*- c++ -*-
2 //*****************************************************************************
17 //*****************************************************************************
18 
19 #ifndef polybori_routines_pbori_algo_h_
20 #define polybori_routines_pbori_algo_h_
21 
22 // include polybori's definitions
23 #include <polybori/pbori_defs.h>
24 
25 // get polybori's functionals
26 #include "pbori_func.h"
27 #include <polybori/common/traits.h>
28 
29 // temporarily
30 #include <polybori/cudd/cudd.h>
32 
34 
35 
37 template< class NaviType, class TermType,
38  class TernaryOperator,
39  class TerminalOperator >
40 TermType
41 dd_backward_transform( NaviType navi, TermType init, TernaryOperator newNode,
42  TerminalOperator terminate ) {
43 
44  TermType result = init;
45 
46  if (navi.isConstant()) { // Reached end of path
47  if (navi.terminalValue()){ // Case of a valid path
48  result = terminate();
49  }
50  }
51  else {
52  result = dd_backward_transform(navi.thenBranch(), init, newNode, terminate);
53  result = newNode(*navi, result,
54  dd_backward_transform(navi.elseBranch(), init, newNode,
55  terminate) );
56  }
57  return result;
58 }
59 
60 
62 template< class NaviType, class TermType, class OutIterator,
63  class ThenBinaryOperator, class ElseBinaryOperator,
64  class TerminalOperator >
65 OutIterator
66 dd_transform( NaviType navi, TermType init, OutIterator result,
67  ThenBinaryOperator then_binop, ElseBinaryOperator else_binop,
68  TerminalOperator terminate ) {
69 
70 
71  if (navi.isConstant()) { // Reached end of path
72  if (navi.terminalValue()){ // Case of a valid path
73  *result = terminate(init);
74  ++result;
75  }
76  }
77  else {
78  result = dd_transform(navi.thenBranch(), then_binop(init, *navi), result,
79  then_binop, else_binop, terminate);
80  result = dd_transform(navi.elseBranch(), else_binop(init, *navi), result,
81  then_binop, else_binop, terminate);
82  }
83  return result;
84 }
85 
88 template< class NaviType, class TermType, class OutIterator,
89  class ThenBinaryOperator, class ElseBinaryOperator,
90  class TerminalOperator, class FirstTermOp >
91 OutIterator
92 dd_transform( NaviType navi, TermType init, OutIterator result,
93  ThenBinaryOperator then_binop, ElseBinaryOperator else_binop,
94  TerminalOperator terminate, FirstTermOp terminate_first ) {
95 
96  if (navi.isConstant()) { // Reached end of path
97  if (navi.terminalValue()){ // Case of a valid path - here leading term
98  *result = terminate_first(init);
99  ++result;
100  }
101  }
102  else {
103  result = dd_transform(navi.thenBranch(), then_binop(init, *navi), result,
104  then_binop, else_binop, terminate, terminate_first);
105  result = dd_transform(navi.elseBranch(), else_binop(init, *navi), result,
106  then_binop, else_binop, terminate);
107  }
108  return result;
109 }
110 
112 template< class NaviType, class TermType, class OutIterator,
113  class ThenBinaryOperator, class ElseBinaryOperator >
114 void
115 dd_transform( const NaviType& navi, const TermType& init,
116  const OutIterator& result,
117  const ThenBinaryOperator& then_binop,
118  const ElseBinaryOperator& else_binop ) {
119 
120  dd_transform(navi, init, result, then_binop, else_binop,
121  project_ith<1>() );
122 }
123 
125 template< class NaviType, class TermType, class OutIterator,
126  class ThenBinaryOperator >
127 void
128 dd_transform( const NaviType& navi, const TermType& init,
129  const OutIterator& result,
130  const ThenBinaryOperator& then_binop ) {
131 
132  dd_transform(navi, init, result, then_binop,
134  project_ith<1>() );
135 }
136 
137 
138 template <class InputIterator, class OutputIterator,
139  class FirstFunction, class UnaryFunction>
140 OutputIterator
141 special_first_transform(InputIterator first, InputIterator last,
142  OutputIterator result,
143  UnaryFunction op, FirstFunction firstop) {
144  InputIterator second(first);
145  if (second != last) {
146  ++second;
147  result = std::transform(first, second, result, firstop);
148  }
149  return std::transform(second, last, result, op);
150 }
151 
152 
154 template <class InputIterator, class Intermediate, class OutputIterator>
155 OutputIterator
156 reversed_inter_copy( InputIterator start, InputIterator finish,
157  Intermediate& inter, OutputIterator output ) {
158 
159  std::copy(start, finish, inter.begin());
160  // force constant
161  return std::copy( const_cast<const Intermediate&>(inter).rbegin(),
162  const_cast<const Intermediate&>(inter).rend(),
163  output );
164 }
165 
168 template <class NaviType>
169 bool
170 dd_on_path(NaviType navi) {
171 
172  if (navi.isConstant())
173  return navi.terminalValue();
174 
175  return dd_on_path(navi.thenBranch()) || dd_on_path(navi.elseBranch());
176 }
177 
180 template <class NaviType, class OrderedIterator>
181 bool
182 dd_owns_term_of_indices(NaviType navi,
183  OrderedIterator start, OrderedIterator finish) {
184 
185  if (!navi.isConstant()) { // Not at end of path
186  bool not_at_end;
187 
188  while( (not_at_end = (start != finish)) && (*start < *navi) )
189  ++start;
190 
191  NaviType elsenode = navi.elseBranch();
192 
193  if (elsenode.isConstant() && elsenode.terminalValue())
194  return true;
195 
196 
197  if (not_at_end){
198 
199  if ( (*start == *navi) &&
200  dd_owns_term_of_indices(navi.thenBranch(), start, finish))
201  return true;
202  else
203  return dd_owns_term_of_indices(elsenode, start, finish);
204  }
205  else {
206 
207  while(!elsenode.isConstant())
208  elsenode.incrementElse();
209  return elsenode.terminalValue();
210  }
211 
212  }
213  return navi.terminalValue();
214 }
215 
219 template <class NaviType, class OrderedIterator, class NodeOperation>
220 NaviType
221 dd_intersect_some_index(NaviType navi,
222  OrderedIterator start, OrderedIterator finish,
223  NodeOperation newNode ) {
224 
225  if (!navi.isConstant()) { // Not at end of path
226  bool not_at_end;
227  while( (not_at_end = (start != finish)) && (*start < *navi) )
228  ++start;
229 
230  if (not_at_end) {
231  NaviType elseNode =
232  dd_intersect_some_index(navi.elseBranch(), start, finish,
233  newNode);
234 
235  if (*start == *navi) {
236 
237  NaviType thenNode =
238  dd_intersect_some_index(navi.thenBranch(), start, finish,
239  newNode);
240 
241  return newNode(*start, navi, thenNode, elseNode);
242  }
243  else
244  return elseNode;
245  }
246  else { // if the start == finish, we only check
247  // validity of the else-only branch
248  while(!navi.isConstant())
249  navi = navi.elseBranch();
250  return newNode(navi);
251  }
252 
253  }
254 
255  return newNode(navi);
256 }
257 
258 
259 
261 template <class NaviType>
262 void
263 dd_print(NaviType navi) {
264 
265  if (!navi.isConstant()) { // Not at end of path
266 
267  std::cout << std::endl<< "idx " << *navi <<" addr "<<
268  ((DdNode*)navi)<<" ref "<<
269  int(PBORI_PREFIX(Cudd_Regular)((DdNode*)navi)->ref) << std::endl;
270 
271  dd_print(navi.thenBranch());
272  dd_print(navi.elseBranch());
273 
274  }
275  else {
276  std::cout << "const isvalid? "<<navi.isValid()<<" addr "
277  <<((DdNode*)navi)<<" ref "<<
278  int(PBORI_PREFIX(Cudd_Regular)((DdNode*)navi)->ref)<<std::endl;
279 
280  }
281 }
282 
283 // Determinine the minimum of the distance between two iterators and limit
284 template <class IteratorType, class SizeType>
285 SizeType
286 limited_distance(IteratorType start, IteratorType finish, SizeType limit) {
287 
288  SizeType result = 0;
289 
290  while ((result < limit) && (start != finish)) {
291  ++start, ++result;
292  }
293 
294  return result;
295 }
296 
297 #if 0
298 // Forward declaration of CTermIter template
299 template <class, class, class, class, class, class> class CTermIter;
300 
301 // Determinine the minimum of the number of terms and limit
302 template <class NaviType, class SizeType>
303 SizeType
304 limited_length(NaviType navi, SizeType limit) {
305 
306 
307  typedef CTermIter<dummy_iterator, NaviType,
308  project_ith<1>, project_ith<1>, project_ith<1, 2>,
309  project_ith<1> >
310  iterator;
311 
312  return limited_distance(iterator(navi), iterator(), limit);
313 }
314 #endif
315 
317 template <class NaviType>
318 bool owns_one(NaviType navi) {
319  while (!navi.isConstant() )
320  navi.incrementElse();
321 
322  return navi.terminalValue();
323 }
324 
325 template <class CacheMgr, class NaviType, class SetType>
326 SetType
327 dd_modulo_monomials(const CacheMgr& cache_mgr,
328  NaviType navi, NaviType rhs, const SetType& init){
329 
330  // Managing trivial cases
331  if (owns_one(rhs)) return cache_mgr.zero();
332 
333  if (navi.isConstant())
334  return cache_mgr.generate(navi);
335 
336  typename SetType::idx_type index = *navi;
337  while(*rhs < index )
338  rhs.incrementElse();
339 
340  if (rhs.isConstant())
341  return cache_mgr.generate(navi);
342 
343  if (rhs == navi)
344  return cache_mgr.zero();
345 
346  // Cache look-up
347  NaviType cached = cache_mgr.find(navi, rhs);
348  if (cached.isValid())
349  return cache_mgr.generate(cached);
350 
351  // Actual computations
352  SetType result(cache_mgr.zero());
353  if (index == *rhs){
354 
355  NaviType rhselse = rhs.elseBranch();
356  SetType thenres =
357  dd_modulo_monomials(cache_mgr, navi.thenBranch(), rhs.thenBranch(), init);
358 
359  result =
360  SetType(index,
361  dd_modulo_monomials(cache_mgr,
362  thenres.navigation(), rhselse, init),
363  dd_modulo_monomials(cache_mgr,
364  navi.elseBranch(), rhselse, init)
365  );
366 
367  }
368  else {
369  PBORI_ASSERT(*rhs > index);
370  result =
371  SetType(index,
372  dd_modulo_monomials(cache_mgr, navi.thenBranch(), rhs, init),
373  dd_modulo_monomials(cache_mgr, navi.elseBranch(), rhs, init)
374  );
375  }
376  cache_mgr.insert(navi, rhs, result.navigation());
377  return result;
378 }
379 
381 template <class CacheMgr, class ModMonCacheMgr, class NaviType, class SetType>
382 SetType
383 dd_minimal_elements(const CacheMgr& cache_mgr, const ModMonCacheMgr& modmon_mgr,
384  NaviType navi, const SetType& init){
385 
386  // Trivial Cases
387  if (navi.isEmpty())
388  return cache_mgr.generate(navi);
389 
390  if (owns_one(navi)) return cache_mgr.one();
391 
392  NaviType ms0 = navi.elseBranch();
393  NaviType ms1 = navi.thenBranch();
394 
395  // Cache look-up
396  NaviType cached = cache_mgr.find(navi);
397  if (cached.isValid())
398  return cache_mgr.generate(cached);
399 
400  SetType minimal_else = dd_minimal_elements(cache_mgr, modmon_mgr, ms0, init);
401  SetType minimal_then =
402  dd_minimal_elements(cache_mgr, modmon_mgr,
403  dd_modulo_monomials(modmon_mgr, ms1,
404  minimal_else.navigation(),
405  init).navigation(),
406  init);
407  SetType result(cache_mgr.zero());
408  if ( (minimal_else.navigation() == ms0)
409  && (minimal_then.navigation() == ms1) )
410  result = cache_mgr.generate(navi);
411  else
412  result = SetType(*navi, minimal_then, minimal_else);
413 
414  cache_mgr.insert(navi, result.navigation());
415  return result;
416 }
417 
418 
422 template <class NaviType, class DDType>
423 DDType
424 dd_minimal_elements(NaviType navi, DDType dd, DDType& multiples) {
425 
426 
427  if (!navi.isConstant()) { // Not at end of path
428 
429  DDType elsedd = dd.subset0(*navi);
430 
431 
432  DDType elseMultiples;
433  elsedd = dd_minimal_elements(navi.elseBranch(), elsedd, elseMultiples);
434 
435  // short cut if else and then branche equal or else contains 1
436  if((navi.elseBranch() == navi.thenBranch()) || elsedd.blankness()){
437  multiples = elseMultiples;
438  return elsedd;
439  }
440 
441  NaviType elseNavi = elseMultiples.navigation();
442 
443  int nmax;
444  if (elseNavi.isConstant()){
445  if (elseNavi.terminalValue())
446  nmax = dd.nVariables();
447  else
448  nmax = *navi;
449  }
450  else
451  nmax = *elseNavi;
452 
453 
454  for(int i = nmax-1; i > *navi; --i){
455  elseMultiples.uniteAssign(elseMultiples.change(i));
456  }
457 
458 
459  DDType thendd = dd.subset1(*navi);
460  thendd = thendd.diff(elseMultiples);
461 
462  DDType thenMultiples;
463  thendd = dd_minimal_elements(navi.thenBranch(), thendd, thenMultiples);
464 
465  NaviType thenNavi = thenMultiples.navigation();
466 
467 
468  if (thenNavi.isConstant()){
469  if (thenNavi.terminalValue())
470  nmax = dd.nVariables();
471  else
472  nmax = *navi;
473  }
474  else
475  nmax = *thenNavi;
476 
477 
478  for(int i = nmax-1; i > *navi; --i){
479  thenMultiples.uniteAssign(thenMultiples.change(i));
480  }
481 
482 
483  thenMultiples = thenMultiples.unite(elseMultiples);
484  thenMultiples = thenMultiples.change(*navi);
485 
486 
487  multiples = thenMultiples.unite(elseMultiples);
488  thendd = thendd.change(*navi);
489 
490  DDType result = thendd.unite(elsedd);
491 
492  return result;
493 
494  }
495 
496  multiples = dd;
497  return dd;
498 }
499 
500 template <class MgrType>
501 inline const MgrType&
502 get_mgr_core(const MgrType& rhs) {
503  return rhs;
504 }
505 
506 
508 // inline CCuddInterface::mgrcore_ptr
509 // get_mgr_core(const CCuddInterface& mgr) {
510 // return mgr.managerCore();
511 // }
512 
514 template<class ManagerType, class ReverseIterator, class MultReverseIterator,
515 class DDBase>
516 inline DDBase
517 cudd_generate_multiples(const ManagerType& mgr,
518  ReverseIterator start, ReverseIterator finish,
519  MultReverseIterator multStart,
520  MultReverseIterator multFinish, type_tag<DDBase> ) {
521 
522  DdNode* prev( (mgr.getManager())->one );
523 
524  DdNode* zeroNode( (mgr.getManager())->zero );
525 
526  PBORI_PREFIX(Cudd_Ref)(prev);
527  while(start != finish) {
528 
529  while((multStart != multFinish) && (*start < *multStart)) {
530 
531  DdNode* result = PBORI_PREFIX(cuddUniqueInterZdd)( mgr.getManager(), *multStart,
532  prev, prev );
533 
534  PBORI_PREFIX(Cudd_Ref)(result);
535  PBORI_PREFIX(Cudd_RecursiveDerefZdd)(mgr.getManager(), prev);
536 
537  prev = result;
538  ++multStart;
539 
540  };
541 
542  DdNode* result = PBORI_PREFIX(cuddUniqueInterZdd)( mgr.getManager(), *start,
543  prev, zeroNode );
544 
545  PBORI_PREFIX(Cudd_Ref)(result);
546  PBORI_PREFIX(Cudd_RecursiveDerefZdd)(mgr.getManager(), prev);
547 
548  prev = result;
549 
550 
551  if((multStart != multFinish) && (*start == *multStart))
552  ++multStart;
553 
554 
555  ++start;
556  }
557 
558  while(multStart != multFinish) {
559 
560  DdNode* result = PBORI_PREFIX(cuddUniqueInterZdd)( mgr.getManager(), *multStart,
561  prev, prev );
562 
563  PBORI_PREFIX(Cudd_Ref)(result);
564  PBORI_PREFIX(Cudd_RecursiveDerefZdd)(mgr.getManager(), prev);
565 
566  prev = result;
567  ++multStart;
568 
569  };
570 
571  PBORI_PREFIX(Cudd_Deref)(prev);
572 
573  typedef DDBase dd_base;
574  return dd_base(mgr, prev);
575  }
576 
577 
578 
580 template<class ManagerType, class ReverseIterator, class DDBase>
581 DDBase
582 cudd_generate_divisors(const ManagerType& mgr,
583  ReverseIterator start, ReverseIterator finish, type_tag<DDBase>) {
584 
585 
586  DdNode* prev= (mgr.getManager())->one;
587 
588  PBORI_PREFIX(Cudd_Ref)(prev);
589  while(start != finish) {
590 
591  DdNode* result = PBORI_PREFIX(cuddUniqueInterZdd)( mgr.getManager(), *start,
592  prev, prev);
593 
594  PBORI_PREFIX(Cudd_Ref)(result);
595  PBORI_PREFIX(Cudd_RecursiveDerefZdd)(mgr.getManager(), prev);
596 
597  prev = result;
598  ++start;
599  }
600 
601  PBORI_PREFIX(Cudd_Deref)(prev);
603  return DDBase(mgr, prev);
604 
605 }
606 
607 
608 template<class Iterator, class SizeType>
609 Iterator
610 bounded_max_element(Iterator start, Iterator finish, SizeType bound){
611 
612  if (*start >= bound)
613  return start;
614 
615  Iterator result(start);
616  if (start != finish)
617  ++start;
618 
619  while (start != finish) {
620  if(*start >= bound)
621  return start;
622  if(*start > *result)
623  result = start;
624  ++start;
625  }
626 
627  return result;
628 }
629 
631 template <class LhsType, class RhsType, class BinaryPredicate>
632 CTypes::comp_type
633 generic_compare_3way(const LhsType& lhs, const RhsType& rhs, BinaryPredicate comp) {
634 
635  if (lhs == rhs)
636  return CTypes::equality;
637 
638  return (comp(lhs, rhs)? CTypes::greater_than: CTypes::less_than);
639 }
640 
641 
642 
643 template <class IteratorLike, class ForwardIteratorTag>
644 IteratorLike
645 increment_iteratorlike(IteratorLike iter, ForwardIteratorTag) {
646 
647  return ++iter;
648 }
649 
650 template <class IteratorLike>
651 IteratorLike
653 
654  return iter.thenBranch();
655 }
656 
657 
658 template <class IteratorLike>
659 IteratorLike
660 increment_iteratorlike(IteratorLike iter) {
661 
662  typedef typename std::iterator_traits<IteratorLike>::iterator_category
663  iterator_category;
664 
665  return increment_iteratorlike(iter, iterator_category());
666 }
667 
668 #ifdef PBORI_LOWLEVEL_XOR
669 
670 // dummy for PBORI_PREFIX(cuddcache) (implemented in pbori_routines.cc)
671 DdNode*
672 pboriCuddZddUnionXor__(DdManager *, DdNode *, DdNode *);
673 
674 
678 template <class MgrType, class NodeType>
679 NodeType
680 pboriCuddZddUnionXor(MgrType zdd, NodeType P, NodeType Q) {
681 
682  int p_top, q_top;
683  NodeType empty = DD_ZERO(zdd), t, e, res;
684  MgrType table = zdd;
685 
686  statLine(zdd);
687 
688  if (P == empty)
689  return(Q);
690  if (Q == empty)
691  return(P);
692  if (P == Q)
693  return(empty);
694 
695  /* Check cache */
697  if (res != NULL)
698  return(res);
699 
700  if (PBORI_PREFIX(cuddIsConstant)(P))
701  p_top = P->index;
702  else
703  p_top = P->index;/* zdd->permZ[P->index]; */
704  if (PBORI_PREFIX(cuddIsConstant)(Q))
705  q_top = Q->index;
706  else
707  q_top = Q->index; /* zdd->permZ[Q->index]; */
708  if (p_top < q_top) {
709  e = pboriCuddZddUnionXor(zdd, PBORI_PREFIX(cuddE)(P), Q);
710  if (e == NULL) return (NULL);
712  res = PBORI_PREFIX(cuddZddGetNode)(zdd, P->index, PBORI_PREFIX(cuddT)(P), e);
713  if (res == NULL) {
715  return(NULL);
716  }
718  } else if (p_top > q_top) {
719  e = pboriCuddZddUnionXor(zdd, P, PBORI_PREFIX(cuddE)(Q));
720  if (e == NULL) return(NULL);
722  res = PBORI_PREFIX(cuddZddGetNode)(zdd, Q->index, PBORI_PREFIX(cuddT)(Q), e);
723  if (res == NULL) {
725  return(NULL);
726  }
728  } else {
729  t = pboriCuddZddUnionXor(zdd, PBORI_PREFIX(cuddT)(P), PBORI_PREFIX(cuddT)(Q));
730  if (t == NULL) return(NULL);
732  e = pboriCuddZddUnionXor(zdd, PBORI_PREFIX(cuddE)(P), PBORI_PREFIX(cuddE)(Q));
733  if (e == NULL) {
735  return(NULL);
736  }
738  res = PBORI_PREFIX(cuddZddGetNode)(zdd, P->index, t, e);
739  if (res == NULL) {
742  return(NULL);
743  }
746  }
747 
749 
750  return(res);
751 } /* end of pboriCuddZddUnionXor */
752 
753 template <class MgrType, class NodeType>
754 NodeType
755 pboriCudd_zddUnionXor(MgrType dd, NodeType P, NodeType Q) {
756 
757  NodeType res;
758  do {
759  dd->reordered = 0;
760  res = pboriCuddZddUnionXor(dd, P, Q);
761  } while (dd->reordered == 1);
762  return(res);
763 }
764 
765 #endif // PBORI_LOWLEVEL_XOR
766 
767 
768 template <class NaviType>
769 bool
770 dd_is_singleton(NaviType navi) {
771 
772  while(!navi.isConstant()) {
773  if (!navi.elseBranch().isEmpty())
774  return false;
775  navi.incrementThen();
776  }
777  return true;
778 }
779 
780 template <class NaviType, class BooleConstant>
781 BooleConstant
782 dd_pair_check(NaviType navi, BooleConstant allowSingleton) {
783 
784  while(!navi.isConstant()) {
785 
786  if (!navi.elseBranch().isEmpty())
787  return dd_is_singleton(navi.elseBranch()) &&
788  dd_is_singleton(navi.thenBranch());
789 
790  navi.incrementThen();
791  }
792  return allowSingleton;//();
793 }
794 
795 
796 template <class NaviType>
797 bool
798 dd_is_singleton_or_pair(NaviType navi) {
799 
800  return dd_pair_check(navi, true);
801 }
802 
803 template <class NaviType>
804 bool
805 dd_is_pair(NaviType navi) {
806 
807  return dd_pair_check(navi, false);
808 }
809 
810 
811 
812 template <class SetType>
813 void combine_sizes(const SetType& bset, double& init) {
814  init += bset.sizeDouble();
815 }
816 
817 template <class SetType>
818 void combine_sizes(const SetType& bset,
819  typename SetType::size_type& init) {
820  init += bset.size();
821 }
822 
823 
824 template <class SizeType, class IdxType, class NaviType, class SetType>
825 SizeType&
826 count_index(SizeType& size, IdxType idx, NaviType navi, const SetType& init) {
827 
828  if (*navi == idx)
829  combine_sizes(SetType(navi.incrementThen(), init.ring()), size);
830 
831  if (*navi < idx) {
832  count_index(size, idx, navi.thenBranch(), init);
833  count_index(size, idx, navi.elseBranch(), init);
834  }
835  return size;
836 }
837 
838 
839 template <class SizeType, class IdxType, class SetType>
840 SizeType&
841 count_index(SizeType& size, IdxType idx, const SetType& bset) {
842 
843  return count_index(size, idx, bset.navigation(), SetType(bset.ring()));
844 }
845 
846 
847 template <class InIter, class OutIter, class Object, class MemberFuncPtr>
848 inline OutIter
849 transform(InIter start, InIter finish, OutIter result, Object& obj,
850  MemberFuncPtr func) {
851  for(; start != finish; ++start, ++result)
852  *result = (obj .* func)(*start);
853 }
854 
855 template <class InIter, class Object, class MemberFuncPtr>
856 inline void
857 for_each(InIter start, InIter finish, Object& obj, MemberFuncPtr func) {
858  for(; start != finish; ++start)
859  (obj .* func)(*start);
860 }
861 
862 template <class InIter, class Object, class MemberFuncPtr>
863 inline void
864 for_each(InIter start, InIter finish, const Object& obj, MemberFuncPtr func) {
865  for(; start != finish; ++start)
866  (obj .* func)(*start);
867 }
868 template <class Type, class Type1>
869 const Type&
870 which(bool condition, const Type1& value1, const Type& value) {
871  if (condition)
872  return value1;
873  return value;
874 }
875 
876 template <class Type, class Type1, class Type2>
877 const Type&
878 which(bool cond1, const Type1& value1,
879  bool cond2, const Type2& value2, const Type& value) {
880  return which(cond1, value1, which(cond2, value2, value) );
881 }
882 
883 template <class Type, class Type1, class Type2, class Type3>
884 const Type&
885 which(bool cond1, const Type1& value1,
886  bool cond2, const Type2& value2,
887  bool cond3, const Type3& value3, const Type& value ) {
888  return which(cond1, value1, cond2, value2, which(cond3, value3, value) );
889 }
890 
891 
892 
893 
894 template <class IDType, class Iterator>
895 bool same_rings(const IDType& id, Iterator start, Iterator finish) {
896 
897  while ((start != finish) && (start->ring().id() == id)) { ++start; }
898  return (start == finish);
899 }
900 
901 template <class Iterator>
902 bool same_rings(Iterator start, Iterator finish) {
903 
904  return (start == finish) || same_rings(start->ring().id(), start, finish);
905 }
906 
908 
909 #endif
#define PBORI_PREFIX(name)
Definition: prefix.h:27
NodeType pboriCuddZddUnionXor(MgrType zdd, NodeType P, NodeType Q)
Definition: pbori_algo.h:680
OutputIterator reversed_inter_copy(InputIterator start, InputIterator finish, Intermediate &inter, OutputIterator output)
Function templates doing a reversed copy using intermediate storage.
Definition: pbori_algo.h:156
#define END_NAMESPACE_PBORI
Finish project's namespace.
Definition: pbori_defs.h:77
bool dd_is_pair(NaviType navi)
Definition: pbori_algo.h:805
void dd_transform(const NaviType &navi, const TermType &init, const OutIterator &result, const ThenBinaryOperator &then_binop)
Function templates for transforming decision diagrams.
Definition: pbori_algo.h:128
#define BEGIN_NAMESPACE_PBORI
Start project's namespace.
Definition: pbori_defs.h:74
#define Cudd_RecursiveDerefZdd
Definition: prefix_internal.h:149
NodeType pboriCudd_zddUnionXor(MgrType dd, NodeType P, NodeType Q)
Definition: pbori_algo.h:755
TermType dd_backward_transform(NaviType navi, TermType init, TernaryOperator newNode, TerminalOperator terminate)
Function templates for transforming decision diagrams.
Definition: pbori_algo.h:41
bool same_rings(Iterator start, Iterator finish)
Definition: pbori_algo.h:902
#define cuddUniqueInterZdd
Definition: prefix_internal.h:181
CTypes::comp_type generic_compare_3way(const LhsType &lhs, const RhsType &rhs, BinaryPredicate comp)
defines lexicographic comparison for variable indices
Definition: pbori_algo.h:633
Accessing ith of n arguments (ITH = 0 returns default value of first type)
Definition: pbori_func.h:144
#define DdManager
Definition: prefix_internal.h:262
#define cuddZddGetNode
Definition: prefix_internal.h:231
DDBase cudd_generate_divisors(const ManagerType &mgr, ReverseIterator start, ReverseIterator finish, type_tag< DDBase >)
temporarily (needs to be more generic) (similar fct in CCuddDDFacade.h)
Definition: pbori_algo.h:582
#define cuddCacheLookup2Zdd
Definition: prefix_internal.h:191
BooleConstant dd_pair_check(NaviType navi, BooleConstant allowSingleton)
Definition: pbori_algo.h:782
IteratorLike increment_iteratorlike(IteratorLike iter)
Definition: pbori_algo.h:660
#define cuddCacheInsert2
Definition: prefix_internal.h:183
This class marks a given type.
Definition: pbori_func.h:613
DDType dd_minimal_elements(NaviType navi, DDType dd, DDType &multiples)
Definition: pbori_algo.h:424
OutputIterator special_first_transform(InputIterator first, InputIterator last, OutputIterator result, UnaryFunction op, FirstFunction firstop)
Definition: pbori_algo.h:141
bool dd_is_singleton(NaviType navi)
Definition: pbori_algo.h:770
const MgrType & get_mgr_core(const MgrType &rhs)
Definition: pbori_algo.h:502
#define PBORI_ASSERT(arg)
Definition: pbori_defs.h:118
bool dd_on_path(NaviType navi)
Definition: pbori_algo.h:170
SizeType & count_index(SizeType &size, IdxType idx, const SetType &bset)
Definition: pbori_algo.h:841
OutIter transform(InIter start, InIter finish, OutIter result, Object &obj, MemberFuncPtr func)
Definition: pbori_algo.h:849
void for_each(InIter start, InIter finish, const Object &obj, MemberFuncPtr func)
Definition: pbori_algo.h:864
DdNode * pboriCuddZddUnionXor__(DdManager *, DdNode *, DdNode *)
Definition: pbori_routines.cc:25
SetType dd_modulo_monomials(const CacheMgr &cache_mgr, NaviType navi, NaviType rhs, const SetType &init)
Definition: pbori_algo.h:327
const Type & which(bool cond1, const Type1 &value1, bool cond2, const Type2 &value2, bool cond3, const Type3 &value3, const Type &value)
Definition: pbori_algo.h:885
DDBase cudd_generate_multiples(const ManagerType &mgr, ReverseIterator start, ReverseIterator finish, MultReverseIterator multStart, MultReverseIterator multFinish, type_tag< DDBase >)
temporarily (needs to be more generic) (similar fct in CCuddDDFacade.h)
Definition: pbori_algo.h:517
polybori::CTypes::idx_type idx_type
Definition: groebner_defs.h:44
#define Cudd_Deref
Definition: prefix_internal.h:160
for iterator_category
Definition: tags.h:60
bool dd_is_singleton_or_pair(NaviType navi)
Definition: pbori_algo.h:798
This class wraps a bool value, which was not converted to a boolean polynomial or monomial yet...
Definition: BooleConstant.h:40
SizeType limited_distance(IteratorType start, IteratorType finish, SizeType limit)
Definition: pbori_algo.h:286
Iterator bounded_max_element(Iterator start, Iterator finish, SizeType bound)
Definition: pbori_algo.h:610
void dd_print(NaviType navi)
Function templates for debugging, prints dd indices and reference counts.
Definition: pbori_algo.h:263
void combine_sizes(const SetType &bset, typename SetType::size_type &init)
Definition: pbori_algo.h:818
NaviType dd_intersect_some_index(NaviType navi, OrderedIterator start, OrderedIterator finish, NodeOperation newNode)
Definition: pbori_algo.h:221
bool dd_owns_term_of_indices(NaviType navi, OrderedIterator start, OrderedIterator finish)
Definition: pbori_algo.h:182
#define Cudd_Ref
Definition: prefix_internal.h:157
bool owns_one(NaviType navi)
Test whether the empty set is included.
Definition: pbori_algo.h:318