source: vis_dev/glu-2.3/src/cuBdd/cuddAddWalsh.c @ 100

Last change on this file since 100 was 13, checked in by cecile, 13 years ago

library glu 2.3
File size: 11.6 KB
Line 
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
80static 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
95static 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******************************************************************************/
115DdNode *
116Cudd_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******************************************************************************/
156DdNode *
157Cudd_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******************************************************************************/
293static DdNode *
294addWalshInt(
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 */
Note: See TracBrowser for help on using the repository browser.