PolyBoRi
|
00001 // -*- c++ -*- 00002 //***************************************************************************** 00055 //***************************************************************************** 00056 00057 // include polybori's definitions 00058 #include "pbori_defs.h" 00059 00060 // get polybori's functionals 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 // template<class NaviType, class SizeType, class ManagerType> 00116 // NaviType 00117 // multiples_of_one_term(NaviType navi, SizeType nmax, ManagerType& man){ 00118 00119 00120 // std::vector<int> indices (Cudd_SupportSize(man,navi)); 00121 // std::vector<int>::iterator iter(indices.begin()); 00122 00123 // NaviType multiples = navi; 00124 00125 // while(!multiples.isConstant()) { 00126 // *iter = *multiples; 00127 // multiples.incrementThen(); 00128 // ++iter; 00129 // } 00130 00131 // std::vector<int>::const_reverse_iterator start(indices.rbegin()), 00132 // finish(indices.rend()); 00133 00134 // // int nmax = dd.nVariables(); 00135 00136 // Cudd_Ref(multiples); 00137 // NaviType emptyset = navi.elseBranch(); 00138 00139 // NaviType tmp; 00140 // SizeType i = nmax-1; 00141 00142 // while(start != finish){ 00143 00144 // while ((idxStart != idxFinish) && (*idxStart > *start)) 00145 // // while(i > *start) { 00146 00147 // tmp = cuddZddGetNode(man, i, multiples, multiples); 00148 // Cudd_Ref(tmp); 00149 // Cudd_Deref(multiples); 00150 // multiples = tmp; 00151 // --i; 00152 // } 00153 // tmp = cuddZddGetNode(man, i, multiples, emptyset); 00154 // Cudd_Ref(tmp); 00155 // Cudd_Deref(multiples); 00156 // multiples = tmp; 00157 // --i; 00158 // ++start; 00159 // } 00160 00161 // return multiples; 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 // std::cout <<"2s "; 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 // See CCuddLastIterator 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 // std::cout <<"TH "<<*thenNavi <<" "<<*elseNavi<< ":"; 00260 00261 bool isReducible = true; 00262 while (isReducible && !thenNavi.isConstant() && !elseNavi.isConstant()){ 00263 00264 while( !thenNavi.isConstant() && (*thenNavi < *elseNavi)) { 00265 // std::cout <<"th "<<*thenNavi <<" "<<*elseNavi<< ":"; 00266 00267 // apply.print(thenNavi); 00268 // apply.print(elseNavi); 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 // std::cout <<""<<isReducible << thenNavi.isConstant()<<std::endl; 00280 00281 elseIdx.push_back(*elseNavi); 00282 00283 // next on last path 00284 elseNavi.incrementThen(); 00285 if( !elseNavi.isConstant() ) { // if still in interior of a path 00286 00287 tmp = elseNavi; // store copy of *this 00288 elseNavi.incrementElse(); // go in direction of last term, if possible 00289 00290 // restore previous value, of else branch was invalid 00291 if( elseNavi.isEmpty() ) 00292 elseNavi = tmp; 00293 00294 } 00295 } 00296 00297 00298 NaviType elseTail, elseMult; 00299 apply.assign(elseTail, elseNavi); 00300 00301 00302 // int initref = ((DdNode*)elseNavi)->ref; 00303 // std::cout << ((DdNode*)elseNavi)->ref <<std::endl; 00304 if (!elseNavi.isConstant()) { 00305 isReducible = false; 00306 elseMult = 00307 indexed_term_multiples(elseTail, idxStart, idxFinish, apply); 00308 // if(elseMult==elseTail) 00309 // Cudd_Deref(elseMult); 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 // std::cerr<< "h1"<<std::endl; 00324 00325 NaviType thenTail, thenMult; 00326 00327 if(!isReducible){ 00328 00329 // if(!thenNavi.isConstant()) 00330 // std::cout << " "<<(*thenNavi)<< " "<< *idxStart<<std::endl; 00331 apply.assign(thenTail, thenNavi); 00333 00334 if (!thenNavi.isConstant()){ 00335 00336 thenMult = 00337 indexed_term_multiples(thenTail, idxStart, idxFinish, apply); 00338 // if(thenMult==thenTail) 00339 // Cudd_Deref(thenMult); 00340 //Cudd_Deref(thenTail);/// 00342 } 00343 else{ 00345 apply.assign(thenMult, thenTail); 00346 } 00347 } 00348 // std::cerr<< "h2"<<std::endl; 00349 // generating elsePath and multiples 00350 ReverseIterator idxIter = idxStart; 00351 const_reverse_iterator start(elseIdx.rbegin()), finish(elseIdx.rend()); 00352 00353 // Cudd_Ref(elseMult); 00354 // std::cout << "isRed"<< isReducible <<std::endl; 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 // std::cerr<< "h3"<<std::endl; 00377 if (isReducible){ 00378 multiples = elseMult; 00379 00380 00382 // Cudd_Ref(elseTail); 00383 //Cudd_Deref(thenTail); 00384 //Cudd_Deref(thenMult); 00385 00386 // std::cerr<< "h4"<<std::endl; 00387 return elseTail; 00388 } 00389 else { 00390 00391 // std::cerr<< "h5"<<std::endl; 00392 const_reverse_iterator start2(thenIdx.rbegin()), finish2(thenIdx.rend()); 00393 ReverseIterator idxIter = idxStart; 00394 00395 // Cudd_Ref(thenMult); 00396 // NaviType printer = thenMult; std::cout<< "thenMult"<<std::endl; 00397 // while(!printer.isConstant()){ 00398 // std::cout<< *printer <<" & "; 00399 // printer.incrementThen(); 00400 // } 00401 if(!thenMult.isConstant()) 00402 while((idxIter != idxFinish) && (*idxIter >= *thenMult) ) 00403 ++idxIter; 00404 00405 00406 // std::cerr<< "h6"<<std::endl; 00407 00408 00409 while(start2 != finish2){ 00410 00411 while((idxIter != idxFinish) && (*idxIter > *start2) ) { 00412 // std::cout<< *idxIter <<" ? "; 00413 apply.multiplesAssign(thenMult, *idxIter); 00414 ++idxIter; 00415 } 00416 apply.productAssign(thenMult, *start2); 00417 // apply.productAssign(thenTail, *start); 00418 if(idxIter != idxFinish) 00419 ++idxIter; 00420 ++start2; 00421 } 00422 00423 00424 apply.replacingUnite(multiples, elseMult, thenMult); 00425 00426 00427 00428 // std::cerr<< "h7"<<std::endl; 00429 // printer = multiples; std::cout<< "mu"<<std::endl; 00430 // while(!printer.isConstant()){ 00431 // // std::cout<< *printer <<" & "; 00432 // printer.incrementThen(); 00433 // } 00434 // std::cout<< std::endl; 00436 // return apply.newNode(navi); 00437 // std::cout << " "<<((DdNode*)thenTail)->ref<<std::endl; 00438 // std::cerr<< "h8"<<std::endl; 00439 00440 apply.kill(elseTail); 00441 apply.kill(thenTail); 00442 00443 00444 return apply.newNode(navi); 00445 } 00446 00447 00448 00449 // // remainder of first term 00450 // while (!thenNavi.isConstant() ){ 00451 // thenIdx.push_back(*thenNavi); 00452 // thenIdx.incrementThen(); 00453 // } 00454 00455 // // remainder of last term 00456 // while (!elseNavi.isConstant()){ 00457 // elseIdx.push_back(*elseNavi); 00458 00459 // elseIdx.incrementThen(); 00460 // if( !elseIdx.isConstant() ) { // if still in interior of a path 00461 00462 // tmp = elseNavi; // store copy of *this 00463 // elseNavi.incrementElse(); // go in direction of last term, if possible 00464 00465 // // restore previous value, of else branch was invalid 00466 // if( elseNavi.isEmpty() ) 00467 // elseNavi = tmp; 00468 // } 00469 // isReducible = false; 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 //Cudd_Deref(thenNode); 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 //DDType 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()) { // Not at end of path 00635 00636 int nlen = apply.length(navi); 00637 00638 if(false&&(nlen == 2)) { 00639 00640 // std::cerr << "hier"<<std::endl; 00641 navi = minimal_of_two_terms(navi, multiples,idxStart, idxEnd, apply); 00642 00643 // std::cerr << "danach"<<std::endl; 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 // int nmax = dd.nVariables(); 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 // else { // Subcase: two proper terms 00727 00728 // thenBr = indexed_term_multiples(thenBr, idxStart, idxEnd, apply); 00729 // elseBr = indexed_term_multiples(elseBr, idxStart, idxEnd, apply); 00730 00731 // } 00732 #endif 00733 } 00734 00735 00736 00737 if(nlen == 1) { // Special case of only one term 00738 // Cudd_Ref(navi); 00739 multiples = indexed_term_multiples(navi, idxStart, idxEnd, apply); 00740 return apply.newNode(navi); 00741 } 00742 00743 00744 // treat else branch 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 // short cut for obvious inclusion 00752 if( (navi.elseBranch() == navi.thenBranch()) || 00753 (elsedd.isConstant() && elsedd.terminalValue()) ){ 00754 multiples = elseMult; 00755 return elsedd; 00756 } 00757 00758 // remove already treated branches 00759 NaviType thenNavi(apply.diff(navi.thenBranch(), elseMult)); 00760 00761 // treat remaining parts of then branch 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 // generate node consisting of all multiples 00769 apply.uniteAssign(thenMult, elseMult); 00770 apply.replacingNode(multiples, *navi, thenMult, elseMult); 00771 00772 // generate result from minimal elements of then and else brach 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