cuddexact.c

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

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

  FileName    [cuddExact.c]

  PackageName [cudd]

  Synopsis    [Functions for exact variable reordering.]

  Description [External procedures included in this file:
		<ul>
		</ul>
	Internal procedures included in this module:
		<ul>
		<li> cuddExact()
		</ul>
	Static procedures included in this module:
		<ul> 
                <li> getMaxBinomial()
		<li> gcd()
                <li> getMatrix()
		<li> freeMatrix()
                <li> getLevelKeys()
                <li> ddShuffle()
                <li> ddSiftUp()
		<li> updateUB()
		<li> ddCountRoots()
		<li> ddClearGlobal()
		<li> computeLB()
		<li> updateEntry()
		<li> pushDown()
		<li> initSymmInfo()
                </ul>]

  Author      [Cheng Hua, Fabio Somenzi]

  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: cuddExact.c,v 1.1.1.1 2003/02/24 22:23:52 wjiang Exp $";
#endif

#ifdef DD_STATS
static int ddTotalShuffles;
#endif

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

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

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

static int getMaxBinomial ARGS((int n));
static int gcd ARGS((int x, int y));
static DdHalfWord ** getMatrix ARGS((int rows, int cols));
static void freeMatrix ARGS((DdHalfWord **matrix));
static int getLevelKeys ARGS((DdManager *table, int l));
static int ddShuffle ARGS((DdManager *table, DdHalfWord *permutation, int lower, int upper));
static int ddSiftUp ARGS((DdManager *table, int x, int xLow));
static int updateUB ARGS((DdManager *table, int oldBound, DdHalfWord *bestOrder, int lower, int upper));
static int ddCountRoots ARGS((DdManager *table, int lower, int upper));
static void ddClearGlobal ARGS((DdManager *table, int lower, int maxlevel));
static int computeLB ARGS((DdManager *table, DdHalfWord *order, int roots, int cost, int lower, int upper, int level));
static int updateEntry ARGS((DdManager *table, DdHalfWord *order, int level, int cost, DdHalfWord **orders, int *costs, int subsets, char *mask, int lower, int upper));
static void pushDown ARGS((DdHalfWord *order, int j, int level));
static DdHalfWord * initSymmInfo ARGS((DdManager *table, int lower, int upper));
static int checkSymmInfo ARGS((DdManager *table, DdHalfWord *symmInfo, int index, int level));

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


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

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


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

  Synopsis    [Exact variable ordering algorithm.]

  Description [Exact variable ordering algorithm. Finds an optimum
  order for the variables between lower and upper.  Returns 1 if
  successful; 0 otherwise.]

  SideEffects [None]

  SeeAlso     []

