cuddcompose.c

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

/**CFile***********************************************************************

  FileName    [cuddCompose.c]

  PackageName [cudd]

  Synopsis    [Functional composition and variable permutation of DDs.]

  Description [External procedures included in this module:
		<ul>
		<li> Cudd_bddCompose()
		<li> Cudd_addCompose()
		<li> Cudd_addPermute()
		<li> Cudd_addSwapVariables()
		<li> Cudd_bddPermute()
		<li> Cudd_bddVarMap()
		<li> Cudd_SetVarMap()
		<li> Cudd_bddSwapVariables()
		<li> Cudd_bddAdjPermuteX()
		<li> Cudd_addVectorCompose()
		<li> Cudd_addGeneralVectorCompose()
		<li> Cudd_addNonSimCompose()
		<li> Cudd_bddVectorCompose()
		</ul>
	       Internal procedures included in this module:
		<ul>
		<li> cuddBddComposeRecur()
		<li> cuddAddComposeRecur()
		</ul>
	       Static procedures included in this module:
		<ul>
		<li> cuddAddPermuteRecur()
		<li> cuddBddPermuteRecur()
		<li> cuddBddVarMapRecur()
		<li> cuddAddVectorComposeRecur()
		<li> cuddAddGeneralVectorComposeRecur()
		<li> cuddAddNonSimComposeRecur()
		<li> cuddBddVectorComposeRecur()
		<li> ddIsIthAddVar()
		<li> ddIsIthAddVarPair()
	       </ul>
  The permutation functions use a local cache because the results to
  be remembered depend on the permutation being applied.  Since the
  permutation is just an array, it cannot be stored in the global
  cache. There are different procedured for BDDs and ADDs. This is
  because bddPermuteRecur uses cuddBddIteRecur. If this were changed,
  the procedures could be merged.]

  Author      [Fabio Somenzi and Kavita Ravi]

  Copyright   [This file was created at the University of Colorado at
  Boulder.  The University of Colorado at Boulder makes no warranty
  about the suitability of this software for any purpose.  It is
  presented on an AS IS basis.]

******************************************************************************/

#include "util.h"
#include "cuddInt.h"


/*---------------------------------------------------------------------------*/
/* Constant declarations                                                     */
/*---------------------------------------------------------------------------*/

/*---------------------------------------------------------------------------*/
/* Stucture declarations                                                     */
/*---------------------------------------------------------------------------*/

/*---------------------------------------------------------------------------*/
/* Type declarations                                                         */
/*---------------------------------------------------------------------------*/

/*---------------------------------------------------------------------------*/
/* Variable declarations                                                     */
/*---------------------------------------------------------------------------*/

#ifndef lint
static char rcsid[] DD_UNUSED = "$Id: cuddCompose.c,v 1.1.1.1 2003/02/24 22:23:51 wjiang Exp $";
#endif

#ifdef DD_DEBUG
static int addPermuteRecurHits;
static int bddPermuteRecurHits;
static int bddVectorComposeHits;
static int addVectorComposeHits;

static int addGeneralVectorComposeHits;
#endif

/*---------------------------------------------------------------------------*/
/* Macro declarations                                                        */
/*---------------------------------------------------------------------------*/


/**AutomaticStart*************************************************************/

/*---------------------------------------------------------------------------*/
/* Static function prototypes                                                */
/*---------------------------------------------------------------------------*/

static DdNode * cuddAddPermuteRecur ARGS((DdManager *manager, DdHashTable *table, DdNode *node, int *permut));
static DdNode * cuddBddPermuteRecur ARGS((DdManager *manager, DdHashTable *table, DdNode *node, int *permut));
static DdNode * cuddBddVarMapRecur ARGS((DdManager *manager, DdNode *f));
static DdNode * cuddAddVectorComposeRecur ARGS((DdManager *dd, DdHashTable *table, DdNode *f, DdNode **vector, int deepest));
static DdNode * cuddAddNonSimComposeRecur ARGS((DdManager *dd, DdNode *f, DdNode **vector, DdNode *key, DdNode *cube, int lastsub));
static DdNode * cuddBddVectorComposeRecur ARGS((DdManager *dd, DdHashTable *table, DdNode *f, DdNode **vector, int deepest));
DD_INLINE static int ddIsIthAddVar ARGS((DdManager *dd, DdNode *f, unsigned int i));

