cuddcompose.c

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

DdNode *
Cudd_bddSwapVariables(
  DdManager * dd,
  DdNode * f,
  DdNode ** x,
  DdNode ** y,
  int  n)
{
    DdNode *swapped;
    int	 i, j, k;
    int	 *permut;

    permut = ALLOC(int,dd->size);
    if (permut == NULL) {
	dd->errorCode = CUDD_MEMORY_OUT;
	return(NULL);
    }
    for (i = 0; i < dd->size; i++) permut[i] = i;
    for (i = 0; i < n; i++) {
	j = x[i]->index;
	k = y[i]->index;
	permut[j] = k;
	permut[k] = j;
    }

    swapped = Cudd_bddPermute(dd,f,permut);
    FREE(permut);

    return(swapped);

} /* end of Cudd_bddSwapVariables */


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

  Synopsis [Rearranges a set of variables in the BDD B.]

  Description [Rearranges a set of variables in the BDD B. The size of
  the set is given by n. This procedure is intended for the
  `randomization' of the priority functions. Returns a pointer to the
  BDD if successful; NULL otherwise.]

  SideEffects [None]

  SeeAlso     [Cudd_bddPermute Cudd_bddSwapVariables
  Cudd_Dxygtdxz Cudd_Dxygtdyz Cudd_PrioritySelect]

******************************************************************************/
DdNode *
Cudd_bddAdjPermuteX(
  DdManager * dd,
  DdNode * B,
  DdNode ** x,
  int  n)
{
    DdNode *swapped;
    int	 i, j, k;
    int	 *permut;

    permut = ALLOC(int,dd->size);
    if (permut == NULL) {
	dd->errorCode = CUDD_MEMORY_OUT;
	return(NULL);
    }
    for (i = 0; i < dd->size; i++) permut[i] = i;
    for (i = 0; i < n-2; i += 3) {
	j = x[i]->index;
	k = x[i+1]->index;
	permut[j] = k;
	permut[k] = j;
    }

    swapped = Cudd_bddPermute(dd,B,permut);
    FREE(permut);

    return(swapped);

} /* end of Cudd_bddAdjPermuteX */


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

  Synopsis    [Composes an ADD with a vector of 0-1 ADDs.]

  Description [Given a vector of 0-1 ADDs, creates a new ADD by
  substituting the 0-1 ADDs for the variables of the ADD f.  There
  should be an entry in vector for each variable in the manager.
  If no substitution is sought for a given variable, the corresponding
  projection function should be specified in the vector.
  This function implements simultaneous composition.
  Returns a pointer to the resulting ADD if successful; NULL
  otherwise.]

  SideEffects [None]

  SeeAlso     [Cudd_addNonSimCompose Cudd_addPermute Cudd_addCompose
  Cudd_bddVectorCompose]

******************************************************************************/
DdNode *
Cudd_addVectorCompose(
  DdManager * dd,
  DdNode * f,
  DdNode ** vector)
{
    DdHashTable		*table;
    DdNode		*res;
    int			deepest;
    int                 i;

    do {
	dd->reordered = 0;
	/* Initialize local cache. */
	table = cuddHashTableInit(dd,1,2);
	if (table == NULL) return(NULL);

	/* Find deepest real substitution. */
	for (deepest = dd->size - 1; deepest >= 0; deepest--) {
	    i = dd->invperm[deepest];
	    if (!ddIsIthAddVar(dd,vector[i],i)) {
		break;
	    }
	}

	/* Recursively solve the problem. */
	res = cuddAddVectorComposeRecur(dd,table,f,vector,deepest);
	if (res != NULL) cuddRef(res);

	/* Dispose of local cache. */
	cuddHashTableQuit(table);
    } while (dd->reordered == 1);

    if (res != NULL) cuddDeref(res);
    return(res);

} /* end of Cudd_addVectorCompose */


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

  Synopsis    [Composes an ADD with a vector of ADDs.]

  Description [Given a vector of ADDs, creates a new ADD by substituting the
  ADDs for the variables of the ADD f. vectorOn contains ADDs to be substituted
  for the x_v and vectorOff the ADDs to be substituted for x_v'. There should
  be an entry in vector for each variable in the manager.  If no substitution
  is sought for a given variable, the corresponding projection function should
  be specified in the vector.  This function implements simultaneous
  composition.  Returns a pointer to the resulting ADD if successful; NULL
  otherwise.]

  SideEffects [None]

  SeeAlso [Cudd_addVectorCompose Cudd_addNonSimCompose Cudd_addPermute
  Cudd_addCompose Cudd_bddVectorCompose]

******************************************************************************/
DdNode *
Cudd_addGeneralVectorCompose(
  DdManager * dd,
  DdNode * f,
  DdNode ** vectorOn,
  DdNode ** vectorOff)
{
    DdHashTable		*table;
    DdNode		*res;
    int			deepest;
    int                 i;

    do {
	dd->reordered = 0;
	/* Initialize local cache. */
	table = cuddHashTableInit(dd,1,2);
	if (table == NULL) return(NULL);

	/* Find deepest real substitution. */
	for (deepest = dd->size - 1; deepest >= 0; deepest--) {
	    i = dd->invperm[deepest];
	    if (!ddIsIthAddVarPair(dd,vectorOn[i],vectorOff[i],i)) {
		break;
	    }
	}

	/* Recursively solve the problem. */
	res = cuddAddGeneralVectorComposeRecur(dd,table,f,vectorOn,
					       vectorOff,deepest);
	if (res != NULL) cuddRef(res);

	/* Dispose of local cache. */
	cuddHashTableQuit(table);
    } while (dd->reordered == 1);

    if (res != NULL) cuddDeref(res);
    return(res);

} /* end of Cudd_addGeneralVectorCompose */


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

  Synopsis    [Composes an ADD with a vector of 0-1 ADDs.]

  Description [Given a vector of 0-1 ADDs, creates a new ADD by
  substituting the 0-1 ADDs for the variables of the ADD f.  There
  should be an entry in vector for each variable in the manager.
  This function implements non-simultaneous composition. If any of the
  functions being composed depends on any of the variables being
  substituted, then the result depends on the order of composition,
  which in turn depends on the variable order: The variables farther from
  the roots in the order are substituted first.
  Returns a pointer to the resulting ADD if successful; NULL
  otherwise.]

  SideEffects [None]

  SeeAlso     [Cudd_addVectorCompose Cudd_addPermute Cudd_addCompose]

******************************************************************************/
DdNode *
Cudd_addNonSimCompose(
  DdManager * dd,
  DdNode * f,
  DdNode ** vector)
{
    DdNode		*cube, *key, *var, *tmp, *piece;
    DdNode		*res;
    int			i, lastsub;

    /* The cache entry for this function is composed of three parts:
    ** f itself, the replacement relation, and the cube of the
    ** variables being substituted.
    ** The replacement relation is the product of the terms (yi EXNOR gi).
    ** This apporach allows us to use the global cache for this function,
    ** with great savings in memory with respect to using arrays for the
    ** cache entries.
    ** First we build replacement relation and cube of substituted
    ** variables from the vector specifying the desired composition.
    */
    key = DD_ONE(dd);
    cuddRef(key);
    cube = DD_ONE(dd);
    cuddRef(cube);
    for (i = (int) dd->size - 1; i >= 0; i--) {
	if (ddIsIthAddVar(dd,vector[i],(unsigned int)i)) {
	    continue;
	}
	var = Cudd_addIthVar(dd,i);
	if (var == NULL) {
	    Cudd_RecursiveDeref(dd,key);
	    Cudd_RecursiveDeref(dd,cube);
	    return(NULL);
	}
	cuddRef(var);
	/* Update cube. */
	tmp = Cudd_addApply(dd,Cudd_addTimes,var,cube);
	if (tmp == NULL) {
	    Cudd_RecursiveDeref(dd,key);
	    Cudd_RecursiveDeref(dd,cube);
	    Cudd_RecursiveDeref(dd,var);
	    return(NULL);
	}
	cuddRef(tmp);
	Cudd_RecursiveDeref(dd,cube);
	cube = tmp;
	/* Update replacement relation. */
	piece = Cudd_addApply(dd,Cudd_addXnor,var,vector[i]);
	if (piece == NULL) {
	    Cudd_RecursiveDeref(dd,key);
	    Cudd_RecursiveDeref(dd,var);
	    return(NULL);
	}
	cuddRef(piece);
	Cudd_RecursiveDeref(dd,var);
	tmp = Cudd_addApply(dd,Cudd_addTimes,key,piece);
	if (tmp == NULL) {
	    Cudd_RecursiveDeref(dd,key);
	    Cudd_RecursiveDeref(dd,piece);
	    return(NULL);
	}
	cuddRef(tmp);
	Cudd_RecursiveDeref(dd,key);
	Cudd_RecursiveDeref(dd,piece);
	key = tmp;
    }

    /* Now try composition, until no reordering occurs. */
    do {
	/* Find real substitution with largest index. */
	for (lastsub = dd->size - 1; lastsub >= 0; lastsub--) {
	    if (!ddIsIthAddVar(dd,vector[lastsub],(unsigned int)lastsub)) {
		break;
	    }
	}

	/* Recursively solve the problem. */
	dd->reordered = 0;
	res = cuddAddNonSimComposeRecur(dd,f,vector,key,cube,lastsub+1);
	if (res != NULL) cuddRef(res);

    } while (dd->reordered == 1);

    Cudd_RecursiveDeref(dd,key);
    Cudd_RecursiveDeref(dd,cube);
    if (res != NULL) cuddDeref(res);
    return(res);

} /* end of Cudd_addNonSimCompose */


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

  Synopsis    [Composes a BDD with a vector of BDDs.]

  Description [Given a vector of BDDs, creates a new BDD by
  substituting the BDDs for the variables of the BDD f.  There
  should be an entry in vector for each variable in the manager.
  If no substitution is sought for a given variable, the corresponding
  projection function should be specified in the vector.
  This function implements simultaneous composition.
  Returns a pointer to the resulting BDD if successful; NULL
  otherwise.]

  SideEffects [None]

  SeeAlso     [Cudd_bddPermute Cudd_bddCompose Cudd_addVectorCompose]

******************************************************************************/
DdNode *
Cudd_bddVectorCompose(
  DdManager * dd,
  DdNode * f,
  DdNode ** vector)
{
    DdHashTable		*table;
    DdNode		*res;
    int			deepest;
    int                 i;

    do {
	dd->reordered = 0;
	/* Initialize local cache. */
	table = cuddHashTableInit(dd,1,2);
	if (table == NULL) return(NULL);

	/* Find deepest real substitution. */
	for (deepest = dd->size - 1; deepest >= 0; deepest--) {
	    i = dd->invperm[deepest];
	    if (vector[i] != dd->vars[i]) {
		break;
	    }
	}

	/* Recursively solve the problem. */
	res = cuddBddVectorComposeRecur(dd,table,f,vector, deepest);
	if (res != NULL) cuddRef(res);

	/* Dispose of local cache. */
	cuddHashTableQuit(table);
    } while (dd->reordered == 1);

    if (res != NULL) cuddDeref(res);
    return(res);

} /* end of Cudd_bddVectorCompose */


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


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

  Synopsis    [Performs the recursive step of Cudd_bddCompose.]

  Description [Performs the recursive step of Cudd_bddCompose.
  Exploits the fact that the composition of f' with g
  produces the complement of the composition of f with g to better
  utilize the cache.  Returns the composed BDD if successful; NULL
  otherwise.]

  SideEffects [None]

  SeeAlso     [Cudd_bddCompose]

******************************************************************************/
DdNode *
cuddBddComposeRecur(
  DdManager * dd,
  DdNode * f,
  DdNode * g,
  DdNode * proj)
{
    DdNode	*F, *G, *f1, *f0, *g1, *g0, *r, *t, *e;
    unsigned int v, topf, topg, topindex;
    int		comple;

    statLine(dd);
    v = dd->perm[proj->index];
    F = Cudd_Regular(f);
    topf = cuddI(dd,F->index);

    /* Terminal case. Subsumes the test for constant f. */
    if (topf > v) return(f);

    /* We solve the problem for a regular pointer, and then complement
    ** the result if the pointer was originally complemented.
    */
    comple = Cudd_IsComplement(f);

    /* Check cache. */
    r = cuddCacheLookup(dd,DD_BDD_COMPOSE_RECUR_TAG,F,g,proj);
    if (r != NULL) {
	return(Cudd_NotCond(r,comple));
    }

    if (topf == v) {
	/* Compose. */
	f1 = cuddT(F);
	f0 = cuddE(F);
	r = cuddBddIteRecur(dd, g, f1, f0);
	if (r == NULL) return(NULL);
    } else {
	/* Compute cofactors of f and g. Remember the index of the top
	** variable.
	*/
	G = Cudd_Regular(g);
	topg = cuddI(dd,G->index);
	if (topf > topg) {
	    topindex = G->index;
	    f1 = f0 = F;