cuddInt.h

Go to the documentation of this file.

#ifndef CUDD_INT_H_
#define CUDD_INT_H_


/*---------------------------------------------------------------------------*/
/* Nested includes                                                           */
/*---------------------------------------------------------------------------*/

#include <math.h>
#include "config.h"
#include "st.h"
#include "mtr.h"
#include "epd.h"
#include "cudd.h"

/*---------------------------------------------------------------------------*/
/* Constant declarations                                                     */
/*---------------------------------------------------------------------------*/

#define CUDD_VERSION        PACKAGE_VERSION

#define DD_MAXREF       ((DdHalfWord) ~0)

#define DD_DEFAULT_RESIZE   10  /* how many extra variables */
                    /* should be added when resizing */
#define DD_MEM_CHUNK        1022

/* These definitions work for CUDD_VALUE_TYPE == double */
#define DD_ONE_VAL      (1.0)
#define DD_ZERO_VAL     (0.0)
#define DD_EPSILON      (1.0e-12)

/* The definitions of +/- infinity in terms of HUGE_VAL work on
** the DECstations and on many other combinations of OS/compiler.
*/
#ifdef HAVE_IEEE_754
#  define DD_PLUS_INF_VAL   (HUGE_VAL)
#else
#  define DD_PLUS_INF_VAL   (10e301)
#  define DD_CRI_HI_MARK    (10e150)
#  define DD_CRI_LO_MARK    (-(DD_CRI_HI_MARK))
#endif
#define DD_MINUS_INF_VAL    (-(DD_PLUS_INF_VAL))

#define DD_NON_CONSTANT     ((DdNode *) 1)  /* for Cudd_bddIteConstant */

/* Unique table and cache management constants. */
#define DD_MAX_SUBTABLE_DENSITY 4   /* tells when to resize a subtable */
/* gc when this percent are dead (measured w.r.t. slots, not keys)
** The first limit (LO) applies normally. The second limit applies when
** the package believes more space for the unique table (i.e., more dead
** nodes) would improve performance, and the unique table is not already
** too large. The third limit applies when memory is low.
*/
#define DD_GC_FRAC_LO       DD_MAX_SUBTABLE_DENSITY * 0.25
#define DD_GC_FRAC_HI       DD_MAX_SUBTABLE_DENSITY * 1.0
#define DD_GC_FRAC_MIN      0.2
#define DD_MIN_HIT      30  /* resize cache when hit ratio
                       above this percentage (default) */
#define DD_MAX_LOOSE_FRACTION   5 /* 1 / (max fraction of memory used for
                     unique table in fast growth mode) */
#define DD_MAX_CACHE_FRACTION   3 /* 1 / (max fraction of memory used for
                     computed table if resizing enabled) */
#define DD_STASH_FRACTION   64 /* 1 / (fraction of memory set
                      aside for emergencies) */
#define DD_MAX_CACHE_TO_SLOTS_RATIO 4 /* used to limit the cache size */

/* Variable ordering default parameter values. */
#define DD_SIFT_MAX_VAR     1000
#define DD_SIFT_MAX_SWAPS   2000000
#define DD_DEFAULT_RECOMB   0
#define DD_MAX_REORDER_GROWTH   1.2
#define DD_FIRST_REORDER    4004    /* 4 for the constants */
#define DD_DYN_RATIO        2   /* when to dynamically reorder */

/* Primes for cache hash functions. */
#define DD_P1           12582917
#define DD_P2           4256249
#define DD_P3           741457
#define DD_P4           1618033999

/* Cache tags for 3-operand operators.  These tags are stored in the
** least significant bits of the cache operand pointers according to
** the following scheme.  The tag consists of two hex digits.  Both digits
** must be even, so that they do not interfere with complementation bits.
** The least significant one is stored in Bits 3:1 of the f operand in the
** cache entry.  Bit 1 is always 1, so that we can differentiate
** three-operand operations from one- and two-operand operations.
** Therefore, the least significant digit is one of {2,6,a,e}.  The most
** significant digit occupies Bits 3:1 of the g operand in the cache
** entry.  It can by any even digit between 0 and e.  This gives a total
** of 5 bits for the tag proper, which means a maximum of 32 three-operand
** operations. */
#define DD_ADD_ITE_TAG              0x02
#define DD_BDD_AND_ABSTRACT_TAG         0x06
#define DD_BDD_XOR_EXIST_ABSTRACT_TAG       0x0a
#define DD_BDD_ITE_TAG              0x0e
#define DD_ADD_BDD_DO_INTERVAL_TAG      0x22
#define DD_BDD_CLIPPING_AND_ABSTRACT_UP_TAG 0x26
#define DD_BDD_CLIPPING_AND_ABSTRACT_DOWN_TAG   0x2a
#define DD_BDD_COMPOSE_RECUR_TAG        0x2e
#define DD_ADD_COMPOSE_RECUR_TAG        0x42
#define DD_ADD_NON_SIM_COMPOSE_TAG      0x46
#define DD_EQUIV_DC_TAG             0x4a
#define DD_ZDD_ITE_TAG              0x4e
#define DD_ADD_ITE_CONSTANT_TAG         0x62
#define DD_ADD_EVAL_CONST_TAG           0x66
#define DD_BDD_ITE_CONSTANT_TAG         0x6a
#define DD_ADD_OUT_SUM_TAG          0x6e
#define DD_BDD_LEQ_UNLESS_TAG           0x82
#define DD_ADD_TRIANGLE_TAG         0x86
#define DD_BDD_MAX_EXP_TAG          0x8a
#define DD_VARS_SYMM_BEFORE_TAG         0x8e
#define DD_VARS_SYMM_BETWEEN_TAG        0xa2

