src/bdd/cudd/cudd.h File Reference

#include "mtr.h"
#include "epd.h"

Include dependency graph for cudd.h:

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

Data Structures
struct	DdChildren
struct	DdNode
Defines
#define	CUDD_VERSION "2.3.1"
#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	CUDD_CONST_INDEX CUDD_MAXINDEX
#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_CONST_INDEX)
#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	Cudd_zddForeachPath(manager, f, gen, path)
#define	EXTERN extern
#define	ARGS(protos) ()
Typedefs
typedef unsigned short	DdHalfWord
typedef struct DdNode	DdNode
typedef struct DdManager	DdManager
typedef struct 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_LAZY_SIFT, 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 }
enum	Cudd_LazyGroupType { CUDD_LAZY_NONE, CUDD_LAZY_SOFT_GROUP, CUDD_LAZY_HARD_GROUP, CUDD_LAZY_UNGROUP }
enum	Cudd_VariableType { CUDD_VAR_PRIMARY_INPUT, CUDD_VAR_PRESENT_STATE, CUDD_VAR_NEXT_STATE }
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_SetReorderingCycle	ARGS ((DdManager *dd, int cycle))
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_SetNextReordering	ARGS ((DdManager *dd, unsigned int next))
EXTERN void Cudd_SetMaxLive	ARGS ((DdManager *dd, unsigned int maxLive))
EXTERN void Cudd_SetMaxMemory	ARGS ((DdManager *dd, long maxMemory))
EXTERN int Cudd_bddBindVar	ARGS ((DdManager *dd, int index))
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_addMonadicApply	ARGS ((DdManager dd, DdNode (op)(DdManager , DdNode ), DdNode f))
EXTERN DdNode *Cudd_addLog	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 ((intdigits, DdApaNumber dividend, unsigned intdivisor, DdApaNumberquotient))
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, DdApaNumberfirst, int digitsSecond, DdApaNumbersecond))
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, intdigits, DdApaNumbernumber, 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, intnvars, int precision))
EXTERN int Cudd_ApaPrintDensity	ARGS ((FILE fp, DdManager dd, DdNode *node, intnvars))
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 DdNode *Cudd_addGeneralVectorCompose	ARGS ((DdManager dd, DdNode f, DdNode vectorOn, DdNode vectorOff))
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_addOuterSum	ARGS ((DdManager dd, DdNode M, DdNode r, DdNode c))
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 DdNode *Cudd_bddClosestCube	ARGS ((DdManager dd, DdNode f, DdNode g, int distance))
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_bddLeqUnless	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 DdNode *Cudd_bddMakePrime	ARGS ((DdManager dd, DdNode cube, DdNode *f))
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 int Cudd_EpdCountMinterm	ARGS ((DdManager manager, DdNode node, int nvars, EpDouble *epd))
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 DdNode *Cudd_SubsetWithMaskVars	ARGS ((DdManager dd, DdNode f, DdNode vars, int nvars, DdNode maskVars, int mvars))
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 DdNode *Cudd_CubeArrayToBdd	ARGS ((DdManager dd, int array))
EXTERN int Cudd_BddToCubeArray	ARGS ((DdManager dd, DdNode cube, int *array))
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))
EXTERN DdGen *Cudd_zddFirstPath	ARGS ((DdManager zdd, DdNode f, int **path))
EXTERN int Cudd_zddNextPath	ARGS ((DdGen gen, int *path))
EXTERN char *Cudd_zddCoverPathToString	ARGS ((DdManager zdd, int path, char *str))
EXTERN int Cudd_bddSetPairIndex	ARGS ((DdManager *dd, int index, int pairIndex))

Define Documentation

#define ARGS ( protos ) ()

Definition at line 542 of file cudd.h.

#define CUDD_CACHE_SLOTS 262144

Definition at line 67 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 348 of file cudd.h.

#define CUDD_CONST_INDEX CUDD_MAXINDEX

Definition at line 86 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 392 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 456 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 490 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 362 of file cudd.h.

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

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_CONST_INDEX). The pointer passed to Cudd_IsConstant may be either regular or complemented.]

SideEffects [none]

