cuddzddreord.c

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

{
    Move	*move;
    Move	*moveUp;	/* list of up move */
    Move	*moveDown;	/* list of down move */

    int		initial_size;
    int		result;

    initial_size = table->keysZ;

#ifdef DD_DEBUG
    assert(table->subtableZ[x].keys > 0);
#endif

    moveDown = NULL;
    moveUp = NULL;

    if (x == x_low) {
	moveDown = cuddZddSiftingDown(table, x, x_high, initial_size);
	/* after that point x --> x_high */
	if (moveDown == NULL)
	    goto cuddZddSiftingAuxOutOfMem;
	result = cuddZddSiftingBackward(table, moveDown,
	    initial_size);
	/* move backward and stop at best position */
	if (!result)
	    goto cuddZddSiftingAuxOutOfMem;

    }
    else if (x == x_high) {
	moveUp = cuddZddSiftingUp(table, x, x_low, initial_size);
	/* after that point x --> x_low */
	if (moveUp == NULL)
	    goto cuddZddSiftingAuxOutOfMem;
	result = cuddZddSiftingBackward(table, moveUp, initial_size);
	/* move backward and stop at best position */
	if (!result)
	    goto cuddZddSiftingAuxOutOfMem;
    }
    else if ((x - x_low) > (x_high - x)) {
	/* must go down first:shorter */
	moveDown = cuddZddSiftingDown(table, x, x_high, initial_size);
	/* after that point x --> x_high */
	if (moveDown == NULL)
	    goto cuddZddSiftingAuxOutOfMem;
	moveUp = cuddZddSiftingUp(table, moveDown->y, x_low,
	    initial_size);
	if (moveUp == NULL)
	    goto cuddZddSiftingAuxOutOfMem;
	result = cuddZddSiftingBackward(table, moveUp, initial_size);
	/* move backward and stop at best position */
	if (!result)
	    goto cuddZddSiftingAuxOutOfMem;
    }
    else {
	moveUp = cuddZddSiftingUp(table, x, x_low, initial_size);
	/* after that point x --> x_high */
	if (moveUp == NULL)
	    goto cuddZddSiftingAuxOutOfMem;
	moveDown = cuddZddSiftingDown(table, moveUp->x, x_high,
	    initial_size);
	/* then move up */
	if (moveDown == NULL)
	    goto cuddZddSiftingAuxOutOfMem;
	result = cuddZddSiftingBackward(table, moveDown,
	    initial_size);
	/* move backward and stop at best position */
	if (!result)
	    goto cuddZddSiftingAuxOutOfMem;
    }

    while (moveDown != NULL) {
	move = moveDown->next;
	cuddDeallocNode(table, (DdNode *)moveDown);
	moveDown = move;
    }
    while (moveUp != NULL) {
	move = moveUp->next;
	cuddDeallocNode(table, (DdNode *)moveUp);
	moveUp = move;
    }

    return(1);

cuddZddSiftingAuxOutOfMem:
    while (moveDown != NULL) {
	move = moveDown->next;
	cuddDeallocNode(table, (DdNode *)moveDown);
	moveDown = move;
    }
    while (moveUp != NULL) {
	move = moveUp->next;
	cuddDeallocNode(table, (DdNode *)moveUp);
	moveUp = move;
    }

    return(0);

} /* end of cuddZddSiftingAux */


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

  Synopsis    [Sifts a variable up.]

  Description [Sifts a variable up. Moves y up until either it reaches
  the bound (x_low) or the size of the ZDD heap increases too much.
  Returns the set of moves in case of success; NULL if memory is full.]

  SideEffects [None]

  SeeAlso     []

******************************************************************************/
static Move *
cuddZddSiftingUp(
  DdManager * table,
  int  x,
  int  x_low,
  int  initial_size)
{
    Move	*moves;
    Move	*move;
    int		y;
    int		size;
    int		limit_size = initial_size;

    moves = NULL;
    y = cuddZddNextLow(table, x);
    while (y >= x_low) {
	size = cuddZddSwapInPlace(table, y, x);
	if (size == 0)
	    goto cuddZddSiftingUpOutOfMem;
	move = (Move *)cuddDynamicAllocNode(table);
	if (move == NULL)
	    goto cuddZddSiftingUpOutOfMem;
	move->x = y;
	move->y = x;
	move->size = size;
	move->next = moves;
	moves = move;

	if ((double)size > (double)limit_size * table->maxGrowth)
	    break;
        if (size < limit_size)
	    limit_size = size;

	x = y;
	y = cuddZddNextLow(table, x);
    }
    return(moves);

cuddZddSiftingUpOutOfMem:
    while (moves != NULL) {
	move = moves->next;
	cuddDeallocNode(table, (DdNode *)moves);
	moves = move;
    }
    return(NULL);

} /* end of cuddZddSiftingUp */


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

  Synopsis    [Sifts a variable down.]

  Description [Sifts a variable down. Moves x down until either it
  reaches the bound (x_high) or the size of the ZDD heap increases too
  much. Returns the set of moves in case of success; NULL if memory is
  full.]

  SideEffects [None]

  SeeAlso     []

