cuddbridge.c

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

	}
	res = Cudd_Not(res);
    } else {
	res = (T == E) ? T : cuddUniqueInter(dd,v,T,E);
	if (res == NULL) {
	    Cudd_RecursiveDeref(dd, T);
	    Cudd_RecursiveDeref(dd, E);
	    return(NULL);
	}
    }
    cuddDeref(T);
    cuddDeref(E);

    /* Store result. */
    cuddCacheInsert1(dd,Cudd_addBddPattern,f,res);

    return(res);

} /* end of cuddAddBddDoPattern */


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


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

  Synopsis    [Performs the recursive step for Cudd_addBddThreshold.]

  Description [Performs the recursive step for Cudd_addBddThreshold.
  Returns a pointer to the BDD if successful; NULL otherwise.]

  SideEffects [None]

  SeeAlso     [addBddDoStrictThreshold]

******************************************************************************/
static DdNode *
addBddDoThreshold(
  DdManager * dd,
  DdNode * f,
  DdNode * val)
{
    DdNode *res, *T, *E;
    DdNode *fv, *fvn;
    int v;

    statLine(dd);
    /* Check terminal case. */
    if (cuddIsConstant(f)) {
	return(Cudd_NotCond(DD_ONE(dd),cuddV(f) < cuddV(val)));
    }

    /* Check cache. */
    res = cuddCacheLookup2(dd,addBddDoThreshold,f,val);
    if (res != NULL) return(res);

    /* Recursive step. */
    v = f->index;
    fv = cuddT(f); fvn = cuddE(f);

    T = addBddDoThreshold(dd,fv,val);
    if (T == NULL) return(NULL);
    cuddRef(T);

    E = addBddDoThreshold(dd,fvn,val);
    if (E == NULL) {
	Cudd_RecursiveDeref(dd, T);
	return(NULL);
    }
    cuddRef(E);
    if (Cudd_IsComplement(T)) {
	res = (T == E) ? Cudd_Not(T) : cuddUniqueInter(dd,v,Cudd_Not(T),Cudd_Not(E));
	if (res == NULL) {
	    Cudd_RecursiveDeref(dd, T);
	    Cudd_RecursiveDeref(dd, E);
	    return(NULL);
	}
	res = Cudd_Not(res);
    } else {
	res = (T == E) ? T : cuddUniqueInter(dd,v,T,E);
	if (res == NULL) {
	    Cudd_RecursiveDeref(dd, T);
	    Cudd_RecursiveDeref(dd, E);
	    return(NULL);
	}
    }
    cuddDeref(T);
    cuddDeref(E);

    /* Store result. */
    cuddCacheInsert2(dd,addBddDoThreshold,f,val,res);

    return(res);

} /* end of addBddDoThreshold */


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

  Synopsis    [Performs the recursive step for Cudd_addBddStrictThreshold.]

  Description [Performs the recursive step for Cudd_addBddStrictThreshold.
  Returns a pointer to the BDD if successful; NULL otherwise.]

  SideEffects [None]

  SeeAlso     [addBddDoThreshold]

******************************************************************************/
static DdNode *
addBddDoStrictThreshold(
  DdManager * dd,
  DdNode * f,
  DdNode * val)
{
    DdNode *res, *T, *E;
    DdNode *fv, *fvn;
    int v;

    statLine(dd);
    /* Check terminal case. */
    if (cuddIsConstant(f)) {
	return(Cudd_NotCond(DD_ONE(dd),cuddV(f) <= cuddV(val)));
    }

    /* Check cache. */
    res = cuddCacheLookup2(dd,addBddDoStrictThreshold,f,val);
    if (res != NULL) return(res);

    /* Recursive step. */
    v = f->index;
    fv = cuddT(f); fvn = cuddE(f);

    T = addBddDoStrictThreshold(dd,fv,val);
    if (T == NULL) return(NULL);
    cuddRef(T);

    E = addBddDoStrictThreshold(dd,fvn,val);
    if (E == NULL) {
	Cudd_RecursiveDeref(dd, T);
	return(NULL);
    }
    cuddRef(E);
    if (Cudd_IsComplement(T)) {
	res = (T == E) ? Cudd_Not(T) : cuddUniqueInter(dd,v,Cudd_Not(T),Cudd_Not(E));
	if (res == NULL) {
	    Cudd_RecursiveDeref(dd, T);
	    Cudd_RecursiveDeref(dd, E);
	    return(NULL);
	}
	res = Cudd_Not(res);
    } else {
	res = (T == E) ? T : cuddUniqueInter(dd,v,T,E);
	if (res == NULL) {
	    Cudd_RecursiveDeref(dd, T);
	    Cudd_RecursiveDeref(dd, E);
	    return(NULL);
	}
    }
    cuddDeref(T);
    cuddDeref(E);

    /* Store result. */
    cuddCacheInsert2(dd,addBddDoStrictThreshold,f,val,res);

    return(res);

} /* end of addBddDoStrictThreshold */


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

  Synopsis    [Performs the recursive step for Cudd_addBddInterval.]

  Description [Performs the recursive step for Cudd_addBddInterval.
  Returns a pointer to the BDD if successful; NULL otherwise.]

  SideEffects [None]

  SeeAlso     [addBddDoThreshold addBddDoStrictThreshold]

