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.c364
1 files changed, 364 insertions, 0 deletions
diff --git a/src/bdd/cudd/cuddAddWalsh.c b/src/bdd/cudd/cuddAddWalsh.c
new file mode 100644
index 00000000..980ee215
--- /dev/null
+++ b/src/bdd/cudd/cuddAddWalsh.c
@@ -0,0 +1,364 @@
+/**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.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 */
generated by cgit v1.2.3 (git 2.25.1) at 2024-06-30 22:39:39 +0000