******************************************************************************/
static Move *
cuddZddSiftingDown(
  DdManager * table,
  int  x,
  int  x_high,
  int  initial_size)
{
    Move	*moves;
    Move	*move;
    int		y;
    int		size;
    int		limit_size = initial_size;

    moves = NULL;
    y = cuddZddNextHigh(table, x);
    while (y <= x_high) {
	size = cuddZddSwapInPlace(table, x, y);
	if (size == 0)
	    goto cuddZddSiftingDownOutOfMem;
	move = (Move *)cuddDynamicAllocNode(table);
	if (move == NULL)
	    goto cuddZddSiftingDownOutOfMem;
	move->x = x;
	move->y = y;
	move->size = size;
	move->next = moves;
	moves = move;

	if ((double)size > (double)limit_size * table->maxGrowth)
	    break;
        if (size < limit_size)
	    limit_size = size;

	x = y;
	y = cuddZddNextHigh(table, x);
    }
    return(moves);

cuddZddSiftingDownOutOfMem:
    while (moves != NULL) {
	move = moves->next;
	cuddDeallocNode(table, (DdNode *)moves);
	moves = move;
    }
    return(NULL);

} /* end of cuddZddSiftingDown */


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

  Synopsis    [Given a set of moves, returns the ZDD heap to the position
  giving the minimum size.]

  Description [Given a set of moves, returns the ZDD heap to the
  position giving the minimum size. In case of ties, returns to the
  closest position giving the minimum size. Returns 1 in case of
  success; 0 otherwise.]

  SideEffects [None]

  SeeAlso     []

******************************************************************************/
static int
cuddZddSiftingBackward(
  DdManager * table,
  Move * moves,
  int  size)
{
    int	    	i;
    int		i_best;
    Move	*move;
    int		res;

    /* Find the minimum size among moves. */
    i_best = -1;
    for (move = moves, i = 0; move != NULL; move = move->next, i++) {
	if (move->size < size) {
	    i_best = i;
	    size = move->size;
	}
    }

    for (move = moves, i = 0; move != NULL; move = move->next, i++) {
	if (i == i_best)
	    break;
	res = cuddZddSwapInPlace(table, move->x, move->y);
	if (!res)
	    return(0);
	if (i_best == -1 && res == size)
	    break;
    }

    return(1);

} /* end of cuddZddSiftingBackward */


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

  Synopsis    [Prepares the ZDD heap for dynamic reordering.]

  Description [Prepares the ZDD heap for dynamic reordering. Does
  garbage collection, to guarantee that there are no dead nodes;
  and clears the cache, which is invalidated by dynamic reordering.]

  SideEffects [None]

******************************************************************************/
static void
zddReorderPreprocess(
  DdManager * table)
{

    /* Clear the cache. */
    cuddCacheFlush(table);

    /* Eliminate dead nodes. Do not scan the cache again. */
    cuddGarbageCollectZdd(table,0);

    return;

} /* end of ddReorderPreprocess */


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

  Synopsis    [Shrinks almost empty ZDD subtables at the end of reordering
  to guarantee that they have a reasonable load factor.]

  Description [Shrinks almost empty subtables at the end of reordering to
  guarantee that they have a reasonable load factor. However, if there many
  nodes are being reclaimed, then no resizing occurs. Returns 1 in case of
  success; 0 otherwise.]

  SideEffects [None]

