PolyBoRi
|
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