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

Go to the source code of this file.

Functions

static int addCheckPositiveCube (DdManager *manager, DdNode *cube)
 
DdNode * Cudd_addExistAbstract (DdManager *manager, DdNode *f, DdNode *cube)
 
DdNode * Cudd_addUnivAbstract (DdManager *manager, DdNode *f, DdNode *cube)
 
DdNode * Cudd_addOrAbstract (DdManager *manager, DdNode *f, DdNode *cube)
 
DdNode * cuddAddExistAbstractRecur (DdManager *manager, DdNode *f, DdNode *cube)
 
DdNode * cuddAddUnivAbstractRecur (DdManager *manager, DdNode *f, DdNode *cube)
 
DdNode * cuddAddOrAbstractRecur (DdManager *manager, DdNode *f, DdNode *cube)
 

Variables

static
ABC_NAMESPACE_IMPL_START char
rcsid[] 		DD_UNUSED = "$Id: cuddAddAbs.c,v 1.15 2004/08/13 18:04:45 fabio Exp $"
 
static DdNode * two
 

Function Documentation

static int addCheckPositiveCube ( DdManager *  manager,
DdNode *  cube 
)
static

AutomaticStart

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

Synopsis [Checks whether cube is an ADD representing the product of positive literals.]

Description [Checks whether cube is an ADD representing the product of positive literals. Returns 1 in case of success; 0 otherwise.]

SideEffects [None]

SeeAlso []

Definition at line 570 of file cuddAddAbs.c.

573 {
574  if (Cudd_IsComplement(cube)) return(0);
575  if (cube == DD_ONE(manager)) return(1);
576  if (cuddIsConstant(cube)) return(0);
577  if (cuddE(cube) == DD_ZERO(manager)) {
578  return(addCheckPositiveCube(manager, cuddT(cube)));
579  }
580  return(0);
581 
582 } /* end of addCheckPositiveCube */
Cudd_IsComplement
#define Cudd_IsComplement(node)
Definition: cudd.h:425
cuddIsConstant
#define cuddIsConstant(node)
Definition: cuddInt.h:620
cuddT
#define cuddT(node)
Definition: cuddInt.h:636
addCheckPositiveCube
static int addCheckPositiveCube(DdManager *manager, DdNode *cube)
Definition: cuddAddAbs.c:570
cuddE
#define cuddE(node)
Definition: cuddInt.h:652
DD_ONE
#define DD_ONE(dd)
Definition: cuddInt.h:911
DD_ZERO
#define DD_ZERO(dd)
Definition: cuddInt.h:927
DdNode* Cudd_addExistAbstract ( DdManager *  manager,
DdNode *  f,
DdNode *  cube 
)

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

Synopsis [Existentially Abstracts all the variables in cube from f.]

Description [Abstracts all the variables in cube from f by summing over all possible values taken by the variables. Returns the abstracted ADD.]

SideEffects [None]

SeeAlso [Cudd_addUnivAbstract Cudd_bddExistAbstract Cudd_addOrAbstract]

Definition at line 129 of file cuddAddAbs.c.

133 {
134  DdNode *res;
135 
136  two = cuddUniqueConst(manager,(CUDD_VALUE_TYPE) 2);
137  if (two == NULL) return(NULL);
138  cuddRef(two);
139 
140  if (addCheckPositiveCube(manager, cube) == 0) {
141  (void) fprintf(manager->err,"Error: Can only abstract cubes");
142  return(NULL);
143  }
144 
145  do {
146  manager->reordered = 0;
147  res = cuddAddExistAbstractRecur(manager, f, cube);
148  } while (manager->reordered == 1);
149 
150  if (res == NULL) {
151  Cudd_RecursiveDeref(manager,two);
152  return(NULL);
153  }
154  cuddRef(res);
155  Cudd_RecursiveDeref(manager,two);
156  cuddDeref(res);
157 
158  return(res);
159 
160 } /* end of Cudd_addExistAbstract */
cuddRef
#define cuddRef(n)
Definition: cuddInt.h:584
two
static DdNode * two
Definition: cuddAddAbs.c:92
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
DdManager::err
FILE * err
Definition: cuddInt.h:442
cuddAddExistAbstractRecur
DdNode * cuddAddExistAbstractRecur(DdManager *manager, DdNode *f, DdNode *cube)
Definition: cuddAddAbs.c:256
DdManager::reordered
int reordered
Definition: cuddInt.h:409
CUDD_VALUE_TYPE
#define CUDD_VALUE_TYPE
Definition: cudd.h:94
addCheckPositiveCube
static int addCheckPositiveCube(DdManager *manager, DdNode *cube)
Definition: cuddAddAbs.c:570
DdNode* Cudd_addOrAbstract ( DdManager *  manager,
DdNode *  f,
DdNode *  cube 
)

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