******************************************************************************/
int
cuddExact(
  DdManager * table,
  int  lower,
  int  upper)
{
    int k, i, j;
    int maxBinomial, oldSubsets, newSubsets;
    int subsetCost;
    int size;			/* number of variables to be reordered */
    int unused, nvars, level, result;
    int upperBound, lowerBound, cost;
    int roots;
    char *mask = NULL;
    DdHalfWord  *symmInfo = NULL;
    DdHalfWord **newOrder = NULL;
    DdHalfWord **oldOrder = NULL;
    int *newCost = NULL;
    int *oldCost = NULL;
    DdHalfWord **tmpOrder;
    int *tmpCost;
    DdHalfWord *bestOrder = NULL;
    DdHalfWord *order;
#ifdef DD_STATS
    int  ddTotalSubsets;
#endif

    /* Restrict the range to be reordered by excluding unused variables
    ** at the two ends. */
    while (table->subtables[lower].keys == 1 &&
	   table->vars[table->invperm[lower]]->ref == 1 &&
	   lower < upper)
	lower++;
    while (table->subtables[upper].keys == 1 &&
	   table->vars[table->invperm[upper]]->ref == 1 &&
	   lower < upper)
	upper--;
    if (lower == upper) return(1); /* trivial problem */

    /* Apply symmetric sifting to get a good upper bound and to extract
    ** symmetry information. */
    result = cuddSymmSiftingConv(table,lower,upper);
    if (result == 0) goto cuddExactOutOfMem;

#ifdef DD_STATS
    (void) fprintf(table->out,"\n");
    ddTotalShuffles = 0;
    ddTotalSubsets = 0;
#endif

    /* Initialization. */
    nvars = table->size;
    size = upper - lower + 1;
    /* Count unused variable among those to be reordered.  This is only
    ** used to compute maxBinomial. */
    unused = 0;
    for (i = lower + 1; i < upper; i++) {
	if (table->subtables[i].keys == 1 &&
	    table->vars[table->invperm[i]]->ref == 1)
	    unused++;
    }

    /* Find the maximum number of subsets we may have to store. */
    maxBinomial = getMaxBinomial(size - unused);
    if (maxBinomial == -1) goto cuddExactOutOfMem;

    newOrder = getMatrix(maxBinomial, size);
    if (newOrder == NULL) goto cuddExactOutOfMem;

    newCost = ALLOC(int, maxBinomial);
    if (newCost == NULL) goto cuddExactOutOfMem;

    oldOrder = getMatrix(maxBinomial, size);
    if (oldOrder == NULL) goto cuddExactOutOfMem;

    oldCost = ALLOC(int, maxBinomial);
    if (oldCost == NULL) goto cuddExactOutOfMem;

    bestOrder = ALLOC(DdHalfWord, size);
    if (bestOrder == NULL) goto cuddExactOutOfMem;

    mask = ALLOC(char, nvars);
    if (mask == NULL) goto cuddExactOutOfMem;

    symmInfo = initSymmInfo(table, lower, upper);
    if (symmInfo == NULL) goto cuddExactOutOfMem;

    roots = ddCountRoots(table, lower, upper);

    /* Initialize the old order matrix for the empty subset and the best
    ** order to the current order. The cost for the empty subset includes
    ** the cost of the levels between upper and the constants. These levels
    ** are not going to change. Hence, we count them only once.
    */
    oldSubsets = 1;
    for (i = 0; i < size; i++) {
	oldOrder[0][i] = bestOrder[i] = (DdHalfWord) table->invperm[i+lower];
    }
    subsetCost = table->constants.keys;
    for (i = upper + 1; i < nvars; i++)
	subsetCost += getLevelKeys(table,i);
    oldCost[0] = subsetCost;
    /* The upper bound is initialized to the current size of the BDDs. */
    upperBound = table->keys - table->isolated;

    /* Now consider subsets of increasing size. */
    for (k = 1; k <= size; k++) {
#if DD_STATS
	(void) fprintf(table->out,"Processing subsets of size %d\n", k);
	fflush(table->out);
#endif
	newSubsets = 0;
	level = size - k;		/* offset of first bottom variable */

	for (i = 0; i < oldSubsets; i++) { /* for each subset of size k-1 */
	    order = oldOrder[i];
	    cost = oldCost[i];
	    lowerBound = computeLB(table, order, roots, cost, lower, upper,
				   level);
	    if (lowerBound >= upperBound)
		continue;
	    /* Impose new order. */
	    result = ddShuffle(table, order, lower, upper);
	    if (result == 0) goto cuddExactOutOfMem;
	    upperBound = updateUB(table,upperBound,bestOrder,lower,upper);
	    /* For each top bottom variable. */
	    for (j = level; j >= 0; j--) {
		/* Skip unused variables. */
		if (table->subtables[j+lower-1].keys == 1 &&
		    table->vars[table->invperm[j+lower-1]]->ref == 1) continue;
		/* Find cost under this order. */
		subsetCost = cost + getLevelKeys(table, lower + level);
		newSubsets = updateEntry(table, order, level, subsetCost,
					 newOrder, newCost, newSubsets, mask,
					 lower, upper);
		if (j == 0)
		    break;
		if (checkSymmInfo(table, symmInfo, order[j-1], level) == 0)
		    continue;
		pushDown(order,j-1,level);
		/* Impose new order. */
		result = ddShuffle(table, order, lower, upper);
		if (result == 0) goto cuddExactOutOfMem;
		upperBound = updateUB(table,upperBound,bestOrder,lower,upper);
	    } /* for each bottom variable */
	} /* for each subset of size k */

	/* New orders become old orders in preparation for next iteration. */
	tmpOrder = oldOrder; tmpCost = oldCost;
	oldOrder = newOrder; oldCost = newCost;
	newOrder = tmpOrder; newCost = tmpCost;
#ifdef DD_STATS
	ddTotalSubsets += newSubsets;
#endif
	oldSubsets = newSubsets;
    }
    result = ddShuffle(table, bestOrder, lower, upper);
    if (result == 0) goto cuddExactOutOfMem;
#ifdef DD_STATS
#ifdef DD_VERBOSE
    (void) fprintf(table->out,"\n");
#endif
    (void) fprintf(table->out,"#:S_EXACT   %8d: total subsets\n",
		   ddTotalSubsets);
    (void) fprintf(table->out,"#:H_EXACT   %8d: total shuffles",
		   ddTotalShuffles);
#endif

    freeMatrix(newOrder);
    freeMatrix(oldOrder);
    FREE(bestOrder);
    FREE(oldCost);
    FREE(newCost);
    FREE(symmInfo);
    FREE(mask);
    return(1);

cuddExactOutOfMem:

    if (newOrder != NULL) freeMatrix(newOrder);
    if (oldOrder != NULL) freeMatrix(oldOrder);
    if (bestOrder != NULL) FREE(bestOrder);
    if (oldCost != NULL) FREE(oldCost);
    if (newCost != NULL) FREE(newCost);
    if (symmInfo != NULL) FREE(symmInfo);
    if (mask != NULL) FREE(mask);
    table->errorCode = CUDD_MEMORY_OUT;
    return(0);

} /* end of cuddExact */


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

  Synopsis    [Returns the maximum value of (n choose k) for a given n.]

  Description [Computes the maximum value of (n choose k) for a given
  n.  The maximum value occurs for k = n/2 when n is even, or k =
  (n-1)/2 when n is odd.  The algorithm used in this procedure is
  quite inefficient, but it avoids intermediate overflow problems.
  Returns the computed value if successful; -1 otherwise.]

  SideEffects [None]

  SeeAlso     []

