cuddapprox.c

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

	infoN->mintermsN += infoE->mintermsP/2;
    } else {
	infoN->mintermsP += infoE->mintermsP/2;
	infoN->mintermsN += infoE->mintermsN/2;
    }

    /* Insert entry for the node in the table. */
    if (st_insert(info->table,(char *)N, (char *)infoN) == ST_OUT_OF_MEM) {
	return(NULL);
    }
    return(infoN);

} /* end of gatherInfoAux */


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

  Synopsis    [Gathers information about each node.]

  Description [Counts minterms and computes reference counts of each
  node in the BDD . The minterm count is separately computed for the
  node and its complement. This is to avoid cancellation
  errors. Returns a pointer to the data structure holding the
  information gathered if successful; NULL otherwise.]

  SideEffects [None]

  SeeAlso     [cuddUnderApprox gatherInfoAux]

******************************************************************************/
static ApproxInfo *
gatherInfo(
  DdManager * dd /* manager */,
  DdNode * node /* function to be analyzed */,
  int  numVars /* number of variables node depends on */,
  int  parity /* gather parity information */)
{
    ApproxInfo	*info;
    NodeData *infoTop;

    /* If user did not give numVars value, set it to the maximum
    ** exponent that the pow function can take. The -1 is due to the
    ** discrepancy in the value that pow takes and the value that
    ** log gives.
    */
    if (numVars == 0) {
	numVars = DBL_MAX_EXP - 1;
    }

    info = ALLOC(ApproxInfo,1);
    if (info == NULL) {
	dd->errorCode = CUDD_MEMORY_OUT;
	return(NULL);
    }
    info->max = pow(2.0,(double) numVars);
    info->one = DD_ONE(dd);
    info->zero = Cudd_Not(info->one);
    info->size = Cudd_DagSize(node);
    /* All the information gathered will be stored in a contiguous
    ** piece of memory, which is allocated here. This can be done
    ** efficiently because we have counted the number of nodes of the
    ** BDD. info->index points to the next available entry in the array
    ** that stores the per-node information. */
    info->page = ALLOC(NodeData,info->size);
    if (info->page == NULL) {
	dd->errorCode = CUDD_MEMORY_OUT;
	FREE(info);
	return(NULL);
    }
    memset(info->page, 0, info->size * sizeof(NodeData)); /* clear all page */
    info->table = st_init_table(st_ptrcmp,st_ptrhash);
    if (info->table == NULL) {
	FREE(info->page);
	FREE(info);
	return(NULL);
    }
    /* We visit the DAG in post-order DFS. Hence, the constant node is
    ** in first position, and the root of the DAG is in last position. */

    /* Info for the constant node: Initialize only fields different from 0. */
    if (st_insert(info->table, (char *)info->one, (char *)info->page) == ST_OUT_OF_MEM) {
	FREE(info->page);
	FREE(info);
	st_free_table(info->table);
	return(NULL);
    }
    info->page[0].mintermsP = info->max;
    info->index = 1;

    infoTop = gatherInfoAux(node,info,parity);
    if (infoTop == NULL) {
	FREE(info->page);
	st_free_table(info->table);
	FREE(info);
	return(NULL);
    }
    if (Cudd_IsComplement(node)) {
	info->minterms = infoTop->mintermsN;
    } else {
	info->minterms = infoTop->mintermsP;
    }

    infoTop->functionRef = 1;
    return(info);

} /* end of gatherInfo */


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

  Synopsis    [Counts the nodes that would be eliminated if a given node
  were replaced by zero.]

  Description [Counts the nodes that would be eliminated if a given
  node were replaced by zero. This procedure uses a queue passed by
  the caller for efficiency: since the queue is left empty at the
  endof the search, it can be reused as is by the next search. Returns
  the count (always striclty positive) if successful; 0 otherwise.]

  SideEffects [None]

  SeeAlso     [cuddUnderApprox]

