cuddzddsymm.c

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

  Description [Given x_low <= x <= x_high moves x up and down between the
  boundaries. Finds the best position and does the required changes.
  Assumes that x is not part of a symmetry group. Returns 1 if
  successful; 0 otherwise.]

  SideEffects [None]

  SeeAlso     []

******************************************************************************/
static int
cuddZddSymmSiftingAux(
  DdManager * table,
  int  x,
  int  x_low,
  int  x_high)
{
    Move *move;
    Move *move_up;	/* list of up move */
    Move *move_down;	/* list of down move */
    int	 initial_size;
    int	 result;
    int	 i;
    int  topbot;	/* index to either top or bottom of symmetry group */
    int	 init_group_size, final_group_size;

    initial_size = table->keysZ;

    move_down = NULL;
    move_up = NULL;

    /* Look for consecutive symmetries above x. */
    for (i = x; i > x_low; i--) {
	if (!cuddZddSymmCheck(table, i - 1, i))
            break;
	/* find top of i-1's symmetry */
	topbot = table->subtableZ[i - 1].next;
	table->subtableZ[i - 1].next = i;
	table->subtableZ[x].next = topbot;
	/* x is bottom of group so its symmetry is top of i-1's
	   group */
	i = topbot + 1; /* add 1 for i--, new i is top of symm group */
    }
    /* Look for consecutive symmetries below x. */
    for (i = x; i < x_high; i++) {
	if (!cuddZddSymmCheck(table, i, i + 1))
            break;
	/* find bottom of i+1's symm group */
	topbot = i + 1;
	while ((unsigned) topbot < table->subtableZ[topbot].next)
	    topbot = table->subtableZ[topbot].next;

	table->subtableZ[topbot].next = table->subtableZ[i].next;
	table->subtableZ[i].next = i + 1;
	i = topbot - 1; /* add 1 for i++,
			   new i is bottom of symm group */
    }

    /* Now x maybe in the middle of a symmetry group. */
    if (x == x_low) { /* Sift down */
	/* Find bottom of x's symm group */
	while ((unsigned) x < table->subtableZ[x].next)
	    x = table->subtableZ[x].next;

	i = table->subtableZ[x].next;
	init_group_size = x - i + 1;

	move_down = cuddZddSymmSifting_down(table, x, x_high,
	    initial_size);
	/* after that point x --> x_high, unless early term */
	if (move_down == ZDD_MV_OOM)
	    goto cuddZddSymmSiftingAuxOutOfMem;

	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
		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 symmetry groups detected,
		   return to best position */
		result = cuddZddSymmSiftingBackward(table,
		    move_down, initial_size);
	    }
	    else {
		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 cuddZddSymmSiftingAuxOutOfMem;
    }
    else if (x == x_high) { /* Sift up */
	/* Find top of x's symm group */
	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;
	}
	init_group_size = i - x + 1;

	move_up = cuddZddSymmSifting_up(table, x, x_low, initial_size);
	/* after that point x --> x_low, unless early term */
	if (move_up == ZDD_MV_OOM)
	    goto cuddZddSymmSiftingAuxOutOfMem;

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

	    if (init_group_size == final_group_size) {
		/* No new symmetry groups detected,
		   return to best position */
		result = cuddZddSymmSiftingBackward(table, move_up,
		    initial_size);
	    }
	    else {
		initial_size = table->keysZ;
		move_down = cuddZddSymmSifting_down(table, x, x_high,
		    initial_size);
		result = cuddZddSymmSiftingBackward(table, move_down,
		    initial_size);
	    }
	}
	else {
	    result = cuddZddSymmSiftingBackward(table, move_up,
		initial_size);
	    /* move backward and stop at best position */
	}
	if (!result)
	    goto cuddZddSymmSiftingAuxOutOfMem;
    }
    else if ((x - x_low) > (x_high - x)) { /* must go down first:
						shorter */
	/* Find bottom of x's symm group */
	while ((unsigned) x < table->subtableZ[x].next)
	    x = table->subtableZ[x].next;

	move_down = cuddZddSymmSifting_down(table, x, x_high,
	    initial_size);
	/* after that point x --> x_high, unless early term */
	if (move_down == ZDD_MV_OOM)
	    goto cuddZddSymmSiftingAuxOutOfMem;

	if (move_down != NULL) {
	    x = move_down->y;
	}
	else {
	    x = table->subtableZ[x].next;
	}
	i = x;
	while ((unsigned) i < table->subtableZ[i].next) {
	    i = table->subtableZ[i].next;
	}
	init_group_size = i - x + 1;

	move_up = cuddZddSymmSifting_up(table, x, x_low, initial_size);
	if (move_up == ZDD_MV_OOM)
	    goto cuddZddSymmSiftingAuxOutOfMem;

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

	    if (init_group_size == final_group_size) {
		/* No new symmetry groups detected,
		   return to best position */
		result = cuddZddSymmSiftingBackward(table, move_up,
		    initial_size);
	    }
	    else {
		while (move_down != NULL) {
		    move = move_down->next;
		    cuddDeallocNode(table, (DdNode *)move_down);
		    move_down = move;
		}
		initial_size = table->keysZ;
		move_down = cuddZddSymmSifting_down(table, x, x_high,
		    initial_size);
		result = cuddZddSymmSiftingBackward(table, move_down,
		    initial_size);
	    }
	}
	else {
	    result = cuddZddSymmSiftingBackward(table, move_up,
		initial_size);
	    /* move backward and stop at best position */
	}
	if (!result)
	    goto cuddZddSymmSiftingAuxOutOfMem;
    }
    else { /* moving up first:shorter */
        /* Find top of x's symmetry group */
	while ((unsigned) x < table->subtableZ[x].next)
	    x = table->subtableZ[x].next;
	x = table->subtableZ[x].next;

	move_up = cuddZddSymmSifting_up(table, x, x_low, initial_size);
	/* after that point x --> x_high, unless early term */
	if (move_up == ZDD_MV_OOM)
	    goto cuddZddSymmSiftingAuxOutOfMem;

	if (move_up != NULL) {
	    x = move_up->x;
	}
	else {
	    while ((unsigned) x < table->subtableZ[x].next)
		x = table->subtableZ[x].next;
	}
	i = table->subtableZ[x].next;
	init_group_size = x - i + 1;

	move_down = cuddZddSymmSifting_down(table, x, x_high,
	    initial_size);
	if (move_down == ZDD_MV_OOM)
	    goto cuddZddSymmSiftingAuxOutOfMem;

	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 {
		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 cuddZddSymmSiftingAuxOutOfMem;
    }

    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);

