cuddaddite.c

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

  Returns a pointer to the resulting ADD if successful; NULL otherwise.]

  SideEffects [None]

  SeeAlso     [Cudd_addNegate]

******************************************************************************/
DdNode *
Cudd_addCmpl(
  DdManager * dd,
  DdNode * f)
{
    DdNode *res;

    do {
	dd->reordered = 0;
	res = cuddAddCmplRecur(dd,f);
    } while (dd->reordered == 1);
    return(res);

} /* end of Cudd_addCmpl */


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

  Synopsis    [Determines whether f is less than or equal to g.]

  Description [Returns 1 if f is less than or equal to g; 0 otherwise.
  No new nodes are created. This procedure works for arbitrary ADDs.
  For 0-1 ADDs Cudd_addEvalConst is more efficient.]

  SideEffects [None]

  SeeAlso     [Cudd_addIteConstant Cudd_addEvalConst Cudd_bddLeq]

******************************************************************************/
int
Cudd_addLeq(
  DdManager * dd,
  DdNode * f,
  DdNode * g)
{
    DdNode *tmp, *fv, *fvn, *gv, *gvn;
    unsigned int topf, topg, res;

    /* Terminal cases. */
    if (f == g) return(1);

    statLine(dd);
    if (cuddIsConstant(f)) {
	if (cuddIsConstant(g)) return(cuddV(f) <= cuddV(g));
	if (f == DD_MINUS_INFINITY(dd)) return(1);
	if (f == DD_PLUS_INFINITY(dd)) return(0); /* since f != g */
    }
    if (g == DD_PLUS_INFINITY(dd)) return(1);
    if (g == DD_MINUS_INFINITY(dd)) return(0); /* since f != g */

    /* Check cache. */
    tmp = cuddCacheLookup2(dd,(DdNode * (*)(DdManager *, DdNode *,
			   DdNode *))Cudd_addLeq,f,g);
    if (tmp != NULL) {
	return(tmp == DD_ONE(dd));
    }

    /* Compute cofactors. One of f and g is not constant. */
    topf = cuddI(dd,f->index);
    topg = cuddI(dd,g->index);
    if (topf <= topg) {
	fv = cuddT(f); fvn = cuddE(f);
    } else {
	fv = fvn = f;
    }
    if (topg <= topf) {
	gv = cuddT(g); gvn = cuddE(g);
    } else {
	gv = gvn = g;
    }

    res = Cudd_addLeq(dd,fvn,gvn) && Cudd_addLeq(dd,fv,gv);

    /* Store result in cache and return. */
    cuddCacheInsert2(dd,(DdNode * (*)(DdManager *, DdNode *, DdNode *))
		     Cudd_addLeq,f,g,Cudd_NotCond(DD_ONE(dd),res==0));
    return(res);

} /* end of Cudd_addLeq */


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


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

  Synopsis    [Implements the recursive step of Cudd_addIte(f,g,h).]

  Description [Implements the recursive step of Cudd_addIte(f,g,h).
  Returns a pointer to the resulting ADD if successful; NULL
  otherwise.]

  SideEffects [None]

  SeeAlso     [Cudd_addIte]