/* Generator constants. */
#define CUDD_GEN_CUBES 0
#define CUDD_GEN_PRIMES 1
#define CUDD_GEN_NODES 2
#define CUDD_GEN_ZDD_PATHS 3
#define CUDD_GEN_EMPTY 0
#define CUDD_GEN_NONEMPTY 1

#if SIZEOF_VOID_P == 8 && SIZEOF_INT == 4
#define CUDD_MAXINDEX       (((DdHalfWord) ~0) >> 1)
#else
#define CUDD_MAXINDEX       ((DdHalfWord) ~0)
#endif

#define CUDD_CONST_INDEX    CUDD_MAXINDEX

#define STAB_SIZE 64

#define CUDD_CHECK_MASK 0x7ff

/*---------------------------------------------------------------------------*/
/* Type declarations                                                         */
/*---------------------------------------------------------------------------*/

#if SIZEOF_VOID_P == 8 && SIZEOF_INT == 4
typedef uint32_t DdHalfWord;
#else
typedef uint16_t DdHalfWord;
#endif

typedef intptr_t ptrint;

typedef uintptr_t ptruint;

typedef struct DdChildren DdChildren;
typedef struct DdHook DdHook;
typedef struct DdSubtable DdSubtable;
typedef struct DdCache DdCache;
typedef struct DdLocalCacheItem DdLocalCacheItem;
typedef struct DdLocalCache DdLocalCache;
typedef struct DdHashItem DdHashItem;
typedef struct DdHashTable DdHashTable;
typedef struct Move Move;
typedef struct IndexKey IndexKey;
typedef struct DdQueueItem DdQueueItem;
typedef struct DdLevelQueue DdLevelQueue;

/*---------------------------------------------------------------------------*/
/* Stucture declarations                                                     */
/*---------------------------------------------------------------------------*/

struct DdChildren {
    struct DdNode *T;   
    struct DdNode *E;   
};

struct DdNode {
    DdHalfWord index;       
    DdHalfWord ref;     
    DdNode *next;       
    union {
    CUDD_VALUE_TYPE value;  
    DdChildren kids;    
    } type;         
};

struct DdGen {
    DdManager   *manager;
    int     type;
    int     status;
    union {
    struct {
        int         *cube;
        CUDD_VALUE_TYPE value;
    } cubes;
    struct {
        int         *cube;
        DdNode      *ub;
    } primes;
    struct {
        int                 size;
    } nodes;
    } gen;
    struct {
    int sp;
    DdNode  **stack;
    } stack;
    DdNode  *node;
};

struct DdHook {
    DD_HFP f;           
    struct DdHook *next;    
};

struct DdLocalCacheItem {
    DdNode *value;
#ifdef DD_CACHE_PROFILE
    ptrint count;
#endif
    DdNode *key[1];
};

struct DdLocalCache {
    DdLocalCacheItem *item;
    unsigned int itemsize;
    unsigned int keysize;
    unsigned int slots;
    int shift;
    double lookUps;
    double minHit;
    double hits;
    unsigned int maxslots;
    DdManager *manager;
    struct DdLocalCache *next;
};

struct DdHashItem {
    struct DdHashItem *next;    
    ptrint count;       
    DdNode *value;      
    DdNode *key[1];     
};

struct DdHashTable {
    unsigned int keysize;   
    unsigned int itemsize;  
    DdHashItem **bucket;    
    DdHashItem *nextFree;   
    DdHashItem **memoryList;    
    unsigned int numBuckets;    
    int shift;          
    unsigned int size;      
    unsigned int maxsize;   
    DdManager *manager;     
};

struct DdCache {
    DdNode *f,*g;       
    ptruint h;          
    DdNode *data;       
#ifdef DD_CACHE_PROFILE
    ptrint count;       
#endif
};

struct DdSubtable {
    DdNode **nodelist;      
    int shift;          
    unsigned int slots;     
    unsigned int keys;      
    unsigned int maxKeys;   
    unsigned int dead;      
    unsigned int next;      
    int bindVar;        
    /* Fields for lazy sifting. */
    Cudd_VariableType varType;  
    int pairIndex;              
    int varHandled;     
    Cudd_LazyGroupType varToBeGrouped; 
};

