diff options
Diffstat (limited to 'abc70930/src/bdd/cudd/cuddAddWalsh.c')
-rw-r--r-- | abc70930/src/bdd/cudd/cuddAddWalsh.c | 364 |
1 files changed, 0 insertions, 364 deletions
diff --git a/abc70930/src/bdd/cudd/cuddAddWalsh.c b/abc70930/src/bdd/cudd/cuddAddWalsh.c deleted file mode 100644 index c6a67e34..00000000 --- a/abc70930/src/bdd/cudd/cuddAddWalsh.c +++ /dev/null @@ -1,364 +0,0 @@ -/**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: - <ul> - <li> Cudd_addWalsh() - <li> Cudd_addResidue() - </ul> - Static procedures included in this module: - <ul> - <li> addWalshInt() - </ul>] - - 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.] - -******************************************************************************/ - -#include "util_hack.h" -#include "cuddInt.h" - - -/*---------------------------------------------------------------------------*/ -/* Constant declarations */ -/*---------------------------------------------------------------------------*/ - - -/*---------------------------------------------------------------------------*/ -/* Stucture declarations */ -/*---------------------------------------------------------------------------*/ - - -/*---------------------------------------------------------------------------*/ -/* Type declarations */ -/*---------------------------------------------------------------------------*/ - - -/*---------------------------------------------------------------------------*/ -/* Variable declarations */ -/*---------------------------------------------------------------------------*/ - -#ifndef lint -static char rcsid[] DD_UNUSED = "$Id: cuddAddWalsh.c,v 1.1.1.1 2003/02/24 22:23:50 wjiang Exp $"; -#endif - - -/*---------------------------------------------------------------------------*/ -/* Macro declarations */ -/*---------------------------------------------------------------------------*/ - - -/**AutomaticStart*************************************************************/ - -/*---------------------------------------------------------------------------*/ -/* Static function prototypes */ -/*---------------------------------------------------------------------------*/ - -static DdNode * addWalshInt ARGS((DdManager *dd, DdNode **x, DdNode **y, int n)); - -/**AutomaticEnd***************************************************************/ - - -/*---------------------------------------------------------------------------*/ -/* Definition of exported functions */ -/*---------------------------------------------------------------------------*/ - - -/**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] - -******************************************************************************/ -DdNode * -Cudd_addWalsh( - DdManager * dd, - DdNode ** x, - DdNode ** y, - int n) -{ - DdNode *res; - - do { - dd->reordered = 0; - res = addWalshInt(dd, x, y, n); - } while (dd->reordered == 1); - return(res); - -} /* end of Cudd_addWalsh */ - - -/**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 [] - -******************************************************************************/ -DdNode * -Cudd_addResidue( - DdManager * dd /* manager */, - int n /* number of bits */, - int m /* modulus */, - int options /* options */, - int top /* index of top variable */) -{ - int msbLsb; /* MSB on top (1) or LSB on top (0) */ - int tc; /* two's complement (1) or unsigned (0) */ - int i, j, k, t, residue, thisOne, previous, index; - DdNode **array[2], *var, *tmp, *res; - - /* Sanity check. */ - if (n < 1 && m < 2) return(NULL); - - msbLsb = options & CUDD_RESIDUE_MSB; - tc = options & CUDD_RESIDUE_TC; - - /* Allocate and initialize working arrays. */ - array[0] = ALLOC(DdNode *,m); - if (array[0] == NULL) { - dd->errorCode = CUDD_MEMORY_OUT; - return(NULL); - } - array[1] = ALLOC(DdNode *,m); - if (array[1] == NULL) { - FREE(array[0]); - dd->errorCode = CUDD_MEMORY_OUT; - return(NULL); - } - for (i = 0; i < m; i++) { - array[0][i] = array[1][i] = NULL; - } - - /* Initialize residues. */ - for (i = 0; i < m; i++) { - tmp = cuddUniqueConst(dd,(CUDD_VALUE_TYPE) i); - if (tmp == NULL) { - for (j = 0; j < i; j++) { - Cudd_RecursiveDeref(dd,array[1][j]); - } - FREE(array[0]); - FREE(array[1]); - return(NULL); - } - cuddRef(tmp); - array[1][i] = tmp; - } - - /* Main iteration. */ - residue = 1; /* residue of 2**0 */ - for (k = 0; k < n; k++) { - /* Choose current and previous arrays. */ - thisOne = k & 1; - previous = thisOne ^ 1; - /* Build an ADD projection function. */ - if (msbLsb) { - index = top+n-k-1; - } else { - index = top+k; - } - var = cuddUniqueInter(dd,index,DD_ONE(dd),DD_ZERO(dd)); - if (var == NULL) { - for (j = 0; j < m; j++) { - Cudd_RecursiveDeref(dd,array[previous][j]); - } - FREE(array[0]); - FREE(array[1]); - return(NULL); - } - cuddRef(var); - for (i = 0; i < m; i ++) { - t = (i + residue) % m; - tmp = Cudd_addIte(dd,var,array[previous][t],array[previous][i]); - if (tmp == NULL) { - for (j = 0; j < i; j++) { - Cudd_RecursiveDeref(dd,array[thisOne][j]); - } - for (j = 0; j < m; j++) { - Cudd_RecursiveDeref(dd,array[previous][j]); - } - FREE(array[0]); - FREE(array[1]); - return(NULL); - } - cuddRef(tmp); - array[thisOne][i] = tmp; - } - /* One layer completed. Free the other array for the next iteration. */ - for (i = 0; i < m; i++) { - Cudd_RecursiveDeref(dd,array[previous][i]); - } - Cudd_RecursiveDeref(dd,var); - /* Update residue of 2**k. */ - residue = (2 * residue) % m; - /* Adjust residue for MSB, if this is a two's complement number. */ - if (tc && (k == n - 1)) { - residue = (m - residue) % m; - } - } - - /* We are only interested in the 0-residue node of the top layer. */ - for (i = 1; i < m; i++) { - Cudd_RecursiveDeref(dd,array[(n - 1) & 1][i]); - } - res = array[(n - 1) & 1][0]; - - FREE(array[0]); - FREE(array[1]); - - cuddDeref(res); - return(res); - -} /* end of Cudd_addResidue */ - - -/*---------------------------------------------------------------------------*/ -/* Definition of internal functions */ -/*---------------------------------------------------------------------------*/ - - -/*---------------------------------------------------------------------------*/ -/* Definition of static functions */ -/*---------------------------------------------------------------------------*/ - - -/**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] - -******************************************************************************/ -static DdNode * -addWalshInt( - DdManager * dd, - DdNode ** x, - DdNode ** y, - int n) -{ - DdNode *one, *minusone; - DdNode *t, *u, *t1, *u1, *v, *w; - int i; - - one = DD_ONE(dd); - if (n == 0) return(one); - - /* Build bottom part of ADD outside loop */ - minusone = cuddUniqueConst(dd,(CUDD_VALUE_TYPE) -1); - if (minusone == NULL) return(NULL); - cuddRef(minusone); - v = Cudd_addIte(dd, y[n-1], minusone, one); - if (v == NULL) { - Cudd_RecursiveDeref(dd, minusone); - return(NULL); - } - cuddRef(v); - u = Cudd_addIte(dd, x[n-1], v, one); - if (u == NULL) { - Cudd_RecursiveDeref(dd, minusone); - Cudd_RecursiveDeref(dd, v); - return(NULL); - } - cuddRef(u); - Cudd_RecursiveDeref(dd, v); - if (n>1) { - w = Cudd_addIte(dd, y[n-1], one, minusone); - if (w == NULL) { - Cudd_RecursiveDeref(dd, minusone); - Cudd_RecursiveDeref(dd, u); - return(NULL); - } - cuddRef(w); - t = Cudd_addIte(dd, x[n-1], w, minusone); - if (t == NULL) { - Cudd_RecursiveDeref(dd, minusone); - Cudd_RecursiveDeref(dd, u); - Cudd_RecursiveDeref(dd, w); - return(NULL); - } - cuddRef(t); - Cudd_RecursiveDeref(dd, w); - } - cuddDeref(minusone); /* minusone is in the result; it won't die */ - - /* Loop to build the rest of the ADD */ - for (i=n-2; i>=0; i--) { - t1 = t; u1 = u; - v = Cudd_addIte(dd, y[i], t1, u1); - if (v == NULL) { - Cudd_RecursiveDeref(dd, u1); - Cudd_RecursiveDeref(dd, t1); - return(NULL); - } - cuddRef(v); - u = Cudd_addIte(dd, x[i], v, u1); - if (u == NULL) { - Cudd_RecursiveDeref(dd, u1); - Cudd_RecursiveDeref(dd, t1); - Cudd_RecursiveDeref(dd, v); - return(NULL); - } - cuddRef(u); - Cudd_RecursiveDeref(dd, v); - if (i>0) { - w = Cudd_addIte(dd, y[i], u1, t1); - if (u == NULL) { - Cudd_RecursiveDeref(dd, u1); - Cudd_RecursiveDeref(dd, t1); - Cudd_RecursiveDeref(dd, u); - return(NULL); - } - cuddRef(w); - t = Cudd_addIte(dd, x[i], w, t1); - if (u == NULL) { - Cudd_RecursiveDeref(dd, u1); - Cudd_RecursiveDeref(dd, t1); - Cudd_RecursiveDeref(dd, u); - Cudd_RecursiveDeref(dd, w); - return(NULL); - } - cuddRef(t); - Cudd_RecursiveDeref(dd, w); - } - Cudd_RecursiveDeref(dd, u1); - Cudd_RecursiveDeref(dd, t1); - } - - cuddDeref(u); - return(u); - -} /* end of addWalshInt */ |