Main Page Namespace List Class Hierarchy Alphabetical List Compound List File List Namespace Members Compound Members File Members

cudd.h File Reference

#include "mtr.h"

Include dependency graph for cudd.h:

This graph shows which files directly or indirectly include this file:

Go to the source code of this file.

Compounds

struct DdChildren

struct DdNode

Defines

#define CUDD_VERSION   "2.3.0"

#define SIZEOF_VOID_P   4

#define SIZEOF_INT   4

#define SIZEOF_LONG   4

#define TRUE   1

#define FALSE   0

#define CUDD_VALUE_TYPE   double

#define CUDD_OUT_OF_MEM   -1

#define CUDD_UNIQUE_SLOTS   256

#define CUDD_CACHE_SLOTS   262144

#define CUDD_RESIDUE_DEFAULT   0

#define CUDD_RESIDUE_MSB   1

#define CUDD_RESIDUE_TC   2

#define CUDD_MAXINDEX   ((DdHalfWord) ~0)

#define DD_APA_BITS   16

#define DD_APA_BASE   (1 << DD_APA_BITS)

#define DD_APA_MASK   (DD_APA_BASE - 1)

#define DD_APA_HEXPRINT   "%04x"

#define Cudd_IsConstant(node)   ((Cudd_Regular(node))->index == CUDD_MAXINDEX)

#define Cudd_Not(node)   ((DdNode *)((long)(node) ^ 01))

#define Cudd_NotCond(node, c)   ((DdNode *)((long)(node) ^ (c)))

#define Cudd_Regular(node)   ((DdNode *)((unsigned long)(node) & ~01))

#define Cudd_Complement(node)   ((DdNode *)((unsigned long)(node) | 01))

#define Cudd_IsComplement(node)   ((int) ((long) (node) & 01))

#define Cudd_T(node)   ((Cudd_Regular(node))->type.kids.T)

#define Cudd_E(node)   ((Cudd_Regular(node))->type.kids.E)

#define Cudd_V(node)   ((Cudd_Regular(node))->type.value)

#define Cudd_ReadIndex(dd, index)   (Cudd_ReadPerm(dd,index))

#define Cudd_ForeachCube(manager, f, gen, cube, value)

#define Cudd_ForeachNode(manager, f, gen, node)

#define EXTERN   extern

#define ARGS(protos)   ()

Typedefs

typedef unsigned short DdHalfWord

typedef DdNode DdNode

typedef DdChildren DdChildren

typedef DdManager DdManager

typedef DdGen DdGen

typedef unsigned short int DdApaDigit

typedef unsigned long int DdApaDoubleDigit

typedef DdApaDigit * DdApaNumber

Enumerations

enum Cudd_ReorderingType {
  CUDD_REORDER_SAME, CUDD_REORDER_NONE, CUDD_REORDER_RANDOM, CUDD_REORDER_RANDOM_PIVOT,
  CUDD_REORDER_SIFT, CUDD_REORDER_SIFT_CONVERGE, CUDD_REORDER_SYMM_SIFT, CUDD_REORDER_SYMM_SIFT_CONV,
  CUDD_REORDER_WINDOW2, CUDD_REORDER_WINDOW3, CUDD_REORDER_WINDOW4, CUDD_REORDER_WINDOW2_CONV,
  CUDD_REORDER_WINDOW3_CONV, CUDD_REORDER_WINDOW4_CONV, CUDD_REORDER_GROUP_SIFT, CUDD_REORDER_GROUP_SIFT_CONV,
  CUDD_REORDER_ANNEALING, CUDD_REORDER_GENETIC, CUDD_REORDER_LINEAR, CUDD_REORDER_LINEAR_CONVERGE,
  CUDD_REORDER_EXACT
}

enum Cudd_AggregationType {
  CUDD_NO_CHECK, CUDD_GROUP_CHECK, CUDD_GROUP_CHECK2, CUDD_GROUP_CHECK3,
  CUDD_GROUP_CHECK4, CUDD_GROUP_CHECK5, CUDD_GROUP_CHECK6, CUDD_GROUP_CHECK7,
  CUDD_GROUP_CHECK8, CUDD_GROUP_CHECK9
}

enum Cudd_HookType { CUDD_PRE_GC_HOOK, CUDD_POST_GC_HOOK, CUDD_PRE_REORDERING_HOOK, CUDD_POST_REORDERING_HOOK }

enum Cudd_ErrorType {
  CUDD_NO_ERROR, CUDD_MEMORY_OUT, CUDD_TOO_MANY_NODES, CUDD_MAX_MEM_EXCEEDED,
  CUDD_INVALID_ARG, CUDD_INTERNAL_ERROR
}

Functions

EXTERN DdNode *Cudd_addNewVar ARGS ((DdManager *dd))

EXTERN DdNode *Cudd_addNewVarAtLevel ARGS ((DdManager *dd, int level))

EXTERN DdNode *Cudd_addIthVar ARGS ((DdManager *dd, int i))

EXTERN int Cudd_zddVarsFromBddVars ARGS ((DdManager *dd, int multiplicity))

EXTERN DdNode *Cudd_addConst ARGS ((DdManager *dd, CUDD_VALUE_TYPE c))

EXTERN int Cudd_IsNonConstant ARGS ((DdNode *f))

EXTERN void Cudd_AutodynEnable ARGS ((DdManager *unique, Cudd_ReorderingType method))

EXTERN void Cudd_AutodynDisable ARGS ((DdManager *unique))

EXTERN int Cudd_ReorderingStatus ARGS ((DdManager *unique, Cudd_ReorderingType *method))

EXTERN void Cudd_SetBackground ARGS ((DdManager *dd, DdNode *bck))

EXTERN void Cudd_SetMinHit ARGS ((DdManager *dd, unsigned int hr))

EXTERN void Cudd_SetLooseUpTo ARGS ((DdManager *dd, unsigned int lut))

EXTERN void Cudd_SetMaxCacheHard ARGS ((DdManager *dd, unsigned int mc))

EXTERN void Cudd_SetSiftMaxVar ARGS ((DdManager *dd, int smv))

EXTERN void Cudd_SetSiftMaxSwap ARGS ((DdManager *dd, int sms))

EXTERN void Cudd_SetMaxGrowth ARGS ((DdManager *dd, double mg))

EXTERN void Cudd_SetTree ARGS ((DdManager *dd, MtrNode *tree))

EXTERN unsigned int Cudd_NodeReadIndex ARGS ((DdNode *node))

EXTERN void Cudd_SetEpsilon ARGS ((DdManager *dd, CUDD_VALUE_TYPE ep))

EXTERN void Cudd_SetGroupcheck ARGS ((DdManager *dd, Cudd_AggregationType gc))

EXTERN void Cudd_SetRecomb ARGS ((DdManager *dd, int recomb))

EXTERN void Cudd_SetSymmviolation ARGS ((DdManager *dd, int symmviolation))

EXTERN void Cudd_SetArcviolation ARGS ((DdManager *dd, int arcviolation))

EXTERN void Cudd_SetPopulationSize ARGS ((DdManager *dd, int populationSize))

EXTERN void Cudd_SetNumberXovers ARGS ((DdManager *dd, int numberXovers))

EXTERN int Cudd_PrintInfo ARGS ((DdManager *dd, FILE *fp))

EXTERN int Cudd_AddHook ARGS ((DdManager *dd, int(*f)(DdManager *, char *, void *), Cudd_HookType where))

EXTERN int Cudd_StdPreReordHook ARGS ((DdManager *dd, char *str, void *data))

EXTERN void Cudd_SetMaxLive ARGS ((DdManager *dd, unsigned int maxLive))

EXTERN void Cudd_SetMaxMemory ARGS ((DdManager *dd, long maxMemory))

EXTERN void Cudd_SetNextReordering ARGS ((DdManager *dd, unsigned int next))

EXTERN DdNode *Cudd_addExistAbstract ARGS ((DdManager *manager, DdNode *f, DdNode *cube))

