cuddutil.c

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

  Synopsis    [Computes the cube of an array of BDD variables.]

  Description [Computes the cube of an array of BDD variables. If
  non-null, the phase argument indicates which literal of each
  variable should appear in the cube. If phase\[i\] is nonzero, then the
  positive literal is used. If phase is NULL, the cube is positive unate.
  Returns a pointer to the result if successful; NULL otherwise.]

  SideEffects [None]

  SeeAlso     [Cudd_addComputeCube Cudd_IndicesToCube Cudd_CubeArrayToBdd]

******************************************************************************/
DdNode *
Cudd_bddComputeCube(
  DdManager * dd,
  DdNode ** vars,
  int * phase,
  int  n)
{
    DdNode	*cube;
    DdNode 	*fn;
    int         i;

    cube = DD_ONE(dd);
    cuddRef(cube);

    for (i = n - 1; i >= 0; i--) {
	if (phase == NULL || phase[i] != 0) {
	    fn = Cudd_bddAnd(dd,vars[i],cube);
	} else {
	    fn = Cudd_bddAnd(dd,Cudd_Not(vars[i]),cube);
	}
	if (fn == NULL) {
	    Cudd_RecursiveDeref(dd,cube);
	    return(NULL);
	}
	cuddRef(fn);
	Cudd_RecursiveDeref(dd,cube);
	cube = fn;
    }
    cuddDeref(cube);

    return(cube);

}  /* end of Cudd_bddComputeCube */


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

  Synopsis    [Computes the cube of an array of ADD variables.]

  Description [Computes the cube of an array of ADD variables.  If
  non-null, the phase argument indicates which literal of each
  variable should appear in the cube. If phase\[i\] is nonzero, then the
  positive literal is used. If phase is NULL, the cube is positive unate.
  Returns a pointer to the result if successful; NULL otherwise.]

  SideEffects [none]

  SeeAlso     [Cudd_bddComputeCube]

******************************************************************************/
DdNode *
Cudd_addComputeCube(
  DdManager * dd,
  DdNode ** vars,
  int * phase,
  int  n)
{
    DdNode	*cube, *zero;
    DdNode 	*fn;
    int         i;

    cube = DD_ONE(dd);
    cuddRef(cube);
    zero = DD_ZERO(dd);

    for (i = n - 1; i >= 0; i--) {
	if (phase == NULL || phase[i] != 0) {
	    fn = Cudd_addIte(dd,vars[i],cube,zero);
	} else {
	    fn = Cudd_addIte(dd,vars[i],zero,cube);
	}
	if (fn == NULL) {
	    Cudd_RecursiveDeref(dd,cube);
	    return(NULL);
	}
	cuddRef(fn);
	Cudd_RecursiveDeref(dd,cube);
	cube = fn;
    }
    cuddDeref(cube);

    return(cube);

} /* end of Cudd_addComputeCube */


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

  Synopsis    [Builds the BDD of a cube from a positional array.]

  Description [Builds a cube from a positional array.  The array must
  have one integer entry for each BDD variable.  If the i-th entry is
  1, the variable of index i appears in true form in the cube; If the
  i-th entry is 0, the variable of index i appears complemented in the
  cube; otherwise the variable does not appear in the cube.  Returns a
  pointer to the BDD for the cube if successful; NULL otherwise.]

  SideEffects [None]

  SeeAlso     [Cudd_bddComputeCube Cudd_IndicesToCube Cudd_BddToCubeArray]

******************************************************************************/
DdNode *
Cudd_CubeArrayToBdd(
  DdManager *dd,
  int *array)
{
    DdNode *cube, *var, *tmp;
    int i;
    int size = Cudd_ReadSize(dd);

    cube = DD_ONE(dd);
    cuddRef(cube);
    for (i = size - 1; i >= 0; i--) {
	if ((array[i] & ~1) == 0) {
	    var = Cudd_bddIthVar(dd,i);
	    tmp = Cudd_bddAnd(dd,cube,Cudd_NotCond(var,array[i]==0));
	    if (tmp == NULL) {
		Cudd_RecursiveDeref(dd,cube);
		return(NULL);
	    }
	    cuddRef(tmp);
	    Cudd_RecursiveDeref(dd,cube);
	    cube = tmp;
	}
    }
    cuddDeref(cube);
    return(cube);

} /* end of Cudd_CubeArrayToBdd */


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

  Synopsis    [Builds a positional array from the BDD of a cube.]

  Description [Builds a positional array from the BDD of a cube.
  Array must have one entry for each BDD variable.  The positional
  array has 1 in i-th position if the variable of index i appears in
  true form in the cube; it has 0 in i-th position if the variable of
  index i appears in complemented form in the cube; finally, it has 2
  in i-th position if the variable of index i does not appear in the
  cube.  Returns 1 if successful (the BDD is indeed a cube); 0
  otherwise.]

  SideEffects [The result is in the array passed by reference.]

  SeeAlso     [Cudd_CubeArrayToBdd]

