src/cuBdd/cuddAddApply.c File Reference

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

Go to the source code of this file.

Functions

DdNode * Cudd_addApply (DdManager *dd, DD_AOP op, 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, DD_MAOP op, DdNode *f)
DdNode * Cudd_addLog (DdManager *dd, DdNode *f)
DdNode * cuddAddApplyRecur (DdManager *dd, DD_AOP op, DdNode *f, DdNode *g)
DdNode * cuddAddMonadicApplyRecur (DdManager *dd, DD_MAOP op, DdNode *f)

Variables

static char rcsid[] DD_UNUSED = "$Id: cuddAddApply.c,v 1.18 2009/02/19 16:15:26 fabio 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 547 of file cuddAddApply.c.

00551 {
00552     DdNode *F, *G;
00553 
00554     F = *f; G = *g;
00555     if (F == G) return(F);
00556     if (F == dd->background) return(F);
00557     if (G == dd->background) return(G);
00558     if (cuddIsConstant(F) && cuddIsConstant(G)) return(dd->background);
00559     return(NULL);
00560 
00561 } /* end of Cudd_addAgreement */

DdNode* Cudd_addApply ( DdManager *  dd,
DD_AOP  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 134 of file cuddAddApply.c.

00139 {
00140     DdNode *res;
00141 
00142     do {
00143         dd->reordered = 0;
00144         res = cuddAddApplyRecur(dd,op,f,g);
00145     } while (dd->reordered == 1);
00146     return(res);
00147 
00148 } /* 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 507 of file cuddAddApply.c.

00511 {
00512     DdNode *F, *G;
00513 
00514     F = *f; G = *g;
00515     if (F == G) return(DD_PLUS_INFINITY(dd));
00516     if (F == DD_PLUS_INFINITY(dd)) return(G);
00517     if (G == DD_PLUS_INFINITY(dd)) return(F);
00518     if (cuddIsConstant(F) && cuddIsConstant(G)) {
00519         if (cuddV(F) != cuddV(G)) {
00520             if (cuddV(F) < cuddV(G)) {
00521                 return(F);
00522             } else {
00523                 return(G);
00524             }
00525         } else {
00526             return(DD_PLUS_INFINITY(dd));
00527         }
00528     }
00529     return(NULL);
00530 
00531 } /* 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 308 of file cuddAddApply.c.

00312 {
00313     DdNode *res;
00314     DdNode *F, *G;
00315     CUDD_VALUE_TYPE value;
00316 
00317     F = *f; G = *g;
00318     /* We would like to use F == G -> F/G == 1, but F and G may
00319     ** contain zeroes. */
00320     if (F == DD_ZERO(dd)) return(DD_ZERO(dd));
00321     if (G == DD_ONE(dd)) return(F);
00322     if (cuddIsConstant(F) && cuddIsConstant(G)) {
00323         value = cuddV(F)/cuddV(G);
00324         res = cuddUniqueConst(dd,value);
00325         return(res);
00326     }
00327     return(NULL);
00328 
00329 } /* 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 773 of file cuddAddApply.c.

00776 {
00777     if (cuddIsConstant(f)) {
00778         CUDD_VALUE_TYPE value = log(cuddV(f));
00779         DdNode *res = cuddUniqueConst(dd,value);
00780         return(res);
00781     }
00782     return(NULL);
00783 
00784 } /* 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 426 of file cuddAddApply.c.

00430 {
00431     DdNode *F, *G;
00432 
00433     F = *f; G = *g;
00434     if (F == G) return(F);
00435     if (F == DD_MINUS_INFINITY(dd)) return(G);
00436     if (G == DD_MINUS_INFINITY(dd)) return(F);
00437 #if 0
00438     /* These special cases probably do not pay off. */
00439     if (F == DD_PLUS_INFINITY(dd)) return(F);
00440     if (G == DD_PLUS_INFINITY(dd)) return(G);
00441 #endif
00442     if (cuddIsConstant(F) && cuddIsConstant(G)) {
00443         if (cuddV(F) >= cuddV(G)) {
00444             return(F);
00445         } else {
00446             return(G);
00447         }
00448     }
00449     if (F > G) { /* swap f and g */
00450         *f = G;
00451         *g = F;
00452     }
00453     return(NULL);
00454 
00455 } /* 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 381 of file cuddAddApply.c.

00385 {
00386     DdNode *F, *G;
00387 
00388     F = *f; G = *g;
00389     if (F == DD_PLUS_INFINITY(dd)) return(G);
00390     if (G == DD_PLUS_INFINITY(dd)) return(F);
00391     if (F == G) return(F);
00392 #if 0
00393     /* These special cases probably do not pay off. */
00394     if (F == DD_MINUS_INFINITY(dd)) return(F);
00395     if (G == DD_MINUS_INFINITY(dd)) return(G);
00396 #endif
00397     if (cuddIsConstant(F) && cuddIsConstant(G)) {
00398         if (cuddV(F) <= cuddV(G)) {
00399             return(F);
00400         } else {
00401             return(G);
00402         }
00403     }
00404     if (F > G) { /* swap f and g */
00405         *f = G;
00406         *g = F;
00407     }
00408     return(NULL);
00409 
00410 } /* 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 345 of file cuddAddApply.c.

00349 {
00350     DdNode *res;
00351     DdNode *F, *G;
00352     CUDD_VALUE_TYPE value;
00353 
00354     F = *f; G = *g;
00355     if (F == G) return(DD_ZERO(dd));
00356     if (F == DD_ZERO(dd)) return(cuddAddNegateRecur(dd,G));
00357     if (G == DD_ZERO(dd)) return(F);
00358     if (cuddIsConstant(F) && cuddIsConstant(G)) {
00359         value = cuddV(F)-cuddV(G);
00360         res = cuddUniqueConst(dd,value);
00361         return(res);
00362     }
00363     return(NULL);
00364 
00365 } /* end of Cudd_addMinus */

