cuddutil.c

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

} /* end of Cudd_EstimateCofactorSimple */


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

  Synopsis    [Counts the number of nodes in an array of DDs.]

  Description [Counts the number of nodes in an array of DDs. Shared
  nodes are counted only once.  Returns the total number of nodes.]

  SideEffects [None]

  SeeAlso     [Cudd_DagSize]

******************************************************************************/
int
Cudd_SharingSize(
  DdNode ** nodeArray,
  int  n)
{
    int	i,j;	

    i = 0;
    for (j = 0; j < n; j++) {
	i += ddDagInt(Cudd_Regular(nodeArray[j]));
    }
    for (j = 0; j < n; j++) {
	ddClearFlag(Cudd_Regular(nodeArray[j]));
    }
    return(i);

} /* end of Cudd_SharingSize */


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

  Synopsis    [Counts the number of minterms of a DD.]

  Description [Counts the number of minterms of a DD. The function is
  assumed to depend on nvars variables. The minterm count is
  represented as a double, to allow for a larger number of variables.
  Returns the number of minterms of the function rooted at node if
  successful; (double) CUDD_OUT_OF_MEM otherwise.]

  SideEffects [None]

  SeeAlso     [Cudd_PrintDebug Cudd_CountPath]

******************************************************************************/
double
Cudd_CountMinterm(
  DdManager * manager,
  DdNode * node,
  int  nvars)
{
    double	max;
    DdHashTable	*table;
    double	res;
    CUDD_VALUE_TYPE epsilon;

    background = manager->background;
    zero = Cudd_Not(manager->one);
    
    max = pow(2.0,(double)nvars);
    table = cuddHashTableInit(manager,1,2);
    if (table == NULL) {
	return((double)CUDD_OUT_OF_MEM);
    }
    epsilon = Cudd_ReadEpsilon(manager);
    Cudd_SetEpsilon(manager,(CUDD_VALUE_TYPE)0.0);
    res = ddCountMintermAux(node,max,table);
    cuddHashTableQuit(table);
    Cudd_SetEpsilon(manager,epsilon);

    return(res);

} /* end of Cudd_CountMinterm */


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

  Synopsis    [Counts the number of paths of a DD.]

  Description [Counts the number of paths of a DD.  Paths to all
  terminal nodes are counted. The path count is represented as a
  double, to allow for a larger number of variables.  Returns the
  number of paths of the function rooted at node if successful;
  (double) CUDD_OUT_OF_MEM otherwise.]

  SideEffects [None]

  SeeAlso     [Cudd_CountMinterm]

******************************************************************************/
double
Cudd_CountPath(
  DdNode * node)
{

    st_table	*table;
    double	i;	

    table = st_init_table(st_ptrcmp,st_ptrhash);
    if (table == NULL) {
	return((double)CUDD_OUT_OF_MEM);
    }
    i = ddCountPathAux(Cudd_Regular(node),table);
    st_foreach(table, cuddStCountfree, NULL);
    st_free_table(table);
    return(i);

} /* end of Cudd_CountPath */


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

  Synopsis    [Counts the number of minterms of a DD with extended precision.]

  Description [Counts the number of minterms of a DD with extended precision.
  The function is assumed to depend on nvars variables. The minterm count is
  represented as an EpDouble, to allow any number of variables.
  Returns 0 if successful; CUDD_OUT_OF_MEM otherwise.]

  SideEffects [None]

  SeeAlso     [Cudd_PrintDebug Cudd_CountPath]

******************************************************************************/
int
Cudd_EpdCountMinterm(
  DdManager * manager,
  DdNode * node,
  int  nvars,
  EpDouble * epd)
{
    EpDouble	max, tmp;
    st_table	*table;
    int		status;

    background = manager->background;
    zero = Cudd_Not(manager->one);
    
    EpdPow2(nvars, &max);
    table = st_init_table(EpdCmp, st_ptrhash);
    if (table == NULL) {
	EpdMakeZero(epd, 0);
	return(CUDD_OUT_OF_MEM);
    }
    status = ddEpdCountMintermAux(Cudd_Regular(node),&max,epd,table);
    st_foreach(table, ddEpdFree, NULL);
    st_free_table(table);
    if (status == CUDD_OUT_OF_MEM) {
	EpdMakeZero(epd, 0);
	return(CUDD_OUT_OF_MEM);
    }
    if (Cudd_IsComplement(node)) {
    	EpdSubtract3(&max, epd, &tmp);
    	EpdCopy(&tmp, epd);
    }
    return(0);

} /* end of Cudd_EpdCountMinterm */


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

  Synopsis    [Counts the number of paths to a non-zero terminal of a DD.]

  Description [Counts the number of paths to a non-zero terminal of a
  DD.  The path count is
  represented as a double, to allow for a larger number of variables.
  Returns the number of paths of the function rooted at node.]

  SideEffects [None]

  SeeAlso     [Cudd_CountMinterm Cudd_CountPath]

