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

cuddInt.h File Reference

#include <math.h>
#include "cudd.h"

Include dependency graph for cuddInt.h:

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

Go to the source code of this file.

Compounds

struct DdCache

struct DdHashItem

struct DdHashTable

struct DdHook

struct DdLevelQueue

struct DdLocalCache

struct DdLocalCacheItem

struct DdManager

struct DdQueueItem

struct DdSubtable

struct Move

Defines

#define DD_INLINE

#define DD_UNUSED

#define DD_MAXREF   ((DdHalfWord) ~0)

#define DD_DEFAULT_RESIZE   10

#define DD_MEM_CHUNK   1022

#define DD_ONE_VAL   (1.0)

#define DD_ZERO_VAL   (0.0)

#define DD_EPSILON   (1.0e-12)

#define DD_PLUS_INF_VAL   (10e301)

#define DD_CRI_HI_MARK   (10e150)

#define DD_CRI_LO_MARK   (-(DD_CRI_HI_MARK))

#define DD_MINUS_INF_VAL   (-(DD_PLUS_INF_VAL))

#define DD_NON_CONSTANT   ((DdNode *) 1)

#define DD_MAX_SUBTABLE_DENSITY   4

#define DD_GC_FRAC_LO   DD_MAX_SUBTABLE_DENSITY * 0.25

#define DD_GC_FRAC_HI   DD_MAX_SUBTABLE_DENSITY * 1.0

#define DD_GC_FRAC_MIN   0.2

#define DD_MIN_HIT   30

#define DD_MAX_LOOSE_FRACTION   5

#define DD_MAX_CACHE_FRACTION   3

#define DD_STASH_FRACTION   64

#define DD_MAX_CACHE_TO_SLOTS_RATIO   4

#define DD_SIFT_MAX_VAR   1000

#define DD_SIFT_MAX_SWAPS   2000000

#define DD_DEFAULT_RECOMB   0

#define DD_MAX_REORDER_GROWTH   1.2

#define DD_FIRST_REORDER   4004

#define DD_DYN_RATIO   2

#define DD_P1   12582917

#define DD_P2   4256249

#define DD_P3   741457

#define DD_P4   1618033999

#define DD_ADD_ITE_TAG   0x02

#define DD_BDD_AND_ABSTRACT_TAG   0x06

#define DD_BDD_XOR_EXIST_ABSTRACT_TAG   0x0a

#define DD_BDD_ITE_TAG   0x0e

#define DD_ADD_BDD_DO_INTERVAL_TAG   0x22

#define DD_BDD_CLIPPING_AND_ABSTRACT_UP_TAG   0x26

#define DD_BDD_CLIPPING_AND_ABSTRACT_DOWN_TAG   0x2a

#define DD_BDD_COMPOSE_RECUR_TAG   0x2e

#define DD_ADD_COMPOSE_RECUR_TAG   0x42

#define DD_ADD_NON_SIM_COMPOSE_TAG   0x46

#define DD_EQUIV_DC_TAG   0x4a

#define DD_ZDD_ITE_TAG   0x4e

#define DD_ADD_ITE_CONSTANT_TAG   0x62

#define DD_ADD_EVAL_CONST_TAG   0x66

#define DD_BDD_ITE_CONSTANT_TAG   0x6a

#define cuddDeallocNode(unique, node)

#define cuddRef(n)   cuddSatInc(Cudd_Regular(n)->ref)

#define cuddDeref(n)   cuddSatDec(Cudd_Regular(n)->ref)

#define cuddIsConstant(node)   ((node)->index == CUDD_MAXINDEX)

#define cuddT(node)   ((node)->type.kids.T)

#define cuddE(node)   ((node)->type.kids.E)

#define cuddV(node)   ((node)->type.value)

#define cuddI(dd, index)   (((index)==CUDD_MAXINDEX)?(int)(index):(dd)->perm[(index)])

#define cuddIZ(dd, index)   (((index)==CUDD_MAXINDEX)?(int)(index):(dd)->permZ[(index)])

#define ddHash(f, g, s)   ((((unsigned)(f) * DD_P1 + (unsigned)(g)) * DD_P2) >> (s))

#define ddCHash(o, f, g, h, s)

#define ddCHash2(o, f, g, s)   (((((unsigned)(f) + (unsigned)(o)) * DD_P1 + (unsigned)(g)) * DD_P2) >> (s))

#define cuddClean(p)   ((DdNode *)((ptruint)(p) & ~0xf))

#define ddMin(x, y)   (((y) < (x)) ? (y) : (x))

#define ddMax(x, y)   (((y) > (x)) ? (y) : (x))

#define ddAbs(x)   (((x)<0) ? -(x) : (x))

#define ddEqualVal(x, y, e)   (ddAbs((x)-(y))<(e))

#define cuddSatInc(x)   ((x) += (x) != (DdHalfWord)DD_MAXREF)

#define cuddSatDec(x)   ((x) -= (x) != (DdHalfWord)DD_MAXREF)

#define DD_ONE(dd)   ((dd)->one)

#define DD_ZERO(dd)   ((dd)->zero)

#define DD_PLUS_INFINITY(dd)   ((dd)->plusinfinity)

#define DD_MINUS_INFINITY(dd)   ((dd)->minusinfinity)

#define cuddAdjust(x)   ((x) = ((x) >= DD_CRI_HI_MARK) ? DD_PLUS_INF_VAL : (((x) <= DD_CRI_LO_MARK) ? DD_MINUS_INF_VAL : (x)))

#define DD_LSDIGIT(x)   ((x) & DD_APA_MASK)

#define DD_MSDIGIT(x)   ((x) >> DD_APA_BITS)

#define statLine(dd)

Typedefs

typedef DdHook DdHook

typedef int ptrint

typedef unsigned int ptruint

typedef DdNode * DdNodePtr

typedef DdLocalCacheItem DdLocalCacheItem

typedef DdLocalCache DdLocalCache

typedef DdHashItem DdHashItem

