cuddint.h

主要进行大规模的电路综合

    int symmviolation;		/* Used during group sifting */
    int arcviolation;		/* Used during group sifting */
    int populationSize;		/* population size for GA */
    int	numberXovers;		/* number of crossovers for GA */
    DdLocalCache *localCaches;	/* local caches currently in existence */
#ifdef __osf__
#pragma pointer_size restore
#endif
    char *hooks;		/* application-specific field (used by vis) */
    DdHook *preGCHook;		/* hooks to be called before GC */
    DdHook *postGCHook;		/* hooks to be called after GC */
    DdHook *preReorderingHook;	/* hooks to be called before reordering */
    DdHook *postReorderingHook;	/* hooks to be called after reordering */
    FILE *out;			/* stdout for this manager */
    FILE *err;			/* stderr for this manager */
#ifdef __osf__
#pragma pointer_size save
#pragma pointer_size short
#endif
    Cudd_ErrorType errorCode;	/* info on last error */
    /* Statistical counters. */
    long memused;		/* total memory allocated for the manager */
    long maxmem;		/* target maximum memory */
    long maxmemhard;		/* hard limit for maximum memory */
    int garbageCollections;	/* number of garbage collections */
    long GCTime;		/* total time spent in garbage collection */
    long reordTime;		/* total time spent in reordering */
    double totCachehits;	/* total number of cache hits */
    double totCacheMisses;	/* total number of cache misses */
    double cachecollisions;	/* number of cache collisions */
    double cacheinserts;	/* number of cache insertions */
    double cacheLastInserts;	/* insertions at the last cache resizing */
    double cachedeletions;	/* number of deletions during garbage coll. */
#ifdef DD_STATS
    double nodesFreed;		/* number of nodes returned to the free list */
    double nodesDropped;	/* number of nodes killed by dereferencing */
#endif
    unsigned int peakLiveNodes;	/* maximum number of live nodes */
#ifdef DD_UNIQUE_PROFILE
    double uniqueLookUps;	/* number of unique table lookups */
    double uniqueLinks;		/* total distance traveled in coll. chains */
#endif
#ifdef DD_COUNT
    double recursiveCalls;	/* number of recursive calls */
#ifdef DD_STATS
    double nextSample;		/* when to write next line of stats */
#endif
    double swapSteps;		/* number of elementary reordering steps */
#endif
#ifdef DD_MIS
    /* mis/verif compatibility fields */
    array_t *iton;		/* maps ids in ddNode to node_t */
    array_t *order;		/* copy of order_list */
    lsHandle handle;		/* where it is in network BDD list */
    network_t *network;
    st_table *local_order;	/* for local BDDs */
    int nvars;			/* variables used so far */
    int threshold;		/* for pseudo var threshold value*/
#endif
};

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

/* Generic level queue item. */
typedef struct DdQueueItem {
    struct DdQueueItem *next;
    struct DdQueueItem *cnext;
    void *key;
} DdQueueItem;

/* Level queue. */
typedef struct DdLevelQueue {
    void *first;
    DdQueueItem **last;
    DdQueueItem *freelist;
    DdQueueItem **buckets;
    int levels;
    int itemsize;
    int size;
    int maxsize;
    int numBuckets;
    int shift;
} DdLevelQueue;

#ifdef __osf__
#pragma pointer_size restore
#endif

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


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

