cuddapi.c

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

******************************************************************************/
int
Cudd_ReadSiftMaxSwap(
  DdManager * dd)
{
    return(dd->siftMaxSwap);

} /* end of Cudd_ReadSiftMaxSwap */


/**Function********************************************************************

  Synopsis    [Sets the siftMaxSwap parameter of the manager.]

  Description [Sets the siftMaxSwap parameter of the manager. This
  parameter gives the maximum number of swaps that will be attempted
  for each invocation of sifting. The real number of swaps may exceed
  the set limit because the package will always complete the sifting
  of the variable that causes the limit to be reached.]

  SideEffects [None]

  SeeAlso     [Cudd_SetSiftMaxVar Cudd_ReadSiftMaxSwap]

******************************************************************************/
void
Cudd_SetSiftMaxSwap(
  DdManager * dd,
  int  sms)
{
    dd->siftMaxSwap = sms;

} /* end of Cudd_SetSiftMaxSwap */


/**Function********************************************************************

  Synopsis    [Reads the maxGrowth parameter of the manager.]

  Description [Reads the maxGrowth parameter of the manager.  This
  parameter determines how much the number of nodes can grow during
  sifting of a variable.  Overall, sifting never increases the size of
  the decision diagrams.  This parameter only refers to intermediate
  results.  A lower value will speed up sifting, possibly at the
  expense of quality.]

  SideEffects [None]

  SeeAlso     [Cudd_SetMaxGrowth Cudd_ReadMaxGrowthAlternate]

******************************************************************************/
double
Cudd_ReadMaxGrowth(
  DdManager * dd)
{
    return(dd->maxGrowth);

} /* end of Cudd_ReadMaxGrowth */


/**Function********************************************************************

  Synopsis    [Sets the maxGrowth parameter of the manager.]

  Description [Sets the maxGrowth parameter of the manager.  This
  parameter determines how much the number of nodes can grow during
  sifting of a variable.  Overall, sifting never increases the size of
  the decision diagrams.  This parameter only refers to intermediate
  results.  A lower value will speed up sifting, possibly at the
  expense of quality.]

  SideEffects [None]

  SeeAlso     [Cudd_ReadMaxGrowth Cudd_SetMaxGrowthAlternate]

******************************************************************************/
void
Cudd_SetMaxGrowth(
  DdManager * dd,
  double mg)
{
    dd->maxGrowth = mg;

} /* end of Cudd_SetMaxGrowth */


/**Function********************************************************************

  Synopsis    [Reads the maxGrowthAlt parameter of the manager.]

  Description [Reads the maxGrowthAlt parameter of the manager.  This
  parameter is analogous to the maxGrowth paramter, and is used every
  given number of reorderings instead of maxGrowth.  The number of
  reorderings is set with Cudd_SetReorderingCycle.  If the number of
  reorderings is 0 (default) maxGrowthAlt is never used.]

  SideEffects [None]

  SeeAlso     [Cudd_ReadMaxGrowth Cudd_SetMaxGrowthAlternate
  Cudd_SetReorderingCycle Cudd_ReadReorderingCycle]

******************************************************************************/
double
Cudd_ReadMaxGrowthAlternate(
  DdManager * dd)
{
    return(dd->maxGrowthAlt);

} /* end of Cudd_ReadMaxGrowthAlternate */


/**Function********************************************************************

  Synopsis    [Sets the maxGrowthAlt parameter of the manager.]

  Description [Sets the maxGrowthAlt parameter of the manager.  This
  parameter is analogous to the maxGrowth paramter, and is used every
  given number of reorderings instead of maxGrowth.  The number of
  reorderings is set with Cudd_SetReorderingCycle.  If the number of
  reorderings is 0 (default) maxGrowthAlt is never used.]

  SideEffects [None]

  SeeAlso     [Cudd_ReadMaxGrowthAlternate Cudd_SetMaxGrowth
  Cudd_SetReorderingCycle Cudd_ReadReorderingCycle]

******************************************************************************/
void
Cudd_SetMaxGrowthAlternate(
  DdManager * dd,
  double mg)
{
    dd->maxGrowthAlt = mg;

} /* end of Cudd_SetMaxGrowthAlternate */