EXTERN DdNode *Cudd_addApply ARGS ((DdManager *dd, DdNode *(*)(DdManager *, DdNode **, DdNode **), DdNode *f, DdNode *g))

EXTERN DdNode *Cudd_addPlus ARGS ((DdManager *dd, DdNode **f, DdNode **g))

EXTERN DdNode *Cudd_addFindMax ARGS ((DdManager *dd, DdNode *f))

EXTERN DdNode *Cudd_addIthBit ARGS ((DdManager *dd, DdNode *f, int bit))

EXTERN DdNode *Cudd_addScalarInverse ARGS ((DdManager *dd, DdNode *f, DdNode *epsilon))

EXTERN DdNode *Cudd_addIte ARGS ((DdManager *dd, DdNode *f, DdNode *g, DdNode *h))

EXTERN DdNode *Cudd_addEvalConst ARGS ((DdManager *dd, DdNode *f, DdNode *g))

EXTERN DdNode *Cudd_addRoundOff ARGS ((DdManager *dd, DdNode *f, int N))

EXTERN DdNode *Cudd_addWalsh ARGS ((DdManager *dd, DdNode **x, DdNode **y, int n))

EXTERN DdNode *Cudd_addResidue ARGS ((DdManager *dd, int n, int m, int options, int top))

EXTERN DdNode *Cudd_bddAndAbstract ARGS ((DdManager *manager, DdNode *f, DdNode *g, DdNode *cube))

EXTERN int Cudd_ApaNumberOfDigits ARGS ((int binaryDigits))

EXTERN DdApaNumber Cudd_NewApaNumber ARGS ((int digits))

EXTERN void Cudd_ApaCopy ARGS ((int digits, DdApaNumber source, DdApaNumber dest))

EXTERN DdApaDigit Cudd_ApaAdd ARGS ((int digits, DdApaNumber a, DdApaNumber b, DdApaNumber sum))

EXTERN DdApaDigit Cudd_ApaSubtract ARGS ((int digits, DdApaNumber a, DdApaNumber b, DdApaNumber diff))

EXTERN DdApaDigit Cudd_ApaShortDivision ARGS ((int digits, DdApaNumber dividend, DdApaDigit divisor, DdApaNumber quotient))

EXTERN unsigned int Cudd_ApaIntDivision ARGS ((int digits, DdApaNumber dividend, unsigned int divisor, DdApaNumber quotient))

EXTERN void Cudd_ApaShiftRight ARGS ((int digits, DdApaDigit in, DdApaNumber a, DdApaNumber b))

EXTERN void Cudd_ApaSetToLiteral ARGS ((int digits, DdApaNumber number, DdApaDigit literal))

EXTERN void Cudd_ApaPowerOfTwo ARGS ((int digits, DdApaNumber number, int power))

EXTERN int Cudd_ApaCompare ARGS ((int digitsFirst, DdApaNumber first, int digitsSecond, DdApaNumber second))

EXTERN int Cudd_ApaCompareRatios ARGS ((int digitsFirst, DdApaNumber firstNum, unsigned int firstDen, int digitsSecond, DdApaNumber secondNum, unsigned int secondDen))

EXTERN int Cudd_ApaPrintHex ARGS ((FILE *fp, int digits, DdApaNumber number))

EXTERN int Cudd_ApaPrintExponential ARGS ((FILE *fp, int digits, DdApaNumber number, int precision))

EXTERN DdApaNumber Cudd_ApaCountMinterm ARGS ((DdManager *manager, DdNode *node, int nvars, int *digits))

EXTERN int Cudd_ApaPrintMinterm ARGS ((FILE *fp, DdManager *dd, DdNode *node, int nvars))

EXTERN int Cudd_ApaPrintMintermExp ARGS ((FILE *fp, DdManager *dd, DdNode *node, int nvars, int precision))

EXTERN int Cudd_ApaPrintDensity ARGS ((FILE *fp, DdManager *dd, DdNode *node, int nvars))

EXTERN DdNode *Cudd_UnderApprox ARGS ((DdManager *dd, DdNode *f, int numVars, int threshold, int safe, double quality))

EXTERN DdNode *Cudd_RemapUnderApprox ARGS ((DdManager *dd, DdNode *f, int numVars, int threshold, double quality))

EXTERN DdNode *Cudd_BiasedUnderApprox ARGS ((DdManager *dd, DdNode *f, DdNode *b, int numVars, int threshold, double quality1, double quality0))

EXTERN DdNode *Cudd_bddBooleanDiff ARGS ((DdManager *manager, DdNode *f, int x))

EXTERN int Cudd_bddVarIsDependent ARGS ((DdManager *dd, DdNode *f, DdNode *var))

EXTERN double Cudd_bddCorrelation ARGS ((DdManager *manager, DdNode *f, DdNode *g))

EXTERN double Cudd_bddCorrelationWeights ARGS ((DdManager *manager, DdNode *f, DdNode *g, double *prob))

EXTERN DdNode *Cudd_addBddThreshold ARGS ((DdManager *dd, DdNode *f, CUDD_VALUE_TYPE value))

EXTERN DdNode *Cudd_addBddInterval ARGS ((DdManager *dd, DdNode *f, CUDD_VALUE_TYPE lower, CUDD_VALUE_TYPE upper))

EXTERN DdNode *Cudd_BddToAdd ARGS ((DdManager *dd, DdNode *B))

EXTERN DdNode *Cudd_bddTransfer ARGS ((DdManager *ddSource, DdManager *ddDestination, DdNode *f))

EXTERN int Cudd_DebugCheck ARGS ((DdManager *table))

EXTERN DdNode *Cudd_bddClippingAnd ARGS ((DdManager *dd, DdNode *f, DdNode *g, int maxDepth, int direction))

EXTERN DdNode *Cudd_bddClippingAndAbstract ARGS ((DdManager *dd, DdNode *f, DdNode *g, DdNode *cube, int maxDepth, int direction))

EXTERN DdNode *Cudd_bddCompose ARGS ((DdManager *dd, DdNode *f, DdNode *g, int v))

EXTERN DdNode *Cudd_addPermute ARGS ((DdManager *manager, DdNode *node, int *permut))

EXTERN DdNode *Cudd_addSwapVariables ARGS ((DdManager *dd, DdNode *f, DdNode **x, DdNode **y, int n))

EXTERN DdNode *Cudd_bddVarMap ARGS ((DdManager *manager, DdNode *f))

EXTERN int Cudd_SetVarMap ARGS ((DdManager *manager, DdNode **x, DdNode **y, int n))

EXTERN DdNode *Cudd_bddAdjPermuteX ARGS ((DdManager *dd, DdNode *B, DdNode **x, int n))

EXTERN DdNode *Cudd_addVectorCompose ARGS ((DdManager *dd, DdNode *f, DdNode **vector))

EXTERN int Cudd_bddApproxConjDecomp ARGS ((DdManager *dd, DdNode *f, DdNode ***conjuncts))

EXTERN int Cudd_bddApproxDisjDecomp ARGS ((DdManager *dd, DdNode *f, DdNode ***disjuncts))

EXTERN int Cudd_bddIsVarEssential ARGS ((DdManager *manager, DdNode *f, int id, int phase))

EXTERN int Cudd_DumpBlif ARGS ((DdManager *dd, int n, DdNode **f, char **inames, char **onames, char *mname, FILE *fp))

EXTERN int Cudd_DumpBlifBody ARGS ((DdManager *dd, int n, DdNode **f, char **inames, char **onames, FILE *fp))

EXTERN DdNode *Cudd_bddConstrain ARGS ((DdManager *dd, DdNode *f, DdNode *c))

EXTERN DdNode *Cudd_bddSqueeze ARGS ((DdManager *dd, DdNode *l, DdNode *u))

EXTERN DdNode *Cudd_SubsetCompress ARGS ((DdManager *dd, DdNode *f, int nvars, int threshold))

