abc70930: src/bdd/cudd/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 #include "st.h"
00048 
00049 #if defined(__GNUC__)
00050 # define DD_INLINE __inline__
00051 # if (__GNUC__ >2 || __GNUC_MINOR__ >=7)
00052 #   define DD_UNUSED __attribute__ ((__unused__))
00053 # else
00054 #   define DD_UNUSED
00055 # endif
00056 #else
00057 # if defined(__cplusplus)
00058 #   define DD_INLINE inline
00059 # else
00060 #   define DD_INLINE
00061 # endif
00062 # define DD_UNUSED
00063 #endif
00064 
00065 
00066 /*---------------------------------------------------------------------------*/
00067 /* Constant declarations                                                     */
00068 /*---------------------------------------------------------------------------*/
00069 
00070 #define DD_MAXREF               ((DdHalfWord) ~0)
00071 
00072 #define DD_DEFAULT_RESIZE       10      /* how many extra variables */
00073                                         /* should be added when resizing */
00074 #define DD_MEM_CHUNK            1022
00075 
00076 /* These definitions work for CUDD_VALUE_TYPE == double */
00077 #define DD_ONE_VAL              (1.0)
00078 #define DD_ZERO_VAL             (0.0)
00079 #define DD_EPSILON              (1.0e-12)
00080 
00081 /* The definitions of +/- infinity in terms of HUGE_VAL work on
00082 ** the DECstations and on many other combinations of OS/compiler.
00083 */
00084 #ifdef HAVE_IEEE_754
00085 #  define DD_PLUS_INF_VAL       (HUGE_VAL)
00086 #else
00087 #  define DD_PLUS_INF_VAL       (10e301)
00088 #  define DD_CRI_HI_MARK        (10e150)
00089 #  define DD_CRI_LO_MARK        (-(DD_CRI_HI_MARK))
00090 #endif
00091 #define DD_MINUS_INF_VAL        (-(DD_PLUS_INF_VAL))
00092 
00093 #define DD_NON_CONSTANT         ((DdNode *) 1)  /* for Cudd_bddIteConstant */
00094 
00095 /* Unique table and cache management constants. */
00096 #define DD_MAX_SUBTABLE_DENSITY 4       /* tells when to resize a subtable */
00097 /* gc when this percent are dead (measured w.r.t. slots, not keys)
00098 ** The first limit (LO) applies normally. The second limit applies when
00099 ** the package believes more space for the unique table (i.e., more dead
00100 ** nodes) would improve performance, and the unique table is not already
00101 ** too large. The third limit applies when memory is low.
00102 */
00103 #define DD_GC_FRAC_LO           DD_MAX_SUBTABLE_DENSITY * 0.25
00104 #define DD_GC_FRAC_HI           DD_MAX_SUBTABLE_DENSITY * 1.0
00105 #define DD_GC_FRAC_MIN          0.2
00106 #define DD_MIN_HIT              30      /* resize cache when hit ratio
00107                                            above this percentage (default) */
00108 #define DD_MAX_LOOSE_FRACTION   5 /* 1 / (max fraction of memory used for
00109                                      unique table in fast growth mode) */
00110 #define DD_MAX_CACHE_FRACTION   3 /* 1 / (max fraction of memory used for
00111                                      computed table if resizing enabled) */
00112 #define DD_STASH_FRACTION       64 /* 1 / (fraction of memory set
00113                                       aside for emergencies) */
00114 #define DD_MAX_CACHE_TO_SLOTS_RATIO 4 /* used to limit the cache size */
00115 
00116 /* Variable ordering default parameter values. */
00117 #define DD_SIFT_MAX_VAR         1000
00118 #define DD_SIFT_MAX_SWAPS       2000000
00119 #define DD_DEFAULT_RECOMB       0
00120 #define DD_MAX_REORDER_GROWTH   1.2
00121 #define DD_FIRST_REORDER        4004    /* 4 for the constants */
00122 #define DD_DYN_RATIO            2       /* when to dynamically reorder */
00123 
00124 /* Primes for cache hash functions. */
00125 #define DD_P1                   12582917
00126 #define DD_P2                   4256249
00127 #define DD_P3                   741457
00128 #define DD_P4                   1618033999
00129 
00130 /* Cache tags for 3-operand operators.  These tags are stored in the
00131 ** least significant bits of the cache operand pointers according to
00132 ** the following scheme.  The tag consists of two hex digits.  Both digits
00133 ** must be even, so that they do not interfere with complementation bits.
00134 ** The least significant one is stored in Bits 3:1 of the f operand in the
00135 ** cache entry.  Bit 1 is always 1, so that we can differentiate
00136 ** three-operand operations from one- and two-operand operations.
00137 ** Therefore, the least significant digit is one of {2,6,a,e}.  The most
00138 ** significant digit occupies Bits 3:1 of the g operand in the cache
00139 ** entry.  It can by any even digit between 0 and e.  This gives a total
00140 ** of 5 bits for the tag proper, which means a maximum of 32 three-operand
00141 ** operations. */
00142 #define DD_ADD_ITE_TAG                          0x02
00143 #define DD_BDD_AND_ABSTRACT_TAG                 0x06
00144 #define DD_BDD_XOR_EXIST_ABSTRACT_TAG           0x0a
00145 #define DD_BDD_ITE_TAG                          0x0e
00146 #define DD_ADD_BDD_DO_INTERVAL_TAG              0x22
00147 #define DD_BDD_CLIPPING_AND_ABSTRACT_UP_TAG     0x26
00148 #define DD_BDD_CLIPPING_AND_ABSTRACT_DOWN_TAG   0x2a
00149 #define DD_BDD_COMPOSE_RECUR_TAG                0x2e
00150 #define DD_ADD_COMPOSE_RECUR_TAG                0x42
00151 #define DD_ADD_NON_SIM_COMPOSE_TAG              0x46
00152 #define DD_EQUIV_DC_TAG                         0x4a
00153 #define DD_ZDD_ITE_TAG                          0x4e
00154 #define DD_ADD_ITE_CONSTANT_TAG                 0x62
00155 #define DD_ADD_EVAL_CONST_TAG                   0x66
00156 #define DD_BDD_ITE_CONSTANT_TAG                 0x6a
00157 #define DD_ADD_OUT_SUM_TAG                      0x6e
00158 #define DD_BDD_LEQ_UNLESS_TAG                   0x82
00159 #define DD_ADD_TRIANGLE_TAG                     0x86
00160 
00161 /* Generator constants. */
00162 #define CUDD_GEN_CUBES 0
00163 #define CUDD_GEN_NODES 1
00164 #define CUDD_GEN_ZDD_PATHS 2
00165 #define CUDD_GEN_EMPTY 0
00166 #define CUDD_GEN_NONEMPTY 1
00167 
00168 
00169 /*---------------------------------------------------------------------------*/
00170 /* Stucture declarations                                                     */
00171 /*---------------------------------------------------------------------------*/
00172 
00173 struct DdGen {
00174     DdManager   *manager;
00175     int         type;
00176     int         status;
00177     union {
00178         struct {
00179             int                 *cube;
00180             CUDD_VALUE_TYPE     value;
00181         } cubes;
00182         struct {
00183             st_table            *visited;
00184             st_generator        *stGen;
00185         } nodes;
00186     } gen;
00187     struct {
00188         int     sp;
00189         DdNode  **stack;
00190     } stack;
00191     DdNode      *node;
00192 };
00193 
00194 /*---------------------------------------------------------------------------*/
00195 /* Type declarations                                                         */
00196 /*---------------------------------------------------------------------------*/
00197 
00198 /* Hooks in CUDD are functions that the application registers with the
00199 ** manager so that they are called at appropriate times. The functions
00200 ** are passed the manager as argument; they should return 1 if
00201 ** successful and 0 otherwise.
00202 */
00203 typedef struct DdHook {         /* hook list element */
00204     int (*f) ARGS((DdManager *, char *, void *)); /* function to be called */
00205     struct DdHook *next;        /* next element in the list */
00206 } DdHook;
00207 
00208 #if SIZEOF_VOID_P == 8 && SIZEOF_INT == 4
00209 typedef long ptrint;
00210 typedef unsigned long ptruint;
00211 #else
00212 typedef int ptrint;
00213 typedef unsigned int ptruint;
00214 #endif
00215 
00216 #ifdef __osf__
00217 #pragma pointer_size save
00218 #pragma pointer_size short
00219 #endif
00220 
00221 typedef DdNode *DdNodePtr;
00222 
00223 /* Generic local cache item. */
00224 typedef struct DdLocalCacheItem {
00225     DdNode *value;
00226 #ifdef DD_CACHE_PROFILE
00227     ptrint count;
00228 #endif
00229     DdNode *key[1];
00230 } DdLocalCacheItem;
00231 
00232 /* Local cache. */
00233 typedef struct DdLocalCache {
00234     DdLocalCacheItem *item;
00235     unsigned int itemsize;
00236     unsigned int keysize;
00237     unsigned int slots;
00238     int shift;
00239     double lookUps;
00240     double minHit;
00241     double hits;
00242     unsigned int maxslots;
00243     DdManager *manager;
00244     struct DdLocalCache *next;
00245 } DdLocalCache;
00246 
00247 /* Generic hash item. */
00248 typedef struct DdHashItem {
00249     struct DdHashItem *next;
00250     ptrint count;
00251     DdNode *value;
00252     DdNode *key[1];
00253 } DdHashItem;
00254 
00255 /* Local hash table */
00256 typedef struct DdHashTable {
00257     unsigned int keysize;
00258     unsigned int itemsize;
00259     DdHashItem **bucket;
00260     DdHashItem *nextFree;
00261     DdHashItem **memoryList;
00262     unsigned int numBuckets;
00263     int shift;
00264     unsigned int size;
00265     unsigned int maxsize;
00266     DdManager *manager;
00267 } DdHashTable;
00268 
00269 typedef struct DdCache {
00270     DdNode *f,*g;               /* DDs */
00271     ptruint h;                  /* either operator or DD */
00272     DdNode *data;               /* already constructed DD */
00273 #ifdef DD_CACHE_PROFILE
00274     ptrint count;
00275 #endif
00276 } DdCache;
00277 
00278 typedef struct DdSubtable {     /* subtable for one index */
00279     DdNode **nodelist;          /* hash table */
00280     int shift;                  /* shift for hash function */
00281     unsigned int slots;         /* size of the hash table */
00282     unsigned int keys;          /* number of nodes stored in this table */
00283     unsigned int maxKeys;       /* slots * DD_MAX_SUBTABLE_DENSITY */
00284     unsigned int dead;          /* number of dead nodes in this table */
00285     unsigned int next;          /* index of next variable in group */
00286     int bindVar;                /* flag to bind this variable to its level */
00287     /* Fields for lazy sifting. */
00288     Cudd_VariableType varType;  /* variable type (ps, ns, pi) */
00289     int pairIndex;              /* corresponding variable index (ps <-> ns) */
00290     int varHandled;             /* flag: 1 means variable is already handled */
00291     Cudd_LazyGroupType varToBeGrouped; /* tells what grouping to apply */
00292 } DdSubtable;
00293 
00294 struct DdManager {      /* specialized DD symbol table */
00295     /* Constants */
00296     DdNode sentinel;            /* for collision lists */
00297     DdNode *one;                /* constant 1 */
00298     DdNode *zero;               /* constant 0 */
00299     DdNode *plusinfinity;       /* plus infinity */
00300     DdNode *minusinfinity;      /* minus infinity */
00301     DdNode *background;         /* background value */
00302     /* Computed Table */
00303     DdCache *acache;            /* address of allocated memory for cache */
00304     DdCache *cache;             /* the cache-based computed table */
00305     unsigned int cacheSlots;    /* total number of cache entries */
00306     int cacheShift;             /* shift value for cache hash function */
00307     double cacheMisses;         /* number of cache misses (since resizing) */
00308     double cacheHits;           /* number of cache hits (since resizing) */
00309     double minHit;              /* hit percentage above which to resize */
00310     int cacheSlack;             /* slots still available for resizing */
00311     unsigned int maxCacheHard;  /* hard limit for cache size */
00312     /* Unique Table */
00313     int size;                   /* number of unique subtables */
00314     int sizeZ;                  /* for ZDD */
00315     int maxSize;                /* max number of subtables before resizing */
00316     int maxSizeZ;               /* for ZDD */
00317     DdSubtable *subtables;      /* array of unique subtables */
00318     DdSubtable *subtableZ;      /* for ZDD */
00319     DdSubtable constants;       /* unique subtable for the constants */
00320     unsigned int slots;         /* total number of hash buckets */
00321     unsigned int keys;          /* total number of BDD and ADD nodes */
00322     unsigned int keysZ;         /* total number of ZDD nodes */
00323     unsigned int dead;          /* total number of dead BDD and ADD nodes */
00324     unsigned int deadZ;         /* total number of dead ZDD nodes */
00325     unsigned int maxLive;       /* maximum number of live nodes */
00326     unsigned int minDead;       /* do not GC if fewer than these dead */
00327     double gcFrac;              /* gc when this fraction is dead */
00328     int gcEnabled;              /* gc is enabled */
00329     unsigned int looseUpTo;     /* slow growth beyond this limit */
00330                                 /* (measured w.r.t. slots, not keys) */
00331     unsigned int initSlots;     /* initial size of a subtable */
00332     DdNode **stack;             /* stack for iterative procedures */
00333     double allocated;           /* number of nodes allocated */
00334                                 /* (not during reordering) */
00335     double reclaimed;           /* number of nodes brought back from the dead */
00336     int isolated;               /* isolated projection functions */
00337     int *perm;                  /* current variable perm. (index to level) */
00338     int *permZ;                 /* for ZDD */
00339     int *invperm;               /* current inv. var. perm. (level to index) */
00340     int *invpermZ;              /* for ZDD */
00341     DdNode **vars;              /* projection functions */
00342     int *map;                   /* variable map for fast swap */
00343     DdNode **univ;              /* ZDD 1 for each variable */
00344     int linearSize;             /* number of rows and columns of linear */
00345     long *interact;             /* interacting variable matrix */
00346     long *linear;               /* linear transform matrix */
00347     /* Memory Management */
00348     DdNode **memoryList;        /* memory manager for symbol table */
00349     DdNode *nextFree;           /* list of free nodes */
00350     char *stash;                /* memory reserve */
00351 #ifndef DD_NO_DEATH_ROW
00352     DdNode **deathRow;          /* queue for dereferencing */
00353     int deathRowDepth;          /* number of slots in the queue */
00354     int nextDead;               /* index in the queue */
00355     unsigned deadMask;          /* mask for circular index update */
00356 #endif
00357     /* General Parameters */
00358     CUDD_VALUE_TYPE epsilon;    /* tolerance on comparisons */
00359     /* Dynamic Reordering Parameters */
00360     int reordered;              /* flag set at the end of reordering */
00361     int reorderings;            /* number of calls to Cudd_ReduceHeap */
00362     int siftMaxVar;             /* maximum number of vars sifted */
00363     int siftMaxSwap;            /* maximum number of swaps per sifting */
00364     double maxGrowth;           /* maximum growth during reordering */
00365     double maxGrowthAlt;        /* alternate maximum growth for reordering */
00366     int reordCycle;             /* how often to apply alternate threshold */
00367     int autoDyn;                /* automatic dynamic reordering flag (BDD) */
00368     int autoDynZ;               /* automatic dynamic reordering flag (ZDD) */
00369     Cudd_ReorderingType autoMethod;  /* default reordering method */
00370     Cudd_ReorderingType autoMethodZ; /* default reordering method (ZDD) */
00371     int realign;                /* realign ZDD order after BDD reordering */
00372     int realignZ;               /* realign BDD order after ZDD reordering */
00373     unsigned int nextDyn;       /* reorder if this size is reached */
00374     unsigned int countDead;     /* if 0, count deads to trigger reordering */
00375     MtrNode *tree;              /* Variable group tree (BDD) */
00376     MtrNode *treeZ;             /* Variable group tree (ZDD) */
00377     Cudd_AggregationType groupcheck; /* Used during group sifting */
00378     int recomb;                 /* Used during group sifting */
00379     int symmviolation;          /* Used during group sifting */
00380     int arcviolation;           /* Used during group sifting */
00381     int populationSize;         /* population size for GA */
00382     int numberXovers;           /* number of crossovers for GA */
00383     DdLocalCache *localCaches;  /* local caches currently in existence */
00384 #ifdef __osf__
00385 #pragma pointer_size restore
00386 #endif
00387     char *hooks;                /* application-specific field (used by vis) */
00388     DdHook *preGCHook;          /* hooks to be called before GC */
00389     DdHook *postGCHook;         /* hooks to be called after GC */
00390     DdHook *preReorderingHook;  /* hooks to be called before reordering */
00391     DdHook *postReorderingHook; /* hooks to be called after reordering */
00392     FILE *out;                  /* stdout for this manager */
00393     FILE *err;                  /* stderr for this manager */
00394 #ifdef __osf__
00395 #pragma pointer_size save
00396 #pragma pointer_size short
00397 #endif
00398     Cudd_ErrorType errorCode;   /* info on last error */
00399     /* Statistical counters. */
00400     long memused;               /* total memory allocated for the manager */
00401     long maxmem;                /* target maximum memory */
00402     long maxmemhard;            /* hard limit for maximum memory */
00403     int garbageCollections;     /* number of garbage collections */
00404     long GCTime;                /* total time spent in garbage collection */
00405     long reordTime;             /* total time spent in reordering */
00406     double totCachehits;        /* total number of cache hits */
00407     double totCacheMisses;      /* total number of cache misses */
00408     double cachecollisions;     /* number of cache collisions */
00409     double cacheinserts;        /* number of cache insertions */
00410     double cacheLastInserts;    /* insertions at the last cache resizing */
00411     double cachedeletions;      /* number of deletions during garbage coll. */
00412 #ifdef DD_STATS
00413     double nodesFreed;          /* number of nodes returned to the free list */
00414     double nodesDropped;        /* number of nodes killed by dereferencing */
00415 #endif
00416     unsigned int peakLiveNodes; /* maximum number of live nodes */
00417 #ifdef DD_UNIQUE_PROFILE
00418     double uniqueLookUps;       /* number of unique table lookups */
00419     double uniqueLinks;         /* total distance traveled in coll. chains */
00420 #endif
00421 #ifdef DD_COUNT
00422     double recursiveCalls;      /* number of recursive calls */
00423 #ifdef DD_STATS
00424     double nextSample;          /* when to write next line of stats */
00425 #endif
00426     double swapSteps;           /* number of elementary reordering steps */
00427 #endif
00428 #ifdef DD_MIS
00429     /* mis/verif compatibility fields */
00430     array_t *iton;              /* maps ids in ddNode to node_t */
00431     array_t *order;             /* copy of order_list */
00432     lsHandle handle;            /* where it is in network BDD list */
00433     network_t *network;
00434     st_table *local_order;      /* for local BDDs */
00435     int nvars;                  /* variables used so far */
00436     int threshold;              /* for pseudo var threshold value*/
00437 #endif
00438 };
00439 
00440 typedef struct Move {
00441     DdHalfWord x;
00442     DdHalfWord y;
00443     unsigned int flags;
00444     int size;
00445     struct Move *next;
00446 } Move;
00447 
00448 /* Generic level queue item. */
00449 typedef struct DdQueueItem {
00450     struct DdQueueItem *next;
00451     struct DdQueueItem *cnext;
00452     void *key;
00453 } DdQueueItem;
00454 
00455 /* Level queue. */
00456 typedef struct DdLevelQueue {
00457     void *first;
00458     DdQueueItem **last;
00459     DdQueueItem *freelist;
00460     DdQueueItem **buckets;
00461     int levels;
00462     int itemsize;
00463     int size;
00464     int maxsize;
00465     int numBuckets;
00466     int shift;
00467 } DdLevelQueue;
00468 
00469 #ifdef __osf__
00470 #pragma pointer_size restore
00471 #endif
00472 
00473 /*---------------------------------------------------------------------------*/
00474 /* Variable declarations                                                     */
00475 /*---------------------------------------------------------------------------*/
00476 
00477 
00478 /*---------------------------------------------------------------------------*/
00479 /* Macro declarations                                                        */
00480 /*---------------------------------------------------------------------------*/
00481 
00495 #define cuddDeallocNode(unique,node) \
00496     (node)->next = (unique)->nextFree; \
00497     (unique)->nextFree = node;
00498 
00499 
00514 #define cuddRef(n) cuddSatInc(Cudd_Regular(n)->ref)
00515 
00516 
00534 #define cuddDeref(n) cuddSatDec(Cudd_Regular(n)->ref)
00535 
00536 
00550 #define cuddIsConstant(node) ((node)->index == CUDD_CONST_INDEX)
00551 
00552 
00566 #define cuddT(node) ((node)->type.kids.T)
00567 
00568 
00582 #define cuddE(node) ((node)->type.kids.E)
00583 
00584 
00598 #define cuddV(node) ((node)->type.value)
00599 
00600 
00616 #define cuddI(dd,index) (((index)==CUDD_CONST_INDEX)?(int)(index):(dd)->perm[(index)])
00617 
00618 
00634 #define cuddIZ(dd,index) (((index)==CUDD_CONST_INDEX)?(int)(index):(dd)->permZ[(index)])
00635 
00636 
00648 #if SIZEOF_VOID_P == 8 && SIZEOF_INT == 4
00649 #define ddHash(f,g,s) \
00650 ((((unsigned)(unsigned long)(f) * DD_P1 + \
00651    (unsigned)(unsigned long)(g)) * DD_P2) >> (s))
00652 #else
00653 #define ddHash(f,g,s) \
00654 ((((unsigned)(f) * DD_P1 + (unsigned)(g)) * DD_P2) >> (s))
00655 #endif
00656 
00657 
00669 #if SIZEOF_VOID_P == 8 && SIZEOF_INT == 4
00670 #define ddCHash(o,f,g,h,s) \
00671 ((((((unsigned)(unsigned long)(f) + (unsigned)(unsigned long)(o)) * DD_P1 + \
00672     (unsigned)(unsigned long)(g)) * DD_P2 + \
00673    (unsigned)(unsigned long)(h)) * DD_P3) >> (s))
00674 #else
00675 #define ddCHash(o,f,g,h,s) \
00676 ((((((unsigned)(f) + (unsigned)(o)) * DD_P1 + (unsigned)(g)) * DD_P2 + \
00677    (unsigned)(h)) * DD_P3) >> (s))
00678 #endif
00679 
00680 
00693 #if SIZEOF_VOID_P == 8 && SIZEOF_INT == 4
00694 #define ddCHash2(o,f,g,s) \
00695 (((((unsigned)(unsigned long)(f) + (unsigned)(unsigned long)(o)) * DD_P1 + \
00696    (unsigned)(unsigned long)(g)) * DD_P2) >> (s))
00697 #else
00698 #define ddCHash2(o,f,g,s) \
00699 (((((unsigned)(f) + (unsigned)(o)) * DD_P1 + (unsigned)(g)) * DD_P2) >> (s))
00700 #endif
00701 
00702 
00714 #define cuddClean(p) ((DdNode *)((ptruint)(p) & ~0xf))
00715 
00716 
00728 #define ddMin(x,y) (((y) < (x)) ? (y) : (x))
00729 
00730 
00742 #define ddMax(x,y) (((y) > (x)) ? (y) : (x))
00743 
00744 
00756 #define ddAbs(x) (((x)<0) ? -(x) : (x))
00757 
00758 
00771 #define ddEqualVal(x,y,e) (ddAbs((x)-(y))<(e))
00772 
00773 
00785 #if SIZEOF_VOID_P == 8 && SIZEOF_INT == 4
00786 #define cuddSatInc(x) ((x)++)
00787 #else
00788 #define cuddSatInc(x) ((x) += (x) != (DdHalfWord)DD_MAXREF)
00789 #endif
00790 
00791 
00803 #if SIZEOF_VOID_P == 8 && SIZEOF_INT == 4
00804 #define cuddSatDec(x) ((x)--)
00805 #else
00806 #define cuddSatDec(x) ((x) -= (x) != (DdHalfWord)DD_MAXREF)
00807 #endif
00808 
00809 
00821 #define DD_ONE(dd)              ((dd)->one)
00822 
00823 
00837 #define DD_ZERO(dd) ((dd)->zero)
00838 
00839 
00851 #define DD_PLUS_INFINITY(dd) ((dd)->plusinfinity)
00852 
00853 
00865 #define DD_MINUS_INFINITY(dd) ((dd)->minusinfinity)
00866 
00867 
00886 #ifdef HAVE_IEEE_754
00887 #define cuddAdjust(x)
00888 #else
00889 #define cuddAdjust(x)           ((x) = ((x) >= DD_CRI_HI_MARK) ? DD_PLUS_INF_VAL : (((x) <= DD_CRI_LO_MARK) ? DD_MINUS_INF_VAL : (x)))
00890 #endif
00891 
00892 
00905 #define DD_LSDIGIT(x)   ((x) & DD_APA_MASK)
00906 
00907 
00920 #define DD_MSDIGIT(x)   ((x) >> DD_APA_BITS)
00921 
00922 
00936 #ifdef DD_COUNT
00937 #ifdef DD_STATS
00938 #define statLine(dd) dd->recursiveCalls++; \
00939 if (dd->recursiveCalls == dd->nextSample) {(void) fprintf(dd->err, \
00940 "@%.0f: %u nodes %u live %.0f dropped %.0f reclaimed\n", dd->recursiveCalls, \
00941 dd->keys, dd->keys - dd->dead, dd->nodesDropped, dd->reclaimed); \
00942 dd->nextSample += 250000;}
00943 #else
00944 #define statLine(dd) dd->recursiveCalls++;
00945 #endif
00946 #else
00947 #define statLine(dd)
00948 #endif
00949 
00950 
00953 /*---------------------------------------------------------------------------*/
00954 /* Function prototypes                                                       */
00955 /*---------------------------------------------------------------------------*/
00956 
00957 EXTERN DdNode * cuddAddExistAbstractRecur ARGS((DdManager *manager, DdNode *f, DdNode *cube));
00958 EXTERN DdNode * cuddAddUnivAbstractRecur ARGS((DdManager *manager, DdNode *f, DdNode *cube));
00959 EXTERN DdNode * cuddAddOrAbstractRecur ARGS((DdManager *manager, DdNode *f, DdNode *cube));
00960 EXTERN DdNode * cuddAddApplyRecur ARGS((DdManager *dd, DdNode * (*)(DdManager *, DdNode **, DdNode **), DdNode *f, DdNode *g));
00961 EXTERN DdNode * cuddAddMonadicApplyRecur ARGS((DdManager * dd, DdNode * (*op)(DdManager *, DdNode *), DdNode * f));
00962 EXTERN DdNode * cuddAddScalarInverseRecur ARGS((DdManager *dd, DdNode *f, DdNode *epsilon));
00963 EXTERN DdNode * cuddAddIteRecur ARGS((DdManager *dd, DdNode *f, DdNode *g, DdNode *h));
00964 EXTERN DdNode * cuddAddCmplRecur ARGS((DdManager *dd, DdNode *f));
00965 EXTERN DdNode * cuddAddNegateRecur ARGS((DdManager *dd, DdNode *f));
00966 EXTERN DdNode * cuddAddRoundOffRecur ARGS((DdManager *dd, DdNode *f, double trunc));
00967 EXTERN DdNode * cuddUnderApprox ARGS((DdManager *dd, DdNode *f, int numVars, int threshold, int safe, double quality));
00968 EXTERN DdNode * cuddRemapUnderApprox ARGS((DdManager *dd, DdNode *f, int numVars, int threshold, double quality));
00969 EXTERN DdNode * cuddBiasedUnderApprox ARGS((DdManager *dd, DdNode *f, DdNode *b, int numVars, int threshold, double quality1, double quality0));
00970 EXTERN DdNode * cuddBddAndAbstractRecur ARGS((DdManager *manager, DdNode *f, DdNode *g, DdNode *cube));
00971 EXTERN int cuddAnnealing ARGS((DdManager *table, int lower, int upper));
00972 EXTERN DdNode * cuddBddExistAbstractRecur ARGS((DdManager *manager, DdNode *f, DdNode *cube));
00973 EXTERN DdNode * cuddBddXorExistAbstractRecur ARGS((DdManager *manager, DdNode *f, DdNode *g, DdNode *cube));
00974 EXTERN DdNode * cuddBddBooleanDiffRecur ARGS((DdManager *manager, DdNode *f, DdNode *var));
00975 EXTERN DdNode * cuddBddIteRecur ARGS((DdManager *dd, DdNode *f, DdNode *g, DdNode *h));
00976 EXTERN DdNode * cuddBddIntersectRecur ARGS((DdManager *dd, DdNode *f, DdNode *g));
00977 EXTERN DdNode * cuddBddAndRecur ARGS((DdManager *manager, DdNode *f, DdNode *g));
00978 EXTERN DdNode * cuddBddXorRecur ARGS((DdManager *manager, DdNode *f, DdNode *g));
00979 EXTERN DdNode * cuddBddTransfer ARGS((DdManager *ddS, DdManager *ddD, DdNode *f));
00980 EXTERN DdNode * cuddAddBddDoPattern ARGS((DdManager *dd, DdNode *f));
00981 EXTERN int cuddInitCache ARGS((DdManager *unique, unsigned int cacheSize, unsigned int maxCacheSize));
00982 EXTERN void cuddCacheInsert ARGS((DdManager *table, ptruint op, DdNode *f, DdNode *g, DdNode *h, DdNode *data));
00983 EXTERN void cuddCacheInsert2 ARGS((DdManager *table, DdNode * (*)(DdManager *, DdNode *, DdNode *), DdNode *f, DdNode *g, DdNode *data));
00984 EXTERN void cuddCacheInsert1 ARGS((DdManager *table, DdNode * (*)(DdManager *, DdNode *), DdNode *f, DdNode *data));
00985 EXTERN DdNode * cuddCacheLookup ARGS((DdManager *table, ptruint op, DdNode *f, DdNode *g, DdNode *h));
00986 EXTERN DdNode * cuddCacheLookupZdd ARGS((DdManager *table, ptruint op, DdNode *f, DdNode *g, DdNode *h));
00987 EXTERN DdNode * cuddCacheLookup2 ARGS((DdManager *table, DdNode * (*)(DdManager *, DdNode *, DdNode *), DdNode *f, DdNode *g));
00988 EXTERN DdNode * cuddCacheLookup1 ARGS((DdManager *table, DdNode * (*)(DdManager *, DdNode *), DdNode *f));
00989 EXTERN DdNode * cuddCacheLookup2Zdd ARGS((DdManager *table, DdNode * (*)(DdManager *, DdNode *, DdNode *), DdNode *f, DdNode *g));
00990 EXTERN DdNode * cuddCacheLookup1Zdd ARGS((DdManager *table, DdNode * (*)(DdManager *, DdNode *), DdNode *f));
00991 EXTERN DdNode * cuddConstantLookup ARGS((DdManager *table, ptruint op, DdNode *f, DdNode *g, DdNode *h));
00992 EXTERN int cuddCacheProfile ARGS((DdManager *table, FILE *fp));
00993 EXTERN void cuddCacheResize ARGS((DdManager *table));
00994 EXTERN void cuddCacheFlush ARGS((DdManager *table));
00995 EXTERN int cuddComputeFloorLog2 ARGS((unsigned int value));
00996 EXTERN int cuddHeapProfile ARGS((DdManager *dd));
00997 EXTERN void cuddPrintNode ARGS((DdNode *f, FILE *fp));
00998 EXTERN void cuddPrintVarGroups ARGS((DdManager * dd, MtrNode * root, int zdd, int silent));
00999 EXTERN DdNode * cuddBddClippingAnd ARGS((DdManager *dd, DdNode *f, DdNode *g, int maxDepth, int direction));
01000 EXTERN DdNode * cuddBddClippingAndAbstract ARGS((DdManager *dd, DdNode *f, DdNode *g, DdNode *cube, int maxDepth, int direction));
01001 EXTERN void cuddGetBranches ARGS((DdNode *g, DdNode **g1, DdNode **g0));
01002 EXTERN int cuddCheckCube ARGS((DdManager *dd, DdNode *g));
01003 EXTERN DdNode * cuddCofactorRecur ARGS((DdManager *dd, DdNode *f, DdNode *g));
01004 EXTERN DdNode * cuddBddComposeRecur ARGS((DdManager *dd, DdNode *f, DdNode *g, DdNode *proj));
01005 EXTERN DdNode * cuddAddComposeRecur ARGS((DdManager *dd, DdNode *f, DdNode *g, DdNode *proj));
01006 EXTERN int cuddExact ARGS((DdManager *table, int lower, int upper));
01007 EXTERN DdNode * cuddBddConstrainRecur ARGS((DdManager *dd, DdNode *f, DdNode *c));
01008 EXTERN DdNode * cuddBddRestrictRecur ARGS((DdManager *dd, DdNode *f, DdNode *c));
01009 EXTERN DdNode * cuddAddConstrainRecur ARGS((DdManager *dd, DdNode *f, DdNode *c));
01010 EXTERN DdNode * cuddAddRestrictRecur ARGS((DdManager *dd, DdNode *f, DdNode *c));
01011 EXTERN DdNode * cuddBddLICompaction ARGS((DdManager *dd, DdNode *f, DdNode *c));
01012 EXTERN int cuddGa ARGS((DdManager *table, int lower, int upper));
01013 EXTERN int cuddTreeSifting ARGS((DdManager *table, Cudd_ReorderingType method));
01014 EXTERN int cuddZddInitUniv ARGS((DdManager *zdd));
01015 EXTERN void cuddZddFreeUniv ARGS((DdManager *zdd));
01016 EXTERN void cuddSetInteract ARGS((DdManager *table, int x, int y));
01017 EXTERN int cuddTestInteract ARGS((DdManager *table, int x, int y));
01018 EXTERN int cuddInitInteract ARGS((DdManager *table));
01019 EXTERN DdLocalCache * cuddLocalCacheInit ARGS((DdManager *manager, unsigned int keySize, unsigned int cacheSize, unsigned int maxCacheSize));
01020 EXTERN void cuddLocalCacheQuit ARGS((DdLocalCache *cache));
01021 EXTERN void cuddLocalCacheInsert ARGS((DdLocalCache *cache, DdNodePtr *key, DdNode *value));
01022 EXTERN DdNode * cuddLocalCacheLookup ARGS((DdLocalCache *cache, DdNodePtr *key));
01023 EXTERN void cuddLocalCacheClearDead ARGS((DdManager *manager));
01024 EXTERN int cuddIsInDeathRow ARGS((DdManager *dd, DdNode *f));
01025 EXTERN int cuddTimesInDeathRow ARGS((DdManager *dd, DdNode *f));
01026 EXTERN void cuddLocalCacheClearAll ARGS((DdManager *manager));
01027 #ifdef DD_CACHE_PROFILE
01028 EXTERN int cuddLocalCacheProfile ARGS((DdLocalCache *cache));
01029 #endif
01030 EXTERN DdHashTable * cuddHashTableInit ARGS((DdManager *manager, unsigned int keySize, unsigned int initSize));
01031 EXTERN void cuddHashTableQuit ARGS((DdHashTable *hash));
01032 EXTERN int cuddHashTableInsert ARGS((DdHashTable *hash, DdNodePtr *key, DdNode *value, ptrint count));
01033 EXTERN DdNode * cuddHashTableLookup ARGS((DdHashTable *hash, DdNodePtr *key));
01034 EXTERN int cuddHashTableInsert1 ARGS((DdHashTable *hash, DdNode *f, DdNode *value, ptrint count));
01035 EXTERN DdNode * cuddHashTableLookup1 ARGS((DdHashTable *hash, DdNode *f));
01036 EXTERN int cuddHashTableInsert2 ARGS((DdHashTable *hash, DdNode *f, DdNode *g, DdNode *value, ptrint count));
01037 EXTERN DdNode * cuddHashTableLookup2 ARGS((DdHashTable *hash, DdNode *f, DdNode *g));
01038 EXTERN int cuddHashTableInsert3 ARGS((DdHashTable *hash, DdNode *f, DdNode *g, DdNode *h, DdNode *value, ptrint count));
01039 EXTERN DdNode * cuddHashTableLookup3 ARGS((DdHashTable *hash, DdNode *f, DdNode *g, DdNode *h));
01040 EXTERN DdLevelQueue * cuddLevelQueueInit ARGS((int levels, int itemSize, int numBuckets));
01041 EXTERN void cuddLevelQueueQuit ARGS((DdLevelQueue *queue));
01042 EXTERN void * cuddLevelQueueEnqueue ARGS((DdLevelQueue *queue, void *key, int level));
01043 EXTERN void cuddLevelQueueDequeue ARGS((DdLevelQueue *queue, int level));
01044 EXTERN int cuddLinearAndSifting ARGS((DdManager *table, int lower, int upper));
01045 EXTERN DdNode * cuddBddLiteralSetIntersectionRecur ARGS((DdManager *dd, DdNode *f, DdNode *g));
01046 EXTERN DdNode * cuddCProjectionRecur ARGS((DdManager *dd, DdNode *R, DdNode *Y, DdNode *Ysupp));
01047 EXTERN DdNode * cuddBddClosestCube ARGS((DdManager *dd, DdNode *f, DdNode *g, CUDD_VALUE_TYPE bound));
01048 EXTERN void cuddReclaim ARGS((DdManager *table, DdNode *n));
01049 EXTERN void cuddReclaimZdd ARGS((DdManager *table, DdNode *n));
01050 EXTERN void cuddClearDeathRow ARGS((DdManager *table));
01051 EXTERN void cuddShrinkDeathRow ARGS((DdManager *table));
01052 EXTERN DdNode * cuddDynamicAllocNode ARGS((DdManager *table));
01053 EXTERN int cuddSifting ARGS((DdManager *table, int lower, int upper));
01054 EXTERN int cuddSwapping ARGS((DdManager *table, int lower, int upper, Cudd_ReorderingType heuristic));
01055 EXTERN int cuddNextHigh ARGS((DdManager *table, int x));
01056 EXTERN int cuddNextLow ARGS((DdManager *table, int x));
01057 EXTERN int cuddSwapInPlace ARGS((DdManager *table, int x, int y));
01058 EXTERN int cuddBddAlignToZdd ARGS((DdManager *table));
01059 EXTERN DdNode * cuddBddMakePrime ARGS((DdManager *dd, DdNode *cube, DdNode *f));
01060 EXTERN DdNode * cuddSolveEqnRecur ARGS((DdManager *bdd, DdNode *F, DdNode *Y, DdNode **G, int n, int *yIndex, int i));
01061 EXTERN DdNode * cuddVerifySol ARGS((DdManager *bdd, DdNode *F, DdNode **G, int *yIndex, int n));
01062 #ifdef ST_INCLUDED
01063 EXTERN DdNode* cuddSplitSetRecur ARGS((DdManager *manager, st_table *mtable, int *varSeen, DdNode *p, double n, double max, int index));
01064 #endif
01065 EXTERN DdNode * cuddSubsetHeavyBranch ARGS((DdManager *dd, DdNode *f, int numVars, int threshold));
01066 EXTERN DdNode * cuddSubsetShortPaths ARGS((DdManager *dd, DdNode *f, int numVars, int threshold, int hardlimit));
01067 EXTERN int cuddSymmCheck ARGS((DdManager *table, int x, int y));
01068 EXTERN int cuddSymmSifting ARGS((DdManager *table, int lower, int upper));
01069 EXTERN int cuddSymmSiftingConv ARGS((DdManager *table, int lower, int upper));
01070 EXTERN DdNode * cuddAllocNode ARGS((DdManager *unique));
01071 EXTERN DdManager * cuddInitTable ARGS((unsigned int numVars, unsigned int numVarsZ, unsigned int numSlots, unsigned int looseUpTo));
01072 EXTERN void cuddFreeTable ARGS((DdManager *unique));
01073 EXTERN int cuddGarbageCollect ARGS((DdManager *unique, int clearCache));
01074 EXTERN int cuddGarbageCollectZdd ARGS((DdManager *unique, int clearCache));
01075 EXTERN DdNode * cuddZddGetNode ARGS((DdManager *zdd, int id, DdNode *T, DdNode *E));
01076 EXTERN DdNode * cuddZddGetNodeIVO ARGS((DdManager *dd, int index, DdNode *g, DdNode *h));
01077 EXTERN DdNode * cuddUniqueInter ARGS((DdManager *unique, int index, DdNode *T, DdNode *E));
01078 EXTERN DdNode * cuddUniqueInterIVO ARGS((DdManager *unique, int index, DdNode *T, DdNode *E));
01079 EXTERN DdNode * cuddUniqueInterZdd ARGS((DdManager *unique, int index, DdNode *T, DdNode *E));
01080 EXTERN DdNode * cuddUniqueConst ARGS((DdManager *unique, CUDD_VALUE_TYPE value));
01081 EXTERN void cuddRehash ARGS((DdManager *unique, int i));
01082 EXTERN void cuddShrinkSubtable ARGS((DdManager *unique, int i));
01083 EXTERN int cuddInsertSubtables ARGS((DdManager *unique, int n, int level));
01084 EXTERN int cuddDestroySubtables ARGS((DdManager *unique, int n));
01085 EXTERN int cuddResizeTableZdd ARGS((DdManager *unique, int index));
01086 EXTERN void cuddSlowTableGrowth ARGS((DdManager *unique));
01087 EXTERN int cuddP ARGS((DdManager *dd, DdNode *f));
01088 #ifdef ST_INCLUDED
01089 EXTERN enum st_retval cuddStCountfree ARGS((char *key, char *value, char *arg));
01090 EXTERN int cuddCollectNodes ARGS((DdNode *f, st_table *visited));
01091 #endif
01092 EXTERN int cuddWindowReorder ARGS((DdManager *table, int low, int high, Cudd_ReorderingType submethod));
01093 EXTERN DdNode   * cuddZddProduct ARGS((DdManager *dd, DdNode *f, DdNode *g));
01094 EXTERN DdNode   * cuddZddUnateProduct ARGS((DdManager *dd, DdNode *f, DdNode *g));
01095 EXTERN DdNode   * cuddZddWeakDiv ARGS((DdManager *dd, DdNode *f, DdNode *g));
01096 EXTERN DdNode   * cuddZddWeakDivF ARGS((DdManager *dd, DdNode *f, DdNode *g));
01097 EXTERN DdNode   * cuddZddDivide ARGS((DdManager *dd, DdNode *f, DdNode *g));
01098 EXTERN DdNode   * cuddZddDivideF ARGS((DdManager *dd, DdNode *f, DdNode *g));
01099 EXTERN int cuddZddGetCofactors3 ARGS((DdManager *dd, DdNode *f, int v, DdNode **f1, DdNode **f0, DdNode **fd));
01100 EXTERN int cuddZddGetCofactors2 ARGS((DdManager *dd, DdNode *f, int v, DdNode **f1, DdNode **f0));
01101 EXTERN DdNode   * cuddZddComplement ARGS((DdManager *dd, DdNode *node));
01102 EXTERN int cuddZddGetPosVarIndex(DdManager * dd, int index);
01103 EXTERN int cuddZddGetNegVarIndex(DdManager * dd, int index);
01104 EXTERN int cuddZddGetPosVarLevel(DdManager * dd, int index);
01105 EXTERN int cuddZddGetNegVarLevel(DdManager * dd, int index);
01106 EXTERN int cuddZddTreeSifting ARGS((DdManager *table, Cudd_ReorderingType method));
01107 EXTERN DdNode   * cuddZddIsop ARGS((DdManager *dd, DdNode *L, DdNode *U, DdNode **zdd_I));
01108 EXTERN DdNode   * cuddBddIsop ARGS((DdManager *dd, DdNode *L, DdNode *U));
01109 EXTERN DdNode   * cuddMakeBddFromZddCover ARGS((DdManager *dd, DdNode *node));
01110 EXTERN int cuddZddLinearSifting ARGS((DdManager *table, int lower, int upper));
01111 EXTERN int cuddZddAlignToBdd ARGS((DdManager *table));
01112 EXTERN int cuddZddNextHigh ARGS((DdManager *table, int x));
01113 EXTERN int cuddZddNextLow ARGS((DdManager *table, int x));
01114 EXTERN int cuddZddUniqueCompare ARGS((int *ptr_x, int *ptr_y));
01115 EXTERN int cuddZddSwapInPlace ARGS((DdManager *table, int x, int y));
01116 EXTERN int cuddZddSwapping ARGS((DdManager *table, int lower, int upper, Cudd_ReorderingType heuristic));
01117 EXTERN int cuddZddSifting ARGS((DdManager *table, int lower, int upper));
01118 EXTERN DdNode * cuddZddIte ARGS((DdManager *dd, DdNode *f, DdNode *g, DdNode *h));
01119 EXTERN DdNode * cuddZddUnion ARGS((DdManager *zdd, DdNode *P, DdNode *Q));
01120 EXTERN DdNode * cuddZddIntersect ARGS((DdManager *zdd, DdNode *P, DdNode *Q));
01121 EXTERN DdNode * cuddZddDiff ARGS((DdManager *zdd, DdNode *P, DdNode *Q));
01122 EXTERN DdNode * cuddZddChangeAux ARGS((DdManager *zdd, DdNode *P, DdNode *zvar));
01123 EXTERN DdNode * cuddZddSubset1 ARGS((DdManager *dd, DdNode *P, int var));
01124 EXTERN DdNode * cuddZddSubset0 ARGS((DdManager *dd, DdNode *P, int var));
01125 EXTERN DdNode * cuddZddChange ARGS((DdManager *dd, DdNode *P, int var));
01126 EXTERN int cuddZddSymmCheck ARGS((DdManager *table, int x, int y));
01127 EXTERN int cuddZddSymmSifting ARGS((DdManager *table, int lower, int upper));
01128 EXTERN int cuddZddSymmSiftingConv ARGS((DdManager *table, int lower, int upper));
01129 EXTERN int cuddZddP ARGS((DdManager *zdd, DdNode *f));
01130 
01133 #endif /* _CUDDINT */