summaryrefslogtreecommitdiffstats
path: root/src/bdd/cudd/cuddAddWalsh.c
diff options
context:
space:
mode:
Diffstat (limited to 'src/bdd/cudd/cuddAddWalsh.c')
-rw-r--r--src/bdd/cudd/cuddAddWalsh.c301
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
generated by cgit v1.2.3 (git 2.25.1) at 2024-08-18 07:15:35 +0000