******************************************************************************/
DdNode *
cuddAddIteRecur(
  DdManager * dd,
  DdNode * f,
  DdNode * g,
  DdNode * h)
{
    DdNode *one,*zero;
    DdNode *r,*Fv,*Fnv,*Gv,*Gnv,*Hv,*Hnv,*t,*e;
    unsigned int topf,topg,toph,v;
    int index;

    statLine(dd);
    /* Trivial cases. */

    /* One variable cases. */
    if (f == (one = DD_ONE(dd))) {	/* ITE(1,G,H) = G */
        return(g);
    }
    if (f == (zero = DD_ZERO(dd))) {	/* ITE(0,G,H) = H */
        return(h);
    }

    /* From now on, f is known to not be a constant. */
    addVarToConst(f,&g,&h,one,zero);

    /* Check remaining one variable cases. */
    if (g == h) {			/* ITE(F,G,G) = G */
        return(g);
    }

    if (g == one) {			/* ITE(F,1,0) = F */
        if (h == zero) return(f);
    }

    topf = cuddI(dd,f->index);
    topg = cuddI(dd,g->index);
    toph = cuddI(dd,h->index);
    v = ddMin(topg,toph);

    /* A shortcut: ITE(F,G,H) = (x,G,H) if F=(x,1,0), x < top(G,H). */
    if (topf < v && cuddT(f) == one && cuddE(f) == zero) {
	r = cuddUniqueInter(dd,(int)f->index,g,h);
	return(r);
    }
    if (topf < v && cuddT(f) == zero && cuddE(f) == one) {
	r = cuddUniqueInter(dd,(int)f->index,h,g);
	return(r);
    }

    /* Check cache. */
    r = cuddCacheLookup(dd,DD_ADD_ITE_TAG,f,g,h);
    if (r != NULL) {
        return(r);
    }

    /* Compute cofactors. */
    if (topf <= v) {
	v = ddMin(topf,v);	/* v = top_var(F,G,H) */
	index = f->index;
        Fv = cuddT(f); Fnv = cuddE(f);
    } else {
        Fv = Fnv = f;
    }
    if (topg == v) {
	index = g->index;
        Gv = cuddT(g); Gnv = cuddE(g);
    } else {
        Gv = Gnv = g;
    }
    if (toph == v) {
	index = h->index;
        Hv = cuddT(h); Hnv = cuddE(h);
    } else {
        Hv = Hnv = h;
    }
    
    /* Recursive step. */
    t = cuddAddIteRecur(dd,Fv,Gv,Hv);
    if (t == NULL) return(NULL);
    cuddRef(t);

    e = cuddAddIteRecur(dd,Fnv,Gnv,Hnv);
    if (e == NULL) {
	Cudd_RecursiveDeref(dd,t);
	return(NULL);
    }
    cuddRef(e);

    r = (t == e) ? t : cuddUniqueInter(dd,index,t,e);
    if (r == NULL) {
	Cudd_RecursiveDeref(dd,t);
	Cudd_RecursiveDeref(dd,e);
	return(NULL);
    }
    cuddDeref(t);
    cuddDeref(e);

    cuddCacheInsert(dd,DD_ADD_ITE_TAG,f,g,h,r);

    return(r);

} /* end of cuddAddIteRecur */


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

  Synopsis    [Performs the recursive step of Cudd_addCmpl.]

  Description [Performs the recursive step of Cudd_addCmpl. Returns a
  pointer to the resulting ADD if successful; NULL otherwise.]

  SideEffects [None]

  SeeAlso     [Cudd_addCmpl]

******************************************************************************/
DdNode *
cuddAddCmplRecur(
  DdManager * dd,
  DdNode * f)
{
    DdNode *one,*zero;
    DdNode *r,*Fv,*Fnv,*t,*e;

    statLine(dd);
    one = DD_ONE(dd);
    zero = DD_ZERO(dd); 

    if (cuddIsConstant(f)) {
        if (f == zero) {
	    return(one);
	} else {
	    return(zero);
	}
    }
    r = cuddCacheLookup1(dd,Cudd_addCmpl,f);
    if (r != NULL) {
	return(r);
    }
    Fv = cuddT(f);
    Fnv = cuddE(f);
    t = cuddAddCmplRecur(dd,Fv);
    if (t == NULL) return(NULL);
    cuddRef(t);
    e = cuddAddCmplRecur(dd,Fnv);
    if (e == NULL) {
	Cudd_RecursiveDeref(dd,t);
	return(NULL);
    }
    cuddRef(e);
    r = (t == e) ? t : cuddUniqueInter(dd,(int)f->index,t,e);
    if (r == NULL) {
	Cudd_RecursiveDeref(dd, t);
	Cudd_RecursiveDeref(dd, e);
	return(NULL);
    }
    cuddDeref(t);
    cuddDeref(e);
    cuddCacheInsert1(dd,Cudd_addCmpl,f,r);
    return(r);

} /* end of cuddAddCmplRecur */


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


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

  Synopsis [Replaces variables with constants if possible (part of
  canonical form).]

  Description []

  SideEffects [None]

******************************************************************************/
static void
addVarToConst(
  DdNode * f,
  DdNode ** gp,
  DdNode ** hp,
  DdNode * one,
  DdNode * zero)
{
    DdNode *g = *gp;
    DdNode *h = *hp;

    if (f == g) { /* ITE(F,F,H) = ITE(F,1,H) = F + H */
	*gp = one;
    }

    if (f == h) { /* ITE(F,G,F) = ITE(F,G,0) = F * G */
	*hp = zero;
    }

} /* end of addVarToConst */