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