glu-2.2: src/cuBdd/cuddBridge.c Source File

00001 
00074 #include "util.h"
00075 #include "cuddInt.h"
00076 
00077 /*---------------------------------------------------------------------------*/
00078 /* Constant declarations                                                     */
00079 /*---------------------------------------------------------------------------*/
00080 
00081 
00082 /*---------------------------------------------------------------------------*/
00083 /* Stucture declarations                                                     */
00084 /*---------------------------------------------------------------------------*/
00085 
00086 
00087 /*---------------------------------------------------------------------------*/
00088 /* Type declarations                                                         */
00089 /*---------------------------------------------------------------------------*/
00090 
00091 
00092 /*---------------------------------------------------------------------------*/
00093 /* Variable declarations                                                     */
00094 /*---------------------------------------------------------------------------*/
00095 
00096 #ifndef lint
00097 static char rcsid[] DD_UNUSED = "$Id: cuddBridge.c,v 1.19 2008/04/25 06:42:55 fabio Exp $";
00098 #endif
00099 
00100 /*---------------------------------------------------------------------------*/
00101 /* Macro declarations                                                        */
00102 /*---------------------------------------------------------------------------*/
00103 
00104 
00105 #ifdef __cplusplus
00106 extern "C" {
00107 #endif
00108 
00111 /*---------------------------------------------------------------------------*/
00112 /* Static function prototypes                                                */
00113 /*---------------------------------------------------------------------------*/
00114 
00115 static DdNode * addBddDoThreshold (DdManager *dd, DdNode *f, DdNode *val);
00116 static DdNode * addBddDoStrictThreshold (DdManager *dd, DdNode *f, DdNode *val);
00117 static DdNode * addBddDoInterval (DdManager *dd, DdNode *f, DdNode *l, DdNode *u);
00118 static DdNode * addBddDoIthBit (DdManager *dd, DdNode *f, DdNode *index);
00119 static DdNode * ddBddToAddRecur (DdManager *dd, DdNode *B);
00120 static DdNode * cuddBddTransferRecur (DdManager *ddS, DdManager *ddD, DdNode *f, st_table *table);
00121 
00124 #ifdef __cplusplus
00125 }
00126 #endif
00127 
00128 
00129 /*---------------------------------------------------------------------------*/
00130 /* Definition of exported functions                                          */
00131 /*---------------------------------------------------------------------------*/
00132 
00133 
00149 DdNode *
00150 Cudd_addBddThreshold(
00151   DdManager * dd,
00152   DdNode * f,
00153   CUDD_VALUE_TYPE  value)
00154 {
00155     DdNode *res;
00156     DdNode *val;
00157     
00158     val = cuddUniqueConst(dd,value);
00159     if (val == NULL) return(NULL);
00160     cuddRef(val);
00161 
00162     do {
00163         dd->reordered = 0;
00164         res = addBddDoThreshold(dd, f, val);
00165     } while (dd->reordered == 1);
00166 
00167     if (res == NULL) {
00168         Cudd_RecursiveDeref(dd, val);
00169         return(NULL);
00170     }
00171     cuddRef(res);
00172     Cudd_RecursiveDeref(dd, val);
00173     cuddDeref(res);
00174     return(res);
00175 
00176 } /* end of Cudd_addBddThreshold */
00177 
00178 
00194 DdNode *
00195 Cudd_addBddStrictThreshold(
00196   DdManager * dd,
00197   DdNode * f,
00198   CUDD_VALUE_TYPE  value)
00199 {
00200     DdNode *res;
00201     DdNode *val;
00202     
00203     val = cuddUniqueConst(dd,value);
00204     if (val == NULL) return(NULL);
00205     cuddRef(val);
00206 
00207     do {
00208         dd->reordered = 0;
00209         res = addBddDoStrictThreshold(dd, f, val);
00210     } while (dd->reordered == 1);
00211 
00212     if (res == NULL) {
00213         Cudd_RecursiveDeref(dd, val);
00214         return(NULL);
00215     }
00216     cuddRef(res);
00217     Cudd_RecursiveDeref(dd, val);
00218     cuddDeref(res);
00219     return(res);
00220 
00221 } /* end of Cudd_addBddStrictThreshold */
00222 
00223 
00239 DdNode *
00240 Cudd_addBddInterval(
00241   DdManager * dd,
00242   DdNode * f,
00243   CUDD_VALUE_TYPE  lower,
00244   CUDD_VALUE_TYPE  upper)
00245 {
00246     DdNode *res;
00247     DdNode *l;
00248     DdNode *u;
00249     
00250     /* Create constant nodes for the interval bounds, so that we can use
00251     ** the global cache.
00252     */
00253     l = cuddUniqueConst(dd,lower);
00254     if (l == NULL) return(NULL);
00255     cuddRef(l);
00256     u = cuddUniqueConst(dd,upper);
00257     if (u == NULL) {
00258         Cudd_RecursiveDeref(dd,l);
00259         return(NULL);
00260     }
00261     cuddRef(u);
00262 
00263     do {
00264         dd->reordered = 0;
00265         res = addBddDoInterval(dd, f, l, u);
00266     } while (dd->reordered == 1);
00267 
00268     if (res == NULL) {
00269         Cudd_RecursiveDeref(dd, l);
00270         Cudd_RecursiveDeref(dd, u);
00271         return(NULL);
00272     }
00273     cuddRef(res);
00274     Cudd_RecursiveDeref(dd, l);
00275     Cudd_RecursiveDeref(dd, u);
00276     cuddDeref(res);
00277     return(res);
00278 
00279 } /* end of Cudd_addBddInterval */
00280 
00281 
00301 DdNode *
00302 Cudd_addBddIthBit(
00303   DdManager * dd,
00304   DdNode * f,
00305   int  bit)
00306 {
00307     DdNode *res;
00308     DdNode *index;
00309     
00310     index = cuddUniqueConst(dd,(CUDD_VALUE_TYPE) bit);
00311     if (index == NULL) return(NULL);
00312     cuddRef(index);
00313 
00314     do {
00315         dd->reordered = 0;
00316         res = addBddDoIthBit(dd, f, index);
00317     } while (dd->reordered == 1);
00318 
00319     if (res == NULL) {
00320         Cudd_RecursiveDeref(dd, index);
00321         return(NULL);
00322     }
00323     cuddRef(res);
00324     Cudd_RecursiveDeref(dd, index);
00325     cuddDeref(res);
00326     return(res);
00327 
00328 } /* end of Cudd_addBddIthBit */
00329 
00330 
00344 DdNode *
00345 Cudd_BddToAdd(
00346   DdManager * dd,
00347   DdNode * B)
00348 {
00349     DdNode *res;
00350 
00351     do {
00352         dd->reordered = 0;
00353         res = ddBddToAddRecur(dd, B);
00354     } while (dd->reordered ==1);
00355     return(res);
00356 
00357 } /* end of Cudd_BddToAdd */
00358 
00359 
00374 DdNode *
00375 Cudd_addBddPattern(
00376   DdManager * dd,
00377   DdNode * f)
00378 {
00379     DdNode *res;
00380     
00381     do {
00382         dd->reordered = 0;
00383         res = cuddAddBddDoPattern(dd, f);
00384     } while (dd->reordered == 1);
00385     return(res);
00386 
00387 } /* end of Cudd_addBddPattern */
00388 
00389 
00404 DdNode *
00405 Cudd_bddTransfer(
00406   DdManager * ddSource,
00407   DdManager * ddDestination,
00408   DdNode * f)
00409 {
00410     DdNode *res;
00411     do {
00412         ddDestination->reordered = 0;
00413         res = cuddBddTransfer(ddSource, ddDestination, f);
00414     } while (ddDestination->reordered == 1);
00415     return(res);
00416 
00417 } /* end of Cudd_bddTransfer */
00418 
00419 
00420 /*---------------------------------------------------------------------------*/
00421 /* Definition of internal functions                                          */
00422 /*---------------------------------------------------------------------------*/
00423 
00424 
00438 DdNode *
00439 cuddBddTransfer(
00440   DdManager * ddS,
00441   DdManager * ddD,
00442   DdNode * f)
00443 {
00444     DdNode *res;
00445     st_table *table = NULL;
00446     st_generator *gen = NULL;
00447     DdNode *key, *value;
00448 
00449     table = st_init_table(st_ptrcmp,st_ptrhash);
00450     if (table == NULL) goto failure;
00451     res = cuddBddTransferRecur(ddS, ddD, f, table);
00452     if (res != NULL) cuddRef(res);
00453 
00454     /* Dereference all elements in the table and dispose of the table.
00455     ** This must be done also if res is NULL to avoid leaks in case of
00456     ** reordering. */
00457     gen = st_init_gen(table);
00458     if (gen == NULL) goto failure;
00459     while (st_gen(gen, &key, &value)) {
00460         Cudd_RecursiveDeref(ddD, value);
00461     }
00462     st_free_gen(gen); gen = NULL;
00463     st_free_table(table); table = NULL;
00464 
00465     if (res != NULL) cuddDeref(res);
00466     return(res);
00467 
00468 failure:
00469     /* No need to free gen because it is always NULL here. */
00470     if (table != NULL) st_free_table(table);
00471     return(NULL);
00472 
00473 } /* end of cuddBddTransfer */
00474 
00475 
00488 DdNode *
00489 cuddAddBddDoPattern(
00490   DdManager * dd,
00491   DdNode * f)
00492 {
00493     DdNode *res, *T, *E;
00494     DdNode *fv, *fvn;
00495     int v;
00496 
00497     statLine(dd);
00498     /* Check terminal case. */
00499     if (cuddIsConstant(f)) {
00500         return(Cudd_NotCond(DD_ONE(dd),f == DD_ZERO(dd)));
00501     }
00502 
00503     /* Check cache. */
00504     res = cuddCacheLookup1(dd,Cudd_addBddPattern,f);
00505     if (res != NULL) return(res);
00506 
00507     /* Recursive step. */
00508     v = f->index;
00509     fv = cuddT(f); fvn = cuddE(f);
00510 
00511     T = cuddAddBddDoPattern(dd,fv);
00512     if (T == NULL) return(NULL);
00513     cuddRef(T);
00514 
00515     E = cuddAddBddDoPattern(dd,fvn);
00516     if (E == NULL) {
00517         Cudd_RecursiveDeref(dd, T);
00518         return(NULL);
00519     }
00520     cuddRef(E);
00521     if (Cudd_IsComplement(T)) {
00522         res = (T == E) ? Cudd_Not(T) : cuddUniqueInter(dd,v,Cudd_Not(T),Cudd_Not(E));
00523         if (res == NULL) {
00524             Cudd_RecursiveDeref(dd, T);
00525             Cudd_RecursiveDeref(dd, E);
00526             return(NULL);
00527         }
00528         res = Cudd_Not(res);
00529     } else {
00530         res = (T == E) ? T : cuddUniqueInter(dd,v,T,E);
00531         if (res == NULL) {
00532             Cudd_RecursiveDeref(dd, T);
00533             Cudd_RecursiveDeref(dd, E);
00534             return(NULL);
00535         }
00536     }
00537     cuddDeref(T);
00538     cuddDeref(E);
00539 
00540     /* Store result. */
00541     cuddCacheInsert1(dd,Cudd_addBddPattern,f,res);
00542 
00543     return(res);
00544 
00545 } /* end of cuddAddBddDoPattern */
00546 
00547 
00548 /*---------------------------------------------------------------------------*/
00549 /* Definition of static functions                                            */
00550 /*---------------------------------------------------------------------------*/
00551 
00552 
00565 static DdNode *
00566 addBddDoThreshold(
00567   DdManager * dd,
00568   DdNode * f,
00569   DdNode * val)
00570 {
00571     DdNode *res, *T, *E;
00572     DdNode *fv, *fvn;
00573     int v;
00574 
00575     statLine(dd);
00576     /* Check terminal case. */
00577     if (cuddIsConstant(f)) {
00578         return(Cudd_NotCond(DD_ONE(dd),cuddV(f) < cuddV(val)));
00579     }
00580 
00581     /* Check cache. */
00582     res = cuddCacheLookup2(dd,addBddDoThreshold,f,val);
00583     if (res != NULL) return(res);
00584 
00585     /* Recursive step. */
00586     v = f->index;
00587     fv = cuddT(f); fvn = cuddE(f);
00588 
00589     T = addBddDoThreshold(dd,fv,val);
00590     if (T == NULL) return(NULL);
00591     cuddRef(T);
00592 
00593     E = addBddDoThreshold(dd,fvn,val);
00594     if (E == NULL) {
00595         Cudd_RecursiveDeref(dd, T);
00596         return(NULL);
00597     }
00598     cuddRef(E);
00599     if (Cudd_IsComplement(T)) {
00600         res = (T == E) ? Cudd_Not(T) : cuddUniqueInter(dd,v,Cudd_Not(T),Cudd_Not(E));
00601         if (res == NULL) {
00602             Cudd_RecursiveDeref(dd, T);
00603             Cudd_RecursiveDeref(dd, E);
00604             return(NULL);
00605         }
00606         res = Cudd_Not(res);
00607     } else {
00608         res = (T == E) ? T : cuddUniqueInter(dd,v,T,E);
00609         if (res == NULL) {
00610             Cudd_RecursiveDeref(dd, T);
00611             Cudd_RecursiveDeref(dd, E);
00612             return(NULL);
00613         }
00614     }
00615     cuddDeref(T);
00616     cuddDeref(E);
00617 
00618     /* Store result. */
00619     cuddCacheInsert2(dd,addBddDoThreshold,f,val,res);
00620 
00621     return(res);
00622 
00623 } /* end of addBddDoThreshold */
00624 
00625 
00638 static DdNode *
00639 addBddDoStrictThreshold(
00640   DdManager * dd,
00641   DdNode * f,
00642   DdNode * val)
00643 {
00644     DdNode *res, *T, *E;
00645     DdNode *fv, *fvn;
00646     int v;
00647 
00648     statLine(dd);
00649     /* Check terminal case. */
00650     if (cuddIsConstant(f)) {
00651         return(Cudd_NotCond(DD_ONE(dd),cuddV(f) <= cuddV(val)));
00652     }
00653 
00654     /* Check cache. */
00655     res = cuddCacheLookup2(dd,addBddDoStrictThreshold,f,val);
00656     if (res != NULL) return(res);
00657 
00658     /* Recursive step. */
00659     v = f->index;
00660     fv = cuddT(f); fvn = cuddE(f);
00661 
00662     T = addBddDoStrictThreshold(dd,fv,val);
00663     if (T == NULL) return(NULL);
00664     cuddRef(T);
00665 
00666     E = addBddDoStrictThreshold(dd,fvn,val);
00667     if (E == NULL) {
00668         Cudd_RecursiveDeref(dd, T);
00669         return(NULL);
00670     }
00671     cuddRef(E);
00672     if (Cudd_IsComplement(T)) {
00673         res = (T == E) ? Cudd_Not(T) : cuddUniqueInter(dd,v,Cudd_Not(T),Cudd_Not(E));
00674         if (res == NULL) {
00675             Cudd_RecursiveDeref(dd, T);
00676             Cudd_RecursiveDeref(dd, E);
00677             return(NULL);
00678         }
00679         res = Cudd_Not(res);
00680     } else {
00681         res = (T == E) ? T : cuddUniqueInter(dd,v,T,E);
00682         if (res == NULL) {
00683             Cudd_RecursiveDeref(dd, T);
00684             Cudd_RecursiveDeref(dd, E);
00685             return(NULL);
00686         }
00687     }
00688     cuddDeref(T);
00689     cuddDeref(E);
00690 
00691     /* Store result. */
00692     cuddCacheInsert2(dd,addBddDoStrictThreshold,f,val,res);
00693 
00694     return(res);
00695 
00696 } /* end of addBddDoStrictThreshold */
00697 
00698 
00711 static DdNode *
00712 addBddDoInterval(
00713   DdManager * dd,
00714   DdNode * f,
00715   DdNode * l,
00716   DdNode * u)
00717 {
00718     DdNode *res, *T, *E;
00719     DdNode *fv, *fvn;
00720     int v;
00721 
00722     statLine(dd);
00723     /* Check terminal case. */
00724     if (cuddIsConstant(f)) {
00725         return(Cudd_NotCond(DD_ONE(dd),cuddV(f) < cuddV(l) || cuddV(f) > cuddV(u)));
00726     }
00727 
00728     /* Check cache. */
00729     res = cuddCacheLookup(dd,DD_ADD_BDD_DO_INTERVAL_TAG,f,l,u);
00730     if (res != NULL) return(res);
00731 
00732     /* Recursive step. */
00733     v = f->index;
00734     fv = cuddT(f); fvn = cuddE(f);
00735 
00736     T = addBddDoInterval(dd,fv,l,u);
00737     if (T == NULL) return(NULL);
00738     cuddRef(T);
00739 
00740     E = addBddDoInterval(dd,fvn,l,u);
00741     if (E == NULL) {
00742         Cudd_RecursiveDeref(dd, T);
00743         return(NULL);
00744     }
00745     cuddRef(E);
00746     if (Cudd_IsComplement(T)) {
00747         res = (T == E) ? Cudd_Not(T) : cuddUniqueInter(dd,v,Cudd_Not(T),Cudd_Not(E));
00748         if (res == NULL) {
00749             Cudd_RecursiveDeref(dd, T);
00750             Cudd_RecursiveDeref(dd, E);
00751             return(NULL);
00752         }
00753         res = Cudd_Not(res);
00754     } else {
00755         res = (T == E) ? T : cuddUniqueInter(dd,v,T,E);
00756         if (res == NULL) {
00757             Cudd_RecursiveDeref(dd, T);
00758             Cudd_RecursiveDeref(dd, E);
00759             return(NULL);
00760         }
00761     }
00762     cuddDeref(T);
00763     cuddDeref(E);
00764 
00765     /* Store result. */
00766     cuddCacheInsert(dd,DD_ADD_BDD_DO_INTERVAL_TAG,f,l,u,res);
00767 
00768     return(res);
00769 
00770 } /* end of addBddDoInterval */
00771 
00772 
00785 static DdNode *
00786 addBddDoIthBit(
00787   DdManager * dd,
00788   DdNode * f,
00789   DdNode * index)
00790 {
00791     DdNode *res, *T, *E;
00792     DdNode *fv, *fvn;
00793     int mask, value;
00794     int v;
00795 
00796     statLine(dd);
00797     /* Check terminal case. */
00798     if (cuddIsConstant(f)) {
00799         mask = 1 << ((int) cuddV(index));
00800         value = (int) cuddV(f);
00801         return(Cudd_NotCond(DD_ONE(dd),(value & mask) == 0));
00802     }
00803 
00804     /* Check cache. */
00805     res = cuddCacheLookup2(dd,addBddDoIthBit,f,index);
00806     if (res != NULL) return(res);
00807 
00808     /* Recursive step. */
00809     v = f->index;
00810     fv = cuddT(f); fvn = cuddE(f);
00811 
00812     T = addBddDoIthBit(dd,fv,index);
00813     if (T == NULL) return(NULL);
00814     cuddRef(T);
00815 
00816     E = addBddDoIthBit(dd,fvn,index);
00817     if (E == NULL) {
00818         Cudd_RecursiveDeref(dd, T);
00819         return(NULL);
00820     }
00821     cuddRef(E);
00822     if (Cudd_IsComplement(T)) {
00823         res = (T == E) ? Cudd_Not(T) : cuddUniqueInter(dd,v,Cudd_Not(T),Cudd_Not(E));
00824         if (res == NULL) {
00825             Cudd_RecursiveDeref(dd, T);
00826             Cudd_RecursiveDeref(dd, E);
00827             return(NULL);
00828         }
00829         res = Cudd_Not(res);
00830     } else {
00831         res = (T == E) ? T : cuddUniqueInter(dd,v,T,E);
00832         if (res == NULL) {
00833             Cudd_RecursiveDeref(dd, T);
00834             Cudd_RecursiveDeref(dd, E);
00835             return(NULL);
00836         }
00837     }
00838     cuddDeref(T);
00839     cuddDeref(E);
00840 
00841     /* Store result. */
00842     cuddCacheInsert2(dd,addBddDoIthBit,f,index,res);
00843 
00844     return(res);
00845 
00846 } /* end of addBddDoIthBit */
00847 
00848 
00861 static DdNode *
00862 ddBddToAddRecur(
00863   DdManager * dd,
00864   DdNode * B)
00865 {
00866     DdNode *one;
00867     DdNode *res, *res1, *T, *E, *Bt, *Be;
00868     int complement = 0;
00869 
00870     statLine(dd);
00871     one = DD_ONE(dd);
00872 
00873     if (Cudd_IsConstant(B)) {
00874         if (B == one) {
00875             res = one;
00876         } else {
00877             res = DD_ZERO(dd);
00878         }
00879         return(res);
00880     }
00881     /* Check visited table */
00882     res = cuddCacheLookup1(dd,ddBddToAddRecur,B);
00883     if (res != NULL) return(res);
00884 
00885     if (Cudd_IsComplement(B)) {
00886         complement = 1;
00887         Bt = cuddT(Cudd_Regular(B));
00888         Be = cuddE(Cudd_Regular(B));
00889     } else {
00890         Bt = cuddT(B);
00891         Be = cuddE(B);
00892     }
00893 
00894     T = ddBddToAddRecur(dd, Bt);
00895     if (T == NULL) return(NULL);
00896     cuddRef(T);
00897 
00898     E = ddBddToAddRecur(dd, Be);
00899     if (E == NULL) {
00900         Cudd_RecursiveDeref(dd, T);
00901         return(NULL);
00902     }
00903     cuddRef(E);
00904 
00905     /* No need to check for T == E, because it is guaranteed not to happen. */
00906     res = cuddUniqueInter(dd, (int) Cudd_Regular(B)->index, T, E);
00907     if (res == NULL) {
00908         Cudd_RecursiveDeref(dd ,T);
00909         Cudd_RecursiveDeref(dd ,E);
00910         return(NULL);
00911     }
00912     cuddDeref(T);
00913     cuddDeref(E);
00914 
00915     if (complement) {
00916         cuddRef(res);
00917         res1 = cuddAddCmplRecur(dd, res);
00918         if (res1 == NULL) {
00919             Cudd_RecursiveDeref(dd, res);
00920             return(NULL);
00921         }
00922         cuddRef(res1);
00923         Cudd_RecursiveDeref(dd, res);
00924         res = res1;
00925         cuddDeref(res);
00926     }
00927 
00928     /* Store result. */
00929     cuddCacheInsert1(dd,ddBddToAddRecur,B,res);
00930 
00931     return(res);
00932 
00933 } /* end of ddBddToAddRecur */
00934 
00935 
00948 static DdNode *
00949 cuddBddTransferRecur(
00950   DdManager * ddS,
00951   DdManager * ddD,
00952   DdNode * f,
00953   st_table * table)
00954 {
00955     DdNode *ft, *fe, *t, *e, *var, *res;
00956     DdNode *one, *zero;
00957     int    index;
00958     int    comple = 0;
00959 
00960     statLine(ddD);
00961     one = DD_ONE(ddD);
00962     comple = Cudd_IsComplement(f);
00963 
00964     /* Trivial cases. */
00965     if (Cudd_IsConstant(f)) return(Cudd_NotCond(one, comple));
00966 
00967     /* Make canonical to increase the utilization of the cache. */
00968     f = Cudd_NotCond(f,comple);
00969     /* Now f is a regular pointer to a non-constant node. */
00970 
00971     /* Check the cache. */
00972     if (st_lookup(table, f, &res))
00973         return(Cudd_NotCond(res,comple));
00974     
00975     /* Recursive step. */
00976     index = f->index;
00977     ft = cuddT(f); fe = cuddE(f);
00978 
00979     t = cuddBddTransferRecur(ddS, ddD, ft, table);
00980     if (t == NULL) {
00981         return(NULL);
00982     }
00983     cuddRef(t);
00984 
00985     e = cuddBddTransferRecur(ddS, ddD, fe, table);
00986     if (e == NULL) {
00987         Cudd_RecursiveDeref(ddD, t);
00988         return(NULL);
00989     }
00990     cuddRef(e);
00991 
00992     zero = Cudd_Not(one);
00993     var = cuddUniqueInter(ddD,index,one,zero);
00994     if (var == NULL) {
00995         Cudd_RecursiveDeref(ddD, t);
00996         Cudd_RecursiveDeref(ddD, e);
00997         return(NULL);
00998     }
00999     res = cuddBddIteRecur(ddD,var,t,e);
01000     if (res == NULL) {
01001         Cudd_RecursiveDeref(ddD, t);
01002         Cudd_RecursiveDeref(ddD, e);
01003         return(NULL);
01004     }
01005     cuddRef(res);
01006     Cudd_RecursiveDeref(ddD, t);
01007     Cudd_RecursiveDeref(ddD, e);
01008 
01009     if (st_add_direct(table, (char *) f, (char *) res) == ST_OUT_OF_MEM) {
01010         Cudd_RecursiveDeref(ddD, res);
01011         return(NULL);
01012     }
01013     return(Cudd_NotCond(res,comple));
01014 
01015 } /* end of cuddBddTransferRecur */
01016