cuddcompose.c

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

    }

    /* Split and recur on children of this node. */
    T = cuddAddVectorComposeRecur(dd,table,cuddT(f),vector,deepest);
    if (T == NULL)  return(NULL);
    cuddRef(T);
    E = cuddAddVectorComposeRecur(dd,table,cuddE(f),vector,deepest);
    if (E == NULL) {
	Cudd_RecursiveDeref(dd, T);
	return(NULL);
    }
    cuddRef(E);

    /* Retrieve the 0-1 ADD for the current top variable and call
    ** cuddAddIteRecur with the T and E we just created.
    */
    res = cuddAddIteRecur(dd,vector[f->index],T,E);
    if (res == NULL) {
	Cudd_RecursiveDeref(dd, T);
	Cudd_RecursiveDeref(dd, E);
	return(NULL);
    }
    cuddRef(res);
    Cudd_RecursiveDeref(dd, T);
    Cudd_RecursiveDeref(dd, E);

    /* Do not keep the result if the reference count is only 1, since
    ** it will not be visited again
    */
    if (f->ref != 1) {
	ptrint fanout = (ptrint) f->ref;
	cuddSatDec(fanout);
	if (!cuddHashTableInsert1(table,f,res,fanout)) {
	    Cudd_RecursiveDeref(dd, res);
	    return(NULL);
	}
    }
    cuddDeref(res);
    return(res);

} /* end of cuddAddVectorComposeRecur */


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

  Synopsis    [Performs the recursive step of Cudd_addGeneralVectorCompose.]

  Description []

  SideEffects [None]

  SeeAlso     []

******************************************************************************/
static DdNode *
cuddAddGeneralVectorComposeRecur(
  DdManager * dd /* DD manager */,
  DdHashTable * table /* computed table */,
  DdNode * f /* ADD in which to compose */,
  DdNode ** vectorOn /* functions to substitute for x_i */,
  DdNode ** vectorOff /* functions to substitute for x_i' */,
  int  deepest /* depth of deepest substitution */)
{
    DdNode	*T,*E,*t,*e;
    DdNode	*res;

    /* If we are past the deepest substitution, return f. */
    if (cuddI(dd,f->index) > deepest) {
	return(f);
    }

    if ((res = cuddHashTableLookup1(table,f)) != NULL) {
#ifdef DD_DEBUG
	addGeneralVectorComposeHits++;
#endif
	return(res);
    }

    /* Split and recur on children of this node. */
    T = cuddAddGeneralVectorComposeRecur(dd,table,cuddT(f),
					 vectorOn,vectorOff,deepest);
    if (T == NULL)  return(NULL);
    cuddRef(T);
    E = cuddAddGeneralVectorComposeRecur(dd,table,cuddE(f),
					 vectorOn,vectorOff,deepest);
    if (E == NULL) {
	Cudd_RecursiveDeref(dd, T);
	return(NULL);
    }
    cuddRef(E);

    /* Retrieve the compose ADDs for the current top variable and call
    ** cuddAddApplyRecur with the T and E we just created.
    */
    t = cuddAddApplyRecur(dd,Cudd_addTimes,vectorOn[f->index],T);
    if (t == NULL) {
      Cudd_RecursiveDeref(dd,T);
      Cudd_RecursiveDeref(dd,E);
      return(NULL);
    }
    cuddRef(t);
    e = cuddAddApplyRecur(dd,Cudd_addTimes,vectorOff[f->index],E);
    if (e == NULL) {
      Cudd_RecursiveDeref(dd,T);
      Cudd_RecursiveDeref(dd,E);
      Cudd_RecursiveDeref(dd,t);
      return(NULL);
    }
    cuddRef(e);
    res = cuddAddApplyRecur(dd,Cudd_addPlus,t,e);
    if (res == NULL) {
      Cudd_RecursiveDeref(dd,T);
      Cudd_RecursiveDeref(dd,E);
      Cudd_RecursiveDeref(dd,t);
      Cudd_RecursiveDeref(dd,e);
      return(NULL);
    }
    cuddRef(res);
    Cudd_RecursiveDeref(dd,T);
    Cudd_RecursiveDeref(dd,E);
    Cudd_RecursiveDeref(dd,t);
    Cudd_RecursiveDeref(dd,e);

    /* Do not keep the result if the reference count is only 1, since
    ** it will not be visited again
    */
    if (f->ref != 1) {
	ptrint fanout = (ptrint) f->ref;
	cuddSatDec(fanout);
	if (!cuddHashTableInsert1(table,f,res,fanout)) {
	    Cudd_RecursiveDeref(dd, res);
	    return(NULL);
	}
    }
    cuddDeref(res);
    return(res);

} /* end of cuddAddGeneralVectorComposeRecur */


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

  Synopsis    [Performs the recursive step of Cudd_addNonSimCompose.]

  Description []

  SideEffects [None]

  SeeAlso     []