Synopsis [Disjunctively abstracts all the variables in cube from the 0-1 ADD f.]

Description [Abstracts all the variables in cube from the 0-1 ADD f by taking the disjunction over all possible values taken by the variables. Returns the abstracted ADD if successful; NULL otherwise.]

SideEffects [None]

SeeAlso [Cudd_addUnivAbstract Cudd_addExistAbstract]

Definition at line 216 of file cuddAddAbs.c.

220 {
221  DdNode *res;
222 
223  if (addCheckPositiveCube(manager, cube) == 0) {
224  (void) fprintf(manager->err,"Error: Can only abstract cubes");
225  return(NULL);
226  }
227 
228  do {
229  manager->reordered = 0;
230  res = cuddAddOrAbstractRecur(manager, f, cube);
231  } while (manager->reordered == 1);
232  return(res);
233 
234 } /* end of Cudd_addOrAbstract */
DdNode
Definition: cudd.h:278
DdManager::err
FILE * err
Definition: cuddInt.h:442
DdManager::reordered
int reordered
Definition: cuddInt.h:409
addCheckPositiveCube
static int addCheckPositiveCube(DdManager *manager, DdNode *cube)
Definition: cuddAddAbs.c:570
cuddAddOrAbstractRecur
DdNode * cuddAddOrAbstractRecur(DdManager *manager, DdNode *f, DdNode *cube)
Definition: cuddAddAbs.c:469
DdNode* Cudd_addUnivAbstract ( DdManager *  manager,
DdNode *  f,
DdNode *  cube 
)

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

Synopsis [Universally Abstracts all the variables in cube from f.]

Description [Abstracts all the variables in cube from f by taking the product over all possible values taken by the variable. Returns the abstracted ADD if successful; NULL otherwise.]

SideEffects [None]

SeeAlso [Cudd_addExistAbstract Cudd_bddUnivAbstract Cudd_addOrAbstract]

Definition at line 178 of file cuddAddAbs.c.

182 {
183  DdNode *res;
184 
185  if (addCheckPositiveCube(manager, cube) == 0) {
186  (void) fprintf(manager->err,"Error: Can only abstract cubes");
187  return(NULL);
188  }
189 
190  do {
191  manager->reordered = 0;
192  res = cuddAddUnivAbstractRecur(manager, f, cube);
193  } while (manager->reordered == 1);
194 
195  return(res);
196 
197 } /* end of Cudd_addUnivAbstract */
DdNode
Definition: cudd.h:278
cuddAddUnivAbstractRecur
DdNode * cuddAddUnivAbstractRecur(DdManager *manager, DdNode *f, DdNode *cube)
Definition: cuddAddAbs.c:361
DdManager::err
FILE * err
Definition: cuddInt.h:442
DdManager::reordered
int reordered
Definition: cuddInt.h:409
addCheckPositiveCube
static int addCheckPositiveCube(DdManager *manager, DdNode *cube)
Definition: cuddAddAbs.c:570
DdNode* cuddAddExistAbstractRecur ( DdManager *  manager,
DdNode *  f,
DdNode *  cube 
)

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

Synopsis [Performs the recursive step of Cudd_addExistAbstract.]

Description [Performs the recursive step of Cudd_addExistAbstract. Returns the ADD obtained by abstracting the variables of cube from f, if successful; NULL otherwise.]

SideEffects [None]

SeeAlso []

Definition at line 256 of file cuddAddAbs.c.