******************************************************************************/
static int
computeSavings(
  DdManager * dd,
  DdNode * f,
  DdNode * skip,
  ApproxInfo * info,
  DdLevelQueue * queue)
{
    NodeData *infoN;
    LocalQueueItem *item;
    DdNode *node;
    int savings = 0;

    node = Cudd_Regular(f);
    skip = Cudd_Regular(skip);
    /* Insert the given node in the level queue. Its local reference
    ** count is set equal to the function reference count so that the
    ** search will continue from it when it is retrieved. */
    item = (LocalQueueItem *)
	cuddLevelQueueEnqueue(queue,node,cuddI(dd,node->index));
    if (item == NULL)
	return(0);
    (void) st_lookup(info->table, (char *)node, (char **)&infoN);
    item->localRef = infoN->functionRef;

    /* Process the queue. */
    while (queue->first != NULL) {
	item = (LocalQueueItem *) queue->first;
	node = item->node;
	cuddLevelQueueDequeue(queue,cuddI(dd,node->index));
	if (node == skip) continue;
	(void) st_lookup(info->table, (char *)node, (char **)&infoN);
	if (item->localRef != infoN->functionRef) {
	    /* This node is shared. */
	    continue;
	}
	savings++;
	if (!cuddIsConstant(cuddT(node))) {
	    item = (LocalQueueItem *) cuddLevelQueueEnqueue(queue,cuddT(node),
					 cuddI(dd,cuddT(node)->index));
	    if (item == NULL) return(0);
	    item->localRef++;
	}
	if (!Cudd_IsConstant(cuddE(node))) {
	    item = (LocalQueueItem *) cuddLevelQueueEnqueue(queue,Cudd_Regular(cuddE(node)),
					 cuddI(dd,Cudd_Regular(cuddE(node))->index));
	    if (item == NULL) return(0);
	    item->localRef++;
	}
    }

#ifdef DD_DEBUG
    /* At the end of a local search the queue should be empty. */
    assert(queue->size == 0);
#endif
    return(savings);

} /* end of computeSavings */


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

  Synopsis    [Update function reference counts.]

  Description [Update function reference counts to account for replacement.
  Returns the number of nodes saved if successful; 0 otherwise.]

  SideEffects [None]

  SeeAlso     [UAmarkNodes RAmarkNodes]

******************************************************************************/
static int
updateRefs(
  DdManager * dd,
  DdNode * f,
  DdNode * skip,
  ApproxInfo * info,
  DdLevelQueue * queue)
{
    NodeData *infoN;
    LocalQueueItem *item;
    DdNode *node;
    int savings = 0;

    node = Cudd_Regular(f);
    /* Insert the given node in the level queue. Its function reference
    ** count is set equal to 0 so that the search will continue from it
    ** when it is retrieved. */
    item = (LocalQueueItem *) cuddLevelQueueEnqueue(queue,node,cuddI(dd,node->index));
    if (item == NULL)
	return(0);
    (void) st_lookup(info->table, (char *)node, (char **)&infoN);
    infoN->functionRef = 0;

    if (skip != NULL) {
	/* Increase the function reference count of the node to be skipped
	** by 1 to account for the node pointing to it that will be created. */
	skip = Cudd_Regular(skip);
	(void) st_lookup(info->table, (char *)skip, (char **)&infoN);
	infoN->functionRef++;
    }

    /* Process the queue. */
    while (queue->first != NULL) {
	item = (LocalQueueItem *) queue->first;
	node = item->node;
	cuddLevelQueueDequeue(queue,cuddI(dd,node->index));
	(void) st_lookup(info->table, (char *)node, (char **)&infoN);
	if (infoN->functionRef != 0) {
	    /* This node is shared or must be skipped. */
	    continue;
	}
	savings++;
	if (!cuddIsConstant(cuddT(node))) {
	    item = (LocalQueueItem *) cuddLevelQueueEnqueue(queue,cuddT(node),
					 cuddI(dd,cuddT(node)->index));
	    if (item == NULL) return(0);
	    (void) st_lookup(info->table, (char *)cuddT(node),
			     (char **)&infoN);
	    infoN->functionRef--;
	}
	if (!Cudd_IsConstant(cuddE(node))) {
	    item = (LocalQueueItem *) cuddLevelQueueEnqueue(queue,Cudd_Regular(cuddE(node)),
					 cuddI(dd,Cudd_Regular(cuddE(node))->index));
	    if (item == NULL) return(0);
	    (void) st_lookup(info->table, (char *)Cudd_Regular(cuddE(node)),
			     (char **)&infoN);
	    infoN->functionRef--;
	}
    }

#ifdef DD_DEBUG
    /* At the end of a local search the queue should be empty. */
    assert(queue->size == 0);
#endif
    return(savings);

} /* end of updateRefs */


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

  Synopsis    [Marks nodes for replacement by zero.]

  Description [Marks nodes for replacement by zero. Returns 1 if successful;
  0 otherwise.]

  SideEffects [None]

  SeeAlso     [cuddUnderApprox]