EXTERN MtrNode *Cudd_MakeTreeNode ARGS ((DdManager *dd, unsigned int low, unsigned int size, unsigned int type))

EXTERN int Cudd_addHarwell ARGS ((FILE *fp, DdManager *dd, DdNode **E, DdNode ***x, DdNode ***y, DdNode ***xn, DdNode ***yn_, int *nx, int *ny, int *m, int *n, int bx, int sx, int by, int sy, int pr))

EXTERN DdManager *Cudd_Init ARGS ((unsigned int numVars, unsigned int numVarsZ, unsigned int numSlots, unsigned int cacheSize, unsigned long maxMemory))

EXTERN int Cudd_ReadLinear ARGS ((DdManager *table, int x, int y))

EXTERN DdNode *Cudd_addMatrixMultiply ARGS ((DdManager *dd, DdNode *A, DdNode *B, DdNode **z, int nz))

EXTERN DdNode *Cudd_addTriangle ARGS ((DdManager *dd, DdNode *f, DdNode *g, DdNode **z, int nz))

EXTERN DdNode *Cudd_PrioritySelect ARGS ((DdManager *dd, DdNode *R, DdNode **x, DdNode **y, DdNode **z, DdNode *Pi, int n, DdNode *(*)(DdManager *, int, DdNode **, DdNode **, DdNode **)))

EXTERN DdNode *Cudd_Xgty ARGS ((DdManager *dd, int N, DdNode **z, DdNode **x, DdNode **y))

EXTERN DdNode *Cudd_Xeqy ARGS ((DdManager *dd, int N, DdNode **x, DdNode **y))

EXTERN DdNode *Cudd_Dxygtdxz ARGS ((DdManager *dd, int N, DdNode **x, DdNode **y, DdNode **z))

EXTERN DdNode *Cudd_CProjection ARGS ((DdManager *dd, DdNode *R, DdNode *Y))

EXTERN DdNode *Cudd_addHamming ARGS ((DdManager *dd, DdNode **xVars, DdNode **yVars, int nVars))

EXTERN int Cudd_MinHammingDist ARGS ((DdManager *dd, DdNode *f, int *minterm, int upperBound))

EXTERN int Cudd_addRead ARGS ((FILE *fp, DdManager *dd, DdNode **E, DdNode ***x, DdNode ***y, DdNode ***xn, DdNode ***yn_, int *nx, int *ny, int *m, int *n, int bx, int sx, int by, int sy))

EXTERN int Cudd_bddRead ARGS ((FILE *fp, DdManager *dd, DdNode **E, DdNode ***x, DdNode ***y, int *nx, int *ny, int *m, int *n, int bx, int sx, int by, int sy))

EXTERN void Cudd_Ref ARGS ((DdNode *n))

EXTERN void Cudd_RecursiveDeref ARGS ((DdManager *table, DdNode *n))

EXTERN int Cudd_CheckZeroRef ARGS ((DdManager *manager))

EXTERN int Cudd_ReduceHeap ARGS ((DdManager *table, Cudd_ReorderingType heuristic, int minsize))

EXTERN int Cudd_ShuffleHeap ARGS ((DdManager *table, int *permutation))

EXTERN DdNode *Cudd_Eval ARGS ((DdManager *dd, DdNode *f, int *inputs))

EXTERN DdNode *Cudd_ShortestPath ARGS ((DdManager *manager, DdNode *f, int *weight, int *support, int *length))

EXTERN DdNode *Cudd_LargestCube ARGS ((DdManager *manager, DdNode *f, int *length))

EXTERN int Cudd_ShortestLength ARGS ((DdManager *manager, DdNode *f, int *weight))

EXTERN DdNode *Cudd_Decreasing ARGS ((DdManager *dd, DdNode *f, int i))

EXTERN int Cudd_EquivDC ARGS ((DdManager *dd, DdNode *F, DdNode *G, DdNode *D))

EXTERN int Cudd_EqualSupNorm ARGS ((DdManager *dd, DdNode *f, DdNode *g, CUDD_VALUE_TYPE tolerance, int pr))

EXTERN double *Cudd_CofMinterm ARGS ((DdManager *dd, DdNode *node))

EXTERN DdNode *Cudd_SolveEqn ARGS ((DdManager *bdd, DdNode *F, DdNode *Y, DdNode **G, int **yIndex, int n))

EXTERN DdNode *Cudd_VerifySol ARGS ((DdManager *bdd, DdNode *F, DdNode **G, int *yIndex, int n))

EXTERN DdNode *Cudd_SplitSet ARGS ((DdManager *manager, DdNode *S, DdNode **xVars, int n, double m))

EXTERN DdNode *Cudd_SubsetHeavyBranch ARGS ((DdManager *dd, DdNode *f, int numVars, int threshold))

EXTERN DdNode *Cudd_SubsetShortPaths ARGS ((DdManager *dd, DdNode *f, int numVars, int threshold, int hardlimit))

EXTERN void Cudd_SymmProfile ARGS ((DdManager *table, int lower, int upper))

EXTERN unsigned int Cudd_Prime ARGS ((unsigned int p))

EXTERN int Cudd_PrintMinterm ARGS ((DdManager *manager, DdNode *node))

EXTERN int Cudd_PrintDebug ARGS ((DdManager *dd, DdNode *f, int n, int pr))

EXTERN int Cudd_EstimateCofactor ARGS ((DdManager *dd, DdNode *node, int i, int phase))

EXTERN int Cudd_EstimateCofactorSimple ARGS ((DdNode *node, int i))

EXTERN int Cudd_SharingSize ARGS ((DdNode **nodeArray, int n))

EXTERN double Cudd_CountMinterm ARGS ((DdManager *manager, DdNode *node, int nvars))

EXTERN DdNode *Cudd_VectorSupport ARGS ((DdManager *dd, DdNode **F, int n))

EXTERN int Cudd_ClassifySupport ARGS ((DdManager *dd, DdNode *f, DdNode *g, DdNode **common, DdNode **onlyF, DdNode **onlyG))

EXTERN int Cudd_bddPickOneCube ARGS ((DdManager *ddm, DdNode *node, char *string))

EXTERN DdNode *Cudd_bddPickOneMinterm ARGS ((DdManager *dd, DdNode *f, DdNode **vars, int n))

EXTERN DdNode **Cudd_bddPickArbitraryMinterms ARGS ((DdManager *dd, DdNode *f, DdNode **vars, int n, int k))

EXTERN DdGen *Cudd_FirstCube ARGS ((DdManager *dd, DdNode *f, int **cube, CUDD_VALUE_TYPE *value))

EXTERN int Cudd_NextCube ARGS ((DdGen *gen, int **cube, CUDD_VALUE_TYPE *value))

EXTERN DdNode *Cudd_bddComputeCube ARGS ((DdManager *dd, DdNode **vars, int *phase, int n))

EXTERN DdGen *Cudd_FirstNode ARGS ((DdManager *dd, DdNode *f, DdNode **node))

EXTERN int Cudd_NextNode ARGS ((DdGen *gen, DdNode **node))

EXTERN int Cudd_GenFree ARGS ((DdGen *gen))

EXTERN DdNode *Cudd_IndicesToCube ARGS ((DdManager *dd, int *array, int n))

EXTERN void Cudd_PrintVersion ARGS ((FILE *fp))

EXTERN long Cudd_Random ARGS (())

EXTERN void Cudd_Srandom ARGS ((long seed))

EXTERN double Cudd_Density ARGS ((DdManager *dd, DdNode *f, int nvars))

EXTERN void Cudd_OutOfMem ARGS ((long size))

EXTERN int Cudd_zddCount ARGS ((DdManager *zdd, DdNode *P))

EXTERN DdNode *Cudd_zddIsop ARGS ((DdManager *dd, DdNode *L, DdNode *U, DdNode **zdd_I))

EXTERN DdNode *Cudd_bddIsop ARGS ((DdManager *dd, DdNode *L, DdNode *U))

