• Main Page
  • Related Pages
  • Namespaces
  • Classes
  • Files
  • File List
  • File Members

pbori_algo.h

Go to the documentation of this file.
00001 // -*- c++ -*-
00002 //*****************************************************************************
00150 //*****************************************************************************
00151 
00152 // include polybori's definitions
00153 #include "pbori_defs.h"
00154 
00155 // get polybori's functionals
00156 #include "pbori_func.h"
00157 #include "pbori_traits.h"
00158 
00159 // temporarily
00160 #include "cudd.h"
00161 #include "cuddInt.h"
00162 #include "CCuddInterface.h"
00163 
00164 #ifndef pbori_algo_h_
00165 #define pbori_algo_h_
00166 
00167 BEGIN_NAMESPACE_PBORI
00168 
00169 
00171 template< class NaviType, class TermType, 
00172           class TernaryOperator, 
00173           class TerminalOperator >
00174 TermType
00175 dd_backward_transform( NaviType navi, TermType init, TernaryOperator newNode,
00176               TerminalOperator terminate ) {
00177  
00178   TermType result = init;
00179 
00180   if (navi.isConstant()) {      // Reached end of path
00181     if (navi.terminalValue()){   // Case of a valid path
00182       result = terminate();
00183     }
00184   }
00185   else {
00186     result = dd_backward_transform(navi.thenBranch(), init, newNode, terminate);
00187     result = newNode(*navi, result, 
00188                      dd_backward_transform(navi.elseBranch(), init, newNode,
00189                                            terminate) );
00190   }
00191   return result;
00192 }
00193 
00194 
00196 template< class NaviType, class TermType, class OutIterator,
00197           class ThenBinaryOperator, class ElseBinaryOperator, 
00198           class TerminalOperator >
00199 OutIterator
00200 dd_transform( NaviType navi, TermType init, OutIterator result, 
00201               ThenBinaryOperator then_binop, ElseBinaryOperator else_binop,
00202               TerminalOperator terminate ) {
00203  
00204 
00205   if (navi.isConstant()) {      // Reached end of path
00206     if (navi.terminalValue()){   // Case of a valid path
00207       *result = terminate(init);
00208       ++result;
00209     }
00210   }
00211   else {
00212     result = dd_transform(navi.thenBranch(), then_binop(init, *navi), result,
00213                  then_binop, else_binop, terminate);
00214     result = dd_transform(navi.elseBranch(), else_binop(init, *navi), result,
00215                  then_binop, else_binop, terminate);
00216   }
00217   return result;
00218 }
00219 
00222 template< class NaviType, class TermType, class OutIterator,
00223           class ThenBinaryOperator, class ElseBinaryOperator, 
00224           class TerminalOperator, class FirstTermOp >
00225 OutIterator
00226 dd_transform( NaviType navi, TermType init, OutIterator result, 
00227               ThenBinaryOperator then_binop, ElseBinaryOperator else_binop,
00228               TerminalOperator terminate, FirstTermOp terminate_first ) {
00229 
00230   if (navi.isConstant()) {      // Reached end of path
00231     if (navi.terminalValue()){   // Case of a valid path - here leading term
00232       *result = terminate_first(init);
00233       ++result;
00234     }
00235   }
00236   else {
00237     result = dd_transform(navi.thenBranch(), then_binop(init, *navi), result,
00238                  then_binop, else_binop, terminate, terminate_first);
00239     result = dd_transform(navi.elseBranch(), else_binop(init, *navi), result,
00240                  then_binop, else_binop, terminate);
00241   }
00242   return result;
00243 }
00244 
00246 template< class NaviType, class TermType, class OutIterator,
00247           class ThenBinaryOperator, class ElseBinaryOperator >
00248 void
00249 dd_transform( const NaviType& navi, const TermType& init, 
00250               const OutIterator& result, 
00251               const ThenBinaryOperator& then_binop, 
00252               const ElseBinaryOperator& else_binop ) {
00253 
00254   dd_transform(navi, init, result, then_binop, else_binop, 
00255                project_ith<1>() );
00256 }
00257 
00259 template< class NaviType, class TermType, class OutIterator,
00260           class ThenBinaryOperator >
00261 void
00262 dd_transform( const NaviType& navi, const TermType& init, 
00263               const OutIterator& result, 
00264               const ThenBinaryOperator& then_binop ) {
00265 
00266   dd_transform(navi, init, result, then_binop,
00267                project_ith<1, 2>(),
00268                project_ith<1>() );
00269 }
00270 
00271 
00272 template <class InputIterator, class OutputIterator, 
00273           class FirstFunction, class UnaryFunction>
00274 OutputIterator 
00275 special_first_transform(InputIterator first, InputIterator last,
00276                         OutputIterator result, 
00277                          UnaryFunction op, FirstFunction firstop) {
00278   InputIterator second(first);
00279   if (second != last) {
00280     ++second;
00281     result = std::transform(first, second, result, firstop);
00282   }
00283   return std::transform(second, last, result, op);
00284 }
00285 
00286 
00288 template <class InputIterator, class Intermediate, class OutputIterator>
00289 OutputIterator
00290 reversed_inter_copy( InputIterator start, InputIterator finish,
00291                      Intermediate& inter, OutputIterator output ) {
00292 
00293     std::copy(start, finish, inter.begin());
00294     // force constant
00295     return std::copy( const_cast<const Intermediate&>(inter).rbegin(),
00296                       const_cast<const Intermediate&>(inter).rend(), 
00297                       output );
00298 }
00299 
00302 template <class NaviType>
00303 bool
00304 dd_on_path(NaviType navi) {
00305  
00306   if (navi.isConstant()) 
00307     return navi.terminalValue();
00308 
00309   return dd_on_path(navi.thenBranch()) || dd_on_path(navi.elseBranch());
00310 }
00311 
00314 template <class NaviType, class OrderedIterator>
00315 bool
00316 dd_owns_term_of_indices(NaviType navi, 
00317                           OrderedIterator start, OrderedIterator finish) {
00318  
00319   if (!navi.isConstant()) {     // Not at end of path
00320     bool not_at_end;
00321 
00322     while( (not_at_end = (start != finish)) && (*start < *navi) )
00323       ++start;
00324 
00325     NaviType elsenode = navi.elseBranch();
00326 
00327     if (elsenode.isConstant() && elsenode.terminalValue())
00328       return true;
00329       
00330 
00331     if (not_at_end){
00332       
00333       if ( (*start == *navi) && 
00334            dd_owns_term_of_indices(navi.thenBranch(), start, finish))
00335         return true;
00336       else  
00337         return dd_owns_term_of_indices(elsenode, start, finish);
00338     }
00339     else {
00340 
00341       while(!elsenode.isConstant()) 
00342         elsenode.incrementElse();
00343       return elsenode.terminalValue();
00344     }
00345    
00346   }
00347   return navi.terminalValue();
00348 }
00349 
00353 template <class NaviType, class OrderedIterator, class NodeOperation>
00354 NaviType
00355 dd_intersect_some_index(NaviType navi, 
00356                         OrderedIterator start, OrderedIterator finish,
00357                         NodeOperation newNode ) {
00358  
00359   if (!navi.isConstant()) {     // Not at end of path
00360     bool not_at_end;
00361     while( (not_at_end = (start != finish)) && (*start < *navi) )
00362       ++start;
00363 
00364     if (not_at_end) {
00365       NaviType elseNode = 
00366         dd_intersect_some_index(navi.elseBranch(), start, finish, 
00367                                 newNode);
00368   
00369       if (*start == *navi) {
00370 
00371         NaviType thenNode = 
00372           dd_intersect_some_index(navi.thenBranch(), start, finish, 
00373                                   newNode);
00374 
00375         return newNode(*start, navi, thenNode, elseNode); 
00376       }
00377       else
00378         return elseNode;
00379     }
00380     else {                      // if the start == finish, we only check 
00381                                 // validity of the else-only branch 
00382       while(!navi.isConstant()) 
00383         navi = navi.elseBranch();
00384       return newNode(navi);
00385     }
00386 
00387   }
00388 
00389   return newNode(navi);
00390 }
00391 
00392 
00393 
00395 template <class NaviType>
00396 void
00397 dd_print(NaviType navi) {
00398  
00399   if (!navi.isConstant()) {     // Not at end of path
00400  
00401     std::cout << std::endl<< "idx " << *navi <<" addr "<<
00402       ((DdNode*)navi)<<" ref "<<
00403       int(Cudd_Regular((DdNode*)navi)->ref) << std::endl;
00404 
00405     dd_print(navi.thenBranch());
00406     dd_print(navi.elseBranch());
00407 
00408   }
00409   else {
00410     std::cout << "const isvalid? "<<navi.isValid()<<" addr "
00411               <<((DdNode*)navi)<<" ref "<<
00412       int(Cudd_Regular((DdNode*)navi)->ref)<<std::endl;
00413 
00414   }
00415 }
00416 
00417 // Determinine the minimum of the distance between two iterators and limit
00418 template <class IteratorType, class SizeType>
00419 SizeType
00420 limited_distance(IteratorType start, IteratorType finish, SizeType limit) {
00421 
00422   SizeType result = 0;
00423 
00424   while ((result < limit) && (start != finish)) {
00425     ++start, ++result;
00426   }
00427 
00428   return result;
00429 }
00430 
00431 #if 0
00432 // Forward declaration of CTermIter template
00433 template <class, class, class, class, class, class> class CTermIter;
00434 
00435 // Determinine the minimum of the number of terms and limit
00436 template <class NaviType, class SizeType>
00437 SizeType
00438 limited_length(NaviType navi, SizeType limit) {
00439 
00440 
00441   typedef CTermIter<dummy_iterator, NaviType, 
00442                     project_ith<1>, project_ith<1>, project_ith<1, 2>, 
00443     project_ith<1> >
00444   iterator;
00445 
00446   return limited_distance(iterator(navi), iterator(), limit);
00447 }
00448 #endif
00449 
00453 template <class NaviType, class DDType>
00454 DDType
00455 dd_minimal_elements(NaviType navi, DDType dd, DDType& multiples) {
00456 
00457 
00458   if (!navi.isConstant()) {     // Not at end of path
00459 
00460     DDType elsedd = dd.subset0(*navi);
00461 
00462 
00463     DDType elseMultiples;
00464     elsedd = dd_minimal_elements(navi.elseBranch(), elsedd, elseMultiples);
00465 
00466     // short cut if else and then branche equal or else contains 1
00467     if((navi.elseBranch() == navi.thenBranch()) || elsedd.blankness()){
00468       multiples = elseMultiples;
00469       return elsedd;
00470     }
00471 
00472     NaviType elseNavi = elseMultiples.navigation();
00473 
00474     int nmax;
00475     if (elseNavi.isConstant()){
00476       if (elseNavi.terminalValue())
00477         nmax = dd.nVariables();
00478       else
00479         nmax = *navi;
00480     }
00481     else
00482       nmax = *elseNavi;
00483 
00484 
00485     for(int i = nmax-1; i > *navi; --i){
00486       elseMultiples.uniteAssign(elseMultiples.change(i)); 
00487     }
00488 
00489 
00490     DDType thendd = dd.subset1(*navi);
00491     thendd = thendd.diff(elseMultiples);
00492 
00493     DDType thenMultiples;
00494     thendd = dd_minimal_elements(navi.thenBranch(), thendd, thenMultiples); 
00495  
00496     NaviType thenNavi = thenMultiples.navigation();
00497 
00498 
00499     if (thenNavi.isConstant()){
00500       if (thenNavi.terminalValue())
00501         nmax =  dd.nVariables();
00502       else
00503         nmax = *navi;
00504     }
00505     else
00506       nmax = *thenNavi;
00507 
00508 
00509     for(int i = nmax-1; i > *navi; --i){
00510       thenMultiples.uniteAssign(thenMultiples.change(i)); 
00511     }
00512 
00513 
00514     thenMultiples = thenMultiples.unite(elseMultiples);
00515     thenMultiples = thenMultiples.change(*navi);
00516 
00517 
00518     multiples = thenMultiples.unite(elseMultiples);
00519     thendd = thendd.change(*navi);
00520 
00521     DDType result =  thendd.unite(elsedd);
00522 
00523     return result;
00524 
00525   }
00526 
00527   multiples = dd;
00528   return dd;
00529 }
00530 
00531 template <class MgrType>
00532 inline const MgrType&
00533 get_mgr_core(const MgrType& rhs) { 
00534   return rhs;
00535 }
00536 inline Cudd*
00537 get_mgr_core(const Cudd& rhs) { 
00538   return &const_cast<Cudd&>(rhs);
00539 }
00540 
00542 inline CCuddInterface::mgrcore_ptr
00543 get_mgr_core(const CCuddInterface& mgr) {
00544   return mgr.managerCore();
00545 }
00546 
00548 template<class ManagerType, class ReverseIterator, class MultReverseIterator>
00549 typename manager_traits<ManagerType>::dd_base
00550 cudd_generate_multiples(const ManagerType& mgr, 
00551                         ReverseIterator start, ReverseIterator finish,
00552                         MultReverseIterator multStart, 
00553                         MultReverseIterator multFinish) {
00554 
00555     DdNode* prev( (mgr.getManager())->one );
00556 
00557     DdNode* zeroNode( (mgr.getManager())->zero ); 
00558 
00559     Cudd_Ref(prev);
00560     while(start != finish) {
00561 
00562       while((multStart != multFinish) && (*start < *multStart)) {
00563 
00564         DdNode* result = cuddUniqueInterZdd( mgr.getManager(), *multStart,
00565                                              prev, prev );
00566 
00567         Cudd_Ref(result);
00568         Cudd_RecursiveDerefZdd(mgr.getManager(), prev);
00569 
00570         prev = result;
00571         ++multStart;
00572 
00573       };
00574 
00575       DdNode* result = cuddUniqueInterZdd( mgr.getManager(), *start,
00576                                            prev, zeroNode );
00577 
00578       Cudd_Ref(result);
00579       Cudd_RecursiveDerefZdd(mgr.getManager(), prev);
00580 
00581       prev = result;
00582 
00583 
00584       if((multStart != multFinish) && (*start == *multStart))
00585         ++multStart;
00586 
00587 
00588       ++start;
00589     }
00590 
00591     while(multStart != multFinish) {
00592 
00593       DdNode* result = cuddUniqueInterZdd( mgr.getManager(), *multStart,
00594                                            prev, prev );
00595 
00596       Cudd_Ref(result);
00597       Cudd_RecursiveDerefZdd(mgr.getManager(), prev);
00598 
00599       prev = result;
00600       ++multStart;
00601 
00602     };
00603 
00604     Cudd_Deref(prev);
00605 
00606     typedef typename manager_traits<ManagerType>::dd_base dd_base;
00607     return dd_base(get_mgr_core(mgr), prev);
00608   }
00609 
00610 
00611 
00613 template<class ManagerType, class ReverseIterator>
00614 typename manager_traits<ManagerType>::dd_base
00615 cudd_generate_divisors(const ManagerType& mgr, 
00616                        ReverseIterator start, ReverseIterator finish) {
00617 
00618   typedef typename manager_traits<ManagerType>::dd_base dd_base;
00619     DdNode* prev= (mgr.getManager())->one;
00620 
00621     Cudd_Ref(prev);
00622     while(start != finish) {
00623  
00624       DdNode* result = cuddUniqueInterZdd( mgr.getManager(), *start,
00625                                            prev, prev);
00626 
00627       Cudd_Ref(result);
00628       Cudd_RecursiveDerefZdd(mgr.getManager(), prev);
00629  
00630       prev = result;
00631       ++start;
00632     }
00633 
00634     Cudd_Deref(prev);
00636       return dd_base(get_mgr_core(mgr), prev);
00637 
00638 }
00639 
00640 
00641 template<class Iterator, class SizeType>
00642 Iterator
00643 bounded_max_element(Iterator start, Iterator finish, SizeType bound){
00644 
00645   if (*start >= bound)
00646     return start;
00647 
00648   Iterator result(start);
00649   if (start != finish)
00650     ++start;
00651 
00652   while (start != finish) {
00653     if(*start >= bound)
00654       return start;
00655     if(*start > *result)
00656       result = start;
00657     ++start;
00658   }
00659 
00660   return result;
00661 }
00662 
00665 template <class LhsType, class RhsType, class BinaryPredicate>
00666 CTypes::comp_type
00667 generic_compare_3way(const LhsType& lhs, const RhsType& rhs, BinaryPredicate comp) {
00668 
00669   if (lhs == rhs)
00670     return CTypes::equality;
00671 
00672   return (comp(lhs, rhs)?  CTypes::greater_than: CTypes::less_than);
00673 }
00674 
00675 
00676 
00677 template <class IteratorLike, class ForwardIteratorTag>
00678 IteratorLike 
00679 increment_iteratorlike(IteratorLike iter, ForwardIteratorTag) {
00680 
00681   return ++iter;
00682 }
00683 
00684 template <class IteratorLike>
00685 IteratorLike 
00686 increment_iteratorlike(IteratorLike iter, navigator_tag) {
00687 
00688   return iter.thenBranch();
00689 }
00690 
00691 
00692 template <class IteratorLike>
00693 IteratorLike 
00694 increment_iteratorlike(IteratorLike iter) {
00695 
00696   typedef typename std::iterator_traits<IteratorLike>::iterator_category
00697     iterator_category;
00698 
00699   return increment_iteratorlike(iter, iterator_category());
00700 }
00701 
00702 #ifdef PBORI_LOWLEVEL_XOR 
00703 
00704 // dummy for cuddcache (implemented in pbori_routines.cc)
00705 DdNode* 
00706 pboriCuddZddUnionXor__(DdManager *, DdNode *, DdNode *);
00707 
00708 
00712 template <class MgrType, class NodeType>
00713 NodeType
00714 pboriCuddZddUnionXor(MgrType zdd, NodeType P, NodeType Q) {
00715 
00716   int           p_top, q_top;
00717   NodeType empty = DD_ZERO(zdd), t, e, res;
00718   MgrType table = zdd;
00719   
00720   statLine(zdd);
00721   
00722   if (P == empty)
00723     return(Q); 
00724   if (Q == empty)
00725     return(P);
00726   if (P == Q)
00727     return(empty);
00728 
00729   /* Check cache */
00730   res = cuddCacheLookup2Zdd(table, pboriCuddZddUnionXor__, P, Q);
00731   if (res != NULL)
00732     return(res);
00733   
00734   if (cuddIsConstant(P))
00735     p_top = P->index;
00736   else
00737     p_top = P->index;/* zdd->permZ[P->index]; */
00738   if (cuddIsConstant(Q))
00739     q_top = Q->index;
00740   else
00741     q_top = Q->index; /* zdd->permZ[Q->index]; */
00742   if (p_top < q_top) {
00743     e = pboriCuddZddUnionXor(zdd, cuddE(P), Q);
00744     if (e == NULL) return (NULL);
00745     Cudd_Ref(e);
00746     res = cuddZddGetNode(zdd, P->index, cuddT(P), e);
00747     if (res == NULL) {
00748       Cudd_RecursiveDerefZdd(table, e);
00749       return(NULL);
00750     }
00751     Cudd_Deref(e);
00752   } else if (p_top > q_top) {
00753     e = pboriCuddZddUnionXor(zdd, P, cuddE(Q));
00754     if (e == NULL) return(NULL);
00755     Cudd_Ref(e);
00756     res = cuddZddGetNode(zdd, Q->index, cuddT(Q), e);
00757     if (res == NULL) {
00758       Cudd_RecursiveDerefZdd(table, e);
00759       return(NULL);
00760     }
00761     Cudd_Deref(e);
00762   } else {
00763     t = pboriCuddZddUnionXor(zdd, cuddT(P), cuddT(Q));
00764     if (t == NULL) return(NULL);
00765     Cudd_Ref(t);
00766     e = pboriCuddZddUnionXor(zdd, cuddE(P), cuddE(Q));
00767     if (e == NULL) {
00768       Cudd_RecursiveDerefZdd(table, t);
00769       return(NULL);
00770     }
00771     Cudd_Ref(e);
00772     res = cuddZddGetNode(zdd, P->index, t, e);
00773     if (res == NULL) {
00774       Cudd_RecursiveDerefZdd(table, t);
00775       Cudd_RecursiveDerefZdd(table, e);
00776       return(NULL);
00777     }
00778     Cudd_Deref(t);
00779     Cudd_Deref(e);
00780   }
00781   
00782   cuddCacheInsert2(table, pboriCuddZddUnionXor__, P, Q, res);
00783   
00784   return(res);
00785 } /* end of pboriCuddZddUnionXor */
00786 
00787 template <class MgrType, class NodeType>
00788 NodeType
00789 pboriCudd_zddUnionXor(MgrType dd, NodeType P, NodeType Q) {
00790 
00791   NodeType res;
00792   do {
00793     dd->reordered = 0;
00794     res = pboriCuddZddUnionXor(dd, P, Q);
00795     } while (dd->reordered == 1);
00796   return(res);
00797 }
00798 
00799 #endif // PBORI_LOWLEVEL_XOR 
00800 
00801 
00802 template <class NaviType>
00803 bool
00804 dd_is_singleton(NaviType navi) {
00805 
00806   while(!navi.isConstant()) {
00807     if (!navi.elseBranch().isEmpty())
00808       return false;
00809     navi.incrementThen();
00810   }
00811   return true;
00812 }
00813 
00814 template <class NaviType, class BooleConstant>
00815 BooleConstant
00816 dd_pair_check(NaviType navi, BooleConstant allowSingleton) {
00817 
00818   while(!navi.isConstant()) {
00819 
00820     if (!navi.elseBranch().isEmpty())
00821       return dd_is_singleton(navi.elseBranch()) && 
00822         dd_is_singleton(navi.thenBranch());
00823 
00824     navi.incrementThen();
00825   }
00826   return allowSingleton;//();
00827 }
00828 
00829 
00830 template <class NaviType>
00831 bool
00832 dd_is_singleton_or_pair(NaviType navi) {
00833 
00834   return dd_pair_check(navi, true);
00835 }
00836 
00837 template <class NaviType>
00838 bool
00839 dd_is_pair(NaviType navi) {
00840 
00841   return dd_pair_check(navi, false);
00842 }
00843 
00844 
00845 
00846 template <class SetType>
00847 void combine_sizes(const SetType& bset, double& init) {
00848   init += bset.sizeDouble();
00849 }
00850 
00851 template <class SetType>
00852 void combine_sizes(const SetType& bset, 
00853                    typename SetType::size_type& init) {
00854   init += bset.size();
00855 }
00856 
00857 
00858 template <class SizeType, class IdxType, class NaviType, class SetType>
00859 SizeType&
00860 count_index(SizeType& size, IdxType idx, NaviType navi, const SetType& init) {
00861 
00862   if (*navi == idx)
00863     combine_sizes(SetType(navi.incrementThen(), init.ring()), size);
00864 
00865   if (*navi < idx) {
00866     count_index(size, idx, navi.thenBranch(), init);
00867     count_index(size, idx, navi.elseBranch(), init);
00868   }
00869   return size;
00870 }
00871 
00872 
00873 template <class SizeType, class IdxType, class SetType>
00874 SizeType&
00875 count_index(SizeType& size, IdxType idx, const SetType& bset) {
00876 
00877   return count_index(size, idx, bset.navigation(), SetType());
00878 }
00879 
00880 END_NAMESPACE_PBORI
00881 
00882 #endif

Generated on Thu Oct 21 2010 06:56:31 for PolyBoRi by  doxygen 1.7.1