#include "util_hack.h"
#include "cuddInt.h"
Go to the source code of this file.
Functions | |
static DdNode *addWalshInt | ARGS ((DdManager *dd, DdNode **x, DdNode **y, int n)) |
DdNode * | Cudd_addWalsh (DdManager *dd, DdNode **x, DdNode **y, int n) |
DdNode * | Cudd_addResidue (DdManager *dd, int n, int m, int options, int top) |
static DdNode * | addWalshInt (DdManager *dd, DdNode **x, DdNode **y, int n) |
Variables | |
static char rcsid[] | DD_UNUSED = "$Id: cuddAddWalsh.c,v 1.1.1.1 2003/02/24 22:23:50 wjiang Exp $" |
Function********************************************************************
Synopsis [Implements the recursive step of Cudd_addWalsh.]
Description [Generates a Walsh matrix in ADD form. Returns a pointer to the matrixi if successful; NULL otherwise.]
SideEffects [None]
Definition at line 267 of file cuddAddWalsh.c.
00272 { 00273 DdNode *one, *minusone; 00274 DdNode *t, *u, *t1, *u1, *v, *w; 00275 int i; 00276 00277 one = DD_ONE(dd); 00278 if (n == 0) return(one); 00279 00280 /* Build bottom part of ADD outside loop */ 00281 minusone = cuddUniqueConst(dd,(CUDD_VALUE_TYPE) -1); 00282 if (minusone == NULL) return(NULL); 00283 cuddRef(minusone); 00284 v = Cudd_addIte(dd, y[n-1], minusone, one); 00285 if (v == NULL) { 00286 Cudd_RecursiveDeref(dd, minusone); 00287 return(NULL); 00288 } 00289 cuddRef(v); 00290 u = Cudd_addIte(dd, x[n-1], v, one); 00291 if (u == NULL) { 00292 Cudd_RecursiveDeref(dd, minusone); 00293 Cudd_RecursiveDeref(dd, v); 00294 return(NULL); 00295 } 00296 cuddRef(u); 00297 Cudd_RecursiveDeref(dd, v); 00298 if (n>1) { 00299 w = Cudd_addIte(dd, y[n-1], one, minusone); 00300 if (w == NULL) { 00301 Cudd_RecursiveDeref(dd, minusone); 00302 Cudd_RecursiveDeref(dd, u); 00303 return(NULL); 00304 } 00305 cuddRef(w); 00306 t = Cudd_addIte(dd, x[n-1], w, minusone); 00307 if (t == NULL) { 00308 Cudd_RecursiveDeref(dd, minusone); 00309 Cudd_RecursiveDeref(dd, u); 00310 Cudd_RecursiveDeref(dd, w); 00311 return(NULL); 00312 } 00313 cuddRef(t); 00314 Cudd_RecursiveDeref(dd, w); 00315 } 00316 cuddDeref(minusone); /* minusone is in the result; it won't die */ 00317 00318 /* Loop to build the rest of the ADD */ 00319 for (i=n-2; i>=0; i--) { 00320 t1 = t; u1 = u; 00321 v = Cudd_addIte(dd, y[i], t1, u1); 00322 if (v == NULL) { 00323 Cudd_RecursiveDeref(dd, u1); 00324 Cudd_RecursiveDeref(dd, t1); 00325 return(NULL); 00326 } 00327 cuddRef(v); 00328 u = Cudd_addIte(dd, x[i], v, u1); 00329 if (u == NULL) { 00330 Cudd_RecursiveDeref(dd, u1); 00331 Cudd_RecursiveDeref(dd, t1); 00332 Cudd_RecursiveDeref(dd, v); 00333 return(NULL); 00334 } 00335 cuddRef(u); 00336 Cudd_RecursiveDeref(dd, v); 00337 if (i>0) { 00338 w = Cudd_addIte(dd, y[i], u1, t1); 00339 if (u == NULL) { 00340 Cudd_RecursiveDeref(dd, u1); 00341 Cudd_RecursiveDeref(dd, t1); 00342 Cudd_RecursiveDeref(dd, u); 00343 return(NULL); 00344 } 00345 cuddRef(w); 00346 t = Cudd_addIte(dd, x[i], w, t1); 00347 if (u == NULL) { 00348 Cudd_RecursiveDeref(dd, u1); 00349 Cudd_RecursiveDeref(dd, t1); 00350 Cudd_RecursiveDeref(dd, u); 00351 Cudd_RecursiveDeref(dd, w); 00352 return(NULL); 00353 } 00354 cuddRef(t); 00355 Cudd_RecursiveDeref(dd, w); 00356 } 00357 Cudd_RecursiveDeref(dd, u1); 00358 Cudd_RecursiveDeref(dd, t1); 00359 } 00360 00361 cuddDeref(u); 00362 return(u); 00363 00364 } /* end of addWalshInt */
AutomaticStart
Function********************************************************************
Synopsis [Builds an ADD for the residue modulo m of an n-bit number.]
Description [Builds an ADD for the residue modulo m of an n-bit number. The modulus must be at least 2, and the number of bits at least 1. Parameter options specifies whether the MSB should be on top or the LSB; and whther the number whose residue is computed is in two's complement notation or not. The macro CUDD_RESIDUE_DEFAULT specifies LSB on top and unsigned number. The macro CUDD_RESIDUE_MSB specifies MSB on top, and the macro CUDD_RESIDUE_TC specifies two's complement residue. To request MSB on top and two's complement residue simultaneously, one can OR the two macros: CUDD_RESIDUE_MSB | CUDD_RESIDUE_TC. Cudd_addResidue returns a pointer to the resulting ADD if successful; NULL otherwise.]
SideEffects [None]
SeeAlso []
Definition at line 130 of file cuddAddWalsh.c.
00136 { 00137 int msbLsb; /* MSB on top (1) or LSB on top (0) */ 00138 int tc; /* two's complement (1) or unsigned (0) */ 00139 int i, j, k, t, residue, thisOne, previous, index; 00140 DdNode **array[2], *var, *tmp, *res; 00141 00142 /* Sanity check. */ 00143 if (n < 1 && m < 2) return(NULL); 00144 00145 msbLsb = options & CUDD_RESIDUE_MSB; 00146 tc = options & CUDD_RESIDUE_TC; 00147 00148 /* Allocate and initialize working arrays. */ 00149 array[0] = ALLOC(DdNode *,m); 00150 if (array[0] == NULL) { 00151 dd->errorCode = CUDD_MEMORY_OUT; 00152 return(NULL); 00153 } 00154 array[1] = ALLOC(DdNode *,m); 00155 if (array[1] == NULL) { 00156 FREE(array[0]); 00157 dd->errorCode = CUDD_MEMORY_OUT; 00158 return(NULL); 00159 } 00160 for (i = 0; i < m; i++) { 00161 array[0][i] = array[1][i] = NULL; 00162 } 00163 00164 /* Initialize residues. */ 00165 for (i = 0; i < m; i++) { 00166 tmp = cuddUniqueConst(dd,(CUDD_VALUE_TYPE) i); 00167 if (tmp == NULL) { 00168 for (j = 0; j < i; j++) { 00169 Cudd_RecursiveDeref(dd,array[1][j]); 00170 } 00171 FREE(array[0]); 00172 FREE(array[1]); 00173 return(NULL); 00174 } 00175 cuddRef(tmp); 00176 array[1][i] = tmp; 00177 } 00178 00179 /* Main iteration. */ 00180 residue = 1; /* residue of 2**0 */ 00181 for (k = 0; k < n; k++) { 00182 /* Choose current and previous arrays. */ 00183 thisOne = k & 1; 00184 previous = thisOne ^ 1; 00185 /* Build an ADD projection function. */ 00186 if (msbLsb) { 00187 index = top+n-k-1; 00188 } else { 00189 index = top+k; 00190 } 00191 var = cuddUniqueInter(dd,index,DD_ONE(dd),DD_ZERO(dd)); 00192 if (var == NULL) { 00193 for (j = 0; j < m; j++) { 00194 Cudd_RecursiveDeref(dd,array[previous][j]); 00195 } 00196 FREE(array[0]); 00197 FREE(array[1]); 00198 return(NULL); 00199 } 00200 cuddRef(var); 00201 for (i = 0; i < m; i ++) { 00202 t = (i + residue) % m; 00203 tmp = Cudd_addIte(dd,var,array[previous][t],array[previous][i]); 00204 if (tmp == NULL) { 00205 for (j = 0; j < i; j++) { 00206 Cudd_RecursiveDeref(dd,array[thisOne][j]); 00207 } 00208 for (j = 0; j < m; j++) { 00209 Cudd_RecursiveDeref(dd,array[previous][j]); 00210 } 00211 FREE(array[0]); 00212 FREE(array[1]); 00213 return(NULL); 00214 } 00215 cuddRef(tmp); 00216 array[thisOne][i] = tmp; 00217 } 00218 /* One layer completed. Free the other array for the next iteration. */ 00219 for (i = 0; i < m; i++) { 00220 Cudd_RecursiveDeref(dd,array[previous][i]); 00221 } 00222 Cudd_RecursiveDeref(dd,var); 00223 /* Update residue of 2**k. */ 00224 residue = (2 * residue) % m; 00225 /* Adjust residue for MSB, if this is a two's complement number. */ 00226 if (tc && (k == n - 1)) { 00227 residue = (m - residue) % m; 00228 } 00229 } 00230 00231 /* We are only interested in the 0-residue node of the top layer. */ 00232 for (i = 1; i < m; i++) { 00233 Cudd_RecursiveDeref(dd,array[(n - 1) & 1][i]); 00234 } 00235 res = array[(n - 1) & 1][0]; 00236 00237 FREE(array[0]); 00238 FREE(array[1]); 00239 00240 cuddDeref(res); 00241 return(res); 00242 00243 } /* end of Cudd_addResidue */
AutomaticEnd Function********************************************************************
Synopsis [Generates a Walsh matrix in ADD form.]
Description [Generates a Walsh matrix in ADD form. Returns a pointer to the matrixi if successful; NULL otherwise.]
SideEffects [None]
Definition at line 89 of file cuddAddWalsh.c.
00094 { 00095 DdNode *res; 00096 00097 do { 00098 dd->reordered = 0; 00099 res = addWalshInt(dd, x, y, n); 00100 } while (dd->reordered == 1); 00101 return(res); 00102 00103 } /* end of Cudd_addWalsh */
char rcsid [] DD_UNUSED = "$Id: cuddAddWalsh.c,v 1.1.1.1 2003/02/24 22:23:50 wjiang Exp $" [static] |
CFile***********************************************************************
FileName [cuddAddWalsh.c]
PackageName [cudd]
Synopsis [Functions that generate Walsh matrices and residue functions in ADD form.]
Description [External procedures included in this module:
Static 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 53 of file cuddAddWalsh.c.