cuddreorder.c

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

    moves = NULL;
    yindex = table->invperm[y];

    /* Initialize the lower bound.
    ** The part of the DD below y will not change.
    ** The part of the DD above y that does not interact with y will not
    ** change. The rest may vanish in the best case, except for
    ** the nodes at level xLow, which will not vanish, regardless.
    */
    limitSize = L = table->keys - table->isolated;
    for (x = xLow + 1; x < y; x++) {
	xindex = table->invperm[x];
	if (cuddTestInteract(table,xindex,yindex)) {
	    isolated = table->vars[xindex]->ref == 1;
	    L -= table->subtables[x].keys - isolated;
	}
    }
    isolated = table->vars[yindex]->ref == 1;
    L -= table->subtables[y].keys - isolated;

    x = cuddNextLow(table,y);
    while (x >= xLow && L <= limitSize) {
	xindex = table->invperm[x];
#ifdef DD_DEBUG
	checkL = table->keys - table->isolated;
	for (z = xLow + 1; z < y; z++) {
	    zindex = table->invperm[z];
	    if (cuddTestInteract(table,zindex,yindex)) {
		isolated = table->vars[zindex]->ref == 1;
		checkL -= table->subtables[z].keys - isolated;
	    }
	}
	isolated = table->vars[yindex]->ref == 1;
	checkL -= table->subtables[y].keys - isolated;
	assert(L == checkL);
#endif
	size = cuddSwapInPlace(table,x,y);
	if (size == 0) goto ddSiftingUpOutOfMem;
	/* Update the lower bound. */
	if (cuddTestInteract(table,xindex,yindex)) {
	    isolated = table->vars[xindex]->ref == 1;
	    L += table->subtables[y].keys - isolated;
	}
	move = (Move *) cuddDynamicAllocNode(table);
	if (move == NULL) goto ddSiftingUpOutOfMem;
	move->x = x;
	move->y = y;
	move->size = size;
	move->next = moves;
	moves = move;
	if ((double) size > (double) limitSize * table->maxGrowth) break;
	if (size < limitSize) limitSize = size;
	y = x;
	x = cuddNextLow(table,y);
    }
    return(moves);

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

} /* end of ddSiftingUp */
    

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

  Synopsis    [Sifts a variable down.]

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

  SideEffects [None]

******************************************************************************/
static Move *
ddSiftingDown(
  DdManager * table,
  int  x,
  int  xHigh)
{
    Move	*moves;
    Move	*move;
    int		y;
    int		size;
    int		R;	/* upper bound on node decrease */
    int		limitSize;
    int		xindex, yindex;
    int		isolated;
#ifdef DD_DEBUG
    int		checkR;
    int		z;
    int		zindex;
#endif

    moves = NULL;
    /* Initialize R */
    xindex = table->invperm[x];
    limitSize = size = table->keys - table->isolated;
    R = 0;
    for (y = xHigh; y > x; y--) {
	yindex = table->invperm[y];
	if (cuddTestInteract(table,xindex,yindex)) {
	    isolated = table->vars[yindex]->ref == 1;
	    R += table->subtables[y].keys - isolated;
	}
    }

    y = cuddNextHigh(table,x);
    while (y <= xHigh && size - R < limitSize) {
#ifdef DD_DEBUG
	checkR = 0;
	for (z = xHigh; z > x; z--) {
	    zindex = table->invperm[z];
	    if (cuddTestInteract(table,xindex,zindex)) {
		isolated = table->vars[zindex]->ref == 1;
		checkR += table->subtables[z].keys - isolated;
	    }
	}
	assert(R == checkR);
#endif
	/* Update upper bound on node decrease. */
	yindex = table->invperm[y];
	if (cuddTestInteract(table,xindex,yindex)) {
	    isolated = table->vars[yindex]->ref == 1;
	    R -= table->subtables[y].keys - isolated;
	}
	size = cuddSwapInPlace(table,x,y);
	if (size == 0) goto ddSiftingDownOutOfMem; 
	move = (Move *) cuddDynamicAllocNode(table);
	if (move == NULL) goto ddSiftingDownOutOfMem;
	move->x = x;
	move->y = y;
	move->size = size;
	move->next = moves;
	moves = move;
	if ((double) size > (double) limitSize * table->maxGrowth) break;
	if (size < limitSize) limitSize = size;
	x = y;
	y = cuddNextHigh(table,x);
    }
    return(moves);

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

} /* end of ddSiftingDown */


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

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

  Description [Given a set of moves, returns the DD 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]

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

    for (move = moves; move != NULL; move = move->next) {
	if (move->size < size) {
	    size = move->size;
	}
    }

    for (move = moves; move != NULL; move = move->next) {
	if (move->size == size) return(1);
	res = cuddSwapInPlace(table,(int)move->x,(int)move->y);
	if (!res) return(0);	
    }

    return(1);

} /* end of ddSiftingBackward */


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

  Synopsis    [Prepares the DD heap for dynamic reordering.]

  Description [Prepares the DD heap for dynamic reordering. Does
  garbage collection, to guarantee that there are no dead nodes;
  clears the cache, which is invalidated by dynamic reordering; initializes
  the number of isolated projection functions; and initializes the
  interaction matrix.  Returns 1 in case of success; 0 otherwise.]

  SideEffects [None]

