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

Go to the source code of this file.

Functions

DdNode * Cudd_addApply (DdManager *dd, DD_AOP op, DdNode *f, DdNode *g)
 
DdNode * Cudd_addPlus (DdManager *dd, DdNode **f, DdNode **g)
 
DdNode * Cudd_addTimes (DdManager *dd, DdNode **f, DdNode **g)
 
DdNode * Cudd_addThreshold (DdManager *dd, DdNode **f, DdNode **g)
 
DdNode * Cudd_addSetNZ (DdManager *dd, DdNode **f, DdNode **g)
 
DdNode * Cudd_addDivide (DdManager *dd, DdNode **f, DdNode **g)
 
DdNode * Cudd_addMinus (DdManager *dd, DdNode **f, DdNode **g)
 
DdNode * Cudd_addMinimum (DdManager *dd, DdNode **f, DdNode **g)
 
DdNode * Cudd_addMaximum (DdManager *dd, DdNode **f, DdNode **g)
 
DdNode * Cudd_addOneZeroMaximum (DdManager *dd, DdNode **f, DdNode **g)
 
DdNode * Cudd_addDiff (DdManager *dd, DdNode **f, DdNode **g)
 
DdNode * Cudd_addAgreement (DdManager *dd, DdNode **f, DdNode **g)
 
DdNode * Cudd_addOr (DdManager *dd, DdNode **f, DdNode **g)
 
DdNode * Cudd_addNand (DdManager *dd, DdNode **f, DdNode **g)
 
DdNode * Cudd_addNor (DdManager *dd, DdNode **f, DdNode **g)
 
DdNode * Cudd_addXor (DdManager *dd, DdNode **f, DdNode **g)
 
DdNode * Cudd_addXnor (DdManager *dd, DdNode **f, DdNode **g)
 
DdNode * Cudd_addMonadicApply (DdManager *dd, DD_MAOP op, DdNode *f)
 
DdNode * Cudd_addLog (DdManager *dd, DdNode *f)
 
DdNode * cuddAddApplyRecur (DdManager *dd, DD_AOP op, DdNode *f, DdNode *g)
 
DdNode * cuddAddMonadicApplyRecur (DdManager *dd, DD_MAOP op, DdNode *f)
 

Variables

static
ABC_NAMESPACE_IMPL_START char
rcsid[] 		DD_UNUSED = "$Id: cuddAddApply.c,v 1.18 2009/02/19 16:15:26 fabio Exp $"
 

Function Documentation

DdNode* Cudd_addAgreement ( DdManager *  dd,
DdNode **  f,
DdNode **  g 
)

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

Synopsis [f if f==g; background if f!=g.]

Description [Returns NULL if not a terminal case; f op g otherwise, where f op g is f if f==g; background if f!=g.]

SideEffects [None]

SeeAlso [Cudd_addApply]

Definition at line 551 of file cuddAddApply.c.

555 {
556  DdNode *F, *G;
557 
558  F = *f; G = *g;
559  if (F == G) return(F);
560  if (F == dd->background) return(F);
561  if (G == dd->background) return(G);
562  if (cuddIsConstant(F) && cuddIsConstant(G)) return(dd->background);
563  return(NULL);
564 
565 } /* end of Cudd_addAgreement */
DdNode
Definition: cudd.h:278
cuddIsConstant
#define cuddIsConstant(node)
Definition: cuddInt.h:620
DdManager::background
DdNode * background
Definition: cuddInt.h:349
DdNode* Cudd_addApply ( DdManager *  dd,
DD_AOP  op,
DdNode *  f,
DdNode *  g 
)

AutomaticStart AutomaticEnd Function********************************************************************

Synopsis [Applies op to the corresponding discriminants of f and g.]

Description [Applies op to the corresponding discriminants of f and g. Returns a pointer to the result if succssful; NULL otherwise.]

SideEffects [None]

SeeAlso [Cudd_addMonadicApply Cudd_addPlus Cudd_addTimes Cudd_addThreshold Cudd_addSetNZ Cudd_addDivide Cudd_addMinus Cudd_addMinimum Cudd_addMaximum Cudd_addOneZeroMaximum Cudd_addDiff Cudd_addAgreement Cudd_addOr Cudd_addNand Cudd_addNor Cudd_addXor Cudd_addXnor]

Definition at line 138 of file cuddAddApply.c.

