src/bdd/cudd/cuddAddApply.c File Reference

#include "util_hack.h"
#include "cuddInt.h"
Include dependency graph for cuddAddApply.c:

Go to the source code of this file.

Functions

DdNode * Cudd_addApply (DdManager *dd, DdNode *(*op)(DdManager *, DdNode **, DdNode **), DdNode *f, DdNode *g)
DdNode * Cudd_addPlus (DdManager *dd, DdNode **f, DdNode **g)
DdNode * Cudd_addTimes (DdManager *dd, DdNode **f, DdNode **g)
DdNode * Cudd_addThreshold (DdManager *dd, DdNode **f, DdNode **g)
DdNode * Cudd_addSetNZ (DdManager *dd, DdNode **f, DdNode **g)
DdNode * Cudd_addDivide (DdManager *dd, DdNode **f, DdNode **g)
DdNode * Cudd_addMinus (DdManager *dd, DdNode **f, DdNode **g)
DdNode * Cudd_addMinimum (DdManager *dd, DdNode **f, DdNode **g)
DdNode * Cudd_addMaximum (DdManager *dd, DdNode **f, DdNode **g)
DdNode * Cudd_addOneZeroMaximum (DdManager *dd, DdNode **f, DdNode **g)
DdNode * Cudd_addDiff (DdManager *dd, DdNode **f, DdNode **g)
DdNode * Cudd_addAgreement (DdManager *dd, DdNode **f, DdNode **g)
DdNode * Cudd_addOr (DdManager *dd, DdNode **f, DdNode **g)
DdNode * Cudd_addNand (DdManager *dd, DdNode **f, DdNode **g)
DdNode * Cudd_addNor (DdManager *dd, DdNode **f, DdNode **g)
DdNode * Cudd_addXor (DdManager *dd, DdNode **f, DdNode **g)
DdNode * Cudd_addXnor (DdManager *dd, DdNode **f, DdNode **g)
DdNode * Cudd_addMonadicApply (DdManager *dd, DdNode *(*op)(DdManager *, DdNode *), DdNode *f)
DdNode * Cudd_addLog (DdManager *dd, DdNode *f)
DdNode * cuddAddApplyRecur (DdManager *dd, DdNode *(*op)(DdManager *, DdNode **, DdNode **), DdNode *f, DdNode *g)
DdNode * cuddAddMonadicApplyRecur (DdManager *dd, DdNode *(*op)(DdManager *, DdNode *), DdNode *f)

Variables

static char rcsid[] DD_UNUSED = "$Id: cuddAddApply.c,v 1.1.1.1 2003/02/24 22:23:50 wjiang Exp $"

Function Documentation

DdNode* Cudd_addAgreement ( DdManager *  dd,
DdNode **  f,
DdNode **  g 
)

Function********************************************************************

Synopsis [f if f==g; background if f!=g.]

Description [Returns NULL if not a terminal case; f op g otherwise, where f op g is f if f==g; background if f!=g.]

SideEffects [None]

SeeAlso [Cudd_addApply]

Definition at line 520 of file cuddAddApply.c.

00524 {
00525     DdNode *F, *G;
00526 
00527     F = *f; G = *g;
00528     if (F == G) return(F);
00529     if (F == dd->background) return(F);
00530     if (G == dd->background) return(G);
00531     if (cuddIsConstant(F) && cuddIsConstant(G)) return(dd->background);
00532     return(NULL);
00533 
00534 } /* end of Cudd_addAgreement */

DdNode* Cudd_addApply ( DdManager *  dd,
DdNode *(*)(DdManager *, DdNode **, DdNode **)  op,
DdNode *  f,
DdNode *  g 
)

AutomaticStart AutomaticEnd Function********************************************************************

Synopsis [Applies op to the corresponding discriminants of f and g.]

Description [Applies op to the corresponding discriminants of f and g. Returns a pointer to the result if succssful; NULL otherwise.]

SideEffects [None]

