abc-master
 All Data Structures Namespaces Files Functions Variables Typedefs Enumerations Enumerator Friends Macros
cuddAddWalsh.c
Go to the documentation of this file.
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 
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 *
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 *
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) {
183  return(NULL);
184  }
185  array[1] = ABC_ALLOC(DdNode *,m);
186  if (array[1] == NULL) {
187  ABC_FREE(array[0]);
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 *
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 
399 
#define cuddRef(n)
Definition: cuddInt.h:584
#define cuddDeref(n)
Definition: cuddInt.h:604
void Cudd_RecursiveDeref(DdManager *table, DdNode *n)
Definition: cuddRef.c:154
Definition: cudd.h:278
DdNode * cuddUniqueConst(DdManager *unique, CUDD_VALUE_TYPE value)
Definition: cuddTable.c:1450
int var(Lit p)
Definition: SolverTypes.h:62
#define ABC_ALLOC(type, num)
Definition: abc_global.h:229
#define CUDD_RESIDUE_TC
Definition: cudd.h:103
int reordered
Definition: cuddInt.h:409
static DdNode * one
Definition: cuddDecomp.c:112
#define ABC_NAMESPACE_IMPL_END
Definition: abc_global.h:108
#define ABC_NAMESPACE_IMPL_START
Definition: abc_global.h:107
DdNode * Cudd_addIte(DdManager *dd, DdNode *f, DdNode *g, DdNode *h)
Definition: cuddAddIte.c:129
#define CUDD_VALUE_TYPE
Definition: cudd.h:94
DdNode * Cudd_addWalsh(DdManager *dd, DdNode **x, DdNode **y, int n)
Definition: cuddAddWalsh.c:120
static ABC_NAMESPACE_IMPL_START char rcsid[] DD_UNUSED
Definition: cuddAddWalsh.c:84
#define ABC_FREE(obj)
Definition: abc_global.h:232
#define CUDD_RESIDUE_MSB
Definition: cudd.h:102
#define DD_ONE(dd)
Definition: cuddInt.h:911
DdNode * Cudd_addResidue(DdManager *dd, int n, int m, int options, int top)
Definition: cuddAddWalsh.c:161
Cudd_ErrorType errorCode
Definition: cuddInt.h:447
DdNode * cuddUniqueInter(DdManager *unique, int index, DdNode *T, DdNode *E)
Definition: cuddTable.c:1128
static DdNode * addWalshInt(DdManager *dd, DdNode **x, DdNode **y, int n)
Definition: cuddAddWalsh.c:298
#define DD_ZERO(dd)
Definition: cuddInt.h:927