typedef DdHashTable DdHashTable

typedef DdCache DdCache

typedef DdSubtable DdSubtable

typedef Move Move

typedef DdQueueItem DdQueueItem

typedef DdLevelQueue DdLevelQueue

Functions

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

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

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

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

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

EXTERN DdNode *cuddAddRoundOffRecur ARGS ((DdManager *dd, DdNode *f, double trunc))

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

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

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

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

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

EXTERN DdNode *cuddBddBooleanDiffRecur ARGS ((DdManager *manager, DdNode *f, DdNode *var))

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

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

EXTERN DdNode *cuddBddTransfer ARGS ((DdManager *ddS, DdManager *ddD, DdNode *f))

EXTERN int cuddInitCache ARGS ((DdManager *unique, unsigned int cacheSize, unsigned int maxCacheSize))

EXTERN void cuddCacheInsert ARGS ((DdManager *table, ptruint op, DdNode *f, DdNode *g, DdNode *h, DdNode *data))

EXTERN void cuddCacheInsert2 ARGS ((DdManager *table, DdNode *(*)(DdManager *, DdNode *, DdNode *), DdNode *f, DdNode *g, DdNode *data))

EXTERN void cuddCacheInsert1 ARGS ((DdManager *table, DdNode *(*)(DdManager *, DdNode *), DdNode *f, DdNode *data))

EXTERN DdNode *cuddCacheLookup ARGS ((DdManager *table, ptruint op, DdNode *f, DdNode *g, DdNode *h))

EXTERN DdNode *cuddCacheLookup2 ARGS ((DdManager *table, DdNode *(*)(DdManager *, DdNode *, DdNode *), DdNode *f, DdNode *g))

EXTERN DdNode *cuddCacheLookup1 ARGS ((DdManager *table, DdNode *(*)(DdManager *, DdNode *), DdNode *f))

EXTERN int cuddCacheProfile ARGS ((DdManager *table, FILE *fp))

EXTERN void cuddCacheResize ARGS ((DdManager *table))

EXTERN int cuddComputeFloorLog2 ARGS ((unsigned int value))

EXTERN int cuddHeapProfile ARGS ((DdManager *dd))

EXTERN void cuddPrintNode ARGS ((DdNode *f, FILE *fp))

EXTERN void cuddPrintVarGroups ARGS ((DdManager *dd, MtrNode *root, int zdd, int silent))

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

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

EXTERN void cuddGetBranches ARGS ((DdNode *g, DdNode **g1, DdNode **g0))

EXTERN int cuddCheckCube ARGS ((DdManager *dd, DdNode *g))

EXTERN DdNode *cuddBddComposeRecur ARGS ((DdManager *dd, DdNode *f, DdNode *g, DdNode *proj))

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

EXTERN int cuddTreeSifting ARGS ((DdManager *table, Cudd_ReorderingType method))

EXTERN int cuddZddInitUniv ARGS ((DdManager *zdd))

EXTERN void cuddSetInteract ARGS ((DdManager *table, int x, int y))

EXTERN DdLocalCache *cuddLocalCacheInit ARGS ((DdManager *manager, unsigned int keySize, unsigned int cacheSize, unsigned int maxCacheSize))

EXTERN void cuddLocalCacheQuit ARGS ((DdLocalCache *cache))

EXTERN void cuddLocalCacheInsert ARGS ((DdLocalCache *cache, DdNodePtr *key, DdNode *value))

EXTERN DdNode *cuddLocalCacheLookup ARGS ((DdLocalCache *cache, DdNodePtr *key))

EXTERN void cuddLocalCacheClearDead ARGS ((DdManager *manager))

EXTERN DdHashTable *cuddHashTableInit ARGS ((DdManager *manager, unsigned int keySize, unsigned int initSize))

EXTERN void cuddHashTableQuit ARGS ((DdHashTable *hash))

EXTERN int cuddHashTableInsert ARGS ((DdHashTable *hash, DdNodePtr *key, DdNode *value, ptrint count))

EXTERN DdNode *cuddHashTableLookup ARGS ((DdHashTable *hash, DdNodePtr *key))

EXTERN int cuddHashTableInsert1 ARGS ((DdHashTable *hash, DdNode *f, DdNode *value, ptrint count))

EXTERN DdNode *cuddHashTableLookup1 ARGS ((DdHashTable *hash, DdNode *f))

EXTERN int cuddHashTableInsert2 ARGS ((DdHashTable *hash, DdNode *f, DdNode *g, DdNode *value, ptrint count))

EXTERN DdNode *cuddHashTableLookup2 ARGS ((DdHashTable *hash, DdNode *f, DdNode *g))

EXTERN int cuddHashTableInsert3 ARGS ((DdHashTable *hash, DdNode *f, DdNode *g, DdNode *h, DdNode *value, ptrint count))

EXTERN DdNode *cuddHashTableLookup3 ARGS ((DdHashTable *hash, DdNode *f, DdNode *g, DdNode *h))

EXTERN DdLevelQueue *cuddLevelQueueInit ARGS ((int levels, int itemSize, int numBuckets))

EXTERN void cuddLevelQueueQuit ARGS ((DdLevelQueue *queue))

EXTERN void *cuddLevelQueueEnqueue ARGS ((DdLevelQueue *queue, void *key, int level))

EXTERN void cuddLevelQueueDequeue ARGS ((DdLevelQueue *queue, int level))

EXTERN DdNode *cuddCProjectionRecur ARGS ((DdManager *dd, DdNode *R, DdNode *Y, DdNode *Ysupp))

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

EXTERN int cuddSwapping ARGS ((DdManager *table, int lower, int upper, Cudd_ReorderingType heuristic))

EXTERN int cuddNextHigh ARGS ((DdManager *table, int x))

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

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

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

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

EXTERN DdNode *cuddAllocNode ARGS ((DdManager *unique))

EXTERN DdManager *cuddInitTable ARGS ((unsigned int numVars, unsigned int numVarsZ, unsigned int numSlots, unsigned int looseUpTo))

