cuddapprox.c

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

  will cause underflow with 2046 variables or more.]

  SideEffects [None]

  SeeAlso     [Cudd_SupersetHeavyBranch Cudd_SupersetShortPaths
  Cudd_RemapOverApprox Cudd_BiasedUnderApprox Cudd_ReadSize]

******************************************************************************/
DdNode *
Cudd_BiasedOverApprox(
  DdManager *dd /* manager */,
  DdNode *f /* function to be superset */,
  DdNode *b /* bias function */,
  int numVars /* number of variables in the support of f */,
  int threshold /* when to stop approximation */,
  double quality1 /* minimum improvement for accepted changes when b=1*/,
  double quality0 /* minimum improvement for accepted changes when b=0 */)
{
    DdNode *subset, *g;

    g = Cudd_Not(f);    
    do {
	dd->reordered = 0;
	subset = cuddBiasedUnderApprox(dd, g, b, numVars, threshold, quality1,
				      quality0);
    } while (dd->reordered == 1);
    
    return(Cudd_NotCond(subset, (subset != NULL)));
    
} /* end of Cudd_BiasedOverApprox */


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


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

  Synopsis    [Applies Tom Shiple's underappoximation algorithm.]

  Description [Applies Tom Shiple's underappoximation algorithm. Proceeds
  in three phases:
  <ul>
  <li> collect information on each node in the BDD; this is done via DFS.
  <li> traverse the BDD in top-down fashion and compute for each node
  whether its elimination increases density.
  <li> traverse the BDD via DFS and actually perform the elimination.
  </ul>
  Returns the approximated BDD if successful; NULL otherwise.]

  SideEffects [None]

  SeeAlso     [Cudd_UnderApprox]

******************************************************************************/
DdNode *
cuddUnderApprox(
  DdManager * dd /* DD manager */,
  DdNode * f /* current DD */,
  int  numVars /* maximum number of variables */,
  int  threshold /* threshold under which approximation stops */,
  int  safe /* enforce safe approximation */,
  double  quality /* minimum improvement for accepted changes */)
{
    ApproxInfo *info;
    DdNode *subset;
    int result;

    if (f == NULL) {
	fprintf(dd->err, "Cannot subset, nil object\n");
	return(NULL);
    }

    if (Cudd_IsConstant(f)) {
	return(f);
    }

    /* Create table where node data are accessible via a hash table. */
    info = gatherInfo(dd, f, numVars, safe);
    if (info == NULL) {
	(void) fprintf(dd->err, "Out-of-memory; Cannot subset\n");
	dd->errorCode = CUDD_MEMORY_OUT;
	return(NULL);
    }

    /* Mark nodes that should be replaced by zero. */
    result = UAmarkNodes(dd, f, info, threshold, safe, quality);
    if (result == 0) {
	(void) fprintf(dd->err, "Out-of-memory; Cannot subset\n");
	FREE(info->page);
	st_free_table(info->table);
	FREE(info);
	dd->errorCode = CUDD_MEMORY_OUT;
	return(NULL);
    }

    /* Build the result. */
    subset = UAbuildSubset(dd, f, info);
#if 1
    if (subset && info->size < Cudd_DagSize(subset))
	(void) fprintf(dd->err, "Wrong prediction: %d versus actual %d\n",
		       info->size, Cudd_DagSize(subset));
#endif
    FREE(info->page);
    st_free_table(info->table);
    FREE(info);

#ifdef DD_DEBUG
    if (subset != NULL) {
	cuddRef(subset);
#if 0
	(void) Cudd_DebugCheck(dd);
	(void) Cudd_CheckKeys(dd);
#endif
	if (!Cudd_bddLeq(dd, subset, f)) {
	    (void) fprintf(dd->err, "Wrong subset\n");
	    dd->errorCode = CUDD_INTERNAL_ERROR;
	}
	cuddDeref(subset);
    }
#endif
    return(subset);

} /* end of cuddUnderApprox */


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

  Synopsis    [Applies the remapping underappoximation algorithm.]

  Description [Applies the remapping underappoximation algorithm.
  Proceeds in three phases:
  <ul>
  <li> collect information on each node in the BDD; this is done via DFS.
  <li> traverse the BDD in top-down fashion and compute for each node
  whether remapping increases density.
  <li> traverse the BDD via DFS and actually perform the elimination.
  </ul>
  Returns the approximated BDD if successful; NULL otherwise.]

  SideEffects [None]

  SeeAlso     [Cudd_RemapUnderApprox]

******************************************************************************/
DdNode *
cuddRemapUnderApprox(
  DdManager * dd /* DD manager */,
  DdNode * f /* current DD */,
  int  numVars /* maximum number of variables */,
  int  threshold /* threshold under which approximation stops */,
  double  quality /* minimum improvement for accepted changes */)
{
    ApproxInfo *info;
    DdNode *subset;
    int result;

    if (f == NULL) {
	fprintf(dd->err, "Cannot subset, nil object\n");
	dd->errorCode = CUDD_INVALID_ARG;
	return(NULL);
    }

    if (Cudd_IsConstant(f)) {
	return(f);
    }

    /* Create table where node data are accessible via a hash table. */
    info = gatherInfo(dd, f, numVars, TRUE);
    if (info == NULL) {
	(void) fprintf(dd->err, "Out-of-memory; Cannot subset\n");
	dd->errorCode = CUDD_MEMORY_OUT;
	return(NULL);
    }

    /* Mark nodes that should be replaced by zero. */
    result = RAmarkNodes(dd, f, info, threshold, quality);
    if (result == 0) {
	(void) fprintf(dd->err, "Out-of-memory; Cannot subset\n");
	FREE(info->page);
	st_free_table(info->table);
	FREE(info);
	dd->errorCode = CUDD_MEMORY_OUT;
	return(NULL);
    }

    /* Build the result. */
    subset = RAbuildSubset(dd, f, info);
#if 1
    if (subset && info->size < Cudd_DagSize(subset))
	(void) fprintf(dd->err, "Wrong prediction: %d versus actual %d\n",
		       info->size, Cudd_DagSize(subset));
#endif
    FREE(info->page);
    st_free_table(info->table);
    FREE(info);

#ifdef DD_DEBUG
    if (subset != NULL) {
	cuddRef(subset);
#if 0
	(void) Cudd_DebugCheck(dd);
	(void) Cudd_CheckKeys(dd);
#endif
	if (!Cudd_bddLeq(dd, subset, f)) {
	    (void) fprintf(dd->err, "Wrong subset\n");
	}
	cuddDeref(subset);
	dd->errorCode = CUDD_INTERNAL_ERROR;
    }
#endif
    return(subset);

} /* end of cuddRemapUnderApprox */


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

  Synopsis    [Applies the biased remapping underappoximation algorithm.]

  Description [Applies the biased remapping underappoximation algorithm.
  Proceeds in three phases:
  <ul>
  <li> collect information on each node in the BDD; this is done via DFS.
  <li> traverse the BDD in top-down fashion and compute for each node
  whether remapping increases density.
  <li> traverse the BDD via DFS and actually perform the elimination.
  </ul>
  Returns the approximated BDD if successful; NULL otherwise.]

  SideEffects [None]

  SeeAlso     [Cudd_BiasedUnderApprox]

******************************************************************************/
DdNode *
cuddBiasedUnderApprox(
  DdManager *dd /* DD manager */,
  DdNode *f /* current DD */,
  DdNode *b /* bias function */,
  int numVars /* maximum number of variables */,
  int threshold /* threshold under which approximation stops */,
  double quality1 /* minimum improvement for accepted changes when b=1 */,
  double quality0 /* minimum improvement for accepted changes when b=1 */)
{
    ApproxInfo *info;
    DdNode *subset;
    int result;
    DdHashTable	*cache;

    if (f == NULL) {
	fprintf(dd->err, "Cannot subset, nil object\n");
	dd->errorCode = CUDD_INVALID_ARG;
	return(NULL);
    }

    if (Cudd_IsConstant(f)) {
	return(f);
    }

    /* Create table where node data are accessible via a hash table. */
    info = gatherInfo(dd, f, numVars, TRUE);
    if (info == NULL) {
	(void) fprintf(dd->err, "Out-of-memory; Cannot subset\n");
	dd->errorCode = CUDD_MEMORY_OUT;
	return(NULL);
    }

    cache = cuddHashTableInit(dd,2,2);
    result = BAapplyBias(dd, Cudd_Regular(f), b, info, cache);
    if (result == CARE_ERROR) {
	(void) fprintf(dd->err, "Out-of-memory; Cannot subset\n");
	cuddHashTableQuit(cache);
	FREE(info->page);
	st_free_table(info->table);
	FREE(info);
	dd->errorCode = CUDD_MEMORY_OUT;
	return(NULL);
    }
    cuddHashTableQuit(cache);

    /* Mark nodes that should be replaced by zero. */
    result = BAmarkNodes(dd, f, info, threshold, quality1, quality0);
    if (result == 0) {
	(void) fprintf(dd->err, "Out-of-memory; Cannot subset\n");
	FREE(info->page);
	st_free_table(info->table);
	FREE(info);
	dd->errorCode = CUDD_MEMORY_OUT;
	return(NULL);
    }

    /* Build the result. */
    subset = RAbuildSubset(dd, f, info);
#if 1
    if (subset && info->size < Cudd_DagSize(subset))
	(void) fprintf(dd->err, "Wrong prediction: %d versus actual %d\n",
		       info->size, Cudd_DagSize(subset));
#endif
    FREE(info->page);
    st_free_table(info->table);
    FREE(info);

#ifdef DD_DEBUG
    if (subset != NULL) {
	cuddRef(subset);
#if 0
	(void) Cudd_DebugCheck(dd);
	(void) Cudd_CheckKeys(dd);
#endif
	if (!Cudd_bddLeq(dd, subset, f)) {
	    (void) fprintf(dd->err, "Wrong subset\n");
	}
	cuddDeref(subset);
	dd->errorCode = CUDD_INTERNAL_ERROR;
    }
#endif
    return(subset);

} /* end of cuddBiasedUnderApprox */


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


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

  Synopsis    [Recursively update the parity of the paths reaching a node.]

  Description [Recursively update the parity of the paths reaching a node.
  Assumes that node is regular and propagates the invariant.]

  SideEffects [None]

  SeeAlso     [gatherInfoAux]

******************************************************************************/
static void
updateParity(
  DdNode * node /* function to analyze */,
  ApproxInfo * info /* info on BDD */,
  int  newparity /* new parity for node */)
{
    NodeData *infoN;
    DdNode *E;

    if (!st_lookup(info->table, (char *)node, (char **)&infoN)) return;
    if ((infoN->parity & newparity) != 0) return;
    infoN->parity |= newparity;
    if (Cudd_IsConstant(node)) return;
    updateParity(cuddT(node),info,newparity);
    E = cuddE(node);
    if (Cudd_IsComplement(E)) {
	updateParity(Cudd_Not(E),info,3-newparity);
    } else {
	updateParity(E,info,newparity);
    }
    return;

} /* end of updateParity */


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

  Synopsis    [Recursively counts minterms and computes reference counts
  of each node in the BDD.]

  Description [Recursively counts minterms and computes reference
  counts of each node in the BDD.  Similar to the cuddCountMintermAux
  which recursively counts the number of minterms for the dag rooted
  at each node in terms of the total number of variables (max). It assumes
  that the node pointer passed to it is regular and it maintains the
  invariant.]

  SideEffects [None]

  SeeAlso     [gatherInfo]

******************************************************************************/
static NodeData *
gatherInfoAux(
  DdNode * node /* function to analyze */,
  ApproxInfo * info /* info on BDD */,
  int  parity /* gather parity information */)
{
    DdNode	*N, *Nt, *Ne;
    NodeData	*infoN, *infoT, *infoE;

    N = Cudd_Regular(node);

    /* Check whether entry for this node exists. */
    if (st_lookup(info->table, (char *)N, (char **)&infoN)) {
	if (parity) {
	    /* Update parity and propagate. */
	    updateParity(N, info, 1 +  (int) Cudd_IsComplement(node));
	}
	return(infoN);
    }

    /* Compute the cofactors. */
    Nt = Cudd_NotCond(cuddT(N), N != node);
    Ne = Cudd_NotCond(cuddE(N), N != node);

    infoT = gatherInfoAux(Nt, info, parity);
    if (infoT == NULL) return(NULL);
    infoE = gatherInfoAux(Ne, info, parity);
    if (infoE == NULL) return(NULL);

    infoT->functionRef++;
    infoE->functionRef++;

    /* Point to the correct location in the page. */
    infoN = &(info->page[info->index++]);
    infoN->parity |= 1 + (short) Cudd_IsComplement(node);

    infoN->mintermsP = infoT->mintermsP/2;
    infoN->mintermsN = infoT->mintermsN/2;
    if (Cudd_IsComplement(Ne) ^ Cudd_IsComplement(node)) {
	infoN->mintermsP += infoE->mintermsN/2;