glu-2.2: src/cuBdd/cuddAddWalsh.c Source File

00001 
00056 #include "util.h"
00057 #include "cuddInt.h"
00058 
00059 
00060 /*---------------------------------------------------------------------------*/
00061 /* Constant declarations                                                     */
00062 /*---------------------------------------------------------------------------*/
00063 
00064 
00065 /*---------------------------------------------------------------------------*/
00066 /* Stucture declarations                                                     */
00067 /*---------------------------------------------------------------------------*/
00068 
00069 
00070 /*---------------------------------------------------------------------------*/
00071 /* Type declarations                                                         */
00072 /*---------------------------------------------------------------------------*/
00073 
00074 
00075 /*---------------------------------------------------------------------------*/
00076 /* Variable declarations                                                     */
00077 /*---------------------------------------------------------------------------*/
00078 
00079 #ifndef lint
00080 static char rcsid[] DD_UNUSED = "$Id: cuddAddWalsh.c,v 1.10 2008/04/17 21:17:11 fabio Exp $";
00081 #endif
00082 
00083 
00084 /*---------------------------------------------------------------------------*/
00085 /* Macro declarations                                                        */
00086 /*---------------------------------------------------------------------------*/
00087 
00088 
00091 /*---------------------------------------------------------------------------*/
00092 /* Static function prototypes                                                */
00093 /*---------------------------------------------------------------------------*/
00094 
00095 static DdNode * addWalshInt (DdManager *dd, DdNode **x, DdNode **y, int n);
00096 
00100 /*---------------------------------------------------------------------------*/
00101 /* Definition of exported functions                                          */
00102 /*---------------------------------------------------------------------------*/
00103 
00104 
00115 DdNode *
00116 Cudd_addWalsh(
00117   DdManager * dd,
00118   DdNode ** x,
00119   DdNode ** y,
00120   int  n)
00121 {
00122     DdNode *res;
00123 
00124     do {
00125         dd->reordered = 0;
00126         res = addWalshInt(dd, x, y, n);
00127     } while (dd->reordered == 1);
00128     return(res);
00129 
00130 } /* end of Cudd_addWalsh */
00131 
00132 
00156 DdNode *
00157 Cudd_addResidue(
00158   DdManager * dd /* manager */,
00159   int  n /* number of bits */,
00160   int  m /* modulus */,
00161   int  options /* options */,
00162   int  top /* index of top variable */)
00163 {
00164     int msbLsb; /* MSB on top (1) or LSB on top (0) */
00165     int tc;     /* two's complement (1) or unsigned (0) */
00166     int i, j, k, t, residue, thisOne, previous, index;
00167     DdNode **array[2], *var, *tmp, *res;
00168 
00169     /* Sanity check. */
00170     if (n < 1 && m < 2) return(NULL);
00171 
00172     msbLsb = options & CUDD_RESIDUE_MSB;
00173     tc = options & CUDD_RESIDUE_TC;
00174 
00175     /* Allocate and initialize working arrays. */
00176     array[0] = ALLOC(DdNode *,m);
00177     if (array[0] == NULL) {
00178         dd->errorCode = CUDD_MEMORY_OUT;
00179         return(NULL);
00180     }
00181     array[1] = ALLOC(DdNode *,m);
00182     if (array[1] == NULL) {
00183         FREE(array[0]);
00184         dd->errorCode = CUDD_MEMORY_OUT;
00185         return(NULL);
00186     }
00187     for (i = 0; i < m; i++) {
00188         array[0][i] = array[1][i] = NULL;
00189     }
00190 
00191     /* Initialize residues. */
00192     for (i = 0; i < m; i++) {
00193         tmp = cuddUniqueConst(dd,(CUDD_VALUE_TYPE) i);
00194         if (tmp == NULL) {
00195             for (j = 0; j < i; j++) {
00196                 Cudd_RecursiveDeref(dd,array[1][j]);
00197             }
00198             FREE(array[0]);
00199             FREE(array[1]);
00200             return(NULL);
00201         }
00202         cuddRef(tmp);
00203         array[1][i] = tmp;
00204     }
00205 
00206     /* Main iteration. */
00207     residue = 1;        /* residue of 2**0 */
00208     for (k = 0; k < n; k++) {
00209         /* Choose current and previous arrays. */
00210         thisOne = k & 1;
00211         previous = thisOne ^ 1;
00212         /* Build an ADD projection function. */
00213         if (msbLsb) {
00214             index = top+n-k-1;
00215         } else {
00216             index = top+k;
00217         }
00218         var = cuddUniqueInter(dd,index,DD_ONE(dd),DD_ZERO(dd));
00219         if (var == NULL) {
00220             for (j = 0; j < m; j++) {
00221                 Cudd_RecursiveDeref(dd,array[previous][j]);
00222             }
00223             FREE(array[0]);
00224             FREE(array[1]);
00225             return(NULL);
00226         }
00227         cuddRef(var);
00228         for (i = 0; i < m; i ++) {
00229             t = (i + residue) % m;
00230             tmp = Cudd_addIte(dd,var,array[previous][t],array[previous][i]);
00231             if (tmp == NULL) {
00232                 for (j = 0; j < i; j++) {
00233                     Cudd_RecursiveDeref(dd,array[thisOne][j]);
00234                 }
00235                 for (j = 0; j < m; j++) {
00236                     Cudd_RecursiveDeref(dd,array[previous][j]);
00237                 }
00238                 FREE(array[0]);
00239                 FREE(array[1]);
00240                 return(NULL);
00241             }
00242             cuddRef(tmp);
00243             array[thisOne][i] = tmp;
00244         }
00245         /* One layer completed. Free the other array for the next iteration. */
00246         for (i = 0; i < m; i++) {
00247             Cudd_RecursiveDeref(dd,array[previous][i]);
00248         }
00249         Cudd_RecursiveDeref(dd,var);
00250         /* Update residue of 2**k. */
00251         residue = (2 * residue) % m;
00252         /* Adjust residue for MSB, if this is a two's complement number. */
00253         if (tc && (k == n - 1)) {
00254             residue = (m - residue) % m;
00255         }
00256     }
00257 
00258     /* We are only interested in the 0-residue node of the top layer. */
00259     for (i = 1; i < m; i++) {
00260         Cudd_RecursiveDeref(dd,array[(n - 1) & 1][i]);
00261     }
00262     res = array[(n - 1) & 1][0];
00263 
00264     FREE(array[0]);
00265     FREE(array[1]);
00266 
00267     cuddDeref(res);
00268     return(res);
00269 
00270 } /* end of Cudd_addResidue */
00271 
00272 
00273 /*---------------------------------------------------------------------------*/
00274 /* Definition of internal functions                                          */
00275 /*---------------------------------------------------------------------------*/
00276 
00277 
00278 /*---------------------------------------------------------------------------*/
00279 /* Definition of static functions                                            */
00280 /*---------------------------------------------------------------------------*/
00281 
00282 
00293 static DdNode *
00294 addWalshInt(
00295   DdManager * dd,
00296   DdNode ** x,
00297   DdNode ** y,
00298   int  n)
00299 {
00300     DdNode *one, *minusone;
00301     DdNode *t, *u, *t1, *u1, *v, *w;
00302     int     i;
00303 
00304     one = DD_ONE(dd);
00305     if (n == 0) return(one);
00306 
00307     /* Build bottom part of ADD outside loop */
00308     minusone = cuddUniqueConst(dd,(CUDD_VALUE_TYPE) -1);
00309     if (minusone == NULL) return(NULL);
00310     cuddRef(minusone);
00311     v = Cudd_addIte(dd, y[n-1], minusone, one);
00312     if (v == NULL) {
00313         Cudd_RecursiveDeref(dd, minusone);
00314         return(NULL);
00315     }
00316     cuddRef(v);
00317     u = Cudd_addIte(dd, x[n-1], v, one);
00318     if (u == NULL) {
00319         Cudd_RecursiveDeref(dd, minusone);
00320         Cudd_RecursiveDeref(dd, v);
00321         return(NULL);
00322     }
00323     cuddRef(u);
00324     Cudd_RecursiveDeref(dd, v);
00325     if (n>1) {
00326         w = Cudd_addIte(dd, y[n-1], one, minusone);
00327         if (w == NULL) {
00328             Cudd_RecursiveDeref(dd, minusone);
00329             Cudd_RecursiveDeref(dd, u);
00330             return(NULL);
00331         }
00332         cuddRef(w);
00333         t = Cudd_addIte(dd, x[n-1], w, minusone);
00334         if (t == NULL) {
00335             Cudd_RecursiveDeref(dd, minusone);
00336             Cudd_RecursiveDeref(dd, u);
00337             Cudd_RecursiveDeref(dd, w);
00338             return(NULL);
00339         }
00340         cuddRef(t);
00341         Cudd_RecursiveDeref(dd, w);
00342     }
00343     cuddDeref(minusone); /* minusone is in the result; it won't die */
00344 
00345     /* Loop to build the rest of the ADD */
00346     for (i=n-2; i>=0; i--) {
00347         t1 = t; u1 = u;
00348         v = Cudd_addIte(dd, y[i], t1, u1);
00349         if (v == NULL) {
00350             Cudd_RecursiveDeref(dd, u1);
00351             Cudd_RecursiveDeref(dd, t1);
00352             return(NULL);
00353         }
00354         cuddRef(v);
00355         u = Cudd_addIte(dd, x[i], v, u1);
00356         if (u == NULL) {
00357             Cudd_RecursiveDeref(dd, u1);
00358             Cudd_RecursiveDeref(dd, t1);
00359             Cudd_RecursiveDeref(dd, v);
00360             return(NULL);
00361         }
00362         cuddRef(u);
00363         Cudd_RecursiveDeref(dd, v);
00364         if (i>0) {
00365             w = Cudd_addIte(dd, y[i], u1, t1);
00366             if (w == NULL) {
00367                 Cudd_RecursiveDeref(dd, u1);
00368                 Cudd_RecursiveDeref(dd, t1);
00369                 Cudd_RecursiveDeref(dd, u);
00370                 return(NULL);
00371             }
00372             cuddRef(w);
00373             t = Cudd_addIte(dd, x[i], w, t1);
00374             if (u == NULL) {
00375                 Cudd_RecursiveDeref(dd, u1);
00376                 Cudd_RecursiveDeref(dd, t1);
00377                 Cudd_RecursiveDeref(dd, u);
00378                 Cudd_RecursiveDeref(dd, w);
00379                 return(NULL);
00380             }
00381             cuddRef(t);
00382             Cudd_RecursiveDeref(dd, w);
00383         }
00384         Cudd_RecursiveDeref(dd, u1);
00385         Cudd_RecursiveDeref(dd, t1);
00386     }
00387 
00388     cuddDeref(u);
00389     return(u);
00390 
00391 } /* end of addWalshInt */