EXTERN int cuddGarbageCollect ARGS ((DdManager *unique, int clearCache))

EXTERN DdNode *cuddZddGetNode ARGS ((DdManager *zdd, int id, DdNode *T, DdNode *E))

EXTERN DdNode *cuddZddGetNodeIVO ARGS ((DdManager *dd, int index, DdNode *g, DdNode *h))

EXTERN DdNode *cuddUniqueInter ARGS ((DdManager *unique, int index, DdNode *T, DdNode *E))

EXTERN DdNode *cuddUniqueConst ARGS ((DdManager *unique, CUDD_VALUE_TYPE value))

EXTERN void cuddRehash ARGS ((DdManager *unique, int i))

EXTERN int cuddInsertSubtables ARGS ((DdManager *unique, int n, int level))

EXTERN int cuddDestroySubtables ARGS ((DdManager *unique, int n))

EXTERN int cuddResizeTableZdd ARGS ((DdManager *unique, int index))

EXTERN int cuddWindowReorder ARGS ((DdManager *table, int low, int high, Cudd_ReorderingType submethod))

EXTERN int cuddZddGetCofactors3 ARGS ((DdManager *dd, DdNode *f, int v, DdNode **f1, DdNode **f0, DdNode **fd))

EXTERN int cuddZddGetCofactors2 ARGS ((DdManager *dd, DdNode *f, int v, DdNode **f1, DdNode **f0))

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

EXTERN int cuddZddGetPosVarIndex (DdManager *dd, int index)

EXTERN int cuddZddGetNegVarIndex (DdManager *dd, int index)

EXTERN int cuddZddGetPosVarLevel (DdManager *dd, int index)

EXTERN int cuddZddGetNegVarLevel (DdManager *dd, int index)

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

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

EXTERN int cuddZddUniqueCompare ARGS ((int *ptr_x, int *ptr_y))

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

EXTERN DdNode *cuddZddChangeAux ARGS ((DdManager *zdd, DdNode *P, DdNode *zvar))

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

EXTERN int cuddZddP ARGS ((DdManager *zdd, DdNode *f))

Define Documentation

#define cuddAdjust ( x ) ((x) = ((x) >= DD_CRI_HI_MARK) ? DD_PLUS_INF_VAL : (((x) <= DD_CRI_LO_MARK) ? DD_MINUS_INF_VAL : (x)))

Macro***********************************************************************
Synopsis [Enforces DD_MINUS_INF_VAL <= x <= DD_PLUS_INF_VAL.]
Description [Enforces DD_MINUS_INF_VAL <= x <= DD_PLUS_INF_VAL. Furthermore, if x <= DD_MINUS_INF_VAL/2, x is set to DD_MINUS_INF_VAL. Similarly, if DD_PLUS_INF_VAL/2 <= x, x is set to DD_PLUS_INF_VAL. Normally this macro is a NOOP. However, if HAVE_IEEE_754 is not defined, it makes sure that a value does not get larger than infinity in absolute value, and once it gets to infinity, stays there. If the value overflows before this macro is applied, no recovery is possible.]
SideEffects [none]
SeeAlso []
Definition at line 838 of file cuddInt.h.

#define cuddClean ( p ) ((DdNode *)((ptruint)(p) & ~0xf))

Macro***********************************************************************
Synopsis [Clears the 4 least significant bits of a pointer.]
Description []
SideEffects [none]
SeeAlso []
Definition at line 663 of file cuddInt.h.

#define cuddDeallocNode ( unique,
node )

Value:
(node)->next = (unique)->nextFree; \ (unique)->nextFree = node;
Macro***********************************************************************
Synopsis [Adds node to the head of the free list.]
Description [Adds node to the head of the free list. Does not deallocate memory chunks that become free. This function is also used by the dynamic reordering functions.]
SideEffects [None]
SeeAlso [cuddAllocNode cuddDynamicAllocNode]
Definition at line 444 of file cuddInt.h.

#define cuddDeref ( n ) cuddSatDec(Cudd_Regular(n)->ref)

Macro***********************************************************************
Synopsis [Decreases the reference count of a node, if it is not saturated.]
Description [Decreases the reference count of node. It is primarily used in recursive procedures to decrease the ref count of a result node before returning it. This accomplishes the goal of removing the protection applied by a previous cuddRef. This being a macro, it is faster than Cudd_Deref, but it cannot be used in constructs like cuddDeref(a = b()).]
SideEffects [none]
SeeAlso [Cudd_Deref]
Definition at line 483 of file cuddInt.h.

#define cuddE ( node ) ((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. The pointer passed to cuddE must be regular.]
SideEffects [none]
SeeAlso [Cudd_E]
Definition at line 531 of file cuddInt.h.

#define cuddI ( dd,
index ) (((index)==CUDD_MAXINDEX)?(int)(index):(dd)->perm[(index)])

Macro***********************************************************************
Synopsis [Finds the current position of variable index in the order.]
Description [Finds the current position of variable index in the order. This macro duplicates the functionality of Cudd_ReadPerm, but it does not check for out-of-bounds indices and it is more efficient.]
SideEffects [none]
SeeAlso [Cudd_ReadPerm]
Definition at line 565 of file cuddInt.h.

#define cuddIsConstant ( node ) ((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 cuddIsConstant must be regular.]
SideEffects [none]
SeeAlso [Cudd_IsConstant]
Definition at line 499 of file cuddInt.h.

#define cuddIZ ( dd,
index ) (((index)==CUDD_MAXINDEX)?(int)(index):(dd)->permZ[(index)])

Macro***********************************************************************
Synopsis [Finds the current position of ZDD variable index in the order.]
Description [Finds the current position of ZDD variable index in the order. This macro duplicates the functionality of Cudd_ReadPermZdd, but it does not check for out-of-bounds indices and it is more efficient.]
SideEffects [none]
SeeAlso [Cudd_ReadPermZdd]
Definition at line 583 of file cuddInt.h.

