cuddapi.c

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

  variable group tree is created by expanding the BDD variable
  tree. In any case, the ZDD variables derived from the same BDD
  variable are merged in a ZDD variable group. If a ZDD variable group
  tree exists, it is freed. Returns 1 if successful; 0 otherwise.]

  SideEffects [None]

  SeeAlso     [Cudd_bddNewVar Cudd_bddIthVar Cudd_bddNewVarAtLevel]

******************************************************************************/
int
Cudd_zddVarsFromBddVars(
  DdManager * dd /* DD manager */,
  int multiplicity /* how many ZDD variables are created for each BDD variable */)
{
    int res;
    int i, j;
    int allnew;
    int *permutation;

    if (multiplicity < 1) return(0);
    allnew = dd->sizeZ == 0;
    if (dd->size * multiplicity > dd->sizeZ) {
	res = cuddResizeTableZdd(dd,dd->size * multiplicity - 1);
	if (res == 0) return(0);
    }
    /* Impose the order of the BDD variables to the ZDD variables. */
    if (allnew) {
	for (i = 0; i < dd->size; i++) {
	    for (j = 0; j < multiplicity; j++) {
		dd->permZ[i * multiplicity + j] =
		    dd->perm[i] * multiplicity + j;
		dd->invpermZ[dd->permZ[i * multiplicity + j]] =
		    i * multiplicity + j;
	    }
	}
	for (i = 0; i < dd->sizeZ; i++) {
	    dd->univ[i]->index = dd->invpermZ[i];
	}
    } else {
	permutation = ALLOC(int,dd->sizeZ);
	if (permutation == NULL) {
	    dd->errorCode = CUDD_MEMORY_OUT;
	    return(0);
	}
	for (i = 0; i < dd->size; i++) {
	    for (j = 0; j < multiplicity; j++) {
		permutation[i * multiplicity + j] =
		    dd->invperm[i] * multiplicity + j;
	    }
	}
	for (i = dd->size * multiplicity; i < dd->sizeZ; i++) {
	    permutation[i] = i;
	}
	res = Cudd_zddShuffleHeap(dd, permutation);
	FREE(permutation);
	if (res == 0) return(0);
    }
    /* Copy and expand the variable group tree if it exists. */
    if (dd->treeZ != NULL) {
	Cudd_FreeZddTree(dd);
    }
    if (dd->tree != NULL) {
	dd->treeZ = Mtr_CopyTree(dd->tree, multiplicity);
	if (dd->treeZ == NULL) return(0);
    } else if (multiplicity > 1) {
	dd->treeZ = Mtr_InitGroupTree(0, dd->sizeZ);
	if (dd->treeZ == NULL) return(0);
	dd->treeZ->index = dd->invpermZ[0];
    }
    /* Create groups for the ZDD variables derived from the same BDD variable.
    */
    if (multiplicity > 1) {
	char *vmask, *lmask;

	vmask = ALLOC(char, dd->size);
	if (vmask == NULL) {
	    dd->errorCode = CUDD_MEMORY_OUT;
	    return(0);
	}
	lmask =  ALLOC(char, dd->size);
	if (lmask == NULL) {
	    dd->errorCode = CUDD_MEMORY_OUT;
	    return(0);
	}
	for (i = 0; i < dd->size; i++) {
	    vmask[i] = lmask[i] = 0;
	}
	res = addMultiplicityGroups(dd,dd->treeZ,multiplicity,vmask,lmask);
	FREE(vmask);
	FREE(lmask);
	if (res == 0) return(0);
    }
    return(1);

} /* end of Cudd_zddVarsFromBddVars */


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

  Synopsis    [Returns the ADD for constant c.]

  Description [Retrieves the ADD for constant c if it already
  exists, or creates a new ADD.  Returns a pointer to the
  ADD if successful; NULL otherwise.]

  SideEffects [None]

  SeeAlso     [Cudd_addNewVar Cudd_addIthVar]

******************************************************************************/
DdNode *
Cudd_addConst(
  DdManager * dd,
  CUDD_VALUE_TYPE  c)
{
    return(cuddUniqueConst(dd,c));

} /* end of Cudd_addConst */


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

  Synopsis    [Returns 1 if a DD node is not constant.]

  Description [Returns 1 if a DD node is not constant. This function is
  useful to test the results of Cudd_bddIteConstant, Cudd_addIteConstant,
  Cudd_addEvalConst. These results may be a special value signifying
  non-constant. In the other cases the macro Cudd_IsConstant can be used.]

  SideEffects [None]

  SeeAlso     [Cudd_IsConstant Cudd_bddIteConstant Cudd_addIteConstant
  Cudd_addEvalConst]