******************************************************************************/
static DdNode *
addBddDoInterval(
  DdManager * dd,
  DdNode * f,
  DdNode * l,
  DdNode * u)
{
    DdNode *res, *T, *E;
    DdNode *fv, *fvn;
    int v;

    statLine(dd);
    /* Check terminal case. */
    if (cuddIsConstant(f)) {
	return(Cudd_NotCond(DD_ONE(dd),cuddV(f) < cuddV(l) || cuddV(f) > cuddV(u)));
    }

    /* Check cache. */
    res = cuddCacheLookup(dd,DD_ADD_BDD_DO_INTERVAL_TAG,f,l,u);
    if (res != NULL) return(res);

    /* Recursive step. */
    v = f->index;
    fv = cuddT(f); fvn = cuddE(f);

    T = addBddDoInterval(dd,fv,l,u);
    if (T == NULL) return(NULL);
    cuddRef(T);

    E = addBddDoInterval(dd,fvn,l,u);
    if (E == NULL) {
	Cudd_RecursiveDeref(dd, T);
	return(NULL);
    }
    cuddRef(E);
    if (Cudd_IsComplement(T)) {
	res = (T == E) ? Cudd_Not(T) : cuddUniqueInter(dd,v,Cudd_Not(T),Cudd_Not(E));
	if (res == NULL) {
	    Cudd_RecursiveDeref(dd, T);
	    Cudd_RecursiveDeref(dd, E);
	    return(NULL);
	}
	res = Cudd_Not(res);
    } else {
	res = (T == E) ? T : cuddUniqueInter(dd,v,T,E);
	if (res == NULL) {
	    Cudd_RecursiveDeref(dd, T);
	    Cudd_RecursiveDeref(dd, E);
	    return(NULL);
	}
    }
    cuddDeref(T);
    cuddDeref(E);

    /* Store result. */
    cuddCacheInsert(dd,DD_ADD_BDD_DO_INTERVAL_TAG,f,l,u,res);

    return(res);

} /* end of addBddDoInterval */


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

  Synopsis    [Performs the recursive step for Cudd_addBddIthBit.]

  Description [Performs the recursive step for Cudd_addBddIthBit.
  Returns a pointer to the BDD if successful; NULL otherwise.]

  SideEffects [None]

  SeeAlso     []

******************************************************************************/
static DdNode *
addBddDoIthBit(
  DdManager * dd,
  DdNode * f,
  DdNode * index)
{
    DdNode *res, *T, *E;
    DdNode *fv, *fvn;
    int mask, value;
    int v;

    statLine(dd);
    /* Check terminal case. */
    if (cuddIsConstant(f)) {
	mask = 1 << ((int) cuddV(index));
	value = (int) cuddV(f);
	return(Cudd_NotCond(DD_ONE(dd),(value & mask) == 0));
    }

    /* Check cache. */
    res = cuddCacheLookup2(dd,addBddDoIthBit,f,index);
    if (res != NULL) return(res);

    /* Recursive step. */
    v = f->index;
    fv = cuddT(f); fvn = cuddE(f);

    T = addBddDoIthBit(dd,fv,index);
    if (T == NULL) return(NULL);
    cuddRef(T);

    E = addBddDoIthBit(dd,fvn,index);
    if (E == NULL) {
	Cudd_RecursiveDeref(dd, T);
	return(NULL);
    }
    cuddRef(E);
    if (Cudd_IsComplement(T)) {
	res = (T == E) ? Cudd_Not(T) : cuddUniqueInter(dd,v,Cudd_Not(T),Cudd_Not(E));
	if (res == NULL) {
	    Cudd_RecursiveDeref(dd, T);
	    Cudd_RecursiveDeref(dd, E);
	    return(NULL);
	}
	res = Cudd_Not(res);
    } else {
	res = (T == E) ? T : cuddUniqueInter(dd,v,T,E);
	if (res == NULL) {
	    Cudd_RecursiveDeref(dd, T);
	    Cudd_RecursiveDeref(dd, E);
	    return(NULL);
	}
    }
    cuddDeref(T);
    cuddDeref(E);

    /* Store result. */
    cuddCacheInsert2(dd,addBddDoIthBit,f,index,res);

    return(res);

} /* end of addBddDoIthBit */


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

  Synopsis    [Performs the recursive step for Cudd_BddToAdd.]

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

  SideEffects [None]

  SeeAlso     []