static DdNode * cuddAddGeneralVectorComposeRecur ARGS((DdManager *dd, DdHashTable *table, DdNode *f, DdNode **vectorOn, DdNode **vectorOff, int deepest));
DD_INLINE static int ddIsIthAddVarPair ARGS((DdManager *dd, DdNode *f, DdNode *g, unsigned int i));

/**AutomaticEnd***************************************************************/


/*---------------------------------------------------------------------------*/
/* Definition of exported functions                                          */
/*---------------------------------------------------------------------------*/


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

  Synopsis    [Substitutes g for x_v in the BDD for f.]

  Description [Substitutes g for x_v in the BDD for f. v is the index of the
  variable to be substituted. Cudd_bddCompose passes the corresponding
  projection function to the recursive procedure, so that the cache may
  be used.  Returns the composed BDD if successful; NULL otherwise.]

  SideEffects [None]

  SeeAlso     [Cudd_addCompose]

******************************************************************************/
DdNode *
Cudd_bddCompose(
  DdManager * dd,
  DdNode * f,
  DdNode * g,
  int  v)
{
    DdNode *proj, *res;

    /* Sanity check. */
    if (v < 0 || v > dd->size) return(NULL);

    proj =  dd->vars[v];
    do {
	dd->reordered = 0;
	res = cuddBddComposeRecur(dd,f,g,proj);
    } while (dd->reordered == 1);
    return(res);

} /* end of Cudd_bddCompose */


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

  Synopsis    [Substitutes g for x_v in the ADD for f.]

  Description [Substitutes g for x_v in the ADD for f. v is the index of the
  variable to be substituted. g must be a 0-1 ADD. Cudd_bddCompose passes
  the corresponding projection function to the recursive procedure, so
  that the cache may be used.  Returns the composed ADD if successful;
  NULL otherwise.]

  SideEffects [None]

  SeeAlso     [Cudd_bddCompose]

******************************************************************************/
DdNode *
Cudd_addCompose(
  DdManager * dd,
  DdNode * f,
  DdNode * g,
  int  v)
{
    DdNode *proj, *res;

    /* Sanity check. */
    if (v < 0 || v > dd->size) return(NULL);

    proj =  dd->vars[v];
    do {
	dd->reordered = 0;
	res = cuddAddComposeRecur(dd,f,g,proj);
    } while (dd->reordered == 1);
    return(res);

} /* end of Cudd_addCompose */


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

  Synopsis    [Permutes the variables of an ADD.]

  Description [Given a permutation in array permut, creates a new ADD
  with permuted variables. There should be an entry in array permut
  for each variable in the manager. The i-th entry of permut holds the
  index of the variable that is to substitute the i-th
  variable. Returns a pointer to the resulting ADD if successful; NULL
  otherwise.]

  SideEffects [None]

  SeeAlso     [Cudd_bddPermute Cudd_addSwapVariables]

******************************************************************************/
DdNode *
Cudd_addPermute(
  DdManager * manager,
  DdNode * node,
  int * permut)
{
    DdHashTable		*table;
    DdNode		*res;

    do {
	manager->reordered = 0;
	table = cuddHashTableInit(manager,1,2);
	if (table == NULL) return(NULL);
	/* Recursively solve the problem. */
	res = cuddAddPermuteRecur(manager,table,node,permut);
	if (res != NULL) cuddRef(res);
	/* Dispose of local cache. */
	cuddHashTableQuit(table);
    } while (manager->reordered == 1);

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

} /* end of Cudd_addPermute */


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

  Synopsis [Swaps two sets of variables of the same size (x and y) in
  the ADD f.]

  Description [Swaps two sets of variables of the same size (x and y) in
  the ADD f.  The size is given by n. The two sets of variables are
  assumed to be disjoint. Returns a pointer to the resulting ADD if
  successful; NULL otherwise.]

  SideEffects [None]

  SeeAlso     [Cudd_addPermute Cudd_bddSwapVariables]