******************************************************************************/
int
Cudd_IsNonConstant(
  DdNode *f)
{
    return(f == DD_NON_CONSTANT || !Cudd_IsConstant(f));

} /* end of Cudd_IsNonConstant */


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

  Synopsis    [Enables automatic dynamic reordering of BDDs and ADDs.]

  Description [Enables automatic dynamic reordering of BDDs and
  ADDs. Parameter method is used to determine the method used for
  reordering. If CUDD_REORDER_SAME is passed, the method is
  unchanged.]

  SideEffects [None]

  SeeAlso     [Cudd_AutodynDisable Cudd_ReorderingStatus
  Cudd_AutodynEnableZdd]

******************************************************************************/
void
Cudd_AutodynEnable(
  DdManager * unique,
  Cudd_ReorderingType  method)
{
    unique->autoDyn = 1;
    if (method != CUDD_REORDER_SAME) {
	unique->autoMethod = method;
    }
#ifndef DD_NO_DEATH_ROW
    /* If reordering is enabled, using the death row causes too many
    ** invocations. Hence, we shrink the death row to just one entry.
    */
    cuddClearDeathRow(unique);
    unique->deathRowDepth = 1;
    unique->deadMask = unique->deathRowDepth - 1;
    if ((unsigned) unique->nextDead > unique->deadMask) {
	unique->nextDead = 0;
    }
    unique->deathRow = REALLOC(DdNodePtr, unique->deathRow,
	unique->deathRowDepth);
#endif
    return;

} /* end of Cudd_AutodynEnable */


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

  Synopsis    [Disables automatic dynamic reordering.]

  Description []

  SideEffects [None]

  SeeAlso     [Cudd_AutodynEnable Cudd_ReorderingStatus
  Cudd_AutodynDisableZdd]

******************************************************************************/
void
Cudd_AutodynDisable(
  DdManager * unique)
{
    unique->autoDyn = 0;
    return;

} /* end of Cudd_AutodynDisable */


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

  Synopsis    [Reports the status of automatic dynamic reordering of BDDs
  and ADDs.]

  Description [Reports the status of automatic dynamic reordering of
  BDDs and ADDs. Parameter method is set to the reordering method
  currently selected. Returns 1 if automatic reordering is enabled; 0
  otherwise.]

  SideEffects [Parameter method is set to the reordering method currently
  selected.]

  SeeAlso     [Cudd_AutodynEnable Cudd_AutodynDisable
  Cudd_ReorderingStatusZdd]

******************************************************************************/
int
Cudd_ReorderingStatus(
  DdManager * unique,
  Cudd_ReorderingType * method)
{
    *method = unique->autoMethod;
    return(unique->autoDyn);

} /* end of Cudd_ReorderingStatus */


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

  Synopsis    [Enables automatic dynamic reordering of ZDDs.]

  Description [Enables automatic dynamic reordering of ZDDs. Parameter
  method is used to determine the method used for reordering ZDDs. If
  CUDD_REORDER_SAME is passed, the method is unchanged.]

  SideEffects [None]

  SeeAlso     [Cudd_AutodynDisableZdd Cudd_ReorderingStatusZdd
  Cudd_AutodynEnable]

******************************************************************************/
void
Cudd_AutodynEnableZdd(
  DdManager * unique,
  Cudd_ReorderingType method)
{
    unique->autoDynZ = 1;
    if (method != CUDD_REORDER_SAME) {
	unique->autoMethodZ = method;
    }
    return;

} /* end of Cudd_AutodynEnableZdd */


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

  Synopsis    [Disables automatic dynamic reordering of ZDDs.]

  Description []

  SideEffects [None]

  SeeAlso     [Cudd_AutodynEnableZdd Cudd_ReorderingStatusZdd
  Cudd_AutodynDisable]

******************************************************************************/
void
Cudd_AutodynDisableZdd(
  DdManager * unique)
{
    unique->autoDynZ = 0;
    return;

} /* end of Cudd_AutodynDisableZdd */


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

  Synopsis    [Reports the status of automatic dynamic reordering of ZDDs.]

  Description [Reports the status of automatic dynamic reordering of
  ZDDs. Parameter method is set to the ZDD reordering method currently
  selected. Returns 1 if automatic reordering is enabled; 0
  otherwise.]

  SideEffects [Parameter method is set to the ZDD reordering method currently
  selected.]

  SeeAlso     [Cudd_AutodynEnableZdd Cudd_AutodynDisableZdd
  Cudd_ReorderingStatus]