struct DdManager {
    /* Constants */
    DdNode sentinel;        
    DdNode *one;        
    DdNode *zero;       
    DdNode *plusinfinity;   
    DdNode *minusinfinity;  
    DdNode *background;     
    /* Computed Table */
    DdCache *acache;        
    DdCache *cache;     
    unsigned int cacheSlots;    
    int cacheShift;     
    double cacheMisses;     
    double cacheHits;       
    double minHit;      
    int cacheSlack;     
    unsigned int maxCacheHard;  
    /* Unique Table */
    int size;           
    int sizeZ;          
    int maxSize;        
    int maxSizeZ;       
    DdSubtable *subtables;  
    DdSubtable *subtableZ;  
    DdSubtable constants;   
    unsigned int slots;     
    unsigned int keys;      
    unsigned int keysZ;     
    unsigned int dead;      
    unsigned int deadZ;     
    unsigned int maxLive;   
    unsigned int minDead;   
    int gcEnabled;      
    double gcFrac;      
    unsigned int looseUpTo; 
    unsigned int initSlots; 
    DdNode **stack;     
    double allocated;       
    double reclaimed;       
    int *perm;          
    int *permZ;         
    int *invperm;       
    int *invpermZ;      
    DdNode **vars;      
    int *map;           
    DdNode **univ;      
    unsigned int isolated;  
    unsigned int originalSize;  
    int linearSize;     
    ptruint *interact;      
    ptruint *linear;        
    /* Memory Management */
    DdNode **memoryList;    
    DdNode *nextFree;       
    char *stash;        
#ifndef DD_NO_DEATH_ROW
    DdNode **deathRow;      
    int deathRowDepth;      
    int nextDead;       
    unsigned deadMask;      
#endif
    /* General Parameters */
    CUDD_VALUE_TYPE epsilon;    
    /* Dynamic Reordering Parameters */
    int reordered;      
    unsigned int reorderings;   
    unsigned int maxReorderings;
    int siftMaxVar;     
    int siftMaxSwap;        
    int ddTotalNumberSwapping;  
    int zddTotalNumberSwapping; 
    int reordCycle;     
    double maxGrowth;       
    double maxGrowthAlt;    
    int autoDyn;        
    int autoDynZ;       
    Cudd_ReorderingType autoMethod;  
    Cudd_ReorderingType autoMethodZ; 
    int realign;        
    int realignZ;       
    unsigned int nextDyn;   
    unsigned int countDead; 
    MtrNode *tree;      
    MtrNode *treeZ;     
    Cudd_AggregationType groupcheck; 
    int recomb;         
    int symmviolation;      
    int arcviolation;       
    int populationSize;     
    int numberXovers;       
    unsigned int randomizeOrder; 
    DdLocalCache *localCaches;  
    void *hooks;        
    DdHook *preGCHook;      
    DdHook *postGCHook;     
    DdHook *preReorderingHook;  
    DdHook *postReorderingHook; 
    FILE *out;          
    FILE *err;          
    Cudd_ErrorType errorCode;   
    unsigned long startTime;    
    unsigned long timeLimit;    
    DD_THFP terminationCallback; 
    void * tcbArg;      
    DD_OOMFP outOfMemCallback;  
    DD_TOHFP timeoutHandler;    
    void * tohArg;      
    /* Statistical counters. */
    size_t memused;     
    size_t maxmem;      
    size_t maxmemhard;      
    int garbageCollections; 
    unsigned long GCTime;   
    unsigned long reordTime;    
    double totCachehits;    
    double totCacheMisses;  
    double cachecollisions; 
    double cacheinserts;    
    double cacheLastInserts;    
    double cachedeletions;  
    unsigned int peakLiveNodes; 
    /* Random number generator. */
    int32_t cuddRand;       
    int32_t cuddRand2;      
    int32_t shuffleSelect;  
    int32_t shuffleTable[STAB_SIZE]; 
#ifdef DD_STATS
    double nodesFreed;      
    double nodesDropped;    
    int totalNISwaps;       
    int extsymmcalls;       
    int extsymm;        
    int secdiffcalls;       
    int secdiff;        
    int secdiffmisfire;     
    int tosses;         
    int acceptances;        
    int totalShuffles;      
    int totalNumberLinearTr;    
    int num_calls;      
#endif
#ifdef DD_UNIQUE_PROFILE
    double uniqueLookUps;   
    double uniqueLinks;     
#endif
#ifdef DD_COUNT
    double recursiveCalls;  
#ifdef DD_STATS
    double nextSample;      
#endif
    double swapSteps;       
#endif
#ifdef DD_DEBUG
    int addPermuteRecurHits;    
    int bddPermuteRecurHits;    
    int bddVectorComposeHits;   
    int addVectorComposeHits;   
    int addGeneralVectorComposeHits; 
    int enableExtraDebug;   
#endif
};

