00001
00002
00153
00154
00155
00156 #include "pbori_defs.h"
00157
00158
00159 #include "pbori_func.h"
00160 #include "pbori_traits.h"
00161
00162
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()) {
00184 if (navi.terminalValue()){
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()) {
00209 if (navi.terminalValue()){
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()) {
00234 if (navi.terminalValue()){
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
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()) {
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()) {
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 {
00384
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()) {
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
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
00436 template <class, class, class, class, class, class> class CTermIter;
00437
00438
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()) {
00462
00463 DDType elsedd = dd.subset0(*navi);
00464
00465
00466 DDType elseMultiples;
00467 elsedd = dd_minimal_elements(navi.elseBranch(), elsedd, elseMultiples);
00468
00469
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
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
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;
00740 if (cuddIsConstant(Q))
00741 q_top = Q->index;
00742 else
00743 q_top = 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 }
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