cuddapprox.c

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

		return(infoN->resultP);
	    }
	} else {
	    if (infoN->resultN != NULL) {
		return(infoN->resultN);
	    }
	}
    } else {
	(void) fprintf(dd->err,
		       "Something is wrong, ought to be in info table\n");
	dd->errorCode = CUDD_INTERNAL_ERROR;
	return(NULL);
    }

    Nt = Cudd_NotCond(cuddT(N), Cudd_IsComplement(node));
    Ne = Cudd_NotCond(cuddE(N), Cudd_IsComplement(node));

    t = UAbuildSubset(dd, Nt, info);
    if (t == NULL) {
	return(NULL);
    }
    cuddRef(t);

    e = UAbuildSubset(dd, Ne, info);
    if (e == NULL) {
	Cudd_RecursiveDeref(dd,t);
	return(NULL);
    }
    cuddRef(e);

    if (Cudd_IsComplement(t)) {
	t = Cudd_Not(t);
	e = Cudd_Not(e);
	r = (t == e) ? t : cuddUniqueInter(dd, N->index, t, e);
	if (r == NULL) {
	    Cudd_RecursiveDeref(dd, e);
	    Cudd_RecursiveDeref(dd, t);
	    return(NULL);
	}
	r = Cudd_Not(r);
    } else {
	r = (t == e) ? t : cuddUniqueInter(dd, N->index, t, e);
	if (r == NULL) {
	    Cudd_RecursiveDeref(dd, e);
	    Cudd_RecursiveDeref(dd, t);
	    return(NULL);
	}
    }
    cuddDeref(t);
    cuddDeref(e);

    if (N == node) {
	infoN->resultP = r;
    } else {
	infoN->resultN = r;
    }

    return(r);

} /* end of UAbuildSubset */


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

  Synopsis    [Marks nodes for remapping.]

  Description [Marks nodes for remapping. Returns 1 if successful; 0
  otherwise.]

  SideEffects [None]

  SeeAlso     [cuddRemapUnderApprox]

******************************************************************************/
static int
RAmarkNodes(
  DdManager * dd /* manager */,
  DdNode * f /* function to be analyzed */,
  ApproxInfo * info /* info on BDD */,
  int  threshold /* when to stop approximating */,
  double  quality /* minimum improvement for accepted changes */)
{
    DdLevelQueue *queue;
    DdLevelQueue *localQueue;
    NodeData *infoN, *infoT, *infoE;
    GlobalQueueItem *item;
    DdNode *node, *T, *E;
    DdNode *shared; /* grandchild shared by the two children of node */
    double numOnset;
    double impact, impactP, impactN;
    double minterms;
    int savings;
    int replace;

#if 0
    (void) fprintf(dd->out,"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);
    }
    /* Enqueue regular pointer to root and initialize impact. */
    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;
    }
    /* The nodes retrieved here are guaranteed to be non-terminal.
    ** The initial node is not terminal because constant nodes are
    ** dealt with in the calling procedure. Subsequent nodes are inserted
    ** only if they are not terminal. */
    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;
#ifdef DD_DEBUG
	assert(item->impactP >= 0 && item->impactP <= 1.0);
	assert(item->impactN >= 0 && item->impactN <= 1.0);
	assert(!Cudd_IsComplement(node));
	assert(!Cudd_IsConstant(node));
#endif
	if (!st_lookup(info->table, (char *)node, (char **)&infoN)) {
	    cuddLevelQueueQuit(queue);
	    cuddLevelQueueQuit(localQueue);
	    return(0);
	}
#ifdef DD_DEBUG
	assert(infoN->parity >= 1 && infoN->parity <= 3);