struct Move {
    DdHalfWord x;
    DdHalfWord y;
    unsigned int flags;
    int size;
    struct Move *next;
};

struct IndexKey {
    int index;
    int keys;
};

struct DdQueueItem {
    struct DdQueueItem *next;
    struct DdQueueItem *cnext;
    void *key;
};

struct DdLevelQueue {
    void *first;
    DdQueueItem **last;
    DdQueueItem *freelist;
    DdQueueItem **buckets;
    int levels;
    int itemsize;
    int size;
    int maxsize;
    int numBuckets;
    int shift;
    DdManager *manager;
};

/*---------------------------------------------------------------------------*/
/* Variable declarations                                                     */
/*---------------------------------------------------------------------------*/


/*---------------------------------------------------------------------------*/
/* Macro declarations                                                        */
/*---------------------------------------------------------------------------*/

#define cuddDeallocNode(unique,node) \
    (node)->next = (unique)->nextFree; \
    (unique)->nextFree = node;

#define cuddDeallocMove(unique,node) \
    ((DdNode *)(node))->ref = 0; \
    ((DdNode *)(node))->next = (unique)->nextFree; \
    (unique)->nextFree = (DdNode *)(node);


#define cuddRef(n) cuddSatInc(Cudd_Regular(n)->ref)


#define cuddDeref(n) cuddSatDec(Cudd_Regular(n)->ref)


#define Cudd_IsConstantInt(node) ((Cudd_Regular(node))->index == CUDD_CONST_INDEX)


#define cuddIsConstant(node) ((node)->index == CUDD_CONST_INDEX)


#define cuddT(node) ((node)->type.kids.T)


#define cuddE(node) ((node)->type.kids.E)


#define cuddV(node) ((node)->type.value)


#define cuddI(dd,index) (((index)==CUDD_CONST_INDEX)?(int)(index):(dd)->perm[(index)])


#define cuddIZ(dd,index) (((index)==CUDD_CONST_INDEX)?(int)(index):(dd)->permZ[(index)])


#if SIZEOF_VOID_P == 8 && SIZEOF_INT == 4
#define ddHash(f,g,s) \
((((unsigned)(ptruint)(f) * DD_P1 + \
   (unsigned)(ptruint)(g)) * DD_P2) >> (s))
#else
#define ddHash(f,g,s) \
((((unsigned)(f) * DD_P1 + (unsigned)(g)) * DD_P2) >> (s))
#endif


#if SIZEOF_VOID_P == 8 && SIZEOF_INT == 4
#define ddCHash(o,f,g,h,s) \
((((((unsigned)(ptruint)(f) + (unsigned)(ptruint)(o)) * DD_P1 + \
    (unsigned)(ptruint)(g)) * DD_P2 + \
   (unsigned)(ptruint)(h)) * DD_P3) >> (s))
#else
#define ddCHash(o,f,g,h,s) \
((((((unsigned)(f) + (unsigned)(o)) * DD_P1 + (unsigned)(g)) * DD_P2 + \
   (unsigned)(h)) * DD_P3) >> (s))
#endif


#if SIZEOF_VOID_P == 8 && SIZEOF_INT == 4
#define ddCHash2(o,f,g,s) \
(((((unsigned)(ptruint)(f) + (unsigned)(ptruint)(o)) * DD_P1 + \
   (unsigned)(ptruint)(g)) * DD_P2) >> (s))
#else
#define ddCHash2(o,f,g,s) \
(((((unsigned)(f) + (unsigned)(o)) * DD_P1 + (unsigned)(g)) * DD_P2) >> (s))
#endif


#define cuddClean(p) ((DdNode *)((ptruint)(p) & ~ (ptruint) 0xf))


#define ddMin(x,y) (((y) < (x)) ? (y) : (x))


#define ddMax(x,y) (((y) > (x)) ? (y) : (x))


#define ddAbs(x) (((x)<0) ? -(x) : (x))


#define ddEqualVal(x,y,e) (ddAbs((x)-(y))<(e))


#if SIZEOF_VOID_P == 8 && SIZEOF_INT == 4
#define cuddSatInc(x) ((x)++)
#else
#define cuddSatInc(x) ((x) += (x) != (DdHalfWord)DD_MAXREF)
#endif


#if SIZEOF_VOID_P == 8 && SIZEOF_INT == 4
#define cuddSatDec(x) ((x)--)
#else
#define cuddSatDec(x) ((x) -= (x) != (DdHalfWord)DD_MAXREF)
#endif


#define DD_ONE(dd)      ((dd)->one)


#define DD_ZERO(dd) ((dd)->zero)


#define DD_PLUS_INFINITY(dd) ((dd)->plusinfinity)


