cudddecomp.c

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

    result = Cudd_bddIterConjDecomp(dd,Cudd_Not(f),disjuncts);
    for (i = 0; i < result; i++) {
	(*disjuncts)[i] = Cudd_Not((*disjuncts)[i]);
    }
    return(result);

} /* end of Cudd_bddIterDisjDecomp */


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

  Synopsis    [Performs two-way conjunctive decomposition of a BDD.]

  Description [Performs two-way conjunctive decomposition of a
  BDD. This procedure owes its name to the fact tht it generalizes the
  decomposition based on the cofactors with respect to one
  variable. Returns the number of conjuncts produced, that is, 2 if
  successful; 1 if no meaningful decomposition was found; 0
  otherwise. The conjuncts produced by this procedure tend to be
  balanced.]

  SideEffects [The two factors are returned in an array as side effects.
  The array is allocated by this function. It is the caller's responsibility
  to free it. On successful completion, the conjuncts are already
  referenced. If the function returns 0, the array for the conjuncts is
  not allocated. If the function returns 1, the only factor equals the
  function to be decomposed.]

  SeeAlso     [Cudd_bddGenDisjDecomp Cudd_bddApproxConjDecomp
  Cudd_bddIterConjDecomp Cudd_bddVarConjDecomp]

******************************************************************************/
int
Cudd_bddGenConjDecomp(
  DdManager * dd /* manager */,
  DdNode * f /* function to be decomposed */,
  DdNode *** conjuncts /* address of the array of conjuncts */)
{
    int result;
    DdNode *glocal, *hlocal;

    one = DD_ONE(dd);
    zero = Cudd_Not(one);
    
    do {
	dd->reordered = 0;
	result = cuddConjunctsAux(dd, f, &glocal, &hlocal);
    } while (dd->reordered == 1);

    if (result == 0) {
	return(0);
    }

    if (glocal != one) {
	if (hlocal != one) {
	    *conjuncts = ALLOC(DdNode *,2);
	    if (*conjuncts == NULL) {
		Cudd_RecursiveDeref(dd,glocal);
		Cudd_RecursiveDeref(dd,hlocal);
		dd->errorCode = CUDD_MEMORY_OUT;
		return(0);
	    }
	    (*conjuncts)[0] = glocal;
	    (*conjuncts)[1] = hlocal;
	    return(2);
	} else {
	    Cudd_RecursiveDeref(dd,hlocal);
	    *conjuncts = ALLOC(DdNode *,1);
	    if (*conjuncts == NULL) {
		Cudd_RecursiveDeref(dd,glocal);
		dd->errorCode = CUDD_MEMORY_OUT;
		return(0);
	    }
	    (*conjuncts)[0] = glocal;
	    return(1);
	}
    } else {
	Cudd_RecursiveDeref(dd,glocal);
	*conjuncts = ALLOC(DdNode *,1);
	if (*conjuncts == NULL) {
	    Cudd_RecursiveDeref(dd,hlocal);
	    dd->errorCode = CUDD_MEMORY_OUT;
	    return(0);
	}
	(*conjuncts)[0] = hlocal;
	return(1);
    }

} /* end of Cudd_bddGenConjDecomp */


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

  Synopsis    [Performs two-way disjunctive decomposition of a BDD.]

  Description [Performs two-way disjunctive decomposition of a BDD.
  Returns the number of disjuncts produced, that is, 2 if successful;
  1 if no meaningful decomposition was found; 0 otherwise. The
  disjuncts produced by this procedure tend to be balanced.]

  SideEffects [The two disjuncts are returned in an array as side effects.
  The array is allocated by this function. It is the caller's responsibility
  to free it. On successful completion, the disjuncts are already
  referenced. If the function returns 0, the array for the disjuncts is
  not allocated. If the function returns 1, the only factor equals the
  function to be decomposed.]

  SeeAlso     [Cudd_bddGenConjDecomp Cudd_bddApproxDisjDecomp
  Cudd_bddIterDisjDecomp Cudd_bddVarDisjDecomp]

