cuddsymmetry.c

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

	    if (size == 0) goto ddSymmSiftingUpOutOfMem;
	    /* Update the lower bound. */
	    z = moves->y;
	    do {
		zindex = table->invperm[z];
		if (cuddTestInteract(table,zindex,yindex)) {
		    isolated = table->vars[zindex]->ref == 1;
		    L += table->subtables[z].keys - isolated;
		}
		z = table->subtables[z].next;
	    } while (z != (int) moves->y);
	    if ((double) size > (double) limitSize * table->maxGrowth)
		return(moves);
	    if (size < limitSize) limitSize = size;
	}
	y = gxtop;
	x = cuddNextLow(table,y);
    }

    return(moves);

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

} /* end of ddSymmSiftingUp */


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

  Synopsis    [Moves x down until either it reaches the bound (xHigh) or
  the size of the DD heap increases too much.]

  Description [Moves x down until either it reaches the bound (xHigh)
  or the size of the DD heap increases too much. Assumes that x is the
  bottom of a symmetry group. Checks x for symmetry to the adjacent
  variables. If symmetry is found, the symmetry group of x is merged
  with the symmetry group of the other variable. Returns the set of
  moves in case of success; MV_OOM if memory is full.]

  SideEffects [None]

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

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

    y = cuddNextHigh(table,x);
    while (y <= xHigh && size - R < limitSize) {
#ifdef DD_DEBUG
	gxtop = table->subtables[x].next;
	checkR = 0;
	for (z = xHigh; z > gxtop; z--) {
	    zindex = table->invperm[z];
	    if (zindex == xindex || cuddTestInteract(table,xindex,zindex)) {
		isolated = table->vars[zindex]->ref == 1;
		checkR += table->subtables[z].keys - isolated;
	    }
	}
	assert(R == checkR);
#endif
	gybot = table->subtables[y].next;
	while (table->subtables[gybot].next != (unsigned) y)
	    gybot = table->subtables[gybot].next;
	if (cuddSymmCheck(table,x,y)) {
	    /* Symmetry found, attach symm groups */
	    gxtop = table->subtables[x].next;
	    table->subtables[x].next = y;
	    table->subtables[gybot].next = gxtop;
	} else if (table->subtables[x].next == (unsigned) x &&
		   table->subtables[y].next == (unsigned) y) {
	    /* x and y have self symmetry */
	    /* 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);
#ifdef DD_DEBUG
	    assert(table->subtables[x].next == (unsigned) x);
	    assert(table->subtables[y].next == (unsigned) y);
#endif
	    if (size == 0) goto ddSymmSiftingDownOutOfMem;
	    move = (Move *) cuddDynamicAllocNode(table);
	    if (move == NULL) goto ddSymmSiftingDownOutOfMem;
	    move->x = x;
	    move->y = y;
	    move->size = size;
	    move->next = moves;
	    moves = move;
	    if ((double) size > (double) limitSize * table->maxGrowth)
		return(moves);
	    if (size < limitSize) limitSize = size;
	} else { /* Group move */
	    /* Update upper bound on node decrease: first phase. */
	    gxtop = table->subtables[x].next;
	    z = gxtop + 1;
	    do {
		zindex = table->invperm[z];
		if (zindex == xindex || cuddTestInteract(table,xindex,zindex)) {
		    isolated = table->vars[zindex]->ref == 1;
		    R -= table->subtables[z].keys - isolated;
		}
		z++;
	    } while (z <= gybot);
	    size = ddSymmGroupMove(table,x,y,&moves);
	    if (size == 0) goto ddSymmSiftingDownOutOfMem;
	    if ((double) size > (double) limitSize * table->maxGrowth)
		return(moves);
	    if (size < limitSize) limitSize = size;
	    /* Update upper bound on node decrease: second phase. */
	    gxtop = table->subtables[gybot].next;
	    for (z = gxtop + 1; z <= gybot; z++) {
		zindex = table->invperm[z];
		if (zindex == xindex || cuddTestInteract(table,xindex,zindex)) {
		    isolated = table->vars[zindex]->ref == 1;
		    R += table->subtables[z].keys - isolated;
		}
	    }
	}
	x = gybot;
	y = cuddNextHigh(table,x);
    }

    return(moves);

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

} /* end of ddSymmSiftingDown */


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

  Synopsis    [Swaps two groups.]

  Description [Swaps two groups. x is assumed to be the bottom variable
  of the first group. y is assumed to be the top variable of the second
  group.  Updates the list of moves. Returns the number of keys in the
  table if successful; 0 otherwise.]

  SideEffects [None]