/**Function********************************************************************

  Synopsis    [Reads the reordCycle parameter of the manager.]

  Description [Reads the reordCycle parameter of the manager.  This
  parameter determines how often the alternate threshold on maximum
  growth is used in reordering.]

  SideEffects [None]

  SeeAlso     [Cudd_ReadMaxGrowthAlternate Cudd_SetMaxGrowthAlternate
  Cudd_SetReorderingCycle]

******************************************************************************/
int
Cudd_ReadReorderingCycle(
  DdManager * dd)
{
    return(dd->reordCycle);

} /* end of Cudd_ReadReorderingCycle */


/**Function********************************************************************

  Synopsis    [Sets the reordCycle parameter of the manager.]

  Description [Sets the reordCycle parameter of the manager.  This
  parameter determines how often the alternate threshold on maximum
  growth is used in reordering.]

  SideEffects [None]

  SeeAlso     [Cudd_ReadMaxGrowthAlternate Cudd_SetMaxGrowthAlternate
  Cudd_ReadReorderingCycle]

******************************************************************************/
void
Cudd_SetReorderingCycle(
  DdManager * dd,
  int cycle)
{
    dd->reordCycle = cycle;

} /* end of Cudd_SetReorderingCycle */


/**Function********************************************************************

  Synopsis    [Returns the variable group tree of the manager.]

  Description []

  SideEffects [None]

  SeeAlso     [Cudd_SetTree Cudd_FreeTree Cudd_ReadZddTree]

******************************************************************************/
MtrNode *
Cudd_ReadTree(
  DdManager * dd)
{
    return(dd->tree);

} /* end of Cudd_ReadTree */


/**Function********************************************************************

  Synopsis    [Sets the variable group tree of the manager.]

  Description []

  SideEffects [None]

  SeeAlso     [Cudd_FreeTree Cudd_ReadTree Cudd_SetZddTree]

******************************************************************************/
void
Cudd_SetTree(
  DdManager * dd,
  MtrNode * tree)
{
    if (dd->tree != NULL) {
	Mtr_FreeTree(dd->tree);
    }
    dd->tree = tree;
    if (tree == NULL) return;

    fixVarTree(tree, dd->perm, dd->size);
    return;

} /* end of Cudd_SetTree */


/**Function********************************************************************

  Synopsis    [Frees the variable group tree of the manager.]

  Description []

  SideEffects [None]

  SeeAlso     [Cudd_SetTree Cudd_ReadTree Cudd_FreeZddTree]

******************************************************************************/
void
Cudd_FreeTree(
  DdManager * dd)
{
    if (dd->tree != NULL) {
	Mtr_FreeTree(dd->tree);
	dd->tree = NULL;
    }
    return;

} /* end of Cudd_FreeTree */


/**Function********************************************************************

  Synopsis    [Returns the variable group tree of the manager.]

  Description []

  SideEffects [None]

  SeeAlso     [Cudd_SetZddTree Cudd_FreeZddTree Cudd_ReadTree]

******************************************************************************/
MtrNode *
Cudd_ReadZddTree(
  DdManager * dd)
{
    return(dd->treeZ);

} /* end of Cudd_ReadZddTree */


/**Function********************************************************************

  Synopsis    [Sets the ZDD variable group tree of the manager.]

  Description []

  SideEffects [None]

  SeeAlso     [Cudd_FreeZddTree Cudd_ReadZddTree Cudd_SetTree]

******************************************************************************/
void
Cudd_SetZddTree(
  DdManager * dd,
  MtrNode * tree)
{
    if (dd->treeZ != NULL) {
	Mtr_FreeTree(dd->treeZ);
    }
    dd->treeZ = tree;
    if (tree == NULL) return;

    fixVarTree(tree, dd->permZ, dd->sizeZ);
    return;

} /* end of Cudd_SetZddTree */


/**Function********************************************************************

  Synopsis    [Frees the variable group tree of the manager.]

  Description []

  SideEffects [None]

  SeeAlso     [Cudd_SetZddTree Cudd_ReadZddTree Cudd_FreeTree]

******************************************************************************/
void
Cudd_FreeZddTree(
  DdManager * dd)
{
    if (dd->treeZ != NULL) {
	Mtr_FreeTree(dd->treeZ);
	dd->treeZ = NULL;
    }
    return;

} /* end of Cudd_FreeZddTree */


