src/cuBdd/cuddAddWalsh.c File Reference
#include "util.h"#include "cuddInt.h"
Go to the source code of this file.
Functions | |
| static DdNode * | addWalshInt (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) |
Variables | |
| static char rcsid[] | DD_UNUSED = "$Id: cuddAddWalsh.c,v 1.10 2008/04/17 21:17:11 fabio Exp $" |
Function Documentation
AutomaticStart
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 294 of file cuddAddWalsh.c.
00299 { 00300 DdNode *one, *minusone; 00301 DdNode *t, *u, *t1, *u1, *v, *w; 00302 int i; 00303 00304 one = DD_ONE(dd); 00305 if (n == 0) return(one); 00306 00307 /* Build bottom part of ADD outside loop */ 00308 minusone = cuddUniqueConst(dd,(CUDD_VALUE_TYPE) -1); 00309 if (minusone == NULL) return(NULL); 00310 cuddRef(minusone); 00311 v = Cudd_addIte(dd, y[n-1], minusone, one); 00312 if (v == NULL) { 00313 Cudd_RecursiveDeref(dd, minusone); 00314 return(NULL); 00315 } 00316 cuddRef(v); 00317 u = Cudd_addIte(dd, x[n-1], v, one); 00318 if (u == NULL) { 00319 Cudd_RecursiveDeref(dd, minusone); 00320 Cudd_RecursiveDeref(dd, v); 00321 return(NULL); 00322 } 00323 cuddRef(u); 00324 Cudd_RecursiveDeref(dd, v); 00325 if (n>1) { 00326 w = Cudd_addIte(dd, y[n-1], one, minusone); 00327 if (w == NULL) { 00328 Cudd_RecursiveDeref(dd, minusone); 00329 Cudd_RecursiveDeref(dd, u); 00330 return(NULL); 00331 } 00332 cuddRef(w); 00333 t = Cudd_addIte(dd, x[n-1], w, minusone); 00334 if (t == NULL) { 00335 Cudd_RecursiveDeref(dd, minusone); 00336 Cudd_RecursiveDeref(dd, u); 00337 Cudd_RecursiveDeref(dd, w); 00338 return(NULL); 00339 } 00340 cuddRef(t); 00341 Cudd_RecursiveDeref(dd, w); 00342 } 00343 cuddDeref(minusone); /* minusone is in the result; it won't die */ 00344 00345 /* Loop to build the rest of the ADD */ 00346 for (i=n-2; i>=0; i--) { 00347 t1 = t; u1 = u; 00348 v = Cudd_addIte(dd, y[i], t1, u1); 00349 if (v == NULL) { 00350 Cudd_RecursiveDeref(dd, u1); 00351 Cudd_RecursiveDeref(dd, t1); 00352 return(NULL); 00353 } 00354 cuddRef(v); 00355 u = Cudd_addIte(dd, x[i], v, u1); 00356 if (u == NULL) { 00357 Cudd_RecursiveDeref(dd, u1); 00358 Cudd_RecursiveDeref(dd, t1); 00359 Cudd_RecursiveDeref(dd, v); 00360 return(NULL); 00361 } 00362 cuddRef(u); 00363 Cudd_RecursiveDeref(dd, v); 00364 if (i>0) { 00365 w = Cudd_addIte(dd, y[i], u1, t1); 00366 if (w == NULL) { 00367 Cudd_RecursiveDeref(dd, u1); 00368 Cudd_RecursiveDeref(dd, t1); 00369 Cudd_RecursiveDeref(dd, u); 00370 return(NULL); 00371 } 00372 cuddRef(w); 00373 t = Cudd_addIte(dd, x[i], w, t1); 00374 if (u == NULL) { 00375 Cudd_RecursiveDeref(dd, u1); 00376 Cudd_RecursiveDeref(dd, t1); 00377 Cudd_RecursiveDeref(dd, u); 00378 Cudd_RecursiveDeref(dd, w); 00379 return(NULL); 00380 } 00381 cuddRef(t); 00382 Cudd_RecursiveDeref(dd, w); 00383 } 00384 Cudd_RecursiveDeref(dd, u1); 00385 Cudd_RecursiveDeref(dd, t1); 00386 } 00387 00388 cuddDeref(u); 00389 return(u); 00390 00391 } /* end of addWalshInt */
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 157 of file cuddAddWalsh.c.
00163 { 00164 int msbLsb; /* MSB on top (1) or LSB on top (0) */ 00165 int tc; /* two's complement (1) or unsigned (0) */ 00166 int i, j, k, t, residue, thisOne, previous, index; 00167 DdNode **array[2], *var, *tmp, *res; 00168 00169 /* Sanity check. */ 00170 if (n < 1 && m < 2) return(NULL); 00171 00172 msbLsb = options & CUDD_RESIDUE_MSB; 00173 tc = options & CUDD_RESIDUE_TC; 00174 00175 /* Allocate and initialize working arrays. */ 00176 array[0] = ALLOC(DdNode *,m); 00177 if (array[0] == NULL) { 00178 dd->errorCode = CUDD_MEMORY_OUT; 00179 return(NULL); 00180 } 00181 array[1] = ALLOC(DdNode *,m); 00182 if (array[1] == NULL) { 00183 FREE(array[0]); 00184 dd->errorCode = CUDD_MEMORY_OUT; 00185 return(NULL); 00186 } 00187 for (i = 0; i < m; i++) { 00188 array[0][i] = array[1][i] = NULL; 00189 } 00190 00191 /* Initialize residues. */ 00192 for (i = 0; i < m; i++) { 00193 tmp = cuddUniqueConst(dd,(CUDD_VALUE_TYPE) i); 00194 if (tmp == NULL) { 00195 for (j = 0; j < i; j++) { 00196 Cudd_RecursiveDeref(dd,array[1][j]); 00197 } 00198 FREE(array[0]); 00199 FREE(array[1]); 00200 return(NULL); 00201 } 00202 cuddRef(tmp); 00203 array[1][i] = tmp; 00204 } 00205 00206 /* Main iteration. */ 00207 residue = 1; /* residue of 2**0 */ 00208 for (k = 0; k < n; k++) { 00209 /* Choose current and previous arrays. */ 00210 thisOne = k & 1; 00211 previous = thisOne ^ 1; 00212 /* Build an ADD projection function. */ 00213 if (msbLsb) { 00214 index = top+n-k-1; 00215 } else { 00216 index = top+k; 00217 } 00218 var = cuddUniqueInter(dd,index,DD_ONE(dd),DD_ZERO(dd)); 00219 if (var == NULL) { 00220 for (j = 0; j < m; j++) { 00221 Cudd_RecursiveDeref(dd,array[previous][j]); 00222 } 00223 FREE(array[0]); 00224 FREE(array[1]); 00225 return(NULL); 00226 } 00227 cuddRef(var); 00228 for (i = 0; i < m; i ++) { 00229 t = (i + residue) % m; 00230 tmp = Cudd_addIte(dd,var,array[previous][t],array[previous][i]); 00231 if (tmp == NULL) { 00232 for (j = 0; j < i; j++) { 00233 Cudd_RecursiveDeref(dd,array[thisOne][j]); 00234 } 00235 for (j = 0; j < m; j++) { 00236 Cudd_RecursiveDeref(dd,array[previous][j]); 00237 } 00238 FREE(array[0]); 00239 FREE(array[1]); 00240 return(NULL); 00241 } 00242 cuddRef(tmp); 00243 array[thisOne][i] = tmp; 00244 } 00245 /* One layer completed. Free the other array for the next iteration. */ 00246 for (i = 0; i < m; i++) { 00247 Cudd_RecursiveDeref(dd,array[previous][i]); 00248 } 00249 Cudd_RecursiveDeref(dd,var); 00250 /* Update residue of 2**k. */ 00251 residue = (2 * residue) % m; 00252 /* Adjust residue for MSB, if this is a two's complement number. */ 00253 if (tc && (k == n - 1)) { 00254 residue = (m - residue) % m; 00255 } 00256 } 00257 00258 /* We are only interested in the 0-residue node of the top layer. */ 00259 for (i = 1; i < m; i++) { 00260 Cudd_RecursiveDeref(dd,array[(n - 1) & 1][i]); 00261 } 00262 res = array[(n - 1) & 1][0]; 00263 00264 FREE(array[0]); 00265 FREE(array[1]); 00266 00267 cuddDeref(res); 00268 return(res); 00269 00270 } /* 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 116 of file cuddAddWalsh.c.
00121 { 00122 DdNode *res; 00123 00124 do { 00125 dd->reordered = 0; 00126 res = addWalshInt(dd, x, y, n); 00127 } while (dd->reordered == 1); 00128 return(res); 00129 00130 } /* end of Cudd_addWalsh */
Variable Documentation
char rcsid [] DD_UNUSED = "$Id: cuddAddWalsh.c,v 1.10 2008/04/17 21:17:11 fabio 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 [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 80 of file cuddAddWalsh.c.