******************************************************************************/
double
Cudd_CountPathsToNonZero(
  DdNode * node)
{

    st_table	*table;
    double	i;	

    table = st_init_table(st_ptrcmp,st_ptrhash);
    if (table == NULL) {
	return((double)CUDD_OUT_OF_MEM);
    }
    i = ddCountPathsToNonZero(node,table);
    st_foreach(table, cuddStCountfree, NULL);
    st_free_table(table);
    return(i);

} /* end of Cudd_CountPathsToNonZero */


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

  Synopsis    [Finds the variables on which a DD depends.]

  Description [Finds the variables on which a DD depends.
  Returns a BDD consisting of the product of the variables if
  successful; NULL otherwise.]

  SideEffects [None]

  SeeAlso     [Cudd_VectorSupport Cudd_ClassifySupport]

******************************************************************************/
DdNode *
Cudd_Support(
  DdManager * dd /* manager */,
  DdNode * f /* DD whose support is sought */)
{
    int	*support;
    DdNode *res, *tmp, *var;
    int	i,j;
    int size;

    /* Allocate and initialize support array for ddSupportStep. */
    size = ddMax(dd->size, dd->sizeZ);
    support = ALLOC(int,size);
    if (support == NULL) {
	dd->errorCode = CUDD_MEMORY_OUT;
	return(NULL);
    }
    for (i = 0; i < size; i++) {
	support[i] = 0;
    }

    /* Compute support and clean up markers. */
    ddSupportStep(Cudd_Regular(f),support);
    ddClearFlag(Cudd_Regular(f));

    /* Transform support from array to cube. */
    do {
	dd->reordered = 0;
	res = DD_ONE(dd);
	cuddRef(res);
	for (j = size - 1; j >= 0; j--) { /* for each level bottom-up */
	    i = (j >= dd->size) ? j : dd->invperm[j];
	    if (support[i] == 1) {
		var = cuddUniqueInter(dd,i,dd->one,Cudd_Not(dd->one));
		cuddRef(var);
		tmp = cuddBddAndRecur(dd,res,var);
		if (tmp == NULL) {
		    Cudd_RecursiveDeref(dd,res);
		    Cudd_RecursiveDeref(dd,var);
		    res = NULL;
		    break;
		}
		cuddRef(tmp);
		Cudd_RecursiveDeref(dd,res);
		Cudd_RecursiveDeref(dd,var);
		res = tmp;
	    }
	}
    } while (dd->reordered == 1);

    FREE(support);
    if (res != NULL) cuddDeref(res);
    return(res);

} /* end of Cudd_Support */


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

  Synopsis    [Finds the variables on which a DD depends.]

  Description [Finds the variables on which a DD depends.
  Returns an index array of the variables if successful; NULL otherwise.]

  SideEffects [None]

  SeeAlso     [Cudd_Support Cudd_VectorSupport Cudd_ClassifySupport]

******************************************************************************/
int *
Cudd_SupportIndex(
  DdManager * dd /* manager */,
  DdNode * f /* DD whose support is sought */)
{
    int	*support;
    int	i;
    int size;

    /* Allocate and initialize support array for ddSupportStep. */
    size = ddMax(dd->size, dd->sizeZ);
    support = ALLOC(int,size);
    if (support == NULL) {
	dd->errorCode = CUDD_MEMORY_OUT;
	return(NULL);
    }
    for (i = 0; i < size; i++) {
	support[i] = 0;
    }

    /* Compute support and clean up markers. */
    ddSupportStep(Cudd_Regular(f),support);
    ddClearFlag(Cudd_Regular(f));

    return(support);

} /* end of Cudd_SupportIndex */


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

  Synopsis    [Counts the variables on which a DD depends.]

  Description [Counts the variables on which a DD depends.
  Returns the number of the variables if successful; CUDD_OUT_OF_MEM
  otherwise.]

  SideEffects [None]

  SeeAlso     [Cudd_Support]