EXTERN int Cudd_zddDagSize ARGS ((DdNode *p_node))

EXTERN double Cudd_zddCountMinterm ARGS ((DdManager *zdd, DdNode *node, int path))

EXTERN DdNode *Cudd_zddUnion ARGS ((DdManager *dd, DdNode *P, DdNode *Q))

EXTERN DdNode *Cudd_zddDiffConst ARGS ((DdManager *zdd, DdNode *P, DdNode *Q))

EXTERN DdNode *Cudd_zddSubset1 ARGS ((DdManager *dd, DdNode *P, int var))

EXTERN int Cudd_zddPrintMinterm ARGS ((DdManager *zdd, DdNode *node))

EXTERN int Cudd_zddPrintDebug ARGS ((DdManager *zdd, DdNode *f, int n, int pr))

Define Documentation

#define ARGS ( protos ) ()

Definition at line 473 of file cudd.h.

#define CUDD_CACHE_SLOTS 262144

Definition at line 66 of file cudd.h.

#define Cudd_Complement ( node ) ((DdNode *)((unsigned long)(node) | 01))

Macro***********************************************************************
Synopsis [Returns the complemented version of a pointer.]
Description []
SideEffects [none]
SeeAlso [Cudd_Regular Cudd_IsComplement]
Definition at line 313 of file cudd.h.

#define Cudd_E ( node ) ((Cudd_Regular(node))->type.kids.E)

Macro***********************************************************************
Synopsis [Returns the else child of an internal node.]
Description [Returns the else child of an internal node. If node is a constant node, the result is unpredictable.]
SideEffects [none]
SeeAlso [Cudd_T Cudd_V]
Definition at line 357 of file cudd.h.

#define Cudd_ForeachCube ( manager,
f,
gen,
cube,
value )

Value:
for((gen) = Cudd_FirstCube(manager, f, &cube, &value);\ Cudd_IsGenEmpty(gen) ? Cudd_GenFree(gen) : TRUE;\ (void) Cudd_NextCube(gen, &cube, &value))
Macro***********************************************************************
Synopsis [Iterates over the cubes of a decision diagram.]
Description [Iterates over the cubes of a decision diagram f.

DdManager *manager;
DdNode *f;
DdGen *gen;
int **cube;
CUDD_VALUE_TYPE *value;
Cudd_ForeachCube allocates and frees the generator. Therefore the application should not try to do that. Also, the cube is freed at the end of Cudd_ForeachCube and hence is not available outside of the loop.
CAUTION: It is assumed that dynamic reordering will not occur while there are open generators. It is the user's responsibility to make sure that dynamic reordering does not occur. As long as new nodes are not created during generation, and dynamic reordering is not called explicitly, dynamic reordering will not occur. Alternatively, it is sufficient to disable dynamic reordering. It is a mistake to dispose of a diagram on which generation is ongoing.]
SideEffects [none]
SeeAlso [Cudd_ForeachNode Cudd_FirstCube Cudd_NextCube Cudd_GenFree Cudd_IsGenEmpty Cudd_AutodynDisable]
Definition at line 421 of file cudd.h.

#define Cudd_ForeachNode ( manager,
f,
gen,
node )

Value:
for((gen) = Cudd_FirstNode(manager, f, &node);\ Cudd_IsGenEmpty(gen) ? Cudd_GenFree(gen) : TRUE;\ (void) Cudd_NextNode(gen, &node))
Macro***********************************************************************
Synopsis [Iterates over the nodes of a decision diagram.]
Description [Iterates over the nodes of a decision diagram f.

DdManager *manager;
DdNode *f;
DdGen *gen;
DdNode **node;
The nodes are returned in a seemingly random order. Cudd_ForeachNode allocates and frees the generator. Therefore the application should not try to do that.
CAUTION: It is assumed that dynamic reordering will not occur while there are open generators. It is the user's responsibility to make sure that dynamic reordering does not occur. As long as new nodes are not created during generation, and dynamic reordering is not called explicitly, dynamic reordering will not occur. Alternatively, it is sufficient to disable dynamic reordering. It is a mistake to dispose of a diagram on which generation is ongoing.]
SideEffects [none]
SeeAlso [Cudd_ForeachCube Cudd_FirstNode Cudd_NextNode Cudd_GenFree Cudd_IsGenEmpty Cudd_AutodynDisable]
Definition at line 455 of file cudd.h.

#define Cudd_IsComplement ( node ) ((int) ((long) (node) & 01))

Macro***********************************************************************
Synopsis [Returns 1 if a pointer is complemented.]
Description []
SideEffects [none]
SeeAlso [Cudd_Regular Cudd_Complement]
Definition at line 327 of file cudd.h.

#define Cudd_IsConstant ( node ) ((Cudd_Regular(node))->index == CUDD_MAXINDEX)

Macro***********************************************************************
Synopsis [Returns 1 if the node is a constant node.]
Description [Returns 1 if the node is a constant node (rather than an internal node). All constant nodes have the same index (CUDD_MAXINDEX). The pointer passed to Cudd_IsConstant may be either regular or complemented.]
SideEffects [none]
SeeAlso []
Definition at line 254 of file cudd.h.

#define CUDD_MAXINDEX ((DdHalfWord) ~0)

Definition at line 80 of file cudd.h.
Referenced by _scv_constraint_manager::_scv_constraint_manager().

#define Cudd_Not ( node ) ((DdNode *)((long)(node) ^ 01))

Macro***********************************************************************
Synopsis [Complements a DD.]
Description [Complements a DD by flipping the complement attribute of the pointer (the least significant bit).]
SideEffects [none]
SeeAlso [Cudd_NotCond]
Definition at line 269 of file cudd.h.

#define Cudd_NotCond ( node,
c ) ((DdNode *)((long)(node) ^ (c)))

Macro***********************************************************************
Synopsis [Complements a DD if a condition is true.]
Description [Complements a DD if condition c is true; c should be either 0 or 1, because it is used directly (for efficiency). If in doubt on the values c may take, use "(c) ? Cudd_Not(node) : node".]
SideEffects [none]
SeeAlso [Cudd_Not]
Definition at line 285 of file cudd.h.

#define CUDD_OUT_OF_MEM -1

Definition at line 63 of file cudd.h.

#define Cudd_ReadIndex ( dd,
index ) (Cudd_ReadPerm(dd,index))

Macro***********************************************************************
Synopsis [Returns the current position in the order of variable index.]
Description [Returns the current position in the order of variable index. This macro is obsolete and is kept for compatibility. New applications should use Cudd_ReadPerm instead.]
SideEffects [none]
SeeAlso [Cudd_ReadPerm]
Definition at line 389 of file cudd.h.

#define Cudd_Regular ( node ) ((DdNode *)((unsigned long)(node) & ~01))

Macro***********************************************************************
Synopsis [Returns the regular version of a pointer.]
Description []
SideEffects [none]
SeeAlso [Cudd_Complement Cudd_IsComplement]
Definition at line 299 of file cudd.h.

#define CUDD_RESIDUE_DEFAULT 0

Definition at line 69 of file cudd.h.

#define CUDD_RESIDUE_MSB 1

Definition at line 70 of file cudd.h.

#define CUDD_RESIDUE_TC 2

Definition at line 71 of file cudd.h.

#define Cudd_T ( node ) ((Cudd_Regular(node))->type.kids.T)

Macro***********************************************************************
Synopsis [Returns the then child of an internal node.]
Description [Returns the then child of an internal node. If node is a constant node, the result is unpredictable.]
SideEffects [none]
SeeAlso [Cudd_E Cudd_V]
Definition at line 342 of file cudd.h.

#define CUDD_UNIQUE_SLOTS 256

Definition at line 65 of file cudd.h.

#define Cudd_V ( node ) ((Cudd_Regular(node))->type.value)

Macro***********************************************************************
Synopsis [Returns the value of a constant node.]
Description [Returns the value of a constant node. If node is an internal node, the result is unpredictable.]
SideEffects [none]
SeeAlso [Cudd_T Cudd_E]
Definition at line 372 of file cudd.h.

