glu-2.2: src/cuBdd/cuddInt.h Source File

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