SeeAlso []

Definition at line 289 of file cudd.h.

#define CUDD_MAXINDEX ((DdHalfWord) ~0)

Definition at line 81 of file cudd.h.

#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 304 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 320 of file cudd.h.

#define CUDD_OUT_OF_MEM -1

Definition at line 64 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 424 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 334 of file cudd.h.

#define CUDD_RESIDUE_DEFAULT 0

Definition at line 70 of file cudd.h.

#define CUDD_RESIDUE_MSB 1

Definition at line 71 of file cudd.h.

#define CUDD_RESIDUE_TC 2

Definition at line 72 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 377 of file cudd.h.

#define CUDD_UNIQUE_SLOTS 256

Definition at line 66 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 407 of file cudd.h.

#define CUDD_VALUE_TYPE double

Definition at line 63 of file cudd.h.

#define CUDD_VERSION "2.3.1"

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.1.1 2003/02/24 22:23:50 wjiang Exp

]

Definition at line 44 of file cudd.h.

#define Cudd_zddForeachPath	(	manager,
		f,
		gen,
		path	)

Value:

for((gen) = Cudd_zddFirstPath(manager, f, &path);\
        Cudd_IsGenEmpty(gen) ? Cudd_GenFree(gen) : TRUE;\
        (void) Cudd_zddNextPath(gen, &path))

Macro***********************************************************************

Synopsis [Iterates over the paths of a ZDD.]

Description [Iterates over the paths of a ZDD f.

DdManager *manager;
DdNode *f;
DdGen *gen;
int *path;

Cudd_zddForeachPath allocates and frees the generator. Therefore the application should not try to do that. Also, the path is freed at the end of Cudd_zddForeachPath 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_zddFirstPath Cudd_zddNextPath Cudd_GenFree Cudd_IsGenEmpty Cudd_AutodynDisable]

Definition at line 524 of file cudd.h.

#define DD_APA_BASE (1 << DD_APA_BITS)

Definition at line 94 of file cudd.h.

#define DD_APA_BITS 16

Definition at line 93 of file cudd.h.

#define DD_APA_HEXPRINT "%04x"

Definition at line 96 of file cudd.h.

#define DD_APA_MASK (DD_APA_BASE - 1)

Definition at line 95 of file cudd.h.

#define EXTERN extern

Definition at line 535 of file cudd.h.

#define FALSE 0

Definition at line 60 of file cudd.h.

#define SIZEOF_INT 4

Definition at line 50 of file cudd.h.

#define SIZEOF_LONG 4

Definition at line 53 of file cudd.h.

#define SIZEOF_VOID_P 4

Definition at line 47 of file cudd.h.

#define TRUE 1

Definition at line 57 of file cudd.h.

Typedef Documentation

typedef unsigned short int DdApaDigit

Definition at line 261 of file cudd.h.

typedef unsigned long int DdApaDoubleDigit

Definition at line 262 of file cudd.h.

typedef DdApaDigit* DdApaNumber

Definition at line 263 of file cudd.h.

typedef struct DdGen DdGen

Definition at line 257 of file cudd.h.

typedef unsigned short DdHalfWord

Definition at line 225 of file cudd.h.

typedef struct DdManager DdManager

Definition at line 255 of file cudd.h.

typedef struct DdNode DdNode

Definition at line 233 of file cudd.h.

Enumeration Type Documentation

enum Cudd_AggregationType

Enum************************************************************************

Synopsis [Type of aggregation methods.]

Description [Type of aggregation methods.]

Enumerator:

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 147 of file cudd.h.

00147              {
00148     CUDD_NO_CHECK,
00149     CUDD_GROUP_CHECK,
00150     CUDD_GROUP_CHECK2,
00151     CUDD_GROUP_CHECK3,
00152     CUDD_GROUP_CHECK4,
00153     CUDD_GROUP_CHECK5,
00154     CUDD_GROUP_CHECK6,
00155     CUDD_GROUP_CHECK7,
00156     CUDD_GROUP_CHECK8,
00157     CUDD_GROUP_CHECK9
00158 } Cudd_AggregationType;

enum Cudd_ErrorType

