cuddzddsymm.c

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

	if (move_down == ZDD_MV_OOM)
	    goto cuddZddSymmSiftingConvAuxOutOfMem;

	if (move_down == NULL ||
	    table->subtableZ[move_down->y].next != move_down->y) {
	    /* symmetry detected may have to make another complete
	       pass */
            if (move_down != NULL) {
		x = move_down->y;
	    }
	    else {
		while ((unsigned) x < table->subtableZ[x].next)
		    x = table->subtableZ[x].next;
		x = table->subtableZ[x].next;
	    }
            i = x;
            while ((unsigned) i < table->subtableZ[i].next) {
                i = table->subtableZ[i].next;
            }
	    final_group_size = i - x + 1;

            if (init_group_size == final_group_size) {
		/* No new symmetries detected,
		   go back to best position */
                result = cuddZddSymmSiftingBackward(table, move_down,
		    initial_size);
            }
	    else {
		while (move_up != NULL) {
		    move = move_up->next;
		    cuddDeallocNode(table, (DdNode *)move_up);
		    move_up = move;
		}
		initial_size = table->keysZ;
		move_up = cuddZddSymmSifting_up(table, x, x_low,
		    initial_size);
		result = cuddZddSymmSiftingBackward(table, move_up,
		    initial_size);
	    }
	}
	else {
	    result = cuddZddSymmSiftingBackward(table, move_down,
		initial_size);
	    /* move backward and stop at best position */
	}
	if (!result)
	    goto cuddZddSymmSiftingConvAuxOutOfMem;
    }

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

    return(1);

cuddZddSymmSiftingConvAuxOutOfMem:
    if (move_down != ZDD_MV_OOM) {
	while (move_down != NULL) {
	    move = move_down->next;
	    cuddDeallocNode(table, (DdNode *)move_down);
	    move_down = move;
	}
    }
    if (move_up != ZDD_MV_OOM) {
	while (move_up != NULL) {
	    move = move_up->next;
	    cuddDeallocNode(table, (DdNode *)move_up);
	    move_up = move;
	}
    }

    return(0);

} /* end of cuddZddSymmSiftingConvAux */


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

  Synopsis [Moves x up until either it reaches the bound (x_low) or
  the size of the ZDD heap increases too much.]

  Description [Moves x up until either it reaches the bound (x_low) or
  the size of the ZDD heap increases too much. Assumes that x is the top
  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; ZDD_MV_OOM if memory is full.]

  SideEffects [None]

  SeeAlso     []

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

    moves = NULL;
    y = cuddZddNextLow(table, x);
    while (y >= x_low) {
	gytop = table->subtableZ[y].next;
	if (cuddZddSymmCheck(table, y, x)) {
	    /* Symmetry found, attach symm groups */
	    table->subtableZ[y].next = x;
	    i = table->subtableZ[x].next;
	    while (table->subtableZ[i].next != (unsigned) x)
		i = table->subtableZ[i].next;
	    table->subtableZ[i].next = gytop;
	}
	else if ((table->subtableZ[x].next == (unsigned) x) &&
	    (table->subtableZ[y].next == (unsigned) y)) {
	    /* x and y have self symmetry */
	    size = cuddZddSwapInPlace(table, y, x);
	    if (size == 0)
		goto cuddZddSymmSifting_upOutOfMem;
	    move = (Move *)cuddDynamicAllocNode(table);
	    if (move == NULL)
		goto cuddZddSymmSifting_upOutOfMem;
	    move->x = y;
	    move->y = x;
	    move->size = size;
	    move->next = moves;
	    moves = move;
	    if ((double)size >
		(double)limit_size * table->maxGrowth)
		return(moves);
	    if (size < limit_size)
		limit_size = size;
	}
	else { /* Group move */
	    size = zdd_group_move(table, y, x, &moves);
	    if ((double)size >
		(double)limit_size * table->maxGrowth)
		return(moves);
	    if (size < limit_size)
		limit_size = size;
	}
	x = gytop;
	y = cuddZddNextLow(table, x);
    }

    return(moves);

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

} /* end of cuddZddSymmSifting_up */


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

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

  Description [Moves x down until either it reaches the bound (x_high)
  or the size of the ZDD 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; ZDD_MV_OOM if memory is full.]

  SideEffects [None]

  SeeAlso     []

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

    moves = NULL;
    y = cuddZddNextHigh(table, x);
    while (y <= x_high) {
	gybot = table->subtableZ[y].next;
	while (table->subtableZ[gybot].next != (unsigned) y)
	    gybot = table->subtableZ[gybot].next;
	if (cuddZddSymmCheck(table, x, y)) {
	    /* Symmetry found, attach symm groups */
	    gxtop = table->subtableZ[x].next;
	    table->subtableZ[x].next = y;
	    i = table->subtableZ[y].next;
	    while (table->subtableZ[i].next != (unsigned) y)
		i = table->subtableZ[i].next;
	    table->subtableZ[i].next = gxtop;
	}
	else if ((table->subtableZ[x].next == (unsigned) x) &&
	    (table->subtableZ[y].next == (unsigned) y)) {
	    /* x and y have self symmetry */
	    size = cuddZddSwapInPlace(table, x, y);
	    if (size == 0)
		goto cuddZddSymmSifting_downOutOfMem;
	    move = (Move *)cuddDynamicAllocNode(table);
	    if (move == NULL)
		goto cuddZddSymmSifting_downOutOfMem;
	    move->x = x;
	    move->y = y;
	    move->size = size;
	    move->next = moves;
	    moves = move;
	    if ((double)size >
		(double)limit_size * table->maxGrowth)
		return(moves);
	    if (size < limit_size)
		limit_size = size;
	    x = y;
	    y = cuddZddNextHigh(table, x);
	}
	else { /* Group move */
	    size = zdd_group_move(table, x, y, &moves);
	    if ((double)size >
		(double)limit_size * table->maxGrowth)
		return(moves);
	    if (size < limit_size)
		limit_size = size;
	}
	x = gybot;
	y = cuddZddNextHigh(table, x);
    }

    return(moves);

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

} /* end of cuddZddSymmSifting_down */