******************************************************************************/
int
Cudd_ReorderingStatusZdd(
  DdManager * unique,
  Cudd_ReorderingType * method)
{
    *method = unique->autoMethodZ;
    return(unique->autoDynZ);

} /* end of Cudd_ReorderingStatusZdd */


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

  Synopsis    [Tells whether the realignment of ZDD order to BDD order is
  enabled.]

  Description [Returns 1 if the realignment of ZDD order to BDD order is
  enabled; 0 otherwise.]

  SideEffects [None]

  SeeAlso     [Cudd_zddRealignEnable Cudd_zddRealignDisable
  Cudd_bddRealignEnable Cudd_bddRealignDisable]

******************************************************************************/
int
Cudd_zddRealignmentEnabled(
  DdManager * unique)
{
    return(unique->realign);

} /* end of Cudd_zddRealignmentEnabled */


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

  Synopsis    [Enables realignment of ZDD order to BDD order.]

  Description [Enables realignment of the ZDD variable order to the
  BDD variable order after the BDDs and ADDs have been reordered.  The
  number of ZDD variables must be a multiple of the number of BDD
  variables for realignment to make sense. If this condition is not met,
  Cudd_ReduceHeap will return 0. Let <code>M</code> be the
  ratio of the two numbers. For the purpose of realignment, the ZDD
  variables from <code>M*i</code> to <code>(M+1)*i-1</code> are
  reagarded as corresponding to BDD variable <code>i</code>. Realignment
  is initially disabled.]

  SideEffects [None]

  SeeAlso     [Cudd_ReduceHeap Cudd_zddRealignDisable
  Cudd_zddRealignmentEnabled Cudd_bddRealignDisable
  Cudd_bddRealignmentEnabled]

******************************************************************************/
void
Cudd_zddRealignEnable(
  DdManager * unique)
{
    unique->realign = 1;
    return;

} /* end of Cudd_zddRealignEnable */


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

  Synopsis    [Disables realignment of ZDD order to BDD order.]

  Description []

  SideEffects [None]

  SeeAlso     [Cudd_zddRealignEnable Cudd_zddRealignmentEnabled
  Cudd_bddRealignEnable Cudd_bddRealignmentEnabled]

******************************************************************************/
void
Cudd_zddRealignDisable(
  DdManager * unique)
{
    unique->realign = 0;
    return;

} /* end of Cudd_zddRealignDisable */


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

  Synopsis    [Tells whether the realignment of BDD order to ZDD order is
  enabled.]

  Description [Returns 1 if the realignment of BDD order to ZDD order is
  enabled; 0 otherwise.]

  SideEffects [None]

  SeeAlso     [Cudd_bddRealignEnable Cudd_bddRealignDisable
  Cudd_zddRealignEnable Cudd_zddRealignDisable]

******************************************************************************/
int
Cudd_bddRealignmentEnabled(
  DdManager * unique)
{
    return(unique->realignZ);

} /* end of Cudd_bddRealignmentEnabled */


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

  Synopsis    [Enables realignment of BDD order to ZDD order.]

  Description [Enables realignment of the BDD variable order to the
  ZDD variable order after the ZDDs have been reordered.  The
  number of ZDD variables must be a multiple of the number of BDD
  variables for realignment to make sense. If this condition is not met,
  Cudd_zddReduceHeap will return 0. Let <code>M</code> be the
  ratio of the two numbers. For the purpose of realignment, the ZDD
  variables from <code>M*i</code> to <code>(M+1)*i-1</code> are
  reagarded as corresponding to BDD variable <code>i</code>. Realignment
  is initially disabled.]

  SideEffects [None]

  SeeAlso     [Cudd_zddReduceHeap Cudd_bddRealignDisable
  Cudd_bddRealignmentEnabled Cudd_zddRealignDisable
  Cudd_zddRealignmentEnabled]

******************************************************************************/
void
Cudd_bddRealignEnable(
  DdManager * unique)
{
    unique->realignZ = 1;
    return;

} /* end of Cudd_bddRealignEnable */


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

  Synopsis    [Disables realignment of ZDD order to BDD order.]

  Description []

  SideEffects [None]

  SeeAlso     [Cudd_bddRealignEnable Cudd_bddRealignmentEnabled
  Cudd_zddRealignEnable Cudd_zddRealignmentEnabled]

******************************************************************************/
void
Cudd_bddRealignDisable(
  DdManager * unique)
{
    unique->realignZ = 0;
    return;

} /* end of Cudd_bddRealignDisable */


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

  Synopsis    [Returns the one constant of the manager.]

  Description [Returns the one constant of the manager. The one
  constant is common to ADDs and BDDs.]

  SideEffects [None]

  SeeAlso [Cudd_ReadZero Cudd_ReadLogicZero Cudd_ReadZddOne]