#define cuddRef ( n ) cuddSatInc(Cudd_Regular(n)->ref)

Macro***********************************************************************
Synopsis [Increases the reference count of a node, if it is not saturated.]
Description [Increases the reference count of a node, if it is not saturated. This being a macro, it is faster than Cudd_Ref, but it cannot be used in constructs like cuddRef(a = b()).]
SideEffects [none]
SeeAlso [Cudd_Ref]
Definition at line 463 of file cuddInt.h.

#define cuddSatDec ( x ) ((x) -= (x) != (DdHalfWord)DD_MAXREF)

Macro***********************************************************************
Synopsis [Saturating decrement operator.]
Description []
SideEffects [none]
SeeAlso [cuddSatInc]
Definition at line 755 of file cuddInt.h.

#define cuddSatInc ( x ) ((x) += (x) != (DdHalfWord)DD_MAXREF)

Macro***********************************************************************
Synopsis [Saturating increment operator.]
Description []
SideEffects [none]
SeeAlso [cuddSatDec]
Definition at line 737 of file cuddInt.h.

#define cuddT ( node ) ((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. The pointer passed to cuddT must be regular.]
SideEffects [none]
SeeAlso [Cudd_T]
Definition at line 515 of file cuddInt.h.

#define cuddV ( node ) ((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. The pointer passed to cuddV must be regular.]
SideEffects [none]
SeeAlso [Cudd_V]
Definition at line 547 of file cuddInt.h.

#define DD_ADD_BDD_DO_INTERVAL_TAG 0x22

Definition at line 134 of file cuddInt.h.

#define DD_ADD_COMPOSE_RECUR_TAG 0x42

Definition at line 138 of file cuddInt.h.

#define DD_ADD_EVAL_CONST_TAG 0x66

Definition at line 143 of file cuddInt.h.

#define DD_ADD_ITE_CONSTANT_TAG 0x62

Definition at line 142 of file cuddInt.h.

#define DD_ADD_ITE_TAG 0x02

Definition at line 130 of file cuddInt.h.

#define DD_ADD_NON_SIM_COMPOSE_TAG 0x46

Definition at line 139 of file cuddInt.h.

#define DD_BDD_AND_ABSTRACT_TAG 0x06

Definition at line 131 of file cuddInt.h.

#define DD_BDD_CLIPPING_AND_ABSTRACT_DOWN_TAG 0x2a

Definition at line 136 of file cuddInt.h.

#define DD_BDD_CLIPPING_AND_ABSTRACT_UP_TAG 0x26

Definition at line 135 of file cuddInt.h.

#define DD_BDD_COMPOSE_RECUR_TAG 0x2e

Definition at line 137 of file cuddInt.h.

#define DD_BDD_ITE_CONSTANT_TAG 0x6a

Definition at line 144 of file cuddInt.h.

#define DD_BDD_ITE_TAG 0x0e

Definition at line 133 of file cuddInt.h.

#define DD_BDD_XOR_EXIST_ABSTRACT_TAG 0x0a

Definition at line 132 of file cuddInt.h.

#define DD_CRI_HI_MARK (10e150)

Definition at line 87 of file cuddInt.h.

#define DD_CRI_LO_MARK (-(DD_CRI_HI_MARK))

Definition at line 88 of file cuddInt.h.

#define DD_DEFAULT_RECOMB 0

Definition at line 118 of file cuddInt.h.

#define DD_DEFAULT_RESIZE 10

Definition at line 71 of file cuddInt.h.

#define DD_DYN_RATIO 2

Definition at line 121 of file cuddInt.h.

#define DD_EPSILON (1.0e-12)

Definition at line 78 of file cuddInt.h.

#define DD_EQUIV_DC_TAG 0x4a

Definition at line 140 of file cuddInt.h.

#define DD_FIRST_REORDER 4004

Definition at line 120 of file cuddInt.h.

#define DD_GC_FRAC_HI DD_MAX_SUBTABLE_DENSITY * 1.0

Definition at line 103 of file cuddInt.h.

#define DD_GC_FRAC_LO DD_MAX_SUBTABLE_DENSITY * 0.25

Definition at line 102 of file cuddInt.h.

#define DD_GC_FRAC_MIN 0.2

Definition at line 104 of file cuddInt.h.

#define DD_INLINE

CHeaderFile*****************************************************************
FileName [cuddInt.h]
PackageName [cudd]
Synopsis [Internal data structures of the CUDD package.]
Description []
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:
cuddInt.h,v 1.1 2002/09/17 21:58:48 dlm Exp
]
Definition at line 59 of file cuddInt.h.

#define DD_LSDIGIT ( x ) ((x) & DD_APA_MASK)

Macro***********************************************************************
Synopsis [Extract the least significant digit of a double digit.]
Description [Extract the least significant digit of a double digit. Used in the manipulation of arbitrary precision integers.]
SideEffects [None]
SeeAlso [DD_MSDIGIT]
Definition at line 854 of file cuddInt.h.

#define DD_MAX_CACHE_FRACTION 3

Definition at line 109 of file cuddInt.h.

#define DD_MAX_CACHE_TO_SLOTS_RATIO 4

Definition at line 113 of file cuddInt.h.

#define DD_MAX_LOOSE_FRACTION 5

Definition at line 107 of file cuddInt.h.

#define DD_MAX_REORDER_GROWTH 1.2

Definition at line 119 of file cuddInt.h.

#define DD_MAX_SUBTABLE_DENSITY 4

Definition at line 95 of file cuddInt.h.

#define DD_MAXREF ((DdHalfWord) ~0)

Definition at line 69 of file cuddInt.h.

#define DD_MEM_CHUNK 1022

Definition at line 73 of file cuddInt.h.

#define DD_MIN_HIT 30

Definition at line 105 of file cuddInt.h.

#define DD_MINUS_INF_VAL (-(DD_PLUS_INF_VAL))

Definition at line 90 of file cuddInt.h.

#define DD_MINUS_INFINITY ( dd ) ((dd)->minusinfinity)