143 {
144  DdNode *res;
145 
146  do {
147  dd->reordered = 0;
148  res = cuddAddApplyRecur(dd,op,f,g);
149  } while (dd->reordered == 1);
150  return(res);
151 
152 } /* end of Cudd_addApply */
DdNode
Definition: cudd.h:278
cuddAddApplyRecur
DdNode * cuddAddApplyRecur(DdManager *dd, DD_AOP op, DdNode *f, DdNode *g)
Definition: cuddAddApply.c:809
DdManager::reordered
int reordered
Definition: cuddInt.h:409
DdNode* Cudd_addDiff ( DdManager *  dd,
DdNode **  f,
DdNode **  g 
)

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

Synopsis [Returns plusinfinity if f=g; returns min(f,g) if f!=g.]

Description [Returns NULL if not a terminal case; f op g otherwise, where f op g is plusinfinity if f=g; min(f,g) if f!=g.]

SideEffects [None]

SeeAlso [Cudd_addApply]

Definition at line 511 of file cuddAddApply.c.

515 {
516  DdNode *F, *G;
517 
518  F = *f; G = *g;
519  if (F == G) return(DD_PLUS_INFINITY(dd));
520  if (F == DD_PLUS_INFINITY(dd)) return(G);
521  if (G == DD_PLUS_INFINITY(dd)) return(F);
522  if (cuddIsConstant(F) && cuddIsConstant(G)) {
523  if (cuddV(F) != cuddV(G)) {
524  if (cuddV(F) < cuddV(G)) {
525  return(F);
526  } else {
527  return(G);
528  }
529  } else {
530  return(DD_PLUS_INFINITY(dd));
531  }
532  }
533  return(NULL);
534 
535 } /* end of Cudd_addDiff */
DdNode
Definition: cudd.h:278
cuddV
#define cuddV(node)
Definition: cuddInt.h:668
cuddIsConstant
#define cuddIsConstant(node)
Definition: cuddInt.h:620
DD_PLUS_INFINITY
#define DD_PLUS_INFINITY(dd)
Definition: cuddInt.h:941
DdNode* Cudd_addDivide ( DdManager *  dd,
DdNode **  f,
DdNode **  g 
)

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

Synopsis [Integer and floating point division.]

Description [Integer and floating point division. Returns NULL if not a terminal case; f / g otherwise.]

SideEffects [None]

SeeAlso [Cudd_addApply]

Definition at line 312 of file cuddAddApply.c.

316 {
317  DdNode *res;
318  DdNode *F, *G;
319  CUDD_VALUE_TYPE value;
320 
321  F = *f; G = *g;
322  /* We would like to use F == G -> F/G == 1, but F and G may
323  ** contain zeroes. */
324  if (F == DD_ZERO(dd)) return(DD_ZERO(dd));
325  if (G == DD_ONE(dd)) return(F);
326  if (cuddIsConstant(F) && cuddIsConstant(G)) {
327  value = cuddV(F)/cuddV(G);
328  res = cuddUniqueConst(dd,value);
329  return(res);
330  }
331  return(NULL);
332 
333 } /* end of Cudd_addDivide */
DdNode
Definition: cudd.h:278
cuddUniqueConst
DdNode * cuddUniqueConst(DdManager *unique, CUDD_VALUE_TYPE value)
Definition: cuddTable.c:1450
cuddV
#define cuddV(node)
Definition: cuddInt.h:668
cuddIsConstant
#define cuddIsConstant(node)
Definition: cuddInt.h:620
CUDD_VALUE_TYPE
#define CUDD_VALUE_TYPE
Definition: cudd.h:94
value
int value
Definition: misc/espresso/main.h:90
DD_ONE
#define DD_ONE(dd)
Definition: cuddInt.h:911
DD_ZERO
#define DD_ZERO(dd)
Definition: cuddInt.h:927
DdNode* Cudd_addLog ( DdManager *  dd,
DdNode *  f 
)

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

Synopsis [Natural logarithm of an ADD.]