******************************************************************************/
int
Cudd_BddToCubeArray(
  DdManager *dd,
  DdNode *cube,
  int *array)
{
    DdNode *scan, *t, *e;
    int i;
    int size = Cudd_ReadSize(dd);
    DdNode *zero = Cudd_Not(DD_ONE(dd));

    for (i = size-1; i >= 0; i--) {
	array[i] = 2;
    }
    scan = cube;
    while (!Cudd_IsConstant(scan)) {
	int index = Cudd_Regular(scan)->index;
	cuddGetBranches(scan,&t,&e);
	if (t == zero) {
	    array[index] = 0;
	    scan = e;
	} else if (e == zero) {
	    array[index] = 1;
	    scan = t;
	} else {
	    return(0);	/* cube is not a cube */
	}
    }
    if (scan == zero) {
	return(0);
    } else {
	return(1);
    }

} /* end of Cudd_BddToCubeArray */


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

  Synopsis    [Finds the first node of a decision diagram.]

  Description [Defines an iterator on the nodes of a decision diagram
  and finds its first node. Returns a generator that contains the
  information necessary to continue the enumeration if successful; NULL
  otherwise.]

  SideEffects [The first node is returned as a side effect.]

  SeeAlso     [Cudd_ForeachNode Cudd_NextNode Cudd_GenFree Cudd_IsGenEmpty
  Cudd_FirstCube]

******************************************************************************/
DdGen *
Cudd_FirstNode(
  DdManager * dd,
  DdNode * f,
  DdNode ** node)
{
    DdGen *gen;
    int retval;

    /* Sanity Check. */
    if (dd == NULL || f == NULL) return(NULL);

    /* Allocate generator an initialize it. */
    gen = ALLOC(DdGen,1);
    if (gen == NULL) {
	dd->errorCode = CUDD_MEMORY_OUT;
	return(NULL);
    }

    gen->manager = dd;
    gen->type = CUDD_GEN_NODES;
    gen->status = CUDD_GEN_EMPTY;
    gen->gen.nodes.visited = NULL;
    gen->gen.nodes.stGen = NULL;
    gen->stack.sp = 0;
    gen->stack.stack = NULL;
    gen->node = NULL;

    gen->gen.nodes.visited = st_init_table(st_ptrcmp,st_ptrhash);
    if (gen->gen.nodes.visited == NULL) {
	FREE(gen);
	return(NULL);
    }

    /* Collect all the nodes in a st table for later perusal. */
    retval = cuddCollectNodes(Cudd_Regular(f),gen->gen.nodes.visited);
    if (retval == 0) {
	st_free_table(gen->gen.nodes.visited);
	FREE(gen);
	return(NULL);
    }

    /* Initialize the st table generator. */
    gen->gen.nodes.stGen = st_init_gen(gen->gen.nodes.visited);
    if (gen->gen.nodes.stGen == NULL) {
	st_free_table(gen->gen.nodes.visited);
	FREE(gen);
	return(NULL);
    }

    /* Find the first node. */
    retval = st_gen(gen->gen.nodes.stGen, (char **) &(gen->node), NULL);
    if (retval != 0) {
	gen->status = CUDD_GEN_NONEMPTY;
	*node = gen->node;
    }

    return(gen);

} /* end of Cudd_FirstNode */


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

  Synopsis    [Finds the next node of a decision diagram.]

  Description [Finds the node of a decision diagram, using generator
  gen. Returns 0 if the enumeration is completed; 1 otherwise.]

  SideEffects [The next node is returned as a side effect.]

  SeeAlso     [Cudd_ForeachNode Cudd_FirstNode Cudd_GenFree Cudd_IsGenEmpty
  Cudd_NextCube]

******************************************************************************/
int
Cudd_NextNode(
  DdGen * gen,
  DdNode ** node)
{
    int retval;

    /* Find the next node. */
    retval = st_gen(gen->gen.nodes.stGen, (char **) &(gen->node), NULL);
    if (retval == 0) {
	gen->status = CUDD_GEN_EMPTY;
    } else {
	*node = gen->node;
    }

    return(retval);

} /* end of Cudd_NextNode */


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

  Synopsis    [Frees a CUDD generator.]

  Description [Frees a CUDD generator. Always returns 0, so that it can
  be used in mis-like foreach constructs.]

  SideEffects [None]

  SeeAlso     [Cudd_ForeachCube Cudd_ForeachNode Cudd_FirstCube Cudd_NextCube
  Cudd_FirstNode Cudd_NextNode Cudd_IsGenEmpty]

