src/bdd/cudd/cuddAddWalsh.c File Reference

#include "util_hack.h"
#include "cuddInt.h"
Include dependency graph for cuddAddWalsh.c:

Go to the source code of this file.

Functions

static DdNode *addWalshInt ARGS ((DdManager *dd, DdNode **x, DdNode **y, int n))
DdNodeCudd_addWalsh (DdManager *dd, DdNode **x, DdNode **y, int n)
DdNodeCudd_addResidue (DdManager *dd, int n, int m, int options, int top)
static DdNodeaddWalshInt (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 Documentation

static DdNode* addWalshInt ( DdManager dd,
DdNode **  x,
DdNode **  y,
int  n 
) [static]

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 */

static DdNode* addWalshInt ARGS ( (DdManager *dd, DdNode **x, DdNode **y, int n)   )  [static]

AutomaticStart

DdNode* Cudd_addResidue ( DdManager dd,
int  n,
int  m,
int  options,
int  top 
)

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 */

DdNode* Cudd_addWalsh ( DdManager dd,
DdNode **  x,
DdNode **  y,
int  n 
)

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 */


Variable Documentation

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.


Generated on Tue Jan 5 12:18:52 2010 for abc70930 by  doxygen 1.6.1