Description [Natural logarithm of an ADDs. Returns NULL if not a terminal case; log(f) otherwise. The discriminants of f must be positive double's.]

SideEffects [None]

SeeAlso [Cudd_addMonadicApply]

Definition at line 777 of file cuddAddApply.c.

780 {
781  if (cuddIsConstant(f)) {
782  CUDD_VALUE_TYPE value = log(cuddV(f));
783  DdNode *res = cuddUniqueConst(dd,value);
784  return(res);
785  }
786  return(NULL);
787 
788 } /* end of Cudd_addLog */
DdNode
Definition: cudd.h:278
cuddUniqueConst
DdNode * cuddUniqueConst(DdManager *unique, CUDD_VALUE_TYPE value)
Definition: cuddTable.c:1450
cuddV
#define cuddV(node)
Definition: cuddInt.h:668
cuddIsConstant
#define cuddIsConstant(node)
Definition: cuddInt.h:620
CUDD_VALUE_TYPE
#define CUDD_VALUE_TYPE
Definition: cudd.h:94
value
int value
Definition: misc/espresso/main.h:90
DdNode* Cudd_addMaximum ( DdManager *  dd,
DdNode **  f,
DdNode **  g 
)

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

Synopsis [Integer and floating point max.]

Description [Integer and floating point max for Cudd_addApply. Returns NULL if not a terminal case; max(f,g) otherwise.]

SideEffects [None]

SeeAlso [Cudd_addApply]

Definition at line 430 of file cuddAddApply.c.

434 {
435  DdNode *F, *G;
436 
437  F = *f; G = *g;
438  if (F == G) return(F);
439  if (F == DD_MINUS_INFINITY(dd)) return(G);
440  if (G == DD_MINUS_INFINITY(dd)) return(F);
441 #if 0
442  /* These special cases probably do not pay off. */
443  if (F == DD_PLUS_INFINITY(dd)) return(F);
444  if (G == DD_PLUS_INFINITY(dd)) return(G);
445 #endif
446  if (cuddIsConstant(F) && cuddIsConstant(G)) {
447  if (cuddV(F) >= cuddV(G)) {
448  return(F);
449  } else {
450  return(G);
451  }
452  }
453  if (F > G) { /* swap f and g */
454  *f = G;
455  *g = F;
456  }
457  return(NULL);
458 
459 } /* end of Cudd_addMaximum */
DdNode
Definition: cudd.h:278
DD_MINUS_INFINITY
#define DD_MINUS_INFINITY(dd)
Definition: cuddInt.h:955
cuddV
#define cuddV(node)
Definition: cuddInt.h:668
cuddIsConstant
#define cuddIsConstant(node)
Definition: cuddInt.h:620
DD_PLUS_INFINITY
#define DD_PLUS_INFINITY(dd)
Definition: cuddInt.h:941
DdNode* Cudd_addMinimum ( DdManager *  dd,
DdNode **  f,
DdNode **  g 
)

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

Synopsis [Integer and floating point min.]

Description [Integer and floating point min for Cudd_addApply. Returns NULL if not a terminal case; min(f,g) otherwise.]

SideEffects [None]

SeeAlso [Cudd_addApply]

Definition at line 385 of file cuddAddApply.c.

389 {
390  DdNode *F, *G;
391 
392  F = *f; G = *g;
393  if (F == DD_PLUS_INFINITY(dd)) return(G);
394  if (G == DD_PLUS_INFINITY(dd)) return(F);
395  if (F == G) return(F);
396 #if 0
397  /* These special cases probably do not pay off. */
398  if (F == DD_MINUS_INFINITY(dd)) return(F);
399  if (G == DD_MINUS_INFINITY(dd)) return(G);
400 #endif
401  if (cuddIsConstant(F) && cuddIsConstant(G)) {
402  if (cuddV(F) <= cuddV(G)) {
403  return(F);
404  } else {
405  return(G);
406  }
407  }
408  if (F > G) { /* swap f and g */
409  *f = G;
410  *g = F;
411  }
412  return(NULL);
413 
414 } /* end of Cudd_addMinimum */
DdNode
Definition: cudd.h:278
DD_MINUS_INFINITY
#define DD_MINUS_INFINITY(dd)
Definition: cuddInt.h:955
cuddV
#define cuddV(node)
Definition: cuddInt.h:668
cuddIsConstant
#define cuddIsConstant(node)
Definition: cuddInt.h:620
DD_PLUS_INFINITY
#define DD_PLUS_INFINITY(dd)
Definition: cuddInt.h:941
DdNode* Cudd_addMinus ( DdManager *  dd,
DdNode **  f,
DdNode **  g 
)

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

Synopsis [Integer and floating point subtraction.]

Description [Integer and floating point subtraction. Returns NULL if not a terminal case; f - g otherwise.]

SideEffects [None]

SeeAlso [Cudd_addApply]

Definition at line 349 of file cuddAddApply.c.

353 {
354  DdNode *res;
355  DdNode *F, *G;
356  CUDD_VALUE_TYPE value;
357 
358  F = *f; G = *g;
359  if (F == G) return(DD_ZERO(dd));
360  if (F == DD_ZERO(dd)) return(cuddAddNegateRecur(dd,G));
361  if (G == DD_ZERO(dd)) return(F);
362  if (cuddIsConstant(F) && cuddIsConstant(G)) {
363  value = cuddV(F)-cuddV(G);
364  res = cuddUniqueConst(dd,value);
365  return(res);
366  }
367  return(NULL);
368 
369 } /* end of Cudd_addMinus */
DdNode
Definition: cudd.h:278
cuddUniqueConst
DdNode * cuddUniqueConst(DdManager *unique, CUDD_VALUE_TYPE value)
Definition: cuddTable.c:1450
cuddV
#define cuddV(node)
Definition: cuddInt.h:668
cuddAddNegateRecur
DdNode * cuddAddNegateRecur(DdManager *dd, DdNode *f)
Definition: cuddAddNeg.c:180
cuddIsConstant
#define cuddIsConstant(node)
Definition: cuddInt.h:620
CUDD_VALUE_TYPE
#define CUDD_VALUE_TYPE
Definition: cudd.h:94
value
int value
Definition: misc/espresso/main.h:90
DD_ZERO
#define DD_ZERO(dd)
Definition: cuddInt.h:927
DdNode* Cudd_addMonadicApply ( DdManager *  dd,
DD_MAOP  op,
DdNode *  f 
)

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

Synopsis [Applies op to the discriminants of f.]

Description [Applies op to the discriminants of f. Returns a pointer to the result if succssful; NULL otherwise.]

SideEffects [None]

SeeAlso [Cudd_addApply Cudd_addLog]

Definition at line 747 of file cuddAddApply.c.

751 {
752  DdNode *res;
753 
754  do {
755  dd->reordered = 0;
756  res = cuddAddMonadicApplyRecur(dd,op,f);
757  } while (dd->reordered == 1);
758  return(res);
759 
760 } /* end of Cudd_addMonadicApply */
DdNode
Definition: cudd.h:278
cuddAddMonadicApplyRecur
DdNode * cuddAddMonadicApplyRecur(DdManager *dd, DD_MAOP op, DdNode *f)
Definition: cuddAddApply.c:893
DdManager::reordered
int reordered
Definition: cuddInt.h:409
DdNode* Cudd_addNand ( DdManager *  dd,
DdNode **  f,
DdNode **  g 
)

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

Synopsis [NAND of two 0-1 ADDs.]

Description [NAND of two 0-1 ADDs. Returns NULL if not a terminal case; f NAND g otherwise.]

SideEffects [None]

SeeAlso [Cudd_addApply]

Definition at line 615 of file cuddAddApply.c.

619 {
620  DdNode *F, *G;
621 
622  F = *f; G = *g;
623  if (F == DD_ZERO(dd) || G == DD_ZERO(dd)) return(DD_ONE(dd));
624  if (cuddIsConstant(F) && cuddIsConstant(G)) return(DD_ZERO(dd));
625  if (F > G) { /* swap f and g */
626  *f = G;
627  *g = F;
628  }
629  return(NULL);
630 
631 } /* end of Cudd_addNand */
DdNode
Definition: cudd.h:278
cuddIsConstant
#define cuddIsConstant(node)
Definition: cuddInt.h:620
DD_ONE
#define DD_ONE(dd)
Definition: cuddInt.h:911
DD_ZERO
#define DD_ZERO(dd)
Definition: cuddInt.h:927
DdNode* Cudd_addNor ( DdManager *  dd,
DdNode **  f,
DdNode **  g 
)

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

Synopsis [NOR of two 0-1 ADDs.]

Description [NOR of two 0-1 ADDs. Returns NULL if not a terminal case; f NOR g otherwise.]

SideEffects [None]

SeeAlso [Cudd_addApply]

Definition at line 647 of file cuddAddApply.c.

651 {
652  DdNode *F, *G;
653 
654  F = *f; G = *g;
655  if (F == DD_ONE(dd) || G == DD_ONE(dd)) return(DD_ZERO(dd));
656  if (cuddIsConstant(F) && cuddIsConstant(G)) return(DD_ONE(dd));
657  if (F > G) { /* swap f and g */
658  *f = G;
659  *g = F;
660  }
661  return(NULL);
662 
663 } /* end of Cudd_addNor */
DdNode
Definition: cudd.h:278
cuddIsConstant
#define cuddIsConstant(node)
Definition: cuddInt.h:620
DD_ONE
#define DD_ONE(dd)
Definition: cuddInt.h:911
DD_ZERO
#define DD_ZERO(dd)
Definition: cuddInt.h:927
DdNode* Cudd_addOneZeroMaximum ( DdManager *  dd,
DdNode **  f,
DdNode **  g 
)

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

Synopsis [Returns 1 if f > g and 0 otherwise.]

Description [Returns 1 if f > g and 0 otherwise. Used in conjunction with Cudd_addApply. Returns NULL if not a terminal case.]

SideEffects [None]

SeeAlso [Cudd_addApply]

Definition at line 476 of file cuddAddApply.c.

480 {
481 
482  if (*f == *g) return(DD_ZERO(dd));
483  if (*g == DD_PLUS_INFINITY(dd))
484  return DD_ZERO(dd);
485  if (cuddIsConstant(*f) && cuddIsConstant(*g)) {
486  if (cuddV(*f) > cuddV(*g)) {
487  return(DD_ONE(dd));
488  } else {
489  return(DD_ZERO(dd));
490  }
491  }
492 
493  return(NULL);
494 
495 } /* end of Cudd_addOneZeroMaximum */
cuddV
#define cuddV(node)
Definition: cuddInt.h:668
cuddIsConstant
#define cuddIsConstant(node)
Definition: cuddInt.h:620
DD_PLUS_INFINITY
#define DD_PLUS_INFINITY(dd)
Definition: cuddInt.h:941
DD_ONE
#define DD_ONE(dd)
Definition: cuddInt.h:911
DD_ZERO
#define DD_ZERO(dd)
Definition: cuddInt.h:927
DdNode* Cudd_addOr ( DdManager *  dd,
DdNode **  f,
DdNode **  g 
)

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

Synopsis [Disjunction of two 0-1 ADDs.]

Description [Disjunction of two 0-1 ADDs. Returns NULL if not a terminal case; f OR g otherwise.]

SideEffects [None]

SeeAlso [Cudd_addApply]

Definition at line 581 of file cuddAddApply.c.

585 {
586  DdNode *F, *G;
587 
588  F = *f; G = *g;
589  if (F == DD_ONE(dd) || G == DD_ONE(dd)) return(DD_ONE(dd));
590  if (cuddIsConstant(F)) return(G);
591  if (cuddIsConstant(G)) return(F);
592  if (F == G) return(F);
593  if (F > G) { /* swap f and g */
594  *f = G;
595  *g = F;
596  }
597  return(NULL);
598 
599 } /* end of Cudd_addOr */
DdNode
Definition: cudd.h:278
cuddIsConstant
#define cuddIsConstant(node)
Definition: cuddInt.h:620
DD_ONE
#define DD_ONE(dd)
Definition: cuddInt.h:911
DdNode* Cudd_addPlus ( DdManager *  dd,
DdNode **  f,
DdNode **  g 
)

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

Synopsis [Integer and floating point addition.]

Description [Integer and floating point addition. Returns NULL if not a terminal case; f+g otherwise.]

SideEffects [None]

SeeAlso [Cudd_addApply]

Definition at line 168 of file cuddAddApply.c.

172 {
173  DdNode *res;
174  DdNode *F, *G;
175  CUDD_VALUE_TYPE value;
176 
177  F = *f; G = *g;
178  if (F == DD_ZERO(dd)) return(G);
179  if (G == DD_ZERO(dd)) return(F);
180  if (cuddIsConstant(F) && cuddIsConstant(G)) {
181  value = cuddV(F)+cuddV(G);
182  res = cuddUniqueConst(dd,value);
183  return(res);
184  }
185  if (F > G) { /* swap f and g */
186  *f = G;
187  *g = F;
188  }
189  return(NULL);
190 
191 } /* end of Cudd_addPlus */
DdNode
Definition: cudd.h:278
cuddUniqueConst
DdNode * cuddUniqueConst(DdManager *unique, CUDD_VALUE_TYPE value)
Definition: cuddTable.c:1450
cuddV
#define cuddV(node)
Definition: cuddInt.h:668
cuddIsConstant
#define cuddIsConstant(node)
Definition: cuddInt.h:620
CUDD_VALUE_TYPE
#define CUDD_VALUE_TYPE
Definition: cudd.h:94
value
int value
Definition: misc/espresso/main.h:90
DD_ZERO
#define DD_ZERO(dd)
Definition: cuddInt.h:927
DdNode* Cudd_addSetNZ ( DdManager *  dd,
DdNode **  f,
DdNode **  g 
)

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

Synopsis [This operator sets f to the value of g wherever g != 0.]

Description [This operator sets f to the value of g wherever g != 0. Returns NULL if not a terminal case; f op g otherwise.]

SideEffects [None]

SeeAlso [Cudd_addApply]

Definition at line 282 of file cuddAddApply.c.

286 {
287  DdNode *F, *G;
288 
289  F = *f; G = *g;
290  if (F == G) return(F);
291  if (F == DD_ZERO(dd)) return(G);
292  if (G == DD_ZERO(dd)) return(F);
293  if (cuddIsConstant(G)) return(G);
294  return(NULL);
295 
296 } /* end of Cudd_addSetNZ */
DdNode
Definition: cudd.h:278
cuddIsConstant
#define cuddIsConstant(node)
Definition: cuddInt.h:620
DD_ZERO
#define DD_ZERO(dd)
Definition: cuddInt.h:927
DdNode* Cudd_addThreshold ( DdManager *  dd,
DdNode **  f,
DdNode **  g 
)

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

Synopsis [f if f>=g; 0 if f<g.]

Description [Threshold operator for Apply (f if f >=g; 0 if f<g). Returns NULL if not a terminal case; f op g otherwise.]

SideEffects [None]

SeeAlso [Cudd_addApply]

Definition at line 248 of file cuddAddApply.c.

252 {
253  DdNode *F, *G;
254 
255  F = *f; G = *g;
256  if (F == G || F == DD_PLUS_INFINITY(dd)) return(F);
257  if (cuddIsConstant(F) && cuddIsConstant(G)) {
258  if (cuddV(F) >= cuddV(G)) {
259  return(F);
260  } else {
261  return(DD_ZERO(dd));
262  }
263  }
264  return(NULL);
265 
266 } /* end of Cudd_addThreshold */
DdNode
Definition: cudd.h:278
cuddV
#define cuddV(node)
Definition: cuddInt.h:668
cuddIsConstant
#define cuddIsConstant(node)
Definition: cuddInt.h:620
DD_PLUS_INFINITY
#define DD_PLUS_INFINITY(dd)
Definition: cuddInt.h:941
DD_ZERO
#define DD_ZERO(dd)
Definition: cuddInt.h:927
DdNode* Cudd_addTimes ( DdManager *  dd,
DdNode **  f,
DdNode **  g 
)

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

Synopsis [Integer and floating point multiplication.]

Description [Integer and floating point multiplication. Returns NULL if not a terminal case; f * g otherwise. This function can be used also to take the AND of two 0-1 ADDs.]

SideEffects [None]

SeeAlso [Cudd_addApply]

Definition at line 208 of file cuddAddApply.c.

212 {
213  DdNode *res;
214  DdNode *F, *G;
215  CUDD_VALUE_TYPE value;
216 
217  F = *f; G = *g;
218  if (F == DD_ZERO(dd) || G == DD_ZERO(dd)) return(DD_ZERO(dd));
219  if (F == DD_ONE(dd)) return(G);
220  if (G == DD_ONE(dd)) return(F);
221  if (cuddIsConstant(F) && cuddIsConstant(G)) {
222  value = cuddV(F)*cuddV(G);
223  res = cuddUniqueConst(dd,value);
224  return(res);
225  }
226  if (F > G) { /* swap f and g */
227  *f = G;
228  *g = F;
229  }
230  return(NULL);
231 
232 } /* end of Cudd_addTimes */
DdNode
Definition: cudd.h:278
cuddUniqueConst
DdNode * cuddUniqueConst(DdManager *unique, CUDD_VALUE_TYPE value)
Definition: cuddTable.c:1450
cuddV
#define cuddV(node)
Definition: cuddInt.h:668
cuddIsConstant
#define cuddIsConstant(node)
Definition: cuddInt.h:620
CUDD_VALUE_TYPE
#define CUDD_VALUE_TYPE
Definition: cudd.h:94
value
int value
Definition: misc/espresso/main.h:90
DD_ONE
#define DD_ONE(dd)
Definition: cuddInt.h:911
DD_ZERO
#define DD_ZERO(dd)
Definition: cuddInt.h:927
DdNode* Cudd_addXnor ( DdManager *  dd,
DdNode **  f,
DdNode **  g 
)

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

Synopsis [XNOR of two 0-1 ADDs.]

Description [XNOR of two 0-1 ADDs. Returns NULL if not a terminal case; f XNOR g otherwise.]

SideEffects [None]

SeeAlso [Cudd_addApply]

Definition at line 713 of file cuddAddApply.c.

717 {
718  DdNode *F, *G;
719 
720  F = *f; G = *g;
721  if (F == G) return(DD_ONE(dd));
722  if (F == DD_ONE(dd) && G == DD_ONE(dd)) return(DD_ONE(dd));
723  if (G == DD_ZERO(dd) && F == DD_ZERO(dd)) return(DD_ONE(dd));
724  if (cuddIsConstant(F) && cuddIsConstant(G)) return(DD_ZERO(dd));
725  if (F > G) { /* swap f and g */
726  *f = G;
727  *g = F;
728  }
729  return(NULL);
730 
731 } /* end of Cudd_addXnor */
DdNode
Definition: cudd.h:278
cuddIsConstant
#define cuddIsConstant(node)
Definition: cuddInt.h:620
DD_ONE
#define DD_ONE(dd)
Definition: cuddInt.h:911
DD_ZERO
#define DD_ZERO(dd)
Definition: cuddInt.h:927
DdNode* Cudd_addXor ( DdManager *  dd,
DdNode **  f,
DdNode **  g 
)

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

Synopsis [XOR of two 0-1 ADDs.]

Description [XOR of two 0-1 ADDs. Returns NULL if not a terminal case; f XOR g otherwise.]

SideEffects [None]

SeeAlso [Cudd_addApply]

Definition at line 679 of file cuddAddApply.c.

683 {
684  DdNode *F, *G;
685 
686  F = *f; G = *g;
687  if (F == G) return(DD_ZERO(dd));
688  if (F == DD_ONE(dd) && G == DD_ZERO(dd)) return(DD_ONE(dd));
689  if (G == DD_ONE(dd) && F == DD_ZERO(dd)) return(DD_ONE(dd));
690  if (cuddIsConstant(F) && cuddIsConstant(G)) return(DD_ZERO(dd));
691  if (F > G) { /* swap f and g */
692  *f = G;
693  *g = F;
694  }
695  return(NULL);
696 
697 } /* end of Cudd_addXor */
DdNode
Definition: cudd.h:278
cuddIsConstant
#define cuddIsConstant(node)
Definition: cuddInt.h:620
DD_ONE
#define DD_ONE(dd)
Definition: cuddInt.h:911
DD_ZERO
#define DD_ZERO(dd)
Definition: cuddInt.h:927
DdNode* cuddAddApplyRecur ( DdManager *  dd,
DD_AOP  op,
DdNode *  f,
DdNode *  g 
)

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

Synopsis [Performs the recursive step of Cudd_addApply.]

Description [Performs the recursive step of Cudd_addApply. Returns a pointer to the result if successful; NULL otherwise.]

SideEffects [None]

SeeAlso [cuddAddMonadicApplyRecur]

Definition at line 809 of file cuddAddApply.c.

814 {
815  DdNode *res,
816  *fv, *fvn, *gv, *gvn,
817  *T, *E;
818  unsigned int ford, gord;
819  unsigned int index;
820  DD_CTFP cacheOp;
821 
822  /* Check terminal cases. Op may swap f and g to increase the
823  * cache hit rate.
824  */
825  statLine(dd);
826  res = (*op)(dd,&f,&g);
827  if (res != NULL) return(res);
828 
829  /* Check cache. */
830  cacheOp = (DD_CTFP) op;
831  res = cuddCacheLookup2(dd,cacheOp,f,g);
832  if (res != NULL) return(res);
833 
834  /* Recursive step. */
835  ford = cuddI(dd,f->index);
836  gord = cuddI(dd,g->index);
837  if (ford <= gord) {
838  index = f->index;
839  fv = cuddT(f);
840  fvn = cuddE(f);
841  } else {
842  index = g->index;
843  fv = fvn = f;
844  }
845  if (gord <= ford) {
846  gv = cuddT(g);
847  gvn = cuddE(g);
848  } else {
849  gv = gvn = g;
850  }
851 
852  T = cuddAddApplyRecur(dd,op,fv,gv);
853  if (T == NULL) return(NULL);
854  cuddRef(T);
855 
856  E = cuddAddApplyRecur(dd,op,fvn,gvn);
857  if (E == NULL) {
858  Cudd_RecursiveDeref(dd,T);
859  return(NULL);
860  }
861  cuddRef(E);
862 
863  res = (T == E) ? T : cuddUniqueInter(dd,(int)index,T,E);
864  if (res == NULL) {
865  Cudd_RecursiveDeref(dd, T);
866  Cudd_RecursiveDeref(dd, E);
867  return(NULL);
868  }
869  cuddDeref(T);
870  cuddDeref(E);
871 
872  /* Store result. */
873  cuddCacheInsert2(dd,cacheOp,f,g,res);
874 
875  return(res);
876 
877 } /* end of cuddAddApplyRecur */
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
cuddAddApplyRecur
DdNode * cuddAddApplyRecur(DdManager *dd, DD_AOP op, DdNode *f, DdNode *g)
Definition: cuddAddApply.c:809
DD_CTFP
DdNode *(* DD_CTFP)(DdManager *, DdNode *, DdNode *)
Definition: cudd.h:321
statLine
#define statLine(dd)
Definition: cuddInt.h:1037
cuddCacheLookup2
DdNode * cuddCacheLookup2(DdManager *table, DD_CTFP op, DdNode *f, DdNode *g)
Definition: cuddCache.c:502
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
cuddUniqueInter
DdNode * cuddUniqueInter(DdManager *unique, int index, DdNode *T, DdNode *E)
Definition: cuddTable.c:1128
DdNode* cuddAddMonadicApplyRecur ( DdManager *  dd,
DD_MAOP  op,
DdNode *  f 
)

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

Synopsis [Performs the recursive step of Cudd_addMonadicApply.]

Description [Performs the recursive step of Cudd_addMonadicApply. Returns a pointer to the result if successful; NULL otherwise.]

SideEffects [None]

SeeAlso [cuddAddApplyRecur]

Definition at line 893 of file cuddAddApply.c.

897 {
898  DdNode *res, *ft, *fe, *T, *E;
899  unsigned int index;
900 
901  /* Check terminal cases. */
902  statLine(dd);
903  res = (*op)(dd,f);
904  if (res != NULL) return(res);
905 
906  /* Check cache. */
907  res = cuddCacheLookup1(dd,op,f);
908  if (res != NULL) return(res);
909 
910  /* Recursive step. */
911  index = f->index;
912  ft = cuddT(f);
913  fe = cuddE(f);
914 
915  T = cuddAddMonadicApplyRecur(dd,op,ft);
916  if (T == NULL) return(NULL);
917  cuddRef(T);
918 
919  E = cuddAddMonadicApplyRecur(dd,op,fe);
920  if (E == NULL) {
921  Cudd_RecursiveDeref(dd,T);
922  return(NULL);
923  }
924  cuddRef(E);
925 
926  res = (T == E) ? T : cuddUniqueInter(dd,(int)index,T,E);
927  if (res == NULL) {
928  Cudd_RecursiveDeref(dd, T);
929  Cudd_RecursiveDeref(dd, E);
930  return(NULL);
931  }
932  cuddDeref(T);
933  cuddDeref(E);
934 
935  /* Store result. */
936  cuddCacheInsert1(dd,op,f,res);
937 
938  return(res);
939 
940 } /* end of cuddAddMonadicApplyRecur */
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
cuddAddMonadicApplyRecur
DdNode * cuddAddMonadicApplyRecur(DdManager *dd, DD_MAOP op, DdNode *f)
Definition: cuddAddApply.c:893
statLine
#define statLine(dd)
Definition: cuddInt.h:1037
cuddCacheLookup1
DdNode * cuddCacheLookup1(DdManager *table, DD_CTFP1 op, DdNode *f)
Definition: cuddCache.c:556
cuddT
#define cuddT(node)
Definition: cuddInt.h:636
DdNode::index
DdHalfWord index
Definition: cudd.h:279
cuddE
#define cuddE(node)
Definition: cuddInt.h:652
cuddUniqueInter
DdNode * cuddUniqueInter(DdManager *unique, int index, DdNode *T, DdNode *E)
Definition: cuddTable.c:1128
cuddCacheInsert1
void cuddCacheInsert1(DdManager *table, DD_CTFP1 op, DdNode *f, DdNode *data)
Definition: cuddCache.c:323

Variable Documentation

ABC_NAMESPACE_IMPL_START char rcsid [] DD_UNUSED = "$Id: cuddAddApply.c,v 1.18 2009/02/19 16:15:26 fabio Exp $"
static

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

FileName [cuddAddApply.c]

PackageName [cudd]

Synopsis [Apply functions for ADDs and their operators.]

Description [External procedures included in this module:

Internal 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 99 of file cuddAddApply.c.