cuddZddSymmSiftingAuxOutOfMem:
    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 cuddZddSymmSiftingAux */


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

  Synopsis [Given x_low <= x <= x_high moves x up and down between the
  boundaries.]

  Description [Given x_low <= x <= x_high moves x up and down between the
  boundaries. Finds the best position and does the required changes.
  Assumes that x is either an isolated variable, or it is the bottom of
  a symmetry group. All symmetries may not have been found, because of
  exceeded growth limit. Returns 1 if successful; 0 otherwise.]

  SideEffects [None]

  SeeAlso     []

******************************************************************************/
static int
cuddZddSymmSiftingConvAux(
  DdManager * table,
  int  x,
  int  x_low,
  int  x_high)
{
    Move	*move;
    Move	*move_up;	/* list of up move */
    Move	*move_down;	/* list of down move */
    int		initial_size;
    int		result;
    int		i;
    int		init_group_size, final_group_size;

    initial_size = table->keysZ;

    move_down = NULL;
    move_up = NULL;

    if (x == x_low) { /* Sift down */
        i = table->subtableZ[x].next;
	init_group_size = x - i + 1;

	move_down = cuddZddSymmSifting_down(table, x, x_high,
	    initial_size);
	/* after that point x --> x_high, unless early term */
	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 {
		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;
    }
    else if (x == x_high) { /* Sift up */
	/* Find top of x's symm group */
	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;
	}
	init_group_size = i - x + 1;

	move_up = cuddZddSymmSifting_up(table, x, x_low, initial_size);
	/* after that point x --> x_low, unless early term */
	if (move_up == ZDD_MV_OOM)
	    goto cuddZddSymmSiftingConvAuxOutOfMem;

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

	    if (init_group_size == final_group_size) {
		/* No new symmetry groups detected,
		   return to best position */
		result = cuddZddSymmSiftingBackward(table, move_up,
		    initial_size);
	    }
	    else {
		initial_size = table->keysZ;
		move_down = cuddZddSymmSifting_down(table, x, x_high,
		    initial_size);
		result = cuddZddSymmSiftingBackward(table, move_down,
		    initial_size);
	    }
	}
	else {
	    result = cuddZddSymmSiftingBackward(table, move_up,
		initial_size);
	    /* move backward and stop at best position */
	}
	if (!result)
	    goto cuddZddSymmSiftingConvAuxOutOfMem;
    }
    else if ((x - x_low) > (x_high - x)) { /* must go down first:
						shorter */
	move_down = cuddZddSymmSifting_down(table, x, x_high,
	    initial_size);
	/* after that point x --> x_high */
	if (move_down == ZDD_MV_OOM)
	    goto cuddZddSymmSiftingConvAuxOutOfMem;

	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;
	}
	init_group_size = i - x + 1;

	move_up = cuddZddSymmSifting_up(table, x, x_low, initial_size);
	if (move_up == ZDD_MV_OOM)
	    goto cuddZddSymmSiftingConvAuxOutOfMem;

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

            if (init_group_size == final_group_size) {
		/* No new symmetry groups detected,
		   return to best position */
                result = cuddZddSymmSiftingBackward(table, move_up,
		    initial_size);
            }
	    else {
		while (move_down != NULL) {
		    move = move_down->next;
		    cuddDeallocNode(table, (DdNode *)move_down);
		    move_down = move;
		}
		initial_size = table->keysZ;
		move_down = cuddZddSymmSifting_down(table, x, x_high,
		    initial_size);
		result = cuddZddSymmSiftingBackward(table, move_down,
		    initial_size);
	    }
	}
	else {
	    result = cuddZddSymmSiftingBackward(table, move_up,
		initial_size);
	    /* move backward and stop at best position */
	}
	if (!result)
	    goto cuddZddSymmSiftingConvAuxOutOfMem;
    }
    else { /* moving up first:shorter */
	/* Find top of x's symmetry group */
	x = table->subtableZ[x].next;

	move_up = cuddZddSymmSifting_up(table, x, x_low, initial_size);
	/* after that point x --> x_high, unless early term */
	if (move_up == ZDD_MV_OOM)
	    goto cuddZddSymmSiftingConvAuxOutOfMem;

	if (move_up != NULL) {
	    x = move_up->x;
	}
	else {
	    while ((unsigned) x < table->subtableZ[x].next)
		x = table->subtableZ[x].next;
	}
        i = table->subtableZ[x].next;
        init_group_size = x - i + 1;

	move_down = cuddZddSymmSifting_down(table, x, x_high,
	    initial_size);