Enum************************************************************************

Synopsis [Type of error codes.]

Description [Type of error codes.]

Enumerator:

CUDD_NO_ERROR
CUDD_MEMORY_OUT
CUDD_TOO_MANY_NODES
CUDD_MAX_MEM_EXCEEDED
CUDD_INVALID_ARG
CUDD_INTERNAL_ERROR

Definition at line 183 of file cudd.h.

00183              {
00184     CUDD_NO_ERROR,
00185     CUDD_MEMORY_OUT,
00186     CUDD_TOO_MANY_NODES,
00187     CUDD_MAX_MEM_EXCEEDED,
00188     CUDD_INVALID_ARG,
00189     CUDD_INTERNAL_ERROR
00190 } Cudd_ErrorType;

enum Cudd_HookType

Enum************************************************************************

Synopsis [Type of hooks.]

Description [Type of hooks.]

Enumerator:

CUDD_PRE_GC_HOOK
CUDD_POST_GC_HOOK
CUDD_PRE_REORDERING_HOOK
CUDD_POST_REORDERING_HOOK

Definition at line 168 of file cudd.h.

00168              {
00169     CUDD_PRE_GC_HOOK,
00170     CUDD_POST_GC_HOOK,
00171     CUDD_PRE_REORDERING_HOOK,
00172     CUDD_POST_REORDERING_HOOK
00173 } Cudd_HookType;

enum Cudd_LazyGroupType

Enum************************************************************************

Synopsis [Group type for lazy sifting.]

Description [Group type for lazy sifting.]

Enumerator:

CUDD_LAZY_NONE
CUDD_LAZY_SOFT_GROUP
CUDD_LAZY_HARD_GROUP
CUDD_LAZY_UNGROUP

Definition at line 200 of file cudd.h.

00200              {
00201     CUDD_LAZY_NONE,
00202     CUDD_LAZY_SOFT_GROUP,
00203     CUDD_LAZY_HARD_GROUP,
00204     CUDD_LAZY_UNGROUP
00205 } Cudd_LazyGroupType;

enum Cudd_ReorderingType

Enum************************************************************************

Synopsis [Type of reordering algorithm.]

Description [Type of reordering algorithm.]

Enumerator:

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_LAZY_SIFT
CUDD_REORDER_EXACT

Definition at line 114 of file cudd.h.

00115 00116 00117 00118 00119 00120 00121 00122 00123 00124 00125 00126 00127 00128 00129 00130 00131 00132 00133 00134 00135 00136 00137

class="fragment">00114 { 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_LAZY_SIFT, CUDD_REORDER_EXACT } Cudd_ReorderingType;

enum Cudd_VariableType

Enum************************************************************************

Synopsis [Variable type.]

Description [Variable type. Currently used only in lazy sifting.]

Enumerator:

CUDD_VAR_PRIMARY_INPUT
CUDD_VAR_PRESENT_STATE
CUDD_VAR_NEXT_STATE

Definition at line 215 of file cudd.h.

00215              {
00216     CUDD_VAR_PRIMARY_INPUT,
00217     CUDD_VAR_PRESENT_STATE,
00218     CUDD_VAR_NEXT_STATE
00219 } Cudd_VariableType;

Function Documentation

EXTERN int Cudd_bddSetPairIndex ARGS ( (DdManager *dd, int index, int pairIndex) )

EXTERN char* Cudd_zddCoverPathToString ARGS ( (DdManager *zdd, int *path, char *str) )

EXTERN int Cudd_zddNextPath ARGS ( (DdGen *gen, int **path) )

EXTERN DdGen* Cudd_zddFirstPath ARGS ( (DdManager *zdd, DdNode *f, int **path) )

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 ( () )

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 int Cudd_BddToCubeArray ARGS ( (DdManager *dd, DdNode *cube, int *array) )

EXTERN DdNode* Cudd_CubeArrayToBdd ARGS ( (DdManager *dd, int *array) )

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_SubsetWithMaskVars ARGS ( (DdManager *dd, DdNode *f, DdNode **vars, int nvars, DdNode **maskVars, int mvars) )

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

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

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

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

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

