src/bdd/cudd/cuddInt.h File Reference

#include <math.h>
#include "cudd.h"
#include "st.h"
Include dependency graph for cuddInt.h:

Go to the source code of this file.

Data Structures

struct  DdGen
struct  DdHook
struct  DdLocalCacheItem
struct  DdLocalCache
struct  DdHashItem
struct  DdHashTable
struct  DdCache
struct  DdSubtable
struct  DdManager
struct  Move
struct  DdQueueItem
struct  DdLevelQueue

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 DD_ADD_OUT_SUM_TAG   0x6e
#define DD_BDD_LEQ_UNLESS_TAG   0x82
#define DD_ADD_TRIANGLE_TAG   0x86
#define CUDD_GEN_CUBES   0
#define CUDD_GEN_NODES   1
#define CUDD_GEN_ZDD_PATHS   2
#define CUDD_GEN_EMPTY   0
#define CUDD_GEN_NONEMPTY   1
#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_CONST_INDEX)
#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_CONST_INDEX)?(int)(index):(dd)->perm[(index)])
#define cuddIZ(dd, index)   (((index)==CUDD_CONST_INDEX)?(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 int ptrint
typedef unsigned int ptruint
typedef DdNode * DdNodePtr

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
*cuddAddMonadicApplyRecur 		ARGS ((DdManager *dd, DdNode *(*op)(DdManager *, DdNode *), DdNode *f))
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 DdNode *cuddBddClosestCube ARGS ((DdManager *dd, DdNode *f, DdNode *g, CUDD_VALUE_TYPE bound))
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 *cuddBddMakePrime ARGS ((DdManager *dd, DdNode *cube, DdNode *f))
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 CUDD_GEN_CUBES   0

Definition at line 162 of file cuddInt.h.

#define CUDD_GEN_EMPTY   0

Definition at line 165 of file cuddInt.h.

#define CUDD_GEN_NODES   1

Definition at line 163 of file cuddInt.h.

#define CUDD_GEN_NONEMPTY   1

Definition at line 166 of file cuddInt.h.

#define CUDD_GEN_ZDD_PATHS   2

Definition at line 164 of file cuddInt.h.

#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 889 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 714 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 495 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 534 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 582 of file cuddInt.h.