******************************************************************************/
int
Cudd_bddGenDisjDecomp(
  DdManager * dd /* manager */,
  DdNode * f /* function to be decomposed */,
  DdNode *** disjuncts /* address of the array of the disjuncts */)
{
    int result, i;

    result = Cudd_bddGenConjDecomp(dd,Cudd_Not(f),disjuncts);
    for (i = 0; i < result; i++) {
	(*disjuncts)[i] = Cudd_Not((*disjuncts)[i]);
    }
    return(result);

} /* end of Cudd_bddGenDisjDecomp */


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

  Synopsis    [Performs two-way conjunctive decomposition of a BDD.]

  Description [Conjunctively decomposes one BDD according to a
  variable.  If <code>f</code> is the function of the BDD and
  <code>x</code> is the variable, the decomposition is
  <code>(f+x)(f+x')</code>.  The variable is chosen so as to balance
  the sizes of the two conjuncts and to keep them small.  Returns the
  number of conjuncts produced, that is, 2 if successful; 1 if no
  meaningful decomposition was found; 0 otherwise.]

  SideEffects [The two factors are returned in an array as side effects.
  The array is allocated by this function. It is the caller's responsibility
  to free it. On successful completion, the conjuncts are already
  referenced. If the function returns 0, the array for the conjuncts is
  not allocated. If the function returns 1, the only factor equals the
  function to be decomposed.]

  SeeAlso     [Cudd_bddVarDisjDecomp Cudd_bddGenConjDecomp
  Cudd_bddApproxConjDecomp Cudd_bddIterConjDecomp]

*****************************************************************************/
int
Cudd_bddVarConjDecomp(
  DdManager * dd /* manager */,
  DdNode * f /* function to be decomposed */,
  DdNode *** conjuncts /* address of the array of conjuncts */)
{
    int best;
    int min;
    DdNode *support, *scan, *var, *glocal, *hlocal;

    /* Find best cofactoring variable. */
    support = Cudd_Support(dd,f);
    if (support == NULL) return(0);
    if (Cudd_IsConstant(support)) {
	*conjuncts = ALLOC(DdNode *,1);
	if (*conjuncts == NULL) {
	    dd->errorCode = CUDD_MEMORY_OUT;
	    return(0);
	}
	(*conjuncts)[0] = f;
	cuddRef((*conjuncts)[0]);
	return(1);
    }
    cuddRef(support);
    min = 1000000000;
    best = -1;
    scan = support;
    while (!Cudd_IsConstant(scan)) {
	int i = scan->index;
	int est1 = Cudd_EstimateCofactor(dd,f,i,1);
	int est0 = Cudd_EstimateCofactor(dd,f,i,0);
	/* Minimize the size of the larger of the two cofactors. */
	int est = (est1 > est0) ? est1 : est0;
	if (est < min) {
	    min = est;
	    best = i;
	}
	scan = cuddT(scan);
    }
#ifdef DD_DEBUG
    assert(best >= 0 && best < dd->size);
#endif
    Cudd_RecursiveDeref(dd,support);

    var = Cudd_bddIthVar(dd,best);
    glocal = Cudd_bddOr(dd,f,var);
    if (glocal == NULL) {
	return(0);
    }
    cuddRef(glocal);
    hlocal = Cudd_bddOr(dd,f,Cudd_Not(var));
    if (hlocal == NULL) {
	Cudd_RecursiveDeref(dd,glocal);
	return(0);
    }
    cuddRef(hlocal);

    if (glocal != DD_ONE(dd)) {
	if (hlocal != DD_ONE(dd)) {
	    *conjuncts = ALLOC(DdNode *,2);
	    if (*conjuncts == NULL) {
		Cudd_RecursiveDeref(dd,glocal);
		Cudd_RecursiveDeref(dd,hlocal);
		dd->errorCode = CUDD_MEMORY_OUT;
		return(0);
	    }
	    (*conjuncts)[0] = glocal;
	    (*conjuncts)[1] = hlocal;
	    return(2);
	} else {
	    Cudd_RecursiveDeref(dd,hlocal);
	    *conjuncts = ALLOC(DdNode *,1);
	    if (*conjuncts == NULL) {
		Cudd_RecursiveDeref(dd,glocal);
		dd->errorCode = CUDD_MEMORY_OUT;
		return(0);
	    }
	    (*conjuncts)[0] = glocal;
	    return(1);
	}
    } else {
	Cudd_RecursiveDeref(dd,glocal);
	*conjuncts = ALLOC(DdNode *,1);
	if (*conjuncts == NULL) {
	    Cudd_RecursiveDeref(dd,hlocal);
	    dd->errorCode = CUDD_MEMORY_OUT;
	    return(0);
	}
	(*conjuncts)[0] = hlocal;
	return(1);
    }

} /* end of Cudd_bddVarConjDecomp */


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

  Synopsis    [Performs two-way disjunctive decomposition of a BDD.]

  Description [Performs two-way disjunctive decomposition of a BDD
  according to a variable. If <code>f</code> is the function of the
  BDD and <code>x</code> is the variable, the decomposition is
  <code>f*x + f*x'</code>.  The variable is chosen so as to balance
  the sizes of the two disjuncts and to keep them small.  Returns the
  number of disjuncts produced, that is, 2 if successful; 1 if no
  meaningful decomposition was found; 0 otherwise.]

  SideEffects [The two disjuncts are returned in an array as side effects.
  The array is allocated by this function. It is the caller's responsibility
  to free it. On successful completion, the disjuncts are already
  referenced. If the function returns 0, the array for the disjuncts is
  not allocated. If the function returns 1, the only factor equals the
  function to be decomposed.]

  SeeAlso     [Cudd_bddVarConjDecomp Cudd_bddApproxDisjDecomp
  Cudd_bddIterDisjDecomp Cudd_bddGenDisjDecomp]

******************************************************************************/
int
Cudd_bddVarDisjDecomp(
  DdManager * dd /* manager */,
  DdNode * f /* function to be decomposed */,
  DdNode *** disjuncts /* address of the array of the disjuncts */)
{
    int result, i;

    result = Cudd_bddVarConjDecomp(dd,Cudd_Not(f),disjuncts);
    for (i = 0; i < result; i++) {
	(*disjuncts)[i] = Cudd_Not((*disjuncts)[i]);
    }
    return(result);

} /* end of Cudd_bddVarDisjDecomp */


/*---------------------------------------------------------------------------*/
/* Definition of internal functions                                          */
/*---------------------------------------------------------------------------*/

/*---------------------------------------------------------------------------*/
/* Definition of static functions                                            */
/*---------------------------------------------------------------------------*/


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

  Synopsis    [Get longest distance of node from constant.]

  Description [Get longest distance of node from constant. Returns the
  distance of the root from the constant if successful; CUDD_OUT_OF_MEM
  otherwise.]

  SideEffects [None]

  SeeAlso     []

******************************************************************************/
static NodeStat *
CreateBotDist(
  DdNode * node,
  st_table * distanceTable)
{
    DdNode *N, *Nv, *Nnv;
    int distance, distanceNv, distanceNnv;
    NodeStat *nodeStat, *nodeStatNv, *nodeStatNnv;

#if 0
    if (Cudd_IsConstant(node)) {
	return(0);
    }
#endif
    
    /* Return the entry in the table if found. */
    N = Cudd_Regular(node);
    if (st_lookup(distanceTable, (char *)N, (char **)&nodeStat)) {
	nodeStat->localRef++;
	return(nodeStat);
    }

    Nv = cuddT(N);
    Nnv = cuddE(N);
    Nv = Cudd_NotCond(Nv, Cudd_IsComplement(node));
    Nnv = Cudd_NotCond(Nnv, Cudd_IsComplement(node));

    /* Recur on the children. */
    nodeStatNv = CreateBotDist(Nv, distanceTable);
    if (nodeStatNv == NULL) return(NULL);
    distanceNv = nodeStatNv->distance;

    nodeStatNnv = CreateBotDist(Nnv, distanceTable);
    if (nodeStatNnv == NULL) return(NULL);
    distanceNnv = nodeStatNnv->distance;
    /* Store max distance from constant; note sometimes this distance
    ** may be to 0.
    */
    distance = (distanceNv > distanceNnv) ? (distanceNv+1) : (distanceNnv + 1);

    nodeStat = ALLOC(NodeStat, 1);
    if (nodeStat == NULL) {
	return(0);
    }
    nodeStat->distance = distance;
    nodeStat->localRef = 1;
    
    if (st_insert(distanceTable, (char *)N, (char *)nodeStat) ==
	ST_OUT_OF_MEM) {
	return(0);

    }
    return(nodeStat);

} /* end of CreateBotDist */


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

  Synopsis    [Count the number of minterms of each node ina a BDD and
  store it in a hash table.]

  Description []

  SideEffects [None]

  SeeAlso     []

******************************************************************************/
static double
CountMinterms(
  DdNode * node,
  double  max,
  st_table * mintermTable,
  FILE *fp)
{
    DdNode *N, *Nv, *Nnv;
    double min, minNv, minNnv;
    double *dummy;

    N = Cudd_Regular(node);

    if (cuddIsConstant(N)) {
	if (node == zero) {
	    return(0);
	} else {
	    return(max);
	}
    }

    /* Return the entry in the table if found. */
    if (st_lookup(mintermTable, (char *)node, (char **)&dummy)) {
	min = *dummy;
	return(min);
    }

    Nv = cuddT(N);
    Nnv = cuddE(N);
    Nv = Cudd_NotCond(Nv, Cudd_IsComplement(node));
    Nnv = Cudd_NotCond(Nnv, Cudd_IsComplement(node));

    /* Recur on the children. */
    minNv = CountMinterms(Nv, max, mintermTable, fp);
    if (minNv == -1.0) return(-1.0);
    minNnv = CountMinterms(Nnv, max, mintermTable, fp);
    if (minNnv == -1.0) return(-1.0);
    min = minNv / 2.0 + minNnv / 2.0;
    /* store 
     */

    dummy = ALLOC(double, 1);
    if (dummy == NULL) return(-1.0);
    *dummy = min;
    if (st_insert(mintermTable, (char *)node, (char *)dummy) == ST_OUT_OF_MEM) {
	(void) fprintf(fp, "st table insert failed\n");
    }
    return(min);

} /* end of CountMinterms */


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