Macro***********************************************************************
Synopsis [Returns the minus infinity constant node.]
Description []
SideEffects [none]
SeeAlso [DD_ONE DD_ZERO DD_PLUS_INFINITY]
Definition at line 814 of file cuddInt.h.

#define DD_MSDIGIT ( x ) ((x) >> DD_APA_BITS)

Macro***********************************************************************
Synopsis [Extract the most significant digit of a double digit.]
Description [Extract the most significant digit of a double digit. Used in the manipulation of arbitrary precision integers.]
SideEffects [None]
SeeAlso [DD_LSDIGIT]
Definition at line 869 of file cuddInt.h.

#define DD_NON_CONSTANT ((DdNode *) 1)

Definition at line 92 of file cuddInt.h.

#define DD_ONE ( dd ) ((dd)->one)

Macro***********************************************************************
Synopsis [Returns the constant 1 node.]
Description []
SideEffects [none]
SeeAlso [DD_ZERO DD_PLUS_INFINITY DD_MINUS_INFINITY]
Definition at line 770 of file cuddInt.h.

#define DD_ONE_VAL (1.0)

Definition at line 76 of file cuddInt.h.

#define DD_P1 12582917

Definition at line 124 of file cuddInt.h.

#define DD_P2 4256249

Definition at line 125 of file cuddInt.h.

#define DD_P3 741457

Definition at line 126 of file cuddInt.h.

#define DD_P4 1618033999

Definition at line 127 of file cuddInt.h.

#define DD_PLUS_INF_VAL (10e301)

Definition at line 86 of file cuddInt.h.

#define DD_PLUS_INFINITY ( dd ) ((dd)->plusinfinity)

Macro***********************************************************************
Synopsis [Returns the plus infinity constant node.]
Description []
SideEffects [none]
SeeAlso [DD_ONE DD_ZERO DD_MINUS_INFINITY]
Definition at line 800 of file cuddInt.h.

#define DD_SIFT_MAX_SWAPS 2000000

Definition at line 117 of file cuddInt.h.

#define DD_SIFT_MAX_VAR 1000

Definition at line 116 of file cuddInt.h.

#define DD_STASH_FRACTION 64

Definition at line 111 of file cuddInt.h.

#define DD_UNUSED

Definition at line 61 of file cuddInt.h.

#define DD_ZDD_ITE_TAG 0x4e

Definition at line 141 of file cuddInt.h.

#define DD_ZERO ( dd ) ((dd)->zero)

Macro***********************************************************************
Synopsis [Returns the arithmetic 0 constant node.]
Description [Returns the arithmetic 0 constant node. This is different from the logical zero. The latter is obtained by Cudd_Not(DD_ONE(dd)).]
SideEffects [none]
SeeAlso [DD_ONE Cudd_Not DD_PLUS_INFINITY DD_MINUS_INFINITY]
Definition at line 786 of file cuddInt.h.

#define DD_ZERO_VAL (0.0)

Definition at line 77 of file cuddInt.h.

#define ddAbs ( x ) (((x)<0) ? -(x) : (x))

Macro***********************************************************************
Synopsis [Computes the absolute value of a number.]
Description []
SideEffects [none]
SeeAlso []
Definition at line 705 of file cuddInt.h.

#define ddCHash ( o,
f,
g,
h,
s )

Value:
((((((unsigned)(f) + (unsigned)(o)) * DD_P1 + (unsigned)(g)) * DD_P2 + \ (unsigned)(h)) * DD_P3) >> (s))
Macro***********************************************************************
Synopsis [Hash function for the cache.]
Description []
SideEffects [none]
SeeAlso [ddHash ddCHash2]
Definition at line 624 of file cuddInt.h.

#define ddCHash2 ( o,
f,
g,
s ) (((((unsigned)(f) + (unsigned)(o)) * DD_P1 + (unsigned)(g)) * DD_P2) >> (s))

Macro***********************************************************************
Synopsis [Hash function for the cache for functions with two operands.]
Description []
SideEffects [none]
SeeAlso [ddHash ddCHash]
Definition at line 647 of file cuddInt.h.

#define ddEqualVal ( x,
y,
e ) (ddAbs((x)-(y))<(e))

Macro***********************************************************************
Synopsis [Returns 1 if the absolute value of the difference of the two arguments x and y is less than e.]
Description []
SideEffects [none]
SeeAlso []
Definition at line 720 of file cuddInt.h.

#define ddHash ( f,
g,
s ) ((((unsigned)(f) * DD_P1 + (unsigned)(g)) * DD_P2) >> (s))

Macro***********************************************************************
Synopsis [Hash function for the unique table.]
Description []
SideEffects [none]
SeeAlso [ddCHash ddCHash2]
Definition at line 602 of file cuddInt.h.

#define ddMax ( x,
y ) (((y) > (x)) ? (y) : (x))

Macro***********************************************************************
Synopsis [Computes the maximum of two numbers.]
Description []
SideEffects [none]
SeeAlso [ddMin]
Definition at line 691 of file cuddInt.h.

#define ddMin ( x,
y ) (((y) < (x)) ? (y) : (x))

Macro***********************************************************************
Synopsis [Computes the minimum of two numbers.]
Description []
SideEffects [none]
SeeAlso [ddMax]
Definition at line 677 of file cuddInt.h.

#define statLine ( dd )

Macro***********************************************************************
Synopsis [Outputs a line of stats.]
Description [Outputs a line of stats if DD_COUNT and DD_STATS are defined. Increments the number of recursive calls if DD_COUNT is defined.]
SideEffects [None]
SeeAlso []
Definition at line 896 of file cuddInt.h.

Typedef Documentation

typedef struct DdCache DdCache

typedef struct DdHashItem DdHashItem

typedef struct DdHashTable DdHashTable

typedef struct DdHook DdHook

typedef struct DdLevelQueue DdLevelQueue

typedef struct DdLocalCache DdLocalCache

typedef struct DdLocalCacheItem DdLocalCacheItem

