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