#define CUDD_VALUE_TYPE double

Definition at line 62 of file cudd.h.

#define CUDD_VERSION "2.3.0"

CHeaderFile*****************************************************************
FileName [cudd.h]
PackageName [cudd]
Synopsis [The University of Colorado decision diagram package.]
Description [External functions and data strucures of the CUDD package.

To turn on the gathering of statistics, define DD_STATS.
To link with mis, define DD_MIS.
Modified by Abelardo Pardo to interface it to VIS. ]
SeeAlso []
Author [Fabio Somenzi]
Copyright [This file was created at the University of Colorado at Boulder. The University of Colorado at Boulder makes no warranty about the suitability of this software for any purpose. It is presented on an AS IS basis.]
Revision [
Id:
cudd.h,v 1.1 2002/09/17 21:58:46 dlm Exp
]
Definition at line 43 of file cudd.h.

#define DD_APA_BASE (1 << DD_APA_BITS)

Definition at line 89 of file cudd.h.

#define DD_APA_BITS 16

Definition at line 88 of file cudd.h.

#define DD_APA_HEXPRINT "%04x"

Definition at line 91 of file cudd.h.

#define DD_APA_MASK (DD_APA_BASE - 1)

Definition at line 90 of file cudd.h.

#define EXTERN extern

Definition at line 466 of file cudd.h.

#define FALSE 0

Definition at line 59 of file cudd.h.

#define SIZEOF_INT 4

Definition at line 49 of file cudd.h.

#define SIZEOF_LONG 4

Definition at line 52 of file cudd.h.

#define SIZEOF_VOID_P 4

Definition at line 46 of file cudd.h.

#define TRUE 1

Definition at line 56 of file cudd.h.

Typedef Documentation

typedef unsigned short int DdApaDigit

Definition at line 226 of file cudd.h.

typedef unsigned long int DdApaDoubleDigit

Definition at line 227 of file cudd.h.

typedef DdApaDigit* DdApaNumber

Definition at line 228 of file cudd.h.

typedef struct DdChildren DdChildren

typedef struct DdGen DdGen

Definition at line 222 of file cudd.h.

typedef unsigned short DdHalfWord

Definition at line 190 of file cudd.h.

typedef struct DdManager DdManager

Definition at line 220 of file cudd.h.

typedef struct DdNode DdNode

Definition at line 198 of file cudd.h.

Enumeration Type Documentation

enum Cudd_AggregationType

Enum************************************************************************
Synopsis [Type of aggregation methods.]
Description [Type of aggregation methods.]
Enumeration values:

CUDD_NO_CHECK

CUDD_GROUP_CHECK

CUDD_GROUP_CHECK2

CUDD_GROUP_CHECK3

CUDD_GROUP_CHECK4

CUDD_GROUP_CHECK5

CUDD_GROUP_CHECK6

CUDD_GROUP_CHECK7

CUDD_GROUP_CHECK8

CUDD_GROUP_CHECK9

Definition at line 141 of file cudd.h.

enum Cudd_ErrorType

Enum************************************************************************
Synopsis [Type of error codes.]
Description [Type of error codes.]
Enumeration values:

CUDD_NO_ERROR

CUDD_MEMORY_OUT

CUDD_TOO_MANY_NODES

CUDD_MAX_MEM_EXCEEDED

CUDD_INVALID_ARG

CUDD_INTERNAL_ERROR

Definition at line 177 of file cudd.h.

enum Cudd_HookType

Enum************************************************************************
Synopsis [Type of hooks.]
Description [Type of hooks.]
Enumeration values:

CUDD_PRE_GC_HOOK

CUDD_POST_GC_HOOK

CUDD_PRE_REORDERING_HOOK

CUDD_POST_REORDERING_HOOK

Definition at line 162 of file cudd.h.

enum Cudd_ReorderingType

Enum************************************************************************
Synopsis [Type of reordering algorithm.]
Description [Type of reordering algorithm.]
Enumeration values:

CUDD_REORDER_SAME

CUDD_REORDER_NONE

CUDD_REORDER_RANDOM

CUDD_REORDER_RANDOM_PIVOT

CUDD_REORDER_SIFT

CUDD_REORDER_SIFT_CONVERGE

CUDD_REORDER_SYMM_SIFT

CUDD_REORDER_SYMM_SIFT_CONV

CUDD_REORDER_WINDOW2

CUDD_REORDER_WINDOW3

CUDD_REORDER_WINDOW4

CUDD_REORDER_WINDOW2_CONV

CUDD_REORDER_WINDOW3_CONV

CUDD_REORDER_WINDOW4_CONV

CUDD_REORDER_GROUP_SIFT

CUDD_REORDER_GROUP_SIFT_CONV

CUDD_REORDER_ANNEALING

CUDD_REORDER_GENETIC

CUDD_REORDER_LINEAR

CUDD_REORDER_LINEAR_CONVERGE

CUDD_REORDER_EXACT

Definition at line 109 of file cudd.h.

Function Documentation

EXTERN int Cudd_zddPrintDebug ARGS ( (DdManager *zdd, DdNode *f, int n, int pr) )

EXTERN int Cudd_zddPrintCover ARGS ( (DdManager *zdd, DdNode *node) )

EXTERN DdNode *cuddZddChange ARGS ( (DdManager *dd, DdNode *P, int var) )

EXTERN DdNode *cuddZddDiff ARGS ( (DdManager *zdd, DdNode *P, DdNode *Q) )

EXTERN DdNode *Cudd_zddDiff ARGS ( (DdManager *dd, DdNode *P, DdNode *Q) )

EXTERN double Cudd_zddCountMinterm ARGS ( (DdManager *zdd, DdNode *node, int path) )

EXTERN int Cudd_zddDagSize ARGS ( (DdNode *p_node) )

EXTERN DdNode* Cudd_bddIsop ARGS ( (DdManager *dd, DdNode *L, DdNode *U) )

EXTERN DdNode* Cudd_zddIsop ARGS ( (DdManager *dd, DdNode *L, DdNode *U, DdNode **zdd_I) )

EXTERN double Cudd_zddCountDouble ARGS ( (DdManager *zdd, DdNode *P) )

EXTERN void Cudd_OutOfMem ARGS ( (long size) )

EXTERN double Cudd_Density ARGS ( (DdManager *dd, DdNode *f, int nvars) )

EXTERN void Cudd_Srandom ARGS ( (long seed) )

EXTERN MtrNode *Mtr_InitTree ARGS ( () )

AutomaticStart************************************************************

EXTERN void Cudd_PrintVersion ARGS ( (FILE *fp) )

EXTERN DdNode* Cudd_IndicesToCube ARGS ( (DdManager *dd, int *array, int n) )

EXTERN int Cudd_IsGenEmpty ARGS ( (DdGen *gen) )

EXTERN int Cudd_NextNode ARGS ( (DdGen *gen, DdNode **node) )

EXTERN DdGen* Cudd_FirstNode ARGS ( (DdManager *dd, DdNode *f, DdNode **node) )

EXTERN DdNode *Cudd_addComputeCube ARGS ( (DdManager *dd, DdNode **vars, int *phase, int n) )

EXTERN int Cudd_NextCube ARGS ( (DdGen *gen, int **cube, CUDD_VALUE_TYPE *value) )

EXTERN DdGen* Cudd_FirstCube ARGS ( (DdManager *dd, DdNode *f, int **cube, CUDD_VALUE_TYPE *value) )

EXTERN DdNode** Cudd_bddPickArbitraryMinterms ARGS ( (DdManager *dd, DdNode *f, DdNode **vars, int n, int k) )

