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

pbori_algo.h

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

Generated on Thu Feb 10 2011 for PolyBoRi by  doxygen 1.7.1