******************************************************************************/
static int
UAmarkNodes(
  DdManager * dd /* manager */,
  DdNode * f /* function to be analyzed */,
  ApproxInfo * info /* info on BDD */,
  int  threshold /* when to stop approximating */,
  int  safe /* enforce safe approximation */,
  double  quality /* minimum improvement for accepted changes */)
{
    DdLevelQueue *queue;
    DdLevelQueue *localQueue;
    NodeData *infoN;
    GlobalQueueItem *item;
    DdNode *node;
    double numOnset;
    double impactP, impactN;
    int savings;

#if 0
    (void) printf("initial size = %d initial minterms = %g\n",
		  info->size, info->minterms);
#endif
    queue = cuddLevelQueueInit(dd->size,sizeof(GlobalQueueItem),info->size);
    if (queue == NULL) {
	return(0);
    }
    localQueue = cuddLevelQueueInit(dd->size,sizeof(LocalQueueItem),
				    dd->initSlots);
    if (localQueue == NULL) {
	cuddLevelQueueQuit(queue);
	return(0);
    }
    node = Cudd_Regular(f);
    item = (GlobalQueueItem *) cuddLevelQueueEnqueue(queue,node,cuddI(dd,node->index));
    if (item == NULL) {
	cuddLevelQueueQuit(queue);
	cuddLevelQueueQuit(localQueue);
	return(0);
    }
    if (Cudd_IsComplement(f)) {
	item->impactP = 0.0;
	item->impactN = 1.0;
    } else {
	item->impactP = 1.0;
	item->impactN = 0.0;
    }
    while (queue->first != NULL) {
	/* If the size of the subset is below the threshold, quit. */
	if (info->size <= threshold)
	    break;
	item = (GlobalQueueItem *) queue->first;
	node = item->node;
	node = Cudd_Regular(node);
	(void) st_lookup(info->table, (char *)node, (char **)&infoN);
	if (safe && infoN->parity == 3) {
	    cuddLevelQueueDequeue(queue,cuddI(dd,node->index));
	    continue;
	}
	impactP = item->impactP;
	impactN = item->impactN;
	numOnset = infoN->mintermsP * impactP + infoN->mintermsN * impactN;
	savings = computeSavings(dd,node,NULL,info,localQueue);
	if (savings == 0) {
	    cuddLevelQueueQuit(queue);
	    cuddLevelQueueQuit(localQueue);
	    return(0);
	}
	cuddLevelQueueDequeue(queue,cuddI(dd,node->index));
#if 0
	(void) printf("node %p: impact = %g/%g numOnset = %g savings %d\n",
		      node, impactP, impactN, numOnset, savings);
#endif
	if ((1 - numOnset / info->minterms) >
	    quality * (1 - (double) savings / info->size)) {
	    infoN->replace = TRUE;
	    info->size -= savings;
	    info->minterms -=numOnset;
#if 0
	    (void) printf("replace: new size = %d new minterms = %g\n",
			  info->size, info->minterms);
#endif
	    savings -= updateRefs(dd,node,NULL,info,localQueue);
	    assert(savings == 0);
	    continue;
	}
	if (!cuddIsConstant(cuddT(node))) {
	    item = (GlobalQueueItem *) cuddLevelQueueEnqueue(queue,cuddT(node),
					 cuddI(dd,cuddT(node)->index));
	    item->impactP += impactP/2.0;
	    item->impactN += impactN/2.0;
	}
	if (!Cudd_IsConstant(cuddE(node))) {
	    item = (GlobalQueueItem *) cuddLevelQueueEnqueue(queue,Cudd_Regular(cuddE(node)),
					 cuddI(dd,Cudd_Regular(cuddE(node))->index));
	    if (Cudd_IsComplement(cuddE(node))) {
		item->impactP += impactN/2.0;
		item->impactN += impactP/2.0;
	    } else {
		item->impactP += impactP/2.0;
		item->impactN += impactN/2.0;
	    }
	}
    }

    cuddLevelQueueQuit(queue);
    cuddLevelQueueQuit(localQueue);
    return(1);

} /* end of UAmarkNodes */


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

  Synopsis    [Builds the subset BDD.] 

  Description [Builds the subset BDD. Based on the info table,
  replaces selected nodes by zero. Returns a pointer to the result if
  successful; NULL otherwise.]

  SideEffects [None]

  SeeAlso     [cuddUnderApprox]

******************************************************************************/
static DdNode *
UAbuildSubset(
  DdManager * dd /* DD manager */,
  DdNode * node /* current node */,
  ApproxInfo * info /* node info */)
{

    DdNode *Nt, *Ne, *N, *t, *e, *r;
    NodeData *infoN;

    if (Cudd_IsConstant(node))
	return(node);

    N = Cudd_Regular(node);

    if (st_lookup(info->table, (char *)N, (char **)&infoN)) {
	if (infoN->replace == TRUE) {
	    return(info->zero);
	}
	if (N == node ) {
	    if (infoN->resultP != NULL) {