diff options
Diffstat (limited to 'src/bdd/cudd/cuddAddApply.c')
-rw-r--r-- | src/bdd/cudd/cuddAddApply.c | 917 |
1 files changed, 0 insertions, 917 deletions
diff --git a/src/bdd/cudd/cuddAddApply.c b/src/bdd/cudd/cuddAddApply.c deleted file mode 100644 index 60c06de6..00000000 --- a/src/bdd/cudd/cuddAddApply.c +++ /dev/null @@ -1,917 +0,0 @@ -/**CFile*********************************************************************** - - FileName [cuddAddApply.c] - - PackageName [cudd] - - Synopsis [Apply functions for ADDs and their operators.] - - Description [External procedures included in this module: - <ul> - <li> Cudd_addApply() - <li> Cudd_addMonadicApply() - <li> Cudd_addPlus() - <li> Cudd_addTimes() - <li> Cudd_addThreshold() - <li> Cudd_addSetNZ() - <li> Cudd_addDivide() - <li> Cudd_addMinus() - <li> Cudd_addMinimum() - <li> Cudd_addMaximum() - <li> Cudd_addOneZeroMaximum() - <li> Cudd_addDiff() - <li> Cudd_addAgreement() - <li> Cudd_addOr() - <li> Cudd_addNand() - <li> Cudd_addNor() - <li> Cudd_addXor() - <li> Cudd_addXnor() - </ul> - Internal procedures included in this module: - <ul> - <li> cuddAddApplyRecur() - <li> cuddAddMonadicApplyRecur() - </ul>] - - 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.] - -******************************************************************************/ - -#include "util_hack.h" -#include "cuddInt.h" - -/*---------------------------------------------------------------------------*/ -/* Constant declarations */ -/*---------------------------------------------------------------------------*/ - - -/*---------------------------------------------------------------------------*/ -/* Stucture declarations */ -/*---------------------------------------------------------------------------*/ - - -/*---------------------------------------------------------------------------*/ -/* Type declarations */ -/*---------------------------------------------------------------------------*/ - - -/*---------------------------------------------------------------------------*/ -/* Variable declarations */ -/*---------------------------------------------------------------------------*/ - -#ifndef lint -static char rcsid[] DD_UNUSED = "$Id: cuddAddApply.c,v 1.1.1.1 2003/02/24 22:23:50 wjiang Exp $"; -#endif - - -/*---------------------------------------------------------------------------*/ -/* Macro declarations */ -/*---------------------------------------------------------------------------*/ - - -/**AutomaticStart*************************************************************/ - -/*---------------------------------------------------------------------------*/ -/* Static function prototypes */ -/*---------------------------------------------------------------------------*/ - - -/**AutomaticEnd***************************************************************/ - - -/*---------------------------------------------------------------------------*/ -/* Definition of exported functions */ -/*---------------------------------------------------------------------------*/ - -/**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] - -******************************************************************************/ -DdNode * -Cudd_addApply( - DdManager * dd, - DdNode * (*op)(DdManager *, DdNode **, DdNode **), - DdNode * f, - DdNode * g) -{ - DdNode *res; - - do { - dd->reordered = 0; - res = cuddAddApplyRecur(dd,op,f,g); - } while (dd->reordered == 1); - return(res); - -} /* end of Cudd_addApply */ - - -/**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] - -******************************************************************************/ -DdNode * -Cudd_addPlus( - DdManager * dd, - DdNode ** f, - DdNode ** g) -{ - DdNode *res; - DdNode *F, *G; - CUDD_VALUE_TYPE value; - - F = *f; G = *g; - if (F == DD_ZERO(dd)) return(G); - if (G == DD_ZERO(dd)) return(F); - if (cuddIsConstant(F) && cuddIsConstant(G)) { - value = cuddV(F)+cuddV(G); - res = cuddUniqueConst(dd,value); - return(res); - } - if (F > G) { /* swap f and g */ - *f = G; - *g = F; - } - return(NULL); - -} /* end of Cudd_addPlus */ - - -/**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] - -******************************************************************************/ -DdNode * -Cudd_addTimes( - DdManager * dd, - DdNode ** f, - DdNode ** g) -{ - DdNode *res; - DdNode *F, *G; - CUDD_VALUE_TYPE value; - - F = *f; G = *g; - if (F == DD_ZERO(dd) || G == DD_ZERO(dd)) return(DD_ZERO(dd)); - if (F == DD_ONE(dd)) return(G); - if (G == DD_ONE(dd)) return(F); - if (cuddIsConstant(F) && cuddIsConstant(G)) { - value = cuddV(F)*cuddV(G); - res = cuddUniqueConst(dd,value); - return(res); - } - if (F > G) { /* swap f and g */ - *f = G; - *g = F; - } - return(NULL); - -} /* end of Cudd_addTimes */ - - -/**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] - -******************************************************************************/ -DdNode * -Cudd_addThreshold( - DdManager * dd, - DdNode ** f, - DdNode ** g) -{ - DdNode *F, *G; - - F = *f; G = *g; - if (F == G || F == DD_PLUS_INFINITY(dd)) return(F); - if (cuddIsConstant(F) && cuddIsConstant(G)) { - if (cuddV(F) >= cuddV(G)) { - return(F); - } else { - return(DD_ZERO(dd)); - } - } - return(NULL); - -} /* end of Cudd_addThreshold */ - - -/**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] - -******************************************************************************/ -DdNode * -Cudd_addSetNZ( - DdManager * dd, - DdNode ** f, - DdNode ** g) -{ - DdNode *F, *G; - - F = *f; G = *g; - if (F == G) return(F); - if (F == DD_ZERO(dd)) return(G); - if (G == DD_ZERO(dd)) return(F); - if (cuddIsConstant(G)) return(G); - return(NULL); - -} /* end of Cudd_addSetNZ */ - - -/**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] - -******************************************************************************/ -DdNode * -Cudd_addDivide( - DdManager * dd, - DdNode ** f, - DdNode ** g) -{ - DdNode *res; - DdNode *F, *G; - CUDD_VALUE_TYPE value; - - F = *f; G = *g; - /* We would like to use F == G -> F/G == 1, but F and G may - ** contain zeroes. */ - if (F == DD_ZERO(dd)) return(DD_ZERO(dd)); - if (G == DD_ONE(dd)) return(F); - if (cuddIsConstant(F) && cuddIsConstant(G)) { - value = cuddV(F)/cuddV(G); - res = cuddUniqueConst(dd,value); - return(res); - } - return(NULL); - -} /* end of Cudd_addDivide */ - - -/**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] - -******************************************************************************/ -DdNode * -Cudd_addMinus( - DdManager * dd, - DdNode ** f, - DdNode ** g) -{ - DdNode *res; - DdNode *F, *G; - CUDD_VALUE_TYPE value; - - F = *f; G = *g; - if (F == G) return(DD_ZERO(dd)); - if (F == DD_ZERO(dd)) return(cuddAddNegateRecur(dd,G)); - if (G == DD_ZERO(dd)) return(F); - if (cuddIsConstant(F) && cuddIsConstant(G)) { - value = cuddV(F)-cuddV(G); - res = cuddUniqueConst(dd,value); - return(res); - } - return(NULL); - -} /* end of Cudd_addMinus */ - - -/**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] - -******************************************************************************/ -DdNode * -Cudd_addMinimum( - DdManager * dd, - DdNode ** f, - DdNode ** g) -{ - DdNode *F, *G; - - F = *f; G = *g; - if (F == DD_PLUS_INFINITY(dd)) return(G); - if (G == DD_PLUS_INFINITY(dd)) return(F); - if (F == G) return(F); -#if 0 - /* These special cases probably do not pay off. */ - if (F == DD_MINUS_INFINITY(dd)) return(F); - if (G == DD_MINUS_INFINITY(dd)) return(G); -#endif - if (cuddIsConstant(F) && cuddIsConstant(G)) { - if (cuddV(F) <= cuddV(G)) { - return(F); - } else { - return(G); - } - } - if (F > G) { /* swap f and g */ - *f = G; - *g = F; - } - return(NULL); - -} /* end of Cudd_addMinimum */ - - -/**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] - -******************************************************************************/ -DdNode * -Cudd_addMaximum( - DdManager * dd, - DdNode ** f, - DdNode ** g) -{ - DdNode *F, *G; - - F = *f; G = *g; - if (F == G) return(F); - if (F == DD_MINUS_INFINITY(dd)) return(G); - if (G == DD_MINUS_INFINITY(dd)) return(F); -#if 0 - /* These special cases probably do not pay off. */ - if (F == DD_PLUS_INFINITY(dd)) return(F); - if (G == DD_PLUS_INFINITY(dd)) return(G); -#endif - if (cuddIsConstant(F) && cuddIsConstant(G)) { - if (cuddV(F) >= cuddV(G)) { - return(F); - } else { - return(G); - } - } - if (F > G) { /* swap f and g */ - *f = G; - *g = F; - } - return(NULL); - -} /* end of Cudd_addMaximum */ - - -/**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] - -******************************************************************************/ -DdNode * -Cudd_addOneZeroMaximum( - DdManager * dd, - DdNode ** f, - DdNode ** g) -{ - - if (*f == *g) return(DD_ZERO(dd)); - if (*g == DD_PLUS_INFINITY(dd)) - return DD_ZERO(dd); - if (cuddIsConstant(*f) && cuddIsConstant(*g)) { - if (cuddV(*f) > cuddV(*g)) { - return(DD_ONE(dd)); - } else { - return(DD_ZERO(dd)); - } - } - - return(NULL); - -} /* end of Cudd_addOneZeroMaximum */ - - -/**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] - -******************************************************************************/ -DdNode * -Cudd_addDiff( - DdManager * dd, - DdNode ** f, - DdNode ** g) -{ - DdNode *F, *G; - - F = *f; G = *g; - if (F == G) return(DD_PLUS_INFINITY(dd)); - if (F == DD_PLUS_INFINITY(dd)) return(G); - if (G == DD_PLUS_INFINITY(dd)) return(F); - if (cuddIsConstant(F) && cuddIsConstant(G)) { - if (cuddV(F) != cuddV(G)) { - if (cuddV(F) < cuddV(G)) { - return(F); - } else { - return(G); - } - } else { - return(DD_PLUS_INFINITY(dd)); - } - } - return(NULL); - -} /* end of Cudd_addDiff */ - - -/**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] - -******************************************************************************/ -DdNode * -Cudd_addAgreement( - DdManager * dd, - DdNode ** f, - DdNode ** g) -{ - DdNode *F, *G; - - F = *f; G = *g; - if (F == G) return(F); - if (F == dd->background) return(F); - if (G == dd->background) return(G); - if (cuddIsConstant(F) && cuddIsConstant(G)) return(dd->background); - return(NULL); - -} /* end of Cudd_addAgreement */ - - -/**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] - -******************************************************************************/ -DdNode * -Cudd_addOr( - DdManager * dd, - DdNode ** f, - DdNode ** g) -{ - DdNode *F, *G; - - F = *f; G = *g; - if (F == DD_ONE(dd) || G == DD_ONE(dd)) return(DD_ONE(dd)); - if (cuddIsConstant(F)) return(G); - if (cuddIsConstant(G)) return(F); - if (F == G) return(F); - if (F > G) { /* swap f and g */ - *f = G; - *g = F; - } - return(NULL); - -} /* end of Cudd_addOr */ - - -/**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] - -******************************************************************************/ -DdNode * -Cudd_addNand( - DdManager * dd, - DdNode ** f, - DdNode ** g) -{ - DdNode *F, *G; - - F = *f; G = *g; - if (F == DD_ZERO(dd) || G == DD_ZERO(dd)) return(DD_ONE(dd)); - if (cuddIsConstant(F) && cuddIsConstant(G)) return(DD_ZERO(dd)); - if (F > G) { /* swap f and g */ - *f = G; - *g = F; - } - return(NULL); - -} /* end of Cudd_addNand */ - - -/**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] - -******************************************************************************/ -DdNode * -Cudd_addNor( - DdManager * dd, - DdNode ** f, - DdNode ** g) -{ - DdNode *F, *G; - - F = *f; G = *g; - if (F == DD_ONE(dd) || G == DD_ONE(dd)) return(DD_ZERO(dd)); - if (cuddIsConstant(F) && cuddIsConstant(G)) return(DD_ONE(dd)); - if (F > G) { /* swap f and g */ - *f = G; - *g = F; - } - return(NULL); - -} /* end of Cudd_addNor */ - - -/**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] - -******************************************************************************/ -DdNode * -Cudd_addXor( - DdManager * dd, - DdNode ** f, - DdNode ** g) -{ - DdNode *F, *G; - - F = *f; G = *g; - if (F == G) return(DD_ZERO(dd)); - if (F == DD_ONE(dd) && G == DD_ZERO(dd)) return(DD_ONE(dd)); - if (G == DD_ONE(dd) && F == DD_ZERO(dd)) return(DD_ONE(dd)); - if (cuddIsConstant(F) && cuddIsConstant(G)) return(DD_ZERO(dd)); - if (F > G) { /* swap f and g */ - *f = G; - *g = F; - } - return(NULL); - -} /* end of Cudd_addXor */ - - -/**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] - -******************************************************************************/ -DdNode * -Cudd_addXnor( - DdManager * dd, - DdNode ** f, - DdNode ** g) -{ - DdNode *F, *G; - - F = *f; G = *g; - if (F == G) return(DD_ONE(dd)); - if (F == DD_ONE(dd) && G == DD_ONE(dd)) return(DD_ONE(dd)); - if (G == DD_ZERO(dd) && F == DD_ZERO(dd)) return(DD_ONE(dd)); - if (cuddIsConstant(F) && cuddIsConstant(G)) return(DD_ZERO(dd)); - if (F > G) { /* swap f and g */ - *f = G; - *g = F; - } - return(NULL); - -} /* end of Cudd_addXnor */ - - -/**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] - -******************************************************************************/ -DdNode * -Cudd_addMonadicApply( - DdManager * dd, - DdNode * (*op)(DdManager *, DdNode *), - DdNode * f) -{ - DdNode *res; - - do { - dd->reordered = 0; - res = cuddAddMonadicApplyRecur(dd,op,f); - } while (dd->reordered == 1); - return(res); - -} /* end of Cudd_addMonadicApply */ - - -/**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] - -******************************************************************************/ -DdNode * -Cudd_addLog( - DdManager * dd, - DdNode * f) -{ - if (cuddIsConstant(f)) { - CUDD_VALUE_TYPE value = log(cuddV(f)); - DdNode *res = cuddUniqueConst(dd,value); - return(res); - } - return(NULL); - -} /* end of Cudd_addLog */ - - -/*---------------------------------------------------------------------------*/ -/* Definition of internal functions */ -/*---------------------------------------------------------------------------*/ - - -/**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] - -******************************************************************************/ -DdNode * -cuddAddApplyRecur( - DdManager * dd, - DdNode * (*op)(DdManager *, DdNode **, DdNode **), - DdNode * f, - DdNode * g) -{ - DdNode *res, - *fv, *fvn, *gv, *gvn, - *T, *E; - unsigned int ford, gord; - unsigned int index; - DdNode *(*cacheOp)(DdManager *, DdNode *, DdNode *); - - /* Check terminal cases. Op may swap f and g to increase the - * cache hit rate. - */ - statLine(dd); - res = (*op)(dd,&f,&g); - if (res != NULL) return(res); - - /* Check cache. */ - cacheOp = (DdNode *(*)(DdManager *, DdNode *, DdNode *)) op; - res = cuddCacheLookup2(dd,cacheOp,f,g); - if (res != NULL) return(res); - - /* Recursive step. */ - ford = cuddI(dd,f->index); - gord = cuddI(dd,g->index); - if (ford <= gord) { - index = f->index; - fv = cuddT(f); - fvn = cuddE(f); - } else { - index = g->index; - fv = fvn = f; - } - if (gord <= ford) { - gv = cuddT(g); - gvn = cuddE(g); - } else { - gv = gvn = g; - } - - T = cuddAddApplyRecur(dd,op,fv,gv); - if (T == NULL) return(NULL); - cuddRef(T); - - E = cuddAddApplyRecur(dd,op,fvn,gvn); - if (E == NULL) { - Cudd_RecursiveDeref(dd,T); - return(NULL); - } - cuddRef(E); - - res = (T == E) ? T : cuddUniqueInter(dd,(int)index,T,E); - if (res == NULL) { - Cudd_RecursiveDeref(dd, T); - Cudd_RecursiveDeref(dd, E); - return(NULL); - } - cuddDeref(T); - cuddDeref(E); - - /* Store result. */ - cuddCacheInsert2(dd,cacheOp,f,g,res); - - return(res); - -} /* end of cuddAddApplyRecur */ - - -/**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] - -******************************************************************************/ -DdNode * -cuddAddMonadicApplyRecur( - DdManager * dd, - DdNode * (*op)(DdManager *, DdNode *), - DdNode * f) -{ - DdNode *res, *ft, *fe, *T, *E; - unsigned int ford; - unsigned int index; - - /* Check terminal cases. */ - statLine(dd); - res = (*op)(dd,f); - if (res != NULL) return(res); - - /* Check cache. */ - res = cuddCacheLookup1(dd,op,f); - if (res != NULL) return(res); - - /* Recursive step. */ - ford = cuddI(dd,f->index); - index = f->index; - ft = cuddT(f); - fe = cuddE(f); - - T = cuddAddMonadicApplyRecur(dd,op,ft); - if (T == NULL) return(NULL); - cuddRef(T); - - E = cuddAddMonadicApplyRecur(dd,op,fe); - if (E == NULL) { - Cudd_RecursiveDeref(dd,T); - return(NULL); - } - cuddRef(E); - - res = (T == E) ? T : cuddUniqueInter(dd,(int)index,T,E); - if (res == NULL) { - Cudd_RecursiveDeref(dd, T); - Cudd_RecursiveDeref(dd, E); - return(NULL); - } - cuddDeref(T); - cuddDeref(E); - - /* Store result. */ - cuddCacheInsert1(dd,op,f,res); - - return(res); - -} /* end of cuddAddMonadicApplyRecur */ - - -/*---------------------------------------------------------------------------*/ -/* Definition of static functions */ -/*---------------------------------------------------------------------------*/ - |