******************************************************************************/
static int
zddReorderPostprocess(
  DdManager * table)
{
    int i, j, posn;
    DdNodePtr *nodelist, *oldnodelist;
    DdNode *node, *next;
    unsigned int slots, oldslots;
    extern void (*MMoutOfMemory)(long);
    void (*saveHandler)(long);

#ifdef DD_VERBOSE
    (void) fflush(table->out);
#endif

    /* If we have very many reclaimed nodes, we do not want to shrink
    ** the subtables, because this will lead to more garbage
    ** collections. More garbage collections mean shorter mean life for
    ** nodes with zero reference count; hence lower probability of finding
    ** a result in the cache.
    */
    if (table->reclaimed > table->allocated * 0.5) return(1);

    /* Resize subtables. */
    for (i = 0; i < table->sizeZ; i++) {
	int shift;
	oldslots = table->subtableZ[i].slots;
	if (oldslots < table->subtableZ[i].keys * DD_MAX_SUBTABLE_SPARSITY ||
	    oldslots <= table->initSlots) continue;
	oldnodelist = table->subtableZ[i].nodelist;
	slots = oldslots >> 1;
	saveHandler = MMoutOfMemory;
	MMoutOfMemory = Cudd_OutOfMem;
	nodelist = ALLOC(DdNodePtr, slots);
	MMoutOfMemory = saveHandler;
	if (nodelist == NULL) {
	    return(1);
	}
	table->subtableZ[i].nodelist = nodelist;
	table->subtableZ[i].slots = slots;
	table->subtableZ[i].shift++;
	table->subtableZ[i].maxKeys = slots * DD_MAX_SUBTABLE_DENSITY;
#ifdef DD_VERBOSE
	(void) fprintf(table->err,
		       "shrunk layer %d (%d keys) from %d to %d slots\n",
		       i, table->subtableZ[i].keys, oldslots, slots);
#endif

	for (j = 0; (unsigned) j < slots; j++) {
	    nodelist[j] = NULL;
	}
	shift = table->subtableZ[i].shift;
	for (j = 0; (unsigned) j < oldslots; j++) {
	    node = oldnodelist[j];
	    while (node != NULL) {
		next = node->next;
		posn = ddHash(cuddT(node), cuddE(node), shift);
		node->next = nodelist[posn];
		nodelist[posn] = node;
		node = next;
	    }
	}
	FREE(oldnodelist);

	table->memused += (slots - oldslots) * sizeof(DdNode *);
	table->slots += slots - oldslots;
	table->minDead = (unsigned) (table->gcFrac * (double) table->slots);
	table->cacheSlack = (int) ddMin(table->maxCacheHard,
	    DD_MAX_CACHE_TO_SLOTS_RATIO*table->slots) -
	    2 * (int) table->cacheSlots;
    }
    /* We don't look at the constant subtable, because it is not
    ** affected by reordering.
    */

    return(1);

} /* end of zddReorderPostprocess */


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

  Synopsis    [Reorders ZDD variables according to a given permutation.]

  Description [Reorders ZDD variables according to a given permutation.
  The i-th permutation array contains the index of the variable that
  should be brought to the i-th level. zddShuffle assumes that no
  dead nodes are present.  The reordering is achieved by a series of
  upward sifts.  Returns 1 if successful; 0 otherwise.]

  SideEffects [None]

  SeeAlso []

******************************************************************************/
static int
zddShuffle(
  DdManager * table,
  int * permutation)
{
    int		index;
    int		level;
    int		position;
    int		numvars;
    int		result;
#ifdef DD_STATS
    long	localTime;
    int		initialSize;
    int		finalSize;
    int		previousSize;
#endif

    zddTotalNumberSwapping = 0;
#ifdef DD_STATS
    localTime = util_cpu_time();
    initialSize = table->keysZ;
    (void) fprintf(table->out,"#:I_SHUFFLE %8d: initial size\n",
		   initialSize); 
#endif

    numvars = table->sizeZ;

    for (level = 0; level < numvars; level++) {
	index = permutation[level];
	position = table->permZ[index];
#ifdef DD_STATS
	previousSize = table->keysZ;
#endif
	result = zddSiftUp(table,position,level);
	if (!result) return(0);
#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 */
	} else {
	    (void) fprintf(table->out,"=");
	}
	fflush(table->out);
#endif
    }

#ifdef DD_STATS
    (void) fprintf(table->out,"\n");
    finalSize = table->keysZ;
    (void) fprintf(table->out,"#:F_SHUFFLE %8d: final size\n",finalSize); 
    (void) fprintf(table->out,"#:T_SHUFFLE %8g: total time (sec)\n",
	((double)(util_cpu_time() - localTime)/1000.0)); 
    (void) fprintf(table->out,"#:N_SHUFFLE %8d: total swaps\n",
		   zddTotalNumberSwapping);
#endif

    return(1);

} /* end of zddShuffle */


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

  Synopsis    [Moves one ZDD variable up.]

  Description [Takes a ZDD variable from position x and sifts it up to
  position xLow;  xLow should be less than or equal to x.
  Returns 1 if successful; 0 otherwise]

  SideEffects [None]

  SeeAlso     []

******************************************************************************/
static int
zddSiftUp(
  DdManager * table,
  int  x,
  int  xLow)
{
    int        y;
    int        size;

    y = cuddZddNextLow(table,x);
    while (y >= xLow) {
	size = cuddZddSwapInPlace(table,y,x);
	if (size == 0) {
	    return(0);
	}
	x = y;
	y = cuddZddNextLow(table,x);
    }
    return(1);

} /* end of zddSiftUp */


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

  Synopsis    [Fixes the ZDD variable group tree after a shuffle.]

  Description [Fixes the ZDD variable group tree after a
  shuffle. Assumes that the order of the variables in a terminal node
  has not been changed.]

  SideEffects [Changes the ZDD variable group tree.]

  SeeAlso     []

******************************************************************************/
static void
zddFixTree(
  DdManager * table,
  MtrNode * treenode)
{
    if (treenode == NULL) return;
    treenode->low = ((int) treenode->index < table->sizeZ) ?
	table->permZ[treenode->index] : treenode->index;
    if (treenode->child != NULL) {
	zddFixTree(table, treenode->child);
    }
    if (treenode->younger != NULL)
	zddFixTree(table, treenode->younger);
    if (treenode->parent != NULL && treenode->low < treenode->parent->low) {
	treenode->parent->low = treenode->low;
	treenode->parent->index = treenode->index;
    }
    return;

} /* end of zddFixTree */