cudd.h

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

struct DdNode {
    DdHalfWord index;
    DdHalfWord ref;		/* reference count */
    DdNode *next;		/* next pointer for unique table */
    union {
	CUDD_VALUE_TYPE value;	/* for constant nodes */
	DdChildren kids;	/* for internal nodes */
    } type;
};

#ifdef __osf__
#pragma pointer_size restore
#endif

typedef struct DdManager DdManager;

typedef struct DdGen DdGen;

/* These typedefs for arbitrary precision arithmetic should agree with
** the corresponding constant definitions above. */
typedef unsigned short int DdApaDigit;
typedef unsigned long int DdApaDoubleDigit;
typedef DdApaDigit * DdApaNumber;

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


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


/**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 Cudd_IsConstant may be either
  regular or complemented.]

  SideEffects  [none]

  SeeAlso      []

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


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

  Synopsis     [Complements a DD.]

  Description  [Complements a DD by flipping the complement attribute of
  the pointer (the least significant bit).]

  SideEffects  [none]

  SeeAlso      [Cudd_NotCond]

******************************************************************************/
#define Cudd_Not(node) ((DdNode *)((long)(node) ^ 01))


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

  Synopsis     [Complements a DD if a condition is true.]

  Description  [Complements a DD if condition c is true; c should be
  either 0 or 1, because it is used directly (for efficiency). If in
  doubt on the values c may take, use "(c) ? Cudd_Not(node) : node".]

  SideEffects  [none]

  SeeAlso      [Cudd_Not]

******************************************************************************/
#define Cudd_NotCond(node,c) ((DdNode *)((long)(node) ^ (c)))


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

  Synopsis     [Returns the regular version of a pointer.]

  Description  []

  SideEffects  [none]

  SeeAlso      [Cudd_Complement Cudd_IsComplement]

******************************************************************************/
#define Cudd_Regular(node) ((DdNode *)((unsigned long)(node) & ~01))


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

  Synopsis     [Returns the complemented version of a pointer.]

  Description  []

  SideEffects  [none]

  SeeAlso      [Cudd_Regular Cudd_IsComplement]

******************************************************************************/
#define Cudd_Complement(node) ((DdNode *)((unsigned long)(node) | 01))


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

  Synopsis     [Returns 1 if a pointer is complemented.]

  Description  []

  SideEffects  [none]

  SeeAlso      [Cudd_Regular Cudd_Complement]

******************************************************************************/
#define Cudd_IsComplement(node)	((int) ((long) (node) & 01))


/**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.]

  SideEffects  [none]

  SeeAlso      [Cudd_E Cudd_V]

******************************************************************************/
#define Cudd_T(node) ((Cudd_Regular(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.]

  SideEffects  [none]

  SeeAlso      [Cudd_T Cudd_V]

******************************************************************************/
#define Cudd_E(node) ((Cudd_Regular(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.]

  SideEffects  [none]

  SeeAlso      [Cudd_T Cudd_E]

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


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

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

  Description [Returns the current position in the order of variable
  index. This macro is obsolete and is kept for compatibility. New
  applications should use Cudd_ReadPerm instead.]

  SideEffects  [none]

  SeeAlso      [Cudd_ReadPerm]

******************************************************************************/
#define Cudd_ReadIndex(dd,index) (Cudd_ReadPerm(dd,index))


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

  Synopsis     [Iterates over the cubes of a decision diagram.]

  Description  [Iterates over the cubes of a decision diagram f.
  <ul>
  <li> DdManager *manager;
  <li> DdNode *f;
  <li> DdGen *gen;
  <li> int *cube;
  <li> CUDD_VALUE_TYPE value;
  </ul>
  Cudd_ForeachCube allocates and frees the generator. Therefore the
  application should not try to do that. Also, the cube is freed at the
  end of Cudd_ForeachCube and hence is not available outside of the loop.<p>
  CAUTION: It is assumed that dynamic reordering will not occur while
  there are open generators. It is the user's responsibility to make sure
  that dynamic reordering does not occur. As long as new nodes are not created
  during generation, and dynamic reordering is not called explicitly,
  dynamic reordering will not occur. Alternatively, it is sufficient to
  disable dynamic reordering. It is a mistake to dispose of a diagram
  on which generation is ongoing.]

  SideEffects  [none]

  SeeAlso      [Cudd_ForeachNode Cudd_FirstCube Cudd_NextCube Cudd_GenFree
  Cudd_IsGenEmpty Cudd_AutodynDisable]

******************************************************************************/
#define Cudd_ForeachCube(manager, f, gen, cube, value)\
    for((gen) = Cudd_FirstCube(manager, f, &cube, &value);\
	Cudd_IsGenEmpty(gen) ? Cudd_GenFree(gen) : TRUE;\
	(void) Cudd_NextCube(gen, &cube, &value))


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

  Synopsis     [Iterates over the nodes of a decision diagram.]

  Description  [Iterates over the nodes of a decision diagram f.
  <ul>
  <li> DdManager *manager;
  <li> DdNode *f;
  <li> DdGen *gen;
  <li> DdNode *node;
  </ul>
  The nodes are returned in a seemingly random order.
  Cudd_ForeachNode allocates and frees the generator. Therefore the
  application should not try to do that.<p>
  CAUTION: It is assumed that dynamic reordering will not occur while
  there are open generators. It is the user's responsibility to make sure
  that dynamic reordering does not occur. As long as new nodes are not created
  during generation, and dynamic reordering is not called explicitly,
  dynamic reordering will not occur. Alternatively, it is sufficient to