PolyBoRi
pbori_algo_int.h
Go to the documentation of this file.
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