******************************************************************************/
static int
ddReorderPreprocess(
  DdManager * table)
{
    int i;
    int res;

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

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

    /* Initialize number of isolated projection functions. */
    table->isolated = 0;
    for (i = 0; i < table->size; i++) {
	if (table->vars[i]->ref == 1) table->isolated++;
    }

    /* Initialize the interaction matrix. */
    res = cuddInitInteract(table);
    if (res == 0) return(0);

    return(1);

} /* end of ddReorderPreprocess */


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

  Synopsis    [Cleans up at the end of reordering.]

  Description []

  SideEffects [None]

******************************************************************************/
static int
ddReorderPostprocess(
  DdManager * table)
{

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

    /* Free interaction matrix. */
    FREE(table->interact);

    return(1);

} /* end of ddReorderPostprocess */


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

  Synopsis    [Reorders variables according to a given permutation.]

  Description [Reorders 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. ddShuffle assumes that no
  dead nodes are present and that the interaction matrix is properly
  initialized.  The reordering is achieved by a series of upward sifts.
  Returns 1 if successful; 0 otherwise.]

  SideEffects [None]

  SeeAlso []

******************************************************************************/
static int
ddShuffle(
  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

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

    numvars = table->size;

    for (level = 0; level < numvars; level++) {
	index = permutation[level];
	position = table->perm[index];
#ifdef DD_STATS
	previousSize = table->keys - table->isolated;
#endif
	result = ddSiftUp(table,position,level);
	if (!result) return(0);
#ifdef DD_STATS
	if (table->keys < (unsigned) previousSize + table->isolated) {
	    (void) fprintf(table->out,"-");
	} else if (table->keys > (unsigned) previousSize + table->isolated) {
	    (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->keys - table->isolated;
    (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",
		   ddTotalNumberSwapping);
    (void) fprintf(table->out,"#:M_SHUFFLE %8d: NI swaps\n",ddTotalNISwaps);
#endif

    return(1);

} /* end of ddShuffle */


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

  Synopsis    [Moves one variable up.]

  Description [Takes a 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
ddSiftUp(
  DdManager * table,
  int  x,
  int  xLow)
{
    int        y;
    int        size;

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

} /* end of ddSiftUp */


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

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

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

  SideEffects [Changes the BDD variable group tree.]

  SeeAlso     []

******************************************************************************/
static void
bddFixTree(
  DdManager * table,
  MtrNode * treenode)
{
    if (treenode == NULL) return;
    treenode->low = ((int) treenode->index < table->size) ?
	table->perm[treenode->index] : treenode->index;
    if (treenode->child != NULL) {
	bddFixTree(table, treenode->child);
    }
    if (treenode->younger != NULL)
	bddFixTree(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 bddFixTree */


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

  Synopsis    [Updates the BDD variable group tree before a shuffle.]

  Description [Updates the BDD variable group tree before a shuffle.
  Returns 1 if successful; 0 otherwise.]

  SideEffects [Changes the BDD variable group tree.]

  SeeAlso     []

******************************************************************************/
static int
ddUpdateMtrTree(
  DdManager * table,
  MtrNode * treenode,
  int * perm,
  int * invperm)
{
    int	i, size, index, level;
    int	minLevel, maxLevel, minIndex;

    if (treenode == NULL) return(1);

    /* i : level */
    for (i = treenode->low; i < treenode->low + treenode->size; i++) {
	index = table->invperm[i];
	level = perm[index];
	if (level < minLevel) {
	    minLevel = level;
	    minIndex = index;
	}
	if (level > maxLevel)
	    maxLevel = level;
    }
    size = maxLevel - minLevel + 1;
    if (size == treenode->size) {
	treenode->low = minLevel;
	treenode->index = minIndex;
    } else
	return(0);

    if (treenode->child != NULL) {
	if (!ddUpdateMtrTree(table, treenode->child, perm, invperm))
	    return(0);
    }
    if (treenode->younger != NULL) {
	if (!ddUpdateMtrTree(table, treenode->younger, perm, invperm))
	    return(0);
    }
    return(1);
}


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

  Synopsis    [Checks the BDD variable group tree before a shuffle.]

  Description [Checks the BDD variable group tree before a shuffle.
  Returns 1 if successful; 0 otherwise.]

  SideEffects [Changes the BDD variable group tree.]

  SeeAlso     []

******************************************************************************/
static int
ddCheckPermuation(
  DdManager * table,
  MtrNode * treenode,
  int * perm,
  int * invperm)
{
    int	i, size, index, level;
    int	minLevel, maxLevel;

    if (treenode == NULL) return(1);

    minLevel = table->size;
    maxLevel = 0;
    /* i : level */
    for (i = treenode->low; i < treenode->low + treenode->size; i++) {
	index = table->invperm[i];
	level = perm[index];
	if (level < minLevel)
	    minLevel = level;
	if (level > maxLevel)
	    maxLevel = level;
    }
    size = maxLevel - minLevel + 1;
    if (size != treenode->size)
	return(0);

    if (treenode->child != NULL) {
	if (!ddCheckPermuation(table, treenode->child, perm, invperm))
	    return(0);
    }
    if (treenode->younger != NULL) {
	if (!ddCheckPermuation(table, treenode->younger, perm, invperm))
	    return(0);
    }
    return(1);
}