******************************************************************************/
int
Cudd_GenFree(
  DdGen * gen)
{

    if (gen == NULL) return(0);
    switch (gen->type) {
    case CUDD_GEN_CUBES:
    case CUDD_GEN_ZDD_PATHS:
	FREE(gen->gen.cubes.cube);
	FREE(gen->stack.stack);
	break;
    case CUDD_GEN_NODES:
	st_free_gen(gen->gen.nodes.stGen);
	st_free_table(gen->gen.nodes.visited);
	break;
    default:
	return(0);
    }
    FREE(gen);
    return(0);

} /* end of Cudd_GenFree */


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

  Synopsis    [Queries the status of a generator.]

  Description [Queries the status of a generator. Returns 1 if the
  generator is empty or NULL; 0 otherswise.]

  SideEffects [None]

  SeeAlso     [Cudd_ForeachCube Cudd_ForeachNode Cudd_FirstCube Cudd_NextCube
  Cudd_FirstNode Cudd_NextNode Cudd_GenFree]

******************************************************************************/
int
Cudd_IsGenEmpty(
  DdGen * gen)
{
    if (gen == NULL) return(1);
    return(gen->status == CUDD_GEN_EMPTY);

} /* end of Cudd_IsGenEmpty */


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

  Synopsis    [Builds a cube of BDD variables from an array of indices.]

  Description [Builds a cube of BDD variables from an array of indices.
  Returns a pointer to the result if successful; NULL otherwise.]

  SideEffects [None]

  SeeAlso     [Cudd_bddComputeCube Cudd_CubeArrayToBdd]

******************************************************************************/
DdNode *
Cudd_IndicesToCube(
  DdManager * dd,
  int * array,
  int  n)
{
    DdNode *cube, *tmp;
    int i;

    cube = DD_ONE(dd);
    cuddRef(cube);
    for (i = n - 1; i >= 0; i--) {
	tmp = Cudd_bddAnd(dd,Cudd_bddIthVar(dd,array[i]),cube);
	if (tmp == NULL) {
	    Cudd_RecursiveDeref(dd,cube);
	    return(NULL);
	}
	cuddRef(tmp);
	Cudd_RecursiveDeref(dd,cube);
	cube = tmp;
    }

    cuddDeref(cube);
    return(cube);

} /* end of Cudd_IndicesToCube */


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

  Synopsis    [Prints the package version number.]

  Description []

  SideEffects [None]

  SeeAlso     []

******************************************************************************/
void
Cudd_PrintVersion(
  FILE * fp)
{
    (void) fprintf(fp, "%s\n", CUDD_VERSION);

} /* end of Cudd_PrintVersion */


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

  Synopsis    [Computes the average distance between adjacent nodes.]

  Description [Computes the average distance between adjacent nodes in
  the manager. Adjacent nodes are node pairs such that the second node
  is the then child, else child, or next node in the collision list.]

  SideEffects [None]

  SeeAlso     []

******************************************************************************/
double
Cudd_AverageDistance(
  DdManager * dd)
{
    double tetotal, nexttotal;
    double tesubtotal, nextsubtotal;
    double temeasured, nextmeasured;
    int i, j;
    int slots, nvars;
    long diff;
    DdNode *scan;
    DdNodePtr *nodelist;
    DdNode *sentinel = &(dd->sentinel);

    nvars = dd->size;
    if (nvars == 0) return(0.0);

    /* Initialize totals. */
    tetotal = 0.0;
    nexttotal = 0.0;
    temeasured = 0.0;
    nextmeasured = 0.0;

    /* Scan the variable subtables. */
    for (i = 0; i < nvars; i++) {
	nodelist = dd->subtables[i].nodelist;
	tesubtotal = 0.0;
	nextsubtotal = 0.0;
	slots = dd->subtables[i].slots;
	for (j = 0; j < slots; j++) {
	    scan = nodelist[j];
	    while (scan != sentinel) {
		diff = (long) scan - (long) cuddT(scan);
		tesubtotal += (double) ddAbs(diff);
		diff = (long) scan - (long) Cudd_Regular(cuddE(scan));
		tesubtotal += (double) ddAbs(diff);
		temeasured += 2.0;
		if (scan->next != NULL) {
		    diff = (long) scan - (long) scan->n