cudd
3.0.0
The University of Colorado Decision Diagram Package
|
Go to the documentation of this file.
65 #define CUDD_VERSION PACKAGE_VERSION
67 #define DD_MAXREF ((DdHalfWord) ~0)
69 #define DD_DEFAULT_RESIZE 10
71 #define DD_MEM_CHUNK 1022
74 #define DD_ONE_VAL (1.0)
75 #define DD_ZERO_VAL (0.0)
76 #define DD_EPSILON (1.0e-12)
82 # define DD_PLUS_INF_VAL (HUGE_VAL)
84 # define DD_PLUS_INF_VAL (10e301)
85 # define DD_CRI_HI_MARK (10e150)
86 # define DD_CRI_LO_MARK (-(DD_CRI_HI_MARK))
88 #define DD_MINUS_INF_VAL (-(DD_PLUS_INF_VAL))
90 #define DD_NON_CONSTANT ((DdNode *) 1)
93 #define DD_MAX_SUBTABLE_DENSITY 4
100 #define DD_GC_FRAC_LO DD_MAX_SUBTABLE_DENSITY * 0.25
101 #define DD_GC_FRAC_HI DD_MAX_SUBTABLE_DENSITY * 1.0
102 #define DD_GC_FRAC_MIN 0.2
103 #define DD_MIN_HIT 30
105 #define DD_MAX_LOOSE_FRACTION 5
107 #define DD_MAX_CACHE_FRACTION 3
109 #define DD_STASH_FRACTION 64
111 #define DD_MAX_CACHE_TO_SLOTS_RATIO 4
114 #define DD_SIFT_MAX_VAR 1000
115 #define DD_SIFT_MAX_SWAPS 2000000
116 #define DD_DEFAULT_RECOMB 0
117 #define DD_MAX_REORDER_GROWTH 1.2
118 #define DD_FIRST_REORDER 4004
119 #define DD_DYN_RATIO 2
122 #define DD_P1 12582917
123 #define DD_P2 4256249
125 #define DD_P4 1618033999
139 #define DD_ADD_ITE_TAG 0x02
140 #define DD_BDD_AND_ABSTRACT_TAG 0x06
141 #define DD_BDD_XOR_EXIST_ABSTRACT_TAG 0x0a
142 #define DD_BDD_ITE_TAG 0x0e
143 #define DD_ADD_BDD_DO_INTERVAL_TAG 0x22
144 #define DD_BDD_CLIPPING_AND_ABSTRACT_UP_TAG 0x26
145 #define DD_BDD_CLIPPING_AND_ABSTRACT_DOWN_TAG 0x2a
146 #define DD_BDD_COMPOSE_RECUR_TAG 0x2e
147 #define DD_ADD_COMPOSE_RECUR_TAG 0x42
148 #define DD_ADD_NON_SIM_COMPOSE_TAG 0x46
149 #define DD_EQUIV_DC_TAG 0x4a
150 #define DD_ZDD_ITE_TAG 0x4e
151 #define DD_ADD_ITE_CONSTANT_TAG 0x62
152 #define DD_ADD_EVAL_CONST_TAG 0x66
153 #define DD_BDD_ITE_CONSTANT_TAG 0x6a
154 #define DD_ADD_OUT_SUM_TAG 0x6e
155 #define DD_BDD_LEQ_UNLESS_TAG 0x82
156 #define DD_ADD_TRIANGLE_TAG 0x86
157 #define DD_BDD_MAX_EXP_TAG 0x8a
158 #define DD_VARS_SYMM_BEFORE_TAG 0x8e
159 #define DD_VARS_SYMM_BETWEEN_TAG 0xa2
162 #define CUDD_GEN_CUBES 0
163 #define CUDD_GEN_PRIMES 1
164 #define CUDD_GEN_NODES 2
165 #define CUDD_GEN_ZDD_PATHS 3
166 #define CUDD_GEN_EMPTY 0
167 #define CUDD_GEN_NONEMPTY 1
176 #if SIZEOF_VOID_P == 8 && SIZEOF_INT == 4
177 #define CUDD_MAXINDEX (((DdHalfWord) ~0) >> 1)
179 #define CUDD_MAXINDEX ((DdHalfWord) ~0)
187 #define CUDD_CONST_INDEX CUDD_MAXINDEX
199 #define CUDD_CHECK_MASK 0x7ff
208 #if SIZEOF_VOID_P == 8 && SIZEOF_INT == 4
316 #ifdef DD_CACHE_PROFILE
327 unsigned int itemsize;
328 unsigned int keysize;
334 unsigned int maxslots;
372 #ifdef DD_CACHE_PROFILE
457 #ifndef DD_NO_DEATH_ROW
540 int totalNumberLinearTr;
543 #ifdef DD_UNIQUE_PROFILE
544 double uniqueLookUps;
548 double recursiveCalls;
555 int addPermuteRecurHits;
556 int bddPermuteRecurHits;
557 int bddVectorComposeHits;
558 int addVectorComposeHits;
559 int addGeneralVectorComposeHits;
560 int enableExtraDebug;
629 #define cuddDeallocNode(unique,node) \
630 (node)->next = (unique)->nextFree; \
631 (unique)->nextFree = node;
644 #define cuddDeallocMove(unique,node) \
645 ((DdNode *)(node))->ref = 0; \
646 ((DdNode *)(node))->next = (unique)->nextFree; \
647 (unique)->nextFree = (DdNode *)(node);
662 #define cuddRef(n) cuddSatInc(Cudd_Regular(n)->ref)
680 #define cuddDeref(n) cuddSatDec(Cudd_Regular(n)->ref)
696 #define Cudd_IsConstantInt(node) ((Cudd_Regular(node))->index == CUDD_CONST_INDEX)
711 #define cuddIsConstant(node) ((node)->index == CUDD_CONST_INDEX)
725 #define cuddT(node) ((node)->type.kids.T)
739 #define cuddE(node) ((node)->type.kids.E)
753 #define cuddV(node) ((node)->type.value)
769 #define cuddI(dd,index) (((index)==CUDD_CONST_INDEX)?(int)(index):(dd)->perm[(index)])
785 #define cuddIZ(dd,index) (((index)==CUDD_CONST_INDEX)?(int)(index):(dd)->permZ[(index)])
798 #if SIZEOF_VOID_P == 8 && SIZEOF_INT == 4
799 #define ddHash(f,g,s) \
800 ((((unsigned)(ptruint)(f) * DD_P1 + \
801 (unsigned)(ptruint)(g)) * DD_P2) >> (s))
803 #define ddHash(f,g,s) \
804 ((((unsigned)(f) * DD_P1 + (unsigned)(g)) * DD_P2) >> (s))
816 #if SIZEOF_VOID_P == 8 && SIZEOF_INT == 4
817 #define ddCHash(o,f,g,h,s) \
818 ((((((unsigned)(ptruint)(f) + (unsigned)(ptruint)(o)) * DD_P1 + \
819 (unsigned)(ptruint)(g)) * DD_P2 + \
820 (unsigned)(ptruint)(h)) * DD_P3) >> (s))
822 #define ddCHash(o,f,g,h,s) \
823 ((((((unsigned)(f) + (unsigned)(o)) * DD_P1 + (unsigned)(g)) * DD_P2 + \
824 (unsigned)(h)) * DD_P3) >> (s))
836 #if SIZEOF_VOID_P == 8 && SIZEOF_INT == 4
837 #define ddCHash2(o,f,g,s) \
838 (((((unsigned)(ptruint)(f) + (unsigned)(ptruint)(o)) * DD_P1 + \
839 (unsigned)(ptruint)(g)) * DD_P2) >> (s))
841 #define ddCHash2(o,f,g,s) \
842 (((((unsigned)(f) + (unsigned)(o)) * DD_P1 + (unsigned)(g)) * DD_P2) >> (s))
852 #define cuddClean(p) ((DdNode *)((ptruint)(p) & ~ (ptruint) 0xf))
863 #define ddMin(x,y) (((y) < (x)) ? (y) : (x))
874 #define ddMax(x,y) (((y) > (x)) ? (y) : (x))
883 #define ddAbs(x) (((x)<0) ? -(x) : (x))
893 #define ddEqualVal(x,y,e) (ddAbs((x)-(y))<(e))
907 #if SIZEOF_VOID_P == 8 && SIZEOF_INT == 4
908 #define cuddSatInc(x) ((x)++)
910 #define cuddSatInc(x) ((x) += (x) != (DdHalfWord)DD_MAXREF)
925 #if SIZEOF_VOID_P == 8 && SIZEOF_INT == 4
926 #define cuddSatDec(x) ((x)--)
928 #define cuddSatDec(x) ((x) -= (x) != (DdHalfWord)DD_MAXREF)
940 #define DD_ONE(dd) ((dd)->one)
954 #define DD_ZERO(dd) ((dd)->zero)
965 #define DD_PLUS_INFINITY(dd) ((dd)->plusinfinity)
976 #define DD_MINUS_INFINITY(dd) ((dd)->minusinfinity)
994 #define cuddAdjust(x)
996 #define cuddAdjust(x) ((x) = ((x) >= DD_CRI_HI_MARK) ? DD_PLUS_INF_VAL : (((x) <= DD_CRI_LO_MARK) ? DD_MINUS_INF_VAL : (x)))
1012 #define statLine(dd) \
1014 (dd)->recursiveCalls++; \
1015 if ((dd)->recursiveCalls == (dd)->nextSample) { \
1016 (void) fprintf((dd)->err, \
1017 "@%.0f: %u nodes %u live %.0f dropped" \
1018 " %.0f reclaimed\n", \
1019 (dd)->recursiveCalls, (dd)->keys, \
1020 (dd)->keys - (dd)->dead, \
1021 (dd)->nodesDropped, (dd)->reclaimed); \
1022 (dd)->nextSample += 250000;} \
1025 #define statLine(dd) (dd)->recursiveCalls++
1028 #define statLine(dd)
1035 #define checkWhetherToGiveUp(dd) \
1037 if (((int64_t) CUDD_CHECK_MASK & (int64_t) (dd)->cacheMisses) == 0) { \
1038 if ((dd)->terminationCallback != NULL && \
1039 (dd)->terminationCallback((dd)->tcbArg)) { \
1040 (dd)->errorCode = CUDD_TERMINATION; \
1043 if (util_cpu_time() - (dd)->startTime > (dd)->timeLimit) { \
1044 (dd)->errorCode = CUDD_TIMEOUT_EXPIRED; \
1131 #ifdef DD_CACHE_PROFILE
1183 extern DdManager *
cuddInitTable(
unsigned int numVars,
unsigned int numVarsZ,
unsigned int numSlots,
unsigned int looseUpTo);
The two children of a non-terminal node.
Definition: cuddInt.h:249
DdNode ** deathRow
Definition: cuddInt.h:454
Specialized DD symbol table.
Definition: cuddInt.h:395
Local cache.
Definition: cuddInt.h:321
int cuddHashTableInsert1(DdHashTable *hash, DdNode *f, DdNode *value, ptrint count)
Inserts an item in a hash table.
Definition: cuddLCache.c:737
void cuddReclaim(DdManager *table, DdNode *n)
Brings children of a dead node back.
Definition: cuddRef.c:540
DdHalfWord ref
Definition: cuddInt.h:259
DdNode * cuddAddIteRecur(DdManager *dd, DdNode *f, DdNode *g, DdNode *h)
Implements the recursive step of Cudd_addIte(f,g,h).
Definition: cuddAddIte.c:423
int cuddSymmSiftingConv(DdManager *table, int lower, int upper)
Symmetric sifting to convergence algorithm.
Definition: cuddSymmetry.c:401
void * tohArg
Definition: cuddInt.h:504
DdNode * cuddCProjectionRecur(DdManager *dd, DdNode *R, DdNode *Y, DdNode *Ysupp)
Performs the recursive step of Cudd_CProjection.
Definition: cuddPriority.c:1386
void cuddSetInteract(DdManager *table, int x, int y)
Set interaction matrix entries.
Definition: cuddInteract.c:133
int cuddZddTreeSifting(DdManager *table, Cudd_ReorderingType method)
Tree sifting algorithm for ZDDs.
Definition: cuddZddGroup.c:187
CUDD hook.
Definition: cuddInt.h:302
unsigned int looseUpTo
Definition: cuddInt.h:430
double cacheMisses
Definition: cuddInt.h:408
int cuddAnnealing(DdManager *table, int lower, int upper)
Get new variable-order by simulated annealing algorithm.
Definition: cuddAnneal.c:119
Reordering move record.
Definition: cuddInt.h:563
int cuddHashTableInsert2(DdHashTable *hash, DdNode *f, DdNode *g, DdNode *value, ptrint count)
Inserts an item in a hash table.
Definition: cuddLCache.c:933
DdChildren kids
Definition: cuddInt.h:263
Cudd_ReorderingType autoMethodZ
Definition: cuddInt.h:475
DdNode * cuddBddClippingAndAbstract(DdManager *dd, DdNode *f, DdNode *g, DdNode *cube, int maxDepth, int direction)
Approximates the conjunction of two BDDs f and g and simultaneously abstracts the variables in cube.
Definition: cuddClip.c:206
DdHook * postGCHook
Definition: cuddInt.h:492
int shift
Definition: cuddInt.h:378
DdNode * cuddBddComposeRecur(DdManager *dd, DdNode *f, DdNode *g, DdNode *proj)
Performs the recursive step of Cudd_bddCompose.
Definition: cuddCompose.c:825
void cuddClearDeathRow(DdManager *table)
Clears the death row.
Definition: cuddRef.c:675
int reordered
Definition: cuddInt.h:462
int cuddP(DdManager *dd, DdNode *f)
Prints a DD to the standard output. One line per node is printed.
Definition: cuddUtil.c:2944
int cuddZddP(DdManager *zdd, DdNode *f)
Prints a ZDD to the standard output. One line per node is printed.
Definition: cuddZddUtil.c:852
DdNode * cuddHashTableLookup3(DdHashTable *hash, DdNode *f, DdNode *g, DdNode *h)
Looks up a key consisting of three pointers in a hash table.
Definition: cuddLCache.c:1100
DdNode * plusinfinity
Definition: cuddInt.h:400
unsigned int cacheSlots
Definition: cuddInt.h:406
DdNode * cuddBddClosestCube(DdManager *dd, DdNode *f, DdNode *g, CUDD_VALUE_TYPE bound)
Performs the recursive step of Cudd_bddClosestCube.
Definition: cuddPriority.c:1612
void cuddCacheInsert1(DdManager *table, DD_CTFP1 op, DdNode *f, DdNode *data)
Inserts a result in the cache for a function with two operands.
Definition: cuddCache.c:272
unsigned int keys
Definition: cuddInt.h:380
Cudd_VariableType
Variable type.
Definition: cudd.h:180
DdHook * postReorderingHook
Definition: cuddInt.h:494
unsigned int keys
Definition: cuddInt.h:422
DdNode * cuddBddExistAbstractRecur(DdManager *manager, DdNode *f, DdNode *cube)
Performs the recursive steps of Cudd_bddExistAbstract.
Definition: cuddBddAbs.c:372
struct DdHashItem * next
Definition: cuddInt.h:339
DdNode * cuddHashTableLookup1(DdHashTable *hash, DdNode *f)
Looks up a key consisting of one pointer in a hash table.
Definition: cuddLCache.c:789
DdNode * cuddLocalCacheLookup(DdLocalCache *cache, DdNodePtr *key)
Looks up in a local cache.
Definition: cuddLCache.c:265
int cuddZddSymmCheck(DdManager *table, int x, int y)
Checks for symmetry of x and y.
Definition: cuddZddSymm.c:153
double totCachehits
Definition: cuddInt.h:512
int garbageCollections
Definition: cuddInt.h:509
DdSubtable constants
Definition: cuddInt.h:420
int cuddHashTableInsert3(DdHashTable *hash, DdNode *f, DdNode *g, DdNode *h, DdNode *value, ptrint count)
Inserts an item in a hash table.
Definition: cuddLCache.c:1044
unsigned int keysize
Definition: cuddInt.h:349
DdNode * cuddZddIsop(DdManager *dd, DdNode *L, DdNode *U, DdNode **zdd_I)
Performs the recursive step of Cudd_zddIsop.
Definition: cuddZddIsop.c:214
size_t maxmemhard
Definition: cuddInt.h:508
DdNode * cuddZddGetNodeIVO(DdManager *dd, int index, DdNode *g, DdNode *h)
Wrapper for cuddUniqueInterZdd that is independent of variable ordering.
Definition: cuddTable.c:1063
DdNode * minusinfinity
Definition: cuddInt.h:401
DdNode * cuddBddAndAbstractRecur(DdManager *manager, DdNode *f, DdNode *g, DdNode *cube)
Takes the AND of two BDDs and simultaneously abstracts the variables in cube.
Definition: cuddAndAbs.c:184
double minHit
Definition: cuddInt.h:410
double gcFrac
Definition: cuddInt.h:429
DdNode * zero
Definition: cuddInt.h:399
int32_t shuffleSelect
Definition: cuddInt.h:522
void cuddCacheFlush(DdManager *table)
Flushes the cache.
Definition: cuddCache.c:945
DdNode * cuddAddComposeRecur(DdManager *dd, DdNode *f, DdNode *g, DdNode *proj)
Performs the recursive step of Cudd_addCompose.
Definition: cuddCompose.c:928
unsigned int numBuckets
Definition: cuddInt.h:354
DdNode * g
Definition: cuddInt.h:365
void cuddLevelQueueDequeue(DdLevelQueue *queue, int level)
Remove an item from the front of a level queue.
Definition: cuddLevelQ.c:355
DdNode * cuddBddXorExistAbstractRecur(DdManager *manager, DdNode *f, DdNode *g, DdNode *cube)
Takes the exclusive OR of two BDDs and simultaneously abstracts the variables in cube.
Definition: cuddBddAbs.c:483
int cuddResizeLinear(DdManager *table)
Resizes the linear transform matrix.
Definition: cuddLinear.c:740
DdHashItem ** memoryList
Definition: cuddInt.h:353
int cuddZddSwapping(DdManager *table, int lower, int upper, Cudd_ReorderingType heuristic)
Reorders variables by a sequence of (non-adjacent) swaps.
Definition: cuddZddReord.c:687
void cuddSlowTableGrowth(DdManager *unique)
Adjusts parameters of a table to slow down its growth.
Definition: cuddTable.c:2451
int arcviolation
Definition: cuddInt.h:485
DdManager * cuddInitTable(unsigned int numVars, unsigned int numVarsZ, unsigned int numSlots, unsigned int looseUpTo)
Creates and initializes the unique table.
Definition: cuddTable.c:342
int cuddComputeFloorLog2(unsigned int value)
Returns the floor of the logarithm to the base 2.
Definition: cuddCache.c:973
unsigned long timeLimit
Definition: cuddInt.h:499
int cuddInitLinear(DdManager *table)
Initializes the linear transform matrix.
Definition: cuddLinear.c:699
unsigned int minDead
Definition: cuddInt.h:427
st_retval
Type of return values for iterators.
Definition: st.h:130
DdNode * cuddZddChange(DdManager *dd, DdNode *P, int var)
Substitutes a variable with its complement in a ZDD.
Definition: cuddZddSetop.c:896
unsigned int itemsize
Definition: cuddInt.h:350
void cuddRehash(DdManager *unique, int i)
Rehashes a unique subtable.
Definition: cuddTable.c:1595
int size
Definition: cuddInt.h:414
int symmviolation
Definition: cuddInt.h:484
int * invperm
Definition: cuddInt.h:439
FILE * err
Definition: cuddInt.h:496
unsigned int maxCacheHard
Definition: cuddInt.h:412
DdHashItem ** bucket
Definition: cuddInt.h:351
DdLocalCache * localCaches
Definition: cuddInt.h:489
Cudd_LazyGroupType
Group type for lazy sifting.
Definition: cudd.h:166
int cuddInsertSubtables(DdManager *unique, int n, int level)
Inserts n new subtables in a unique table at level.
Definition: cuddTable.c:1857
DdNode * cuddBddMakePrime(DdManager *dd, DdNode *cube, DdNode *f)
Performs the recursive step of Cudd_bddMakePrime.
Definition: cuddSat.c:963
Level queue.
Definition: cuddInt.h:591
DdNode * cuddZddWeakDivF(DdManager *dd, DdNode *f, DdNode *g)
Performs the recursive step of Cudd_zddWeakDivF.
Definition: cuddZddFuncs.c:879
CUDD generator.
Definition: cuddInt.h:270
DdNode * cuddAllocNode(DdManager *unique)
Fast storage allocation for DdNodes in the table.
Definition: cuddTable.c:225
multi-way tree node.
Definition: mtrInt.h:109
DdNode * cuddAddOrAbstractRecur(DdManager *manager, DdNode *f, DdNode *cube)
Performs the recursive step of Cudd_addOrAbstract.
Definition: cuddAddAbs.c:432
int cuddInitInteract(DdManager *table)
Initializes the interaction matrix.
Definition: cuddInteract.c:210
int cuddZddGetPosVarLevel(DdManager *dd, int index)
Returns the level of positive ZDD variable.
Definition: cuddZddFuncs.c:1530
DdNode * cuddCacheLookup(DdManager *table, ptruint op, DdNode *f, DdNode *g, DdNode *h)
Looks up in the cache for the result of op applied to f, g, and h.
Definition: cuddCache.c:312
int reordCycle
Definition: cuddInt.h:469
DdHook * preGCHook
Definition: cuddInt.h:491
int cuddZddGetCofactors3(DdManager *dd, DdNode *f, int v, DdNode **f1, DdNode **f0, DdNode **fd)
Computes the three-way decomposition of f w.r.t. v.
Definition: cuddZddFuncs.c:1313
void cuddLocalCacheInsert(DdLocalCache *cache, DdNodePtr *key, DdNode *value)
Inserts a result in a local cache.
Definition: cuddLCache.c:236
int * perm
Definition: cuddInt.h:437
void cuddLocalCacheClearDead(DdManager *manager)
Clears the dead entries of the local caches of a manager.
Definition: cuddLCache.c:308
intptr_t ptrint
Signed integer that is the size of a pointer.
Definition: cuddInt.h:220
DdNode * cuddRemapUnderApprox(DdManager *dd, DdNode *f, int numVars, int threshold, double quality)
Applies the remapping underappoximation algorithm.
Definition: cuddApprox.c:582
int cuddIsInDeathRow(DdManager *dd, DdNode *f)
Checks whether a node is in the death row.
Definition: cuddRef.c:709
int linearSize
Definition: cuddInt.h:446
DdNode * cuddZddComplement(DdManager *dd, DdNode *node)
Computes a complement of a ZDD node.
Definition: cuddZddFuncs.c:1467
DdNode * cuddAddExistAbstractRecur(DdManager *manager, DdNode *f, DdNode *cube)
Performs the recursive step of Cudd_addExistAbstract.
Definition: cuddAddAbs.c:223
Decision diagram node.
Definition: cuddInt.h:257
unsigned int maxReorderings
Definition: cuddInt.h:464
int32_t cuddRand2
Definition: cuddInt.h:521
int cuddZddAlignToBdd(DdManager *table)
Reorders ZDD variables according to the order of the BDD variables.
Definition: cuddZddReord.c:304
DdNode * cuddSplitSetRecur(DdManager *manager, st_table *mtable, int *varSeen, DdNode *p, double n, double max, int index)
Implements the recursive step of Cudd_SplitSet.
Definition: cuddSplit.c:224
char * stash
Definition: cuddInt.h:452
double maxGrowth
Definition: cuddInt.h:470
DdSubtable * subtableZ
Definition: cuddInt.h:419
DdNode * cuddZddGetNode(DdManager *zdd, int id, DdNode *T, DdNode *E)
Wrapper for cuddUniqueInterZdd.
Definition: cuddTable.c:1029
Cudd_ReorderingType autoMethod
Definition: cuddInt.h:474
Cudd_ErrorType
Type of error codes.
Definition: cudd.h:151
int bindVar
Definition: cuddInt.h:384
Multiway-branch tree manipulation.
DdNode * cuddZddIte(DdManager *dd, DdNode *f, DdNode *g, DdNode *h)
Performs the recursive step of Cudd_zddIte.
Definition: cuddZddSetop.c:376
DdNode * cuddAddUnivAbstractRecur(DdManager *manager, DdNode *f, DdNode *cube)
Performs the recursive step of Cudd_addUnivAbstract.
Definition: cuddAddAbs.c:326
int deathRowDepth
Definition: cuddInt.h:455
DdNode * nextFree
Definition: cuddInt.h:451
Cudd_AggregationType
Type of aggregation methods.
Definition: cudd.h:123
int cuddSifting(DdManager *table, int lower, int upper)
Implementation of Rudell's sifting algorithm.
Definition: cuddReorder.c:457
DdNode * cuddZddDiff(DdManager *zdd, DdNode *P, DdNode *Q)
Performs the recursive step of Cudd_zddDiff.
Definition: cuddZddSetop.c:651
Cudd_LazyGroupType varToBeGrouped
Definition: cuddInt.h:389
ptrint count
Definition: cuddInt.h:340
void * tcbArg
Definition: cuddInt.h:501
DdLevelQueue * cuddLevelQueueInit(int levels, int itemSize, int numBuckets, DdManager *manager)
Initializes a level queue.
Definition: cuddLevelQ.c:143
void * hooks
Definition: cuddInt.h:490
Cudd_AggregationType groupcheck
Definition: cuddInt.h:482
int sizeZ
Definition: cuddInt.h:415
DdNode * cuddUniqueInterZdd(DdManager *unique, int index, DdNode *T, DdNode *E)
Checks the unique table for the existence of an internal ZDD node.
Definition: cuddTable.c:1374
int(* DD_THFP)(const void *)
Type of termination handler.
Definition: cudd.h:266
DdNode ** vars
Definition: cuddInt.h:441
DdHook * preReorderingHook
Definition: cuddInt.h:493
unsigned long startTime
Definition: cuddInt.h:498
uintptr_t ptruint
Unsigned integer that is the size of a pointer.
Definition: cuddInt.h:227
int cuddInitCache(DdManager *unique, unsigned int cacheSize, unsigned int maxCacheSize)
Initializes the computed table.
Definition: cuddCache.c:107
DdNode * cuddBddIntersectRecur(DdManager *dd, DdNode *f, DdNode *g)
Implements the recursive step of Cudd_bddIntersect.
Definition: cuddBddIte.c:853
int cuddWindowReorder(DdManager *table, int low, int high, Cudd_ReorderingType submethod)
Reorders by applying the method of the sliding window.
Definition: cuddWindow.c:109
void cuddLevelQueueQuit(DdLevelQueue *queue)
Shuts down a level queue.
Definition: cuddLevelQ.c:197
DD_HFP f
Definition: cuddInt.h:303
struct DdHook * next
Definition: cuddInt.h:304
DdSubtable * subtables
Definition: cuddInt.h:418
unsigned int initSlots
Definition: cuddInt.h:432
int recomb
Definition: cuddInt.h:483
double cacheLastInserts
Definition: cuddInt.h:516
DdNode * next
Definition: cuddInt.h:260
DdNodePtr * cuddNodeArray(DdNode *f, int *n)
Recursively collects all the nodes of a DD in an array.
Definition: cuddUtil.c:3055
unsigned int nextDyn
Definition: cuddInt.h:478
DdNode * cuddSubsetShortPaths(DdManager *dd, DdNode *f, int numVars, int threshold, int hardlimit)
The outermost procedure to return a subset of the given BDD with the shortest path lengths.
Definition: cuddSubsetSP.c:274
DdNode * cuddBddLiteralSetIntersectionRecur(DdManager *dd, DdNode *f, DdNode *g)
Performs the recursive step of Cudd_bddLiteralSetIntersection.
Definition: cuddLiteral.c:138
DdNode * cuddZddDivide(DdManager *dd, DdNode *f, DdNode *g)
Performs the recursive step of Cudd_zddDivide.
Definition: cuddZddFuncs.c:1114
int cacheShift
Definition: cuddInt.h:407
DdNode * cuddBddIteRecur(DdManager *dd, DdNode *f, DdNode *g, DdNode *h)
Implements the recursive step of Cudd_bddIte.
Definition: cuddBddIte.c:716
double allocated
Definition: cuddInt.h:434
DdCache * cache
Definition: cuddInt.h:405
void cuddCacheResize(DdManager *table)
Resizes the cache.
Definition: cuddCache.c:835
void cuddUpdateInteractionMatrix(DdManager *table, int xindex, int yindex)
Updates the interaction matrix.
Definition: cuddLinear.c:662
DdNode * cuddAddConstrainRecur(DdManager *dd, DdNode *f, DdNode *c)
Performs the recursive step of Cudd_addConstrain.
Definition: cuddGenCof.c:1212
DdNode ** stack
Definition: cuddInt.h:433
int varHandled
Definition: cuddInt.h:388
int zddTotalNumberSwapping
Definition: cuddInt.h:468
unsigned int maxLive
Definition: cuddInt.h:426
DdNode * cuddCacheLookup1Zdd(DdManager *table, DD_CTFP1 op, DdNode *f)
Looks up in the cache for the result of op applied to f.
Definition: cuddCache.c:588
DdNode * cuddZddUnateProduct(DdManager *dd, DdNode *f, DdNode *g)
Performs the recursive step of Cudd_zddUnateProduct.
Definition: cuddZddFuncs.c:579
unsigned int originalSize
Definition: cuddInt.h:445
unsigned int dead
Definition: cuddInt.h:382
DdNode * cuddSolveEqnRecur(DdManager *bdd, DdNode *F, DdNode *Y, DdNode **G, int n, int *yIndex, int i)
Implements the recursive step of Cudd_SolveEqn.
Definition: cuddSolve.c:189
int32_t cuddRand
Definition: cuddInt.h:520
int * invpermZ
Definition: cuddInt.h:440
DdNode * cuddZddUnion(DdManager *zdd, DdNode *P, DdNode *Q)
Performs the recursive step of Cudd_zddUnion.
Definition: cuddZddSetop.c:497
int ddTotalNumberSwapping
Definition: cuddInt.h:467
int cuddTestInteract(DdManager *table, int x, int y)
Test interaction matrix entries.
Definition: cuddInteract.c:165
int populationSize
Definition: cuddInt.h:486
DdNode * cuddZddSubset1(DdManager *dd, DdNode *P, int var)
Computes the positive cofactor of a ZDD w.r.t. a variable.
Definition: cuddZddSetop.c:802
DdNode * cuddZddProduct(DdManager *dd, DdNode *f, DdNode *g)
Performs the recursive step of Cudd_zddProduct.
Definition: cuddZddFuncs.c:344
unsigned int isolated
Definition: cuddInt.h:444
DdNode * cuddAddMonadicApplyRecur(DdManager *dd, DD_MAOP op, DdNode *f)
Performs the recursive step of Cudd_addMonadicApply.
Definition: cuddAddApply.c:837
void cuddPrintVarGroups(DdManager *dd, MtrNode *root, int zdd, int silent)
Prints the variable groups as a parenthesized list.
Definition: cuddCheck.c:700
CUDD_VALUE_TYPE epsilon
Definition: cuddInt.h:460
int cuddZddSymmSifting(DdManager *table, int lower, int upper)
Symmetric sifting algorithm for ZDDs.
Definition: cuddZddSymm.c:256
DdCache * acache
Definition: cuddInt.h:404
int cuddZddNextHigh(DdManager *table, int x)
Finds the next subtable with a larger index.
Definition: cuddZddReord.c:360
int cuddExact(DdManager *table, int lower, int upper)
Exact variable ordering algorithm.
Definition: cuddExact.c:114
DdNode ** memoryList
Definition: cuddInt.h:450
DdNode * cuddBddIsop(DdManager *dd, DdNode *L, DdNode *U)
Performs the recursive step of Cudd_bddIsop.
Definition: cuddZddIsop.c:552
unsigned int slots
Definition: cuddInt.h:421
Cudd_VariableType varType
Definition: cuddInt.h:386
Generic local cache item.
Definition: cuddInt.h:310
int cuddCollectNodes(DdNode *f, st_table *visited)
Recursively collects all the nodes of a DD in a symbol table.
Definition: cuddUtil.c:3000
DdHalfWord index
Definition: cuddInt.h:258
int cuddZddLinearSifting(DdManager *table, int lower, int upper)
Implementation of the linear sifting algorithm for ZDDs.
Definition: cuddZddLin.c:125
int cuddTreeSifting(DdManager *table, Cudd_ReorderingType method)
Tree sifting algorithm.
Definition: cuddGroup.c:205
unsigned int dead
Definition: cuddInt.h:424
void cuddReclaimZdd(DdManager *table, DdNode *n)
Brings children of a dead ZDD node back.
Definition: cuddRef.c:591
uint32_t DdHalfWord
Type that is half the size of a pointer.
Definition: cuddInt.h:205
double cachecollisions
Definition: cuddInt.h:514
DdNode * cuddAddApplyRecur(DdManager *dd, DD_AOP op, DdNode *f, DdNode *g)
Performs the recursive step of Cudd_addApply.
Definition: cuddAddApply.c:753
unsigned int maxKeys
Definition: cuddInt.h:381
DdNode * cuddBiasedUnderApprox(DdManager *dd, DdNode *f, DdNode *b, int numVars, int threshold, double quality1, double quality0)
Applies the biased remapping underappoximation algorithm.
Definition: cuddApprox.c:671
int numberXovers
Definition: cuddInt.h:487
DdHashItem * nextFree
Definition: cuddInt.h:352
int cuddResizeTableZdd(DdManager *unique, int index)
Increases the number of ZDD subtables in a unique table so that it meets or exceeds index.
Definition: cuddTable.c:2309
DdNode * cuddAddRestrictRecur(DdManager *dd, DdNode *f, DdNode *c)
Performs the recursive step of Cudd_addRestrict.
Definition: cuddGenCof.c:1316
void cuddShrinkDeathRow(DdManager *table)
Shrinks the death row.
Definition: cuddRef.c:640
DdLocalCache * cuddLocalCacheInit(DdManager *manager, unsigned int keySize, unsigned int cacheSize, unsigned int maxCacheSize)
Initializes a local computed table.
Definition: cuddLCache.c:157
DdManager * manager
Definition: cuddInt.h:358
int cuddLinearAndSifting(DdManager *table, int lower, int upper)
BDD reduction based on combination of sifting and linear transformations.
Definition: cuddLinear.c:193
unsigned int size
Definition: cuddInt.h:356
struct DdNode * E
Definition: cuddInt.h:251
ptruint h
Definition: cuddInt.h:366
int cuddLinearInPlace(DdManager *table, int x, int y)
Linearly combines two adjacent variables.
Definition: cuddLinear.c:308
Subtable for one index.
Definition: cuddInt.h:376
DdNode * cuddAddBddDoPattern(DdManager *dd, DdNode *f)
Performs the recursive step for Cudd_addBddPattern.
Definition: cuddBridge.c:462
int cuddSymmSifting(DdManager *table, int lower, int upper)
Symmetric sifting algorithm.
Definition: cuddSymmetry.c:284
int cuddZddGetCofactors2(DdManager *dd, DdNode *f, int v, DdNode **f1, DdNode **f0)
Computes the two-way decomposition of f w.r.t. v.
Definition: cuddZddFuncs.c:1437
DdNode * cuddVerifySol(DdManager *bdd, DdNode *F, DdNode **G, int *yIndex, int n)
Implements the recursive step of Cudd_VerifySol.
Definition: cuddSolve.c:312
DdNode * cuddBddNPAndRecur(DdManager *manager, DdNode *f, DdNode *g)
Implements the recursive step of Cudd_bddAnd.
Definition: cuddGenCof.c:1070
void cuddGetBranches(DdNode *g, DdNode **g1, DdNode **g0)
Computes the children of g.
Definition: cuddCof.c:225
int cuddZddInitUniv(DdManager *zdd)
Initializes the ZDD universe.
Definition: cuddInit.c:221
DdNode * data
Definition: cuddInt.h:367
double cachedeletions
Definition: cuddInt.h:517
DD_THFP terminationCallback
Definition: cuddInt.h:500
unsigned int maxsize
Definition: cuddInt.h:357
DdNode * cuddBddTransfer(DdManager *ddS, DdManager *ddD, DdNode *f)
Convert a BDD from a manager to another one.
Definition: cuddBridge.c:415
DdNode * cuddAddCmplRecur(DdManager *dd, DdNode *f)
Performs the recursive step of Cudd_addCmpl.
Definition: cuddAddIte.c:541
void cuddCacheInsert2(DdManager *table, DD_CTFP op, DdNode *f, DdNode *g, DdNode *data)
Inserts a result in the cache for a function with two operands.
Definition: cuddCache.c:233
double cacheinserts
Definition: cuddInt.h:515
void * cuddHashTableGenericLookup(DdHashTable *hash, DdNode *f)
Looks up a key consisting of one pointer in a hash table.
Definition: cuddLCache.c:893
int cuddZddGetNegVarLevel(DdManager *dd, int index)
Returns the level of negative ZDD variable.
Definition: cuddZddFuncs.c:1543
DdNode ** nodelist
Definition: cuddInt.h:377
DD_TOHFP timeoutHandler
Definition: cuddInt.h:503
DdNode * cuddBddClippingAnd(DdManager *dd, DdNode *f, DdNode *g, int maxDepth, int direction)
Approximates the conjunction of two BDDs f and g.
Definition: cuddClip.c:177
void cuddLocalCacheClearAll(DdManager *manager)
Clears the local caches of a manager.
Definition: cuddLCache.c:356
DdNode * cuddHashTableLookup(DdHashTable *hash, DdNodePtr *key)
Looks up a key in a hash table.
Definition: cuddLCache.c:673
ptruint * linear
Definition: cuddInt.h:448
int cuddZddSifting(DdManager *table, int lower, int upper)
Implementation of Rudell's sifting algorithm.
Definition: cuddZddReord.c:805
unsigned int countDead
Definition: cuddInt.h:479
DdNode * cuddAddRoundOffRecur(DdManager *dd, DdNode *f, double trunc)
Implements the recursive step of Cudd_addRoundOff.
Definition: cuddAddNeg.c:222
int siftMaxVar
Definition: cuddInt.h:465
The University of Colorado extended double precision package.
int cuddTimesInDeathRow(DdManager *dd, DdNode *f)
Counts how many times a node is in the death row.
Definition: cuddRef.c:737
MtrNode * tree
Definition: cuddInt.h:480
int cuddGa(DdManager *table, int lower, int upper)
Genetic algorithm for DD reordering.
Definition: cuddGenetic.c:165
unsigned int randomizeOrder
Definition: cuddInt.h:488
DdNode * cuddCofactorRecur(DdManager *dd, DdNode *f, DdNode *g)
Performs the recursive step of Cudd_Cofactor.
Definition: cuddCof.c:253
DdNode * cuddAddNegateRecur(DdManager *dd, DdNode *f)
Implements the recursive step of Cudd_addNegate.
Definition: cuddAddNeg.c:162
DdNode * cuddUniqueConst(DdManager *unique, CUDD_VALUE_TYPE value)
Checks the unique table for the existence of a constant node.
Definition: cuddTable.c:1509
DdNode * cuddCacheLookup2(DdManager *table, DD_CTFP op, DdNode *f, DdNode *g)
Looks up in the cache for the result of op applied to f and g.
Definition: cuddCache.c:432
int cuddHeapProfile(DdManager *dd)
Prints information about the heap.
Definition: cuddCheck.c:610
DdNode * cuddDynamicAllocNode(DdManager *table)
Dynamically allocates a Node.
Definition: cuddReorder.c:361
int(* DD_HFP)(DdManager *, const char *, void *)
Type of hook function.
Definition: cudd.h:234
void * cuddLevelQueueEnqueue(DdLevelQueue *queue, void *key, int level)
Inserts a new key in a level queue.
Definition: cuddLevelQ.c:234
DdNode * cuddBddRestrictRecur(DdManager *dd, DdNode *f, DdNode *c)
Performs the recursive step of Cudd_bddRestrict.
Definition: cuddGenCof.c:920
DdNode * cuddSubsetHeavyBranch(DdManager *dd, DdNode *f, int numVars, int threshold)
The main procedure that returns a subset by choosing the heavier branch in the BDD.
Definition: cuddSubsetHB.c:278
int autoDynZ
Definition: cuddInt.h:473
int cuddZddGetNegVarIndex(DdManager *dd, int index)
Returns the index of negative ZDD variable.
Definition: cuddZddFuncs.c:1516
void cuddCacheInsert(DdManager *table, ptruint op, DdNode *f, DdNode *g, DdNode *h, DdNode *data)
Inserts a result in the cache for a function with three operands.
Definition: cuddCache.c:190
int cuddSymmCheck(DdManager *table, int x, int y)
Checks for symmetry of x and y.
Definition: cuddSymmetry.c:155
void(* DD_OOMFP)(size_t)
Type of memory-out function.
Definition: cudd.h:258
double CUDD_VALUE_TYPE
Type of the value of a terminal node.
Definition: cudd.h:189
double cacheHits
Definition: cuddInt.h:409
DdNode * cuddCacheLookup2Zdd(DdManager *table, DD_CTFP op, DdNode *f, DdNode *g)
Looks up in the cache for the result of op applied to f and g.
Definition: cuddCache.c:536
DdNode sentinel
Definition: cuddInt.h:397
DdNode * cuddMakeBddFromZddCover(DdManager *dd, DdNode *node)
Converts a ZDD cover to a BDD.
Definition: cuddZddIsop.c:775
int cuddSwapping(DdManager *table, int lower, int upper, Cudd_ReorderingType heuristic)
Reorders variables by a sequence of (non-adjacent) swaps.
Definition: cuddReorder.c:556
unsigned int peakLiveNodes
Definition: cuddInt.h:518
unsigned int next
Definition: cuddInt.h:383
DdNode * background
Definition: cuddInt.h:402
CUDD_VALUE_TYPE value
Definition: cuddInt.h:262
size_t maxmem
Definition: cuddInt.h:507
int realignZ
Definition: cuddInt.h:477
int cuddZddNextLow(DdManager *table, int x)
Finds the next subtable with a smaller index.
Definition: cuddZddReord.c:379
int cuddNextHigh(DdManager *table, int x)
Finds the next subtable with a larger index.
Definition: cuddReorder.c:665
DdNode ** univ
Definition: cuddInt.h:443
int * map
Definition: cuddInt.h:442
DdNode * cuddUniqueInterIVO(DdManager *unique, int index, DdNode *T, DdNode *E)
Wrapper for cuddUniqueInter that is independent of variable ordering.
Definition: cuddTable.c:1334
enum st_retval cuddStCountfree(void *key, void *value, void *arg)
Frees the memory used to store the minterm counts recorded in the visited table.
Definition: cuddUtil.c:2971
int cuddZddUniqueCompare(void const *ptr_x, void const *ptr_y)
Comparison function used by qsort.
Definition: cuddZddReord.c:402
DdNode * cuddCacheLookup1(DdManager *table, DD_CTFP1 op, DdNode *f)
Looks up in the cache for the result of op applied to f.
Definition: cuddCache.c:484
Cudd_ReorderingType
Type of reordering algorithm.
Definition: cudd.h:94
unsigned deadMask
Definition: cuddInt.h:457
DD_OOMFP outOfMemCallback
Definition: cuddInt.h:502
DdNode * key[1]
Definition: cuddInt.h:342
double totCacheMisses
Definition: cuddInt.h:513
int cuddGarbageCollect(DdManager *unique, int clearCache)
Performs garbage collection on the BDD and ZDD unique tables.
Definition: cuddTable.c:736
DdNode * cuddBddLICompaction(DdManager *dd, DdNode *f, DdNode *c)
Performs safe minimization of a BDD.
Definition: cuddGenCof.c:1443
void cuddLocalCacheQuit(DdLocalCache *cache)
Shuts down a local computed table.
Definition: cuddLCache.c:215
void cuddPrintNode(DdNode *f, FILE *fp)
Prints out information on a node.
Definition: cuddCheck.c:671
unsigned int keysZ
Definition: cuddInt.h:423
int cuddNextLow(DdManager *table, int x)
Finds the next subtable with a smaller index.
Definition: cuddReorder.c:686
DdNode * cuddBddAndRecur(DdManager *manager, DdNode *f, DdNode *g)
Implements the recursive step of Cudd_bddAnd.
Definition: cuddBddIte.c:970
unsigned int reorderings
Definition: cuddInt.h:463
int cuddHashTableInsert(DdHashTable *hash, DdNodePtr *key, DdNode *value, ptrint count)
Inserts an item in a hash table.
Definition: cuddLCache.c:617
void(* DD_TOHFP)(DdManager *, void *)
Type of timeout handler.
Definition: cudd.h:270
DdNode * cuddZddIntersect(DdManager *zdd, DdNode *P, DdNode *Q)
Performs the recursive step of Cudd_zddIntersect.
Definition: cuddZddSetop.c:581
int gcEnabled
Definition: cuddInt.h:428
DdNode * cuddZddDivideF(DdManager *dd, DdNode *f, DdNode *g)
Performs the recursive step of Cudd_zddDivideF.
Definition: cuddZddFuncs.c:1211
Local hash table item.
Definition: cuddInt.h:338
#define STAB_SIZE
Size of the random number generator shuffle table.
Definition: cuddInt.h:188
void * cuddLevelQueueFirst(DdLevelQueue *queue, void *key, int level)
Inserts the first key in a level queue.
Definition: cuddLevelQ.c:304
DdNode * cuddBddXorRecur(DdManager *manager, DdNode *f, DdNode *g)
Implements the recursive step of Cudd_bddXor.
Definition: cuddBddIte.c:1100
unsigned long reordTime
Definition: cuddInt.h:511
ptruint * interact
Definition: cuddInt.h:447
unsigned int slots
Definition: cuddInt.h:379
int cuddCacheProfile(DdManager *table, FILE *fp)
Computes and prints a profile of the cache usage.
Definition: cuddCache.c:700
FILE * out
Definition: cuddInt.h:495
int32_t shuffleTable[64]
Definition: cuddInt.h:523
int cuddBddAlignToZdd(DdManager *table)
Reorders BDD variables according to the order of the ZDD variables.
Definition: cuddReorder.c:1195
int pairIndex
Definition: cuddInt.h:387
double maxGrowthAlt
Definition: cuddInt.h:471
unsigned int deadZ
Definition: cuddInt.h:425
double reclaimed
Definition: cuddInt.h:436
DdNode * cuddZddWeakDiv(DdManager *dd, DdNode *f, DdNode *g)
Performs the recursive step of Cudd_zddWeakDiv.
Definition: cuddZddFuncs.c:721
void cuddZddFreeUniv(DdManager *zdd)
Frees the ZDD universe.
Definition: cuddInit.c:267
int cuddZddSymmSiftingConv(DdManager *table, int lower, int upper)
Symmetric sifting to convergence algorithm for ZDDs.
Definition: cuddZddSymm.c:376
int cuddZddGetPosVarIndex(DdManager *dd, int index)
Returns the index of positive ZDD variable.
Definition: cuddZddFuncs.c:1502
int realign
Definition: cuddInt.h:476
int autoDyn
Definition: cuddInt.h:472
DdNode * cuddZddSubset0(DdManager *dd, DdNode *P, int var)
Computes the negative cofactor of a ZDD w.r.t. a variable.
Definition: cuddZddSetop.c:850
int cuddZddSwapInPlace(DdManager *table, int x, int y)
Swaps two adjacent variables.
Definition: cuddZddReord.c:426
int maxSize
Definition: cuddInt.h:416
int cuddSwapInPlace(DdManager *table, int x, int y)
Swaps two adjacent variables.
Definition: cuddReorder.c:709
DdNode * cuddCacheLookupZdd(DdManager *table, ptruint op, DdNode *f, DdNode *g, DdNode *h)
Looks up in the cache for the result of op applied to f, g, and h.
Definition: cuddCache.c:372
int nextDead
Definition: cuddInt.h:456
Generic level queue item.
Definition: cuddInt.h:582
struct DdNode * T
Definition: cuddInt.h:250
unsigned long GCTime
Definition: cuddInt.h:510
DdNode * value
Definition: cuddInt.h:341
void cuddShrinkSubtable(DdManager *unique, int i)
Shrinks a subtable.
Definition: cuddTable.c:1764
void cuddHashTableQuit(DdHashTable *hash)
Shuts down a hash table.
Definition: cuddLCache.c:538
DdNode * one
Definition: cuddInt.h:398
void cuddFreeTable(DdManager *unique)
Frees the resources associated to a unique table.
Definition: cuddTable.c:668
Computed table.
Definition: cuddInt.h:364
DdNode * cuddConstantLookup(DdManager *table, ptruint op, DdNode *f, DdNode *g, DdNode *h)
Looks up in the cache for the result of op applied to f, g, and h.
Definition: cuddCache.c:645
Used to sort variables for reordering.
Definition: cuddInt.h:574
int cuddDestroySubtables(DdManager *unique, int n)
Destroys the n most recently created subtables in a unique table.
Definition: cuddTable.c:2176
int * permZ
Definition: cuddInt.h:438
DdNode * cuddBddConstrainRecur(DdManager *dd, DdNode *f, DdNode *c)
Performs the recursive step of Cudd_bddConstrain.
Definition: cuddGenCof.c:791
MtrNode * treeZ
Definition: cuddInt.h:481
Symbol table header.
Definition: st.c:101
Local hash table.
Definition: cuddInt.h:348
DdNode * cuddBddBooleanDiffRecur(DdManager *manager, DdNode *f, DdNode *var)
Performs the recursive steps of Cudd_bddBoleanDiff.
Definition: cuddBddAbs.c:655
Cudd_ErrorType errorCode
Definition: cuddInt.h:497
DdHashTable * cuddHashTableInit(DdManager *manager, unsigned int keySize, unsigned int initSize)
Initializes a hash table.
Definition: cuddLCache.c:489
void cuddHashTableGenericQuit(DdHashTable *hash)
Shuts down a hash table.
Definition: cuddLCache.c:582
int cacheSlack
Definition: cuddInt.h:411
int maxSizeZ
Definition: cuddInt.h:417
DdNode * cuddZddChangeAux(DdManager *zdd, DdNode *P, DdNode *zvar)
Performs the recursive step of Cudd_zddChange.
Definition: cuddZddSetop.c:728
The University of Colorado decision diagram package.
size_t memused
Definition: cuddInt.h:506
DdNode * cuddHashTableLookup2(DdHashTable *hash, DdNode *f, DdNode *g)
Looks up a key consisting of two pointers in a hash table.
Definition: cuddLCache.c:987
DdNode * cuddAddScalarInverseRecur(DdManager *dd, DdNode *f, DdNode *epsilon)
Performs the recursive step of addScalarInverse.
Definition: cuddAddInv.c:139
int shift
Definition: cuddInt.h:355
int cuddHashTableGenericInsert(DdHashTable *hash, DdNode *f, void *value)
Inserts a generic item in a hash table.
Definition: cuddLCache.c:846
int siftMaxSwap
Definition: cuddInt.h:466
DdNode * cuddUniqueInter(DdManager *unique, int index, DdNode *T, DdNode *E)
Checks the unique table for the existence of an internal node.
Definition: cuddTable.c:1118
DdNode * cuddUnderApprox(DdManager *dd, DdNode *f, int numVars, int threshold, int safe, double quality)
Applies Tom Shiple's underappoximation algorithm.
Definition: cuddApprox.c:493