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