EXTERN int Cudd_EpdCountMinterm ARGS ( (DdManager *manager, DdNode *node, int nvars, EpDouble *epd) )

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

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

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

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

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

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

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

EXTERN int cuddZddSymmSiftingConv ARGS ( (DdManager *table, int lower, int upper) )

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

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

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

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

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

EXTERN DdNode *cuddMakeBddFromZddCover ARGS ( (DdManager *dd, DdNode *node) )

EXTERN DdNode* Cudd_bddMakePrime ARGS ( (DdManager *dd, DdNode *cube, DdNode *f) )

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

EXTERN int Cudd_bddLeqUnless ARGS ( (DdManager *dd, DdNode *f, DdNode *g, DdNode *D) )

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

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

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

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

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

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

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

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

EXTERN void cuddLocalCacheClearAll ARGS ( (DdManager *manager) )

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

static int ddLeavesInt ARGS ( (DdNode *n) )

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 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 DdNode* Cudd_bddClosestCube ARGS ( (DdManager *dd, DdNode *f, DdNode *g, int *distance) )

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

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

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

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

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

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

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_addOuterSum ARGS ( (DdManager *dd, DdNode *M, DdNode *r, DdNode *c) )

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

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

static void cuddXorLinear ARGS ( (DdManager *table, int x, int y) )

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

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 MtrNode *Cudd_MakeZddTreeNode ARGS ( (DdManager *dd, unsigned int low, unsigned int size, unsigned int type) )

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

EXTERN int Cudd_bddPrintCover ARGS ( (DdManager *dd, DdNode *l, DdNode *u) )

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

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

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

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

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

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

EXTERN DdNode* Cudd_addGeneralVectorCompose ARGS ( (DdManager *dd, DdNode *f, DdNode **vectorOn, DdNode **vectorOff) )

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

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

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

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

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

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

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

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

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

static int zddReorderPostprocess ARGS ( (DdManager *table) )

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

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

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

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

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

EXTERN DdNode *cuddBddXorRecur ARGS ( (DdManager *manager, DdNode *f, DdNode *g) )

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

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

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

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

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

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

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

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

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

EXTERN int Cudd_ApaPrintExponential ARGS ( (FILE *fp, intdigits, DdApaNumbernumber, int precision) )

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

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

EXTERN int Cudd_ApaCompare ARGS ( (int digitsFirst, DdApaNumberfirst, int digitsSecond, DdApaNumbersecond) )

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

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

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

EXTERN unsigned int Cudd_ApaIntDivision ARGS ( (intdigits, DdApaNumber dividend, unsigned intdivisor, DdApaNumberquotient) )

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

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

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

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

EXTERN DdApaNumber Cudd_NewApaNumber ARGS ( (int digits) )

EXTERN int Cudd_ApaNumberOfDigits ARGS ( (int binaryDigits) )

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

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

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

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

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

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

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

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

EXTERN int cuddP ARGS ( (DdManager *dd, DdNode *f) )

EXTERN DdNode* Cudd_addMonadicApply ARGS ( (DdManager *dd, DdNode *(*op)(DdManager *, DdNode *), DdNode *f) )

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

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

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

static int ddIsVarHandled ARGS ( (DdManager *dd, int index) )

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

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

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

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

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

EXTERN void Cudd_SetStderr ARGS ( (DdManager *dd, FILE *fp) )

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

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

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

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

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

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

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

EXTERN int Cudd_CountLeaves ARGS ( (DdNode *node) )

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

EXTERN void Cudd_SetReorderingCycle ARGS ( (DdManager *dd, int cycle) )

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

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

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

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

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

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

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

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

EXTERN void cuddSlowTableGrowth ARGS ( (DdManager *unique) )

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

EXTERN int Cudd_IsNonConstant ARGS ( (DdNode *f) )

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

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

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

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

EXTERN double Cudd_AverageDistance ARGS ( (DdManager *dd) )

AutomaticStart

src/bdd/cudd/cudd.h File Reference

Data Structures

Defines

Typedefs

Enumerations

Functions

Define Documentation

Typedef Documentation

Enumeration Type Documentation

Function Documentation