#endif
	if (infoN->parity == 3) {
	    /* This node can be reached through paths of different parity.
	    ** It is not safe to replace it, because remapping will give
	    ** an incorrect result, while replacement by 0 may cause node
	    ** splitting. */
	    cuddLevelQueueDequeue(queue,cuddI(dd,node->index));
	    continue;
	}
	T = cuddT(node);
	E = cuddE(node);
	shared = NULL;
	impactP = item->impactP;
	impactN = item->impactN;
	if (Cudd_bddLeq(dd,T,E)) {
	    /* Here we know that E is regular. */
#ifdef DD_DEBUG
	    assert(!Cudd_IsComplement(E));
#endif
	    (void) st_lookup(info->table, (char *)T, (char **)&infoT);
	    (void) st_lookup(info->table, (char *)E, (char **)&infoE);
	    if (infoN->parity == 1) {
		impact = impactP;
		minterms = infoE->mintermsP/2.0 - infoT->mintermsP/2.0;
		if (infoE->functionRef == 1 && !Cudd_IsConstant(E)) {
		    savings = 1 + computeSavings(dd,E,NULL,info,localQueue);
		    if (savings == 1) {
			cuddLevelQueueQuit(queue);
			cuddLevelQueueQuit(localQueue);
			return(0);
		    }
		} else {
		    savings = 1;
		}
		replace = REPLACE_E;
	    } else {
#ifdef DD_DEBUG
		assert(infoN->parity == 2);
#endif
		impact = impactN;
		minterms = infoT->mintermsN/2.0 - infoE->mintermsN/2.0;
		if (infoT->functionRef == 1 && !Cudd_IsConstant(T)) {
		    savings = 1 + computeSavings(dd,T,NULL,info,localQueue);
		    if (savings == 1) {
			cuddLevelQueueQuit(queue);
			cuddLevelQueueQuit(localQueue);
			return(0);
		    }
		} else {
		    savings = 1;
		}
		replace = REPLACE_T;
	    }
	    numOnset = impact * minterms;
	} else if (Cudd_bddLeq(dd,E,T)) {
	    /* Here E may be complemented. */
	    DdNode *Ereg = Cudd_Regular(E);
	    (void) st_lookup(info->table, (char *)T, (char **)&infoT);
	    (void) st_lookup(info->table, (char *)Ereg, (char **)&infoE);
	    if (infoN->parity == 1) {
		impact = impactP;
		minterms = infoT->mintermsP/2.0 -
		    ((E == Ereg) ? infoE->mintermsP : infoE->mintermsN)/2.0;
		if (infoT->functionRef == 1 && !Cudd_IsConstant(T)) {
		    savings = 1 + computeSavings(dd,T,NULL,info,localQueue);
		    if (savings == 1) {
			cuddLevelQueueQuit(queue);
			cuddLevelQueueQuit(localQueue);
			return(0);
		    }
		} else {
		    savings = 1;
		}
		replace = REPLACE_T;
	    } else {
#ifdef DD_DEBUG
		assert(infoN->parity == 2);
#endif
		impact = impactN;
		minterms = ((E == Ereg) ? infoE->mintermsN :
			    infoE->mintermsP)/2.0 - infoT->mintermsN/2.0;
		if (infoE->functionRef == 1 && !Cudd_IsConstant(E)) {
		    savings = 1 + computeSavings(dd,E,NULL,info,localQueue);
		    if (savings == 1) {
			cuddLevelQueueQuit(queue);
			cuddLevelQueueQuit(localQueue);
			return(0);
		    }
		} else {
		    savings = 1;
		}
		replace = REPLACE_E;
	    }
	    numOnset = impact * minterms;
	} else {
	    DdNode *Ereg = Cudd_Regular(E);
	    DdNode *TT = cuddT(T);
	    DdNode *ET = Cudd_NotCond(cuddT(Ereg), Cudd_IsComplement(E));
	    if (T->index == Ereg->index && TT == ET) {
		shared = TT;
		replace = REPLACE_TT;
	    } else {
		DdNode *TE = cuddE(T);
		DdNode *EE = Cudd_NotCond(cuddE(Ereg), Cudd_IsComplement(E));
		if (T->index == Ereg->index && TE == EE) {
		    shared = TE;
		    replace = REPLACE_TE;
		} else {
		    replace = REPLACE_N;
		}
	    }
	    numOnset = infoN->mintermsP * impactP + infoN->mintermsN * impactN;
	    savings = computeSavings(dd,node,shared,info,localQueue);
	    if (shared != NULL) {
		NodeData *infoS;
		(void) st_lookup(info->table, (char *)Cudd_Regular(shared),
				 (char **)&infoS);
		if (Cudd_IsComplement(shared)) {
		    numOnset -= (infoS->mintermsN * impactP +
			infoS->mintermsP * impactN)/2.0;
		} else {
		    numOnset -= (infoS->mintermsP * impactP +
			infoS->mintermsN * impactN)/2.0;
		}
		savings--;
	    }
	}

	cuddLevelQueueDequeue(queue,cuddI(dd,node->index));