******************************************************************************/
int
Cudd_SupportSize(
  DdManager * dd /* manager */,
  DdNode * f /* DD whose support size is sought */)
{
    int	*support;
    int	i;
    int size;
    int count;

    /* Allocate and initialize support array for ddSupportStep. */
    size = ddMax(dd->size, dd->sizeZ);
    support = ALLOC(int,size);
    if (support == NULL) {
	dd->errorCode = CUDD_MEMORY_OUT;
	return(CUDD_OUT_OF_MEM);
    }
    for (i = 0; i < size; i++) {
	support[i] = 0;
    }

    /* Compute support and clean up markers. */
    ddSupportStep(Cudd_Regular(f),support);
    ddClearFlag(Cudd_Regular(f));

    /* Count support variables. */
    count = 0;
    for (i = 0; i < size; i++) {
	if (support[i] == 1) count++;
    }

    FREE(support);
    return(count);

} /* end of Cudd_SupportSize */


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

  Synopsis    [Finds the variables on which a set of DDs depends.]

  Description [Finds the variables on which a set of DDs depends.
  The set must contain either BDDs and ADDs, or ZDDs.
  Returns a BDD consisting of the product of the variables if
  successful; NULL otherwise.]

  SideEffects [None]

  SeeAlso     [Cudd_Support Cudd_ClassifySupport]

******************************************************************************/
DdNode *
Cudd_VectorSupport(
  DdManager * dd /* manager */,
  DdNode ** F /* array of DDs whose support is sought */,
  int  n /* size of the array */)
{
    int	*support;
    DdNode *res, *tmp, *var;
    int	i,j;
    int size;

    /* Allocate and initialize support array for ddSupportStep. */
    size = ddMax(dd->size, dd->sizeZ);
    support = ALLOC(int,size);
    if (support == NULL) {
	dd->errorCode = CUDD_MEMORY_OUT;
	return(NULL);
    }
    for (i = 0; i < size; i++) {
	support[i] = 0;
    }

    /* Compute support and clean up markers. */
    for (i = 0; i < n; i++) {
	ddSupportStep(Cudd_Regular(F[i]),support);
    }
    for (i = 0; i < n; i++) {
	ddClearFlag(Cudd_Regular(F[i]));
    }

    /* Transform support from array to cube. */
    res = DD_ONE(dd);
    cuddRef(res);
    for (j = size - 1; j >= 0; j--) { /* for each level bottom-up */
	i = (j >= dd->size) ? j : dd->invperm[j];
	if (support[i] == 1) {
	    var = cuddUniqueInter(dd,i,dd->one,Cudd_Not(dd->one));
	    cuddRef(var);
	    tmp = Cudd_bddAnd(dd,res,var);
	    if (tmp == NULL) {
		Cudd_RecursiveDeref(dd,res);
		Cudd_RecursiveDeref(dd,var);
		FREE(support);
		return(NULL);
	    }
	    cuddRef(tmp);
	    Cudd_RecursiveDeref(dd,res);
	    Cudd_RecursiveDeref(dd,var);
	    res = tmp;
	}
    }

    FREE(support);
    cuddDeref(res);
    return(res);

} /* end of Cudd_VectorSupport */


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

  Synopsis    [Finds the variables on which a set of DDs depends.]

  Description [Finds the variables on which a set of DDs depends.
  The set must contain either BDDs and ADDs, or ZDDs.
  Returns an index array of the variables if successful; NULL otherwise.]

  SideEffects [None]

  SeeAlso     [Cudd_SupportIndex Cudd_VectorSupport Cudd_ClassifySupport]

******************************************************************************/
int *
Cudd_VectorSupportIndex(
  DdManager * dd /* manager */,
  DdNode ** F /* array of DDs whose support is sought */,
  int  n /* size of the array */)
{
    int	*support;
    int	i;
    int size;

    /* Allocate and initialize support array for ddSupportStep. */
    size = ddMax(dd->size, dd->sizeZ);
    support = ALLOC(int,size);
    if (support == NULL) {
	dd->errorCode = CUDD_MEMORY_OUT;
	return(NULL);
    }
    for (i = 0; i < size; i++) {
	support[i] = 0;
    }

    /* Compute support and clean up markers. */
    for (i = 0; i < n; i++) {
	ddSupportStep(Cudd_Regular(F[i]),support);
    }
    for (i = 0; i < n; i++) {
	ddClearFlag(Cudd_Regular(F[i]));
    }

    return(support);

} /* end of Cudd_VectorSupportIndex */


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

  Synopsis    [Counts the variables on which a set of DDs depends.]

  Description [Counts the variables on which a set of DDs depends.
  The set must contain either BDDs and ADDs, or ZDDs.
  Returns the number of the variables if successful; CUDD_OUT_OF_MEM