cuddzddlin.c

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

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

  FileName    [cuddZddLin.c]

  PackageName [cudd]

  Synopsis    [Procedures for dynamic variable ordering of ZDDs.]

  Description [Internal procedures included in this module:
		    <ul>
		    <li> cuddZddLinearSifting()
		    </ul>
	       Static procedures included in this module:
		    <ul>
		    <li> cuddZddLinearInPlace()
		    <li> cuddZddLinerAux()
		    <li> cuddZddLinearUp()
		    <li> cuddZddLinearDown()
		    <li> cuddZddLinearBackward()
		    <li> cuddZddUndoMoves()
		    </ul>
	      ]

  SeeAlso     [cuddLinear.c cuddZddReord.c]

  Author      [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                                                     */
/*---------------------------------------------------------------------------*/

#define CUDD_SWAP_MOVE 0
#define CUDD_LINEAR_TRANSFORM_MOVE 1
#define CUDD_INVERSE_TRANSFORM_MOVE 2

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


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


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

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

extern  int	*zdd_entry;
extern	int	zddTotalNumberSwapping;
static	int	zddTotalNumberLinearTr;
static  DdNode	*empty;


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


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

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

static int cuddZddLinearAux ARGS((DdManager *table, int x, int xLow, int xHigh));
static Move * cuddZddLinearUp ARGS((DdManager *table, int y, int xLow, Move *prevMoves));
static Move * cuddZddLinearDown ARGS((DdManager *table, int x, int xHigh, Move *prevMoves));
static int cuddZddLinearBackward ARGS((DdManager *table, int size, Move *moves));
static Move* cuddZddUndoMoves ARGS((DdManager *table, Move *moves));

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


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


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




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

  Synopsis    [Implementation of the linear sifting algorithm for ZDDs.]

  Description [Implementation of the linear sifting algorithm for ZDDs.
  Assumes that no dead nodes are present.
    <ol>
    <li> Order all the variables according to the number of entries
    in each unique table.
    <li> Sift the variable up and down and applies the XOR transformation,
    remembering each time the total size of the DD heap.
    <li> Select the best permutation.
    <li> Repeat 3 and 4 for all variables.
    </ol>
  Returns 1 if successful; 0 otherwise.]

  SideEffects [None]

  SeeAlso     []

******************************************************************************/
int
cuddZddLinearSifting(
  DdManager * table,
  int  lower,
  int  upper)
{
    int	i;
    int	*var;
    int	size;
    int	x;
    int	result;
#ifdef DD_STATS
    int	previousSize;
#endif

    size = table->sizeZ;
    empty = table->zero;

    /* Find order in which to sift variables. */
    var = NULL;
    zdd_entry = ALLOC(int, size);
    if (zdd_entry == NULL) {
	table->errorCode = CUDD_MEMORY_OUT;
	goto cuddZddSiftingOutOfMem;
    }
    var = ALLOC(int, size);
    if (var == NULL) {
	table->errorCode = CUDD_MEMORY_OUT;
	goto cuddZddSiftingOutOfMem;
    }

    for (i = 0; i < size; i++) {
	x = table->permZ[i];
	zdd_entry[i] = table->subtableZ[x].keys;
	var[i] = i;
    }

    qsort((void *)var, size, sizeof(int), (int (*)(const void *, const void *))cuddZddUniqueCompare);

    /* Now sift. */
    for (i = 0; i < ddMin(table->siftMaxVar, size); i++) {
	if (zddTotalNumberSwapping >= table->siftMaxSwap)
	    break;
	x = table->permZ[var[i]];
	if (x < lower || x > upper) continue;
#ifdef DD_STATS
	previousSize = table->keysZ;
#endif
	result = cuddZddLinearAux(table, x, lower, upper);
	if (!result)
	    goto cuddZddSiftingOutOfMem;
#ifdef DD_STATS
	if (table->keysZ < (unsigned) previousSize) {
	    (void) fprintf(table->out,"-");
	} else if (table->keysZ > (unsigned) previousSize) {
	    (void) fprintf(table->out,"+");	/* should never happen */
	    (void) fprintf(table->out,"\nSize increased from %d to %d while sifting variable %d\n", previousSize, table->keysZ , var[i]);
	} else {
	    (void) fprintf(table->out,"=");
	}
	fflush(table->out);
#endif
    }

    FREE(var);
    FREE(zdd_entry);

    return(1);

cuddZddSiftingOutOfMem:

    if (zdd_entry != NULL) FREE(zdd_entry);
    if (var != NULL) FREE(var);

    return(0);

} /* end of cuddZddLinearSifting */


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


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

  Synopsis    [Linearly combines two adjacent variables.]

  Description [Linearly combines two adjacent variables. It assumes
  that no dead nodes are present on entry to this procedure.  The
  procedure then guarantees that no dead nodes will be present when it
  terminates.  cuddZddLinearInPlace assumes that x &lt; y.  Returns the
  number of keys in the table if successful; 0 otherwise.]

  SideEffects [None]

  SeeAlso     [cuddZddSwapInPlace cuddLinearInPlace]

******************************************************************************/
int
cuddZddLinearInPlace(
  DdManager * table,
  int  x,
  int  y)
{
    DdNodePtr *xlist, *ylist;
    int		xindex, yindex;
    int		xslots, yslots;
    int		xshift, yshift;
    int         oldxkeys, oldykeys;
    int         newxkeys, newykeys;
    int		i;
    int		posn;
    DdNode	*f, *f1, *f0, *f11, *f10, *f01, *f00;
    DdNode	*newf1, *newf0, *g, *next, *previous;
    DdNode	*special;

#ifdef DD_DEBUG
    assert(x < y);
    assert(cuddZddNextHigh(table,x) == y);
    assert(table->subtableZ[x].keys != 0);
    assert(table->subtableZ[y].keys != 0);
    assert(table->subtableZ[x].dead == 0);
    assert(table->subtableZ[y].dead == 0);
#endif

    zddTotalNumberLinearTr++;

    /* Get parameters of x subtable. */
    xindex   = table->invpermZ[x];
    xlist    = table->subtableZ[x].nodelist;
    oldxkeys = table->subtableZ[x].keys;
    xslots   = table->subtableZ[x].slots;
    xshift   = table->subtableZ[x].shift;
    newxkeys = 0;

    /* Get parameters of y subtable. */
    yindex   = table->invpermZ[y];
    ylist    = table->subtableZ[y].nodelist;
    oldykeys = table->subtableZ[y].keys;
    yslots   = table->subtableZ[y].slots;
    yshift   = table->subtableZ[y].shift;
    newykeys = oldykeys;

    /* The nodes in the x layer are put in two chains.  The chain
    ** pointed by g holds the normal nodes. When re-expressed they stay
    ** in the x list. The chain pointed by special holds the elements
    ** that will move to the y list.
    */
    g = special = NULL;
    for (i = 0; i < xslots; i++) {
	f = xlist[i];
	if (f == NULL) continue;
	xlist[i] = NULL;
	while (f != NULL) {
	    next = f->next;
	    f1 = cuddT(f);
	    /* if (f1->index == yindex) */ cuddSatDec(f1->ref);
	    f0 = cuddE(f);
	    /* if (f0->index == yindex) */ cuddSatDec(f0->ref);
	    if ((int) f1->index == yindex && cuddE(f1) == empty &&
		(int) f0->index != yindex) {
		f->next = special;
		special = f;
	    } else {
		f->next = g;
		g = f;
	    }
	    f = next;
	} /* while there are elements in the collision chain */
    } /* for each slot of the x subtable */

    /* Mark y nodes with pointers from above x. We mark them by
    **  changing their index to x.
    */
    for (i = 0; i < yslots; i++) {
	f = ylist[i];
	while (f != NULL) {
	    if (f->ref != 0) {
		f->index = xindex;
	    }
	    f = f->next;
	} /* while there are elements in the collision chain */
    } /* for each slot of the y subtable */

    /* Move special nodes to the y list. */
    f = special;
    while (f != NULL) {
	next = f->next;
	f1 = cuddT(f);
	f11 = cuddT(f1);
	cuddT(f) = f11;
	cuddSatInc(f11->ref);
	f0 = cuddE(f);
	cuddSatInc(f0->ref);
	f->index = yindex;
	/* Insert at the beginning of the list so that it will be
	** found first if there is a duplicate. The duplicate will
	** eventually be moved or garbage collected. No node
	** re-expression will add a pointer to it.
	*/
	posn = ddHash(f11, f0, yshift);
	f->next = ylist[posn];
	ylist[posn] = f;
	newykeys++;
	f = next;
    }

    /* Take care of the remaining x nodes that must be re-expressed.
    ** They form a linked list pointed by g.
    */
    f = g;
    while (f != NULL) {
#ifdef DD_COUNT
	table->swapSteps++;
#endif
	next = f->next;
	/* Find f1, f0, f11, f10, f01, f00. */
	f1 = cuddT(f);
	if ((int) f1->index == yindex || (int) f1->index == xindex) {
	    f11 = cuddT(f1); f10 = cuddE(f1);
	} else {
	    f11 = empty; f10 = f1;
	}
	f0 = cuddE(f);
	if ((int) f0->index == yindex || (int) f0->index == xindex) {
	    f01 = cuddT(f0); f00 = cuddE(f0);
	} else {
	    f01 = empty; f00 = f0;
	}
	/* Create the new T child. */
	if (f01 == empty) {
	    newf1 = f10;
	    cuddSatInc(newf1->ref);
	} else {
	    /* Check ylist for triple (yindex, f01, f10). */
	    posn = ddHash(f01, f10, yshift);
	    /* For each element newf1 in collision list ylist[posn]. */
	    newf1 = ylist[posn];
	    /* Search the collision chain skipping the marked nodes. */
	    while (newf1 != NULL) {
		if (cuddT(newf1) == f01 && cuddE(newf1) == f10 &&
		    (int) newf1->index == yindex) {
		    cuddSatInc(newf1->ref);
		    break; /* match */
		}
		newf1 = newf1->next;
	    } /* while newf1 */
	    if (newf1 == NULL) {	/* no match */
		newf1 = cuddDynamicAllocNode(table);
		if (newf1 == NULL)
		    goto zddSwapOutOfMem;
		newf1->index = yindex; newf1->ref = 1;
		cuddT(newf1) = f01;
		cuddE(newf1) = f10;
		/* Insert newf1 in the collision list ylist[pos];
		** increase the ref counts of f01 and f10
		*/
		newykeys++;
		newf1->next = ylist[posn];
		ylist[posn] = newf1;
		cuddSatInc(f01->ref);
		cuddSatInc(f10->ref);
	    }
	}
	cuddT(f) = newf1;

	/* Do the same for f0. */
	/* Create the new E child. */
	if (f11 == empty) {
	    newf0 = f00;
	    cuddSatInc(newf0->ref);
	} else {
	    /* Check ylist for triple (yindex, f11, f00). */
	    posn = ddHash(f11, f00, yshift);
	    /* For each element newf0 in collision list ylist[posn]. */
	    newf0 = ylist[posn];
	    while (newf0 != NULL) {
		if (cuddT(newf0) == f11 && cuddE(newf0) == f00 &&
		    (int) newf0->index == yindex) {
		    cuddSatInc(newf0->ref);
		    break; /* match */
		}
		newf0 = newf0->next;
	    } /* while newf0 */
	    if (newf0 == NULL) {	/* no match */
		newf0 = cuddDynamicAllocNode(table);
		if (newf0 == NULL)
		    goto zddSwapOutOfMem;
		newf0->index = yindex; newf0->ref = 1;
		cuddT(newf0) = f11; cuddE(newf0) = f00;
		/* Insert newf0 in the collision list ylist[posn];
		** increase the ref counts of f11 and f00.
		*/
		newykeys++;
		newf0->next = ylist[posn];
		ylist[posn] = newf0;
		cuddSatInc(f11->ref);
		cuddSatInc(f00->ref);
	    }
	}
	cuddE(f) = newf0;

	/* Re-insert the modified f in xlist.
	** The modified f does not already exists in xlist.
	** (Because of the uniqueness of the cofactors.)
	*/
	posn = ddHash(newf1, newf0, xshift);
	newxkeys++;
	f->next = xlist[posn];
	xlist[posn] = f;
	f = next;
    } /* while f != NULL */

    /* GC the y layer and move the marked nodes to the x list. */

    /* For each node f in ylist. */
    for (i = 0; i < yslots; i++) {
	previous = NULL;
	f = ylist[i];
	while (f != NULL) {
	    next = f->next;
	    if (f->ref == 0) {
		cuddSatDec(cuddT(f)->ref);
		cuddSatDec(cuddE(f)->ref);
		cuddDeallocNode(table, f);
		newykeys--;
		if (previous == NULL)
		    ylist[i] = next;
		else
		    previous->next = next;
	    } else if ((int) f->index == xindex) { /* move marked node */
		if (previous == NULL)
		    ylist[i] = next;
		else
		    previous->next = next;
		f1 = cuddT(f);
		cuddSatDec(f1->ref);
		/* Check ylist for triple (yindex, f1, empty). */
		posn = ddHash(f1, empty, yshift);
		/* For each element newf1 in collision list ylist[posn]. */
		newf1 = ylist[posn];
		while (newf1 != NULL) {
		    if (cuddT(newf1) == f1 && cuddE(newf1) == empty &&
			(int) newf1->index == yindex) {
			cuddSatInc(newf1->ref);
			break; /* match */
		    }