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