/**Macro***********************************************************************

  Synopsis    [Adds node to the head of the free list.]

  Description [Adds node to the head of the free list.  Does not
  deallocate memory chunks that become free.  This function is also
  used by the dynamic reordering functions.]

  SideEffects [None]

  SeeAlso     [cuddAllocNode cuddDynamicAllocNode]

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


/**Macro***********************************************************************

  Synopsis     [Increases the reference count of a node, if it is not
  saturated.]

  Description  [Increases the reference count of a node, if it is not
  saturated. This being a macro, it is faster than Cudd_Ref, but it
  cannot be used in constructs like cuddRef(a = b()).]

  SideEffects  [none]

  SeeAlso      [Cudd_Ref]

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


/**Macro***********************************************************************

  Synopsis     [Decreases the reference count of a node, if it is not
  saturated.]

  Description  [Decreases the reference count of node. It is primarily
  used in recursive procedures to decrease the ref count of a result
  node before returning it. This accomplishes the goal of removing the
  protection applied by a previous cuddRef. This being a macro, it is
  faster than Cudd_Deref, but it cannot be used in constructs like
  cuddDeref(a = b()).]

  SideEffects  [none]

  SeeAlso      [Cudd_Deref]

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


/**Macro***********************************************************************

  Synopsis     [Returns 1 if the node is a constant node.]

  Description  [Returns 1 if the node is a constant node (rather than an
  internal node). All constant nodes have the same index
  (CUDD_CONST_INDEX). The pointer passed to cuddIsConstant must be regular.]

  SideEffects  [none]

  SeeAlso      [Cudd_IsConstant]

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


/**Macro***********************************************************************

  Synopsis     [Returns the then child of an internal node.]

  Description  [Returns the then child of an internal node. If
  <code>node</code> is a constant node, the result is unpredictable.
  The pointer passed to cuddT must be regular.]

  SideEffects  [none]

  SeeAlso      [Cudd_T]

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


/**Macro***********************************************************************

  Synopsis     [Returns the else child of an internal node.]

  Description  [Returns the else child of an internal node. If
  <code>node</code> is a constant node, the result is unpredictable.
  The pointer passed to cuddE must be regular.]

  SideEffects  [none]

  SeeAlso      [Cudd_E]

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


/**Macro***********************************************************************

  Synopsis     [Returns the value of a constant node.]

  Description  [Returns the value of a constant node. If
  <code>node</code> is an internal node, the result is unpredictable.
  The pointer passed to cuddV must be regular.]

  SideEffects  [none]

  SeeAlso      [Cudd_V]

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


/**Macro***********************************************************************

  Synopsis    [Finds the current position of variable index in the
  order.]

  Description [Finds the current position of variable index in the
  order.  This macro duplicates the functionality of Cudd_ReadPerm,
  but it does not check for out-of-bounds indices and it is more
  efficient.]

  SideEffects [none]

  SeeAlso     [Cudd_ReadPerm]

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


/**Macro***********************************************************************

  Synopsis    [Finds the current position of ZDD variable index in the
  order.]

  Description [Finds the current position of ZDD variable index in the
  order.  This macro duplicates the functionality of Cudd_ReadPermZdd,
  but it does not check for out-of-bounds indices and it is more
  efficient.]

  SideEffects [none]

  SeeAlso     [Cudd_ReadPermZdd]

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


/**Macro***********************************************************************

  Synopsis    [Hash function for the unique table.]

  Description []

  SideEffects [none]

  SeeAlso     [ddCHash ddCHash2]

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


/**Macro***********************************************************************

  Synopsis    [Hash function for the cache.]

  Description []

  SideEffects [none]

  SeeAlso     [ddHash ddCHash2]

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


/**Macro***********************************************************************

  Synopsis    [Hash function for the cache for functions with two
  operands.]

  Description []

  SideEffects [none]

  SeeAlso     [ddHash ddCHash]

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


/**Macro***********************************************************************

  Synopsis    [Clears the 4 least significant bits of a pointer.]

  Description []

  SideEffects [none]

  SeeAlso     []

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


/**Macro***********************************************************************

  Synopsis    [Computes the minimum of two numbers.]

  Description []

  SideEffects [none]

  SeeAlso     [ddMax]

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


/**Macro***********************************************************************

  Synopsis    [Computes the maximum of two numbers.]

  Description []

  SideEffects [none]

  SeeAlso     [ddMin]

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


/**Macro***********************************************************************

  Synopsis    [Computes the absolute value of a number.]

  Description []

  SideEffects [none]

  SeeAlso     []

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