diff options
Diffstat (limited to 'src/bdd/cudd/cuddAddWalsh.c')
-rw-r--r-- | src/bdd/cudd/cuddAddWalsh.c | 301 |
1 files changed, 165 insertions, 136 deletions
diff --git a/src/bdd/cudd/cuddAddWalsh.c b/src/bdd/cudd/cuddAddWalsh.c index 44b4415d..e8e8a641 100644 --- a/src/bdd/cudd/cuddAddWalsh.c +++ b/src/bdd/cudd/cuddAddWalsh.c @@ -8,21 +8,48 @@ 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>] + <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.] + 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.] ******************************************************************************/ @@ -33,6 +60,7 @@ ABC_NAMESPACE_IMPL_START + /*---------------------------------------------------------------------------*/ /* Constant declarations */ /*---------------------------------------------------------------------------*/ @@ -53,7 +81,7 @@ ABC_NAMESPACE_IMPL_START /*---------------------------------------------------------------------------*/ #ifndef lint -static char rcsid[] DD_UNUSED = "$Id: cuddAddWalsh.c,v 1.1.1.1 2003/02/24 22:23:50 wjiang Exp $"; +static char rcsid[] DD_UNUSED = "$Id: cuddAddWalsh.c,v 1.10 2008/04/17 21:17:11 fabio Exp $"; #endif @@ -68,7 +96,7 @@ static char rcsid[] DD_UNUSED = "$Id: cuddAddWalsh.c,v 1.1.1.1 2003/02/24 22:23: /* Static function prototypes */ /*---------------------------------------------------------------------------*/ -static DdNode * addWalshInt ARGS((DdManager *dd, DdNode **x, DdNode **y, int n)); +static DdNode * addWalshInt (DdManager *dd, DdNode **x, DdNode **y, int n); /**AutomaticEnd***************************************************************/ @@ -98,8 +126,8 @@ Cudd_addWalsh( DdNode *res; do { - dd->reordered = 0; - res = addWalshInt(dd, x, y, n); + dd->reordered = 0; + res = addWalshInt(dd, x, y, n); } while (dd->reordered == 1); return(res); @@ -137,8 +165,8 @@ Cudd_addResidue( 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 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; @@ -151,89 +179,89 @@ Cudd_addResidue( /* Allocate and initialize working arrays. */ array[0] = ABC_ALLOC(DdNode *,m); if (array[0] == NULL) { - dd->errorCode = CUDD_MEMORY_OUT; - return(NULL); + dd->errorCode = CUDD_MEMORY_OUT; + return(NULL); } array[1] = ABC_ALLOC(DdNode *,m); if (array[1] == NULL) { - ABC_FREE(array[0]); - dd->errorCode = CUDD_MEMORY_OUT; - return(NULL); + ABC_FREE(array[0]); + dd->errorCode = CUDD_MEMORY_OUT; + return(NULL); } for (i = 0; i < m; i++) { - array[0][i] = array[1][i] = NULL; + 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]); + tmp = cuddUniqueConst(dd,(CUDD_VALUE_TYPE) i); + if (tmp == NULL) { + for (j = 0; j < i; j++) { + Cudd_RecursiveDeref(dd,array[1][j]); + } + ABC_FREE(array[0]); + ABC_FREE(array[1]); + return(NULL); } - ABC_FREE(array[0]); - ABC_FREE(array[1]); - return(NULL); - } - cuddRef(tmp); - array[1][i] = tmp; + cuddRef(tmp); + array[1][i] = tmp; } /* Main iteration. */ - residue = 1; /* residue of 2**0 */ + 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]); + /* 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; } - ABC_FREE(array[0]); - ABC_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]); + 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]); + } + ABC_FREE(array[0]); + ABC_FREE(array[1]); + return(NULL); } - for (j = 0; j < m; j++) { - Cudd_RecursiveDeref(dd,array[previous][j]); + 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]); + } + ABC_FREE(array[0]); + ABC_FREE(array[1]); + return(NULL); + } + cuddRef(tmp); + array[thisOne][i] = tmp; } - ABC_FREE(array[0]); - ABC_FREE(array[1]); - return(NULL); + /* 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; } - 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]); + Cudd_RecursiveDeref(dd,array[(n - 1) & 1][i]); } res = array[(n - 1) & 1][0]; @@ -274,8 +302,7 @@ addWalshInt( int n) { DdNode *one, *minusone; - DdNode *t = NULL; // Suppress "might be used uninitialized" - DdNode *u, *t1, *u1, *v, *w; + DdNode *t, *u, *t1, *u1, *v, *w; int i; one = DD_ONE(dd); @@ -287,84 +314,86 @@ addWalshInt( cuddRef(minusone); v = Cudd_addIte(dd, y[n-1], minusone, one); if (v == NULL) { - Cudd_RecursiveDeref(dd, minusone); - return(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); + 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); + 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); - 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); + 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(w); - t = Cudd_addIte(dd, x[i], w, t1); + 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 (w == 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); - 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 */ + + ABC_NAMESPACE_IMPL_END |