#if 0
	if (replace == REPLACE_T || replace == REPLACE_E)
	    (void) printf("node %p: impact = %g numOnset = %g savings %d\n",
			  node, impact, numOnset, savings);
	else
	    (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 = replace;
	    info->size -= savings;
	    info->minterms -=numOnset;
#if 0
	    (void) printf("remap(%d): new size = %d new minterms = %g\n",
			  replace, info->size, info->minterms);
#endif
	    if (replace == REPLACE_N) {
		savings -= updateRefs(dd,node,NULL,info,localQueue);
	    } else if (replace == REPLACE_T) {
		savings -= updateRefs(dd,node,E,info,localQueue);
	    } else if (replace == REPLACE_E) {
		savings -= updateRefs(dd,node,T,info,localQueue);
	    } else {
#ifdef DD_DEBUG
		assert(replace == REPLACE_TT || replace == REPLACE_TE);
#endif
		savings -= updateRefs(dd,node,shared,info,localQueue) - 1;
	    }
	    assert(savings == 0);
	} else {
	    replace = NOTHING;
	}
	if (replace == REPLACE_N) continue;
	if ((replace == REPLACE_E || replace == NOTHING) &&
	    !cuddIsConstant(cuddT(node))) {
	    item = (GlobalQueueItem *) cuddLevelQueueEnqueue(queue,cuddT(node),
					 cuddI(dd,cuddT(node)->index));
	    if (replace == REPLACE_E) {
		item->impactP += impactP;
		item->impactN += impactN;
	    } else {
		item->impactP += impactP/2.0;
		item->impactN += impactN/2.0;
	    }
	}
	if ((replace == REPLACE_T || replace == NOTHING) &&
	    !Cudd_IsConstant(cuddE(node))) {
	    item = (GlobalQueueItem *) cuddLevelQueueEnqueue(queue,Cudd_Regular(cuddE(node)),
					 cuddI(dd,Cudd_Regular(cuddE(node))->index));
	    if (Cudd_IsComplement(cuddE(node))) {
		if (replace == REPLACE_T) {
		    item->impactP += impactN;
		    item->impactN += impactP;
		} else {
		    item->impactP += impactN/2.0;
		    item->impactN += impactP/2.0;
		}
	    } else {
		if (replace == REPLACE_T) {
		    item->impactP += impactP;
		    item->impactN += impactN;
		} else {
		    item->impactP += impactP/2.0;
		    item->impactN += impactN/2.0;
		}
	    }
	}
	if ((replace == REPLACE_TT || replace == REPLACE_TE) &&
	    !Cudd_IsConstant(shared)) {
	    item = (GlobalQueueItem *) cuddLevelQueueEnqueue(queue,Cudd_Regular(shared),
					 cuddI(dd,Cudd_Regular(shared)->index));
	    if (Cudd_IsComplement(shared)) {
		if (replace == REPLACE_T) {
		    item->impactP += impactN;
		    item->impactN += impactP;
		} else {
		    item->impactP += impactN/2.0;
		    item->impactN += impactP/2.0;
		}
	    } else {
		if (replace == REPLACE_T) {
		    item->impactP += impactP;
		    item->impactN += impactN;
		} else {
		    item->impactP += impactP/2.0;
		    item->impactN += impactN/2.0;
		}
	    }
	}
    }

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

} /* end of RAmarkNodes */


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

  Synopsis    [Marks nodes for remapping.]

  Description [Marks nodes for remapping. Returns 1 if successful; 0
  otherwise.]

  SideEffects [None]

  SeeAlso     [cuddRemapUnderApprox]

******************************************************************************/
static int
BAmarkNodes(
  DdManager *dd /* manager */,
  DdNode *f /* function to be analyzed */,
  ApproxInfo *info /* info on BDD */,
  int threshold /* when to stop approximating */,
  double quality1 /* minimum improvement for accepted changes when b=1 */,
  double quality0 /* minimum improvement for accepted changes when b=0 */)
{
    DdLevelQueue *queue;
    DdLevelQueue *localQueue;
    NodeData *infoN, *infoT, *infoE;
    GlobalQueueItem *item;
    DdNode *node, *T, *E;
    DdNode *shared; /* grandchild shared by the two children of node */
    double numOnset;
    double impact, impactP, impactN;
    double minterms;
    double quality;
    int savings;
    int replace;

#if 0
    (void) fprintf(dd->out,"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);