/**Function********************************************************************

  Synopsis    [Returns the index of the node.]

  Description [Returns the index of the node. The node pointer can be
  either regular or complemented.]

  SideEffects [None]

  SeeAlso [Cudd_ReadIndex]

******************************************************************************/
unsigned int
Cudd_NodeReadIndex(
  DdNode * node)
{
    return((unsigned int) Cudd_Regular(node)->index);

} /* end of Cudd_NodeReadIndex */


/**Function********************************************************************

  Synopsis    [Returns the current position of the i-th variable in the
  order.]

  Description [Returns the current position of the i-th variable in
  the order. If the index is CUDD_CONST_INDEX, returns
  CUDD_CONST_INDEX; otherwise, if the index is out of bounds returns
  -1.]

  SideEffects [None]

  SeeAlso     [Cudd_ReadInvPerm Cudd_ReadPermZdd]

******************************************************************************/
int
Cudd_ReadPerm(
  DdManager * dd,
  int  i)
{
    if (i == CUDD_CONST_INDEX) return(CUDD_CONST_INDEX);
    if (i < 0 || i >= dd->size) return(-1);
    return(dd->perm[i]);

} /* end of Cudd_ReadPerm */


/**Function********************************************************************

  Synopsis    [Returns the current position of the i-th ZDD variable in the
  order.]

  Description [Returns the current position of the i-th ZDD variable
  in the order. If the index is CUDD_CONST_INDEX, returns
  CUDD_CONST_INDEX; otherwise, if the index is out of bounds returns
  -1.]

  SideEffects [None]

  SeeAlso     [Cudd_ReadInvPermZdd Cudd_ReadPerm]

******************************************************************************/
int
Cudd_ReadPermZdd(
  DdManager * dd,
  int  i)
{
    if (i == CUDD_CONST_INDEX) return(CUDD_CONST_INDEX);
    if (i < 0 || i >= dd->sizeZ) return(-1);
    return(dd->permZ[i]);

} /* end of Cudd_ReadPermZdd */


/**Function********************************************************************

  Synopsis    [Returns the index of the variable currently in the i-th
  position of the order.]

  Description [Returns the index of the variable currently in the i-th
  position of the order. If the index is CUDD_CONST_INDEX, returns
  CUDD_CONST_INDEX; otherwise, if the index is out of bounds returns -1.]

  SideEffects [None]

  SeeAlso     [Cudd_ReadPerm Cudd_ReadInvPermZdd]

******************************************************************************/
int
Cudd_ReadInvPerm(
  DdManager * dd,
  int  i)
{
    if (i == CUDD_CONST_INDEX) return(CUDD_CONST_INDEX);
    if (i < 0 || i >= dd->size) return(-1);
    return(dd->invperm[i]);

} /* end of Cudd_ReadInvPerm */


/**Function********************************************************************

  Synopsis    [Returns the index of the ZDD variable currently in the i-th
  position of the order.]

  Description [Returns the index of the ZDD variable currently in the
  i-th position of the order. If the index is CUDD_CONST_INDEX, returns
  CUDD_CONST_INDEX; otherwise, if the index is out of bounds returns -1.]

  SideEffects [None]

  SeeAlso     [Cudd_ReadPerm Cudd_ReadInvPermZdd]

******************************************************************************/
int
Cudd_ReadInvPermZdd(
  DdManager * dd,
  int  i)
{
    if (i == CUDD_CONST_INDEX) return(CUDD_CONST_INDEX);
    if (i < 0 || i >= dd->sizeZ) return(-1);
    return(dd->invpermZ[i]);

} /* end of Cudd_ReadInvPermZdd */


/**Function********************************************************************

  Synopsis    [Returns the i-th element of the vars array.]

  Description [Returns the i-th element of the vars array if it falls
  within the array bounds; NULL otherwise. If i is the index of an
  existing variable, this function produces the same result as
  Cudd_bddIthVar. However, if the i-th var does not exist yet,
  Cudd_bddIthVar will create it, whereas Cudd_ReadVars will not.]

  SideEffects [None]

  SeeAlso     [Cudd_bddIthVar]

******************************************************************************/
DdNode *
Cudd_ReadVars(
  DdManager * dd,
  int  i)
{
    if (i < 0 || i >