abc70930: src/bdd/cudd/cuddBridge.c Source File

00001 
00047 #include        "util_hack.h"
00048 #include        "cuddInt.h"
00049 
00050 /*---------------------------------------------------------------------------*/
00051 /* Constant declarations                                                     */
00052 /*---------------------------------------------------------------------------*/
00053 
00054 
00055 /*---------------------------------------------------------------------------*/
00056 /* Stucture declarations                                                     */
00057 /*---------------------------------------------------------------------------*/
00058 
00059 
00060 /*---------------------------------------------------------------------------*/
00061 /* Type declarations                                                         */
00062 /*---------------------------------------------------------------------------*/
00063 
00064 
00065 /*---------------------------------------------------------------------------*/
00066 /* Variable declarations                                                     */
00067 /*---------------------------------------------------------------------------*/
00068 
00069 #ifndef lint
00070 static char rcsid[] DD_UNUSED = "$Id: cuddBridge.c,v 1.1.1.1 2003/02/24 22:23:51 wjiang Exp $";
00071 #endif
00072 
00073 /*---------------------------------------------------------------------------*/
00074 /* Macro declarations                                                        */
00075 /*---------------------------------------------------------------------------*/
00076 
00077 
00080 /*---------------------------------------------------------------------------*/
00081 /* Static function prototypes                                                */
00082 /*---------------------------------------------------------------------------*/
00083 
00084 static DdNode * addBddDoThreshold ARGS((DdManager *dd, DdNode *f, DdNode *val));
00085 static DdNode * addBddDoStrictThreshold ARGS((DdManager *dd, DdNode *f, DdNode *val));
00086 static DdNode * addBddDoInterval ARGS((DdManager *dd, DdNode *f, DdNode *l, DdNode *u));
00087 static DdNode * addBddDoIthBit ARGS((DdManager *dd, DdNode *f, DdNode *index));
00088 static DdNode * ddBddToAddRecur ARGS((DdManager *dd, DdNode *B));
00089 static DdNode * cuddBddTransferRecur ARGS((DdManager *ddS, DdManager *ddD, DdNode *f, st_table *table));
00090 
00094 /*---------------------------------------------------------------------------*/
00095 /* Definition of exported functions                                          */
00096 /*---------------------------------------------------------------------------*/
00097 
00098 
00114 DdNode *
00115 Cudd_addBddThreshold(
00116   DdManager * dd,
00117   DdNode * f,
00118   CUDD_VALUE_TYPE  value)
00119 {
00120     DdNode *res;
00121     DdNode *val;
00122     
00123     val = cuddUniqueConst(dd,value);
00124     if (val == NULL) return(NULL);
00125     cuddRef(val);
00126 
00127     do {
00128         dd->reordered = 0;
00129         res = addBddDoThreshold(dd, f, val);
00130     } while (dd->reordered == 1);
00131 
00132     if (res == NULL) {
00133         Cudd_RecursiveDeref(dd, val);
00134         return(NULL);
00135     }
00136     cuddRef(res);
00137     Cudd_RecursiveDeref(dd, val);
00138     cuddDeref(res);
00139     return(res);
00140 
00141 } /* end of Cudd_addBddThreshold */
00142 
00143 
00159 DdNode *
00160 Cudd_addBddStrictThreshold(
00161   DdManager * dd,
00162   DdNode * f,
00163   CUDD_VALUE_TYPE  value)
00164 {
00165     DdNode *res;
00166     DdNode *val;
00167     
00168     val = cuddUniqueConst(dd,value);
00169     if (val == NULL) return(NULL);
00170     cuddRef(val);
00171 
00172     do {
00173         dd->reordered = 0;
00174         res = addBddDoStrictThreshold(dd, f, val);
00175     } while (dd->reordered == 1);
00176 
00177     if (res == NULL) {
00178         Cudd_RecursiveDeref(dd, val);
00179         return(NULL);
00180     }
00181     cuddRef(res);
00182     Cudd_RecursiveDeref(dd, val);
00183     cuddDeref(res);
00184     return(res);
00185 
00186 } /* end of Cudd_addBddStrictThreshold */
00187 
00188 
00204 DdNode *
00205 Cudd_addBddInterval(
00206   DdManager * dd,
00207   DdNode * f,
00208   CUDD_VALUE_TYPE  lower,
00209   CUDD_VALUE_TYPE  upper)
00210 {
00211     DdNode *res;
00212     DdNode *l;
00213     DdNode *u;
00214     
00215     /* Create constant nodes for the interval bounds, so that we can use
00216     ** the global cache.
00217     */
00218     l = cuddUniqueConst(dd,lower);
00219     if (l == NULL) return(NULL);
00220     cuddRef(l);
00221     u = cuddUniqueConst(dd,upper);
00222     if (u == NULL) {
00223         Cudd_RecursiveDeref(dd,l);
00224         return(NULL);
00225     }
00226     cuddRef(u);
00227 
00228     do {
00229         dd->reordered = 0;
00230         res = addBddDoInterval(dd, f, l, u);
00231     } while (dd->reordered == 1);
00232 
00233     if (res == NULL) {
00234         Cudd_RecursiveDeref(dd, l);
00235         Cudd_RecursiveDeref(dd, u);
00236         return(NULL);
00237     }
00238     cuddRef(res);
00239     Cudd_RecursiveDeref(dd, l);
00240     Cudd_RecursiveDeref(dd, u);
00241     cuddDeref(res);
00242     return(res);
00243 
00244 } /* end of Cudd_addBddInterval */
00245 
00246 
00266 DdNode *
00267 Cudd_addBddIthBit(
00268   DdManager * dd,
00269   DdNode * f,
00270   int  bit)
00271 {
00272     DdNode *res;
00273     DdNode *index;
00274     
00275     index = cuddUniqueConst(dd,(CUDD_VALUE_TYPE) bit);
00276     if (index == NULL) return(NULL);
00277     cuddRef(index);
00278 
00279     do {
00280         dd->reordered = 0;
00281         res = addBddDoIthBit(dd, f, index);
00282     } while (dd->reordered == 1);
00283 
00284     if (res == NULL) {
00285         Cudd_RecursiveDeref(dd, index);
00286         return(NULL);
00287     }
00288     cuddRef(res);
00289     Cudd_RecursiveDeref(dd, index);
00290     cuddDeref(res);
00291     return(res);
00292 
00293 } /* end of Cudd_addBddIthBit */
00294 
00295 
00309 DdNode *
00310 Cudd_BddToAdd(
00311   DdManager * dd,
00312   DdNode * B)
00313 {
00314     DdNode *res;
00315 
00316     do {
00317         dd->reordered = 0;
00318         res = ddBddToAddRecur(dd, B);
00319     } while (dd->reordered ==1);
00320     return(res);
00321 
00322 } /* end of Cudd_BddToAdd */
00323 
00324 
00339 DdNode *
00340 Cudd_addBddPattern(
00341   DdManager * dd,
00342   DdNode * f)
00343 {
00344     DdNode *res;
00345     
00346     do {
00347         dd->reordered = 0;
00348         res = cuddAddBddDoPattern(dd, f);
00349     } while (dd->reordered == 1);
00350     return(res);
00351 
00352 } /* end of Cudd_addBddPattern */
00353 
00354 
00369 DdNode *
00370 Cudd_bddTransfer(
00371   DdManager * ddSource,
00372   DdManager * ddDestination,
00373   DdNode * f)
00374 {
00375     DdNode *res;
00376     do {
00377         ddDestination->reordered = 0;
00378         res = cuddBddTransfer(ddSource, ddDestination, f);
00379     } while (ddDestination->reordered == 1);
00380     return(res);
00381 
00382 } /* end of Cudd_bddTransfer */
00383 
00384 
00385 /*---------------------------------------------------------------------------*/
00386 /* Definition of internal functions                                          */
00387 /*---------------------------------------------------------------------------*/
00388 
00389 
00403 DdNode *
00404 cuddBddTransfer(
00405   DdManager * ddS,
00406   DdManager * ddD,
00407   DdNode * f)
00408 {
00409     DdNode *res;
00410     st_table *table = NULL;
00411     st_generator *gen = NULL;
00412     DdNode *key, *value;
00413 
00414     table = st_init_table(st_ptrcmp,st_ptrhash);
00415     if (table == NULL) goto failure;
00416     res = cuddBddTransferRecur(ddS, ddD, f, table);
00417     if (res != NULL) cuddRef(res);
00418 
00419     /* Dereference all elements in the table and dispose of the table.
00420     ** This must be done also if res is NULL to avoid leaks in case of
00421     ** reordering. */
00422     gen = st_init_gen(table);
00423     if (gen == NULL) goto failure;
00424     while (st_gen(gen, (char **) &key, (char **) &value)) {
00425         Cudd_RecursiveDeref(ddD, value);
00426     }
00427     st_free_gen(gen); gen = NULL;
00428     st_free_table(table); table = NULL;
00429 
00430     if (res != NULL) cuddDeref(res);
00431     return(res);
00432 
00433 failure:
00434     if (table != NULL) st_free_table(table);
00435     if (gen != NULL) st_free_gen(gen);
00436     return(NULL);
00437 
00438 } /* end of cuddBddTransfer */
00439 
00440 
00453 DdNode *
00454 cuddAddBddDoPattern(
00455   DdManager * dd,
00456   DdNode * f)
00457 {
00458     DdNode *res, *T, *E;
00459     DdNode *fv, *fvn;
00460     int v;
00461 
00462     statLine(dd);
00463     /* Check terminal case. */
00464     if (cuddIsConstant(f)) {
00465         return(Cudd_NotCond(DD_ONE(dd),f == DD_ZERO(dd)));
00466     }
00467 
00468     /* Check cache. */
00469     res = cuddCacheLookup1(dd,Cudd_addBddPattern,f);
00470     if (res != NULL) return(res);
00471 
00472     /* Recursive step. */
00473     v = f->index;
00474     fv = cuddT(f); fvn = cuddE(f);
00475 
00476     T = cuddAddBddDoPattern(dd,fv);
00477     if (T == NULL) return(NULL);
00478     cuddRef(T);
00479 
00480     E = cuddAddBddDoPattern(dd,fvn);
00481     if (E == NULL) {
00482         Cudd_RecursiveDeref(dd, T);
00483         return(NULL);
00484     }
00485     cuddRef(E);
00486     if (Cudd_IsComplement(T)) {
00487         res = (T == E) ? Cudd_Not(T) : cuddUniqueInter(dd,v,Cudd_Not(T),Cudd_Not(E));
00488         if (res == NULL) {
00489             Cudd_RecursiveDeref(dd, T);
00490             Cudd_RecursiveDeref(dd, E);
00491             return(NULL);
00492         }
00493         res = Cudd_Not(res);
00494     } else {
00495         res = (T == E) ? T : cuddUniqueInter(dd,v,T,E);
00496         if (res == NULL) {
00497             Cudd_RecursiveDeref(dd, T);
00498             Cudd_RecursiveDeref(dd, E);
00499             return(NULL);
00500         }
00501     }
00502     cuddDeref(T);
00503     cuddDeref(E);
00504 
00505     /* Store result. */
00506     cuddCacheInsert1(dd,Cudd_addBddPattern,f,res);
00507 
00508     return(res);
00509 
00510 } /* end of cuddAddBddDoPattern */
00511 
00512 
00513 /*---------------------------------------------------------------------------*/
00514 /* Definition of static functions                                            */
00515 /*---------------------------------------------------------------------------*/
00516 
00517 
00530 static DdNode *
00531 addBddDoThreshold(
00532   DdManager * dd,
00533   DdNode * f,
00534   DdNode * val)
00535 {
00536     DdNode *res, *T, *E;
00537     DdNode *fv, *fvn;
00538     int v;
00539 
00540     statLine(dd);
00541     /* Check terminal case. */
00542     if (cuddIsConstant(f)) {
00543         return(Cudd_NotCond(DD_ONE(dd),cuddV(f) < cuddV(val)));
00544     }
00545 
00546     /* Check cache. */
00547     res = cuddCacheLookup2(dd,addBddDoThreshold,f,val);
00548     if (res != NULL) return(res);
00549 
00550     /* Recursive step. */
00551     v = f->index;
00552     fv = cuddT(f); fvn = cuddE(f);
00553 
00554     T = addBddDoThreshold(dd,fv,val);
00555     if (T == NULL) return(NULL);
00556     cuddRef(T);
00557 
00558     E = addBddDoThreshold(dd,fvn,val);
00559     if (E == NULL) {
00560         Cudd_RecursiveDeref(dd, T);
00561         return(NULL);
00562     }
00563     cuddRef(E);
00564     if (Cudd_IsComplement(T)) {
00565         res = (T == E) ? Cudd_Not(T) : cuddUniqueInter(dd,v,Cudd_Not(T),Cudd_Not(E));
00566         if (res == NULL) {
00567             Cudd_RecursiveDeref(dd, T);
00568             Cudd_RecursiveDeref(dd, E);
00569             return(NULL);
00570         }
00571         res = Cudd_Not(res);
00572     } else {
00573         res = (T == E) ? T : cuddUniqueInter(dd,v,T,E);
00574         if (res == NULL) {
00575             Cudd_RecursiveDeref(dd, T);
00576             Cudd_RecursiveDeref(dd, E);
00577             return(NULL);
00578         }
00579     }
00580     cuddDeref(T);
00581     cuddDeref(E);
00582 
00583     /* Store result. */
00584     cuddCacheInsert2(dd,addBddDoThreshold,f,val,res);
00585 
00586     return(res);
00587 
00588 } /* end of addBddDoThreshold */
00589 
00590 
00603 static DdNode *
00604 addBddDoStrictThreshold(
00605   DdManager * dd,
00606   DdNode * f,
00607   DdNode * val)
00608 {
00609     DdNode *res, *T, *E;
00610     DdNode *fv, *fvn;
00611     int v;
00612 
00613     statLine(dd);
00614     /* Check terminal case. */
00615     if (cuddIsConstant(f)) {
00616         return(Cudd_NotCond(DD_ONE(dd),cuddV(f) <= cuddV(val)));
00617     }
00618 
00619     /* Check cache. */
00620     res = cuddCacheLookup2(dd,addBddDoStrictThreshold,f,val);
00621     if (res != NULL) return(res);
00622 
00623     /* Recursive step. */
00624     v = f->index;
00625     fv = cuddT(f); fvn = cuddE(f);
00626 
00627     T = addBddDoStrictThreshold(dd,fv,val);
00628     if (T == NULL) return(NULL);
00629     cuddRef(T);
00630 
00631     E = addBddDoStrictThreshold(dd,fvn,val);
00632     if (E == NULL) {
00633         Cudd_RecursiveDeref(dd, T);
00634         return(NULL);
00635     }
00636     cuddRef(E);
00637     if (Cudd_IsComplement(T)) {
00638         res = (T == E) ? Cudd_Not(T) : cuddUniqueInter(dd,v,Cudd_Not(T),Cudd_Not(E));
00639         if (res == NULL) {
00640             Cudd_RecursiveDeref(dd, T);
00641             Cudd_RecursiveDeref(dd, E);
00642             return(NULL);
00643         }
00644         res = Cudd_Not(res);
00645     } else {
00646         res = (T == E) ? T : cuddUniqueInter(dd,v,T,E);
00647         if (res == NULL) {
00648             Cudd_RecursiveDeref(dd, T);
00649             Cudd_RecursiveDeref(dd, E);
00650             return(NULL);
00651         }
00652     }
00653     cuddDeref(T);
00654     cuddDeref(E);
00655 
00656     /* Store result. */
00657     cuddCacheInsert2(dd,addBddDoStrictThreshold,f,val,res);
00658 
00659     return(res);
00660 
00661 } /* end of addBddDoStrictThreshold */
00662 
00663 
00676 static DdNode *
00677 addBddDoInterval(
00678   DdManager * dd,
00679   DdNode * f,
00680   DdNode * l,
00681   DdNode * u)
00682 {
00683     DdNode *res, *T, *E;
00684     DdNode *fv, *fvn;
00685     int v;
00686 
00687     statLine(dd);
00688     /* Check terminal case. */
00689     if (cuddIsConstant(f)) {
00690         return(Cudd_NotCond(DD_ONE(dd),cuddV(f) < cuddV(l) || cuddV(f) > cuddV(u)));
00691     }
00692 
00693     /* Check cache. */
00694     res = cuddCacheLookup(dd,DD_ADD_BDD_DO_INTERVAL_TAG,f,l,u);
00695     if (res != NULL) return(res);
00696 
00697     /* Recursive step. */
00698     v = f->index;
00699     fv = cuddT(f); fvn = cuddE(f);
00700 
00701     T = addBddDoInterval(dd,fv,l,u);
00702     if (T == NULL) return(NULL);
00703     cuddRef(T);
00704 
00705     E = addBddDoInterval(dd,fvn,l,u);
00706     if (E == NULL) {
00707         Cudd_RecursiveDeref(dd, T);
00708         return(NULL);
00709     }
00710     cuddRef(E);
00711     if (Cudd_IsComplement(T)) {
00712         res = (T == E) ? Cudd_Not(T) : cuddUniqueInter(dd,v,Cudd_Not(T),Cudd_Not(E));
00713         if (res == NULL) {
00714             Cudd_RecursiveDeref(dd, T);
00715             Cudd_RecursiveDeref(dd, E);
00716             return(NULL);
00717         }
00718         res = Cudd_Not(res);
00719     } else {
00720         res = (T == E) ? T : cuddUniqueInter(dd,v,T,E);
00721         if (res == NULL) {
00722             Cudd_RecursiveDeref(dd, T);
00723             Cudd_RecursiveDeref(dd, E);
00724             return(NULL);
00725         }
00726     }
00727     cuddDeref(T);
00728     cuddDeref(E);
00729 
00730     /* Store result. */
00731     cuddCacheInsert(dd,DD_ADD_BDD_DO_INTERVAL_TAG,f,l,u,res);
00732 
00733     return(res);
00734 
00735 } /* end of addBddDoInterval */
00736 
00737 
00750 static DdNode *
00751 addBddDoIthBit(
00752   DdManager * dd,
00753   DdNode * f,
00754   DdNode * index)
00755 {
00756     DdNode *res, *T, *E;
00757     DdNode *fv, *fvn;
00758     int mask, value;
00759     int v;
00760 
00761     statLine(dd);
00762     /* Check terminal case. */
00763     if (cuddIsConstant(f)) {
00764         mask = 1 << ((int) cuddV(index));
00765         value = (int) cuddV(f);
00766         return(Cudd_NotCond(DD_ONE(dd),(value & mask) == 0));
00767     }
00768 
00769     /* Check cache. */
00770     res = cuddCacheLookup2(dd,addBddDoIthBit,f,index);
00771     if (res != NULL) return(res);
00772 
00773     /* Recursive step. */
00774     v = f->index;
00775     fv = cuddT(f); fvn = cuddE(f);
00776 
00777     T = addBddDoIthBit(dd,fv,index);
00778     if (T == NULL) return(NULL);
00779     cuddRef(T);
00780 
00781     E = addBddDoIthBit(dd,fvn,index);
00782     if (E == NULL) {
00783         Cudd_RecursiveDeref(dd, T);
00784         return(NULL);
00785     }
00786     cuddRef(E);
00787     if (Cudd_IsComplement(T)) {
00788         res = (T == E) ? Cudd_Not(T) : cuddUniqueInter(dd,v,Cudd_Not(T),Cudd_Not(E));
00789         if (res == NULL) {
00790             Cudd_RecursiveDeref(dd, T);
00791             Cudd_RecursiveDeref(dd, E);
00792             return(NULL);
00793         }
00794         res = Cudd_Not(res);
00795     } else {
00796         res = (T == E) ? T : cuddUniqueInter(dd,v,T,E);
00797         if (res == NULL) {
00798             Cudd_RecursiveDeref(dd, T);
00799             Cudd_RecursiveDeref(dd, E);
00800             return(NULL);
00801         }
00802     }
00803     cuddDeref(T);
00804     cuddDeref(E);
00805 
00806     /* Store result. */
00807     cuddCacheInsert2(dd,addBddDoIthBit,f,index,res);
00808 
00809     return(res);
00810 
00811 } /* end of addBddDoIthBit */
00812 
00813 
00826 static DdNode *
00827 ddBddToAddRecur(
00828   DdManager * dd,
00829   DdNode * B)
00830 {
00831     DdNode *one;
00832     DdNode *res, *res1, *T, *E, *Bt, *Be;
00833     int complement = 0;
00834 
00835     statLine(dd);
00836     one = DD_ONE(dd);
00837 
00838     if (Cudd_IsConstant(B)) {
00839         if (B == one) {
00840             res = one;
00841         } else {
00842             res = DD_ZERO(dd);
00843         }
00844         return(res);
00845     }
00846     /* Check visited table */
00847     res = cuddCacheLookup1(dd,ddBddToAddRecur,B);
00848     if (res != NULL) return(res);
00849 
00850     if (Cudd_IsComplement(B)) {
00851         complement = 1;
00852         Bt = cuddT(Cudd_Regular(B));
00853         Be = cuddE(Cudd_Regular(B));
00854     } else {
00855         Bt = cuddT(B);
00856         Be = cuddE(B);
00857     }
00858 
00859     T = ddBddToAddRecur(dd, Bt);
00860     if (T == NULL) return(NULL);
00861     cuddRef(T);
00862 
00863     E = ddBddToAddRecur(dd, Be);
00864     if (E == NULL) {
00865         Cudd_RecursiveDeref(dd, T);
00866         return(NULL);
00867     }
00868     cuddRef(E);
00869 
00870     /* No need to check for T == E, because it is guaranteed not to happen. */
00871     res = cuddUniqueInter(dd, (int) Cudd_Regular(B)->index, T, E);
00872     if (res == NULL) {
00873         Cudd_RecursiveDeref(dd ,T);
00874         Cudd_RecursiveDeref(dd ,E);
00875         return(NULL);
00876     }
00877     cuddDeref(T);
00878     cuddDeref(E);
00879 
00880     if (complement) {
00881         cuddRef(res);
00882         res1 = cuddAddCmplRecur(dd, res);
00883         if (res1 == NULL) {
00884             Cudd_RecursiveDeref(dd, res);
00885             return(NULL);
00886         }
00887         cuddRef(res1);
00888         Cudd_RecursiveDeref(dd, res);
00889         res = res1;
00890         cuddDeref(res);
00891     }
00892 
00893     /* Store result. */
00894     cuddCacheInsert1(dd,ddBddToAddRecur,B,res);
00895 
00896     return(res);
00897 
00898 } /* end of ddBddToAddRecur */
00899 
00900 
00913 static DdNode *
00914 cuddBddTransferRecur(
00915   DdManager * ddS,
00916   DdManager * ddD,
00917   DdNode * f,
00918   st_table * table)
00919 {
00920     DdNode *ft, *fe, *t, *e, *var, *res;
00921     DdNode *one, *zero;
00922     int    index;
00923     int    comple = 0;
00924 
00925     statLine(ddD);
00926     one = DD_ONE(ddD);
00927     comple = Cudd_IsComplement(f);
00928 
00929     /* Trivial cases. */
00930     if (Cudd_IsConstant(f)) return(Cudd_NotCond(one, comple));
00931 
00932     /* Make canonical to increase the utilization of the cache. */
00933     f = Cudd_NotCond(f,comple);
00934     /* Now f is a regular pointer to a non-constant node. */
00935 
00936     /* Check the cache. */
00937     if(st_lookup(table, (char *)f, (char **) &res))
00938         return(Cudd_NotCond(res,comple));
00939     
00940     /* Recursive step. */
00941     index = f->index;
00942     ft = cuddT(f); fe = cuddE(f);
00943 
00944     t = cuddBddTransferRecur(ddS, ddD, ft, table);
00945     if (t == NULL) {
00946         return(NULL);
00947     }
00948     cuddRef(t);
00949 
00950     e = cuddBddTransferRecur(ddS, ddD, fe, table);
00951     if (e == NULL) {
00952         Cudd_RecursiveDeref(ddD, t);
00953         return(NULL);
00954     }
00955     cuddRef(e);
00956 
00957     zero = Cudd_Not(one);
00958     var = cuddUniqueInter(ddD,index,one,zero);
00959     if (var == NULL) {
00960         Cudd_RecursiveDeref(ddD, t);
00961         Cudd_RecursiveDeref(ddD, e);
00962         return(NULL);
00963     }
00964     res = cuddBddIteRecur(ddD,var,t,e);
00965     if (res == NULL) {
00966         Cudd_RecursiveDeref(ddD, t);
00967         Cudd_RecursiveDeref(ddD, e);
00968         return(NULL);
00969     }
00970     cuddRef(res);
00971     Cudd_RecursiveDeref(ddD, t);
00972     Cudd_RecursiveDeref(ddD, e);
00973 
00974     if (st_add_direct(table, (char *) f, (char *) res) == ST_OUT_OF_MEM) {
00975         Cudd_RecursiveDeref(ddD, res);
00976         return(NULL);
00977     }
00978     return(Cudd_NotCond(res,comple));
00979 
00980 } /* end of cuddBddTransferRecur */
00981