abc-master
 All Data Structures Namespaces Files Functions Variables Typedefs Enumerations Enumerator Friends Macros
Functions | Variables
cuddAddWalsh.c File Reference
#include "misc/util/util_hack.h"
#include "cuddInt.h"

Go to the source code of this file.

Functions

static DdNode * addWalshInt (DdManager *dd, DdNode **x, DdNode **y, int n)
 
DdNode * Cudd_addWalsh (DdManager *dd, DdNode **x, DdNode **y, int n)
 
DdNode * Cudd_addResidue (DdManager *dd, int n, int m, int options, int top)
 

Variables

static
ABC_NAMESPACE_IMPL_START char
rcsid[] 		DD_UNUSED = "$Id: cuddAddWalsh.c,v 1.10 2008/04/17 21:17:11 fabio Exp $"
 

Function Documentation

static DdNode * addWalshInt ( DdManager *  dd,
DdNode **  x,
DdNode **  y,
int  n 
)
static

AutomaticStart

Function********************************************************************

Synopsis [Implements the recursive step of Cudd_addWalsh.]

Description [Generates a Walsh matrix in ADD form. Returns a pointer to the matrixi if successful; NULL otherwise.]

SideEffects [None]

Definition at line 298 of file cuddAddWalsh.c.

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 */
cuddRef
#define cuddRef(n)
Definition: cuddInt.h:584
cuddDeref
#define cuddDeref(n)
Definition: cuddInt.h:604
Cudd_RecursiveDeref
void Cudd_RecursiveDeref(DdManager *table, DdNode *n)
Definition: cuddRef.c:154
DdNode
Definition: cudd.h:278
cuddUniqueConst
DdNode * cuddUniqueConst(DdManager *unique, CUDD_VALUE_TYPE value)
Definition: cuddTable.c:1450
one
static DdNode * one
Definition: cuddDecomp.c:112
Cudd_addIte
DdNode * Cudd_addIte(DdManager *dd, DdNode *f, DdNode *g, DdNode *h)
Definition: cuddAddIte.c:129
CUDD_VALUE_TYPE
#define CUDD_VALUE_TYPE
Definition: cudd.h:94
DD_ONE
#define DD_ONE(dd)
Definition: cuddInt.h:911
DdNode* Cudd_addResidue ( DdManager *  dd,
int  n,
int  m,
int  options,
int  top 
)

Function********************************************************************

Synopsis [Builds an ADD for the residue modulo m of an n-bit number.]

Description [Builds an ADD for the residue modulo m of an n-bit number. The modulus must be at least 2, and the number of bits at least 1. Parameter options specifies whether the MSB should be on top or the LSB; and whther the number whose residue is computed is in two's complement notation or not. The macro CUDD_RESIDUE_DEFAULT specifies LSB on top and unsigned number. The macro CUDD_RESIDUE_MSB specifies MSB on top, and the macro CUDD_RESIDUE_TC specifies two's complement residue. To request MSB on top and two's complement residue simultaneously, one can OR the two macros: CUDD_RESIDUE_MSB | CUDD_RESIDUE_TC. Cudd_addResidue returns a pointer to the resulting ADD if successful; NULL otherwise.]

SideEffects [None]

SeeAlso []

Definition at line 161 of file cuddAddWalsh.c.

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 */
cuddRef
#define cuddRef(n)
Definition: cuddInt.h:584
cuddDeref
#define cuddDeref(n)
Definition: cuddInt.h:604
Cudd_RecursiveDeref
void Cudd_RecursiveDeref(DdManager *table, DdNode *n)
Definition: cuddRef.c:154
DdNode
Definition: cudd.h:278
cuddUniqueConst
DdNode * cuddUniqueConst(DdManager *unique, CUDD_VALUE_TYPE value)
Definition: cuddTable.c:1450
Minisat::var
int var(Lit p)
Definition: SolverTypes.h:62
ABC_ALLOC
#define ABC_ALLOC(type, num)
Definition: abc_global.h:229
CUDD_RESIDUE_TC
#define CUDD_RESIDUE_TC
Definition: cudd.h:103
Cudd_addIte
DdNode * Cudd_addIte(DdManager *dd, DdNode *f, DdNode *g, DdNode *h)
Definition: cuddAddIte.c:129
CUDD_VALUE_TYPE
#define CUDD_VALUE_TYPE
Definition: cudd.h:94
ABC_FREE
#define ABC_FREE(obj)
Definition: abc_global.h:232
CUDD_RESIDUE_MSB
#define CUDD_RESIDUE_MSB
Definition: cudd.h:102
DD_ONE
#define DD_ONE(dd)
Definition: cuddInt.h:911
DdManager::errorCode
Cudd_ErrorType errorCode
Definition: cuddInt.h:447
cuddUniqueInter
DdNode * cuddUniqueInter(DdManager *unique, int index, DdNode *T, DdNode *E)
Definition: cuddTable.c:1128
DD_ZERO
#define DD_ZERO(dd)
Definition: cuddInt.h:927
DdNode* Cudd_addWalsh ( DdManager *  dd,
DdNode **  x,
DdNode **  y,
int  n 
)

AutomaticEnd Function********************************************************************

Synopsis [Generates a Walsh matrix in ADD form.]

Description [Generates a Walsh matrix in ADD form. Returns a pointer to the matrixi if successful; NULL otherwise.]

SideEffects [None]

Definition at line 120 of file cuddAddWalsh.c.

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 */
DdNode
Definition: cudd.h:278
DdManager::reordered
int reordered
Definition: cuddInt.h:409
addWalshInt
static DdNode * addWalshInt(DdManager *dd, DdNode **x, DdNode **y, int n)
Definition: cuddAddWalsh.c:298

Variable Documentation

ABC_NAMESPACE_IMPL_START char rcsid [] DD_UNUSED = "$Id: cuddAddWalsh.c,v 1.10 2008/04/17 21:17:11 fabio Exp $"
static

CFile***********************************************************************

FileName [cuddAddWalsh.c]

PackageName [cudd]

Synopsis [Functions that generate Walsh matrices and residue functions in ADD form.]

Description [External procedures included in this module:

Static procedures included in this module:

]

Author [Fabio Somenzi]

Copyright [Copyright (c) 1995-2004, Regents of the University of Colorado

All rights reserved.

Redistribution and use in source and binary forms, with or without modification, are permitted provided that the following conditions are met:

Redistributions of source code must retain the above copyright notice, this list of conditions and the following disclaimer.

Redistributions in binary form must reproduce the above copyright notice, this list of conditions and the following disclaimer in the documentation and/or other materials provided with the distribution.

Neither the name of the University of Colorado nor the names of its contributors may be used to endorse or promote products derived from this software without specific prior written permission.

THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT OWNER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.]

Definition at line 84 of file cuddAddWalsh.c.