00001
00002
00055
00056
00057
00058 #include "pbori_defs.h"
00059
00060
00061 #include "pbori_func.h"
00062 #include "CCuddNavigator.h"
00063 #ifndef pbori_algo_int_h_
00064 #define pbori_algo_int_h_
00065
00066 BEGIN_NAMESPACE_PBORI
00067
00068
00069
00070 inline void
00071 inc_ref(DdNode* node) {
00072 Cudd_Ref(node);
00073 }
00074
00075 template<class NaviType>
00076 inline void
00077 inc_ref(const NaviType & navi) {
00078 navi.incRef();
00079 }
00080
00081 inline void
00082 dec_ref(DdNode* node) {
00083 Cudd_Deref(node);
00084 }
00085
00086 template<class NaviType>
00087 inline void
00088 dec_ref(const NaviType & navi) {
00089 navi.decRef();
00090 }
00091
00092 inline DdNode*
00093 do_get_node(DdNode* node) {
00094 return node;
00095 }
00096
00097 template<class NaviType>
00098 inline DdNode*
00099 do_get_node(const NaviType & navi) {
00100 return navi.getNode();
00101 }
00102
00103 template <class MgrType>
00104 inline void
00105 recursive_dec_ref(const MgrType& mgr, DdNode* node) {
00106 Cudd_RecursiveDerefZdd(mgr, node);
00107 }
00108
00109 template <class MgrType, class NaviType>
00110 inline void
00111 recursive_dec_ref(const MgrType& mgr, const NaviType & navi) {
00112 navi.recursiveDecRef(mgr);
00113 }
00114
00115
00116
00117
00118
00119
00120
00121
00122
00123
00124
00125
00126
00127
00128
00129
00130
00131
00132
00133
00134
00135
00136
00137
00138
00139
00140
00141
00142
00143
00144
00145
00146
00147
00148
00149
00150
00151
00152
00153
00154
00155
00156
00157
00158
00159
00160
00161
00162
00163
00164
00165 template<class NaviType, class ReverseIterator, class DDOperations>
00166 NaviType
00167 indexed_term_multiples(NaviType navi,
00168 ReverseIterator idxStart, ReverseIterator idxFinish,
00169 const DDOperations& apply){
00170
00171 typedef typename NaviType::value_type idx_type;
00172 typedef typename std::vector<idx_type> vector_type;
00173 typedef typename vector_type::iterator iterator;
00174 typedef typename vector_type::const_reverse_iterator const_reverse_iterator;
00175
00176 vector_type indices(apply.nSupport(navi));
00177 iterator iter(indices.begin());
00178
00179 NaviType multiples = navi;
00180
00181 while(!multiples.isConstant()) {
00182 *iter = *multiples;
00183 multiples.incrementThen();
00184 ++iter;
00185 }
00186
00187 const_reverse_iterator start(indices.rbegin()),
00188 finish(indices.rend());
00189
00190
00191 inc_ref(multiples);
00192
00193 while(start != finish){
00194
00195 while( (idxStart != idxFinish) && (*idxStart > *start) ) {
00196 apply.multiplesAssign(multiples, *idxStart);
00197 ++idxStart;
00198 }
00199 apply.productAssign(multiples, *start);
00200 if(idxStart != idxFinish)
00201 ++idxStart;
00202
00203 ++start;
00204 }
00205
00206 return multiples;
00207 }
00208
00209
00210 template <class NaviType>
00211 bool
00212 is_reducible_by(NaviType first, NaviType second){
00213
00214 while(!second.isConstant()){
00215 while( (!first.isConstant()) && (*first < *second))
00216 first.incrementThen();
00217 if(*first != *second)
00218 return false;
00219 second.incrementThen();
00220 }
00221 return true;
00222 }
00223
00224 template<class NaviType, class ReverseIterator, class DDOperations>
00225 NaviType
00226 minimal_of_two_terms(NaviType navi, NaviType& multiples,
00227 ReverseIterator idxStart, ReverseIterator idxFinish,
00228 const DDOperations& apply){
00229
00230 typedef typename NaviType::value_type idx_type;
00231 typedef typename std::vector<idx_type> vector_type;
00232 typedef typename vector_type::iterator iterator;
00233 typedef typename vector_type::size_type size_type;
00234 typedef typename vector_type::const_reverse_iterator const_reverse_iterator;
00235
00236
00237
00238
00239 size_type nmax = apply.nSupport(navi);
00240 vector_type thenIdx(nmax), elseIdx(nmax);
00241
00242 thenIdx.resize(0);
00243 elseIdx.resize(0);
00244
00245 NaviType thenNavi = navi;
00246 NaviType elseNavi = navi;
00247
00248
00249 NaviType tmp(elseNavi);
00250 elseNavi.incrementElse();
00251
00252 while(!elseNavi.isConstant()){
00253 tmp = elseNavi;
00254 elseNavi.incrementElse();
00255 }
00256 if(elseNavi.isEmpty())
00257 elseNavi = tmp;
00258
00259
00260
00261 bool isReducible = true;
00262 while (isReducible && !thenNavi.isConstant() && !elseNavi.isConstant()){
00263
00264 while( !thenNavi.isConstant() && (*thenNavi < *elseNavi)) {
00265
00266
00267
00268
00269 thenIdx.push_back(*thenNavi);
00270 thenNavi.incrementThen();
00271 }
00272
00273 if(!thenNavi.isConstant() && (*thenNavi == *elseNavi) ){
00274 thenIdx.push_back(*thenNavi);
00275 thenNavi.incrementThen();
00276 }
00277 else
00278 isReducible = false;
00279
00280
00281 elseIdx.push_back(*elseNavi);
00282
00283
00284 elseNavi.incrementThen();
00285 if( !elseNavi.isConstant() ) {
00286
00287 tmp = elseNavi;
00288 elseNavi.incrementElse();
00289
00290
00291 if( elseNavi.isEmpty() )
00292 elseNavi = tmp;
00293
00294 }
00295 }
00296
00297
00298 NaviType elseTail, elseMult;
00299 apply.assign(elseTail, elseNavi);
00300
00301
00302
00303
00304 if (!elseNavi.isConstant()) {
00305 isReducible = false;
00306 elseMult =
00307 indexed_term_multiples(elseTail, idxStart, idxFinish, apply);
00308
00309
00310 }
00311 else {
00314 apply.assign(elseMult, elseTail);
00315 }
00316
00317 NaviType tmp2 = prepend_multiples_wrt_indices(elseMult, *navi,
00318 idxStart, idxFinish, apply);
00319
00320 tmp2.incRef();
00321 elseMult.decRef();
00322 elseMult = tmp2;
00323
00324
00325 NaviType thenTail, thenMult;
00326
00327 if(!isReducible){
00328
00329
00330
00331 apply.assign(thenTail, thenNavi);
00333
00334 if (!thenNavi.isConstant()){
00335
00336 thenMult =
00337 indexed_term_multiples(thenTail, idxStart, idxFinish, apply);
00338
00339
00340
00342 }
00343 else{
00345 apply.assign(thenMult, thenTail);
00346 }
00347 }
00348
00349
00350 ReverseIterator idxIter = idxStart;
00351 const_reverse_iterator start(elseIdx.rbegin()), finish(elseIdx.rend());
00352
00353
00354
00355
00356 if(!elseMult.isConstant())
00357 while((idxIter != idxFinish) && (*idxIter >= *elseMult) )
00358 ++idxIter;
00359
00360 while(start != finish){
00361
00362 while((idxIter != idxFinish) && (*idxIter > *start) ) {
00363
00364 apply.multiplesAssign(elseMult, *idxIter);
00365 ++idxIter;
00366 }
00367 apply.productAssign(elseMult, *start);
00368
00369 if (isReducible)
00370 apply.productAssign(elseTail, *start);
00371
00372 if(idxIter != idxFinish)
00373 ++idxIter;
00374 ++start;
00375 }
00376
00377 if (isReducible){
00378 multiples = elseMult;
00379
00380
00382
00383
00384
00385
00386
00387 return elseTail;
00388 }
00389 else {
00390
00391
00392 const_reverse_iterator start2(thenIdx.rbegin()), finish2(thenIdx.rend());
00393 ReverseIterator idxIter = idxStart;
00394
00395
00396
00397
00398
00399
00400
00401 if(!thenMult.isConstant())
00402 while((idxIter != idxFinish) && (*idxIter >= *thenMult) )
00403 ++idxIter;
00404
00405
00406
00407
00408
00409 while(start2 != finish2){
00410
00411 while((idxIter != idxFinish) && (*idxIter > *start2) ) {
00412
00413 apply.multiplesAssign(thenMult, *idxIter);
00414 ++idxIter;
00415 }
00416 apply.productAssign(thenMult, *start2);
00417
00418 if(idxIter != idxFinish)
00419 ++idxIter;
00420 ++start2;
00421 }
00422
00423
00424 apply.replacingUnite(multiples, elseMult, thenMult);
00425
00426
00427
00428
00429
00430
00431
00432
00433
00434
00436
00437
00438
00439
00440 apply.kill(elseTail);
00441 apply.kill(thenTail);
00442
00443
00444 return apply.newNode(navi);
00445 }
00446
00447
00448
00449
00450
00451
00452
00453
00454
00455
00456
00457
00458
00459
00460
00461
00462
00463
00464
00465
00466
00467
00468
00469
00470
00471
00472
00473
00474 }
00475
00476
00477 template <class NaviType, class SizeType, class ReverseIterator,
00478 class DDOperations>
00479 NaviType
00480 prepend_multiples_wrt_indices(NaviType navi, SizeType minIdx,
00481 ReverseIterator start, ReverseIterator finish,
00482 const DDOperations& apply) {
00483
00484 if (navi.isConstant()){
00485 if (!navi.terminalValue())
00486 return navi;
00487 }
00488 else
00489 while ( (start != finish) && (*start >= *navi) )
00490 ++start;
00491
00492 while( (start != finish) && (*start > minIdx) ){
00493 apply.multiplesAssign(navi, *start);
00494 ++start;
00495 }
00496 return navi;
00497 }
00498
00499 template<class FunctionType, class ManagerType, class NodeType>
00500 void apply_assign_cudd_function(FunctionType func, ManagerType& mgr,
00501 NodeType& first, const NodeType& second) {
00502
00503 NodeType newNode(func(mgr, do_get_node(first), do_get_node(second)));
00504 inc_ref(newNode);
00505 recursive_dec_ref(mgr, first);
00506 first = newNode;
00507 }
00508
00509
00510
00511 template<class FunctionType, class ManagerType, class ResultType,
00512 class NodeType>
00513 void apply_replacing_cudd_function(FunctionType func, ManagerType& mgr,
00514 ResultType& newNode,
00515 const NodeType& first,
00516 const NodeType& second) {
00517
00518 newNode = NodeType(func(mgr, do_get_node(first), do_get_node(second)));
00519 inc_ref(newNode);
00520 recursive_dec_ref(mgr, first);
00521 recursive_dec_ref(mgr, second);
00522 }
00523
00524 template<class FunctionType, class ManagerType, class NodeType>
00525 NodeType apply_cudd_function(FunctionType func, ManagerType& mgr,
00526 const NodeType& first, const NodeType& second) {
00527
00528 NodeType newNode;
00529 newNode = NodeType(func(mgr, do_get_node(first), do_get_node(second)));
00530 inc_ref(newNode);
00531 return newNode;
00532 }
00533
00534 template <class DDType>
00535 class dd_operations;
00536
00537 template<>
00538 class dd_operations<CTypes::dd_type::navigator> {
00539 public:
00540 typedef DdManager* manager_type;
00541 typedef CTypes::dd_type dd_type;
00542 typedef dd_type::navigator navigator;
00543 typedef dd_type::idx_type idx_type;
00544 typedef dd_type::size_type size_type;
00545
00546 dd_operations(manager_type man): mgr(man) {}
00547 void replacingUnite(navigator& newNode,
00548 const navigator& first, const navigator& second) const {
00549
00550 apply_replacing_cudd_function(Cudd_zddUnion, mgr, newNode, first, second);
00551 }
00552
00553 void uniteAssign(navigator& first, const navigator& second) const {
00554 apply_assign_cudd_function(Cudd_zddUnion, mgr, first, second);
00555 }
00556 void diffAssign(navigator& first, const navigator& second) const {
00557 apply_assign_cudd_function(Cudd_zddDiff, mgr, first, second);
00558 }
00559 navigator diff(const navigator& first, const navigator& second) const {
00560 return apply_cudd_function(Cudd_zddDiff, mgr, first, second);
00561 }
00562 void replacingNode(navigator& newNode, idx_type idx,
00563 navigator& first, navigator& second) const {
00564
00565 newNode = navigator(cuddZddGetNode(mgr, idx, first.getNode(),
00566 second.getNode()));
00567 newNode.incRef();
00568 recursive_dec_ref(mgr, first);
00569 recursive_dec_ref(mgr, second);
00570 }
00571
00572 void newNodeAssign(idx_type idx,
00573 navigator& thenNode, const navigator& elseNode) const {
00574 navigator newNode = navigator(cuddZddGetNode(mgr, idx,
00575 thenNode.getNode(),
00576 elseNode.getNode()));
00577 newNode.incRef();
00578
00579 recursive_dec_ref(mgr, thenNode);
00580 thenNode = newNode;
00581 }
00582
00583 void multiplesAssign(navigator& node, idx_type idx) const {
00584 newNodeAssign(idx, node, node);
00585 }
00586
00587 void productAssign(navigator& node, idx_type idx) const {
00588 navigator emptyset = navigator(Cudd_ReadZero(mgr));
00589 newNodeAssign(idx, node, emptyset);
00590 }
00591
00592 void assign(navigator& first, const navigator& second) const {
00593
00594 first = second;
00595 first.incRef();
00596 }
00597 void replace(navigator& first, const navigator& second) const {
00598 recursive_dec_ref(mgr, first);
00599 first = second;
00600 }
00601
00602 size_type nSupport(const navigator& node) const {
00603 return Cudd_SupportSize(mgr, node.getNode());
00604 }
00605 size_type length(const navigator& node) const {
00606 return Cudd_zddCount(mgr, node.getNode());
00607 }
00608
00609 navigator& newNode(navigator& node) const {
00610 node.incRef();
00611 return node;
00612 }
00613
00614 void kill(navigator& node) const {
00615 recursive_dec_ref(mgr, node);
00616 }
00617 protected:
00618 manager_type mgr;
00619 };
00620
00624 template <class NaviType, class DDType2, class ReverseIterator,
00625 class DDOperations>
00626
00627 NaviType
00628 dd_minimal_elements(NaviType navi,DDType2& multiples,
00629 ReverseIterator idxStart, ReverseIterator idxEnd,
00630 const DDOperations& apply) {
00631
00632
00633
00634 if (!navi.isConstant()) {
00635
00636 int nlen = apply.length(navi);
00637
00638 if(false&&(nlen == 2)) {
00639
00640
00641 navi = minimal_of_two_terms(navi, multiples,idxStart, idxEnd, apply);
00642
00643
00644 return navi;
00645
00646 #if 0
00647 multiples = navi;
00648
00649
00650 std::vector<int> indices (apply.nSupport(navi));
00651 std::vector<int>::iterator iter(indices.begin()), iend(indices.end());
00652 bool is_reducible = true;
00653 bool reducible_tested = false;
00654
00655 int used = 0;
00656 NaviType thenBr;
00657 NaviType elseBr;
00658 while( is_reducible&&(!multiples.isConstant())) {
00659 *iter = *multiples;
00660 used++;
00661
00662 thenBr = multiples.thenBranch();
00663 elseBr = multiples.elseBranch();
00664
00665 if((elseBr.isConstant() && elseBr.terminalValue())) {
00666 --iter;
00667 --used;
00668 multiples = elseBr;
00669 }
00670 else if (elseBr.isConstant() && !elseBr.terminalValue())
00671 multiples = thenBr;
00672 else {
00673 if (!reducible_tested){
00674 reducible_tested == true;
00675 is_reducible = is_reducible_by(thenBr, elseBr);
00676 }
00677 if(is_reducible){
00678 --iter;
00679 --used;
00680 }
00681
00682 multiples = elseBr;
00683 }
00684
00685
00686 ++iter;
00687
00688 }
00689
00690
00691
00692 indices.resize(used);
00693
00694 if (is_reducible) {
00695
00696 std::vector<int>::const_reverse_iterator start(indices.rbegin()),
00697 finish(indices.rend());
00698
00699
00700
00701 inc_ref(multiples);
00702
00703
00704 NaviType tmp,tmpnavi;
00705
00706 apply.assign(tmpnavi, multiples);
00707
00708 ReverseIterator idxIter = idxStart;
00709 while(start != finish){
00710
00711 while((idxIter != idxEnd) && (*idxIter > *start) ) {
00712
00713 apply.multiplesAssign(multiples, *idxIter);
00714 ++idxIter;
00715 }
00716 apply.productAssign(multiples, *start);
00717 apply.productAssign(tmpnavi, *start);
00718 if(idxIter != idxEnd)
00719 ++idxIter;
00720 ++start;
00721 }
00722
00723 navi = tmpnavi;
00724 return navi;
00725 }
00726
00727
00728
00729
00730
00731
00732 #endif
00733 }
00734
00735
00736
00737 if(nlen == 1) {
00738
00739 multiples = indexed_term_multiples(navi, idxStart, idxEnd, apply);
00740 return apply.newNode(navi);
00741 }
00742
00743
00744
00745 NaviType elseMult;
00746 NaviType elsedd = dd_minimal_elements(navi.elseBranch(),
00747 elseMult, idxStart, idxEnd, apply);
00748 elseMult = prepend_multiples_wrt_indices(elseMult, *navi,
00749 idxStart, idxEnd, apply);
00750
00751
00752 if( (navi.elseBranch() == navi.thenBranch()) ||
00753 (elsedd.isConstant() && elsedd.terminalValue()) ){
00754 multiples = elseMult;
00755 return elsedd;
00756 }
00757
00758
00759 NaviType thenNavi(apply.diff(navi.thenBranch(), elseMult));
00760
00761
00762 NaviType thenMult;
00763 apply.replace(thenNavi, dd_minimal_elements(thenNavi, thenMult,
00764 idxStart, idxEnd, apply));
00765 thenMult = prepend_multiples_wrt_indices(thenMult, *navi,
00766 idxStart, idxEnd, apply);
00767
00768
00769 apply.uniteAssign(thenMult, elseMult);
00770 apply.replacingNode(multiples, *navi, thenMult, elseMult);
00771
00772
00773 NaviType result;
00774 apply.replacingNode(result, *navi, thenNavi, elsedd);
00775
00776 return result;
00777
00778 }
00779
00780 apply.assign(multiples, navi);
00781
00782 return apply.newNode(navi);
00783 }
00784
00785 END_NAMESPACE_PBORI
00786
00787 #endif