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