260 {
261  DdNode *T, *E, *res, *res1, *res2, *zero;
262 
263  statLine(manager);
264  zero = DD_ZERO(manager);
265 
266  /* Cube is guaranteed to be a cube at this point. */
267  if (f == zero || cuddIsConstant(cube)) {
268  return(f);
269  }
270 
271  /* Abstract a variable that does not appear in f => multiply by 2. */
272  if (cuddI(manager,f->index) > cuddI(manager,cube->index)) {
273  res1 = cuddAddExistAbstractRecur(manager, f, cuddT(cube));
274  if (res1 == NULL) return(NULL);
275  cuddRef(res1);
276  /* Use the "internal" procedure to be alerted in case of
277  ** dynamic reordering. If dynamic reordering occurs, we
278  ** have to abort the entire abstraction.
279  */
280  res = cuddAddApplyRecur(manager,Cudd_addTimes,res1,two);
281  if (res == NULL) {
282  Cudd_RecursiveDeref(manager,res1);
283  return(NULL);
284  }
285  cuddRef(res);
286  Cudd_RecursiveDeref(manager,res1);
287  cuddDeref(res);
288  return(res);
289  }
290 
291  if ((res = cuddCacheLookup2(manager, Cudd_addExistAbstract, f, cube)) != NULL) {
292  return(res);
293  }
294 
295  T = cuddT(f);
296  E = cuddE(f);
297 
298  /* If the two indices are the same, so are their levels. */
299  if (f->index == cube->index) {
300  res1 = cuddAddExistAbstractRecur(manager, T, cuddT(cube));
301  if (res1 == NULL) return(NULL);
302  cuddRef(res1);
303  res2 = cuddAddExistAbstractRecur(manager, E, cuddT(cube));
304  if (res2 == NULL) {
305  Cudd_RecursiveDeref(manager,res1);
306  return(NULL);
307  }
308  cuddRef(res2);
309  res = cuddAddApplyRecur(manager, Cudd_addPlus, res1, res2);
310  if (res == NULL) {
311  Cudd_RecursiveDeref(manager,res1);
312  Cudd_RecursiveDeref(manager,res2);
313  return(NULL);
314  }
315  cuddRef(res);
316  Cudd_RecursiveDeref(manager,res1);
317  Cudd_RecursiveDeref(manager,res2);
318  cuddCacheInsert2(manager, Cudd_addExistAbstract, f, cube, res);
319  cuddDeref(res);
320  return(res);
321  } else { /* if (cuddI(manager,f->index) < cuddI(manager,cube->index)) */
322  res1 = cuddAddExistAbstractRecur(manager, T, cube);
323  if (res1 == NULL) return(NULL);
324  cuddRef(res1);
325  res2 = cuddAddExistAbstractRecur(manager, E, cube);
326  if (res2 == NULL) {
327  Cudd_RecursiveDeref(manager,res1);
328  return(NULL);
329  }
330  cuddRef(res2);
331  res = (res1 == res2) ? res1 :
332  cuddUniqueInter(manager, (int) f->index, res1, res2);
333  if (res == NULL) {
334  Cudd_RecursiveDeref(manager,res1);
335  Cudd_RecursiveDeref(manager,res2);
336  return(NULL);
337  }
338  cuddDeref(res1);
339  cuddDeref(res2);
340  cuddCacheInsert2(manager, Cudd_addExistAbstract, f, cube, res);
341  return(res);
342  }
343 
344 } /* end of cuddAddExistAbstractRecur */
cuddRef
#define cuddRef(n)
Definition: cuddInt.h:584
two
static DdNode * two
Definition: cuddAddAbs.c:92
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
cuddCacheInsert2
void cuddCacheInsert2(DdManager *table, DD_CTFP op, DdNode *f, DdNode *g, DdNode *data)
Definition: cuddCache.c:277
cuddAddApplyRecur
DdNode * cuddAddApplyRecur(DdManager *dd, DD_AOP op, DdNode *f, DdNode *g)
Definition: cuddAddApply.c:809
cuddAddExistAbstractRecur
DdNode * cuddAddExistAbstractRecur(DdManager *manager, DdNode *f, DdNode *cube)
Definition: cuddAddAbs.c:256
statLine
#define statLine(dd)
Definition: cuddInt.h:1037
cuddCacheLookup2
DdNode * cuddCacheLookup2(DdManager *table, DD_CTFP op, DdNode *f, DdNode *g)
Definition: cuddCache.c:502
Cudd_addPlus
DdNode * Cudd_addPlus(DdManager *dd, DdNode **f, DdNode **g)
Definition: cuddAddApply.c:168
cuddIsConstant
#define cuddIsConstant(node)
Definition: cuddInt.h:620
Cudd_addExistAbstract
DdNode * Cudd_addExistAbstract(DdManager *manager, DdNode *f, DdNode *cube)
Definition: cuddAddAbs.c:129
cuddT
#define cuddT(node)
Definition: cuddInt.h:636
cuddI
#define cuddI(dd, index)
Definition: cuddInt.h:686
DdNode::index
DdHalfWord index
Definition: cudd.h:279
cuddE
#define cuddE(node)
Definition: cuddInt.h:652
Cudd_addTimes
DdNode * Cudd_addTimes(DdManager *dd, DdNode **f, DdNode **g)
Definition: cuddAddApply.c:208
cuddUniqueInter
DdNode * cuddUniqueInter(DdManager *unique, int index, DdNode *T, DdNode *E)
Definition: cuddTable.c:1128
zero
static DdNode * zero
Definition: cuddApa.c:100
DD_ZERO
#define DD_ZERO(dd)
Definition: cuddInt.h:927
DdNode* cuddAddOrAbstractRecur ( DdManager *  manager,
DdNode *  f,
DdNode *  cube 
)

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