SeeAlso [Cudd_addMonadicApply Cudd_addPlus Cudd_addTimes Cudd_addThreshold Cudd_addSetNZ Cudd_addDivide Cudd_addMinus Cudd_addMinimum Cudd_addMaximum Cudd_addOneZeroMaximum Cudd_addDiff Cudd_addAgreement Cudd_addOr Cudd_addNand Cudd_addNor Cudd_addXor Cudd_addXnor]

Definition at line 107 of file cuddAddApply.c.

00112 {
00113     DdNode *res;
00114 
00115     do {
00116         dd->reordered = 0;
00117         res = cuddAddApplyRecur(dd,op,f,g);
00118     } while (dd->reordered == 1);
00119     return(res);
00120 
00121 } /* end of Cudd_addApply */

DdNode* Cudd_addDiff ( DdManager *  dd,
DdNode **  f,
DdNode **  g 
)

Function********************************************************************

Synopsis [Returns plusinfinity if f=g; returns min(f,g) if f!=g.]

Description [Returns NULL if not a terminal case; f op g otherwise, where f op g is plusinfinity if f=g; min(f,g) if f!=g.]

SideEffects [None]

SeeAlso [Cudd_addApply]

Definition at line 480 of file cuddAddApply.c.

00484 {
00485     DdNode *F, *G;
00486 
00487     F = *f; G = *g;
00488     if (F == G) return(DD_PLUS_INFINITY(dd));
00489     if (F == DD_PLUS_INFINITY(dd)) return(G);
00490     if (G == DD_PLUS_INFINITY(dd)) return(F);
00491     if (cuddIsConstant(F) && cuddIsConstant(G)) {
00492         if (cuddV(F) != cuddV(G)) {
00493             if (cuddV(F) < cuddV(G)) {
00494                 return(F);
00495             } else {
00496                 return(G);
00497             }
00498         } else {
00499             return(DD_PLUS_INFINITY(dd));
00500         }
00501     }
00502     return(NULL);
00503 
00504 } /* end of Cudd_addDiff */

DdNode* Cudd_addDivide ( DdManager *  dd,
DdNode **  f,
DdNode **  g 
)

Function********************************************************************

Synopsis [Integer and floating point division.]

Description [Integer and floating point division. Returns NULL if not a terminal case; f / g otherwise.]

SideEffects [None]

SeeAlso [Cudd_addApply]

Definition at line 281 of file cuddAddApply.c.

00285 {
00286     DdNode *res;
00287     DdNode *F, *G;
00288     CUDD_VALUE_TYPE value;
00289 
00290     F = *f; G = *g;
00291     /* We would like to use F == G -> F/G == 1, but F and G may
00292     ** contain zeroes. */
00293     if (F == DD_ZERO(dd)) return(DD_ZERO(dd));
00294     if (G == DD_ONE(dd)) return(F);
00295     if (cuddIsConstant(F) && cuddIsConstant(G)) {
00296         value = cuddV(F)/cuddV(G);
00297         res = cuddUniqueConst(dd,value);
00298         return(res);
00299     }
00300     return(NULL);
00301 
00302 } /* end of Cudd_addDivide */

DdNode* Cudd_addLog ( DdManager *  dd,
DdNode *  f 
)

Function********************************************************************

Synopsis [Natural logarithm of an ADD.]