#define DD_MINUS_INFINITY(dd) ((dd)->minusinfinity)


#ifdef HAVE_IEEE_754
#define cuddAdjust(x)
#else
#define cuddAdjust(x)       ((x) = ((x) >= DD_CRI_HI_MARK) ? DD_PLUS_INF_VAL : (((x) <= DD_CRI_LO_MARK) ? DD_MINUS_INF_VAL : (x)))
#endif


#ifdef DD_COUNT
#ifdef DD_STATS
#define statLine(dd)                                                    \
    do {                                                                \
        (dd)->recursiveCalls++;                                         \
        if ((dd)->recursiveCalls == (dd)->nextSample) {                 \
            (void) fprintf((dd)->err,                                   \
                           "@%.0f: %u nodes %u live %.0f dropped"       \
                           " %.0f reclaimed\n",                         \
                           (dd)->recursiveCalls, (dd)->keys,            \
                           (dd)->keys - (dd)->dead,                     \
                           (dd)->nodesDropped, (dd)->reclaimed);        \
            (dd)->nextSample += 250000;}                                \
    } while (0)
#else
#define statLine(dd) (dd)->recursiveCalls++
#endif
#else
#define statLine(dd)
#endif


#define checkWhetherToGiveUp(dd)                                        \
    do {                                                                \
        if (((int64_t) CUDD_CHECK_MASK & (int64_t) (dd)->cacheMisses) == 0) { \
            if ((dd)->terminationCallback != NULL &&                    \
                (dd)->terminationCallback((dd)->tcbArg)) {              \
                (dd)->errorCode = CUDD_TERMINATION;                     \
                return(NULL);                                           \
            }                                                           \
            if (util_cpu_time() - (dd)->startTime > (dd)->timeLimit) {  \
                (dd)->errorCode = CUDD_TIMEOUT_EXPIRED;                 \
                return(NULL);                                           \
            }                                                           \
        }                                                               \
    } while (0)


/*---------------------------------------------------------------------------*/
/* Function prototypes                                                       */
/*---------------------------------------------------------------------------*/

