diff options
Diffstat (limited to 'src/bdd/cudd/cuddInt.h')
| -rw-r--r-- | src/bdd/cudd/cuddInt.h | 825 |
1 files changed, 442 insertions, 383 deletions
diff --git a/src/bdd/cudd/cuddInt.h b/src/bdd/cudd/cuddInt.h index ca24a8aa..09892ba5 100644 --- a/src/bdd/cudd/cuddInt.h +++ b/src/bdd/cudd/cuddInt.h @@ -12,12 +12,39 @@ 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.] + Copyright [Copyright (c) 1995-2004, Regents of the University of Colorado - Revision [$Id: cuddInt.h,v 1.1.1.1 2003/02/24 22:23:52 wjiang Exp $] + All rights reserved. + + Redistribution and use in source and binary forms, with or without + modification, are permitted provided that the following conditions + are met: + + Redistributions of source code must retain the above copyright + notice, this list of conditions and the following disclaimer. + + Redistributions in binary form must reproduce the above copyright + notice, this list of conditions and the following disclaimer in the + documentation and/or other materials provided with the distribution. + + Neither the name of the University of Colorado nor the names of its + contributors may be used to endorse or promote products derived from + this software without specific prior written permission. + + THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS + "AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT + LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS + FOR A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE + COPYRIGHT OWNER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, + INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, + BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; + LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER + CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT + LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN + ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE + POSSIBILITY OF SUCH DAMAGE.] + + Revision [$Id: cuddInt.h,v 1.139 2009/03/08 02:49:02 fabio Exp $] ******************************************************************************/ @@ -25,7 +52,6 @@ #define _CUDDINT - /*---------------------------------------------------------------------------*/ /* Nested includes */ /*---------------------------------------------------------------------------*/ @@ -71,65 +97,65 @@ ABC_NAMESPACE_HEADER_START /* Constant declarations */ /*---------------------------------------------------------------------------*/ -#define DD_MAXREF ((DdHalfWord) ~0) +#define DD_MAXREF ((DdHalfWord) ~0) -#define DD_DEFAULT_RESIZE 10 /* how many extra variables */ - /* should be added when resizing */ -#define DD_MEM_CHUNK 1022 +#define DD_DEFAULT_RESIZE 10 /* how many extra variables */ + /* should be added when resizing */ +#define DD_MEM_CHUNK 1022 /* These definitions work for CUDD_VALUE_TYPE == double */ -#define DD_ONE_VAL (1.0) -#define DD_ZERO_VAL (0.0) -#define DD_EPSILON (1.0e-12) +#define DD_ONE_VAL (1.0) +#define DD_ZERO_VAL (0.0) +#define DD_EPSILON (1.0e-12) /* The definitions of +/- infinity in terms of HUGE_VAL work on ** the DECstations and on many other combinations of OS/compiler. */ #ifdef HAVE_IEEE_754 -# define DD_PLUS_INF_VAL (HUGE_VAL) +# define DD_PLUS_INF_VAL (HUGE_VAL) #else -# define DD_PLUS_INF_VAL (10e301) -# define DD_CRI_HI_MARK (10e150) -# define DD_CRI_LO_MARK (-(DD_CRI_HI_MARK)) +# define DD_PLUS_INF_VAL (10e301) +# define DD_CRI_HI_MARK (10e150) +# define DD_CRI_LO_MARK (-(DD_CRI_HI_MARK)) #endif -#define DD_MINUS_INF_VAL (-(DD_PLUS_INF_VAL)) +#define DD_MINUS_INF_VAL (-(DD_PLUS_INF_VAL)) -#define DD_NON_CONSTANT ((DdNode *) 1) /* for Cudd_bddIteConstant */ +#define DD_NON_CONSTANT ((DdNode *) 1) /* for Cudd_bddIteConstant */ /* Unique table and cache management constants. */ -#define DD_MAX_SUBTABLE_DENSITY 4 /* tells when to resize a subtable */ +#define DD_MAX_SUBTABLE_DENSITY 4 /* tells when to resize a subtable */ /* gc when this percent are dead (measured w.r.t. slots, not keys) ** The first limit (LO) applies normally. The second limit applies when ** the package believes more space for the unique table (i.e., more dead ** nodes) would improve performance, and the unique table is not already ** too large. The third limit applies when memory is low. */ -#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 /* resize cache when hit ratio - above this percentage (default) */ -#define DD_MAX_LOOSE_FRACTION 5 /* 1 / (max fraction of memory used for - unique table in fast growth mode) */ -#define DD_MAX_CACHE_FRACTION 3 /* 1 / (max fraction of memory used for - computed table if resizing enabled) */ -#define DD_STASH_FRACTION 64 /* 1 / (fraction of memory set - aside for emergencies) */ +#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 /* resize cache when hit ratio + above this percentage (default) */ +#define DD_MAX_LOOSE_FRACTION 5 /* 1 / (max fraction of memory used for + unique table in fast growth mode) */ +#define DD_MAX_CACHE_FRACTION 3 /* 1 / (max fraction of memory used for + computed table if resizing enabled) */ +#define DD_STASH_FRACTION 64 /* 1 / (fraction of memory set + aside for emergencies) */ #define DD_MAX_CACHE_TO_SLOTS_RATIO 4 /* used to limit the cache size */ /* Variable ordering default parameter values. */ -#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 /* 4 for the constants */ -#define DD_DYN_RATIO 2 /* when to dynamically reorder */ +#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 /* 4 for the constants */ +#define DD_DYN_RATIO 2 /* when to dynamically reorder */ /* Primes for cache hash functions. */ -#define DD_P1 12582917 -#define DD_P2 4256249 -#define DD_P3 741457 -#define DD_P4 1618033999 +#define DD_P1 12582917 +#define DD_P2 4256249 +#define DD_P3 741457 +#define DD_P4 1618033999 /* Cache tags for 3-operand operators. These tags are stored in the ** least significant bits of the cache operand pointers according to @@ -143,29 +169,30 @@ ABC_NAMESPACE_HEADER_START ** entry. It can by any even digit between 0 and e. This gives a total ** of 5 bits for the tag proper, which means a maximum of 32 three-operand ** operations. */ -#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 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 /* Generator constants. */ #define CUDD_GEN_CUBES 0 -#define CUDD_GEN_NODES 1 -#define CUDD_GEN_ZDD_PATHS 2 +#define CUDD_GEN_PRIMES 1 +#define CUDD_GEN_NODES 2 +#define CUDD_GEN_ZDD_PATHS 3 #define CUDD_GEN_EMPTY 0 #define CUDD_GEN_NONEMPTY 1 @@ -175,26 +202,37 @@ ABC_NAMESPACE_HEADER_START /*---------------------------------------------------------------------------*/ struct DdGen { - DdManager *manager; - int type; - int status; + DdManager *manager; + int type; + int status; union { - struct { - int *cube; - CUDD_VALUE_TYPE value; - } cubes; - struct { - st_table *visited; - st_generator *stGen; - } nodes; + struct { + int *cube; + CUDD_VALUE_TYPE value; + } cubes; + struct { + int *cube; + DdNode *ub; + } primes; + struct { + int size; + } nodes; } gen; struct { - int sp; - DdNode **stack; + int sp; +#ifdef __osf__ +#pragma pointer_size save +#pragma pointer_size short +#endif + DdNode **stack; +#ifdef __osf__ +#pragma pointer_size restore +#endif } stack; - DdNode *node; + DdNode *node; }; + /*---------------------------------------------------------------------------*/ /* Type declarations */ /*---------------------------------------------------------------------------*/ @@ -204,9 +242,9 @@ struct DdGen { ** are passed the manager as argument; they should return 1 if ** successful and 0 otherwise. */ -typedef struct DdHook { /* hook list element */ - int (*f) ARGS((DdManager *, char *, void *)); /* function to be called */ - struct DdHook *next; /* next element in the list */ +typedef struct DdHook { /* hook list element */ + DD_HFP f; /* function to be called */ + struct DdHook *next; /* next element in the list */ } DdHook; #if SIZEOF_VOID_P == 8 && SIZEOF_INT == 4 @@ -271,173 +309,173 @@ typedef struct DdHashTable { } DdHashTable; typedef struct DdCache { - DdNode *f,*g; /* DDs */ - ptruint h; /* either operator or DD */ - DdNode *data; /* already constructed DD */ + DdNode *f,*g; /* DDs */ + ptruint h; /* either operator or DD */ + DdNode *data; /* already constructed DD */ #ifdef DD_CACHE_PROFILE ptrint count; #endif } DdCache; -typedef struct DdSubtable { /* subtable for one index */ - DdNode **nodelist; /* hash table */ - int shift; /* shift for hash function */ - unsigned int slots; /* size of the hash table */ - unsigned int keys; /* number of nodes stored in this table */ - unsigned int maxKeys; /* slots * DD_MAX_SUBTABLE_DENSITY */ - unsigned int dead; /* number of dead nodes in this table */ - unsigned int next; /* index of next variable in group */ - int bindVar; /* flag to bind this variable to its level */ +typedef struct DdSubtable { /* subtable for one index */ + DdNode **nodelist; /* hash table */ + int shift; /* shift for hash function */ + unsigned int slots; /* size of the hash table */ + unsigned int keys; /* number of nodes stored in this table */ + unsigned int maxKeys; /* slots * DD_MAX_SUBTABLE_DENSITY */ + unsigned int dead; /* number of dead nodes in this table */ + unsigned int next; /* index of next variable in group */ + int bindVar; /* flag to bind this variable to its level */ /* Fields for lazy sifting. */ Cudd_VariableType varType; /* variable type (ps, ns, pi) */ int pairIndex; /* corresponding variable index (ps <-> ns) */ - int varHandled; /* flag: 1 means variable is already handled */ + int varHandled; /* flag: 1 means variable is already handled */ Cudd_LazyGroupType varToBeGrouped; /* tells what grouping to apply */ } DdSubtable; -struct DdManager { /* specialized DD symbol table */ +struct DdManager { /* specialized DD symbol table */ /* Constants */ - DdNode sentinel; /* for collision lists */ - DdNode *one; /* constant 1 */ - DdNode *zero; /* constant 0 */ - DdNode *plusinfinity; /* plus infinity */ - DdNode *minusinfinity; /* minus infinity */ - DdNode *background; /* background value */ + DdNode sentinel; /* for collision lists */ + DdNode *one; /* constant 1 */ + DdNode *zero; /* constant 0 */ + DdNode *plusinfinity; /* plus infinity */ + DdNode *minusinfinity; /* minus infinity */ + DdNode *background; /* background value */ /* Computed Table */ - DdCache *acache; /* address of allocated memory for cache */ - DdCache *cache; /* the cache-based computed table */ + DdCache *acache; /* address of allocated memory for cache */ + DdCache *cache; /* the cache-based computed table */ unsigned int cacheSlots; /* total number of cache entries */ - int cacheShift; /* shift value for cache hash function */ - double cacheMisses; /* number of cache misses (since resizing) */ - double cacheHits; /* number of cache hits (since resizing) */ - double minHit; /* hit percentage above which to resize */ - int cacheSlack; /* slots still available for resizing */ - unsigned int maxCacheHard; /* hard limit for cache size */ + int cacheShift; /* shift value for cache hash function */ + double cacheMisses; /* number of cache misses (since resizing) */ + double cacheHits; /* number of cache hits (since resizing) */ + double minHit; /* hit percentage above which to resize */ + int cacheSlack; /* slots still available for resizing */ + unsigned int maxCacheHard; /* hard limit for cache size */ /* Unique Table */ - int size; /* number of unique subtables */ - int sizeZ; /* for ZDD */ - int maxSize; /* max number of subtables before resizing */ - int maxSizeZ; /* for ZDD */ - DdSubtable *subtables; /* array of unique subtables */ - DdSubtable *subtableZ; /* for ZDD */ - DdSubtable constants; /* unique subtable for the constants */ - unsigned int slots; /* total number of hash buckets */ - unsigned int keys; /* total number of BDD and ADD nodes */ - unsigned int keysZ; /* total number of ZDD nodes */ - unsigned int dead; /* total number of dead BDD and ADD nodes */ - unsigned int deadZ; /* total number of dead ZDD nodes */ - unsigned int maxLive; /* maximum number of live nodes */ - unsigned int minDead; /* do not GC if fewer than these dead */ - double gcFrac; /* gc when this fraction is dead */ - int gcEnabled; /* gc is enabled */ - unsigned int looseUpTo; /* slow growth beyond this limit */ - /* (measured w.r.t. slots, not keys) */ - unsigned int initSlots; /* initial size of a subtable */ - DdNode **stack; /* stack for iterative procedures */ - double allocated; /* number of nodes allocated */ - /* (not during reordering) */ - double reclaimed; /* number of nodes brought back from the dead */ - int isolated; /* isolated projection functions */ - int *perm; /* current variable perm. (index to level) */ - int *permZ; /* for ZDD */ - int *invperm; /* current inv. var. perm. (level to index) */ - int *invpermZ; /* for ZDD */ - DdNode **vars; /* projection functions */ - int *map; /* variable map for fast swap */ - DdNode **univ; /* ZDD 1 for each variable */ - int linearSize; /* number of rows and columns of linear */ - long *interact; /* interacting variable matrix */ - long *linear; /* linear transform matrix */ + int size; /* number of unique subtables */ + int sizeZ; /* for ZDD */ + int maxSize; /* max number of subtables before resizing */ + int maxSizeZ; /* for ZDD */ + DdSubtable *subtables; /* array of unique subtables */ + DdSubtable *subtableZ; /* for ZDD */ + DdSubtable constants; /* unique subtable for the constants */ + unsigned int slots; /* total number of hash buckets */ + unsigned int keys; /* total number of BDD and ADD nodes */ + unsigned int keysZ; /* total number of ZDD nodes */ + unsigned int dead; /* total number of dead BDD and ADD nodes */ + unsigned int deadZ; /* total number of dead ZDD nodes */ + unsigned int maxLive; /* maximum number of live nodes */ + unsigned int minDead; /* do not GC if fewer than these dead */ + double gcFrac; /* gc when this fraction is dead */ + int gcEnabled; /* gc is enabled */ + unsigned int looseUpTo; /* slow growth beyond this limit */ + /* (measured w.r.t. slots, not keys) */ + unsigned int initSlots; /* initial size of a subtable */ + DdNode **stack; /* stack for iterative procedures */ + double allocated; /* number of nodes allocated */ + /* (not during reordering) */ + double reclaimed; /* number of nodes brought back from the dead */ + int isolated; /* isolated projection functions */ + int *perm; /* current variable perm. (index to level) */ + int *permZ; /* for ZDD */ + int *invperm; /* current inv. var. perm. (level to index) */ + int *invpermZ; /* for ZDD */ + DdNode **vars; /* projection functions */ + int *map; /* variable map for fast swap */ + DdNode **univ; /* ZDD 1 for each variable */ + int linearSize; /* number of rows and columns of linear */ + long *interact; /* interacting variable matrix */ + long *linear; /* linear transform matrix */ /* Memory Management */ - DdNode **memoryList; /* memory manager for symbol table */ - DdNode *nextFree; /* list of free nodes */ - char *stash; /* memory reserve */ + DdNode **memoryList; /* memory manager for symbol table */ + DdNode *nextFree; /* list of free nodes */ + char *stash; /* memory reserve */ #ifndef DD_NO_DEATH_ROW - DdNode **deathRow; /* queue for dereferencing */ - int deathRowDepth; /* number of slots in the queue */ - int nextDead; /* index in the queue */ - unsigned deadMask; /* mask for circular index update */ + DdNode **deathRow; /* queue for dereferencing */ + int deathRowDepth; /* number of slots in the queue */ + int nextDead; /* index in the queue */ + unsigned deadMask; /* mask for circular index update */ #endif /* General Parameters */ CUDD_VALUE_TYPE epsilon; /* tolerance on comparisons */ /* Dynamic Reordering Parameters */ - int reordered; /* flag set at the end of reordering */ - int reorderings; /* number of calls to Cudd_ReduceHeap */ - int siftMaxVar; /* maximum number of vars sifted */ - int siftMaxSwap; /* maximum number of swaps per sifting */ - double maxGrowth; /* maximum growth during reordering */ - double maxGrowthAlt; /* alternate maximum growth for reordering */ - int reordCycle; /* how often to apply alternate threshold */ - int autoDyn; /* automatic dynamic reordering flag (BDD) */ - int autoDynZ; /* automatic dynamic reordering flag (ZDD) */ + int reordered; /* flag set at the end of reordering */ + int reorderings; /* number of calls to Cudd_ReduceHeap */ + int siftMaxVar; /* maximum number of vars sifted */ + int siftMaxSwap; /* maximum number of swaps per sifting */ + double maxGrowth; /* maximum growth during reordering */ + double maxGrowthAlt; /* alternate maximum growth for reordering */ + int reordCycle; /* how often to apply alternate threshold */ + int autoDyn; /* automatic dynamic reordering flag (BDD) */ + int autoDynZ; /* automatic dynamic reordering flag (ZDD) */ Cudd_ReorderingType autoMethod; /* default reordering method */ Cudd_ReorderingType autoMethodZ; /* default reordering method (ZDD) */ - int realign; /* realign ZDD order after BDD reordering */ - int realignZ; /* realign BDD order after ZDD reordering */ - unsigned int nextDyn; /* reorder if this size is reached */ - unsigned int countDead; /* if 0, count deads to trigger reordering */ - MtrNode *tree; /* Variable group tree (BDD) */ - MtrNode *treeZ; /* Variable group tree (ZDD) */ + int realign; /* realign ZDD order after BDD reordering */ + int realignZ; /* realign BDD order after ZDD reordering */ + unsigned int nextDyn; /* reorder if this size is reached */ + unsigned int countDead; /* if 0, count deads to trigger reordering */ + MtrNode *tree; /* Variable group tree (BDD) */ + MtrNode *treeZ; /* Variable group tree (ZDD) */ Cudd_AggregationType groupcheck; /* Used during group sifting */ - int recomb; /* Used during group sifting */ - int symmviolation; /* Used during group sifting */ - int arcviolation; /* Used during group sifting */ - int populationSize; /* population size for GA */ - int numberXovers; /* number of crossovers for GA */ - DdLocalCache *localCaches; /* local caches currently in existence */ + int recomb; /* Used during group sifting */ + int symmviolation; /* Used during group sifting */ + int arcviolation; /* Used during group sifting */ + int populationSize; /* population size for GA */ + int numberXovers; /* number of crossovers for GA */ + DdLocalCache *localCaches; /* local caches currently in existence */ #ifdef __osf__ #pragma pointer_size restore #endif - char *hooks; /* application-specific field (used by vis) */ - DdHook *preGCHook; /* hooks to be called before GC */ - DdHook *postGCHook; /* hooks to be called after GC */ - DdHook *preReorderingHook; /* hooks to be called before reordering */ - DdHook *postReorderingHook; /* hooks to be called after reordering */ - FILE *out; /* stdout for this manager */ - FILE *err; /* stderr for this manager */ + char *hooks; /* application-specific field (used by vis) */ + DdHook *preGCHook; /* hooks to be called before GC */ + DdHook *postGCHook; /* hooks to be called after GC */ + DdHook *preReorderingHook; /* hooks to be called before reordering */ + DdHook *postReorderingHook; /* hooks to be called after reordering */ + FILE *out; /* stdout for this manager */ + FILE *err; /* stderr for this manager */ #ifdef __osf__ #pragma pointer_size save #pragma pointer_size short #endif - Cudd_ErrorType errorCode; /* info on last error */ + Cudd_ErrorType errorCode; /* info on last error */ /* Statistical counters. */ - long memused; /* total memory allocated for the manager */ - long maxmem; /* target maximum memory */ - long maxmemhard; /* hard limit for maximum memory */ - int garbageCollections; /* number of garbage collections */ - long GCTime; /* total time spent in garbage collection */ - long reordTime; /* total time spent in reordering */ - double totCachehits; /* total number of cache hits */ - double totCacheMisses; /* total number of cache misses */ - double cachecollisions; /* number of cache collisions */ - double cacheinserts; /* number of cache insertions */ + unsigned long memused; /* total memory allocated for the manager */ + unsigned long maxmem; /* target maximum memory */ + unsigned long maxmemhard; /* hard limit for maximum memory */ + int garbageCollections; /* number of garbage collections */ + long GCTime; /* total time spent in garbage collection */ + long reordTime; /* total time spent in reordering */ + double totCachehits; /* total number of cache hits */ + double totCacheMisses; /* total number of cache misses */ + double cachecollisions; /* number of cache collisions */ + double cacheinserts; /* number of cache insertions */ double cacheLastInserts; /* insertions at the last cache resizing */ - double cachedeletions; /* number of deletions during garbage coll. */ + double cachedeletions; /* number of deletions during garbage coll. */ #ifdef DD_STATS - double nodesFreed; /* number of nodes returned to the free list */ - double nodesDropped; /* number of nodes killed by dereferencing */ + double nodesFreed; /* number of nodes returned to the free list */ + double nodesDropped; /* number of nodes killed by dereferencing */ #endif - unsigned int peakLiveNodes; /* maximum number of live nodes */ + unsigned int peakLiveNodes; /* maximum number of live nodes */ #ifdef DD_UNIQUE_PROFILE - double uniqueLookUps; /* number of unique table lookups */ - double uniqueLinks; /* total distance traveled in coll. chains */ + double uniqueLookUps; /* number of unique table lookups */ + double uniqueLinks; /* total distance traveled in coll. chains */ #endif #ifdef DD_COUNT - double recursiveCalls; /* number of recursive calls */ + double recursiveCalls; /* number of recursive calls */ #ifdef DD_STATS - double nextSample; /* when to write next line of stats */ + double nextSample; /* when to write next line of stats */ #endif - double swapSteps; /* number of elementary reordering steps */ + double swapSteps; /* number of elementary reordering steps */ #endif #ifdef DD_MIS /* mis/verif compatibility fields */ - array_t *iton; /* maps ids in ddNode to node_t */ + array_t *iton; /* maps ids in ddNode to node_t */ array_t *order; /* copy of order_list */ - lsHandle handle; /* where it is in network BDD list */ + lsHandle handle; /* where it is in network BDD list */ network_t *network; - st_table *local_order; /* for local BDDs */ - int nvars; /* variables used so far */ - int threshold; /* for pseudo var threshold value*/ + st_table *local_order; /* for local BDDs */ + int nvars; /* variables used so far */ + int threshold; /* for pseudo var threshold value*/ #endif DdNode * bFunc; DdNode * bFunc2; @@ -496,13 +534,31 @@ typedef struct DdLevelQueue { SideEffects [None] - SeeAlso [cuddAllocNode cuddDynamicAllocNode] + SeeAlso [cuddAllocNode cuddDynamicAllocNode cuddDeallocMove] ******************************************************************************/ #define cuddDeallocNode(unique,node) \ (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 [cuddDeallocNode cuddDynamicAllocNode] + +******************************************************************************/ +#define cuddDeallocMove(unique,node) \ + ((DdNode *)(node))->ref = 0; \ + ((DdNode *)(node))->next = (unique)->nextFree; \ + (unique)->nextFree = (DdNode *)(node); + /**Macro*********************************************************************** @@ -620,7 +676,7 @@ typedef struct DdLevelQueue { SeeAlso [Cudd_ReadPerm] ******************************************************************************/ -#define cuddI(dd,index) (((index)==CUDD_CONST_INDEX)?(int)(index):(dd)->perm[(index)]) +#define cuddI(dd,index) (((index)==CUDD_CONST_INDEX)?(int)(index):(dd)->perm[(index)]) /**Macro*********************************************************************** @@ -638,7 +694,7 @@ typedef struct DdLevelQueue { SeeAlso [Cudd_ReadPermZdd] ******************************************************************************/ -#define cuddIZ(dd,index) (((index)==CUDD_CONST_INDEX)?(int)(index):(dd)->permZ[(index)]) +#define cuddIZ(dd,index) (((index)==CUDD_CONST_INDEX)?(int)(index):(dd)->permZ[(index)]) /**Macro*********************************************************************** @@ -654,8 +710,8 @@ typedef struct DdLevelQueue { ******************************************************************************/ #if SIZEOF_VOID_P == 8 && SIZEOF_INT == 4 #define ddHash(f,g,s) \ -((((unsigned)(unsigned long)(f) * DD_P1 + \ - (unsigned)(unsigned long)(g)) * DD_P2) >> (s)) +((((unsigned)(ptruint)(f) * DD_P1 + \ + (unsigned)(ptruint)(g)) * DD_P2) >> (s)) #else #define ddHash(f,g,s) \ ((((unsigned)(f) * DD_P1 + (unsigned)(g)) * DD_P2) >> (s)) @@ -675,9 +731,9 @@ typedef struct DdLevelQueue { ******************************************************************************/ #if SIZEOF_VOID_P == 8 && SIZEOF_INT == 4 #define ddCHash(o,f,g,h,s) \ -((((((unsigned)(unsigned long)(f) + (unsigned)(unsigned long)(o)) * DD_P1 + \ - (unsigned)(unsigned long)(g)) * DD_P2 + \ - (unsigned)(unsigned long)(h)) * DD_P3) >> (s)) +((((((unsigned)(ptruint)(f) + (unsigned)(ptruint)(o)) * DD_P1 + \ + (unsigned)(ptruint)(g)) * DD_P2 + \ + (unsigned)(ptruint)(h)) * DD_P3) >> (s)) #else #define ddCHash(o,f,g,h,s) \ ((((((unsigned)(f) + (unsigned)(o)) * DD_P1 + (unsigned)(g)) * DD_P2 + \ @@ -699,8 +755,8 @@ typedef struct DdLevelQueue { ******************************************************************************/ #if SIZEOF_VOID_P == 8 && SIZEOF_INT == 4 #define ddCHash2(o,f,g,s) \ -(((((unsigned)(unsigned long)(f) + (unsigned)(unsigned long)(o)) * DD_P1 + \ - (unsigned)(unsigned long)(g)) * DD_P2) >> (s)) +(((((unsigned)(ptruint)(f) + (unsigned)(ptruint)(o)) * DD_P1 + \ + (unsigned)(ptruint)(g)) * DD_P2) >> (s)) #else #define ddCHash2(o,f,g,s) \ (((((unsigned)(f) + (unsigned)(o)) * DD_P1 + (unsigned)(g)) * DD_P2) >> (s)) @@ -825,7 +881,7 @@ typedef struct DdLevelQueue { SeeAlso [DD_ZERO DD_PLUS_INFINITY DD_MINUS_INFINITY] ******************************************************************************/ -#define DD_ONE(dd) ((dd)->one) +#define DD_ONE(dd) ((dd)->one) /**Macro*********************************************************************** @@ -893,7 +949,7 @@ typedef struct DdLevelQueue { #ifdef HAVE_IEEE_754 #define cuddAdjust(x) #else -#define cuddAdjust(x) ((x) = ((x) >= DD_CRI_HI_MARK) ? DD_PLUS_INF_VAL : (((x) <= DD_CRI_LO_MARK) ? DD_MINUS_INF_VAL : (x))) +#define cuddAdjust(x) ((x) = ((x) >= DD_CRI_HI_MARK) ? DD_PLUS_INF_VAL : (((x) <= DD_CRI_LO_MARK) ? DD_MINUS_INF_VAL : (x))) #endif @@ -909,7 +965,7 @@ typedef struct DdLevelQueue { SeeAlso [DD_MSDIGIT] ******************************************************************************/ -#define DD_LSDIGIT(x) ((x) & DD_APA_MASK) +#define DD_LSDIGIT(x) ((x) & DD_APA_MASK) /**Macro*********************************************************************** @@ -924,7 +980,7 @@ typedef struct DdLevelQueue { SeeAlso [DD_LSDIGIT] ******************************************************************************/ -#define DD_MSDIGIT(x) ((x) >> DD_APA_BITS) +#define DD_MSDIGIT(x) ((x) >> DD_APA_BITS) /**Macro*********************************************************************** @@ -961,181 +1017,184 @@ dd->nextSample += 250000;} /* Function prototypes */ /*---------------------------------------------------------------------------*/ -EXTERN DdNode * cuddAddExistAbstractRecur ARGS((DdManager *manager, DdNode *f, DdNode *cube)); -EXTERN DdNode * cuddAddUnivAbstractRecur ARGS((DdManager *manager, DdNode *f, DdNode *cube)); -EXTERN DdNode * cuddAddOrAbstractRecur 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 * cuddAddNegateRecur 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 * cuddBddExistAbstractRecur ARGS((DdManager *manager, DdNode *f, DdNode *cube)); -EXTERN DdNode * cuddBddXorExistAbstractRecur ARGS((DdManager *manager, DdNode *f, DdNode *g, DdNode *cube)); -EXTERN DdNode * cuddBddBooleanDiffRecur ARGS((DdManager *manager, DdNode *f, DdNode *var)); -EXTERN DdNode * cuddBddIteRecur ARGS((DdManager *dd, DdNode *f, DdNode *g, DdNode *h)); -EXTERN DdNode * cuddBddIntersectRecur ARGS((DdManager *dd, DdNode *f, DdNode *g)); -EXTERN DdNode * cuddBddAndRecur ARGS((DdManager *manager, DdNode *f, DdNode *g)); -EXTERN DdNode * cuddBddXorRecur ARGS((DdManager *manager, DdNode *f, DdNode *g)); -EXTERN DdNode * cuddBddTransfer ARGS((DdManager *ddS, DdManager *ddD, DdNode *f)); -EXTERN DdNode * cuddAddBddDoPattern ARGS((DdManager *dd, 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 * cuddCacheLookupZdd 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 DdNode * cuddCacheLookup2Zdd ARGS((DdManager *table, DdNode * (*)(DdManager *, DdNode *, DdNode *), DdNode *f, DdNode *g)); -EXTERN DdNode * cuddCacheLookup1Zdd ARGS((DdManager *table, DdNode * (*)(DdManager *, DdNode *), DdNode *f)); -EXTERN DdNode * cuddConstantLookup ARGS((DdManager *table, ptruint op, DdNode *f, DdNode *g, DdNode *h)); -EXTERN int cuddCacheProfile ARGS((DdManager *table, FILE *fp)); -EXTERN void cuddCacheResize ARGS((DdManager *table)); -EXTERN void cuddCacheFlush 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 * cuddCofactorRecur ARGS((DdManager *dd, DdNode *f, DdNode *g)); -EXTERN DdNode * cuddBddComposeRecur ARGS((DdManager *dd, DdNode *f, DdNode *g, DdNode *proj)); -EXTERN DdNode * cuddAddComposeRecur ARGS((DdManager *dd, DdNode *f, DdNode *g, DdNode *proj)); -EXTERN int cuddExact ARGS((DdManager *table, int lower, int upper)); -EXTERN DdNode * cuddBddConstrainRecur ARGS((DdManager *dd, DdNode *f, DdNode *c)); -EXTERN DdNode * cuddBddRestrictRecur ARGS((DdManager *dd, DdNode *f, DdNode *c)); -EXTERN DdNode * cuddAddConstrainRecur ARGS((DdManager *dd, DdNode *f, DdNode *c)); -EXTERN DdNode * cuddAddRestrictRecur ARGS((DdManager *dd, DdNode *f, DdNode *c)); -EXTERN DdNode * cuddBddLICompaction ARGS((DdManager *dd, DdNode *f, DdNode *c)); -EXTERN int cuddGa ARGS((DdManager *table, int lower, int upper)); -EXTERN int cuddTreeSifting ARGS((DdManager *table, Cudd_ReorderingType method, int TimeStop)); -EXTERN int cuddZddInitUniv ARGS((DdManager *zdd)); -EXTERN void cuddZddFreeUniv ARGS((DdManager *zdd)); -EXTERN void cuddSetInteract ARGS((DdManager *table, int x, int y)); -EXTERN int cuddTestInteract ARGS((DdManager *table, int x, int y)); -EXTERN int cuddInitInteract ARGS((DdManager *table)); -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 int cuddIsInDeathRow ARGS((DdManager *dd, DdNode *f)); -EXTERN int cuddTimesInDeathRow ARGS((DdManager *dd, DdNode *f)); -EXTERN void cuddLocalCacheClearAll ARGS((DdManager *manager)); +extern DdNode * cuddAddExistAbstractRecur( DdManager * manager, DdNode * f, DdNode * cube ); +extern DdNode * cuddAddUnivAbstractRecur( DdManager * manager, DdNode * f, DdNode * cube ); +extern DdNode * cuddAddOrAbstractRecur( DdManager * manager, DdNode * f, DdNode * cube ); +extern DdNode * cuddAddApplyRecur( DdManager * dd, DdNode * (*)(DdManager * , DdNode ** , DdNode **), DdNode * f, DdNode * g ); +extern DdNode * cuddAddMonadicApplyRecur( DdManager * dd, DdNode * (*)(DdManager * , DdNode *), DdNode * f ); +extern DdNode * cuddAddScalarInverseRecur( DdManager * dd, DdNode * f, DdNode * epsilon ); +extern DdNode * cuddAddIteRecur( DdManager * dd, DdNode * f, DdNode * g, DdNode * h ); +extern DdNode * cuddAddCmplRecur( DdManager * dd, DdNode * f ); +extern DdNode * cuddAddNegateRecur( DdManager * dd, DdNode * f ); +extern DdNode * cuddAddRoundOffRecur( DdManager * dd, DdNode * f, double trunc ); +extern DdNode * cuddUnderApprox( DdManager * dd, DdNode * f, int numVars, int threshold, int safe, double quality ); +extern DdNode * cuddRemapUnderApprox( DdManager * dd, DdNode * f, int numVars, int threshold, double quality ); +extern DdNode * cuddBiasedUnderApprox( DdManager * dd, DdNode * f, DdNode * b, int numVars, int threshold, double quality1, double quality0 ); +extern DdNode * cuddBddAndAbstractRecur( DdManager * manager, DdNode * f, DdNode * g, DdNode * cube ); +extern int cuddAnnealing( DdManager * table, int lower, int upper ); +extern DdNode * cuddBddExistAbstractRecur( DdManager * manager, DdNode * f, DdNode * cube ); +extern DdNode * cuddBddXorExistAbstractRecur( DdManager * manager, DdNode * f, DdNode * g, DdNode * cube ); +extern DdNode * cuddBddBooleanDiffRecur( DdManager * manager, DdNode * f, DdNode * var ); +extern DdNode * cuddBddIteRecur( DdManager * dd, DdNode * f, DdNode * g, DdNode * h ); +extern DdNode * cuddBddIntersectRecur( DdManager * dd, DdNode * f, DdNode * g ); +extern DdNode * cuddBddAndRecur( DdManager * manager, DdNode * f, DdNode * g ); +extern DdNode * cuddBddXorRecur( DdManager * manager, DdNode * f, DdNode * g ); +extern DdNode * cuddBddTransfer( DdManager * ddS, DdManager * ddD, DdNode * f ); +extern DdNode * cuddAddBddDoPattern( DdManager * dd, DdNode * f ); +extern int cuddInitCache( DdManager * unique, unsigned int cacheSize, unsigned int maxCacheSize ); +extern void cuddCacheInsert( DdManager * table, ptruint op, DdNode * f, DdNode * g, DdNode * h, DdNode * data ); +extern void cuddCacheInsert2( DdManager * table, DdNode * (*)(DdManager * , DdNode * , DdNode *), DdNode * f, DdNode * g, DdNode * data ); +extern void cuddCacheInsert1( DdManager * table, DdNode * (*)(DdManager * , DdNode *), DdNode * f, DdNode * data ); +extern DdNode * cuddCacheLookup( DdManager * table, ptruint op, DdNode * f, DdNode * g, DdNode * h ); +extern DdNode * cuddCacheLookupZdd( DdManager * table, ptruint op, DdNode * f, DdNode * g, DdNode * h ); +extern DdNode * cuddCacheLookup2( DdManager * table, DdNode * (*)(DdManager * , DdNode * , DdNode *), DdNode * f, DdNode * g ); +extern DdNode * cuddCacheLookup1( DdManager * table, DdNode * (*)(DdManager * , DdNode *), DdNode * f ); +extern DdNode * cuddCacheLookup2Zdd( DdManager * table, DdNode * (*)(DdManager * , DdNode * , DdNode *), DdNode * f, DdNode * g ); +extern DdNode * cuddCacheLookup1Zdd( DdManager * table, DdNode * (*)(DdManager * , DdNode *), DdNode * f ); +extern DdNode * cuddConstantLookup( DdManager * table, ptruint op, DdNode * f, DdNode * g, DdNode * h ); +extern int cuddCacheProfile( DdManager * table, FILE * fp ); +extern void cuddCacheResize( DdManager * table ); +extern void cuddCacheFlush( DdManager * table ); +extern int cuddComputeFloorLog2( unsigned int value ); +extern int cuddHeapProfile( DdManager * dd ); +extern void cuddPrintNode( DdNode * f, FILE * fp ); +extern void cuddPrintVarGroups( DdManager * dd, MtrNode * root, int zdd, int silent ); +extern DdNode * cuddBddClippingAnd( DdManager * dd, DdNode * f, DdNode * g, int maxDepth, int direction ); +extern DdNode * cuddBddClippingAndAbstract( DdManager * dd, DdNode * f, DdNode * g, DdNode * cube, int maxDepth, int direction ); +extern void cuddGetBranches( DdNode * g, DdNode ** g1, DdNode ** g0 ); +extern int cuddCheckCube( DdManager * dd, DdNode * g ); +extern DdNode * cuddCofactorRecur( DdManager * dd, DdNode * f, DdNode * g ); +extern DdNode * cuddBddComposeRecur( DdManager * dd, DdNode * f, DdNode * g, DdNode * proj ); +extern DdNode * cuddAddComposeRecur( DdManager * dd, DdNode * f, DdNode * g, DdNode * proj ); +extern int cuddExact( DdManager * table, int lower, int upper ); +extern DdNode * cuddBddConstrainRecur( DdManager * dd, DdNode * f, DdNode * c ); +extern DdNode * cuddBddRestrictRecur( DdManager * dd, DdNode * f, DdNode * c ); +extern DdNode * cuddBddNPAndRecur( DdManager * dd, DdNode * f, DdNode * c ); +extern DdNode * cuddAddConstrainRecur( DdManager * dd, DdNode * f, DdNode * c ); +extern DdNode * cuddAddRestrictRecur( DdManager * dd, DdNode * f, DdNode * c ); +extern DdNode * cuddBddLICompaction( DdManager * dd, DdNode * f, DdNode * c ); +extern int cuddGa( DdManager * table, int lower, int upper ); +extern int cuddTreeSifting( DdManager * table, Cudd_ReorderingType method ); +extern int cuddZddInitUniv( DdManager * zdd ); +extern void cuddZddFreeUniv( DdManager * zdd ); +extern void cuddSetInteract( DdManager * table, int x, int y ); +extern int cuddTestInteract( DdManager * table, int x, int y ); +extern int cuddInitInteract( DdManager * table ); +extern DdLocalCache * cuddLocalCacheInit( DdManager * manager, unsigned int keySize, unsigned int cacheSize, unsigned int maxCacheSize ); +extern void cuddLocalCacheQuit( DdLocalCache * cache ); +extern void cuddLocalCacheInsert( DdLocalCache * cache, DdNodePtr * key, DdNode * value ); +extern DdNode * cuddLocalCacheLookup( DdLocalCache * cache, DdNodePtr * key ); +extern void cuddLocalCacheClearDead( DdManager * manager ); +extern int cuddIsInDeathRow( DdManager * dd, DdNode * f ); +extern int cuddTimesInDeathRow( DdManager * dd, DdNode * f ); +extern void cuddLocalCacheClearAll( DdManager * manager ); #ifdef DD_CACHE_PROFILE -EXTERN int cuddLocalCacheProfile ARGS((DdLocalCache *cache)); +extern int cuddLocalCacheProfile( DdLocalCache * cache ); #endif -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 int cuddLinearAndSifting ARGS((DdManager *table, int lower, int upper)); -EXTERN DdNode * cuddBddLiteralSetIntersectionRecur ARGS((DdManager *dd, DdNode *f, DdNode *g)); -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 void cuddReclaimZdd ARGS((DdManager *table, DdNode *n)); -EXTERN void cuddClearDeathRow ARGS((DdManager *table)); -EXTERN void cuddShrinkDeathRow ARGS((DdManager *table)); -EXTERN DdNode * cuddDynamicAllocNode ARGS((DdManager *table)); -EXTERN int cuddSifting ARGS((DdManager *table, int lower, int upper)); -EXTERN int cuddSwapping ARGS((DdManager *table, int lower, int upper, Cudd_ReorderingType heuristic)); -EXTERN int cuddNextHigh ARGS((DdManager *table, int x)); -EXTERN int cuddNextLow ARGS((DdManager *table, int x)); -EXTERN int cuddSwapInPlace ARGS((DdManager *table, int x, int y)); -EXTERN int cuddBddAlignToZdd ARGS((DdManager *table)); -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 DdHashTable * cuddHashTableInit( DdManager * manager, unsigned int keySize, unsigned int initSize ); +extern void cuddHashTableQuit( DdHashTable * hash ); +extern int cuddHashTableInsert( DdHashTable * hash, DdNodePtr * key, DdNode * value, ptrint count ); +extern DdNode * cuddHashTableLookup( DdHashTable * hash, DdNodePtr * key ); +extern int cuddHashTableInsert1( DdHashTable * hash, DdNode * f, DdNode * value, ptrint count ); +extern DdNode * cuddHashTableLookup1( DdHashTable * hash, DdNode * f ); +extern int cuddHashTableInsert2( DdHashTable * hash, DdNode * f, DdNode * g, DdNode * value, ptrint count ); +extern DdNode * cuddHashTableLookup2( DdHashTable * hash, DdNode * f, DdNode * g ); +extern int cuddHashTableInsert3( DdHashTable * hash, DdNode * f, DdNode * g, DdNode * h, DdNode * value, ptrint count ); +extern DdNode * cuddHashTableLookup3( DdHashTable * hash, DdNode * f, DdNode * g, DdNode * h ); +extern DdLevelQueue * cuddLevelQueueInit( int levels, int itemSize, int numBuckets ); +extern void cuddLevelQueueQuit( DdLevelQueue * queue ); +extern void * cuddLevelQueueEnqueue( DdLevelQueue * queue, void * key, int level ); +extern void cuddLevelQueueDequeue( DdLevelQueue * queue, int level ); +extern int cuddLinearAndSifting( DdManager * table, int lower, int upper ); +extern int cuddLinearInPlace( DdManager * table, int x, int y ); +extern void cuddUpdateInteractionMatrix( DdManager * table, int xindex, int yindex ); +extern int cuddInitLinear( DdManager * table ); +extern int cuddResizeLinear( DdManager * table ); +extern DdNode * cuddBddLiteralSetIntersectionRecur( DdManager * dd, DdNode * f, DdNode * g ); +extern DdNode * cuddCProjectionRecur( DdManager * dd, DdNode * R, DdNode * Y, DdNode * Ysupp ); +extern DdNode * cuddBddClosestCube( DdManager * dd, DdNode * f, DdNode * g, CUDD_VALUE_TYPE bound ); +extern void cuddReclaim( DdManager * table, DdNode * n ); +extern void cuddReclaimZdd( DdManager * table, DdNode * n ); +extern void cuddClearDeathRow( DdManager * table ); +extern void cuddShrinkDeathRow( DdManager * table ); +extern DdNode * cuddDynamicAllocNode( DdManager * table ); +extern int cuddSifting( DdManager * table, int lower, int upper ); +extern int cuddSwapping( DdManager * table, int lower, int upper, Cudd_ReorderingType heuristic ); +extern int cuddNextHigh( DdManager * table, int x ); +extern int cuddNextLow( DdManager * table, int x ); +extern int cuddSwapInPlace( DdManager * table, int x, int y ); +extern int cuddBddAlignToZdd( DdManager * table ); +extern DdNode * cuddBddMakePrime( DdManager * dd, DdNode * cube, DdNode * f ); +extern DdNode * cuddSolveEqnRecur( DdManager * bdd, DdNode * F, DdNode * Y, DdNode ** G, int n, int * yIndex, int i ); +extern DdNode * cuddVerifySol( DdManager * bdd, DdNode * F, DdNode ** G, int * yIndex, int n ); #ifdef ST_INCLUDED -EXTERN DdNode* cuddSplitSetRecur ARGS((DdManager *manager, st_table *mtable, int *varSeen, DdNode *p, double n, double max, int index)); +extern DdNode * cuddSplitSetRecur( DdManager * manager, st_table * mtable, int * varSeen, DdNode * p, double n, double max, int index ); #endif -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 int cuddSymmCheck ARGS((DdManager *table, int x, int y)); -EXTERN int cuddSymmSifting ARGS((DdManager *table, int lower, int upper, int TimeStop)); -EXTERN int cuddSymmSiftingConv ARGS((DdManager *table, int lower, int upper)); -EXTERN DdNode * cuddAllocNode ARGS((DdManager *unique)); -EXTERN DdManager * cuddInitTable ARGS((unsigned int numVars, unsigned int numVarsZ, unsigned int numSlots, unsigned int looseUpTo)); -EXTERN void cuddFreeTable ARGS((DdManager *unique)); -EXTERN int cuddGarbageCollect ARGS((DdManager *unique, int clearCache)); -EXTERN int cuddGarbageCollectZdd 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 * cuddUniqueInterIVO ARGS((DdManager *unique, int index, DdNode *T, DdNode *E)); -EXTERN DdNode * cuddUniqueInterZdd 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 void cuddShrinkSubtable 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 void cuddSlowTableGrowth ARGS((DdManager *unique)); -EXTERN int cuddP ARGS((DdManager *dd, DdNode *f)); +extern DdNode * cuddSubsetHeavyBranch( DdManager * dd, DdNode * f, int numVars, int threshold ); +extern DdNode * cuddSubsetShortPaths( DdManager * dd, DdNode * f, int numVars, int threshold, int hardlimit ); +extern int cuddSymmCheck( DdManager * table, int x, int y ); +extern int cuddSymmSifting( DdManager * table, int lower, int upper ); +extern int cuddSymmSiftingConv( DdManager * table, int lower, int upper ); +extern DdNode * cuddAllocNode( DdManager * unique ); +extern DdManager * cuddInitTable( unsigned int numVars, unsigned int numVarsZ, unsigned int numSlots, unsigned int looseUpTo ); +extern void cuddFreeTable( DdManager * unique ); +extern int cuddGarbageCollect( DdManager * unique, int clearCache ); +extern DdNode * cuddZddGetNode( DdManager * zdd, int id, DdNode * T, DdNode * E ); +extern DdNode * cuddZddGetNodeIVO( DdManager * dd, int index, DdNode * g, DdNode * h ); +extern DdNode * cuddUniqueInter( DdManager * unique, int index, DdNode * T, DdNode * E ); +extern DdNode * cuddUniqueInterIVO( DdManager * unique, int index, DdNode * T, DdNode * E ); +extern DdNode * cuddUniqueInterZdd( DdManager * unique, int index, DdNode * T, DdNode * E ); +extern DdNode * cuddUniqueConst( DdManager * unique, CUDD_VALUE_TYPE value ); +extern void cuddRehash( DdManager * unique, int i ); +extern void cuddShrinkSubtable( DdManager * unique, int i ); +extern int cuddInsertSubtables( DdManager * unique, int n, int level ); +extern int cuddDestroySubtables( DdManager * unique, int n ); +extern int cuddResizeTableZdd( DdManager * unique, int index ); +extern void cuddSlowTableGrowth( DdManager * unique ); +extern int cuddP( DdManager * dd, DdNode * f ); #ifdef ST_INCLUDED -EXTERN enum st_retval cuddStCountfree ARGS((char *key, char *value, char *arg)); -EXTERN int cuddCollectNodes ARGS((DdNode *f, st_table *visited)); +extern enum st_retval cuddStCountfree( char * key, char * value, char * arg ); +extern int cuddCollectNodes( DdNode * f, st_table * visited ); #endif -EXTERN int cuddWindowReorder ARGS((DdManager *table, int low, int high, Cudd_ReorderingType submethod)); -EXTERN DdNode * cuddZddProduct ARGS((DdManager *dd, DdNode *f, DdNode *g)); -EXTERN DdNode * cuddZddUnateProduct ARGS((DdManager *dd, DdNode *f, DdNode *g)); -EXTERN DdNode * cuddZddWeakDiv ARGS((DdManager *dd, DdNode *f, DdNode *g)); -EXTERN DdNode * cuddZddWeakDivF ARGS((DdManager *dd, DdNode *f, DdNode *g)); -EXTERN DdNode * cuddZddDivide ARGS((DdManager *dd, DdNode *f, DdNode *g)); -EXTERN DdNode * cuddZddDivideF ARGS((DdManager *dd, DdNode *f, DdNode *g)); -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 int cuddZddTreeSifting ARGS((DdManager *table, Cudd_ReorderingType method)); -EXTERN DdNode * cuddZddIsop ARGS((DdManager *dd, DdNode *L, DdNode *U, DdNode **zdd_I)); -EXTERN DdNode * cuddBddIsop ARGS((DdManager *dd, DdNode *L, DdNode *U)); -EXTERN DdNode * cuddMakeBddFromZddCover ARGS((DdManager *dd, DdNode *node)); -EXTERN int cuddZddLinearSifting ARGS((DdManager *table, int lower, int upper)); -EXTERN int cuddZddAlignToBdd ARGS((DdManager *table)); -EXTERN int cuddZddNextHigh ARGS((DdManager *table, int x)); -EXTERN int cuddZddNextLow ARGS((DdManager *table, int x)); -EXTERN int cuddZddUniqueCompare ARGS((int *ptr_x, int *ptr_y)); -EXTERN int cuddZddSwapInPlace ARGS((DdManager *table, int x, int y)); -EXTERN int cuddZddSwapping ARGS((DdManager *table, int lower, int upper, Cudd_ReorderingType heuristic)); -EXTERN int cuddZddSifting ARGS((DdManager *table, int lower, int upper)); -EXTERN DdNode * cuddZddIte ARGS((DdManager *dd, DdNode *f, DdNode *g, DdNode *h)); -EXTERN DdNode * cuddZddUnion ARGS((DdManager *zdd, DdNode *P, DdNode *Q)); -EXTERN DdNode * cuddZddIntersect ARGS((DdManager *zdd, DdNode *P, DdNode *Q)); -EXTERN DdNode * cuddZddDiff 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 DdNode * cuddZddSubset0 ARGS((DdManager *dd, DdNode *P, int var)); -EXTERN DdNode * cuddZddChange ARGS((DdManager *dd, DdNode *P, int var)); -EXTERN int cuddZddSymmCheck ARGS((DdManager *table, int x, int y)); -EXTERN int cuddZddSymmSifting ARGS((DdManager *table, int lower, int upper)); -EXTERN int cuddZddSymmSiftingConv ARGS((DdManager *table, int lower, int upper)); -EXTERN int cuddZddP ARGS((DdManager *zdd, DdNode *f)); - -EXTERN void (*MMoutOfMemory)(long); +extern DdNodePtr * cuddNodeArray( DdNode * f, int * n ); +extern int cuddWindowReorder( DdManager * table, int low, int high, Cudd_ReorderingType submethod ); +extern DdNode * cuddZddProduct( DdManager * dd, DdNode * f, DdNode * g ); +extern DdNode * cuddZddUnateProduct( DdManager * dd, DdNode * f, DdNode * g ); +extern DdNode * cuddZddWeakDiv( DdManager * dd, DdNode * f, DdNode * g ); +extern DdNode * cuddZddWeakDivF( DdManager * dd, DdNode * f, DdNode * g ); +extern DdNode * cuddZddDivide( DdManager * dd, DdNode * f, DdNode * g ); +extern DdNode * cuddZddDivideF( DdManager * dd, DdNode * f, DdNode * g ); +extern int cuddZddGetCofactors3( DdManager * dd, DdNode * f, int v, DdNode ** f1, DdNode ** f0, DdNode ** fd ); +extern int cuddZddGetCofactors2( DdManager * dd, DdNode * f, int v, DdNode ** f1, DdNode ** f0 ); +extern DdNode * cuddZddComplement( 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 int cuddZddTreeSifting( DdManager * table, Cudd_ReorderingType method ); +extern DdNode * cuddZddIsop( DdManager * dd, DdNode * L, DdNode * U, DdNode ** zdd_I ); +extern DdNode * cuddBddIsop( DdManager * dd, DdNode * L, DdNode * U ); +extern DdNode * cuddMakeBddFromZddCover( DdManager * dd, DdNode * node ); +extern int cuddZddLinearSifting( DdManager * table, int lower, int upper ); +extern int cuddZddAlignToBdd( DdManager * table ); +extern int cuddZddNextHigh( DdManager * table, int x ); +extern int cuddZddNextLow( DdManager * table, int x ); +extern int cuddZddUniqueCompare( int * ptr_x, int * ptr_y ); +extern int cuddZddSwapInPlace( DdManager * table, int x, int y ); +extern int cuddZddSwapping( DdManager * table, int lower, int upper, Cudd_ReorderingType heuristic ); +extern int cuddZddSifting( DdManager * table, int lower, int upper ); +extern DdNode * cuddZddIte( DdManager * dd, DdNode * f, DdNode * g, DdNode * h ); +extern DdNode * cuddZddUnion( DdManager * zdd, DdNode * P, DdNode * Q ); +extern DdNode * cuddZddIntersect( DdManager * zdd, DdNode * P, DdNode * Q ); +extern DdNode * cuddZddDiff( DdManager * zdd, DdNode * P, DdNode * Q ); +extern DdNode * cuddZddChangeAux( DdManager * zdd, DdNode * P, DdNode * zvar ); +extern DdNode * cuddZddSubset1( DdManager * dd, DdNode * P, int var ); +extern DdNode * cuddZddSubset0( DdManager * dd, DdNode * P, int var ); +extern DdNode * cuddZddChange( DdManager * dd, DdNode * P, int var ); +extern int cuddZddSymmCheck( DdManager * table, int x, int y ); +extern int cuddZddSymmSifting( DdManager * table, int lower, int upper ); +extern int cuddZddSymmSiftingConv( DdManager * table, int lower, int upper ); +extern int cuddZddP( DdManager * zdd, DdNode * f ); /**AutomaticEnd***************************************************************/ |