******************************************************************************/
DdNode *
Cudd_addSwapVariables(
  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_addPermute(dd,f,permut);
    FREE(permut);

    return(swapped);

} /* end of Cudd_addSwapVariables */


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

  Synopsis    [Permutes the variables of a BDD.]

  Description [Given a permutation in array permut, creates a new BDD
  with permuted variables. There should be an entry in array permut
  for each variable in the manager. The i-th entry of permut holds the
  index of the variable that is to substitute the i-th variable.
  Returns a pointer to the resulting BDD if successful; NULL
  otherwise.]

  SideEffects [None]

  SeeAlso     [Cudd_addPermute Cudd_bddSwapVariables]

******************************************************************************/
DdNode *
Cudd_bddPermute(
  DdManager * manager,
  DdNode * node,
  int * permut)
{
    DdHashTable		*table;
    DdNode		*res;

    do {
	manager->reordered = 0;
	table = cuddHashTableInit(manager,1,2);
	if (table == NULL) return(NULL);
	res = cuddBddPermuteRecur(manager,table,node,permut);
	if (res != NULL) cuddRef(res);
	/* Dispose of local cache. */
	cuddHashTableQuit(table);

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

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

} /* end of Cudd_bddPermute */


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

  Synopsis    [Remaps the variables of a BDD using the default variable map.]

  Description [Remaps the variables of a BDD using the default
  variable map.  A typical use of this function is to swap two sets of
  variables.  The variable map must be registered with Cudd_SetVarMap.
  Returns a pointer to the resulting BDD if successful; NULL
  otherwise.]

  SideEffects [None]

  SeeAlso     [Cudd_bddPermute Cudd_bddSwapVariables Cudd_SetVarMap]

******************************************************************************/
DdNode *
Cudd_bddVarMap(
  DdManager * manager /* DD manager */,
  DdNode * f /* function in which to remap variables */)
{
    DdNode *res;

    if (manager->map == NULL) return(NULL);
    do {
	manager->reordered = 0;
	res = cuddBddVarMapRecur(manager, f);
    } while (manager->reordered == 1);

    return(res);

} /* end of Cudd_bddVarMap */


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

  Synopsis [Registers a variable mapping with the manager.]

  Description [Registers with the manager a variable mapping described
  by two sets of variables.  This variable mapping is then used by
  functions like Cudd_bddVarMap.  This function is convenient for
  those applications that perform the same mapping several times.
  However, if several different permutations are used, it may be more
  efficient not to rely on the registered mapping, because changing
  mapping causes the cache to be cleared.  (The initial setting,
  however, does not clear the cache.) The two sets of variables (x and
  y) must have the same size (x and y).  The size is given by n. The
  two sets of variables are normally disjoint, but this restriction is
  not imposeded by the function. When new variables are created, the
  map is automatically extended (each new variable maps to
  itself). The typical use, however, is to wait until all variables
  are created, and then create the map.  Returns 1 if the mapping is
  successfully registered with the manager; 0 otherwise.]

  SideEffects [Modifies the manager. May clear the cache.]

  SeeAlso     [Cudd_bddVarMap Cudd_bddPermute Cudd_bddSwapVariables]

******************************************************************************/
int
Cudd_SetVarMap (
  DdManager *manager /* DD manager */,
  DdNode **x /* first array of variables */,
  DdNode **y /* second array of variables */,
  int n /* length of both arrays */)
{
    int i;

    if (manager->map != NULL) {
	cuddCacheFlush(manager);
    } else {
	manager->map = ALLOC(int,manager->maxSize);
	if (manager->map == NULL) {
	    manager->errorCode = CUDD_MEMORY_OUT;
	    return(0);
	}
	manager->memused += sizeof(int) * manager->maxSize;
    }
    /* Initialize the map to the identity. */
    for (i = 0; i < manager->size; i++) {
	manager->map[i] = i;
    }
    /* Create the map. */
    for (i = 0; i < n; i++) {
	manager->map[x[i]->index] = y[i]->index;
	manager->map[y[i]->index] = x[i]->index;
    }
    return(1);

} /* end of Cudd_SetVarMap */


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

  Synopsis [Swaps two sets of variables of the same size (x and y) in
  the BDD f.]

  Description [Swaps two sets of variables of the same size (x and y)
  in the BDD f. The size is given by n. The two sets of variables are
  assumed to be disjoint.  Returns a pointer to the resulting BDD if
  successful; NULL otherwise.]

  SideEffects [None]

  SeeAlso     [Cudd_bddPermute Cudd_addSwapVariables]

******************************************************************************/