EXTERN DdNode* Cudd_bddPickOneMinterm ARGS ( (


Compounds
struct	DdChildren
struct	DdNode
Defines
#define	CUDD_VERSION "2.3.0"
#define	SIZEOF_VOID_P 4
#define	SIZEOF_INT 4
#define	SIZEOF_LONG 4
#define	TRUE 1
#define	FALSE 0
#define	CUDD_VALUE_TYPE double
#define	CUDD_OUT_OF_MEM -1
#define	CUDD_UNIQUE_SLOTS 256
#define	CUDD_CACHE_SLOTS 262144
#define	CUDD_RESIDUE_DEFAULT 0
#define	CUDD_RESIDUE_MSB 1
#define	CUDD_RESIDUE_TC 2
#define	CUDD_MAXINDEX ((DdHalfWord) ~0)
#define	DD_APA_BITS 16
#define	DD_APA_BASE (1 << DD_APA_BITS)
#define	DD_APA_MASK (DD_APA_BASE - 1)
#define	DD_APA_HEXPRINT "%04x"
#define	Cudd_IsConstant(node) ((Cudd_Regular(node))->index == CUDD_MAXINDEX)
#define	Cudd_Not(node) ((DdNode *)((long)(node) ^ 01))
#define	Cudd_NotCond(node, c) ((DdNode *)((long)(node) ^ (c)))
#define	Cudd_Regular(node) ((DdNode *)((unsigned long)(node) & ~01))
#define	Cudd_Complement(node) ((DdNode *)((unsigned long)(node) \| 01))
#define	Cudd_IsComplement(node) ((int) ((long) (node) & 01))
#define	Cudd_T(node) ((Cudd_Regular(node))->type.kids.T)
#define	Cudd_E(node) ((Cudd_Regular(node))->type.kids.E)
#define	Cudd_V(node) ((Cudd_Regular(node))->type.value)
#define	Cudd_ReadIndex(dd, index) (Cudd_ReadPerm(dd,index))
#define	Cudd_ForeachCube(manager, f, gen, cube, value)
#define	Cudd_ForeachNode(manager, f, gen, node)
#define	EXTERN extern
#define	ARGS(protos) ()
Typedefs
typedef unsigned short	DdHalfWord
typedef DdNode	DdNode
typedef DdChildren	DdChildren
typedef DdManager	DdManager
typedef DdGen	DdGen
typedef unsigned short int	DdApaDigit
typedef unsigned long int	DdApaDoubleDigit
typedef DdApaDigit *	DdApaNumber
Enumerations
enum	Cudd_ReorderingType { CUDD_REORDER_SAME, CUDD_REORDER_NONE, CUDD_REORDER_RANDOM, CUDD_REORDER_RANDOM_PIVOT, CUDD_REORDER_SIFT, CUDD_REORDER_SIFT_CONVERGE, CUDD_REORDER_SYMM_SIFT, CUDD_REORDER_SYMM_SIFT_CONV, CUDD_REORDER_WINDOW2, CUDD_REORDER_WINDOW3, CUDD_REORDER_WINDOW4, CUDD_REORDER_WINDOW2_CONV, CUDD_REORDER_WINDOW3_CONV, CUDD_REORDER_WINDOW4_CONV, CUDD_REORDER_GROUP_SIFT, CUDD_REORDER_GROUP_SIFT_CONV, CUDD_REORDER_ANNEALING, CUDD_REORDER_GENETIC, CUDD_REORDER_LINEAR, CUDD_REORDER_LINEAR_CONVERGE, CUDD_REORDER_EXACT }
enum	Cudd_AggregationType { CUDD_NO_CHECK, CUDD_GROUP_CHECK, CUDD_GROUP_CHECK2, CUDD_GROUP_CHECK3, CUDD_GROUP_CHECK4, CUDD_GROUP_CHECK5, CUDD_GROUP_CHECK6, CUDD_GROUP_CHECK7, CUDD_GROUP_CHECK8, CUDD_GROUP_CHECK9 }
enum	Cudd_HookType { CUDD_PRE_GC_HOOK, CUDD_POST_GC_HOOK, CUDD_PRE_REORDERING_HOOK, CUDD_POST_REORDERING_HOOK }
enum	Cudd_ErrorType { CUDD_NO_ERROR, CUDD_MEMORY_OUT, CUDD_TOO_MANY_NODES, CUDD_MAX_MEM_EXCEEDED, CUDD_INVALID_ARG, CUDD_INTERNAL_ERROR }
Functions
EXTERN DdNode *Cudd_addNewVar	ARGS ((DdManager *dd))
EXTERN DdNode *Cudd_addNewVarAtLevel	ARGS ((DdManager *dd, int level))
EXTERN DdNode *Cudd_addIthVar	ARGS ((DdManager *dd, int i))
EXTERN int Cudd_zddVarsFromBddVars	ARGS ((DdManager *dd, int multiplicity))
EXTERN DdNode *Cudd_addConst	ARGS ((DdManager *dd, CUDD_VALUE_TYPE c))
EXTERN int Cudd_IsNonConstant	ARGS ((DdNode *f))
EXTERN void Cudd_AutodynEnable	ARGS ((DdManager *unique, Cudd_ReorderingType method))
EXTERN void Cudd_AutodynDisable	ARGS ((DdManager *unique))
EXTERN int Cudd_ReorderingStatus	ARGS ((DdManager unique, Cudd_ReorderingType method))
EXTERN void Cudd_SetBackground	ARGS ((DdManager dd, DdNode bck))
EXTERN void Cudd_SetMinHit	ARGS ((DdManager *dd, unsigned int hr))
EXTERN void Cudd_SetLooseUpTo	ARGS ((DdManager *dd, unsigned int lut))
EXTERN void Cudd_SetMaxCacheHard	ARGS ((DdManager *dd, unsigned int mc))
EXTERN void Cudd_SetSiftMaxVar	ARGS ((DdManager *dd, int smv))
EXTERN void Cudd_SetSiftMaxSwap	ARGS ((DdManager *dd, int sms))
EXTERN void Cudd_SetMaxGrowth	ARGS ((DdManager *dd, double mg))
EXTERN void Cudd_SetTree	ARGS ((DdManager dd, MtrNode tree))
EXTERN unsigned int Cudd_NodeReadIndex	ARGS ((DdNode *node))
EXTERN void Cudd_SetEpsilon	ARGS ((DdManager *dd, CUDD_VALUE_TYPE ep))
EXTERN void Cudd_SetGroupcheck	ARGS ((DdManager *dd, Cudd_AggregationType gc))
EXTERN void Cudd_SetRecomb	ARGS ((DdManager *dd, int recomb))
EXTERN void Cudd_SetSymmviolation	ARGS ((DdManager *dd, int symmviolation))
EXTERN void Cudd_SetArcviolation	ARGS ((DdManager *dd, int arcviolation))
EXTERN void Cudd_SetPopulationSize	ARGS ((DdManager *dd, int populationSize))
EXTERN void Cudd_SetNumberXovers	ARGS ((DdManager *dd, int numberXovers))
EXTERN int Cudd_PrintInfo	ARGS ((DdManager dd, FILE fp))
EXTERN int Cudd_AddHook	ARGS ((DdManager dd, int(f)(DdManager , char , void *), Cudd_HookType where))
EXTERN int Cudd_StdPreReordHook	ARGS ((DdManager dd, char str, void *data))
EXTERN void Cudd_SetMaxLive	ARGS ((DdManager *dd, unsigned int maxLive))
EXTERN void Cudd_SetMaxMemory	ARGS ((DdManager *dd, long maxMemory))
EXTERN void Cudd_SetNextReordering	ARGS ((DdManager *dd, unsigned int next))
EXTERN DdNode *Cudd_addExistAbstract	ARGS ((DdManager manager, DdNode f, DdNode *cube))
EXTERN DdNode *Cudd_addApply	ARGS ((DdManager dd, DdNode ()(DdManager , DdNode , DdNode ), DdNode f, DdNode g))
EXTERN DdNode *Cudd_addPlus	ARGS ((DdManager dd, DdNode f, DdNode *g))
EXTERN DdNode *Cudd_addFindMax	ARGS ((DdManager dd, DdNode f))
EXTERN DdNode *Cudd_addIthBit	ARGS ((DdManager dd, DdNode f, int bit))
EXTERN DdNode *Cudd_addScalarInverse	ARGS ((DdManager dd, DdNode f, DdNode *epsilon))
EXTERN DdNode *Cudd_addIte	ARGS ((DdManager dd, DdNode f, DdNode g, DdNode h))
EXTERN DdNode *Cudd_addEvalConst	ARGS ((DdManager dd, DdNode f, DdNode *g))
EXTERN DdNode *Cudd_addRoundOff	ARGS ((DdManager dd, DdNode f, int N))
EXTERN DdNode *Cudd_addWalsh	ARGS ((DdManager dd, DdNode x, DdNode *y, int n))
EXTERN DdNode *Cudd_addResidue	ARGS ((DdManager *dd, int n, int m, int options, int top))
EXTERN DdNode *Cudd_bddAndAbstract	ARGS ((DdManager manager, DdNode f, DdNode g, DdNode cube))
EXTERN int Cudd_ApaNumberOfDigits	ARGS ((int binaryDigits))
EXTERN DdApaNumber Cudd_NewApaNumber	ARGS ((int digits))
EXTERN void Cudd_ApaCopy	ARGS ((int digits, DdApaNumber source, DdApaNumber dest))
EXTERN DdApaDigit Cudd_ApaAdd	ARGS ((int digits, DdApaNumber a, DdApaNumber b, DdApaNumber sum))
EXTERN DdApaDigit Cudd_ApaSubtract	ARGS ((int digits, DdApaNumber a, DdApaNumber b, DdApaNumber diff))
EXTERN DdApaDigit Cudd_ApaShortDivision	ARGS ((int digits, DdApaNumber dividend, DdApaDigit divisor, DdApaNumber quotient))
EXTERN unsigned int Cudd_ApaIntDivision	ARGS ((int digits, DdApaNumber dividend, unsigned int divisor, DdApaNumber quotient))
EXTERN void Cudd_ApaShiftRight	ARGS ((int digits, DdApaDigit in, DdApaNumber a, DdApaNumber b))
EXTERN void Cudd_ApaSetToLiteral	ARGS ((int digits, DdApaNumber number, DdApaDigit literal))
EXTERN void Cudd_ApaPowerOfTwo	ARGS ((int digits, DdApaNumber number, int power))
EXTERN int Cudd_ApaCompare	ARGS ((int digitsFirst, DdApaNumber first, int digitsSecond, DdApaNumber second))
EXTERN int Cudd_ApaCompareRatios	ARGS ((int digitsFirst, DdApaNumber firstNum, unsigned int firstDen, int digitsSecond, DdApaNumber secondNum, unsigned int secondDen))
EXTERN int Cudd_ApaPrintHex	ARGS ((FILE *fp, int digits, DdApaNumber number))
EXTERN int Cudd_ApaPrintExponential	ARGS ((FILE *fp, int digits, DdApaNumber number, int precision))
EXTERN DdApaNumber Cudd_ApaCountMinterm	ARGS ((DdManager manager, DdNode node, int nvars, int *digits))
EXTERN int Cudd_ApaPrintMinterm	ARGS ((FILE fp, DdManager dd, DdNode *node, int nvars))
EXTERN int Cudd_ApaPrintMintermExp	ARGS ((FILE fp, DdManager dd, DdNode *node, int nvars, int precision))
EXTERN int Cudd_ApaPrintDensity	ARGS ((FILE fp, DdManager dd, DdNode *node, int nvars))
EXTERN DdNode *Cudd_UnderApprox	ARGS ((DdManager dd, DdNode f, int numVars, int threshold, int safe, double quality))
EXTERN DdNode *Cudd_RemapUnderApprox	ARGS ((DdManager dd, DdNode f, int numVars, int threshold, double quality))
EXTERN DdNode *Cudd_BiasedUnderApprox	ARGS ((DdManager dd, DdNode f, DdNode *b, int numVars, int threshold, double quality1, double quality0))
EXTERN DdNode *Cudd_bddBooleanDiff	ARGS ((DdManager manager, DdNode f, int x))
EXTERN int Cudd_bddVarIsDependent	ARGS ((DdManager dd, DdNode f, DdNode *var))
EXTERN double Cudd_bddCorrelation	ARGS ((DdManager manager, DdNode f, DdNode *g))
EXTERN double Cudd_bddCorrelationWeights	ARGS ((DdManager manager, DdNode f, DdNode g, double prob))
EXTERN DdNode *Cudd_addBddThreshold	ARGS ((DdManager dd, DdNode f, CUDD_VALUE_TYPE value))
EXTERN DdNode *Cudd_addBddInterval	ARGS ((DdManager dd, DdNode f, CUDD_VALUE_TYPE lower, CUDD_VALUE_TYPE upper))
EXTERN DdNode *Cudd_BddToAdd	ARGS ((DdManager dd, DdNode B))
EXTERN DdNode *Cudd_bddTransfer	ARGS ((DdManager ddSource, DdManager ddDestination, DdNode *f))
EXTERN int Cudd_DebugCheck	ARGS ((DdManager *table))
EXTERN DdNode *Cudd_bddClippingAnd	ARGS ((DdManager dd, DdNode f, DdNode *g, int maxDepth, int direction))
EXTERN DdNode *Cudd_bddClippingAndAbstract	ARGS ((DdManager dd, DdNode f, DdNode g, DdNode cube, int maxDepth, int direction))
EXTERN DdNode *Cudd_bddCompose	ARGS ((DdManager dd, DdNode f, DdNode *g, int v))
EXTERN DdNode *Cudd_addPermute	ARGS ((DdManager manager, DdNode node, int *permut))
EXTERN DdNode *Cudd_addSwapVariables	ARGS ((DdManager dd, DdNode f, DdNode x, DdNode y, int n))
EXTERN DdNode *Cudd_bddVarMap	ARGS ((DdManager manager, DdNode f))
EXTERN int Cudd_SetVarMap	ARGS ((DdManager manager, DdNode x, DdNode *y, int n))
EXTERN DdNode *Cudd_bddAdjPermuteX	ARGS ((DdManager dd, DdNode B, DdNode **x, int n))
EXTERN DdNode *Cudd_addVectorCompose	ARGS ((DdManager dd, DdNode f, DdNode **vector))
EXTERN int Cudd_bddApproxConjDecomp	ARGS ((DdManager dd, DdNode f, DdNode ***conjuncts))
EXTERN int Cudd_bddApproxDisjDecomp	ARGS ((DdManager dd, DdNode f, DdNode ***disjuncts))
EXTERN int Cudd_bddIsVarEssential	ARGS ((DdManager manager, DdNode f, int id, int phase))
EXTERN int Cudd_DumpBlif	ARGS ((DdManager dd, int n, DdNode f, char inames, char onames, char mname, FILE *fp))
EXTERN int Cudd_DumpBlifBody	ARGS ((DdManager dd, int n, DdNode f, char inames, char onames, FILE fp))
EXTERN DdNode *Cudd_bddConstrain	ARGS ((DdManager dd, DdNode f, DdNode *c))
EXTERN DdNode *Cudd_bddSqueeze	ARGS ((DdManager dd, DdNode l, DdNode *u))
EXTERN DdNode *Cudd_SubsetCompress	ARGS ((DdManager dd, DdNode f, int nvars, int threshold))
EXTERN MtrNode *Cudd_MakeTreeNode	ARGS ((DdManager *dd, unsigned int low, unsigned int size, unsigned int type))
EXTERN int Cudd_addHarwell	ARGS ((FILE fp, DdManager dd, DdNode E, DdNode x, DdNode y, DdNode xn, DdNode *yn_, int nx, int ny, int m, int *n, int bx, int sx, int by, int sy, int pr))
EXTERN DdManager *Cudd_Init	ARGS ((unsigned int numVars, unsigned int numVarsZ, unsigned int numSlots, unsigned int cacheSize, unsigned long maxMemory))
EXTERN int Cudd_ReadLinear	ARGS ((DdManager *table, int x, int y))
EXTERN DdNode *Cudd_addMatrixMultiply	ARGS ((DdManager dd, DdNode A, DdNode B, DdNode *z, int nz))
EXTERN DdNode *Cudd_addTriangle	ARGS ((DdManager dd, DdNode f, DdNode g, DdNode *z, int nz))
EXTERN DdNode *Cudd_PrioritySelect	ARGS ((DdManager dd, DdNode R, DdNode x, DdNode y, DdNode *z, DdNode Pi, int n, DdNode ()(DdManager , int, DdNode , DdNode , DdNode *)))
EXTERN DdNode *Cudd_Xgty	ARGS ((DdManager dd, int N, DdNode z, DdNode x, DdNode *y))
EXTERN DdNode *Cudd_Xeqy	ARGS ((DdManager dd, int N, DdNode x, DdNode *y))
EXTERN DdNode *Cudd_Dxygtdxz	ARGS ((DdManager dd, int N, DdNode x, DdNode y, DdNode *z))
EXTERN DdNode *Cudd_CProjection	ARGS ((DdManager dd, DdNode R, DdNode *Y))
EXTERN DdNode *Cudd_addHamming	ARGS ((DdManager dd, DdNode xVars, DdNode *yVars, int nVars))
EXTERN int Cudd_MinHammingDist	ARGS ((DdManager dd, DdNode f, int *minterm, int upperBound))
EXTERN int Cudd_addRead	ARGS ((FILE fp, DdManager dd, DdNode E, DdNode x, DdNode y, DdNode xn, DdNode *yn_, int nx, int ny, int m, int *n, int bx, int sx, int by, int sy))
EXTERN int Cudd_bddRead	ARGS ((FILE fp, DdManager dd, DdNode E, DdNode x, DdNode *y, int nx, int ny, int m, int *n, int bx, int sx, int by, int sy))
EXTERN void Cudd_Ref	ARGS ((DdNode *n))
EXTERN void Cudd_RecursiveDeref	ARGS ((DdManager table, DdNode n))
EXTERN int Cudd_CheckZeroRef	ARGS ((DdManager *manager))
EXTERN int Cudd_ReduceHeap	ARGS ((DdManager *table, Cudd_ReorderingType heuristic, int minsize))
EXTERN int Cudd_ShuffleHeap	ARGS ((DdManager table, int permutation))
EXTERN DdNode *Cudd_Eval	ARGS ((DdManager dd, DdNode f, int *inputs))
EXTERN DdNode *Cudd_ShortestPath	ARGS ((DdManager manager, DdNode f, int weight, int support, int *length))
EXTERN DdNode *Cudd_LargestCube	ARGS ((DdManager manager, DdNode f, int *length))
EXTERN int Cudd_ShortestLength	ARGS ((DdManager manager, DdNode f, int *weight))
EXTERN DdNode *Cudd_Decreasing	ARGS ((DdManager dd, DdNode f, int i))
EXTERN int Cudd_EquivDC	ARGS ((DdManager dd, DdNode F, DdNode G, DdNode D))
EXTERN int Cudd_EqualSupNorm	ARGS ((DdManager dd, DdNode f, DdNode *g, CUDD_VALUE_TYPE tolerance, int pr))
EXTERN double *Cudd_CofMinterm	ARGS ((DdManager dd, DdNode node))
EXTERN DdNode *Cudd_SolveEqn	ARGS ((DdManager bdd, DdNode F, DdNode Y, DdNode G, int *yIndex, int n))
EXTERN DdNode *Cudd_VerifySol	ARGS ((DdManager bdd, DdNode F, DdNode *G, int yIndex, int n))
EXTERN DdNode *Cudd_SplitSet	ARGS ((DdManager manager, DdNode S, DdNode **xVars, int n, double m))
EXTERN DdNode *Cudd_SubsetHeavyBranch	ARGS ((DdManager dd, DdNode f, int numVars, int threshold))
EXTERN DdNode *Cudd_SubsetShortPaths	ARGS ((DdManager dd, DdNode f, int numVars, int threshold, int hardlimit))
EXTERN void Cudd_SymmProfile	ARGS ((DdManager *table, int lower, int upper))
EXTERN unsigned int Cudd_Prime	ARGS ((unsigned int p))
EXTERN int Cudd_PrintMinterm	ARGS ((DdManager manager, DdNode node))
EXTERN int Cudd_PrintDebug	ARGS ((DdManager dd, DdNode f, int n, int pr))
EXTERN int Cudd_EstimateCofactor	ARGS ((DdManager dd, DdNode node, int i, int phase))
EXTERN int Cudd_EstimateCofactorSimple	ARGS ((DdNode *node, int i))
EXTERN int Cudd_SharingSize	ARGS ((DdNode **nodeArray, int n))
EXTERN double Cudd_CountMinterm	ARGS ((DdManager manager, DdNode node, int nvars))
EXTERN DdNode *Cudd_VectorSupport	ARGS ((DdManager dd, DdNode *F, int n))
EXTERN int Cudd_ClassifySupport	ARGS ((DdManager dd, DdNode f, DdNode g, DdNode common, DdNode onlyF, DdNode *onlyG))
EXTERN int Cudd_bddPickOneCube	ARGS ((DdManager ddm, DdNode node, char *string))
EXTERN DdNode *Cudd_bddPickOneMinterm	ARGS ((DdManager dd, DdNode f, DdNode **vars, int n))
EXTERN DdNode **Cudd_bddPickArbitraryMinterms	ARGS ((DdManager dd, DdNode f, DdNode **vars, int n, int k))
EXTERN DdGen *Cudd_FirstCube	ARGS ((DdManager dd, DdNode f, int *cube, CUDD_VALUE_TYPE value))
EXTERN int Cudd_NextCube	ARGS ((DdGen gen, int cube, CUDD_VALUE_TYPE value))
EXTERN DdNode *Cudd_bddComputeCube	ARGS ((DdManager dd, DdNode vars, int phase, int n))
EXTERN DdGen *Cudd_FirstNode	ARGS ((DdManager dd, DdNode f, DdNode **node))
EXTERN int Cudd_NextNode	ARGS ((DdGen gen, DdNode *node))
EXTERN int Cudd_GenFree	ARGS ((DdGen *gen))
EXTERN DdNode *Cudd_IndicesToCube	ARGS ((DdManager dd, int array, int n))
EXTERN void Cudd_PrintVersion	ARGS ((FILE *fp))
EXTERN long Cudd_Random	ARGS (())
EXTERN void Cudd_Srandom	ARGS ((long seed))
EXTERN double Cudd_Density	ARGS ((DdManager dd, DdNode f, int nvars))
EXTERN void Cudd_OutOfMem	ARGS ((long size))
EXTERN int Cudd_zddCount	ARGS ((DdManager zdd, DdNode P))
EXTERN DdNode *Cudd_zddIsop	ARGS ((DdManager dd, DdNode L, DdNode U, DdNode *zdd_I))
EXTERN DdNode *Cudd_bddIsop	ARGS ((DdManager dd, DdNode L, DdNode *U))
EXTERN int Cudd_zddDagSize	ARGS ((DdNode *p_node))
EXTERN double Cudd_zddCountMinterm	ARGS ((DdManager zdd, DdNode node, int path))
EXTERN DdNode *Cudd_zddUnion	ARGS ((DdManager dd, DdNode P, DdNode *Q))
EXTERN DdNode *Cudd_zddDiffConst	ARGS ((DdManager zdd, DdNode P, DdNode *Q))
EXTERN DdNode *Cudd_zddSubset1	ARGS ((DdManager dd, DdNode P, int var))
EXTERN int Cudd_zddPrintMinterm	ARGS ((DdManager zdd, DdNode node))
EXTERN int Cudd_zddPrintDebug	ARGS ((DdManager zdd, DdNode f, int n, int pr))