Synopsis [Performs the recursive step of Cudd_addOrAbstract.]

Description [Performs the recursive step of Cudd_addOrAbstract. Returns the ADD obtained by abstracting the variables of cube from f, if successful; NULL otherwise.]

SideEffects [None]

SeeAlso []

Definition at line 469 of file cuddAddAbs.c.

473 {
474  DdNode *T, *E, *res, *res1, *res2, *one;
475 
476  statLine(manager);
477  one = DD_ONE(manager);
478 
479  /* Cube is guaranteed to be a cube at this point. */
480  if (cuddIsConstant(f) || cube == one) {
481  return(f);
482  }
483 
484  /* Abstract a variable that does not appear in f. */
485  if (cuddI(manager,f->index) > cuddI(manager,cube->index)) {
486  res = cuddAddOrAbstractRecur(manager, f, cuddT(cube));
487  return(res);
488  }
489 
490  if ((res = cuddCacheLookup2(manager, Cudd_addOrAbstract, f, cube)) != NULL) {
491  return(res);
492  }
493 
494  T = cuddT(f);
495  E = cuddE(f);
496 
497  /* If the two indices are the same, so are their levels. */
498  if (f->index == cube->index) {
499  res1 = cuddAddOrAbstractRecur(manager, T, cuddT(cube));
500  if (res1 == NULL) return(NULL);
501  cuddRef(res1);
502  if (res1 != one) {
503  res2 = cuddAddOrAbstractRecur(manager, E, cuddT(cube));
504  if (res2 == NULL) {
505  Cudd_RecursiveDeref(manager,res1);
506  return(NULL);
507  }
508  cuddRef(res2);
509  res = cuddAddApplyRecur(manager, Cudd_addOr, res1, res2);
510  if (res == NULL) {
511  Cudd_RecursiveDeref(manager,res1);
512  Cudd_RecursiveDeref(manager,res2);
513  return(NULL);
514  }
515  cuddRef(res);
516  Cudd_RecursiveDeref(manager,res1);
517  Cudd_RecursiveDeref(manager,res2);
518  } else {
519  res = res1;
520  }
521  cuddCacheInsert2(manager, Cudd_addOrAbstract, f, cube, res);
522  cuddDeref(res);
523  return(res);
524  } else { /* if (cuddI(manager,f->index) < cuddI(manager,cube->index)) */
525  res1 = cuddAddOrAbstractRecur(manager, T, cube);
526  if (res1 == NULL) return(NULL);
527  cuddRef(res1);
528  res2 = cuddAddOrAbstractRecur(manager, E, cube);
529  if (res2 == NULL) {
530  Cudd_RecursiveDeref(manager,res1);
531  return(NULL);
532  }
533  cuddRef(res2);
534  res = (res1 == res2) ? res1 :
535  cuddUniqueInter(manager, (int) f->index, res1, res2);
536  if (res == NULL) {
537  Cudd_RecursiveDeref(manager,res1);
538  Cudd_RecursiveDeref(manager,res2);
539  return(NULL);
540  }
541  cuddDeref(res1);
542  cuddDeref(res2);
543  cuddCacheInsert2(manager, Cudd_addOrAbstract, f, cube, res);
544  return(res);
545  }
546 
547 } /* end of cuddAddOrAbstractRecur */
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
cuddCacheInsert2
void cuddCacheInsert2(DdManager *table, DD_CTFP op, DdNode *f, DdNode *g, DdNode *data)
Definition: cuddCache.c:277
Cudd_addOr
DdNode * Cudd_addOr(DdManager *dd, DdNode **f, DdNode **g)
Definition: cuddAddApply.c:581
cuddAddApplyRecur
DdNode * cuddAddApplyRecur(DdManager *dd, DD_AOP op, DdNode *f, DdNode *g)
Definition: cuddAddApply.c:809
Cudd_addOrAbstract
DdNode * Cudd_addOrAbstract(DdManager *manager, DdNode *f, DdNode *cube)
Definition: cuddAddAbs.c:216
statLine
#define statLine(dd)
Definition: cuddInt.h:1037
cuddCacheLookup2
DdNode * cuddCacheLookup2(DdManager *table, DD_CTFP op, DdNode *f, DdNode *g)
Definition: cuddCache.c:502
one
static DdNode * one
Definition: cuddDecomp.c:112
cuddIsConstant
#define cuddIsConstant(node)
Definition: cuddInt.h:620
cuddT
#define cuddT(node)
Definition: cuddInt.h:636
cuddI
#define cuddI(dd, index)
Definition: cuddInt.h:686
DdNode::index
DdHalfWord index
Definition: cudd.h:279
cuddAddOrAbstractRecur
DdNode * cuddAddOrAbstractRecur(DdManager *manager, DdNode *f, DdNode *cube)
Definition: cuddAddAbs.c:469
cuddE
#define cuddE(node)
Definition: cuddInt.h:652
DD_ONE
#define DD_ONE(dd)
Definition: cuddInt.h:911
cuddUniqueInter
DdNode * cuddUniqueInter(DdManager *unique, int index, DdNode *T, DdNode *E)
Definition: cuddTable.c:1128
DdNode* cuddAddUnivAbstractRecur ( DdManager *  manager,
DdNode *  f,
DdNode *  cube 
)

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