/**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
cuddZddSymmSiftingBackward(
  DdManager * table,
  Move * moves,
  int  size)
{
    int		i;
    int		i_best;
    Move	*move;
    int		res;

    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;
	if ((table->subtableZ[move->x].next == move->x) &&
	    (table->subtableZ[move->y].next == move->y)) {
	    res = cuddZddSwapInPlace(table, move->x, move->y);
	    if (!res) return(0);
	}
	else { /* Group move necessary */
	    res = zdd_group_move_backward(table, move->x, move->y);
	}
	if (i_best == -1 && res == size)
	    break;
    }

    return(1);

} /* end of cuddZddSymmSiftingBackward */


/**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]

  SeeAlso     []

******************************************************************************/
static int
zdd_group_move(
  DdManager * table,
  int  x,
  int  y,
  Move ** moves)
{
    Move	*move;
    int		size;
    int		i, temp, gxtop, gxbot, gytop, gybot, yprev;
    int		swapx, swapy;

#ifdef DD_DEBUG
    assert(x < y);	/* we assume that x < y */
#endif
    /* Find top and bottom for the two groups. */
    gxtop = table->subtableZ[x].next;
    gytop = y;
    gxbot = x;
    gybot = table->subtableZ[y].next;
    while (table->subtableZ[gybot].next != (unsigned) y)
	gybot = table->subtableZ[gybot].next;
    yprev = gybot;

    while (x <= y) {
	while (y > gxtop) {
	    /* Set correct symmetries. */
	    temp = table->subtableZ[x].next;
	    if (temp == x)
		temp = y;
	    i = gxtop;
	    for (;;) {
		if (table->subtableZ[i].next == (unsigned) x) {
		    table->subtableZ[i].next = y;
		    break;
		} else {
		    i = table->subtableZ[i].next;
		}
	    }
	    if (table->subtableZ[y].next != (unsigned) y) {
		table->subtableZ[x].next = table->subtableZ[y].next;
	    } else {
		table->subtableZ[x].next = x;
	    }

	    if (yprev != y) {
		table->subtableZ[yprev].next = x;
	    } else {
		yprev = x;
	    }
	    table->subtableZ[y].next = temp;

	    size = cuddZddSwapInPlace(table, x, y);
	    if (size == 0)
		goto zdd_group_moveOutOfMem;
            swapx = x;
	    swapy = y;
	    y = x;
	    x--;
	} /* while y > gxtop */

	/* Trying to find the next y. */
	if (table->subtableZ[y].next <= (unsigned) y) {
	    gybot = y;
	} else {
	    y = table->subtableZ[y].next;
	}

	yprev = gxtop;
	gxtop++;
	gxbot++;
	x = gxbot;
    } /* while x <= y, end of group movement */
    move = (Move *)cuddDynamicAllocNode(table);
    if (move == NULL)
	goto zdd_group_moveOutOfMem;
    move->x = swapx;
    move->y = swapy;
    move->size = table->keysZ;
    move->next = *moves;
    *moves = move;

    return(table->keysZ);

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

} /* end of zdd_group_move */


