#include "util_hack.h"
#include "cuddInt.h"
Go to the source code of this file.
Functions | |
DdNode * | Cudd_addNegate (DdManager *dd, DdNode *f) |
DdNode * | Cudd_addRoundOff (DdManager *dd, DdNode *f, int N) |
DdNode * | cuddAddNegateRecur (DdManager *dd, DdNode *f) |
DdNode * | cuddAddRoundOffRecur (DdManager *dd, DdNode *f, double trunc) |
Variables | |
static char rcsid[] | DD_UNUSED = "$Id: cuddAddNeg.c,v 1.1.1.1 2003/02/24 22:23:50 wjiang Exp $" |
AutomaticStart AutomaticEnd Function********************************************************************
Synopsis [Computes the additive inverse of an ADD.]
Description [Computes the additive inverse of an ADD. Returns a pointer to the result if successful; NULL otherwise.]
SideEffects [None]
SeeAlso [Cudd_addCmpl]
Definition at line 89 of file cuddAddNeg.c.
00092 { 00093 DdNode *res; 00094 00095 do { 00096 res = cuddAddNegateRecur(dd,f); 00097 } while (dd->reordered == 1); 00098 return(res); 00099 00100 } /* end of Cudd_addNegate */
Function********************************************************************
Synopsis [Rounds off the discriminants of an ADD.]
Description [Rounds off the discriminants of an ADD. The discriminants are rounded off to N digits after the decimal. Returns a pointer to the result ADD if successful; NULL otherwise.]
SideEffects [None]
SeeAlso []
Definition at line 117 of file cuddAddNeg.c.
00121 { 00122 DdNode *res; 00123 double trunc = pow(10.0,(double)N); 00124 00125 do { 00126 res = cuddAddRoundOffRecur(dd,f,trunc); 00127 } while (dd->reordered == 1); 00128 return(res); 00129 00130 } /* end of Cudd_addRoundOff */
Function********************************************************************
Synopsis [Implements the recursive step of Cudd_addNegate.]
Description [Implements the recursive step of Cudd_addNegate. Returns a pointer to the result.]
SideEffects [None]
Definition at line 149 of file cuddAddNeg.c.
00152 { 00153 DdNode *res, 00154 *fv, *fvn, 00155 *T, *E; 00156 00157 statLine(dd); 00158 /* Check terminal cases. */ 00159 if (cuddIsConstant(f)) { 00160 res = cuddUniqueConst(dd,-cuddV(f)); 00161 return(res); 00162 } 00163 00164 /* Check cache */ 00165 res = cuddCacheLookup1(dd,Cudd_addNegate,f); 00166 if (res != NULL) return(res); 00167 00168 /* Recursive Step */ 00169 fv = cuddT(f); 00170 fvn = cuddE(f); 00171 T = cuddAddNegateRecur(dd,fv); 00172 if (T == NULL) return(NULL); 00173 cuddRef(T); 00174 00175 E = cuddAddNegateRecur(dd,fvn); 00176 if (E == NULL) { 00177 Cudd_RecursiveDeref(dd,T); 00178 return(NULL); 00179 } 00180 cuddRef(E); 00181 res = (T == E) ? T : cuddUniqueInter(dd,(int)f->index,T,E); 00182 if (res == NULL) { 00183 Cudd_RecursiveDeref(dd, T); 00184 Cudd_RecursiveDeref(dd, E); 00185 return(NULL); 00186 } 00187 cuddDeref(T); 00188 cuddDeref(E); 00189 00190 /* Store result. */ 00191 cuddCacheInsert1(dd,Cudd_addNegate,f,res); 00192 00193 return(res); 00194 00195 } /* end of cuddAddNegateRecur */
Function********************************************************************
Synopsis [Implements the recursive step of Cudd_addRoundOff.]
Description [Implements the recursive step of Cudd_addRoundOff. Returns a pointer to the result.]
SideEffects [None]
Definition at line 209 of file cuddAddNeg.c.
00213 { 00214 00215 DdNode *res, *fv, *fvn, *T, *E; 00216 double n; 00217 DdNode *(*cacheOp)(DdManager *, DdNode *); 00218 00219 statLine(dd); 00220 if (cuddIsConstant(f)) { 00221 n = ceil(cuddV(f)*trunc)/trunc; 00222 res = cuddUniqueConst(dd,n); 00223 return(res); 00224 } 00225 cacheOp = (DdNode *(*)(DdManager *, DdNode *)) Cudd_addRoundOff; 00226 res = cuddCacheLookup1(dd,cacheOp,f); 00227 if (res != NULL) { 00228 return(res); 00229 } 00230 /* Recursive Step */ 00231 fv = cuddT(f); 00232 fvn = cuddE(f); 00233 T = cuddAddRoundOffRecur(dd,fv,trunc); 00234 if (T == NULL) { 00235 return(NULL); 00236 } 00237 cuddRef(T); 00238 E = cuddAddRoundOffRecur(dd,fvn,trunc); 00239 if (E == NULL) { 00240 Cudd_RecursiveDeref(dd,T); 00241 return(NULL); 00242 } 00243 cuddRef(E); 00244 res = (T == E) ? T : cuddUniqueInter(dd,(int)f->index,T,E); 00245 if (res == NULL) { 00246 Cudd_RecursiveDeref(dd,T); 00247 Cudd_RecursiveDeref(dd,E); 00248 return(NULL); 00249 } 00250 cuddDeref(T); 00251 cuddDeref(E); 00252 00253 /* Store result. */ 00254 cuddCacheInsert1(dd,cacheOp,f,res); 00255 return(res); 00256 00257 } /* end of cuddAddRoundOffRecur */
char rcsid [] DD_UNUSED = "$Id: cuddAddNeg.c,v 1.1.1.1 2003/02/24 22:23:50 wjiang Exp $" [static] |
CFile***********************************************************************
FileName [cuddAddNeg.c]
PackageName [cudd]
Synopsis [function to compute the negation of an ADD.]
Description [External procedures included in this module:
Internal procedures included in this module:
]
Author [Fabio Somenzi, Balakrishna Kumthekar]
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 53 of file cuddAddNeg.c.