DdNode* Cudd_addMonadicApply ( DdManager *  dd,
DD_MAOP  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 743 of file cuddAddApply.c.

00747 {
00748     DdNode *res;
00749 
00750     do {
00751         dd->reordered = 0;
00752         res = cuddAddMonadicApplyRecur(dd,op,f);
00753     } while (dd->reordered == 1);
00754     return(res);
00755 
00756 } /* 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 611 of file cuddAddApply.c.

00615 {
00616     DdNode *F, *G;
00617 
00618     F = *f; G = *g;
00619     if (F == DD_ZERO(dd) || G == DD_ZERO(dd)) return(DD_ONE(dd));
00620     if (cuddIsConstant(F) && cuddIsConstant(G)) return(DD_ZERO(dd));
00621     if (F > G) { /* swap f and g */
00622         *f = G;
00623         *g = F;
00624     }
00625     return(NULL);
00626 
00627 } /* 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 643 of file cuddAddApply.c.

00647 {
00648     DdNode *F, *G;
00649 
00650     F = *f; G = *g;
00651     if (F == DD_ONE(dd) || G == DD_ONE(dd)) return(DD_ZERO(dd));
00652     if (cuddIsConstant(F) && cuddIsConstant(G)) return(DD_ONE(dd));
00653     if (F > G) { /* swap f and g */
00654         *f = G;
00655         *g = F;
00656     }
00657     return(NULL);
00658 
00659 } /* 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 472 of file cuddAddApply.c.

00476 {
00477 
00478     if (*f == *g) return(DD_ZERO(dd));
00479     if (*g == DD_PLUS_INFINITY(dd))
00480         return DD_ZERO(dd);
00481     if (cuddIsConstant(*f) && cuddIsConstant(*g)) {
00482         if (cuddV(*f) > cuddV(*g)) {
00483             return(DD_ONE(dd));
00484         } else {
00485             return(DD_ZERO(dd));
00486         }
00487     }
00488 
00489     return(NULL);
00490 
00491 } /* 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 577 of file cuddAddApply.c.

00581 {
00582     DdNode *F, *G;
00583 
00584     F = *f; G = *g;
00585     if (F == DD_ONE(dd) || G == DD_ONE(dd)) return(DD_ONE(dd));
00586     if (cuddIsConstant(F)) return(G);
00587     if (cuddIsConstant(G)) return(F);
00588     if (F == G) return(F);
00589     if (F > G) { /* swap f and g */
00590         *f = G;
00591         *g = F;
00592     }
00593     return(NULL);
00594 
00595 } /* 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 164 of file cuddAddApply.c.

00168 {
00169     DdNode *res;
00170     DdNode *F, *G;
00171     CUDD_VALUE_TYPE value;
00172 
00173     F = *f; G = *g;
00174     if (F == DD_ZERO(dd)) return(G);
00175     if (G == DD_ZERO(dd)) return(F);
00176     if (cuddIsConstant(F) && cuddIsConstant(G)) {
00177         value = cuddV(F)+cuddV(G);
00178         res = cuddUniqueConst(dd,value);
00179         return(res);
00180     }
00181     if (F > G) { /* swap f and g */
00182         *f = G;
00183         *g = F;
00184     }
00185     return(NULL);
00186 
00187 } /* 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 278 of file cuddAddApply.c.

00282 {
00283     DdNode *F, *G;
00284 
00285     F = *f; G = *g;
00286     if (F == G) return(F);
00287     if (F == DD_ZERO(dd)) return(G);
00288     if (G == DD_ZERO(dd)) return(F);
00289     if (cuddIsConstant(G)) return(G);
00290     return(NULL);
00291 
00292 } /* 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 244 of file cuddAddApply.c.

00248 {
00249     DdNode *F, *G;
00250 
00251     F = *f; G = *g;
00252     if (F == G || F == DD_PLUS_INFINITY(dd)) return(F);
00253     if (cuddIsConstant(F) && cuddIsConstant(G)) {
00254         if (cuddV(F) >= cuddV(G)) {
00255             return(F);
00256         } else {
00257             return(DD_ZERO(dd));
00258         }
00259     }
00260     return(NULL);
00261 
00262 } /* 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 204 of file cuddAddApply.c.

00208 {
00209     DdNode *res;
00210     DdNode *F, *G;
00211     CUDD_VALUE_TYPE value;
00212 
00213     F = *f; G = *g;
00214     if (F == DD_ZERO(dd) || G == DD_ZERO(dd)) return(DD_ZERO(dd));
00215     if (F == DD_ONE(dd)) return(G);
00216     if (G == DD_ONE(dd)) return(F);
00217     if (cuddIsConstant(F) && cuddIsConstant(G)) {
00218         value = cuddV(F)*cuddV(G);
00219         res = cuddUniqueConst(dd,value);
00220         return(res);
00221     }
00222     if (F > G) { /* swap f and g */
00223         *f = G;
00224         *g = F;
00225     }
00226     return(NULL);
00227 
00228 } /* 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 709 of file cuddAddApply.c.

00713 {
00714     DdNode *F, *G;
00715 
00716     F = *f; G = *g;
00717     if (F == G) return(DD_ONE(dd));
00718     if (F == DD_ONE(dd) && G == DD_ONE(dd)) return(DD_ONE(dd));
00719     if (G == DD_ZERO(dd) && F == DD_ZERO(dd)) return(DD_ONE(dd));
00720     if (cuddIsConstant(F) && cuddIsConstant(G)) return(DD_ZERO(dd));
00721     if (F > G) { /* swap f and g */
00722         *f = G;
00723         *g = F;
00724     }
00725     return(NULL);
00726 
00727 } /* 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 675 of file cuddAddApply.c.

00679 {
00680     DdNode *F, *G;
00681 
00682     F = *f; G = *g;
00683     if (F == G) return(DD_ZERO(dd));
00684     if (F == DD_ONE(dd) && G == DD_ZERO(dd)) return(DD_ONE(dd));
00685     if (G == DD_ONE(dd) && F == DD_ZERO(dd)) return(DD_ONE(dd));
00686     if (cuddIsConstant(F) && cuddIsConstant(G)) return(DD_ZERO(dd));
00687     if (F > G) { /* swap f and g */
00688         *f = G;
00689         *g = F;
00690     }
00691     return(NULL);
00692 
00693 } /* end of Cudd_addXor */