******************************************************************************/
static int
ddSymmGroupMove(
  DdManager * table,
  int  x,
  int  y,
  Move ** moves)
{
    Move *move;
    int	 size;
    int  i,j;
    int  xtop,xbot,xsize,ytop,ybot,ysize,newxtop;
    int  swapx,swapy;

#if DD_DEBUG
    assert(x < y);	/* we assume that x < y */
#endif
    /* Find top, bottom, and size for the two groups. */
    xbot = x;
    xtop = table->subtables[x].next;
    xsize = xbot - xtop + 1;
    ybot = y;
    while ((unsigned) ybot < table->subtables[ybot].next)
	ybot = table->subtables[ybot].next;
    ytop = y;
    ysize = ybot - ytop + 1;

    /* Sift the variables of the second group up through the first group. */
    for (i = 1; i <= ysize; i++) {
        for (j = 1; j <= xsize; j++) {
	    size = cuddSwapInPlace(table,x,y);
	    if (size == 0) return(0);
	    swapx = x; swapy = y;
	    y = x;
	    x = y - 1;
	}
	y = ytop + i;
	x = y - 1;
    }

    /* fix symmetries */
    y = xtop; /* ytop is now where xtop used to be */
    for (i = 0; i < ysize-1 ; i++) {
	table->subtables[y].next = y + 1;
	y = y + 1;
    }
    table->subtables[y].next = xtop; /* y is bottom of its group, join */
    				     /* its symmetry to top of its group */
    x = y + 1;
    newxtop = x;
    for (i = 0; i < xsize - 1 ; i++) {
	table->subtables[x].next = x + 1;
	x = x + 1;
    }
    table->subtables[x].next = newxtop; /* x is bottom of its group, join */
    					/* its symmetry to top of its group */
    /* Store group move */
    move = (Move *) cuddDynamicAllocNode(table);
    if (move == NULL) return(0);
    move->x = swapx;
    move->y = swapy;
    move->size = size;
    move->next = *moves;
    *moves = move;

    return(size);

} /* end of ddSymmGroupMove */


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

  Synopsis    [Undoes the swap of two groups.]

  Description [Undoes the swap of two groups. x is assumed to be the
  bottom variable of the first group. y is assumed to be the top
  variable of the second group.  Returns the number of keys in the table
  if successful; 0 otherwise.]

  SideEffects [None]

******************************************************************************/
static int
ddSymmGroupMoveBackward(
  DdManager * table,
  int  x,
  int  y)
{
    int	size;
    int i,j;
    int	xtop,xbot,xsize,ytop,ybot,ysize,newxtop;

#if DD_DEBUG
    assert(x < y); /* We assume that x < y */
#endif

    /* Find top, bottom, and size for the two groups. */
    xbot = x;
    xtop = table->subtables[x].next;
    xsize = xbot - xtop + 1;
    ybot = y;
    while ((unsigned) ybot < table->subtables[ybot].next)
	ybot = table->subtables[ybot].next;
    ytop = y;
    ysize = ybot - ytop + 1;

    /* Sift the variables of the second group up through the first group. */
    for (i = 1; i <= ysize; i++) {
        for (j = 1; j <= xsize; j++) {
	    size = cuddSwapInPlace(table,x,y);
	    if (size == 0) return(0);
	    y = x;
	    x = cuddNextLow(table,y);
	}
	y = ytop + i;
	x = y - 1;
    }

    /* Fix symmetries. */
    y = xtop;
    for (i = 0; i < ysize-1 ; i++) {
	table->subtables[y].next = y + 1;
	y = y + 1;
    }
    table->subtables[y].next = xtop; /* y is bottom of its group, join */
    				     /* its symmetry to top of its group */
    x = y + 1;
    newxtop = x;
    for (i = 0; i < xsize-1 ; i++) {
	table->subtables[x].next = x + 1;
	x = x + 1;
    }
    table->subtables[x].next = newxtop; /* x is bottom of its group, join */
					/* its symmetry to top of its group */

    return(size);

} /* end of ddSymmGroupMoveBackward */


/**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
ddSymmSiftingBackward(
  DdManager * table,
  Move * moves,
  int  size)
{
    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);
	if (table->subtables[move->x].next == move->x && table->subtables[move->y].next == move->y) {
	    res = cuddSwapInPlace(table,(int)move->x,(int)move->y);
#ifdef DD_DEBUG
	    assert(table->subtables[move->x].next == move->x);
	    assert(table->subtables[move->y].next == move->y);
#endif
	} else { /* Group move necessary */
	    res = ddSymmGroupMoveBackward(table,(int)move->x,(int)move->y);
	}
	if (!res) return(0);
    }

    return(1);

} /* end of ddSymmSiftingBackward */


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

  Synopsis    [Counts numbers of symmetric variables and symmetry
  groups.]

  Description []

  SideEffects [None]

******************************************************************************/
static void
ddSymmSummary(
  DdManager * table,
  int  lower,
  int  upper,
  int * symvars,
  int * symgroups)
{
    int i,x,gbot;
    int TotalSymm = 0;
    int TotalSymmGroups = 0;

    for (i = lower; i <= upper; i++) {
	if (table->subtables[i].next != (unsigned) i) {
	    TotalSymmGroups++;
	    x = i;
	    do {
		TotalSymm++;
		gbot = x;
		x = table->subtables[x].next;
	    } while (x != i);
#ifdef DD_DEBUG
	    assert(table->subtables[gbot].next == (unsigned) i);
#endif
	    i = gbot;
	}
    }
    *symvars = TotalSymm;
    *symgroups = TotalSymmGroups;

    return;

} /* end of ddSymmSummary */