******************************************************************************/
static DdNode *
cuddAddNonSimComposeRecur(
  DdManager * dd,
  DdNode * f,
  DdNode ** vector,
  DdNode * key,
  DdNode * cube,
  int  lastsub)
{
    DdNode *f1, *f0, *key1, *key0, *cube1, *var;
    DdNode *T,*E;
    DdNode *r;
    unsigned int top, topf, topk, topc;
    unsigned int index;
    int i;
    DdNode **vect1;
    DdNode **vect0;

    statLine(dd);
    /* If we are past the deepest substitution, return f. */
    if (cube == DD_ONE(dd) || cuddIsConstant(f)) {
	return(f);
    }

    /* If problem already solved, look up answer and return. */
    r = cuddCacheLookup(dd,DD_ADD_NON_SIM_COMPOSE_TAG,f,key,cube);
    if (r != NULL) {
	return(r);
    }

    /* Find top variable. we just need to look at f, key, and cube,
    ** because all the varibles in the gi are in key.
    */
    topf = cuddI(dd,f->index);
    topk = cuddI(dd,key->index);
    top = ddMin(topf,topk);
    topc = cuddI(dd,cube->index);
    top = ddMin(top,topc);
    index = dd->invperm[top];

    /* Compute the cofactors. */
    if (topf == top) {
	f1 = cuddT(f);
	f0 = cuddE(f);
    } else {
	f1 = f0 = f;
    }
    if (topc == top) {
	cube1 = cuddT(cube);
	/* We want to eliminate vector[index] from key. Otherwise
	** cache performance is severely affected. Hence we
	** existentially quantify the variable with index "index" from key.
	*/
	var = Cudd_addIthVar(dd, (int) index);
	if (var == NULL) {
	    return(NULL);
	}
	cuddRef(var);
	key1 = cuddAddExistAbstractRecur(dd, key, var);
	if (key1 == NULL) {
	    Cudd_RecursiveDeref(dd,var);
	    return(NULL);
	}
	cuddRef(key1);
	Cudd_RecursiveDeref(dd,var);
	key0 = key1;
    } else {
	cube1 = cube;
	if (topk == top) {
	    key1 = cuddT(key);
	    key0 = cuddE(key);
	} else {
	    key1 = key0 = key;
	}
	cuddRef(key1);
    }

    /* Allocate two new vectors for the cofactors of vector. */
    vect1 = ALLOC(DdNode *,lastsub);
    if (vect1 == NULL) {
	dd->errorCode = CUDD_MEMORY_OUT;
	Cudd_RecursiveDeref(dd,key1);
	return(NULL);
    }
    vect0 = ALLOC(DdNode *,lastsub);
    if (vect0 == NULL) {
	dd->errorCode = CUDD_MEMORY_OUT;
	Cudd_RecursiveDeref(dd,key1);
	FREE(vect1);
	return(NULL);
    }

    /* Cofactor the gi. Eliminate vect1[index] and vect0[index], because
    ** we do not need them.
    */
    for (i = 0; i < lastsub; i++) {
	DdNode *gi = vector[i];
	if (gi == NULL) {
	    vect1[i] = vect0[i] = NULL;
	} else if (gi->index == index) {
	    vect1[i] = cuddT(gi);
	    vect0[i] = cuddE(gi);
	} else {
	    vect1[i] = vect0[i] = gi;
	}
    }
    vect1[index] = vect0[index] = NULL;

    /* Recur on children. */
    T = cuddAddNonSimComposeRecur(dd,f1,vect1,key1,cube1,lastsub);
    FREE(vect1);
    if (T == NULL) {
	Cudd_RecursiveDeref(dd,key1);
	FREE(vect0);
	return(NULL);
    }
    cuddRef(T);
    E = cuddAddNonSimComposeRecur(dd,f0,vect0,key0,cube1,lastsub);
    FREE(vect0);
    if (E == NULL) {
	Cudd_RecursiveDeref(dd,key1);
	Cudd_RecursiveDeref(dd,T);
	return(NULL);
    }
    cuddRef(E);
    Cudd_RecursiveDeref(dd,key1);

    /* Retrieve the 0-1 ADD for the current top variable from vector,
    ** and call cuddAddIteRecur with the T and E we just created.
    */
    r = cuddAddIteRecur(dd,vector[index],T,E);
    if (r == NULL) {
	Cudd_RecursiveDeref(dd,T);
	Cudd_RecursiveDeref(dd,E);
	return(NULL);
    }
    cuddRef(r);
    Cudd_RecursiveDeref(dd,T);
    Cudd_RecursiveDeref(dd,E);
    cuddDeref(r);

    /* Store answer to trim recursion. */
    cuddCacheInsert(dd,DD_ADD_NON_SIM_COMPOSE_TAG,f,key,cube,r);

    return(r);

} /* end of cuddAddNonSimComposeRecur */


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

  Synopsis    [Performs the recursive step of Cudd_bddVectorCompose.]

  Description []

  SideEffects [None]

  SeeAlso     []

