cuddInt.h Source File

00001 
00024 #ifndef _CUDDINT
00025 #define _CUDDINT
00026 
00027 
00028 /*---------------------------------------------------------------------------*/
00029 /* Nested includes                                                           */
00030 /*---------------------------------------------------------------------------*/
00031 
00032 #ifdef DD_MIS
00033 #include "array.h"
00034 #include "list.h"
00035 #include "st.h"
00036 #include "espresso.h"
00037 #include "node.h"
00038 #ifdef SIS
00039 #include "graph.h"
00040 #include "astg.h"
00041 #endif
00042 #include "network.h"
00043 #endif
00044 
00045 #include <math.h>
00046 #include "cudd.h"
00047 
00048 #if defined(__GNUC__)
00049 # define DD_INLINE __inline__
00050 # if (__GNUC__ >2 || __GNUC_MINOR__ >=7)
00051 #   define DD_UNUSED __attribute__ ((__unused__))
00052 # else
00053 #   define DD_UNUSED
00054 # endif
00055 #else
00056 # if defined(__cplusplus)
00057 #   define DD_INLINE inline
00058 # else
00059 #   define DD_INLINE
00060 # endif
00061 # define DD_UNUSED
00062 #endif
00063 
00064 
00065 /*---------------------------------------------------------------------------*/
00066 /* Constant declarations                                                     */
00067 /*---------------------------------------------------------------------------*/
00068 
00069 #define DD_MAXREF   ((DdHalfWord) ~0)
00070 
00071 #define DD_DEFAULT_RESIZE 10  /* how many extra variables */
00072           /* should be added when resizing */
00073 #define DD_MEM_CHUNK    1022
00074 
00075 /* These definitions work for CUDD_VALUE_TYPE == double */
00076 #define DD_ONE_VAL    (1.0)
00077 #define DD_ZERO_VAL   (0.0)
00078 #define DD_EPSILON    (1.0e-12)
00079 
00080 /* The definitions of +/- infinity in terms of HUGE_VAL work on
00081 ** the DECstations and on many other combinations of OS/compiler.
00082 */
00083 #ifdef HAVE_IEEE_754
00084 #  define DD_PLUS_INF_VAL (HUGE_VAL)
00085 #else
00086 #  define DD_PLUS_INF_VAL (10e301)
00087 #  define DD_CRI_HI_MARK  (10e150)
00088 #  define DD_CRI_LO_MARK  (-(DD_CRI_HI_MARK))
00089 #endif
00090 #define DD_MINUS_INF_VAL  (-(DD_PLUS_INF_VAL))
00091 
00092 #define DD_NON_CONSTANT   ((DdNode *) 1)  /* for Cudd_bddIteConstant */
00093 
00094 /* Unique table and cache management constants. */
00095 #define DD_MAX_SUBTABLE_DENSITY 4 /* tells when to resize a subtable */
00096 /* gc when this percent are dead (measured w.r.t. slots, not keys)
00097 ** The first limit (LO) applies normally. The second limit applies when
00098 ** the package believes more space for the unique table (i.e., more dead
00099 ** nodes) would improve performance, and the unique table is not already
00100 ** too large. The third limit applies when memory is low.
00101 */
00102 #define DD_GC_FRAC_LO   DD_MAX_SUBTABLE_DENSITY * 0.25
00103 #define DD_GC_FRAC_HI   DD_MAX_SUBTABLE_DENSITY * 1.0
00104 #define DD_GC_FRAC_MIN    0.2
00105 #define DD_MIN_HIT    30  /* resize cache when hit ratio
00106              above this percentage (default) */
00107 #define DD_MAX_LOOSE_FRACTION 5 /* 1 / (max fraction of memory used for
00108              unique table in fast growth mode) */
00109 #define DD_MAX_CACHE_FRACTION 3 /* 1 / (max fraction of memory used for
00110              computed table if resizing enabled) */
00111 #define DD_STASH_FRACTION 64 /* 1 / (fraction of memory set
00112               aside for emergencies) */
00113 #define DD_MAX_CACHE_TO_SLOTS_RATIO 4 /* used to limit the cache size */
00114 
00115 /* Variable ordering default parameter values. */
00116 #define DD_SIFT_MAX_VAR   1000
00117 #define DD_SIFT_MAX_SWAPS 2000000
00118 #define DD_DEFAULT_RECOMB 0
00119 #define DD_MAX_REORDER_GROWTH 1.2
00120 #define DD_FIRST_REORDER  4004  /* 4 for the constants */
00121 #define DD_DYN_RATIO    2 /* when to dynamically reorder */
00122 
00123 /* Primes for cache hash functions. */
00124 #define DD_P1     12582917
00125 #define DD_P2     4256249
00126 #define DD_P3     741457
00127 #define DD_P4     1618033999
00128 
00129 /* Cache tags for 3-operand operators. */
00130 #define DD_ADD_ITE_TAG        0x02
00131 #define DD_BDD_AND_ABSTRACT_TAG     0x06
00132 #define DD_BDD_XOR_EXIST_ABSTRACT_TAG   0x0a
00133 #define DD_BDD_ITE_TAG        0x0e
00134 #define DD_ADD_BDD_DO_INTERVAL_TAG    0x22
00135 #define DD_BDD_CLIPPING_AND_ABSTRACT_UP_TAG 0x26
00136 #define DD_BDD_CLIPPING_AND_ABSTRACT_DOWN_TAG 0x2a
00137 #define DD_BDD_COMPOSE_RECUR_TAG    0x2e
00138 #define DD_ADD_COMPOSE_RECUR_TAG    0x42
00139 #define DD_ADD_NON_SIM_COMPOSE_TAG    0x46
00140 #define DD_EQUIV_DC_TAG       0x4a
00141 #define DD_ZDD_ITE_TAG        0x4e
00142 #define DD_ADD_ITE_CONSTANT_TAG     0x62
00143 #define DD_ADD_EVAL_CONST_TAG     0x66
00144 #define DD_BDD_ITE_CONSTANT_TAG     0x6a
00145 
00146 /*---------------------------------------------------------------------------*/
00147 /* Stucture declarations                                                     */
00148 /*---------------------------------------------------------------------------*/
00149 
00150 
00151 /*---------------------------------------------------------------------------*/
00152 /* Type declarations                                                         */
00153 /*---------------------------------------------------------------------------*/
00154 
00155 /* Hooks in CUDD are functions that the application registers with the
00156 ** manager so that they are called at appropriate times. The functions
00157 ** are passed the manager as argument; they should return 1 if
00158 ** successful and 0 otherwise.
00159 */
00160 typedef struct DdHook {   /* hook list element */
00161     int (*f) ARGS((DdManager *, char *, void *)); /* function to be called */
00162     struct DdHook *next;  /* next element in the list */
00163 } DdHook;
00164 
00165 #if SIZEOF_VOID_P == 8 && SIZEOF_INT == 4
00166 typedef long ptrint;
00167 typedef unsigned long ptruint;
00168 #else
00169 typedef int ptrint;
00170 typedef unsigned int ptruint;
00171 #endif
00172 
00173 #ifdef __osf__
00174 #pragma pointer_size save
00175 #pragma pointer_size short
00176 #endif
00177 
00178 typedef DdNode *DdNodePtr;
00179 
00180 /* Generic local cache item. */
00181 typedef struct DdLocalCacheItem {
00182     DdNode *value;
00183 #ifdef DD_CACHE_PROFILE
00184     ptrint count;
00185 #endif
00186     DdNode *key[1];
00187 } DdLocalCacheItem;
00188 
00189 /* Local cache. */
00190 typedef struct DdLocalCache {
00191     DdLocalCacheItem *item;
00192     unsigned int itemsize;
00193     unsigned int keysize;
00194     unsigned int slots;
00195     int shift;
00196     double lookUps;
00197     double minHit;
00198     double hits;
00199     unsigned int maxslots;
00200     DdManager *manager;
00201     struct DdLocalCache *next;
00202 } DdLocalCache;
00203 
00204 /* Generic hash item. */
00205 typedef struct DdHashItem {
00206     struct DdHashItem *next;
00207     ptrint count;
00208     DdNode *value;
00209     DdNode *key[1];
00210 } DdHashItem;
00211 
00212 /* Local hash table */
00213 typedef struct DdHashTable {
00214     unsigned int keysize;
00215     unsigned int itemsize;
00216     DdHashItem **bucket;
00217     DdHashItem *nextFree;
00218     DdHashItem **memoryList;
00219     unsigned int numBuckets;
00220     int shift;
00221     unsigned int size;
00222     unsigned int maxsize;
00223     DdManager *manager;
00224 } DdHashTable;
00225 
00226 typedef struct DdCache {
00227     DdNode *f,*g;   /* DDs */
00228     ptruint h;      /* either operator or DD */
00229     DdNode *data;   /* already constructed DD */
00230 #ifdef DD_CACHE_PROFILE
00231     ptrint count;
00232 #endif
00233 } DdCache;
00234 
00235 typedef struct DdSubtable { /* subtable for one index */
00236     DdNode **nodelist;    /* hash table */
00237     int shift;      /* shift for hash function */
00238     unsigned int slots;   /* size of the hash table */
00239     unsigned int keys;    /* number of nodes stored in this table */
00240     unsigned int maxKeys; /* slots * DD_MAX_SUBTABLE_DENSITY */
00241     unsigned int dead;    /* number of dead nodes in this table */
00242     unsigned int next;    /* index of next variable in group */
00243 } DdSubtable;
00244 
00245 struct DdManager {  /* specialized DD symbol table */
00246     /* Constants */
00247     DdNode sentinel;    /* for collision lists */
00248     DdNode *one;    /* constant 1 */
00249     DdNode *zero;   /* constant 0 */
00250     DdNode *plusinfinity; /* plus infinity */
00251     DdNode *minusinfinity;  /* minus infinity */
00252     DdNode *background;   /* background value */
00253     /* Computed Table */
00254     DdCache *acache;    /* address of allocated memory for cache */
00255     DdCache *cache;   /* the cache-based computed table */
00256     unsigned int cacheSlots;  /* total number of cache entries */
00257     int cacheShift;   /* shift value for cache hash function */
00258     double cacheMisses;   /* number of cache misses (since resizing) */
00259     double cacheHits;   /* number of cache hits (since resizing) */
00260     double minHit;    /* hit percentage above which to resize */
00261     int cacheSlack;   /* slots still available for resizing */
00262     unsigned int maxCacheHard;  /* hard limit for cache size */
00263     /* Unique Table */
00264     int size;     /* number of unique subtables */
00265     int sizeZ;      /* for ZDD */
00266     int maxSize;    /* max number of subtables before resizing */
00267     int maxSizeZ;   /* for ZDD */
00268     DdSubtable *subtables;  /* array of unique subtables */
00269     DdSubtable *subtableZ;  /* for ZDD */
00270     DdSubtable constants; /* unique subtable for the constants */
00271     unsigned int slots;   /* total number of hash buckets */
00272     unsigned int keys;    /* total number of BDD and ADD nodes */
00273     unsigned int keysZ;   /* total number of ZDD nodes */
00274     unsigned int dead;    /* total number of dead BDD and ADD nodes */
00275     unsigned int deadZ;   /* total number of dead ZDD nodes */
00276     unsigned int maxLive; /* maximum number of live nodes */
00277     unsigned int minDead; /* do not GC if fewer than these dead */
00278     double gcFrac;    /* gc when this fraction is dead */
00279     int gcEnabled;    /* gc is enabled */
00280     unsigned int looseUpTo; /* slow growth beyond this limit */
00281         /* (measured w.r.t. slots, not keys) */
00282     unsigned int initSlots; /* initial size of a subtable */
00283     DdNode **stack;   /* stack for iterative procedures */
00284     double allocated;   /* number of nodes allocated */
00285         /* (not during reordering) */
00286     double reclaimed;   /* number of nodes brought back from the dead */
00287     int isolated;   /* isolated projection functions */
00288     int *perm;      /* current variable perm. (index to level) */
00289     int *permZ;     /* for ZDD */
00290     int *invperm;   /* current inv. var. perm. (level to index) */
00291     int *invpermZ;    /* for ZDD */
00292     DdNode **vars;    /* projection functions */
00293     int *map;     /* variable map for fast swap */
00294     DdNode **univ;    /* ZDD 1 for each variable */
00295     int linearSize;   /* number of rows and columns of linear */
00296     long *interact;   /* interacting variable matrix */
00297     long *linear;   /* linear transform matrix */
00298     /* Memory Management */
00299     DdNode **memoryList;  /* memory manager for symbol table */
00300     DdNode *nextFree;   /* list of free nodes */
00301     char *stash;    /* memory reserve */
00302 #ifndef DD_NO_DEATH_ROW
00303     DdNode **deathRow;    /* queue for dereferencing */
00304     int deathRowDepth;    /* number of slots in the queue */
00305     int nextDead;   /* index in the queue */
00306     unsigned deadMask;    /* mask for circular index update */
00307 #endif
00308     /* General Parameters */
00309     CUDD_VALUE_TYPE epsilon;  /* tolerance on comparisons */
00310     /* Dynamic Reordering Parameters */
00311     int reordered;    /* flag set at the end of reordering */
00312     int reorderings;    /* number of calls to Cudd_ReduceHeap */
00313     int siftMaxVar;   /* maximum number of vars sifted */
00314     int siftMaxSwap;    /* maximum number of swaps per sifting */
00315     double maxGrowth;   /* maximum growth during reordering */
00316     int autoDyn;    /* automatic dynamic reordering flag (BDD) */
00317     int autoDynZ;   /* automatic dynamic reordering flag (ZDD) */
00318     Cudd_ReorderingType autoMethod;  /* default reordering method */
00319     Cudd_ReorderingType autoMethodZ; /* default reordering method (ZDD) */
00320     int realign;    /* realign ZDD order after BDD reordering */
00321     int realignZ;   /* realign BDD order after ZDD reordering */
00322     unsigned int nextDyn; /* reorder if this size is reached */
00323     unsigned int countDead; /* if 0, count deads to trigger reordering */
00324     MtrNode *tree;    /* Variable group tree (BDD) */
00325     MtrNode *treeZ;   /* Variable group tree (ZDD) */
00326     Cudd_AggregationType groupcheck; /* Used during group sifting */
00327     int recomb;     /* Used during group sifting */
00328     int symmviolation;    /* Used during group sifting */
00329     int arcviolation;   /* Used during group sifting */
00330     int populationSize;   /* population size for GA */
00331     int numberXovers;   /* number of crossovers for GA */
00332     DdLocalCache *localCaches;  /* local caches currently in existence */
00333 #ifdef __osf__
00334 #pragma pointer_size restore
00335 #endif
00336     char *hooks;    /* application-specific field (used by vis) */
00337     DdHook *preGCHook;    /* hooks to be called before GC */
00338     DdHook *postGCHook;   /* hooks to be called after GC */
00339     DdHook *preReorderingHook;  /* hooks to be called before reordering */
00340     DdHook *postReorderingHook; /* hooks to be called after reordering */
00341     FILE *out;      /* stdout for this manager */
00342     FILE *err;      /* stderr for this manager */
00343 #ifdef __osf__
00344 #pragma pointer_size save
00345 #pragma pointer_size short
00346 #endif
00347     Cudd_ErrorType errorCode; /* info on last error */
00348     /* Statistical counters. */
00349     long memused;   /* total memory allocated for the manager */
00350     long maxmem;    /* target maximum memory */
00351     long maxmemhard;    /* hard limit for maximum memory */
00352     int garbageCollections; /* number of garbage collections */
00353     long GCTime;    /* total time spent in garbage collection */
00354     long reordTime;   /* total time spent in reordering */
00355     double totCachehits;  /* total number of cache hits */
00356     double totCacheMisses;  /* total number of cache misses */
00357     double cachecollisions; /* number of cache collisions */
00358     double cacheinserts;  /* number of cache insertions */
00359     double cacheLastInserts;  /* insertions at the last cache resizing */
00360     double cachedeletions;  /* number of deletions during garbage coll. */
00361 #ifdef DD_STATS
00362     double nodesFreed;    /* number of nodes returned to the free list */
00363     double nodesDropped;  /* number of nodes killed by dereferencing */
00364 #endif
00365     unsigned int peakLiveNodes; /* maximum number of live nodes */
00366 #ifdef DD_UNIQUE_PROFILE
00367     double uniqueLookUps; /* number of unique table lookups */
00368     double uniqueLinks;   /* total distance traveled in coll. chains */
00369 #endif
00370 #ifdef DD_COUNT
00371     double recursiveCalls;  /* number of recursive calls */
00372 #ifdef DD_STATS
00373     double nextSample;    /* when to write next line of stats */
00374 #endif
00375     double swapSteps;   /* number of elementary reordering steps */
00376 #endif
00377 #ifdef DD_MIS
00378     /* mis/verif compatibility fields */
00379     array_t *iton;    /* maps ids in ddNode to node_t */
00380     array_t *order;   /* copy of order_list */
00381     lsHandle handle;    /* where it is in network BDD list */
00382     network_t *network;
00383     st_table *local_order;  /* for local BDDs */
00384     int nvars;      /* variables used so far */
00385     int threshold;    /* for pseudo var threshold value*/
00386 #endif
00387 };
00388 
00389 typedef struct Move {
00390     DdHalfWord x;
00391     DdHalfWord y;
00392     unsigned int flags;
00393     int size;
00394     struct Move *next;
00395 } Move;
00396 
00397 /* Generic level queue item. */
00398 typedef struct DdQueueItem {
00399     struct DdQueueItem *next;
00400     struct DdQueueItem *cnext;
00401     void *key;
00402 } DdQueueItem;
00403 
00404 /* Level queue. */
00405 typedef struct DdLevelQueue {
00406     void *first;
00407     DdQueueItem **last;
00408     DdQueueItem *freelist;
00409     DdQueueItem **buckets;
00410     int levels;
00411     int itemsize;
00412     int size;
00413     int maxsize;
00414     int numBuckets;
00415     int shift;
00416 } DdLevelQueue;
00417 
00418 #ifdef __osf__
00419 #pragma pointer_size restore
00420 #endif
00421 
00422 /*---------------------------------------------------------------------------*/
00423 /* Variable declarations                                                     */
00424 /*---------------------------------------------------------------------------*/
00425 
00426 
00427 /*---------------------------------------------------------------------------*/
00428 /* Macro declarations                                                        */
00429 /*---------------------------------------------------------------------------*/
00430 
00444 #define cuddDeallocNode(unique,node) \
00445     (node)->next = (unique)->nextFree; \
00446     (unique)->nextFree = node;
00447 
00448 
00463 #define cuddRef(n) cuddSatInc(Cudd_Regular(n)->ref)
00464 
00465 
00483 #define cuddDeref(n) cuddSatDec(Cudd_Regular(n)->ref)
00484 
00485 
00499 #define cuddIsConstant(node) ((node)->index == CUDD_MAXINDEX)
00500 
00501 
00515 #define cuddT(node) ((node)->type.kids.T)
00516 
00517 
00531 #define cuddE(node) ((node)->type.kids.E)
00532 
00533 
00547 #define cuddV(node) ((node)->type.value)
00548 
00549 
00565 #define cuddI(dd,index) (((index)==CUDD_MAXINDEX)?(int)(index):(dd)->perm[(index)])
00566 
00567 
00583 #define cuddIZ(dd,index) (((index)==CUDD_MAXINDEX)?(int)(index):(dd)->permZ[(index)])
00584 
00585 
00597 #if SIZEOF_VOID_P == 8 && SIZEOF_INT == 4
00598 #define ddHash(f,g,s) \
00599 ((((unsigned)(unsigned long)(f) * DD_P1 + \
00600    (unsigned)(unsigned long)(g)) * DD_P2) >> (s))
00601 #else
00602 #define ddHash(f,g,s) \
00603 ((((unsigned)(f) * DD_P1 + (unsigned)(g)) * DD_P2) >> (s))
00604 #endif
00605 
00606 
00618 #if SIZEOF_VOID_P == 8 && SIZEOF_INT == 4
00619 #define ddCHash(o,f,g,h,s) \
00620 ((((((unsigned)(unsigned long)(f) + (unsigned)(unsigned long)(o)) * DD_P1 + \
00621     (unsigned)(unsigned long)(g)) * DD_P2 + \
00622    (unsigned)(unsigned long)(h)) * DD_P3) >> (s))
00623 #else
00624 #define ddCHash(o,f,g,h,s) \
00625 ((((((unsigned)(f) + (unsigned)(o)) * DD_P1 + (unsigned)(g)) * DD_P2 + \
00626    (unsigned)(h)) * DD_P3) >> (s))
00627 #endif
00628 
00629 
00642 #if SIZEOF_VOID_P == 8 && SIZEOF_INT == 4
00643 #define ddCHash2(o,f,g,s) \
00644 (((((unsigned)(unsigned long)(f) + (unsigned)(unsigned long)(o)) * DD_P1 + \
00645    (unsigned)(unsigned long)(g)) * DD_P2) >> (s))
00646 #else
00647 #define ddCHash2(o,f,g,s) \
00648 (((((unsigned)(f) + (unsigned)(o)) * DD_P1 + (unsigned)(g)) * DD_P2) >> (s))
00649 #endif
00650 
00651 
00663 #define cuddClean(p) ((DdNode *)((ptruint)(p) & ~0xf))
00664 
00665 
00677 #define ddMin(x,y) (((y) < (x)) ? (y) : (x))
00678 
00679 
00691 #define ddMax(x,y) (((y) > (x)) ? (y) : (x))
00692 
00693 
00705 #define ddAbs(x) (((x)<0) ? -(x) : (x))
00706 
00707 
00720 #define ddEqualVal(x,y,e) (ddAbs((x)-(y))<(e))
00721 
00722 
00734 #if SIZEOF_VOID_P == 8 && SIZEOF_INT == 4
00735 #define cuddSatInc(x) ((x)++)
00736 #else
00737 #define cuddSatInc(x) ((x) += (x) != (DdHalfWord)DD_MAXREF)
00738 #endif
00739 
00740 
00752 #if SIZEOF_VOID_P == 8 && SIZEOF_INT == 4
00753 #define cuddSatDec(x) ((x)--)
00754 #else
00755 #define cuddSatDec(x) ((x) -= (x) != (DdHalfWord)DD_MAXREF)
00756 #endif
00757 
00758 
00770 #define DD_ONE(dd)    ((dd)->one)
00771 
00772 
00786 #define DD_ZERO(dd) ((dd)->zero)
00787 
00788 
00800 #define DD_PLUS_INFINITY(dd) ((dd)->plusinfinity)
00801 
00802 
00814 #define DD_MINUS_INFINITY(dd) ((dd)->minusinfinity)
00815 
00816 
00835 #ifdef HAVE_IEEE_754
00836 #  define cuddAdjust(x)
00837 #else
00838 #  define cuddAdjust(x)   ((x) = ((x) >= DD_CRI_HI_MARK) ? DD_PLUS_INF_VAL : (((x) <= DD_CRI_LO_MARK) ? DD_MINUS_INF_VAL : (x)))
00839 #endif
00840 
00841 
00854 #define DD_LSDIGIT(x) ((x) & DD_APA_MASK)
00855 
00856 
00869 #define DD_MSDIGIT(x) ((x) >> DD_APA_BITS)
00870 
00871 
00885 #ifdef DD_COUNT
00886 #ifdef DD_STATS
00887 #define statLine(dd) dd->recursiveCalls++; \
00888 if (dd->recursiveCalls == dd->nextSample) {(void) fprintf(dd->err, \
00889 "@%.0f: %u nodes %u live %.0f dropped %.0f reclaimed\n", dd->recursiveCalls, \
00890 dd->keys, dd->keys - dd->dead, dd->nodesDropped, dd->reclaimed); \
00891 dd->nextSample += 250000;}
00892 #else
00893 #define statLine(dd) dd->recursiveCalls++;
00894 #endif
00895 #else
00896 #define statLine(dd)
00897 #endif
00898 
00899 
00902 /*---------------------------------------------------------------------------*/
00903 /* Function prototypes                                                       */
00904 /*---------------------------------------------------------------------------*/
00905 
00906 EXTERN DdNode * cuddAddExistAbstractRecur ARGS((DdManager *manager, DdNode *f, DdNode *cube));
00907 EXTERN DdNode * cuddAddUnivAbstractRecur ARGS((DdManager *manager, DdNode *f, DdNode *cube));
00908 EXTERN DdNode * cuddAddOrAbstractRecur ARGS((DdManager *manager, DdNode *f, DdNode *cube));
00909 EXTERN DdNode * cuddAddApplyRecur ARGS((DdManager *dd, DdNode * (*)(DdManager *, DdNode **, DdNode **), DdNode *f, DdNode *g));
00910 EXTERN DdNode * cuddAddScalarInverseRecur ARGS((DdManager *dd, DdNode *f, DdNode *epsilon));
00911 EXTERN DdNode * cuddAddIteRecur ARGS((DdManager *dd, DdNode *f, DdNode *g, DdNode *h));
00912 EXTERN DdNode * cuddAddCmplRecur ARGS((DdManager *dd, DdNode *f));
00913 EXTERN DdNode * cuddAddNegateRecur ARGS((DdManager *dd, DdNode *f));
00914 EXTERN DdNode * cuddAddRoundOffRecur ARGS((DdManager *dd, DdNode *f, double trunc));
00915 EXTERN DdNode * cuddUnderApprox ARGS((DdManager *dd, DdNode *f, int numVars, int threshold, int safe, double quality));
00916 EXTERN DdNode * cuddRemapUnderApprox ARGS((DdManager *dd, DdNode *f, int numVars, int threshold, double quality));
00917 EXTERN DdNode * cuddBiasedUnderApprox ARGS((DdManager *dd, DdNode *f, DdNode *b, int numVars, int threshold, double quality1, double quality0));
00918 EXTERN DdNode * cuddBddAndAbstractRecur ARGS((DdManager *manager, DdNode *f, DdNode *g, DdNode *cube));
00919 EXTERN int cuddAnnealing ARGS((DdManager *table, int lower, int upper));
00920 EXTERN DdNode * cuddBddExistAbstractRecur ARGS((DdManager *manager, DdNode *f, DdNode *cube));
00921 EXTERN DdNode * cuddBddXorExistAbstractRecur ARGS((DdManager *manager, DdNode *f, DdNode *g, DdNode *cube));
00922 EXTERN DdNode * cuddBddBooleanDiffRecur ARGS((DdManager *manager, DdNode *f, DdNode *var));
00923 EXTERN DdNode * cuddBddIteRecur ARGS((DdManager *dd, DdNode *f, DdNode *g, DdNode *h));
00924 EXTERN DdNode * cuddBddIntersectRecur ARGS((DdManager *dd, DdNode *f, DdNode *g));
00925 EXTERN DdNode * cuddBddAndRecur ARGS((DdManager *manager, DdNode *f, DdNode *g));
00926 EXTERN DdNode * cuddBddXorRecur ARGS((DdManager *manager, DdNode *f, DdNode *g));
00927 EXTERN DdNode * cuddBddTransfer ARGS((DdManager *ddS, DdManager *ddD, DdNode *f));
00928 EXTERN int cuddInitCache ARGS((DdManager *unique, unsigned int cacheSize, unsigned int maxCacheSize));
00929 EXTERN void cuddCacheInsert ARGS((DdManager *table, ptruint op, DdNode *f, DdNode *g, DdNode *h, DdNode *data));
00930 EXTERN void cuddCacheInsert2 ARGS((DdManager *table, DdNode * (*)(DdManager *, DdNode *, DdNode *), DdNode *f, DdNode *g, DdNode *data));
00931 EXTERN void cuddCacheInsert1 ARGS((DdManager *table, DdNode * (*)(DdManager *, DdNode *), DdNode *f, DdNode *data));
00932 EXTERN DdNode * cuddCacheLookup ARGS((DdManager *table, ptruint op, DdNode *f, DdNode *g, DdNode *h));
00933 EXTERN DdNode * cuddCacheLookupZdd ARGS((DdManager *table, ptruint op, DdNode *f, DdNode *g, DdNode *h));
00934 EXTERN DdNode * cuddCacheLookup2 ARGS((DdManager *table, DdNode * (*)(DdManager *, DdNode *, DdNode *), DdNode *f, DdNode *g));
00935 EXTERN DdNode * cuddCacheLookup1 ARGS((DdManager *table, DdNode * (*)(DdManager *, DdNode *), DdNode *f));
00936 EXTERN DdNode * cuddCacheLookup2Zdd ARGS((DdManager *table, DdNode * (*)(DdManager *, DdNode *, DdNode *), DdNode *f, DdNode *g));
00937 EXTERN DdNode * cuddCacheLookup1Zdd ARGS((DdManager *table, DdNode * (*)(DdManager *, DdNode *), DdNode *f));
00938 EXTERN DdNode * cuddConstantLookup ARGS((DdManager *table, ptruint op, DdNode *f, DdNode *g, DdNode *h));
00939 EXTERN int cuddCacheProfile ARGS((DdManager *table, FILE *fp));
00940 EXTERN void cuddCacheResize ARGS((DdManager *table));
00941 EXTERN void cuddCacheFlush ARGS((DdManager *table));
00942 EXTERN int cuddComputeFloorLog2 ARGS((unsigned int value));
00943 EXTERN int cuddHeapProfile ARGS((DdManager *dd));
00944 EXTERN void cuddPrintNode ARGS((DdNode *f, FILE *fp));
00945 EXTERN void cuddPrintVarGroups ARGS((DdManager * dd, MtrNode * root, int zdd, int silent));
00946 EXTERN DdNode * cuddBddClippingAnd ARGS((DdManager *dd, DdNode *f, DdNode *g, int maxDepth, int direction));
00947 EXTERN DdNode * cuddBddClippingAndAbstract ARGS((DdManager *dd, DdNode *f, DdNode *g, DdNode *cube, int maxDepth, int direction));
00948 EXTERN void cuddGetBranches ARGS((DdNode *g, DdNode **g1, DdNode **g0));
00949 EXTERN int cuddCheckCube ARGS((DdManager *dd, DdNode *g));
00950 EXTERN DdNode * cuddCofactorRecur ARGS((DdManager *dd, DdNode *f, DdNode *g));
00951 EXTERN DdNode * cuddBddComposeRecur ARGS((DdManager *dd, DdNode *f, DdNode *g, DdNode *proj));
00952 EXTERN DdNode * cuddAddComposeRecur ARGS((DdManager *dd, DdNode *f, DdNode *g, DdNode *proj));
00953 EXTERN int cuddExact ARGS((DdManager *table, int lower, int upper));
00954 EXTERN DdNode * cuddBddConstrainRecur ARGS((DdManager *dd, DdNode *f, DdNode *c));
00955 EXTERN DdNode * cuddBddRestrictRecur ARGS((DdManager *dd, DdNode *f, DdNode *c));
00956 EXTERN DdNode * cuddAddConstrainRecur ARGS((DdManager *dd, DdNode *f, DdNode *c));
00957 EXTERN DdNode * cuddAddRestrictRecur ARGS((DdManager *dd, DdNode *f, DdNode *c));
00958 EXTERN DdNode * cuddBddLICompaction ARGS((DdManager *dd, DdNode *f, DdNode *c));
00959 EXTERN int cuddGa ARGS((DdManager *table, int lower, int upper));
00960 EXTERN int cuddTreeSifting ARGS((DdManager *table, Cudd_ReorderingType method));
00961 EXTERN int cuddZddInitUniv ARGS((DdManager *zdd));
00962 EXTERN void cuddZddFreeUniv ARGS((DdManager *zdd));
00963 EXTERN void cuddSetInteract ARGS((DdManager *table, int x, int y));
00964 EXTERN int cuddTestInteract ARGS((DdManager *table, int x, int y));
00965 EXTERN int cuddInitInteract ARGS((DdManager *table));
00966 EXTERN DdLocalCache * cuddLocalCacheInit ARGS((DdManager *manager, unsigned int keySize, unsigned int cacheSize, unsigned int maxCacheSize));
00967 EXTERN void cuddLocalCacheQuit ARGS((DdLocalCache *cache));
00968 EXTERN void cuddLocalCacheInsert ARGS((DdLocalCache *cache, DdNodePtr *key, DdNode *value));
00969 EXTERN DdNode * cuddLocalCacheLookup ARGS((DdLocalCache *cache, DdNodePtr *key));
00970 EXTERN void cuddLocalCacheClearDead ARGS((DdManager *manager));
00971 EXTERN int cuddIsInDeathRow ARGS((DdManager *dd, DdNode *f));
00972 EXTERN int cuddTimesInDeathRow ARGS((DdManager *dd, DdNode *f));
00973 EXTERN void cuddLocalCacheClearAll ARGS((DdManager *manager));
00974 #ifdef DD_CACHE_PROFILE
00975 EXTERN int cuddLocalCacheProfile ARGS((DdLocalCache *cache));
00976 #endif
00977 EXTERN DdHashTable * cuddHashTableInit ARGS((DdManager *manager, unsigned int keySize, unsigned int initSize));
00978 EXTERN void cuddHashTableQuit ARGS((DdHashTable *hash));
00979 EXTERN int cuddHashTableInsert ARGS((DdHashTable *hash, DdNodePtr *key, DdNode *value, ptrint count));
00980 EXTERN DdNode * cuddHashTableLookup ARGS((DdHashTable *hash, DdNodePtr *key));
00981 EXTERN int cuddHashTableInsert1 ARGS((DdHashTable *hash, DdNode *f, DdNode *value, ptrint count));
00982 EXTERN DdNode * cuddHashTableLookup1 ARGS((DdHashTable *hash, DdNode *f));
00983 EXTERN int cuddHashTableInsert2 ARGS((DdHashTable *hash, DdNode *f, DdNode *g, DdNode *value, ptrint count));
00984 EXTERN DdNode * cuddHashTableLookup2 ARGS((DdHashTable *hash, DdNode *f, DdNode *g));
00985 EXTERN int cuddHashTableInsert3 ARGS((DdHashTable *hash, DdNode *f, DdNode *g, DdNode *h, DdNode *value, ptrint count));
00986 EXTERN DdNode * cuddHashTableLookup3 ARGS((DdHashTable *hash, DdNode *f, DdNode *g, DdNode *h));
00987 EXTERN DdLevelQueue * cuddLevelQueueInit ARGS((int levels, int itemSize, int numBuckets));
00988 EXTERN void cuddLevelQueueQuit ARGS((DdLevelQueue *queue));
00989 EXTERN void * cuddLevelQueueEnqueue ARGS((DdLevelQueue *queue, void *key, int level));
00990 EXTERN void cuddLevelQueueDequeue ARGS((DdLevelQueue *queue, int level));
00991 EXTERN int cuddLinearAndSifting ARGS((DdManager *table, int lower, int upper));
00992 EXTERN DdNode * cuddBddLiteralSetIntersectionRecur ARGS((DdManager *dd, DdNode *f, DdNode *g));
00993 EXTERN DdNode * cuddCProjectionRecur ARGS((DdManager *dd, DdNode *R, DdNode *Y, DdNode *Ysupp));
00994 EXTERN void cuddReclaim ARGS((DdManager *table, DdNode *n));
00995 EXTERN void cuddReclaimZdd ARGS((DdManager *table, DdNode *n));
00996 EXTERN void cuddClearDeathRow ARGS((DdManager *table));
00997 EXTERN void cuddShrinkDeathRow ARGS((DdManager *table));
00998 EXTERN DdNode * cuddDynamicAllocNode ARGS((DdManager *table));
00999 EXTERN int cuddSifting ARGS((DdManager *table, int lower, int upper));
01000 EXTERN int cuddSwapping ARGS((DdManager *table, int lower, int upper, Cudd_ReorderingType heuristic));
01001 EXTERN int cuddNextHigh ARGS((DdManager *table, int x));
01002 EXTERN int cuddNextLow ARGS((DdManager *table, int x));
01003 EXTERN int cuddSwapInPlace ARGS((DdManager *table, int x, int y));
01004 EXTERN int cuddBddAlignToZdd ARGS((DdManager *table));
01005 EXTERN DdNode * cuddSolveEqnRecur ARGS((DdManager *bdd, DdNode *F, DdNode *Y, DdNode **G, int n, int *yIndex, int i));
01006 EXTERN DdNode * cuddVerifySol ARGS((DdManager *bdd, DdNode *F, DdNode **G, int *yIndex, int n));
01007 #ifdef ST_INCLUDED
01008 EXTERN DdNode* cuddSplitSetRecur ARGS((DdManager *manager, st_table *mtable, int *varSeen, DdNode *p, double n, double max, int index));
01009 #endif
01010 EXTERN DdNode * cuddSubsetHeavyBranch ARGS((DdManager *dd, DdNode *f, int numVars, int threshold));
01011 EXTERN DdNode * cuddSubsetShortPaths ARGS((DdManager *dd, DdNode *f, int numVars, int threshold, int hardlimit));
01012 EXTERN int cuddSymmCheck ARGS((DdManager *table, int x, int y));
01013 EXTERN int cuddSymmSifting ARGS((DdManager *table, int lower, int upper));
01014 EXTERN int cuddSymmSiftingConv ARGS((DdManager *table, int lower, int upper));
01015 EXTERN DdNode * cuddAllocNode ARGS((DdManager *unique));
01016 EXTERN DdManager * cuddInitTable ARGS((unsigned int numVars, unsigned int numVarsZ, unsigned int numSlots, unsigned int looseUpTo));
01017 EXTERN void cuddFreeTable ARGS((DdManager *unique));
01018 EXTERN int cuddGarbageCollect ARGS((DdManager *unique, int clearCache));
01019 EXTERN int cuddGarbageCollectZdd ARGS((DdManager *unique, int clearCache));
01020 EXTERN DdNode * cuddZddGetNode ARGS((DdManager *zdd, int id, DdNode *T, DdNode *E));
01021 EXTERN DdNode * cuddZddGetNodeIVO ARGS((DdManager *dd, int index, DdNode *g, DdNode *h));
01022 EXTERN DdNode * cuddUniqueInter ARGS((DdManager *unique, int index, DdNode *T, DdNode *E));
01023 EXTERN DdNode * cuddUniqueInterIVO ARGS((DdManager *unique, int index, DdNode *T, DdNode *E));
01024 EXTERN DdNode * cuddUniqueInterZdd ARGS((DdManager *unique, int index, DdNode *T, DdNode *E));
01025 EXTERN DdNode * cuddUniqueConst ARGS((DdManager *unique, CUDD_VALUE_TYPE value));
01026 EXTERN void cuddRehash ARGS((DdManager *unique, int i));
01027 EXTERN void cuddShrinkSubtable ARGS((DdManager *unique, int i));
01028 EXTERN int cuddInsertSubtables ARGS((DdManager *unique, int n, int level));
01029 EXTERN int cuddDestroySubtables ARGS((DdManager *unique, int n));
01030 EXTERN int cuddResizeTableZdd ARGS((DdManager *unique, int index));
01031 EXTERN void cuddSlowTableGrowth ARGS((DdManager *unique));
01032 EXTERN int cuddP ARGS((DdManager *dd, DdNode *f));
01033 #ifdef ST_INCLUDED
01034 EXTERN enum st_retval cuddStCountfree ARGS((char *key, char *value, char *arg));
01035 EXTERN int cuddCollectNodes ARGS((DdNode *f, st_table *visited));
01036 #endif
01037 EXTERN int cuddWindowReorder ARGS((DdManager *table, int low, int high, Cudd_ReorderingType submethod));
01038 EXTERN DdNode * cuddZddProduct ARGS((DdManager *dd, DdNode *f, DdNode *g));
01039 EXTERN DdNode * cuddZddUnateProduct ARGS((DdManager *dd, DdNode *f, DdNode *g));
01040 EXTERN DdNode * cuddZddWeakDiv ARGS((DdManager *dd, DdNode *f, DdNode *g));
01041 EXTERN DdNode * cuddZddWeakDivF ARGS((DdManager *dd, DdNode *f, DdNode *g));
01042 EXTERN DdNode * cuddZddDivide ARGS((DdManager *dd, DdNode *f, DdNode *g));
01043 EXTERN DdNode * cuddZddDivideF ARGS((DdManager *dd, DdNode *f, DdNode *g));
01044 EXTERN int cuddZddGetCofactors3 ARGS((DdManager *dd, DdNode *f, int v, DdNode **f1, DdNode **f0, DdNode **fd));
01045 EXTERN int cuddZddGetCofactors2 ARGS((DdManager *dd, DdNode *f, int v, DdNode **f1, DdNode **f0));
01046 EXTERN DdNode * cuddZddComplement ARGS((DdManager *dd, DdNode *node));
01047 EXTERN int cuddZddGetPosVarIndex(DdManager * dd, int index);
01048 EXTERN int cuddZddGetNegVarIndex(DdManager * dd, int index);
01049 EXTERN int cuddZddGetPosVarLevel(DdManager * dd, int index);
01050 EXTERN int cuddZddGetNegVarLevel(DdManager * dd, int index);
01051 EXTERN int cuddZddTreeSifting ARGS((DdManager *table, Cudd_ReorderingType method));
01052 EXTERN DdNode * cuddZddIsop ARGS((DdManager *dd, DdNode *L, DdNode *U, DdNode **zdd_I));
01053 EXTERN DdNode * cuddBddIsop ARGS((DdManager *dd, DdNode *L, DdNode *U));
01054 EXTERN DdNode * cuddMakeBddFromZddCover ARGS((DdManager *dd, DdNode *node));
01055 EXTERN int cuddZddLinearSifting ARGS((DdManager *table, int lower, int upper));
01056 EXTERN int cuddZddAlignToBdd ARGS((DdManager *table));
01057 EXTERN int cuddZddNextHigh ARGS((DdManager *table, int x));
01058 EXTERN int cuddZddNextLow ARGS((DdManager *table, int x));
01059 EXTERN int cuddZddUniqueCompare ARGS((int *ptr_x, int *ptr_y));
01060 EXTERN int cuddZddSwapInPlace ARGS((DdManager *table, int x, int y));
01061 EXTERN int cuddZddSwapping ARGS((DdManager *table, int lower, int upper, Cudd_ReorderingType heuristic));
01062 EXTERN int cuddZddSifting ARGS((DdManager *table, int lower, int upper));
01063 EXTERN DdNode * cuddZddIte ARGS((DdManager *dd, DdNode *f, DdNode *g, DdNode *h));
01064 EXTERN DdNode * cuddZddUnion ARGS((DdManager *zdd, DdNode *P, DdNode *Q));
01065 EXTERN DdNode * cuddZddIntersect ARGS((DdManager *zdd, DdNode *P, DdNode *Q));
01066 EXTERN DdNode * cuddZddDiff ARGS((DdManager *zdd, DdNode *P, DdNode *Q));
01067 EXTERN DdNode * cuddZddChangeAux ARGS((DdManager *zdd, DdNode *P, DdNode *zvar));
01068 EXTERN DdNode * cuddZddSubset1 ARGS((DdManager *dd, DdNode *P, int var));
01069 EXTERN DdNode * cuddZddSubset0 ARGS((DdManager *dd, DdNode *P, int var));
01070 EXTERN DdNode * cuddZddChange ARGS((DdManager *dd, DdNode *P, int var));
01071 EXTERN int cuddZddSymmCheck ARGS((DdManager *table, int x, int y));
01072 EXTERN int cuddZddSymmSifting ARGS((DdManager *table, int lower, int upper));
01073 EXTERN int cuddZddSymmSiftingConv ARGS((DdManager *table, int lower, int upper));
01074 EXTERN int cuddZddP ARGS((DdManager *zdd, DdNode *f));
01075 
01078 #endif /* _CUDDINT */