00001
00002
00150
00151
00152
00153 #include "pbori_defs.h"
00154
00155
00156 #include "pbori_func.h"
00157 #include "pbori_traits.h"
00158
00159
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()) {
00181 if (navi.terminalValue()){
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()) {
00206 if (navi.terminalValue()){
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()) {
00231 if (navi.terminalValue()){
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
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()) {
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()) {
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 {
00381
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()) {
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
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
00433 template <class, class, class, class, class, class> class CTermIter;
00434
00435
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()) {
00459
00460 DDType elsedd = dd.subset0(*navi);
00461
00462
00463 DDType elseMultiples;
00464 elsedd = dd_minimal_elements(navi.elseBranch(), elsedd, elseMultiples);
00465
00466
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
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
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;
00738 if (cuddIsConstant(Q))
00739 q_top = Q->index;
00740 else
00741 q_top = 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 }
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
