#include "util_hack.h"
#include "cuddInt.h"
Go to the source code of this file.
Functions | |
static DdNode *addDoIthBit | ARGS ((DdManager *dd, DdNode *f, DdNode *index)) |
DdNode * | Cudd_addFindMax (DdManager *dd, DdNode *f) |
DdNode * | Cudd_addFindMin (DdManager *dd, DdNode *f) |
DdNode * | Cudd_addIthBit (DdManager *dd, DdNode *f, int bit) |
static DdNode * | addDoIthBit (DdManager *dd, DdNode *f, DdNode *index) |
Variables | |
static char rcsid[] | DD_UNUSED = "$Id: cuddAddFind.c,v 1.1.1.1 2003/02/24 22:23:50 wjiang Exp $" |
Function********************************************************************
Synopsis [Performs the recursive step for Cudd_addIthBit.]
Description [Performs the recursive step for Cudd_addIthBit. Returns a pointer to the BDD if successful; NULL otherwise.]
SideEffects [None]
SeeAlso []
Definition at line 231 of file cuddAddFind.c.
00235 { 00236 DdNode *res, *T, *E; 00237 DdNode *fv, *fvn; 00238 int mask, value; 00239 int v; 00240 00241 statLine(dd); 00242 /* Check terminal case. */ 00243 if (cuddIsConstant(f)) { 00244 mask = 1 << ((int) cuddV(index)); 00245 value = (int) cuddV(f); 00246 return((value & mask) == 0 ? DD_ZERO(dd) : DD_ONE(dd)); 00247 } 00248 00249 /* Check cache. */ 00250 res = cuddCacheLookup2(dd,addDoIthBit,f,index); 00251 if (res != NULL) return(res); 00252 00253 /* Recursive step. */ 00254 v = f->index; 00255 fv = cuddT(f); fvn = cuddE(f); 00256 00257 T = addDoIthBit(dd,fv,index); 00258 if (T == NULL) return(NULL); 00259 cuddRef(T); 00260 00261 E = addDoIthBit(dd,fvn,index); 00262 if (E == NULL) { 00263 Cudd_RecursiveDeref(dd, T); 00264 return(NULL); 00265 } 00266 cuddRef(E); 00267 00268 res = (T == E) ? T : cuddUniqueInter(dd,v,T,E); 00269 if (res == NULL) { 00270 Cudd_RecursiveDeref(dd, T); 00271 Cudd_RecursiveDeref(dd, E); 00272 return(NULL); 00273 } 00274 cuddDeref(T); 00275 cuddDeref(E); 00276 00277 /* Store result. */ 00278 cuddCacheInsert2(dd,addDoIthBit,f,index,res); 00279 00280 return(res); 00281 00282 } /* end of addDoIthBit */
AutomaticStart
AutomaticEnd Function********************************************************************
Synopsis [Finds the maximum discriminant of f.]
Description [Returns a pointer to a constant ADD.]
SideEffects [None]
Definition at line 87 of file cuddAddFind.c.
00090 { 00091 DdNode *t, *e, *res; 00092 00093 statLine(dd); 00094 if (cuddIsConstant(f)) { 00095 return(f); 00096 } 00097 00098 res = cuddCacheLookup1(dd,Cudd_addFindMax,f); 00099 if (res != NULL) { 00100 return(res); 00101 } 00102 00103 t = Cudd_addFindMax(dd,cuddT(f)); 00104 if (t == DD_PLUS_INFINITY(dd)) return(t); 00105 00106 e = Cudd_addFindMax(dd,cuddE(f)); 00107 00108 res = (cuddV(t) >= cuddV(e)) ? t : e; 00109 00110 cuddCacheInsert1(dd,Cudd_addFindMax,f,res); 00111 00112 return(res); 00113 00114 } /* end of Cudd_addFindMax */
Function********************************************************************
Synopsis [Finds the minimum discriminant of f.]
Description [Returns a pointer to a constant ADD.]
SideEffects [None]
Definition at line 127 of file cuddAddFind.c.
00130 { 00131 DdNode *t, *e, *res; 00132 00133 statLine(dd); 00134 if (cuddIsConstant(f)) { 00135 return(f); 00136 } 00137 00138 res = cuddCacheLookup1(dd,Cudd_addFindMin,f); 00139 if (res != NULL) { 00140 return(res); 00141 } 00142 00143 t = Cudd_addFindMin(dd,cuddT(f)); 00144 if (t == DD_MINUS_INFINITY(dd)) return(t); 00145 00146 e = Cudd_addFindMin(dd,cuddE(f)); 00147 00148 res = (cuddV(t) <= cuddV(e)) ? t : e; 00149 00150 cuddCacheInsert1(dd,Cudd_addFindMin,f,res); 00151 00152 return(res); 00153 00154 } /* end of Cudd_addFindMin */
Function********************************************************************
Synopsis [Extracts the i-th bit from an ADD.]
Description [Produces an ADD from another ADD by replacing all discriminants whose i-th bit is equal to 1 with 1, and all other discriminants with 0. The i-th bit refers to the integer representation of the leaf value. If the value is has a fractional part, it is ignored. Repeated calls to this procedure allow one to transform an integer-valued ADD into an array of ADDs, one for each bit of the leaf values. Returns a pointer to the resulting ADD if successful; NULL otherwise.]
SideEffects [None]
SeeAlso [Cudd_addBddIthBit]
Definition at line 176 of file cuddAddFind.c.
00180 { 00181 DdNode *res; 00182 DdNode *index; 00183 00184 /* Use a constant node to remember the bit, so that we can use the 00185 ** global cache. 00186 */ 00187 index = cuddUniqueConst(dd,(CUDD_VALUE_TYPE) bit); 00188 if (index == NULL) return(NULL); 00189 cuddRef(index); 00190 00191 do { 00192 dd->reordered = 0; 00193 res = addDoIthBit(dd, f, index); 00194 } while (dd->reordered == 1); 00195 00196 if (res == NULL) { 00197 Cudd_RecursiveDeref(dd, index); 00198 return(NULL); 00199 } 00200 cuddRef(res); 00201 Cudd_RecursiveDeref(dd, index); 00202 cuddDeref(res); 00203 return(res); 00204 00205 } /* end of Cudd_addIthBit */
char rcsid [] DD_UNUSED = "$Id: cuddAddFind.c,v 1.1.1.1 2003/02/24 22:23:50 wjiang Exp $" [static] |
CFile***********************************************************************
FileName [cuddAddFind.c]
PackageName [cudd]
Synopsis [Functions to find maximum and minimum in an ADD and to extract the i-th bit.]
Description [External procedures included in this module:
Static functions 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 53 of file cuddAddFind.c.