#ifdef __cplusplus
extern "C" {
#endif

extern DdNode * cuddAddExistAbstractRecur(DdManager *manager, DdNode *f, DdNode *cube);
extern DdNode * cuddAddUnivAbstractRecur(DdManager *manager, DdNode *f, DdNode *cube);
extern DdNode * cuddAddOrAbstractRecur(DdManager *manager, DdNode *f, DdNode *cube);
extern DdNode * cuddAddApplyRecur(DdManager *dd, DdNode * (*)(DdManager *, DdNode **, DdNode **), DdNode *f, DdNode *g);
extern DdNode * cuddAddMonadicApplyRecur(DdManager * dd, DdNode * (*op)(DdManager *, DdNode *), DdNode * f);
extern DdNode * cuddAddScalarInverseRecur(DdManager *dd, DdNode *f, DdNode *epsilon);
extern DdNode * cuddAddIteRecur(DdManager *dd, DdNode *f, DdNode *g, DdNode *h);
extern DdNode * cuddAddCmplRecur(DdManager *dd, DdNode *f);
extern DdNode * cuddAddNegateRecur(DdManager *dd, DdNode *f);
extern DdNode * cuddAddRoundOffRecur(DdManager *dd, DdNode *f, double trunc);
extern DdNode * cuddUnderApprox(DdManager *dd, DdNode *f, int numVars, int threshold, int safe, double quality);
extern DdNode * cuddRemapUnderApprox(DdManager *dd, DdNode *f, int numVars, int threshold, double quality);
extern DdNode * cuddBiasedUnderApprox(DdManager *dd, DdNode *f, DdNode *b, int numVars, int threshold, double quality1, double quality0);
extern DdNode * cuddBddAndAbstractRecur(DdManager *manager, DdNode *f, DdNode *g, DdNode *cube);
extern int cuddAnnealing(DdManager *table, int lower, int upper);
extern DdNode * cuddBddExistAbstractRecur(DdManager *manager, DdNode *f, DdNode *cube);
extern DdNode * cuddBddXorExistAbstractRecur(DdManager *manager, DdNode *f, DdNode *g, DdNode *cube);
extern DdNode * cuddBddBooleanDiffRecur(DdManager *manager, DdNode *f, DdNode *var);
extern DdNode * cuddBddIteRecur(DdManager *dd, DdNode *f, DdNode *g, DdNode *h);
extern DdNode * cuddBddIntersectRecur(DdManager *dd, DdNode *f, DdNode *g);
extern DdNode * cuddBddAndRecur(DdManager *manager, DdNode *f, DdNode *g);
extern DdNode * cuddBddXorRecur(DdManager *manager, DdNode *f, DdNode *g);
extern DdNode * cuddBddTransfer(DdManager *ddS, DdManager *ddD, DdNode *f);
extern DdNode * cuddAddBddDoPattern(DdManager *dd, DdNode *f);
extern int cuddInitCache(DdManager *unique, unsigned int cacheSize, unsigned int maxCacheSize);
extern void cuddCacheInsert(DdManager *table, ptruint op, DdNode *f, DdNode *g, DdNode *h, DdNode *data);
extern void cuddCacheInsert2(DdManager *table, DdNode * (*)(DdManager *, DdNode *, DdNode *), DdNode *f, DdNode *g, DdNode *data);
extern void cuddCacheInsert1(DdManager *table, DdNode * (*)(DdManager *, DdNode *), DdNode *f, DdNode *data);
extern DdNode * cuddCacheLookup(DdManager *table, ptruint op, DdNode *f, DdNode *g, DdNode *h);
extern DdNode * cuddCacheLookupZdd(DdManager *table, ptruint op, DdNode *f, DdNode *g, DdNode *h);
extern DdNode * cuddCacheLookup2(DdManager *table, DdNode * (*)(DdManager *, DdNode *, DdNode *), DdNode *f, DdNode *g);
extern DdNode * cuddCacheLookup1(DdManager *table, DdNode * (*)(DdManager *, DdNode *), DdNode *f);
extern DdNode * cuddCacheLookup2Zdd(DdManager *table, DdNode * (*)(DdManager *, DdNode *, DdNode *), DdNode *f, DdNode *g);
extern DdNode * cuddCacheLookup1Zdd(DdManager *table, DdNode * (*)(DdManager *, DdNode *), DdNode *f);
extern DdNode * cuddConstantLookup(DdManager *table, ptruint op, DdNode *f, DdNode *g, DdNode *h);
extern int cuddCacheProfile(DdManager *table, FILE *fp);
extern void cuddCacheResize(DdManager *table);
extern void cuddCacheFlush(DdManager *table);
extern int cuddComputeFloorLog2(unsigned int value);
extern int cuddHeapProfile(DdManager *dd);
extern void cuddPrintNode(DdNode *f, FILE *fp);
extern void cuddPrintVarGroups(DdManager * dd, MtrNode * root, int zdd, int silent);
extern DdNode * cuddBddClippingAnd(DdManager *dd, DdNode *f, DdNode *g, int maxDepth, int direction);
extern DdNode * cuddBddClippingAndAbstract(DdManager *dd, DdNode *f, DdNode *g, DdNode *cube, int maxDepth, int direction);
extern void cuddGetBranches(DdNode *g, DdNode **g1, DdNode **g0);
extern DdNode * cuddCofactorRecur(DdManager *dd, DdNode *f, DdNode *g);
extern DdNode * cuddBddComposeRecur(DdManager *dd, DdNode *f, DdNode *g, DdNode *proj);
extern DdNode * cuddAddComposeRecur(DdManager *dd, DdNode *f, DdNode *g, DdNode *proj);
extern int cuddExact(DdManager *table, int lower, int upper);
extern DdNode * cuddBddConstrainRecur(DdManager *dd, DdNode *f, DdNode *c);
extern DdNode * cuddBddRestrictRecur(DdManager *dd, DdNode *f, DdNode *c);
extern DdNode * cuddBddNPAndRecur(DdManager *dd, DdNode *f, DdNode *c);
extern DdNode * cuddAddConstrainRecur(DdManager *dd, DdNode *f, DdNode *c);
extern DdNode * cuddAddRestrictRecur(DdManager *dd, DdNode *f, DdNode *c);
extern DdNode * cuddBddLICompaction(DdManager *dd, DdNode *f, DdNode *c);
extern int cuddGa(DdManager *table, int lower, int upper);
extern int cuddTreeSifting(DdManager *table, Cudd_ReorderingType method);
extern int cuddZddInitUniv(DdManager *zdd);
extern void cuddZddFreeUniv(DdManager *zdd);
extern void cuddSetInteract(DdManager *table, int x, int y);
extern int cuddTestInteract(DdManager *table, int x, int y);
extern int cuddInitInteract(DdManager *table);
extern DdLocalCache * cuddLocalCacheInit(DdManager *manager, unsigned int keySize, unsigned int cacheSize, unsigned int maxCacheSize);
extern void cuddLocalCacheQuit(DdLocalCache *cache);
extern void cuddLocalCacheInsert(DdLocalCache *cache, DdNodePtr *key, DdNode *value);
extern DdNode * cuddLocalCacheLookup(DdLocalCache *cache, DdNodePtr *key);
extern void cuddLocalCacheClearDead(DdManager *manager);
extern int cuddIsInDeathRow(DdManager *dd, DdNode *f);
extern int cuddTimesInDeathRow(DdManager *dd, DdNode *f);
extern void cuddLocalCacheClearAll(DdManager *manager);
#ifdef DD_CACHE_PROFILE
extern int cuddLocalCacheProfile(DdLocalCache *cache);
#endif
extern DdHashTable * cuddHashTableInit(DdManager *manager, unsigned int keySize, unsigned int initSize);
extern void cuddHashTableQuit(DdHashTable *hash);
extern void cuddHashTableGenericQuit(DdHashTable *hash);
extern int cuddHashTableInsert(DdHashTable *hash, DdNodePtr *key, DdNode *value, ptrint count);
extern DdNode * cuddHashTableLookup(DdHashTable *hash, DdNodePtr *key);
extern int cuddHashTableInsert1(DdHashTable *hash, DdNode *f, DdNode *value, ptrint count);
extern DdNode * cuddHashTableLookup1(DdHashTable *hash, DdNode *f);
extern int cuddHashTableInsert2(DdHashTable *hash, DdNode *f, DdNode *g, DdNode *value, ptrint count);
extern DdNode * cuddHashTableLookup2(DdHashTable *hash, DdNode *f, DdNode *g);
extern int cuddHashTableInsert3(DdHashTable *hash, DdNode *f, DdNode *g, DdNode *h, DdNode *value, ptrint count);
extern DdNode * cuddHashTableLookup3(DdHashTable *hash, DdNode *f, DdNode *g, DdNode *h);
extern int cuddHashTableGenericInsert(DdHashTable * hash, DdNode * f, void * value);
extern void * cuddHashTableGenericLookup(DdHashTable * hash, DdNode * f);
extern DdLevelQueue * cuddLevelQueueInit(int levels, int itemSize, int numBuckets, DdManager * manager);
extern void cuddLevelQueueQuit(DdLevelQueue *queue);
extern void * cuddLevelQueueFirst(DdLevelQueue * queue, void * key, int  level);
extern void * cuddLevelQueueEnqueue(DdLevelQueue *queue, void *key, int level);
extern void cuddLevelQueueDequeue(DdLevelQueue *queue, int level);
extern int cuddLinearAndSifting(DdManager *table, int lower, int upper);
extern int cuddLinearInPlace(DdManager * table, int  x, int  y);
extern void cuddUpdateInteractionMatrix(DdManager * table, int  xindex, int  yindex);
extern int cuddInitLinear(DdManager *table);
extern int cuddResizeLinear(DdManager *table);
extern DdNode * cuddBddLiteralSetIntersectionRecur(DdManager *dd, DdNode *f, DdNode *g);
extern DdNode * cuddCProjectionRecur(DdManager *dd, DdNode *R, DdNode *Y, DdNode *Ysupp);
extern DdNode * cuddBddClosestCube(DdManager *dd, DdNode *f, DdNode *g, CUDD_VALUE_TYPE bound);
extern void cuddReclaim(DdManager *table, DdNode *n);
extern void cuddReclaimZdd(DdManager *table, DdNode *n);
extern void cuddClearDeathRow(DdManager *table);
extern void cuddShrinkDeathRow(DdManager *table);
extern DdNode * cuddDynamicAllocNode(DdManager *table);
extern int cuddSifting(DdManager *table, int lower, int upper);
extern int cuddSwapping(DdManager *table, int lower, int upper, Cudd_ReorderingType heuristic);
extern int cuddNextHigh(DdManager *table, int x);
extern int cuddNextLow(DdManager *table, int x);
extern int cuddSwapInPlace(DdManager *table, int x, int y);
extern int cuddBddAlignToZdd(DdManager *table);
extern DdNode * cuddBddMakePrime(DdManager *dd, DdNode *cube, DdNode *f);
extern DdNode * cuddSolveEqnRecur(DdManager *bdd, DdNode *F, DdNode *Y, DdNode **G, int n, int *yIndex, int i);
extern DdNode * cuddVerifySol(DdManager *bdd, DdNode *F, DdNode **G, int *yIndex, int n);
#ifdef ST_H_
extern DdNode* cuddSplitSetRecur(DdManager *manager, st_table *mtable, int *varSeen, DdNode *p, double n, double max, int index);
#endif
extern DdNode * cuddSubsetHeavyBranch(DdManager *dd, DdNode *f, int numVars, int threshold);
extern DdNode * cuddSubsetShortPaths(DdManager *dd, DdNode *f, int numVars, int threshold, int hardlimit);
extern int cuddSymmCheck(DdManager *table, int x, int y);
extern int cuddSymmSifting(DdManager *table, int lower, int upper);
extern int cuddSymmSiftingConv(DdManager *table, int lower, int upper);
extern DdNode * cuddAllocNode(DdManager *unique);
extern DdManager * cuddInitTable(unsigned int numVars, unsigned int numVarsZ, unsigned int numSlots, unsigned int looseUpTo);
extern void cuddFreeTable(DdManager *unique);
extern int cuddGarbageCollect(DdManager *unique, int clearCache);
extern DdNode * cuddZddGetNode(DdManager *zdd, int id, DdNode *T, DdNode *E);
extern DdNode * cuddZddGetNodeIVO(DdManager *dd, int index, DdNode *g, DdNode *h);
extern DdNode * cuddUniqueInter(DdManager *unique, int index, DdNode *T, DdNode *E);
extern DdNode * cuddUniqueInterIVO(DdManager *unique, int index, DdNode *T, DdNode *E);
extern DdNode * cuddUniqueInterZdd(DdManager *unique, int index, DdNode *T, DdNode *E);
extern DdNode * cuddUniqueConst(DdManager *unique, CUDD_VALUE_TYPE value);
extern void cuddRehash(DdManager *unique, int i);
extern void cuddShrinkSubtable(DdManager *unique, int i);
extern int cuddInsertSubtables(DdManager *unique, int n, int level);
extern int cuddDestroySubtables(DdManager *unique, int n);
extern int cuddResizeTableZdd(DdManager *unique, int index);
extern void cuddSlowTableGrowth(DdManager *unique);
extern int cuddP(DdManager *dd, DdNode *f);
#ifdef ST_H_
extern enum st_retval cuddStCountfree(void *key, void *value, void *arg);
extern int cuddCollectNodes(DdNode *f, st_table *visited);
#endif
extern DdNodePtr * cuddNodeArray(DdNode *f, int *n);
extern int cuddWindowReorder(DdManager *table, int low, int high, Cudd_ReorderingType submethod);
extern DdNode * cuddZddProduct(DdManager *dd, DdNode *f, DdNode *g);
extern DdNode * cuddZddUnateProduct(DdManager *dd, DdNode *f, DdNode *g);
extern DdNode * cuddZddWeakDiv(DdManager *dd, DdNode *f, DdNode *g);
extern DdNode * cuddZddWeakDivF(DdManager *dd, DdNode *f, DdNode *g);
extern DdNode * cuddZddDivide(DdManager *dd, DdNode *f, DdNode *g);
extern DdNode * cuddZddDivideF(DdManager *dd, DdNode *f, DdNode *g);
extern int cuddZddGetCofactors3(DdManager *dd, DdNode *f, int v, DdNode **f1, DdNode **f0, DdNode **fd);
extern int cuddZddGetCofactors2(DdManager *dd, DdNode *f, int v, DdNode **f1, DdNode **f0);
extern DdNode * cuddZddComplement(DdManager *dd, DdNode *node);
extern int cuddZddGetPosVarIndex(DdManager * dd, int index);
extern int cuddZddGetNegVarIndex(DdManager * dd, int index);
extern int cuddZddGetPosVarLevel(DdManager * dd, int index);
extern int cuddZddGetNegVarLevel(DdManager * dd, int index);
extern int cuddZddTreeSifting(DdManager *table, Cudd_ReorderingType method);
extern DdNode * cuddZddIsop(DdManager *dd, DdNode *L, DdNode *U, DdNode **zdd_I);
extern DdNode * cuddBddIsop(DdManager *dd, DdNode *L, DdNode *U);
extern DdNode * cuddMakeBddFromZddCover(DdManager *dd, DdNode *node);
extern int cuddZddLinearSifting(DdManager *table, int lower, int upper);
extern int cuddZddAlignToBdd(DdManager *table);
extern int cuddZddNextHigh(DdManager *table, int x);
extern int cuddZddNextLow(DdManager *table, int x);
extern int cuddZddUniqueCompare(void const *ptr_x, void const *ptr_y);
extern int cuddZddSwapInPlace(DdManager *table, int x, int y);
extern int cuddZddSwapping(DdManager *table, int lower, int upper, Cudd_ReorderingType heuristic);
extern int cuddZddSifting(DdManager *table, int lower, int upper);
extern DdNode * cuddZddIte(DdManager *dd, DdNode *f, DdNode *g, DdNode *h);
extern DdNode * cuddZddUnion(DdManager *zdd, DdNode *P, DdNode *Q);
extern DdNode * cuddZddIntersect(DdManager *zdd, DdNode *P, DdNode *Q);
extern DdNode * cuddZddDiff(DdManager *zdd, DdNode *P, DdNode *Q);
extern DdNode * cuddZddChangeAux(DdManager *zdd, DdNode *P, DdNode *zvar);
extern DdNode * cuddZddSubset1(DdManager *dd, DdNode *P, int var);
extern DdNode * cuddZddSubset0(DdManager *dd, DdNode *P, int var);
extern DdNode * cuddZddChange(DdManager *dd, DdNode *P, int var);
extern int cuddZddSymmCheck(DdManager *table, int x, int y);
extern int cuddZddSymmSifting(DdManager *table, int lower, int upper);
extern int cuddZddSymmSiftingConv(DdManager *table, int lower, int upper);
extern int cuddZddP(DdManager *zdd, DdNode *f);

#ifdef __cplusplus
} /* end of extern "C" */
#endif

#endif /* CUDD_INT_H_ */