distr/cudd/cuddAddWalsh.c

   1 /**CFile***********************************************************************
   2
   3   FileName    [cuddAddWalsh.c]
   4
   5   PackageName [cudd]
   6
   7   Synopsis    [Functions that generate Walsh matrices and residue
   8   functions in ADD form.]
   9
  10   Description [External procedures included in this module:
  11             <ul>
  12             <li> Cudd_addWalsh()
  13             <li> Cudd_addResidue()
  14             </ul>
  15         Static procedures included in this module:
  16             <ul>
  17             <li> addWalshInt()
  18             </ul>]
  19
  20   Author      [Fabio Somenzi]
  21
  22   Copyright   [Copyright (c) 1995-2004, Regents of the University of Colorado
  23
  24   All rights reserved.
  25
  26   Redistribution and use in source and binary forms, with or without
  27   modification, are permitted provided that the following conditions
  28   are met:
  29
  30   Redistributions of source code must retain the above copyright
  31   notice, this list of conditions and the following disclaimer.
  32
  33   Redistributions in binary form must reproduce the above copyright
  34   notice, this list of conditions and the following disclaimer in the
  35   documentation and/or other materials provided with the distribution.
  36
  37   Neither the name of the University of Colorado nor the names of its
  38   contributors may be used to endorse or promote products derived from
  39   this software without specific prior written permission.
  40
  41   THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS
  42   "AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT
  43   LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS
  44   FOR A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE
  45   COPYRIGHT OWNER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT,
  46   INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING,
  47   BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES;
  48   LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER
  49   CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT
  50   LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN
  51   ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE
  52   POSSIBILITY OF SUCH DAMAGE.]
  53
  54 ******************************************************************************/
  55
  56 #include "util.h"
  57 #include "cuddInt.h"
  58
  59
  60 /*---------------------------------------------------------------------------*/
  61 /* Constant declarations                                                     */
  62 /*---------------------------------------------------------------------------*/
  63
  64
  65 /*---------------------------------------------------------------------------*/
  66 /* Stucture declarations                                                     */
  67 /*---------------------------------------------------------------------------*/
  68
  69
  70 /*---------------------------------------------------------------------------*/
  71 /* Type declarations                                                         */
  72 /*---------------------------------------------------------------------------*/
  73
  74
  75 /*---------------------------------------------------------------------------*/
  76 /* Variable declarations                                                     */
  77 /*---------------------------------------------------------------------------*/
  78
  79 #ifndef lint
  80 static char rcsid[] DD_UNUSED = "$Id: cuddAddWalsh.c,v 1.10 2008/04/17 21:17:11 fabio Exp $";
  81 #endif
  82
  83
  84 /*---------------------------------------------------------------------------*/
  85 /* Macro declarations                                                        */
  86 /*---------------------------------------------------------------------------*/
  87
  88
  89 /**AutomaticStart*************************************************************/
  90
  91 /*---------------------------------------------------------------------------*/
  92 /* Static function prototypes                                                */
  93 /*---------------------------------------------------------------------------*/
  94
  95 static DdNode * addWalshInt (DdManager *dd, DdNode **x, DdNode **y, int n);
  96
  97 /**AutomaticEnd***************************************************************/
  98
  99
 100 /*---------------------------------------------------------------------------*/
 101 /* Definition of exported functions                                          */
 102 /*---------------------------------------------------------------------------*/
 103
 104
 105 /**Function********************************************************************
 106
 107   Synopsis    [Generates a Walsh matrix in ADD form.]
 108
 109   Description [Generates a Walsh matrix in ADD form. Returns a pointer
 110   to the matrixi if successful; NULL otherwise.]
 111
 112   SideEffects [None]
 113
 114 ******************************************************************************/
 115 DdNode *
 116 Cudd_addWalsh(
 117   DdManager * dd,
 118   DdNode ** x,
 119   DdNode ** y,
 120   int  n)
 121 {
 122     DdNode *res;
 123
 124     do {
 125         dd->reordered = 0;
 126         res = addWalshInt(dd, x, y, n);
 127     } while (dd->reordered == 1);
 128     return(res);
 129
 130 } /* end of Cudd_addWalsh */
 131
 132
 133 /**Function********************************************************************
 134
 135   Synopsis    [Builds an ADD for the residue modulo m of an n-bit
 136   number.]
 137
 138   Description [Builds an ADD for the residue modulo m of an n-bit
 139   number. The modulus must be at least 2, and the number of bits at
 140   least 1. Parameter options specifies whether the MSB should be on top
 141   or the LSB; and whther the number whose residue is computed is in
 142   two's complement notation or not. The macro CUDD_RESIDUE_DEFAULT
 143   specifies LSB on top and unsigned number. The macro CUDD_RESIDUE_MSB
 144   specifies MSB on top, and the macro CUDD_RESIDUE_TC specifies two's
 145   complement residue. To request MSB on top and two's complement residue
 146   simultaneously, one can OR the two macros:
 147   CUDD_RESIDUE_MSB | CUDD_RESIDUE_TC.
 148   Cudd_addResidue returns a pointer to the resulting ADD if successful;
 149   NULL otherwise.]
 150
 151   SideEffects [None]
 152
 153   SeeAlso     []
 154
 155 ******************************************************************************/
 156 DdNode *
 157 Cudd_addResidue(
 158   DdManager * dd /* manager */,
 159   int  n /* number of bits */,
 160   int  m /* modulus */,
 161   int  options /* options */,
 162   int  top /* index of top variable */)
 163 {
 164     int msbLsb; /* MSB on top (1) or LSB on top (0) */
 165     int tc;     /* two's complement (1) or unsigned (0) */
 166     int i, j, k, t, residue, thisOne, previous, index;
 167     DdNode **array[2], *var, *tmp, *res;
 168
 169     /* Sanity check. */
 170     if (n < 1 && m < 2) return(NULL);
 171
 172     msbLsb = options & CUDD_RESIDUE_MSB;
 173     tc = options & CUDD_RESIDUE_TC;
 174
 175     /* Allocate and initialize working arrays. */
 176     array[0] = ALLOC(DdNode *,m);
 177     if (array[0] == NULL) {
 178         dd->errorCode = CUDD_MEMORY_OUT;
 179         return(NULL);
 180     }
 181     array[1] = ALLOC(DdNode *,m);
 182     if (array[1] == NULL) {
 183         FREE(array[0]);
 184         dd->errorCode = CUDD_MEMORY_OUT;
 185         return(NULL);
 186     }
 187     for (i = 0; i < m; i++) {
 188         array[0][i] = array[1][i] = NULL;
 189     }
 190
 191     /* Initialize residues. */
 192     for (i = 0; i < m; i++) {
 193         tmp = cuddUniqueConst(dd,(CUDD_VALUE_TYPE) i);
 194         if (tmp == NULL) {
 195             for (j = 0; j < i; j++) {
 196                 Cudd_RecursiveDeref(dd,array[1][j]);
 197             }
 198             FREE(array[0]);
 199             FREE(array[1]);
 200             return(NULL);
 201         }
 202         cuddRef(tmp);
 203         array[1][i] = tmp;
 204     }
 205
 206     /* Main iteration. */
 207     residue = 1;        /* residue of 2**0 */
 208     for (k = 0; k < n; k++) {
 209         /* Choose current and previous arrays. */
 210         thisOne = k & 1;
 211         previous = thisOne ^ 1;
 212         /* Build an ADD projection function. */
 213         if (msbLsb) {
 214             index = top+n-k-1;
 215         } else {
 216             index = top+k;
 217         }
 218         var = cuddUniqueInter(dd,index,DD_ONE(dd),DD_ZERO(dd));
 219         if (var == NULL) {
 220             for (j = 0; j < m; j++) {
 221                 Cudd_RecursiveDeref(dd,array[previous][j]);
 222             }
 223             FREE(array[0]);
 224             FREE(array[1]);
 225             return(NULL);
 226         }
 227         cuddRef(var);
 228         for (i = 0; i < m; i ++) {
 229             t = (i + residue) % m;
 230             tmp = Cudd_addIte(dd,var,array[previous][t],array[previous][i]);
 231             if (tmp == NULL) {
 232                 for (j = 0; j < i; j++) {
 233                     Cudd_RecursiveDeref(dd,array[thisOne][j]);
 234                 }
 235                 for (j = 0; j < m; j++) {
 236                     Cudd_RecursiveDeref(dd,array[previous][j]);
 237                 }
 238                 FREE(array[0]);
 239                 FREE(array[1]);
 240                 return(NULL);
 241             }
 242             cuddRef(tmp);
 243             array[thisOne][i] = tmp;
 244         }
 245         /* One layer completed. Free the other array for the next iteration. */
 246         for (i = 0; i < m; i++) {
 247             Cudd_RecursiveDeref(dd,array[previous][i]);
 248         }
 249         Cudd_RecursiveDeref(dd,var);
 250         /* Update residue of 2**k. */
 251         residue = (2 * residue) % m;
 252         /* Adjust residue for MSB, if this is a two's complement number. */
 253         if (tc && (k == n - 1)) {
 254             residue = (m - residue) % m;
 255         }
 256     }
 257
 258     /* We are only interested in the 0-residue node of the top layer. */
 259     for (i = 1; i < m; i++) {
 260         Cudd_RecursiveDeref(dd,array[(n - 1) & 1][i]);
 261     }
 262     res = array[(n - 1) & 1][0];
 263
 264     FREE(array[0]);
 265     FREE(array[1]);
 266
 267     cuddDeref(res);
 268     return(res);
 269
 270 } /* end of Cudd_addResidue */
 271
 272
 273 /*---------------------------------------------------------------------------*/
 274 /* Definition of internal functions                                          */
 275 /*---------------------------------------------------------------------------*/
 276
 277
 278 /*---------------------------------------------------------------------------*/
 279 /* Definition of static functions                                            */
 280 /*---------------------------------------------------------------------------*/
 281
 282
 283 /**Function********************************************************************
 284
 285   Synopsis    [Implements the recursive step of Cudd_addWalsh.]
 286
 287   Description [Generates a Walsh matrix in ADD form. Returns a pointer
 288   to the matrixi if successful; NULL otherwise.]
 289
 290   SideEffects [None]
 291
 292 ******************************************************************************/
 293 static DdNode *
 294 addWalshInt(
 295   DdManager * dd,
 296   DdNode ** x,
 297   DdNode ** y,
 298   int  n)
 299 {
 300     DdNode *one, *minusone;
 301     DdNode *t, *u, *t1, *u1, *v, *w;
 302     int     i;
 303
 304     one = DD_ONE(dd);
 305     if (n == 0) return(one);
 306
 307     /* Build bottom part of ADD outside loop */
 308     minusone = cuddUniqueConst(dd,(CUDD_VALUE_TYPE) -1);
 309     if (minusone == NULL) return(NULL);
 310     cuddRef(minusone);
 311     v = Cudd_addIte(dd, y[n-1], minusone, one);
 312     if (v == NULL) {
 313         Cudd_RecursiveDeref(dd, minusone);
 314         return(NULL);
 315     }
 316     cuddRef(v);
 317     u = Cudd_addIte(dd, x[n-1], v, one);
 318     if (u == NULL) {
 319         Cudd_RecursiveDeref(dd, minusone);
 320         Cudd_RecursiveDeref(dd, v);
 321         return(NULL);
 322     }
 323     cuddRef(u);
 324     Cudd_RecursiveDeref(dd, v);
 325     if (n>1) {
 326         w = Cudd_addIte(dd, y[n-1], one, minusone);
 327         if (w == NULL) {
 328             Cudd_RecursiveDeref(dd, minusone);
 329             Cudd_RecursiveDeref(dd, u);
 330             return(NULL);
 331         }
 332         cuddRef(w);
 333         t = Cudd_addIte(dd, x[n-1], w, minusone);
 334         if (t == NULL) {
 335             Cudd_RecursiveDeref(dd, minusone);
 336             Cudd_RecursiveDeref(dd, u);
 337             Cudd_RecursiveDeref(dd, w);
 338             return(NULL);
 339         }
 340         cuddRef(t);
 341         Cudd_RecursiveDeref(dd, w);
 342     }
 343     cuddDeref(minusone); /* minusone is in the result; it won't die */
 344
 345     /* Loop to build the rest of the ADD */
 346     for (i=n-2; i>=0; i--) {
 347         t1 = t; u1 = u;
 348         v = Cudd_addIte(dd, y[i], t1, u1);
 349         if (v == NULL) {
 350             Cudd_RecursiveDeref(dd, u1);
 351             Cudd_RecursiveDeref(dd, t1);
 352             return(NULL);
 353         }
 354         cuddRef(v);
 355         u = Cudd_addIte(dd, x[i], v, u1);
 356         if (u == NULL) {
 357             Cudd_RecursiveDeref(dd, u1);
 358             Cudd_RecursiveDeref(dd, t1);
 359             Cudd_RecursiveDeref(dd, v);
 360             return(NULL);
 361         }
 362         cuddRef(u);
 363         Cudd_RecursiveDeref(dd, v);
 364         if (i>0) {
 365             w = Cudd_addIte(dd, y[i], u1, t1);
 366             if (w == NULL) {
 367                 Cudd_RecursiveDeref(dd, u1);
 368                 Cudd_RecursiveDeref(dd, t1);
 369                 Cudd_RecursiveDeref(dd, u);
 370                 return(NULL);
 371             }
 372             cuddRef(w);
 373             t = Cudd_addIte(dd, x[i], w, t1);
 374             if (u == NULL) {
 375                 Cudd_RecursiveDeref(dd, u1);
 376                 Cudd_RecursiveDeref(dd, t1);
 377                 Cudd_RecursiveDeref(dd, u);
 378                 Cudd_RecursiveDeref(dd, w);
 379                 return(NULL);
 380             }
 381             cuddRef(t);
 382             Cudd_RecursiveDeref(dd, w);
 383         }
 384         Cudd_RecursiveDeref(dd, u1);
 385         Cudd_RecursiveDeref(dd, t1);
 386     }
 387
 388     cuddDeref(u);
 389     return(u);
 390
 391 } /* end of addWalshInt */