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 "misc/util/util_hack.h"
57 #include "cuddInt.h"
58
59 ABC_NAMESPACE_IMPL_START
60
61
62
63
64 /*---------------------------------------------------------------------------*/
65 /* Constant declarations */
66 /*---------------------------------------------------------------------------*/
67
68
69 /*---------------------------------------------------------------------------*/
70 /* Stucture declarations */
71 /*---------------------------------------------------------------------------*/
72
73
74 /*---------------------------------------------------------------------------*/
75 /* Type declarations */
76 /*---------------------------------------------------------------------------*/
77
78
79 /*---------------------------------------------------------------------------*/
80 /* Variable declarations */
81 /*---------------------------------------------------------------------------*/
82
83 #ifndef lint
84 static char rcsid[] DD_UNUSED = "$Id: cuddAddWalsh.c,v 1.10 2008/04/17 21:17:11 fabio Exp $";
85 #endif
86
87
88 /*---------------------------------------------------------------------------*/
89 /* Macro declarations */
90 /*---------------------------------------------------------------------------*/
91
92
93 /**AutomaticStart*************************************************************/
94
95 /*---------------------------------------------------------------------------*/
96 /* Static function prototypes */
97 /*---------------------------------------------------------------------------*/
98
99 static DdNode * addWalshInt (DdManager *dd, DdNode **x, DdNode **y, int n);
100
101 /**AutomaticEnd***************************************************************/
102
103
104 /*---------------------------------------------------------------------------*/
105 /* Definition of exported functions */
106 /*---------------------------------------------------------------------------*/
107
108
109 /**Function********************************************************************
110
111 Synopsis [Generates a Walsh matrix in ADD form.]
112
113 Description [Generates a Walsh matrix in ADD form. Returns a pointer
114 to the matrixi if successful; NULL otherwise.]
115
116 SideEffects [None]
117
118 ******************************************************************************/
119 DdNode *
Cudd_addWalsh(DdManager * dd,DdNode ** x,DdNode ** y,int n)120 Cudd_addWalsh(
121 DdManager * dd,
122 DdNode ** x,
123 DdNode ** y,
124 int n)
125 {
126 DdNode *res;
127
128 do {
129 dd->reordered = 0;
130 res = addWalshInt(dd, x, y, n);
131 } while (dd->reordered == 1);
132 return(res);
133
134 } /* end of Cudd_addWalsh */
135
136
137 /**Function********************************************************************
138
139 Synopsis [Builds an ADD for the residue modulo m of an n-bit
140 number.]
141
142 Description [Builds an ADD for the residue modulo m of an n-bit
143 number. The modulus must be at least 2, and the number of bits at
144 least 1. Parameter options specifies whether the MSB should be on top
145 or the LSB; and whther the number whose residue is computed is in
146 two's complement notation or not. The macro CUDD_RESIDUE_DEFAULT
147 specifies LSB on top and unsigned number. The macro CUDD_RESIDUE_MSB
148 specifies MSB on top, and the macro CUDD_RESIDUE_TC specifies two's
149 complement residue. To request MSB on top and two's complement residue
150 simultaneously, one can OR the two macros:
151 CUDD_RESIDUE_MSB | CUDD_RESIDUE_TC.
152 Cudd_addResidue returns a pointer to the resulting ADD if successful;
153 NULL otherwise.]
154
155 SideEffects [None]
156
157 SeeAlso []
158
159 ******************************************************************************/
160 DdNode *
Cudd_addResidue(DdManager * dd,int n,int m,int options,int top)161 Cudd_addResidue(
162 DdManager * dd /* manager */,
163 int n /* number of bits */,
164 int m /* modulus */,
165 int options /* options */,
166 int top /* index of top variable */)
167 {
168 int msbLsb; /* MSB on top (1) or LSB on top (0) */
169 int tc; /* two's complement (1) or unsigned (0) */
170 int i, j, k, t, residue, thisOne, previous, index;
171 DdNode **array[2], *var, *tmp, *res;
172
173 /* Sanity check. */
174 if (n < 1 && m < 2) return(NULL);
175
176 msbLsb = options & CUDD_RESIDUE_MSB;
177 tc = options & CUDD_RESIDUE_TC;
178
179 /* Allocate and initialize working arrays. */
180 array[0] = ABC_ALLOC(DdNode *,m);
181 if (array[0] == NULL) {
182 dd->errorCode = CUDD_MEMORY_OUT;
183 return(NULL);
184 }
185 array[1] = ABC_ALLOC(DdNode *,m);
186 if (array[1] == NULL) {
187 ABC_FREE(array[0]);
188 dd->errorCode = CUDD_MEMORY_OUT;
189 return(NULL);
190 }
191 for (i = 0; i < m; i++) {
192 array[0][i] = array[1][i] = NULL;
193 }
194
195 /* Initialize residues. */
196 for (i = 0; i < m; i++) {
197 tmp = cuddUniqueConst(dd,(CUDD_VALUE_TYPE) i);
198 if (tmp == NULL) {
199 for (j = 0; j < i; j++) {
200 Cudd_RecursiveDeref(dd,array[1][j]);
201 }
202 ABC_FREE(array[0]);
203 ABC_FREE(array[1]);
204 return(NULL);
205 }
206 cuddRef(tmp);
207 array[1][i] = tmp;
208 }
209
210 /* Main iteration. */
211 residue = 1; /* residue of 2**0 */
212 for (k = 0; k < n; k++) {
213 /* Choose current and previous arrays. */
214 thisOne = k & 1;
215 previous = thisOne ^ 1;
216 /* Build an ADD projection function. */
217 if (msbLsb) {
218 index = top+n-k-1;
219 } else {
220 index = top+k;
221 }
222 var = cuddUniqueInter(dd,index,DD_ONE(dd),DD_ZERO(dd));
223 if (var == NULL) {
224 for (j = 0; j < m; j++) {
225 Cudd_RecursiveDeref(dd,array[previous][j]);
226 }
227 ABC_FREE(array[0]);
228 ABC_FREE(array[1]);
229 return(NULL);
230 }
231 cuddRef(var);
232 for (i = 0; i < m; i ++) {
233 t = (i + residue) % m;
234 tmp = Cudd_addIte(dd,var,array[previous][t],array[previous][i]);
235 if (tmp == NULL) {
236 for (j = 0; j < i; j++) {
237 Cudd_RecursiveDeref(dd,array[thisOne][j]);
238 }
239 for (j = 0; j < m; j++) {
240 Cudd_RecursiveDeref(dd,array[previous][j]);
241 }
242 ABC_FREE(array[0]);
243 ABC_FREE(array[1]);
244 return(NULL);
245 }
246 cuddRef(tmp);
247 array[thisOne][i] = tmp;
248 }
249 /* One layer completed. Free the other array for the next iteration. */
250 for (i = 0; i < m; i++) {
251 Cudd_RecursiveDeref(dd,array[previous][i]);
252 }
253 Cudd_RecursiveDeref(dd,var);
254 /* Update residue of 2**k. */
255 residue = (2 * residue) % m;
256 /* Adjust residue for MSB, if this is a two's complement number. */
257 if (tc && (k == n - 1)) {
258 residue = (m - residue) % m;
259 }
260 }
261
262 /* We are only interested in the 0-residue node of the top layer. */
263 for (i = 1; i < m; i++) {
264 Cudd_RecursiveDeref(dd,array[(n - 1) & 1][i]);
265 }
266 res = array[(n - 1) & 1][0];
267
268 ABC_FREE(array[0]);
269 ABC_FREE(array[1]);
270
271 cuddDeref(res);
272 return(res);
273
274 } /* end of Cudd_addResidue */
275
276
277 /*---------------------------------------------------------------------------*/
278 /* Definition of internal functions */
279 /*---------------------------------------------------------------------------*/
280
281
282 /*---------------------------------------------------------------------------*/
283 /* Definition of static functions */
284 /*---------------------------------------------------------------------------*/
285
286
287 /**Function********************************************************************
288
289 Synopsis [Implements the recursive step of Cudd_addWalsh.]
290
291 Description [Generates a Walsh matrix in ADD form. Returns a pointer
292 to the matrixi if successful; NULL otherwise.]
293
294 SideEffects [None]
295
296 ******************************************************************************/
297 static DdNode *
addWalshInt(DdManager * dd,DdNode ** x,DdNode ** y,int n)298 addWalshInt(
299 DdManager * dd,
300 DdNode ** x,
301 DdNode ** y,
302 int n)
303 {
304 DdNode *one, *minusone;
305 DdNode *t = NULL, *u = NULL, *t1, *u1, *v, *w;
306 int i;
307
308 one = DD_ONE(dd);
309 if (n == 0) return(one);
310
311 /* Build bottom part of ADD outside loop */
312 minusone = cuddUniqueConst(dd,(CUDD_VALUE_TYPE) -1);
313 if (minusone == NULL) return(NULL);
314 cuddRef(minusone);
315 v = Cudd_addIte(dd, y[n-1], minusone, one);
316 if (v == NULL) {
317 Cudd_RecursiveDeref(dd, minusone);
318 return(NULL);
319 }
320 cuddRef(v);
321 u = Cudd_addIte(dd, x[n-1], v, one);
322 if (u == NULL) {
323 Cudd_RecursiveDeref(dd, minusone);
324 Cudd_RecursiveDeref(dd, v);
325 return(NULL);
326 }
327 cuddRef(u);
328 Cudd_RecursiveDeref(dd, v);
329 if (n>1) {
330 w = Cudd_addIte(dd, y[n-1], one, minusone);
331 if (w == NULL) {
332 Cudd_RecursiveDeref(dd, minusone);
333 Cudd_RecursiveDeref(dd, u);
334 return(NULL);
335 }
336 cuddRef(w);
337 t = Cudd_addIte(dd, x[n-1], w, minusone);
338 if (t == NULL) {
339 Cudd_RecursiveDeref(dd, minusone);
340 Cudd_RecursiveDeref(dd, u);
341 Cudd_RecursiveDeref(dd, w);
342 return(NULL);
343 }
344 cuddRef(t);
345 Cudd_RecursiveDeref(dd, w);
346 }
347 cuddDeref(minusone); /* minusone is in the result; it won't die */
348
349 /* Loop to build the rest of the ADD */
350 for (i=n-2; i>=0; i--) {
351 t1 = t; u1 = u;
352 v = Cudd_addIte(dd, y[i], t1, u1);
353 if (v == NULL) {
354 Cudd_RecursiveDeref(dd, u1);
355 Cudd_RecursiveDeref(dd, t1);
356 return(NULL);
357 }
358 cuddRef(v);
359 u = Cudd_addIte(dd, x[i], v, u1);
360 if (u == NULL) {
361 Cudd_RecursiveDeref(dd, u1);
362 Cudd_RecursiveDeref(dd, t1);
363 Cudd_RecursiveDeref(dd, v);
364 return(NULL);
365 }
366 cuddRef(u);
367 Cudd_RecursiveDeref(dd, v);
368 if (i>0) {
369 w = Cudd_addIte(dd, y[i], u1, t1);
370 if (w == NULL) {
371 Cudd_RecursiveDeref(dd, u1);
372 Cudd_RecursiveDeref(dd, t1);
373 Cudd_RecursiveDeref(dd, u);
374 return(NULL);
375 }
376 cuddRef(w);
377 t = Cudd_addIte(dd, x[i], w, t1);
378 if (u == NULL) {
379 Cudd_RecursiveDeref(dd, u1);
380 Cudd_RecursiveDeref(dd, t1);
381 Cudd_RecursiveDeref(dd, u);
382 Cudd_RecursiveDeref(dd, w);
383 return(NULL);
384 }
385 cuddRef(t);
386 Cudd_RecursiveDeref(dd, w);
387 }
388 Cudd_RecursiveDeref(dd, u1);
389 Cudd_RecursiveDeref(dd, t1);
390 }
391
392 cuddDeref(u);
393 return(u);
394
395 } /* end of addWalshInt */
396
397
398 ABC_NAMESPACE_IMPL_END
399
400