******************************************************************************/
static DdNode *
cuddBddVectorComposeRecur(
  DdManager * dd /* DD manager */,
  DdHashTable * table /* computed table */,
  DdNode * f /* BDD in which to compose */,
  DdNode ** vector /* functions to be composed */,
  int deepest /* depth of the deepest substitution */)
{
    DdNode	*F,*T,*E;
    DdNode	*res;

    statLine(dd);
    F = Cudd_Regular(f);

    /* If we are past the deepest substitution, return f. */
    if (cuddI(dd,F->index) > deepest) {
	return(f);
    }

    /* If problem already solved, look up answer and return. */
    if ((res = cuddHashTableLookup1(table,F)) != NULL) {
#ifdef DD_DEBUG
	bddVectorComposeHits++;
#endif
	return(Cudd_NotCond(res,F != f));
    }

    /* Split and recur on children of this node. */
    T = cuddBddVectorComposeRecur(dd,table,cuddT(F),vector, deepest);
    if (T == NULL) return(NULL);
    cuddRef(T);
    E = cuddBddVectorComposeRecur(dd,table,cuddE(F),vector, deepest);
    if (E == NULL) {
	Cudd_IterDerefBdd(dd, T);
	return(NULL);
    }
    cuddRef(E);

    /* Call cuddBddIteRecur with the BDD that replaces the current top
    ** variable and the T and E we just created.
    */
    res = cuddBddIteRecur(dd,vector[F->index],T,E);
    if (res == NULL) {
	Cudd_IterDerefBdd(dd, T);
	Cudd_IterDerefBdd(dd, E);
	return(NULL);
    }
    cuddRef(res);
    Cudd_IterDerefBdd(dd, T);
    Cudd_IterDerefBdd(dd, E);	

    /* Do not keep the result if the reference count is only 1, since
    ** it will not be visited again.
    */
    if (F->ref != 1) {
	ptrint fanout = (ptrint) F->ref;
	cuddSatDec(fanout);
	if (!cuddHashTableInsert1(table,F,res,fanout)) {
	    Cudd_IterDerefBdd(dd, res);
	    return(NULL);
	}
    }
    cuddDeref(res);
    return(Cudd_NotCond(res,F != f));

} /* end of cuddBddVectorComposeRecur */


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

  Synopsis    [Comparison of a function to the i-th ADD variable.]

  Description [Comparison of a function to the i-th ADD variable. Returns 1 if
  the function is the i-th ADD variable; 0 otherwise.]

  SideEffects [None]

  SeeAlso     []

******************************************************************************/
DD_INLINE
static int
ddIsIthAddVar(
  DdManager * dd,
  DdNode * f,
  unsigned int  i)
{
    return(f->index == i && cuddT(f) == DD_ONE(dd) && cuddE(f) == DD_ZERO(dd));

} /* end of ddIsIthAddVar */


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

  Synopsis    [Comparison of a pair of functions to the i-th ADD variable.]

  Description [Comparison of a pair of functions to the i-th ADD
  variable. Returns 1 if the functions are the i-th ADD variable and its
  complement; 0 otherwise.]

  SideEffects [None]

  SeeAlso     []

******************************************************************************/
DD_INLINE
static int
ddIsIthAddVarPair(
  DdManager * dd,
  DdNode * f,
  DdNode * g,
  unsigned int  i)
{
    return(f->index == i && g->index == i && 
	   cuddT(f) == DD_ONE(dd) && cuddE(f) == DD_ZERO(dd) &&
	   cuddT(g) == DD_ZERO(dd) && cuddE(g) == DD_ONE(dd));

} /* end of ddIsIthAddVarPair */