******************************************************************************/
static int
getMaxBinomial(
  int  n)
{
    int *numerator;
    int i, j, k, y, g, result;

    k = (n & ~1) >> 1;

    numerator = ALLOC(int,k);
    if (numerator == NULL) return(-1);
    
    for (i = 0; i < k; i++)
	numerator[i] = n - i;
    
    for (i = k; i > 1; i--) {
	y = i;
	for (j = 0; j < k; j++) {
	    if (numerator[j] == 1) continue;
	    g = gcd(numerator[j], y);
	    if (g != 1) {
		numerator[j] /= g;
		if (y == g) break;
		y /= g;
	    }
	}
    }

    result = 1;
    for (i = 0; i < k; i++)
	result *= numerator[i];

    FREE(numerator);
    return(result);

}  /* end of getMaxBinomial */


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

  Synopsis    [Returns the gcd of two integers.]

  Description [Returns the gcd of two integers. Uses the binary GCD
  algorithm described in Cormen, Leiserson, and Rivest.]

  SideEffects [None]

  SeeAlso     []

******************************************************************************/
static int
gcd(
  int  x,
  int  y)
{
    int a;
    int b;
    int lsbMask;

    /* GCD(n,0) = n. */
    if (x == 0) return(y);
    if (y == 0) return(x);

    a = x; b = y; lsbMask = 1;
    
    /* Here both a and b are != 0. The iteration maintains this invariant.
    ** Hence, we only need to check for when they become equal.
    */
    while (a != b) {
	if (a & lsbMask) {
	    if (b & lsbMask) {	/* both odd */
		if (a < b) {
		    b = (b - a) >> 1;
		} else {
		    a = (a - b) >> 1;
		}
	    } else {		/* a odd, b even */
		b >>= 1;
	    }
	} else {
	    if (b & lsbMask) {	/* a even, b odd */
		a >>= 1;
	    } else {		/* both even */
		lsbMask <<= 1;
	    }
	}
    }

    return(a);

} /* end of gcd */


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

  Synopsis    [Allocates a two-dimensional matrix of ints.]

  Description [Allocates a two-dimensional matrix of ints.
  Returns the pointer to the matrix if successful; NULL otherwise.]

  SideEffects [None]

  SeeAlso     [freeMatrix]

******************************************************************************/
static DdHalfWord **
getMatrix(
  int  rows /* number of rows */,
  int  cols /* number of columns */)
{
    DdHalfWord **matrix;
    int i;

    if (cols*rows == 0) return(NULL);
    matrix = ALLOC(DdHalfWord *, rows);
    if (matrix == NULL) return(NULL);
    matrix[0] = ALLOC(DdHalfWord, cols*rows);
    if (matrix[0] == NULL) return(NULL);
    for (i = 1; i < rows; i++) {
	matrix[i] = matrix[i-1] + cols;
    }
    return(matrix);

} /* end of getMatrix */


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

  Synopsis    [Frees a two-dimensional matrix allocated by getMatrix.]

  Description []

  SideEffects [None]

  SeeAlso     [getMatrix]

******************************************************************************/
static void
freeMatrix(
  DdHalfWord ** matrix)
{
    FREE(matrix[0]);
    FREE(matrix);
    return;

} /* end of freeMatrix */


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

  Synopsis    [Returns the number of nodes at one level of a unique table.]

  Description [Returns the number of nodes at one level of a unique table.
  The projection function, if isolated, is not counted.]

  SideEffects [None]

  SeeAlso []

******************************************************************************/
static int
getLevelKeys(
  DdManager * table,
  int  l)
{
    int isolated;
    int x;        /* x is an index */

    x = table->invperm[l];
    isolated = table->vars[x]->ref == 1;

    return(table->subtables[l].keys - isolated);

} /* end of getLevelKeys */