DdNode* cuddAddApplyRecur ( DdManager *  dd,
DD_AOP  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 805 of file cuddAddApply.c.

00810 {
00811     DdNode *res,
00812            *fv, *fvn, *gv, *gvn,
00813            *T, *E;
00814     unsigned int ford, gord;
00815     unsigned int index;
00816     DD_CTFP cacheOp;
00817 
00818     /* Check terminal cases. Op may swap f and g to increase the
00819      * cache hit rate.
00820      */
00821     statLine(dd);
00822     res = (*op)(dd,&f,&g);
00823     if (res != NULL) return(res);
00824 
00825     /* Check cache. */
00826     cacheOp = (DD_CTFP) op;
00827     res = cuddCacheLookup2(dd,cacheOp,f,g);
00828     if (res != NULL) return(res);
00829 
00830     /* Recursive step. */
00831     ford = cuddI(dd,f->index);
00832     gord = cuddI(dd,g->index);
00833     if (ford <= gord) {
00834         index = f->index;
00835         fv = cuddT(f);
00836         fvn = cuddE(f);
00837     } else {
00838         index = g->index;
00839         fv = fvn = f;
00840     }
00841     if (gord <= ford) {
00842         gv = cuddT(g);
00843         gvn = cuddE(g);
00844     } else {
00845         gv = gvn = g;
00846     }
00847 
00848     T = cuddAddApplyRecur(dd,op,fv,gv);
00849     if (T == NULL) return(NULL);
00850     cuddRef(T);
00851 
00852     E = cuddAddApplyRecur(dd,op,fvn,gvn);
00853     if (E == NULL) {
00854         Cudd_RecursiveDeref(dd,T);
00855         return(NULL);
00856     }
00857     cuddRef(E);
00858 
00859     res = (T == E) ? T : cuddUniqueInter(dd,(int)index,T,E);
00860     if (res == NULL) {
00861         Cudd_RecursiveDeref(dd, T);
00862         Cudd_RecursiveDeref(dd, E);
00863         return(NULL);
00864     }
00865     cuddDeref(T);
00866     cuddDeref(E);
00867 
00868     /* Store result. */
00869     cuddCacheInsert2(dd,cacheOp,f,g,res);
00870 
00871     return(res);
00872 
00873 } /* end of cuddAddApplyRecur */

DdNode* cuddAddMonadicApplyRecur ( DdManager *  dd,
DD_MAOP  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 889 of file cuddAddApply.c.

00893 {
00894     DdNode *res, *ft, *fe, *T, *E;
00895     unsigned int index;
00896 
00897     /* Check terminal cases. */
00898     statLine(dd);
00899     res = (*op)(dd,f);
00900     if (res != NULL) return(res);
00901 
00902     /* Check cache. */
00903     res = cuddCacheLookup1(dd,op,f);
00904     if (res != NULL) return(res);
00905 
00906     /* Recursive step. */
00907     index = f->index;
00908     ft = cuddT(f);
00909     fe = cuddE(f);
00910 
00911     T = cuddAddMonadicApplyRecur(dd,op,ft);
00912     if (T == NULL) return(NULL);
00913     cuddRef(T);
00914 
00915     E = cuddAddMonadicApplyRecur(dd,op,fe);
00916     if (E == NULL) {
00917         Cudd_RecursiveDeref(dd,T);
00918         return(NULL);
00919     }
00920     cuddRef(E);
00921 
00922     res = (T == E) ? T : cuddUniqueInter(dd,(int)index,T,E);
00923     if (res == NULL) {
00924         Cudd_RecursiveDeref(dd, T);
00925         Cudd_RecursiveDeref(dd, E);
00926         return(NULL);
00927     }
00928     cuddDeref(T);
00929     cuddDeref(E);
00930 
00931     /* Store result. */
00932     cuddCacheInsert1(dd,op,f,res);
00933 
00934     return(res);
00935 
00936 } /* end of cuddAddMonadicApplyRecur */

Variable Documentation

char rcsid [] DD_UNUSED = "$Id: cuddAddApply.c,v 1.18 2009/02/19 16:15:26 fabio 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 [Copyright (c) 1995-2004, Regents of the University of Colorado

All rights reserved.

Redistribution and use in source and binary forms, with or without modification, are permitted provided that the following conditions are met:

Redistributions of source code must retain the above copyright notice, this list of conditions and the following disclaimer.

Redistributions in binary form must reproduce the above copyright notice, this list of conditions and the following disclaimer in the documentation and/or other materials provided with the distribution.

Neither the name of the University of Colorado nor the names of its contributors may be used to endorse or promote products derived from this software without specific prior written permission.

THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT OWNER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.]

Definition at line 95 of file cuddAddApply.c.

Generated on Tue Jan 12 13:57:17 2010 for glu-2.2 by  doxygen 1.6.1