#define cuddI ( dd,
index   )     (((index)==CUDD_CONST_INDEX)?(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 616 of file cuddInt.h.

#define cuddIsConstant ( node   )     ((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 cuddIsConstant must be regular.]

SideEffects [none]

SeeAlso [Cudd_IsConstant]

Definition at line 550 of file cuddInt.h.

#define cuddIZ ( dd,
index   )     (((index)==CUDD_CONST_INDEX)?(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 634 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 514 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 806 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 788 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 566 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 598 of file cuddInt.h.

#define DD_ADD_BDD_DO_INTERVAL_TAG   0x22

Definition at line 146 of file cuddInt.h.

#define DD_ADD_COMPOSE_RECUR_TAG   0x42

Definition at line 150 of file cuddInt.h.

#define DD_ADD_EVAL_CONST_TAG   0x66

Definition at line 155 of file cuddInt.h.

#define DD_ADD_ITE_CONSTANT_TAG   0x62

Definition at line 154 of file cuddInt.h.

#define DD_ADD_ITE_TAG   0x02

Definition at line 142 of file cuddInt.h.

#define DD_ADD_NON_SIM_COMPOSE_TAG   0x46

Definition at line 151 of file cuddInt.h.

#define DD_ADD_OUT_SUM_TAG   0x6e

Definition at line 157 of file cuddInt.h.

#define DD_ADD_TRIANGLE_TAG   0x86

Definition at line 159 of file cuddInt.h.

#define DD_BDD_AND_ABSTRACT_TAG   0x06

Definition at line 143 of file cuddInt.h.

#define DD_BDD_CLIPPING_AND_ABSTRACT_DOWN_TAG   0x2a

Definition at line 148 of file cuddInt.h.

#define DD_BDD_CLIPPING_AND_ABSTRACT_UP_TAG   0x26

Definition at line 147 of file cuddInt.h.

#define DD_BDD_COMPOSE_RECUR_TAG   0x2e

Definition at line 149 of file cuddInt.h.

#define DD_BDD_ITE_CONSTANT_TAG   0x6a

Definition at line 156 of file cuddInt.h.

#define DD_BDD_ITE_TAG   0x0e

Definition at line 145 of file cuddInt.h.

#define DD_BDD_LEQ_UNLESS_TAG   0x82

Definition at line 158 of file cuddInt.h.

#define DD_BDD_XOR_EXIST_ABSTRACT_TAG   0x0a

Definition at line 144 of file cuddInt.h.

#define DD_CRI_HI_MARK   (10e150)

Definition at line 88 of file cuddInt.h.

#define DD_CRI_LO_MARK   (-(DD_CRI_HI_MARK))

Definition at line 89 of file cuddInt.h.

#define DD_DEFAULT_RECOMB   0

Definition at line 119 of file cuddInt.h.

#define DD_DEFAULT_RESIZE   10

Definition at line 72 of file cuddInt.h.

#define DD_DYN_RATIO   2

Definition at line 122 of file cuddInt.h.

#define DD_EPSILON   (1.0e-12)

Definition at line 79 of file cuddInt.h.

#define DD_EQUIV_DC_TAG   0x4a

Definition at line 152 of file cuddInt.h.

#define DD_FIRST_REORDER   4004

Definition at line 121 of file cuddInt.h.

#define DD_GC_FRAC_HI   DD_MAX_SUBTABLE_DENSITY * 1.0

Definition at line 104 of file cuddInt.h.

#define DD_GC_FRAC_LO   DD_MAX_SUBTABLE_DENSITY * 0.25

Definition at line 103 of file cuddInt.h.

#define DD_GC_FRAC_MIN   0.2

Definition at line 105 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.1.1 2003/02/24 22:23:52 wjiang Exp

]

Definition at line 60 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 905 of file cuddInt.h.

#define DD_MAX_CACHE_FRACTION   3

Definition at line 110 of file cuddInt.h.

#define DD_MAX_CACHE_TO_SLOTS_RATIO   4

Definition at line 114 of file cuddInt.h.

#define DD_MAX_LOOSE_FRACTION   5

Definition at line 108 of file cuddInt.h.

#define DD_MAX_REORDER_GROWTH   1.2

Definition at line 120 of file cuddInt.h.

#define DD_MAX_SUBTABLE_DENSITY   4

Definition at line 96 of file cuddInt.h.

#define DD_MAXREF   ((DdHalfWord) ~0)

Definition at line 70 of file cuddInt.h.

#define DD_MEM_CHUNK   1022

Definition at line 74 of file cuddInt.h.

#define DD_MIN_HIT   30

Definition at line 106 of file cuddInt.h.

#define DD_MINUS_INF_VAL   (-(DD_PLUS_INF_VAL))

Definition at line 91 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 865 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 920 of file cuddInt.h.

#define DD_NON_CONSTANT   ((DdNode *) 1)

Definition at line 93 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 821 of file cuddInt.h.

#define DD_ONE_VAL   (1.0)

Definition at line 77 of file cuddInt.h.

#define DD_P1   12582917

Definition at line 125 of file cuddInt.h.

#define DD_P2   4256249

Definition at line 126 of file cuddInt.h.

#define DD_P3   741457

Definition at line 127 of file cuddInt.h.

#define DD_P4   1618033999

Definition at line 128 of file cuddInt.h.

#define DD_PLUS_INF_VAL   (10e301)

Definition at line 87 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 851 of file cuddInt.h.

#define DD_SIFT_MAX_SWAPS   2000000

Definition at line 118 of file cuddInt.h.

#define DD_SIFT_MAX_VAR   1000

Definition at line 117 of file cuddInt.h.

#define DD_STASH_FRACTION   64

Definition at line 112 of file cuddInt.h.

#define DD_UNUSED

Definition at line 62 of file cuddInt.h.

#define DD_ZDD_ITE_TAG   0x4e

Definition at line 153 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 837 of file cuddInt.h.

#define DD_ZERO_VAL   (0.0)

Definition at line 78 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 756 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 675 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 698 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 771 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 653 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 742 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 728 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 947 of file cuddInt.h.

Typedef Documentation

typedef DdNode* DdNodePtr

Definition at line 221 of file cuddInt.h.

typedef int ptrint

Definition at line 212 of file cuddInt.h.

typedef unsigned int ptruint

Definition at line 213 of file cuddInt.h.

Function Documentation

EXTERN int cuddZddP ARGS ( (DdManager *zdd, DdNode *f)   ) 
EXTERN DdNode* cuddZddSubset1 ARGS ( (DdManager *dd, DdNode *P, int var)   ) 
static DdNode *zdd_subset0_aux 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 cuddZddGetCofactors2 ARGS ( (DdManager *dd, DdNode *f, int v, DdNode **f1, DdNode **f0)   ) 
EXTERN int cuddZddGetCofactors3 ARGS ( (DdManager *dd, DdNode *f, int v, DdNode **f1, DdNode **f0, DdNode **fd)   ) 
EXTERN int cuddWindowReorder ARGS ( (DdManager *table, int low, int high, Cudd_ReorderingType submethod)   ) 
EXTERN int cuddResizeTableZdd ARGS ( (DdManager *unique, int index)   ) 
EXTERN int cuddDestroySubtables ARGS ( (DdManager *unique, int n)   ) 
EXTERN int cuddInsertSubtables ARGS ( (DdManager *unique, int n, int level)   ) 
EXTERN void cuddShrinkSubtable ARGS ( (DdManager *unique, int i)   ) 
EXTERN DdNode* cuddUniqueConst ARGS ( (DdManager *unique, CUDD_VALUE_TYPE value)   ) 
EXTERN DdNode *cuddUniqueInterZdd ARGS ( (DdManager *unique, int index, DdNode *T, DdNode *E)   ) 
EXTERN DdNode* cuddZddGetNodeIVO ARGS ( (DdManager *dd, int index, DdNode *g, DdNode *h)   ) 
EXTERN DdNode* cuddZddGetNode ARGS ( (DdManager *zdd, int id, DdNode *T, DdNode *E)   ) 
EXTERN int cuddGarbageCollectZdd ARGS ( (DdManager *unique, int clearCache)   ) 
EXTERN DdManager* cuddInitTable ARGS ( (unsigned int numVars, unsigned int numVarsZ, unsigned int numSlots, unsigned int looseUpTo)   ) 
EXTERN DdNode* cuddAllocNode ARGS ( (DdManager *unique)   ) 
EXTERN DdNode* cuddSubsetShortPaths ARGS ( (DdManager *dd, DdNode *f, int numVars, int threshold, int hardlimit)   ) 
EXTERN DdNode* cuddSubsetHeavyBranch ARGS ( (DdManager *dd, DdNode *f, int numVars, int threshold)   ) 
EXTERN DdNode* cuddVerifySol ARGS ( (DdManager *bdd, DdNode *F, DdNode **G, int *yIndex, int n)   ) 
EXTERN DdNode* cuddSolveEqnRecur ARGS ( (DdManager *bdd, DdNode *F, DdNode *Y, DdNode **G, int n, int *yIndex, int i)   ) 
EXTERN DdNode* cuddBddMakePrime ARGS ( (DdManager *dd, DdNode *cube, DdNode *f)   ) 
EXTERN int cuddZddNextLow ARGS ( (DdManager *table, int x)   ) 
EXTERN int cuddZddSwapping ARGS ( (DdManager *table, int lower, int upper, Cudd_ReorderingType heuristic)   ) 
EXTERN void cuddReclaim ARGS ( (DdManager *table, DdNode *n)   ) 
EXTERN DdNode* cuddBddClosestCube ARGS ( (DdManager *dd, DdNode *f, DdNode *g, CUDD_VALUE_TYPE bound)   ) 
EXTERN DdNode* cuddCProjectionRecur ARGS ( (DdManager *dd, DdNode *R, DdNode *Y, DdNode *Ysupp)   ) 
EXTERN void cuddLevelQueueDequeue ARGS ( (DdLevelQueue *queue, int level)   ) 
EXTERN void* cuddLevelQueueEnqueue ARGS ( (DdLevelQueue *queue, void *key, int level)   ) 
EXTERN void cuddLevelQueueQuit ARGS ( (DdLevelQueue *queue)   ) 
EXTERN DdLevelQueue* cuddLevelQueueInit ARGS ( (int levels, int itemSize, int numBuckets)   ) 
EXTERN DdNode* cuddHashTableLookup3 ARGS ( (DdHashTable *hash, DdNode *f, DdNode *g, DdNode *h)   ) 
EXTERN int cuddHashTableInsert3 ARGS ( (DdHashTable *hash, DdNode *f, DdNode *g, DdNode *h, DdNode *value, ptrint count)   ) 
EXTERN DdNode* cuddHashTableLookup2 ARGS ( (DdHashTable *hash, DdNode *f, DdNode *g)   ) 
EXTERN int cuddHashTableInsert2 ARGS ( (DdHashTable *hash, DdNode *f, DdNode *g, DdNode *value, ptrint count)   ) 
EXTERN DdNode* cuddHashTableLookup1 ARGS ( (DdHashTable *hash, DdNode *f)   ) 
EXTERN int cuddHashTableInsert1 ARGS ( (DdHashTable *hash, DdNode *f, DdNode *value, ptrint count)   ) 
EXTERN DdNode* cuddHashTableLookup ARGS ( (DdHashTable *hash, DdNodePtr *key)   ) 
EXTERN int cuddHashTableInsert ARGS ( (DdHashTable *hash, DdNodePtr *key, DdNode *value, ptrint count)   ) 
static DD_INLINE DdHashItem *cuddHashTableAlloc ARGS ( (DdHashTable *hash)   ) 
EXTERN DdHashTable* cuddHashTableInit ARGS ( (DdManager *manager, unsigned int keySize, unsigned int initSize)   ) 
EXTERN void cuddLocalCacheClearDead ARGS ( (DdManager *manager)   ) 
EXTERN DdNode* cuddLocalCacheLookup ARGS ( (DdLocalCache *cache, DdNodePtr *key)   ) 
EXTERN void cuddLocalCacheInsert ARGS ( (DdLocalCache *cache, DdNodePtr *key, DdNode *value)   ) 
static void cuddLocalCacheRemoveFromList ARGS ( (DdLocalCache *cache)   ) 
EXTERN DdLocalCache* cuddLocalCacheInit ARGS ( (DdManager *manager, unsigned int keySize, unsigned int cacheSize, unsigned int maxCacheSize)   ) 
EXTERN void cuddSetInteract ARGS ( (DdManager *table, int x, int y)   ) 
EXTERN void cuddZddFreeUniv ARGS ( (DdManager *zdd)   ) 
EXTERN int cuddZddTreeSifting ARGS ( (DdManager *table, Cudd_ReorderingType method)   ) 
EXTERN DdNode* cuddBddConstrainRecur ARGS ( (DdManager *dd, DdNode *f, DdNode *c)   ) 
EXTERN DdNode *cuddAddComposeRecur ARGS ( (DdManager *dd, DdNode *f, DdNode *g, DdNode *proj)   ) 
EXTERN int cuddCheckCube ARGS ( (DdManager *dd, DdNode *g)   ) 
EXTERN void cuddGetBranches ARGS ( (DdNode *g, DdNode **g1, DdNode **g0)   ) 
EXTERN DdNode* cuddBddClippingAndAbstract ARGS ( (DdManager *dd, DdNode *f, DdNode *g, DdNode *cube, int maxDepth, int direction)   ) 
EXTERN DdNode* cuddBddClippingAnd ARGS ( (DdManager *dd, DdNode *f, DdNode *g, int maxDepth, int direction)   ) 
EXTERN void cuddPrintVarGroups ARGS ( (DdManager *dd, MtrNode *root, int zdd, int silent)   ) 
EXTERN void cuddPrintNode ARGS ( (DdNode *f, FILE *fp)   ) 
EXTERN int cuddHeapProfile ARGS ( (DdManager *dd)   ) 
EXTERN int cuddComputeFloorLog2 ARGS ( (unsigned int value)   ) 
EXTERN void cuddCacheResize ARGS ( (DdManager *table)   ) 
EXTERN int cuddCacheProfile ARGS ( (DdManager *table, FILE *fp)   ) 
EXTERN DdNode *cuddCacheLookup1Zdd ARGS ( (DdManager *table, DdNode *(*)(DdManager *, DdNode *), DdNode *f)   ) 
EXTERN DdNode *cuddCacheLookup2Zdd ARGS ( (DdManager *table, DdNode *(*)(DdManager *, DdNode *, DdNode *), DdNode *f, DdNode *g)   ) 
EXTERN DdNode *cuddConstantLookup ARGS ( (DdManager *table, ptruint op, DdNode *f, DdNode *g, DdNode *h)   ) 
EXTERN void cuddCacheInsert1 ARGS ( (DdManager *table, DdNode *(*)(DdManager *, DdNode *), DdNode *f, DdNode *data)   ) 
EXTERN void cuddCacheInsert2 ARGS ( (DdManager *table, DdNode *(*)(DdManager *, DdNode *, DdNode *), DdNode *f, DdNode *g, DdNode *data)   ) 
EXTERN void cuddCacheInsert ARGS ( (DdManager *table, ptruint op, DdNode *f, DdNode *g, DdNode *h, DdNode *data)   ) 
EXTERN int cuddInitCache ARGS ( (DdManager *unique, unsigned int cacheSize, unsigned int maxCacheSize)   ) 
EXTERN DdNode* cuddBddTransfer ARGS ( (DdManager *ddS, DdManager *ddD, DdNode *f)   ) 
EXTERN DdNode* cuddBddAndRecur ARGS ( (DdManager *manager, DdNode *f, DdNode *g)   ) 
EXTERN DdNode* cuddBddIntersectRecur ARGS ( (DdManager *dd, DdNode *f, DdNode *g)   ) 
EXTERN DdNode* cuddBddBooleanDiffRecur ARGS ( (DdManager *manager, DdNode *f, DdNode *var)   ) 
EXTERN int cuddAnnealing ARGS ( (DdManager *table, int lower, int upper)   ) 
EXTERN DdNode* cuddBddAndAbstractRecur ARGS ( (DdManager *manager, DdNode *f, DdNode *g, DdNode *cube)   ) 
EXTERN DdNode* cuddBiasedUnderApprox ARGS ( (DdManager *dd, DdNode *f, DdNode *b, int numVars, int threshold, double quality1, double quality0)   ) 
EXTERN DdNode* cuddRemapUnderApprox ARGS ( (DdManager *dd, DdNode *f, int numVars, int threshold, double quality)   ) 
EXTERN DdNode* cuddUnderApprox ARGS ( (DdManager *dd, DdNode *f, int numVars, int threshold, int safe, double quality)   ) 
EXTERN DdNode* cuddAddRoundOffRecur ARGS ( (DdManager *dd, DdNode *f, double trunc)   ) 
EXTERN DdNode* cuddAddCmplRecur ARGS ( (DdManager *dd, DdNode *f)   ) 
EXTERN DdNode* cuddAddIteRecur ARGS ( (DdManager *dd, DdNode *f, DdNode *g, DdNode *h)   ) 
EXTERN DdNode* cuddAddScalarInverseRecur ARGS ( (DdManager *dd, DdNode *f, DdNode *epsilon)   ) 
EXTERN DdNode* cuddAddMonadicApplyRecur ARGS ( (DdManager *dd, DdNode *(*op)(DdManager *, DdNode *), DdNode *f)   ) 
EXTERN DdNode* cuddAddApplyRecur ARGS ( (DdManager *dd, DdNode *(*)(DdManager *, DdNode **, DdNode **), DdNode *f, DdNode *g)   ) 
EXTERN DdNode* cuddAddExistAbstractRecur ARGS ( (DdManager *manager, DdNode *f, DdNode *cube)   ) 

AutomaticStart

EXTERN int cuddZddGetNegVarIndex ( DdManager *  dd,
int  index 
)

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

Synopsis [Returns the index of negative ZDD variable.]

Description [Returns the index of negative ZDD variable.]

SideEffects []

SeeAlso []

Definition at line 1555 of file cuddZddFuncs.c.

01558 {
01559     int nv = index | 0x1;
01560     return(nv);
01561 } /* end of cuddZddGetPosVarIndex */

EXTERN int cuddZddGetNegVarLevel ( DdManager *  dd,
int  index 
)

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

Synopsis [Returns the level of negative ZDD variable.]

Description [Returns the level of negative ZDD variable.]

SideEffects []

SeeAlso []

Definition at line 1597 of file cuddZddFuncs.c.

01600 {
01601     int nv = cuddZddGetNegVarIndex(dd, index);
01602     return(dd->permZ[nv]);
01603 } /* end of cuddZddGetNegVarLevel */

EXTERN int cuddZddGetPosVarIndex ( DdManager *  dd,
int  index 
)

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

Synopsis [Returns the index of positive ZDD variable.]

Description [Returns the index of positive ZDD variable.]

SideEffects []

SeeAlso []

Definition at line 1534 of file cuddZddFuncs.c.

01537 {
01538     int pv = (index >> 1) << 1;
01539     return(pv);
01540 } /* end of cuddZddGetPosVarIndex */

EXTERN int cuddZddGetPosVarLevel ( DdManager *  dd,
int  index 
)

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

Synopsis [Returns the level of positive ZDD variable.]

Description [Returns the level of positive ZDD variable.]

SideEffects []

SeeAlso []

Definition at line 1576 of file cuddZddFuncs.c.

01579 {
01580     int pv = cuddZddGetPosVarIndex(dd, index);
01581     return(dd->permZ[pv]);
01582 } /* end of cuddZddGetPosVarLevel */

Generated on Tue Jan 5 12:18:55 2010 for abc70930 by  doxygen 1.6.1