typedef DdNode* DdNodePtr

Definition at line 178 of file cuddInt.h.

typedef struct DdQueueItem DdQueueItem

typedef struct DdSubtable DdSubtable

typedef struct Move Move

typedef int ptrint

Definition at line 169 of file cuddInt.h.

typedef unsigned int ptruint

Definition at line 170 of file cuddInt.h.

Function Documentation

EXTERN int cuddZddP ARGS ( (DdManager *zdd, DdNode *f) )

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

EXTERN DdNode* cuddZddChangeAux ARGS ( (DdManager *zdd, DdNode *P, DdNode *zvar) )

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

EXTERN int cuddZddUniqueCompare ARGS ( (int *ptr_x, int *ptr_y) )

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

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

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

EXTERN int cud


Compounds
struct	DdCache
struct	DdHashItem
struct	DdHashTable
struct	DdHook
struct	DdLevelQueue
struct	DdLocalCache
struct	DdLocalCacheItem
struct	DdManager
struct	DdQueueItem
struct	DdSubtable
struct	Move
Defines
#define	DD_INLINE
#define	DD_UNUSED
#define	DD_MAXREF ((DdHalfWord) ~0)
#define	DD_DEFAULT_RESIZE 10
#define	DD_MEM_CHUNK 1022
#define	DD_ONE_VAL (1.0)
#define	DD_ZERO_VAL (0.0)
#define	DD_EPSILON (1.0e-12)
#define	DD_PLUS_INF_VAL (10e301)
#define	DD_CRI_HI_MARK (10e150)
#define	DD_CRI_LO_MARK (-(DD_CRI_HI_MARK))
#define	DD_MINUS_INF_VAL (-(DD_PLUS_INF_VAL))
#define	DD_NON_CONSTANT ((DdNode *) 1)
#define	DD_MAX_SUBTABLE_DENSITY 4
#define	DD_GC_FRAC_LO DD_MAX_SUBTABLE_DENSITY * 0.25
#define	DD_GC_FRAC_HI DD_MAX_SUBTABLE_DENSITY * 1.0
#define	DD_GC_FRAC_MIN 0.2
#define	DD_MIN_HIT 30
#define	DD_MAX_LOOSE_FRACTION 5
#define	DD_MAX_CACHE_FRACTION 3
#define	DD_STASH_FRACTION 64
#define	DD_MAX_CACHE_TO_SLOTS_RATIO 4
#define	DD_SIFT_MAX_VAR 1000
#define	DD_SIFT_MAX_SWAPS 2000000
#define	DD_DEFAULT_RECOMB 0
#define	DD_MAX_REORDER_GROWTH 1.2
#define	DD_FIRST_REORDER 4004
#define	DD_DYN_RATIO 2
#define	DD_P1 12582917
#define	DD_P2 4256249
#define	DD_P3 741457
#define	DD_P4 1618033999
#define	DD_ADD_ITE_TAG 0x02
#define	DD_BDD_AND_ABSTRACT_TAG 0x06
#define	DD_BDD_XOR_EXIST_ABSTRACT_TAG 0x0a
#define	DD_BDD_ITE_TAG 0x0e
#define	DD_ADD_BDD_DO_INTERVAL_TAG 0x22
#define	DD_BDD_CLIPPING_AND_ABSTRACT_UP_TAG 0x26
#define	DD_BDD_CLIPPING_AND_ABSTRACT_DOWN_TAG 0x2a
#define	DD_BDD_COMPOSE_RECUR_TAG 0x2e
#define	DD_ADD_COMPOSE_RECUR_TAG 0x42
#define	DD_ADD_NON_SIM_COMPOSE_TAG 0x46
#define	DD_EQUIV_DC_TAG 0x4a
#define	DD_ZDD_ITE_TAG 0x4e
#define	DD_ADD_ITE_CONSTANT_TAG 0x62
#define	DD_ADD_EVAL_CONST_TAG 0x66
#define	DD_BDD_ITE_CONSTANT_TAG 0x6a
#define	cuddDeallocNode(unique, node)
#define	cuddRef(n) cuddSatInc(Cudd_Regular(n)->ref)
#define	cuddDeref(n) cuddSatDec(Cudd_Regular(n)->ref)
#define	cuddIsConstant(node) ((node)->index == CUDD_MAXINDEX)
#define	cuddT(node) ((node)->type.kids.T)
#define	cuddE(node) ((node)->type.kids.E)
#define	cuddV(node) ((node)->type.value)
#define	cuddI(dd, index) (((index)==CUDD_MAXINDEX)?(int)(index):(dd)->perm[(index)])
#define	cuddIZ(dd, index) (((index)==CUDD_MAXINDEX)?(int)(index):(dd)->permZ[(index)])
#define	ddHash(f, g, s) ((((unsigned)(f) * DD_P1 + (unsigned)(g)) * DD_P2) >> (s))
#define	ddCHash(o, f, g, h, s)
#define	ddCHash2(o, f, g, s) (((((unsigned)(f) + (unsigned)(o)) * DD_P1 + (unsigned)(g)) * DD_P2) >> (s))
#define	cuddClean(p) ((DdNode *)((ptruint)(p) & ~0xf))
#define	ddMin(x, y) (((y) < (x)) ? (y) : (x))
#define	ddMax(x, y) (((y) > (x)) ? (y) : (x))
#define	ddAbs(x) (((x)<0) ? -(x) : (x))
#define	ddEqualVal(x, y, e) (ddAbs((x)-(y))<(e))
#define	cuddSatInc(x) ((x) += (x) != (DdHalfWord)DD_MAXREF)
#define	cuddSatDec(x) ((x) -= (x) != (DdHalfWord)DD_MAXREF)
#define	DD_ONE(dd) ((dd)->one)
#define	DD_ZERO(dd) ((dd)->zero)
#define	DD_PLUS_INFINITY(dd) ((dd)->plusinfinity)
#define	DD_MINUS_INFINITY(dd) ((dd)->minusinfinity)
#define	cuddAdjust(x) ((x) = ((x) >= DD_CRI_HI_MARK) ? DD_PLUS_INF_VAL : (((x) <= DD_CRI_LO_MARK) ? DD_MINUS_INF_VAL : (x)))
#define	DD_LSDIGIT(x) ((x) & DD_APA_MASK)
#define	DD_MSDIGIT(x) ((x) >> DD_APA_BITS)
#define	statLine(dd)
Typedefs
typedef DdHook	DdHook
typedef int	ptrint
typedef unsigned int	ptruint
typedef DdNode *	DdNodePtr
typedef DdLocalCacheItem	DdLocalCacheItem
typedef DdLocalCache	DdLocalCache
typedef DdHashItem	DdHashItem
typedef DdHashTable	DdHashTable
typedef DdCache	DdCache
typedef DdSubtable	DdSubtable
typedef Move	Move
typedef DdQueueItem	DdQueueItem
typedef DdLevelQueue	DdLevelQueue
Functions
EXTERN DdNode *cuddAddExistAbstractRecur	ARGS ((DdManager manager, DdNode f, DdNode *cube))
EXTERN DdNode *cuddAddApplyRecur	ARGS ((DdManager dd, DdNode ()(DdManager , DdNode , DdNode ), DdNode f, DdNode g))
EXTERN DdNode *cuddAddScalarInverseRecur	ARGS ((DdManager dd, DdNode f, DdNode *epsilon))
EXTERN DdNode *cuddAddIteRecur	ARGS ((DdManager dd, DdNode f, DdNode g, DdNode h))
EXTERN DdNode *cuddAddCmplRecur	ARGS ((DdManager dd, DdNode f))
EXTERN DdNode *cuddAddRoundOffRecur	ARGS ((DdManager dd, DdNode f, double trunc))
EXTERN DdNode *cuddUnderApprox	ARGS ((DdManager dd, DdNode f, int numVars, int threshold, int safe, double quality))
EXTERN DdNode *cuddRemapUnderApprox	ARGS ((DdManager dd, DdNode f, int numVars, int threshold, double quality))
EXTERN DdNode *cuddBiasedUnderApprox	ARGS ((DdManager dd, DdNode f, DdNode *b, int numVars, int threshold, double quality1, double quality0))
EXTERN DdNode *cuddBddAndAbstractRecur	ARGS ((DdManager manager, DdNode f, DdNode g, DdNode cube))
EXTERN int cuddAnnealing	ARGS ((DdManager *table, int lower, int upper))
EXTERN DdNode *cuddBddBooleanDiffRecur	ARGS ((DdManager manager, DdNode f, DdNode *var))
EXTERN DdNode *cuddBddIntersectRecur	ARGS ((DdManager dd, DdNode f, DdNode *g))
EXTERN DdNode *cuddBddAndRecur	ARGS ((DdManager manager, DdNode f, DdNode *g))
EXTERN DdNode *cuddBddTransfer	ARGS ((DdManager ddS, DdManager ddD, DdNode *f))
EXTERN int cuddInitCache	ARGS ((DdManager *unique, unsigned int cacheSize, unsigned int maxCacheSize))
EXTERN void cuddCacheInsert	ARGS ((DdManager table, ptruint op, DdNode f, DdNode g, DdNode h, DdNode *data))
EXTERN void cuddCacheInsert2	ARGS ((DdManager table, DdNode ()(DdManager , DdNode , DdNode ), DdNode f, DdNode g, DdNode *data))
EXTERN void cuddCacheInsert1	ARGS ((DdManager table, DdNode ()(DdManager , DdNode ), DdNode f, DdNode *data))
EXTERN DdNode *cuddCacheLookup	ARGS ((DdManager table, ptruint op, DdNode f, DdNode g, DdNode h))
EXTERN DdNode *cuddCacheLookup2	ARGS ((DdManager table, DdNode ()(DdManager , DdNode , DdNode ), DdNode f, DdNode g))
EXTERN DdNode *cuddCacheLookup1	ARGS ((DdManager table, DdNode ()(DdManager , DdNode ), DdNode f))
EXTERN int cuddCacheProfile	ARGS ((DdManager table, FILE fp))
EXTERN void cuddCacheResize	ARGS ((DdManager *table))
EXTERN int cuddComputeFloorLog2	ARGS ((unsigned int value))
EXTERN int cuddHeapProfile	ARGS ((DdManager *dd))
EXTERN void cuddPrintNode	ARGS ((DdNode f, FILE fp))
EXTERN void cuddPrintVarGroups	ARGS ((DdManager dd, MtrNode root, int zdd, int silent))
EXTERN DdNode *cuddBddClippingAnd	ARGS ((DdManager dd, DdNode f, DdNode *g, int maxDepth, int direction))
EXTERN DdNode *cuddBddClippingAndAbstract	ARGS ((DdManager dd, DdNode f, DdNode g, DdNode cube, int maxDepth, int direction))
EXTERN void cuddGetBranches	ARGS ((DdNode g, DdNode g1, DdNode *g0))
EXTERN int cuddCheckCube	ARGS ((DdManager dd, DdNode g))
EXTERN DdNode *cuddBddComposeRecur	ARGS ((DdManager dd, DdNode f, DdNode g, DdNode proj))
EXTERN DdNode *cuddBddConstrainRecur	ARGS ((DdManager dd, DdNode f, DdNode *c))
EXTERN int cuddTreeSifting	ARGS ((DdManager *table, Cudd_ReorderingType method))
EXTERN int cuddZddInitUniv	ARGS ((DdManager *zdd))
EXTERN void cuddSetInteract	ARGS ((DdManager *table, int x, int y))
EXTERN DdLocalCache *cuddLocalCacheInit	ARGS ((DdManager *manager, unsigned int keySize, unsigned int cacheSize, unsigned int maxCacheSize))
EXTERN void cuddLocalCacheQuit	ARGS ((DdLocalCache *cache))
EXTERN void cuddLocalCacheInsert	ARGS ((DdLocalCache cache, DdNodePtr key, DdNode *value))
EXTERN DdNode *cuddLocalCacheLookup	ARGS ((DdLocalCache cache, DdNodePtr key))
EXTERN void cuddLocalCacheClearDead	ARGS ((DdManager *manager))
EXTERN DdHashTable *cuddHashTableInit	ARGS ((DdManager *manager, unsigned int keySize, unsigned int initSize))
EXTERN void cuddHashTableQuit	ARGS ((DdHashTable *hash))
EXTERN int cuddHashTableInsert	ARGS ((DdHashTable hash, DdNodePtr key, DdNode *value, ptrint count))
EXTERN DdNode *cuddHashTableLookup	ARGS ((DdHashTable hash, DdNodePtr key))
EXTERN int cuddHashTableInsert1	ARGS ((DdHashTable hash, DdNode f, DdNode *value, ptrint count))
EXTERN DdNode *cuddHashTableLookup1	ARGS ((DdHashTable hash, DdNode f))
EXTERN int cuddHashTableInsert2	ARGS ((DdHashTable hash, DdNode f, DdNode g, DdNode value, ptrint count))
EXTERN DdNode *cuddHashTableLookup2	ARGS ((DdHashTable hash, DdNode f, DdNode *g))
EXTERN int cuddHashTableInsert3	ARGS ((DdHashTable hash, DdNode f, DdNode g, DdNode h, DdNode *value, ptrint count))
EXTERN DdNode *cuddHashTableLookup3	ARGS ((DdHashTable hash, DdNode f, DdNode g, DdNode h))
EXTERN DdLevelQueue *cuddLevelQueueInit	ARGS ((int levels, int itemSize, int numBuckets))
EXTERN void cuddLevelQueueQuit	ARGS ((DdLevelQueue *queue))
EXTERN void *cuddLevelQueueEnqueue	ARGS ((DdLevelQueue queue, void key, int level))
EXTERN void cuddLevelQueueDequeue	ARGS ((DdLevelQueue *queue, int level))
EXTERN DdNode *cuddCProjectionRecur	ARGS ((DdManager dd, DdNode R, DdNode Y, DdNode Ysupp))
EXTERN void cuddReclaim	ARGS ((DdManager table, DdNode n))
EXTERN int cuddSwapping	ARGS ((DdManager *table, int lower, int upper, Cudd_ReorderingType heuristic))
EXTERN int cuddNextHigh	ARGS ((DdManager *table, int x))
EXTERN DdNode *cuddSolveEqnRecur	ARGS ((DdManager bdd, DdNode F, DdNode Y, DdNode G, int n, int yIndex, int i))
EXTERN DdNode *cuddVerifySol	ARGS ((DdManager bdd, DdNode F, DdNode *G, int yIndex, int n))
EXTERN DdNode *cuddSubsetHeavyBranch	ARGS ((DdManager dd, DdNode f, int numVars, int threshold))
EXTERN DdNode *cuddSubsetShortPaths	ARGS ((DdManager dd, DdNode f, int numVars, int threshold, int hardlimit))
EXTERN DdNode *cuddAllocNode	ARGS ((DdManager *unique))
EXTERN DdManager *cuddInitTable	ARGS ((unsigned int numVars, unsigned int numVarsZ, unsigned int numSlots, unsigned int looseUpTo))
EXTERN int cuddGarbageCollect	ARGS ((DdManager *unique, int clearCache))
EXTERN DdNode *cuddZddGetNode	ARGS ((DdManager zdd, int id, DdNode T, DdNode *E))
EXTERN DdNode *cuddZddGetNodeIVO	ARGS ((DdManager dd, int index, DdNode g, DdNode *h))
EXTERN DdNode *cuddUniqueInter	ARGS ((DdManager unique, int index, DdNode T, DdNode *E))
EXTERN DdNode *cuddUniqueConst	ARGS ((DdManager *unique, CUDD_VALUE_TYPE value))
EXTERN void cuddRehash	ARGS ((DdManager *unique, int i))
EXTERN int cuddInsertSubtables	ARGS ((DdManager *unique, int n, int level))
EXTERN int cuddDestroySubtables	ARGS ((DdManager *unique, int n))
EXTERN int cuddResizeTableZdd	ARGS ((DdManager *unique, int index))
EXTERN int cuddWindowReorder	ARGS ((DdManager *table, int low, int high, Cudd_ReorderingType submethod))
EXTERN int cuddZddGetCofactors3	ARGS ((DdManager dd, DdNode f, int v, DdNode f1, DdNode f0, DdNode **fd))
EXTERN int cuddZddGetCofactors2	ARGS ((DdManager dd, DdNode f, int v, DdNode f1, DdNode f0))
EXTERN DdNode *cuddZddComplement	ARGS ((DdManager dd, DdNode node))
EXTERN int	cuddZddGetPosVarIndex (DdManager *dd, int index)
EXTERN int	cuddZddGetNegVarIndex (DdManager *dd, int index)
EXTERN int	cuddZddGetPosVarLevel (DdManager *dd, int index)
EXTERN int	cuddZddGetNegVarLevel (DdManager *dd, int index)
EXTERN DdNode *cuddZddIsop	ARGS ((DdManager dd, DdNode L, DdNode U, DdNode *zdd_I))
EXTERN DdNode *cuddBddIsop	ARGS ((DdManager dd, DdNode L, DdNode *U))
EXTERN int cuddZddUniqueCompare	ARGS ((int ptr_x, int ptr_y))
EXTERN DdNode *cuddZddUnion	ARGS ((DdManager zdd, DdNode P, DdNode *Q))
EXTERN DdNode *cuddZddChangeAux	ARGS ((DdManager zdd, DdNode P, DdNode *zvar))
EXTERN DdNode *cuddZddSubset1	ARGS ((DdManager dd, DdNode P, int var))
EXTERN int cuddZddP	ARGS ((DdManager zdd, DdNode f))