/**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 1 if successful; 0 otherwise.]

  SideEffects [None]

  SeeAlso     []

******************************************************************************/
static int
zdd_group_move_backward(
  DdManager * table,
  int  x,
  int  y)
{
    int	       size;
    int        i, temp, gxtop, gxbot, gytop, gybot, yprev;

#ifdef DD_DEBUG
    assert(x < y);	/* we assume that x < y */
#endif
    /* Find top and bottom of the two groups. */
    gxtop = table->subtableZ[x].next;
    gytop = y;
    gxbot = x;
    gybot = table->subtableZ[y].next;
    while (table->subtableZ[gybot].next != (unsigned) y)
	gybot = table->subtableZ[gybot].next;
    yprev = gybot;

    while (x <= y) {
	while (y > gxtop) {
	    /* Set correct symmetries. */
	    temp = table->subtableZ[x].next;
	    if (temp == x)
		temp = y;
	    i = gxtop;
	    for (;;) {
		if (table->subtableZ[i].next == (unsigned) x) {
		    table->subtableZ[i].next = y;
		    break;
		} else {
		    i = table->subtableZ[i].next;
		}
	    }
	    if (table->subtableZ[y].next != (unsigned) y) {
		table->subtableZ[x].next = table->subtableZ[y].next;
	    } else {
		table->subtableZ[x].next = x;
	    }

	    if (yprev != y) {
		table->subtableZ[yprev].next = x;
	    } else {
		yprev = x;
	    }
	    table->subtableZ[y].next = temp;

	    size = cuddZddSwapInPlace(table, x, y);
	    if (size == 0)
		return(0);
	    y = x;
	    x--;
	} /* while y > gxtop */

	/* Trying to find the next y. */
	if (table->subtableZ[y].next <= (unsigned) y) {
	    gybot = y;
	} else {
	    y = table->subtableZ[y].next;
	}

	yprev = gxtop;
	gxtop++;
	gxbot++;
	x = gxbot;
    } /* while x <= y, end of group movement backward */

    return(size);

} /* end of zdd_group_move_backward */


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

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

  Description []

  SideEffects [None]

******************************************************************************/
static void
cuddZddSymmSummary(
  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->subtableZ[i].next != (unsigned) i) {
	    TotalSymmGroups++;
	    x = i;
	    do {
		TotalSymm++;
		gbot = x;
		x = table->subtableZ[x].next;
	    } while (x != i);
#ifdef DD_DEBUG
	    assert(table->subtableZ[gbot].next == (unsigned) i);
#endif
	    i = gbot;
	}
    }
    *symvars = TotalSymm;
    *symgroups = TotalSymmGroups;

    return;

} /* end of cuddZddSymmSummary */