******************************************************************************/
static DdNode *
ddBddToAddRecur(
  DdManager * dd,
  DdNode * B)
{
    DdNode *one;
    DdNode *res, *res1, *T, *E, *Bt, *Be;
    int complement = 0;

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

    if (Cudd_IsConstant(B)) {
	if (B == one) {
	    res = one;
	} else {
	    res = DD_ZERO(dd);
	}
	return(res);
    }
    /* Check visited table */
    res = cuddCacheLookup1(dd,ddBddToAddRecur,B);
    if (res != NULL) return(res);

    if (Cudd_IsComplement(B)) {
	complement = 1;
	Bt = cuddT(Cudd_Regular(B));
	Be = cuddE(Cudd_Regular(B));
    } else {
	Bt = cuddT(B);
	Be = cuddE(B);
    }

    T = ddBddToAddRecur(dd, Bt);
    if (T == NULL) return(NULL);
    cuddRef(T);

    E = ddBddToAddRecur(dd, Be);
    if (E == NULL) {
	Cudd_RecursiveDeref(dd, T);
	return(NULL);
    }
    cuddRef(E);

    /* No need to check for T == E, because it is guaranteed not to happen. */
    res = cuddUniqueInter(dd, (int) Cudd_Regular(B)->index, T, E);
    if (res == NULL) {
	Cudd_RecursiveDeref(dd ,T);
	Cudd_RecursiveDeref(dd ,E);
	return(NULL);
    }
    cuddDeref(T);
    cuddDeref(E);

    if (complement) {
	cuddRef(res);
	res1 = cuddAddCmplRecur(dd, res);
	if (res1 == NULL) {
	    Cudd_RecursiveDeref(dd, res);
	    return(NULL);
	}
	cuddRef(res1);
	Cudd_RecursiveDeref(dd, res);
	res = res1;
	cuddDeref(res);
    }

    /* Store result. */
    cuddCacheInsert1(dd,ddBddToAddRecur,B,res);

    return(res);

} /* end of ddBddToAddRecur */


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

  Synopsis    [Performs the recursive step of Cudd_bddTransfer.]

  Description [Performs the recursive step of Cudd_bddTransfer.
  Returns a pointer to the result if successful; NULL otherwise.]

  SideEffects [None]

  SeeAlso     [cuddBddTransfer]

******************************************************************************/
static DdNode *
cuddBddTransferRecur(
  DdManager * ddS,
  DdManager * ddD,
  DdNode * f,
  st_table * table)
{
    DdNode *ft, *fe, *t, *e, *var, *res;
    DdNode *one, *zero;
    int	   index;
    int    comple = 0;

    statLine(ddD);
    one = DD_ONE(ddD);
    comple = Cudd_IsComplement(f);

    /* Trivial cases. */
    if (Cudd_IsConstant(f)) return(Cudd_NotCond(one, comple));

    /* Make canonical to increase the utilization of the cache. */
    f = Cudd_NotCond(f,comple);
    /* Now f is a regular pointer to a non-constant node. */

    /* Check the cache. */
    if(st_lookup(table, (char *)f, (char **) &res))
	return(Cudd_NotCond(res,comple));
    
    /* Recursive step. */
    index = f->index;
    ft = cuddT(f); fe = cuddE(f);

    t = cuddBddTransferRecur(ddS, ddD, ft, table);
    if (t == NULL) {
    	return(NULL);
    }
    cuddRef(t);

    e = cuddBddTransferRecur(ddS, ddD, fe, table);
    if (e == NULL) {
    	Cudd_RecursiveDeref(ddD, t);
    	return(NULL);
    }
    cuddRef(e);

    zero = Cudd_Not(one);
    var = cuddUniqueInter(ddD,index,one,zero);
    if (var == NULL) {
	Cudd_RecursiveDeref(ddD, t);
	Cudd_RecursiveDeref(ddD, e);
    	return(NULL);
    }
    res = cuddBddIteRecur(ddD,var,t,e);
    if (res == NULL) {
	Cudd_RecursiveDeref(ddD, t);
	Cudd_RecursiveDeref(ddD, e);
	return(NULL);
    }
    cuddRef(res);
    Cudd_RecursiveDeref(ddD, t);
    Cudd_RecursiveDeref(ddD, e);

    if (st_add_direct(table, (char *) f, (char *) res) == ST_OUT_OF_MEM) {
	Cudd_RecursiveDeref(ddD, res);
	return(NULL);
    }
    return(Cudd_NotCond(res,comple));

} /* end of cuddBddTransferRecur */