PolyBoRi
pbori_algo.h
Go to the documentation of this file.
1 // -*- c++ -*-
2 //*****************************************************************************
150 //*****************************************************************************
151 
152 // include polybori's definitions
153 #include "pbori_defs.h"
154 
155 // get polybori's functionals
156 #include "pbori_func.h"
157 #include "pbori_traits.h"
158 
159 // temporarily
160 #include "cudd.h"
161 #include "cuddInt.h"
162 #include "CCuddInterface.h"
163 
164 #ifndef pbori_algo_h_
165 #define pbori_algo_h_
166 
168 
169 
171 template< class NaviType, class TermType,
172  class TernaryOperator,
173  class TerminalOperator >
174 TermType
175 dd_backward_transform( NaviType navi, TermType init, TernaryOperator newNode,
176  TerminalOperator terminate ) {
177 
178  TermType result = init;
179 
180  if (navi.isConstant()) { // Reached end of path
181  if (navi.terminalValue()){ // Case of a valid path
182  result = terminate();
183  }
184  }
185  else {
186  result = dd_backward_transform(navi.thenBranch(), init, newNode, terminate);
187  result = newNode(*navi, result,
188  dd_backward_transform(navi.elseBranch(), init, newNode,
189  terminate) );
190  }
191  return result;
192 }
193 
194 
196 template< class NaviType, class TermType, class OutIterator,
197  class ThenBinaryOperator, class ElseBinaryOperator,
198  class TerminalOperator >
199 OutIterator
200 dd_transform( NaviType navi, TermType init, OutIterator result,
201  ThenBinaryOperator then_binop, ElseBinaryOperator else_binop,
202  TerminalOperator terminate ) {
203 
204 
205  if (navi.isConstant()) { // Reached end of path
206  if (navi.terminalValue()){ // Case of a valid path
207  *result = terminate(init);
208  ++result;
209  }
210  }
211  else {
212  result = dd_transform(navi.thenBranch(), then_binop(init, *navi), result,
213  then_binop, else_binop, terminate);
214  result = dd_transform(navi.elseBranch(), else_binop(init, *navi), result,
215  then_binop, else_binop, terminate);
216  }
217  return result;
218 }
219 
222 template< class NaviType, class TermType, class OutIterator,
223  class ThenBinaryOperator, class ElseBinaryOperator,
224  class TerminalOperator, class FirstTermOp >
225 OutIterator
226 dd_transform( NaviType navi, TermType init, OutIterator result,
227  ThenBinaryOperator then_binop, ElseBinaryOperator else_binop,
228  TerminalOperator terminate, FirstTermOp terminate_first ) {
229 
230  if (navi.isConstant()) { // Reached end of path
231  if (navi.terminalValue()){ // Case of a valid path - here leading term
232  *result = terminate_first(init);
233  ++result;
234  }
235  }
236  else {
237  result = dd_transform(navi.thenBranch(), then_binop(init, *navi), result,
238  then_binop, else_binop, terminate, terminate_first);
239  result = dd_transform(navi.elseBranch(), else_binop(init, *navi), result,
240  then_binop, else_binop, terminate);
241  }
242  return result;
243 }
244 
246 template< class NaviType, class TermType, class OutIterator,
247  class ThenBinaryOperator, class ElseBinaryOperator >
248 void
249 dd_transform( const NaviType& navi, const TermType& init,
250  const OutIterator& result,
251  const ThenBinaryOperator& then_binop,
252  const ElseBinaryOperator& else_binop ) {
253 
254  dd_transform(navi, init, result, then_binop, else_binop,
255  project_ith<1>() );
256 }
257 
259 template< class NaviType, class TermType, class OutIterator,
260  class ThenBinaryOperator >
261 void
262 dd_transform( const NaviType& navi, const TermType& init,
263  const OutIterator& result,
264  const ThenBinaryOperator& then_binop ) {
265 
266  dd_transform(navi, init, result, then_binop,
268  project_ith<1>() );
269 }
270 
271 
272 template <class InputIterator, class OutputIterator,
273  class FirstFunction, class UnaryFunction>
274 OutputIterator
275 special_first_transform(InputIterator first, InputIterator last,
276  OutputIterator result,
277  UnaryFunction op, FirstFunction firstop) {
278  InputIterator second(first);
279  if (second != last) {
280  ++second;
281  result = std::transform(first, second, result, firstop);
282  }
283  return std::transform(second, last, result, op);
284 }
285 
286 
288 template <class InputIterator, class Intermediate, class OutputIterator>
289 OutputIterator
290 reversed_inter_copy( InputIterator start, InputIterator finish,
291  Intermediate& inter, OutputIterator output ) {
292 
293  std::copy(start, finish, inter.begin());
294  // force constant
295  return std::copy( const_cast<const Intermediate&>(inter).rbegin(),
296  const_cast<const Intermediate&>(inter).rend(),
297  output );
298 }
299 
302 template <class NaviType>
303 bool
304 dd_on_path(NaviType navi) {
305 
306  if (navi.isConstant())
307  return navi.terminalValue();
308 
309  return dd_on_path(navi.thenBranch()) || dd_on_path(navi.elseBranch());
310 }
311 
314 template <class NaviType, class OrderedIterator>
315 bool
316 dd_owns_term_of_indices(NaviType navi,
317  OrderedIterator start, OrderedIterator finish) {
318 
319  if (!navi.isConstant()) { // Not at end of path
320  bool not_at_end;
321 
322  while( (not_at_end = (start != finish)) && (*start < *navi) )
323  ++start;
324 
325  NaviType elsenode = navi.elseBranch();
326 
327  if (elsenode.isConstant() && elsenode.terminalValue())
328  return true;
329 
330 
331  if (not_at_end){
332 
333  if ( (*start == *navi) &&
334  dd_owns_term_of_indices(navi.thenBranch(), start, finish))
335  return true;
336  else
337  return dd_owns_term_of_indices(elsenode, start, finish);
338  }
339  else {
340 
341  while(!elsenode.isConstant())
342  elsenode.incrementElse();
343  return elsenode.terminalValue();
344  }
345 
346  }
347  return navi.terminalValue();
348 }
349 
353 template <class NaviType, class OrderedIterator, class NodeOperation>
354 NaviType
355 dd_intersect_some_index(NaviType navi,
356  OrderedIterator start, OrderedIterator finish,
357  NodeOperation newNode ) {
358 
359  if (!navi.isConstant()) { // Not at end of path
360  bool not_at_end;
361  while( (not_at_end = (start != finish)) && (*start < *navi) )
362  ++start;
363 
364  if (not_at_end) {
365  NaviType elseNode =
366  dd_intersect_some_index(navi.elseBranch(), start, finish,
367  newNode);
368 
369  if (*start == *navi) {
370 
371  NaviType thenNode =
372  dd_intersect_some_index(navi.thenBranch(), start, finish,
373  newNode);
374 
375  return newNode(*start, navi, thenNode, elseNode);
376  }
377  else
378  return elseNode;
379  }
380  else { // if the start == finish, we only check
381  // validity of the else-only branch
382  while(!navi.isConstant())
383  navi = navi.elseBranch();
384  return newNode(navi);
385  }
386 
387  }
388 
389  return newNode(navi);
390 }
391 
392 
393 
395 template <class NaviType>
396 void
397 dd_print(NaviType navi) {
398 
399  if (!navi.isConstant()) { // Not at end of path
400 
401  std::cout << std::endl<< "idx " << *navi <<" addr "<<
402  ((DdNode*)navi)<<" ref "<<
403  int(Cudd_Regular((DdNode*)navi)->ref) << std::endl;
404 
405  dd_print(navi.thenBranch());
406  dd_print(navi.elseBranch());
407 
408  }
409  else {
410  std::cout << "const isvalid? "<<navi.isValid()<<" addr "
411  <<((DdNode*)navi)<<" ref "<<
412  int(Cudd_Regular((DdNode*)navi)->ref)<<std::endl;
413 
414  }
415 }
416 
417 // Determinine the minimum of the distance between two iterators and limit
418 template <class IteratorType, class SizeType>
419 SizeType
420 limited_distance(IteratorType start, IteratorType finish, SizeType limit) {
421 
422  SizeType result = 0;
423 
424  while ((result < limit) && (start != finish)) {
425  ++start, ++result;
426  }
427 
428  return result;
429 }
430 
431 #if 0
432 // Forward declaration of CTermIter template
433 template <class, class, class, class, class, class> class CTermIter;
434 
435 // Determinine the minimum of the number of terms and limit
436 template <class NaviType, class SizeType>
437 SizeType
438 limited_length(NaviType navi, SizeType limit) {
439 
440 
441  typedef CTermIter<dummy_iterator, NaviType,
442  project_ith<1>, project_ith<1>, project_ith<1, 2>,
443  project_ith<1> >
444  iterator;
445 
446  return limited_distance(iterator(navi), iterator(), limit);
447 }
448 #endif
449 
453 template <class NaviType, class DDType>
454 DDType
455 dd_minimal_elements(NaviType navi, DDType dd, DDType& multiples) {
456 
457 
458  if (!navi.isConstant()) { // Not at end of path
459 
460  DDType elsedd = dd.subset0(*navi);
461 
462 
463  DDType elseMultiples;
464  elsedd = dd_minimal_elements(navi.elseBranch(), elsedd, elseMultiples);
465 
466  // short cut if else and then branche equal or else contains 1
467  if((navi.elseBranch() == navi.thenBranch()) || elsedd.blankness()){
468  multiples = elseMultiples;
469  return elsedd;
470  }
471 
472  NaviType elseNavi = elseMultiples.navigation();
473 
474  int nmax;
475  if (elseNavi.isConstant()){
476  if (elseNavi.terminalValue())
477  nmax = dd.nVariables();
478  else
479  nmax = *navi;
480  }
481  else
482  nmax = *elseNavi;
483 
484 
485  for(int i = nmax-1; i > *navi; --i){
486  elseMultiples.uniteAssign(elseMultiples.change(i));
487  }
488 
489 
490  DDType thendd = dd.subset1(*navi);
491  thendd = thendd.diff(elseMultiples);
492 
493  DDType thenMultiples;
494  thendd = dd_minimal_elements(navi.thenBranch(), thendd, thenMultiples);
495 
496  NaviType thenNavi = thenMultiples.navigation();
497 
498 
499  if (thenNavi.isConstant()){
500  if (thenNavi.terminalValue())
501  nmax = dd.nVariables();
502  else
503  nmax = *navi;
504  }
505  else
506  nmax = *thenNavi;
507 
508 
509  for(int i = nmax-1; i > *navi; --i){
510  thenMultiples.uniteAssign(thenMultiples.change(i));
511  }
512 
513 
514  thenMultiples = thenMultiples.unite(elseMultiples);
515  thenMultiples = thenMultiples.change(*navi);
516 
517 
518  multiples = thenMultiples.unite(elseMultiples);
519  thendd = thendd.change(*navi);
520 
521  DDType result = thendd.unite(elsedd);
522 
523  return result;
524 
525  }
526 
527  multiples = dd;
528  return dd;
529 }
530 
531 template <class MgrType>
532 inline const MgrType&
533 get_mgr_core(const MgrType& rhs) {
534  return rhs;
535 }
536 inline Cudd*
537 get_mgr_core(const Cudd& rhs) {
538  return &const_cast<Cudd&>(rhs);
539 }
540 
542 inline CCuddInterface::mgrcore_ptr
544  return mgr.managerCore();
545 }
546 
548 template<class ManagerType, class ReverseIterator, class MultReverseIterator>
549 typename manager_traits<ManagerType>::dd_base
550 cudd_generate_multiples(const ManagerType& mgr,
551  ReverseIterator start, ReverseIterator finish,
552  MultReverseIterator multStart,
553  MultReverseIterator multFinish) {
554 
555  DdNode* prev( (mgr.getManager())->one );
556 
557  DdNode* zeroNode( (mgr.getManager())->zero );
558 
559  Cudd_Ref(prev);
560  while(start != finish) {
561 
562  while((multStart != multFinish) && (*start < *multStart)) {
563 
564  DdNode* result = cuddUniqueInterZdd( mgr.getManager(), *multStart,
565  prev, prev );
566 
567  Cudd_Ref(result);
568  Cudd_RecursiveDerefZdd(mgr.getManager(), prev);
569 
570  prev = result;
571  ++multStart;
572 
573  };
574 
575  DdNode* result = cuddUniqueInterZdd( mgr.getManager(), *start,
576  prev, zeroNode );
577 
578  Cudd_Ref(result);
579  Cudd_RecursiveDerefZdd(mgr.getManager(), prev);
580 
581  prev = result;
582 
583 
584  if((multStart != multFinish) && (*start == *multStart))
585  ++multStart;
586 
587 
588  ++start;
589  }
590 
591  while(multStart != multFinish) {
592 
593  DdNode* result = cuddUniqueInterZdd( mgr.getManager(), *multStart,
594  prev, prev );
595 
596  Cudd_Ref(result);
597  Cudd_RecursiveDerefZdd(mgr.getManager(), prev);
598 
599  prev = result;
600  ++multStart;
601 
602  };
603 
604  Cudd_Deref(prev);
605 
606  typedef typename manager_traits<ManagerType>::dd_base dd_base;
607  return dd_base(get_mgr_core(mgr), prev);
608  }
609 
610 
611 
613 template<class ManagerType, class ReverseIterator>
614 typename manager_traits<ManagerType>::dd_base
615 cudd_generate_divisors(const ManagerType& mgr,
616  ReverseIterator start, ReverseIterator finish) {
617 
618  typedef typename manager_traits<ManagerType>::dd_base dd_base;
619  DdNode* prev= (mgr.getManager())->one;
620 
621  Cudd_Ref(prev);
622  while(start != finish) {
623 
624  DdNode* result = cuddUniqueInterZdd( mgr.getManager(), *start,
625  prev, prev);
626 
627  Cudd_Ref(result);
628  Cudd_RecursiveDerefZdd(mgr.getManager(), prev);
629 
630  prev = result;
631  ++start;
632  }
633 
634  Cudd_Deref(prev);
636  return dd_base(get_mgr_core(mgr), prev);
637 
638 }
639 
640 
641 template<class Iterator, class SizeType>
642 Iterator
643 bounded_max_element(Iterator start, Iterator finish, SizeType bound){
644 
645  if (*start >= bound)
646  return start;
647 
648  Iterator result(start);
649  if (start != finish)
650  ++start;
651 
652  while (start != finish) {
653  if(*start >= bound)
654  return start;
655  if(*start > *result)
656  result = start;
657  ++start;
658  }
659 
660  return result;
661 }
662 
665 template <class LhsType, class RhsType, class BinaryPredicate>
666 CTypes::comp_type
667 generic_compare_3way(const LhsType& lhs, const RhsType& rhs, BinaryPredicate comp) {
668 
669  if (lhs == rhs)
670  return CTypes::equality;
671 
672  return (comp(lhs, rhs)? CTypes::greater_than: CTypes::less_than);
673 }
674 
675 
676 
677 template <class IteratorLike, class ForwardIteratorTag>
678 IteratorLike
679 increment_iteratorlike(IteratorLike iter, ForwardIteratorTag) {
680 
681  return ++iter;
682 }
683 
684 template <class IteratorLike>
685 IteratorLike
687 
688  return iter.thenBranch();
689 }
690 
691 
692 template <class IteratorLike>
693 IteratorLike
694 increment_iteratorlike(IteratorLike iter) {
695 
696  typedef typename std::iterator_traits<IteratorLike>::iterator_category
697  iterator_category;
698 
699  return increment_iteratorlike(iter, iterator_category());
700 }
701 
702 #ifdef PBORI_LOWLEVEL_XOR
703 
704 // dummy for cuddcache (implemented in pbori_routines.cc)
705 DdNode*
706 pboriCuddZddUnionXor__(DdManager *, DdNode *, DdNode *);
707 
708 
712 template <class MgrType, class NodeType>
713 NodeType
714 pboriCuddZddUnionXor(MgrType zdd, NodeType P, NodeType Q) {
715 
716  int p_top, q_top;
717  NodeType empty = DD_ZERO(zdd), t, e, res;
718  MgrType table = zdd;
719 
720  statLine(zdd);
721 
722  if (P == empty)
723  return(Q);
724  if (Q == empty)
725  return(P);
726  if (P == Q)
727  return(empty);
728 
729  /* Check cache */
730  res = cuddCacheLookup2Zdd(table, pboriCuddZddUnionXor__, P, Q);
731  if (res != NULL)
732  return(res);
733 
734  if (cuddIsConstant(P))
735  p_top = P->index;
736  else
737  p_top = P->index;/* zdd->permZ[P->index]; */
738  if (cuddIsConstant(Q))
739  q_top = Q->index;
740  else
741  q_top = Q->index; /* zdd->permZ[Q->index]; */
742  if (p_top < q_top) {
743  e = pboriCuddZddUnionXor(zdd, cuddE(P), Q);
744  if (e == NULL) return (NULL);
745  Cudd_Ref(e);
746  res = cuddZddGetNode(zdd, P->index, cuddT(P), e);
747  if (res == NULL) {
748  Cudd_RecursiveDerefZdd(table, e);
749  return(NULL);
750  }
751  Cudd_Deref(e);
752  } else if (p_top > q_top) {
753  e = pboriCuddZddUnionXor(zdd, P, cuddE(Q));
754  if (e == NULL) return(NULL);
755  Cudd_Ref(e);
756  res = cuddZddGetNode(zdd, Q->index, cuddT(Q), e);
757  if (res == NULL) {
758  Cudd_RecursiveDerefZdd(table, e);
759  return(NULL);
760  }
761  Cudd_Deref(e);
762  } else {
763  t = pboriCuddZddUnionXor(zdd, cuddT(P), cuddT(Q));
764  if (t == NULL) return(NULL);
765  Cudd_Ref(t);
766  e = pboriCuddZddUnionXor(zdd, cuddE(P), cuddE(Q));
767  if (e == NULL) {
768  Cudd_RecursiveDerefZdd(table, t);
769  return(NULL);
770  }
771  Cudd_Ref(e);
772  res = cuddZddGetNode(zdd, P->index, t, e);
773  if (res == NULL) {
774  Cudd_RecursiveDerefZdd(table, t);
775  Cudd_RecursiveDerefZdd(table, e);
776  return(NULL);
777  }
778  Cudd_Deref(t);
779  Cudd_Deref(e);
780  }
781 
782  cuddCacheInsert2(table, pboriCuddZddUnionXor__, P, Q, res);
783 
784  return(res);
785 } /* end of pboriCuddZddUnionXor */
786 
787 template <class MgrType, class NodeType>
788 NodeType
789 pboriCudd_zddUnionXor(MgrType dd, NodeType P, NodeType Q) {
790 
791  NodeType res;
792  do {
793  dd->reordered = 0;
794  res = pboriCuddZddUnionXor(dd, P, Q);
795  } while (dd->reordered == 1);
796  return(res);
797 }
798 
799 #endif // PBORI_LOWLEVEL_XOR
800 
801 
802 template <class NaviType>
803 bool
804 dd_is_singleton(NaviType navi) {
805 
806  while(!navi.isConstant()) {
807  if (!navi.elseBranch().isEmpty())
808  return false;
809  navi.incrementThen();
810  }
811  return true;
812 }
813 
814 template <class NaviType, class BooleConstant>
815 BooleConstant
816 dd_pair_check(NaviType navi, BooleConstant allowSingleton) {
817 
818  while(!navi.isConstant()) {
819 
820  if (!navi.elseBranch().isEmpty())
821  return dd_is_singleton(navi.elseBranch()) &&
822  dd_is_singleton(navi.thenBranch());
823 
824  navi.incrementThen();
825  }
826  return allowSingleton;//();
827 }
828 
829 
830 template <class NaviType>
831 bool
832 dd_is_singleton_or_pair(NaviType navi) {
833 
834  return dd_pair_check(navi, true);
835 }
836 
837 template <class NaviType>
838 bool
839 dd_is_pair(NaviType navi) {
840 
841  return dd_pair_check(navi, false);
842 }
843 
844 
845 
846 template <class SetType>
847 void combine_sizes(const SetType& bset, double& init) {
848  init += bset.sizeDouble();
849 }
850 
851 template <class SetType>
852 void combine_sizes(const SetType& bset,
853  typename SetType::size_type& init) {
854  init += bset.size();
855 }
856 
857 
858 template <class SizeType, class IdxType, class NaviType, class SetType>
859 SizeType&
860 count_index(SizeType& size, IdxType idx, NaviType navi, const SetType& init) {
861 
862  if (*navi == idx)
863  combine_sizes(SetType(navi.incrementThen(), init.ring()), size);
864 
865  if (*navi < idx) {
866  count_index(size, idx, navi.thenBranch(), init);
867  count_index(size, idx, navi.elseBranch(), init);
868  }
869  return size;
870 }
871 
872 
873 template <class SizeType, class IdxType, class SetType>
874 SizeType&
875 count_index(SizeType& size, IdxType idx, const SetType& bset) {
876 
877  return count_index(size, idx, bset.navigation(), SetType());
878 }
879 
881 
882 #endif