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