Synopsis [Performs the recursive step of Cudd_addUnivAbstract.]

Description [Performs the recursive step of Cudd_addUnivAbstract. Returns the ADD obtained by abstracting the variables of cube from f, if successful; NULL otherwise.]

SideEffects [None]

SeeAlso []

Definition at line 361 of file cuddAddAbs.c.

365 {
366  DdNode *T, *E, *res, *res1, *res2, *one, *zero;
367 
368  statLine(manager);
369  one = DD_ONE(manager);
370  zero = DD_ZERO(manager);
371 
372  /* Cube is guaranteed to be a cube at this point.
373  ** zero and one are the only constatnts c such that c*c=c.
374  */
375  if (f == zero || f == one || cube == one) {
376  return(f);
377  }
378 
379  /* Abstract a variable that does not appear in f. */
380  if (cuddI(manager,f->index) > cuddI(manager,cube->index)) {
381  res1 = cuddAddUnivAbstractRecur(manager, f, cuddT(cube));
382  if (res1 == NULL) return(NULL);
383  cuddRef(res1);
384  /* Use the "internal" procedure to be alerted in case of
385  ** dynamic reordering. If dynamic reordering occurs, we
386  ** have to abort the entire abstraction.
387  */
388  res = cuddAddApplyRecur(manager, Cudd_addTimes, res1, res1);
389  if (res == NULL) {
390  Cudd_RecursiveDeref(manager,res1);
391  return(NULL);
392  }
393  cuddRef(res);
394  Cudd_RecursiveDeref(manager,res1);
395  cuddDeref(res);
396  return(res);
397  }
398 
399  if ((res = cuddCacheLookup2(manager, Cudd_addUnivAbstract, f, cube)) != NULL) {
400  return(res);
401  }
402 
403  T = cuddT(f);
404  E = cuddE(f);
405 
406  /* If the two indices are the same, so are their levels. */
407  if (f->index == cube->index) {
408  res1 = cuddAddUnivAbstractRecur(manager, T, cuddT(cube));
409  if (res1 == NULL) return(NULL);
410  cuddRef(res1);
411  res2 = cuddAddUnivAbstractRecur(manager, E, cuddT(cube));
412  if (res2 == NULL) {
413  Cudd_RecursiveDeref(manager,res1);
414  return(NULL);
415  }
416  cuddRef(res2);
417  res = cuddAddApplyRecur(manager, Cudd_addTimes, res1, res2);
418  if (res == NULL) {
419  Cudd_RecursiveDeref(manager,res1);
420  Cudd_RecursiveDeref(manager,res2);
421  return(NULL);
422  }
423  cuddRef(res);
424  Cudd_RecursiveDeref(manager,res1);
425  Cudd_RecursiveDeref(manager,res2);
426  cuddCacheInsert2(manager, Cudd_addUnivAbstract, f, cube, res);
427  cuddDeref(res);
428  return(res);
429  } else { /* if (cuddI(manager,f->index) < cuddI(manager,cube->index)) */
430  res1 = cuddAddUnivAbstractRecur(manager, T, cube);
431  if (res1 == NULL) return(NULL);
432  cuddRef(res1);
433  res2 = cuddAddUnivAbstractRecur(manager, E, cube);
434  if (res2 == NULL) {
435  Cudd_RecursiveDeref(manager,res1);
436  return(NULL);
437  }
438  cuddRef(res2);
439  res = (res1 == res2) ? res1 :
440  cuddUniqueInter(manager, (int) f->index, res1, res2);
441  if (res == NULL) {
442  Cudd_RecursiveDeref(manager,res1);
443  Cudd_RecursiveDeref(manager,res2);
444  return(NULL);
445  }
446  cuddDeref(res1);
447  cuddDeref(res2);
448  cuddCacheInsert2(manager, Cudd_addUnivAbstract, f, cube, res);
449  return(res);
450  }
451 
452 } /* end of cuddAddUnivAbstractRecur */
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
cuddCacheInsert2
void cuddCacheInsert2(DdManager *table, DD_CTFP op, DdNode *f, DdNode *g, DdNode *data)
Definition: cuddCache.c:277
cuddAddUnivAbstractRecur
DdNode * cuddAddUnivAbstractRecur(DdManager *manager, DdNode *f, DdNode *cube)
Definition: cuddAddAbs.c:361
cuddAddApplyRecur
DdNode * cuddAddApplyRecur(DdManager *dd, DD_AOP op, DdNode *f, DdNode *g)
Definition: cuddAddApply.c:809
Cudd_addUnivAbstract
DdNode * Cudd_addUnivAbstract(DdManager *manager, DdNode *f, DdNode *cube)
Definition: cuddAddAbs.c:178
statLine
#define statLine(dd)
Definition: cuddInt.h:1037
cuddCacheLookup2
DdNode * cuddCacheLookup2(DdManager *table, DD_CTFP op, DdNode *f, DdNode *g)
Definition: cuddCache.c:502
one
static DdNode * one
Definition: cuddDecomp.c:112
cuddT
#define cuddT(node)
Definition: cuddInt.h:636
cuddI
#define cuddI(dd, index)
Definition: cuddInt.h:686
DdNode::index
DdHalfWord index
Definition: cudd.h:279
cuddE
#define cuddE(node)
Definition: cuddInt.h:652
DD_ONE
#define DD_ONE(dd)
Definition: cuddInt.h:911
Cudd_addTimes
DdNode * Cudd_addTimes(DdManager *dd, DdNode **f, DdNode **g)
Definition: cuddAddApply.c:208
cuddUniqueInter
DdNode * cuddUniqueInter(DdManager *unique, int index, DdNode *T, DdNode *E)
Definition: cuddTable.c:1128
zero
static DdNode * zero
Definition: cuddApa.c:100
DD_ZERO
#define DD_ZERO(dd)
Definition: cuddInt.h:927

Variable Documentation

ABC_NAMESPACE_IMPL_START char rcsid [] DD_UNUSED = "$Id: cuddAddAbs.c,v 1.15 2004/08/13 18:04:45 fabio Exp $"
static

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

FileName [cuddAddAbs.c]

PackageName [cudd]

Synopsis [Quantification functions for ADDs.]

Description [External procedures included in this module:

Internal 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 89 of file cuddAddAbs.c.

DdNode* two
static

Definition at line 92 of file cuddAddAbs.c.