Description [Natural logarithm of an ADDs. Returns NULL if not a terminal case; log(f) otherwise. The discriminants of f must be positive double's.]

SideEffects [None]

SeeAlso [Cudd_addMonadicApply]

Definition at line 746 of file cuddAddApply.c.

00749 {
00750     if (cuddIsConstant(f)) {
00751         CUDD_VALUE_TYPE value = log(cuddV(f));
00752         DdNode *res = cuddUniqueConst(dd,value);
00753         return(res);
00754     }
00755     return(NULL);
00756 
00757 } /* end of Cudd_addLog */

DdNode* Cudd_addMaximum ( DdManager *  dd,
DdNode **  f,
DdNode **  g 
)

Function********************************************************************

Synopsis [Integer and floating point max.]

Description [Integer and floating point max for Cudd_addApply. Returns NULL if not a terminal case; max(f,g) otherwise.]

SideEffects [None]

SeeAlso [Cudd_addApply]

Definition at line 399 of file cuddAddApply.c.

00403 {
00404     DdNode *F, *G;
00405 
00406     F = *f; G = *g;
00407     if (F == G) return(F);
00408     if (F == DD_MINUS_INFINITY(dd)) return(G);
00409     if (G == DD_MINUS_INFINITY(dd)) return(F);
00410 #if 0
00411     /* These special cases probably do not pay off. */
00412     if (F == DD_PLUS_INFINITY(dd)) return(F);
00413     if (G == DD_PLUS_INFINITY(dd)) return(G);
00414 #endif
00415     if (cuddIsConstant(F) && cuddIsConstant(G)) {
00416         if (cuddV(F) >= cuddV(G)) {
00417             return(F);
00418         } else {
00419             return(G);
00420         }
00421     }
00422     if (F > G) { /* swap f and g */
00423         *f = G;
00424         *g = F;
00425     }
00426     return(NULL);
00427 
00428 } /* end of Cudd_addMaximum */

DdNode* Cudd_addMinimum ( DdManager *  dd,
DdNode **  f,
DdNode **  g 
)

Function********************************************************************

Synopsis [Integer and floating point min.]

Description [Integer and floating point min for Cudd_addApply. Returns NULL if not a terminal case; min(f,g) otherwise.]

SideEffects [None]

SeeAlso [Cudd_addApply]

Definition at line 354 of file cuddAddApply.c.

00358 {
00359     DdNode *F, *G;
00360 
00361     F = *f; G = *g;
00362     if (F == DD_PLUS_INFINITY(dd)) return(G);
00363     if (G == DD_PLUS_INFINITY(dd)) return(F);
00364     if (F == G) return(F);
00365 #if 0
00366     /* These special cases probably do not pay off. */
00367     if (F == DD_MINUS_INFINITY(dd)) return(F);
00368     if (G == DD_MINUS_INFINITY(dd)) return(G);
00369 #endif
00370     if (cuddIsConstant(F) && cuddIsConstant(G)) {
00371         if (cuddV(F) <= cuddV(G)) {
00372             return(F);
00373         } else {
00374             return(G);
00375         }
00376     }
00377     if (F > G) { /* swap f and g */
00378         *f = G;
00379         *g = F;
00380     }
00381     return(NULL);
00382 
00383 } /* end of Cudd_addMinimum */

DdNode* Cudd_addMinus ( DdManager *  dd,
DdNode **  f,
DdNode **  g 
)

Function********************************************************************

Synopsis [Integer and floating point subtraction.]

Description [Integer and floating point subtraction. Returns NULL if not a terminal case; f - g otherwise.]

SideEffects [None]

SeeAlso [Cudd_addApply]

Definition at line 318 of file cuddAddApply.c.

00322 {
00323     DdNode *res;
00324     DdNode *F, *G;
00325     CUDD_VALUE_TYPE value;
00326 
00327     F = *f; G = *g;
00328     if (F == G) return(DD_ZERO(dd));
00329     if (F == DD_ZERO(dd)) return(cuddAddNegateRecur(dd,G));
00330     if (G == DD_ZERO(dd)) return(F);
00331     if (cuddIsConstant(F) && cuddIsConstant(G)) {
00332         value = cuddV(F)-cuddV(G);
00333         res = cuddUniqueConst(dd,value);
00334         return(res);
00335     }
00336     return(NULL);
00337 
00338 } /* end of Cudd_addMinus */

DdNode* Cudd_addMonadicApply ( DdManager *  dd,
DdNode *(*)(DdManager *, DdNode *)  op,
DdNode *  f 
)

Function********************************************************************

Synopsis [Applies op to the discriminants of f.]

Description [Applies op to the discriminants of f. Returns a pointer to the result if succssful; NULL otherwise.]

SideEffects [None]

SeeAlso [Cudd_addApply Cudd_addLog]

Definition at line 716 of file cuddAddApply.c.

00720 {
00721     DdNode *res;
00722 
00723     do {
00724         dd->reordered = 0;
00725         res = cuddAddMonadicApplyRecur(dd,op,f);
00726     } while (dd->reordered == 1);
00727     return(res);
00728 
00729 } /* end of Cudd_addMonadicApply */

DdNode* Cudd_addNand ( DdManager *  dd,
DdNode **  f,
DdNode **  g 
)

Function********************************************************************

Synopsis [NAND of two 0-1 ADDs.]

Description [NAND of two 0-1 ADDs. Returns NULL if not a terminal case; f NAND g otherwise.]

SideEffects [None]

SeeAlso [Cudd_addApply]

Definition at line 584 of file cuddAddApply.c.

00588 {
00589     DdNode *F, *G;
00590 
00591     F = *f; G = *g;
00592     if (F == DD_ZERO(dd) || G == DD_ZERO(dd)) return(DD_ONE(dd));
00593     if (cuddIsConstant(F) && cuddIsConstant(G)) return(DD_ZERO(dd));
00594     if (F > G) { /* swap f and g */
00595         *f = G;
00596         *g = F;
00597     }
00598     return(NULL);
00599 
00600 } /* end of Cudd_addNand */

DdNode* Cudd_addNor ( DdManager *  dd,
DdNode **  f,
DdNode **  g 
)

Function********************************************************************

Synopsis [NOR of two 0-1 ADDs.]

Description [NOR of two 0-1 ADDs. Returns NULL if not a terminal case; f NOR g otherwise.]

SideEffects [None]

SeeAlso [Cudd_addApply]

Definition at line 616 of file cuddAddApply.c.

00620 {
00621     DdNode *F, *G;
00622 
00623     F = *f; G = *g;
00624     if (F == DD_ONE(dd) || G == DD_ONE(dd)) return(DD_ZERO(dd));
00625     if (cuddIsConstant(F) && cuddIsConstant(G)) return(DD_ONE(dd));
00626     if (F > G) { /* swap f and g */
00627         *f = G;
00628         *g = F;
00629     }
00630     return(NULL);
00631 
00632 } /* end of Cudd_addNor */

DdNode* Cudd_addOneZeroMaximum ( DdManager *  dd,
DdNode **  f,
DdNode **  g 
)

Function********************************************************************

Synopsis [Returns 1 if f > g and 0 otherwise.]

Description [Returns 1 if f > g and 0 otherwise. Used in conjunction with Cudd_addApply. Returns NULL if not a terminal case.]

SideEffects [None]

SeeAlso [Cudd_addApply]

Definition at line 445 of file cuddAddApply.c.

00449 {
00450 
00451     if (*f == *g) return(DD_ZERO(dd));
00452     if (*g == DD_PLUS_INFINITY(dd))
00453         return DD_ZERO(dd);
00454     if (cuddIsConstant(*f) && cuddIsConstant(*g)) {
00455         if (cuddV(*f) > cuddV(*g)) {
00456             return(DD_ONE(dd));
00457         } else {
00458             return(DD_ZERO(dd));
00459         }
00460     }
00461 
00462     return(NULL);
00463 
00464 } /* end of Cudd_addOneZeroMaximum */

DdNode* Cudd_addOr ( DdManager *  dd,
DdNode **  f,
DdNode **  g 
)

Function********************************************************************

Synopsis [Disjunction of two 0-1 ADDs.]

Description [Disjunction of two 0-1 ADDs. Returns NULL if not a terminal case; f OR g otherwise.]

SideEffects [None]

SeeAlso [Cudd_addApply]

Definition at line 550 of file cuddAddApply.c.

00554 {
00555     DdNode *F, *G;
00556 
00557     F = *f; G = *g;
00558     if (F == DD_ONE(dd) || G == DD_ONE(dd)) return(DD_ONE(dd));
00559     if (cuddIsConstant(F)) return(G);
00560     if (cuddIsConstant(G)) return(F);
00561     if (F == G) return(F);
00562     if (F > G) { /* swap f and g */
00563         *f = G;
00564         *g = F;
00565     }
00566     return(NULL);
00567 
00568 } /* end of Cudd_addOr */

DdNode* Cudd_addPlus ( DdManager *  dd,
DdNode **  f,
DdNode **  g 
)

Function********************************************************************

Synopsis [Integer and floating point addition.]

Description [Integer and floating point addition. Returns NULL if not a terminal case; f+g otherwise.]

SideEffects [None]

SeeAlso [Cudd_addApply]

Definition at line 137 of file cuddAddApply.c.

00141 {
00142     DdNode *res;
00143     DdNode *F, *G;
00144     CUDD_VALUE_TYPE value;
00145 
00146     F = *f; G = *g;
00147     if (F == DD_ZERO(dd)) return(G);
00148     if (G == DD_ZERO(dd)) return(F);
00149     if (cuddIsConstant(F) && cuddIsConstant(G)) {
00150         value = cuddV(F)+cuddV(G);
00151         res = cuddUniqueConst(dd,value);
00152         return(res);
00153     }
00154     if (F > G) { /* swap f and g */
00155         *f = G;
00156         *g = F;
00157     }
00158     return(NULL);
00159 
00160 } /* end of Cudd_addPlus */

DdNode* Cudd_addSetNZ ( DdManager *  dd,
DdNode **  f,
DdNode **  g 
)

Function********************************************************************

Synopsis [This operator sets f to the value of g wherever g != 0.]

Description [This operator sets f to the value of g wherever g != 0. Returns NULL if not a terminal case; f op g otherwise.]

SideEffects [None]

SeeAlso [Cudd_addApply]

Definition at line 251 of file cuddAddApply.c.

00255 {
00256     DdNode *F, *G;
00257 
00258     F = *f; G = *g;
00259     if (F == G) return(F);
00260     if (F == DD_ZERO(dd)) return(G);
00261     if (G == DD_ZERO(dd)) return(F);
00262     if (cuddIsConstant(G)) return(G);
00263     return(NULL);
00264 
00265 } /* end of Cudd_addSetNZ */

DdNode* Cudd_addThreshold ( DdManager *  dd,
DdNode **  f,
DdNode **  g 
)

Function********************************************************************

Synopsis [f if f>=g; 0 if f<g.]

Description [Threshold operator for Apply (f if f >=g; 0 if f<g). Returns NULL if not a terminal case; f op g otherwise.]

SideEffects [None]

SeeAlso [Cudd_addApply]

Definition at line 217 of file cuddAddApply.c.

00221 {
00222     DdNode *F, *G;
00223 
00224     F = *f; G = *g;
00225     if (F == G || F == DD_PLUS_INFINITY(dd)) return(F);
00226     if (cuddIsConstant(F) && cuddIsConstant(G)) {
00227         if (cuddV(F) >= cuddV(G)) {
00228             return(F);
00229         } else {
00230             return(DD_ZERO(dd));
00231         }
00232     }
00233     return(NULL);
00234 
00235 } /* end of Cudd_addThreshold */

DdNode* Cudd_addTimes ( DdManager *  dd,
DdNode **  f,
DdNode **  g 
)

Function********************************************************************

Synopsis [Integer and floating point multiplication.]

Description [Integer and floating point multiplication. Returns NULL if not a terminal case; f * g otherwise. This function can be used also to take the AND of two 0-1 ADDs.]

SideEffects [None]

SeeAlso [Cudd_addApply]

Definition at line 177 of file cuddAddApply.c.

00181 {
00182     DdNode *res;
00183     DdNode *F, *G;
00184     CUDD_VALUE_TYPE value;
00185 
00186     F = *f; G = *g;
00187     if (F == DD_ZERO(dd) || G == DD_ZERO(dd)) return(DD_ZERO(dd));
00188     if (F == DD_ONE(dd)) return(G);
00189     if (G == DD_ONE(dd)) return(F);
00190     if (cuddIsConstant(F) && cuddIsConstant(G)) {
00191         value = cuddV(F)*cuddV(G);
00192         res = cuddUniqueConst(dd,value);
00193         return(res);
00194     }
00195     if (F > G) { /* swap f and g */
00196         *f = G;
00197         *g = F;
00198     }
00199     return(NULL);
00200 
00201 } /* end of Cudd_addTimes */

DdNode* Cudd_addXnor ( DdManager *  dd,
DdNode **  f,
DdNode **  g 
)

Function********************************************************************

Synopsis [XNOR of two 0-1 ADDs.]

Description [XNOR of two 0-1 ADDs. Returns NULL if not a terminal case; f XNOR g otherwise.]

SideEffects [None]

SeeAlso [Cudd_addApply]

Definition at line 682 of file cuddAddApply.c.

00686 {
00687     DdNode *F, *G;
00688 
00689     F = *f; G = *g;
00690     if (F == G) return(DD_ONE(dd));
00691     if (F == DD_ONE(dd) && G == DD_ONE(dd)) return(DD_ONE(dd));
00692     if (G == DD_ZERO(dd) && F == DD_ZERO(dd)) return(DD_ONE(dd));
00693     if (cuddIsConstant(F) && cuddIsConstant(G)) return(DD_ZERO(dd));
00694     if (F > G) { /* swap f and g */
00695         *f = G;
00696         *g = F;
00697     }
00698     return(NULL);
00699 
00700 } /* end of Cudd_addXnor */

DdNode* Cudd_addXor ( DdManager *  dd,
DdNode **  f,
DdNode **  g 
)

Function********************************************************************

Synopsis [XOR of two 0-1 ADDs.]

Description [XOR of two 0-1 ADDs. Returns NULL if not a terminal case; f XOR g otherwise.]

SideEffects [None]

SeeAlso [Cudd_addApply]

Definition at line 648 of file cuddAddApply.c.

00652 {
00653     DdNode *F, *G;
00654 
00655     F = *f; G = *g;
00656     if (F == G) return(DD_ZERO(dd));
00657     if (F == DD_ONE(dd) && G == DD_ZERO(dd)) return(DD_ONE(dd));
00658     if (G == DD_ONE(dd) && F == DD_ZERO(dd)) return(DD_ONE(dd));
00659     if (cuddIsConstant(F) && cuddIsConstant(G)) return(DD_ZERO(dd));
00660     if (F > G) { /* swap f and g */
00661         *f = G;
00662         *g = F;
00663     }
00664     return(NULL);
00665 
00666 } /* end of Cudd_addXor */

DdNode* cuddAddApplyRecur ( DdManager *  dd,
DdNode *(*)(DdManager *, DdNode **, DdNode **)  op,
DdNode *  f,
DdNode *  g 
)

Function********************************************************************

Synopsis [Performs the recursive step of Cudd_addApply.]

Description [Performs the recursive step of Cudd_addApply. Returns a pointer to the result if successful; NULL otherwise.]

SideEffects [None]

SeeAlso [cuddAddMonadicApplyRecur]

Definition at line 778 of file cuddAddApply.c.

00783 {
00784     DdNode *res,
00785            *fv, *fvn, *gv, *gvn,
00786            *T, *E;
00787     unsigned int ford, gord;
00788     unsigned int index;
00789     DdNode *(*cacheOp)(DdManager *, DdNode *, DdNode *);
00790 
00791     /* Check terminal cases. Op may swap f and g to increase the
00792      * cache hit rate.
00793      */
00794     statLine(dd);
00795     res = (*op)(dd,&f,&g);
00796     if (res != NULL) return(res);
00797 
00798     /* Check cache. */
00799     cacheOp = (DdNode *(*)(DdManager *, DdNode *, DdNode *)) op;
00800     res = cuddCacheLookup2(dd,cacheOp,f,g);
00801     if (res != NULL) return(res);
00802 
00803     /* Recursive step. */
00804     ford = cuddI(dd,f->index);
00805     gord = cuddI(dd,g->index);
00806     if (ford <= gord) {
00807         index = f->index;
00808         fv = cuddT(f);
00809         fvn = cuddE(f);
00810     } else {
00811         index = g->index;
00812         fv = fvn = f;
00813     }
00814     if (gord <= ford) {
00815         gv = cuddT(g);
00816         gvn = cuddE(g);
00817     } else {
00818         gv = gvn = g;
00819     }
00820 
00821     T = cuddAddApplyRecur(dd,op,fv,gv);
00822     if (T == NULL) return(NULL);
00823     cuddRef(T);
00824 
00825     E = cuddAddApplyRecur(dd,op,fvn,gvn);
00826     if (E == NULL) {
00827         Cudd_RecursiveDeref(dd,T);
00828         return(NULL);
00829     }
00830     cuddRef(E);
00831 
00832     res = (T == E) ? T : cuddUniqueInter(dd,(int)index,T,E);
00833     if (res == NULL) {
00834         Cudd_RecursiveDeref(dd, T);
00835         Cudd_RecursiveDeref(dd, E);
00836         return(NULL);
00837     }
00838     cuddDeref(T);
00839     cuddDeref(E);
00840 
00841     /* Store result. */
00842     cuddCacheInsert2(dd,cacheOp,f,g,res);
00843 
00844     return(res);
00845 
00846 } /* end of cuddAddApplyRecur */

DdNode* cuddAddMonadicApplyRecur ( DdManager *  dd,
DdNode *(*)(DdManager *, DdNode *)  op,
DdNode *  f 
)

Function********************************************************************

Synopsis [Performs the recursive step of Cudd_addMonadicApply.]

Description [Performs the recursive step of Cudd_addMonadicApply. Returns a pointer to the result if successful; NULL otherwise.]

SideEffects [None]

SeeAlso [cuddAddApplyRecur]

Definition at line 862 of file cuddAddApply.c.

00866 {
00867     DdNode *res, *ft, *fe, *T, *E;
00868     unsigned int ford;
00869     unsigned int index;
00870 
00871     /* Check terminal cases. */
00872     statLine(dd);
00873     res = (*op)(dd,f);
00874     if (res != NULL) return(res);
00875 
00876     /* Check cache. */
00877     res = cuddCacheLookup1(dd,op,f);
00878     if (res != NULL) return(res);
00879 
00880     /* Recursive step. */
00881     ford = cuddI(dd,f->index);
00882     index = f->index;
00883     ft = cuddT(f);
00884     fe = cuddE(f);
00885 
00886     T = cuddAddMonadicApplyRecur(dd,op,ft);
00887     if (T == NULL) return(NULL);
00888     cuddRef(T);
00889 
00890     E = cuddAddMonadicApplyRecur(dd,op,fe);
00891     if (E == NULL) {
00892         Cudd_RecursiveDeref(dd,T);
00893         return(NULL);
00894     }
00895     cuddRef(E);
00896 
00897     res = (T == E) ? T : cuddUniqueInter(dd,(int)index,T,E);
00898     if (res == NULL) {
00899         Cudd_RecursiveDeref(dd, T);
00900         Cudd_RecursiveDeref(dd, E);
00901         return(NULL);
00902     }
00903     cuddDeref(T);
00904     cuddDeref(E);
00905 
00906     /* Store result. */
00907     cuddCacheInsert1(dd,op,f,res);
00908 
00909     return(res);
00910 
00911 } /* end of cuddAddMonadicApplyRecur */

Variable Documentation

char rcsid [] DD_UNUSED = "$Id: cuddAddApply.c,v 1.1.1.1 2003/02/24 22:23:50 wjiang Exp $" [static]

CFile***********************************************************************

FileName [cuddAddApply.c]

PackageName [cudd]

Synopsis [Apply functions for ADDs and their operators.]

Description [External procedures included in this module:

Internal procedures included in this module:

]

Author [Fabio Somenzi]

Copyright [This file was created at the University of Colorado at Boulder. The University of Colorado at Boulder makes no warranty about the suitability of this software for any purpose. It is presented on an AS IS basis.]

Definition at line 68 of file cuddAddApply.c.

Generated on Tue Jan 5 12:18:52 2010 for abc70930 by  doxygen 1.6.1