cuddzddlin.c

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

		    newf1 = newf1->next;
		} /* while newf1 */
		if (newf1 == NULL) {	/* no match */
		    newf1 = cuddDynamicAllocNode(table);
		    if (newf1 == NULL)
			goto zddSwapOutOfMem;
		    newf1->index = yindex; newf1->ref = 1;
		    cuddT(newf1) = f1; cuddE(newf1) = empty;
		    /* Insert newf1 in the collision list ylist[posn];
		    ** increase the ref counts of f1 and empty.
		    */
		    newykeys++;
		    newf1->next = ylist[posn];
		    ylist[posn] = newf1;
		    if (posn == i && previous == NULL)
			previous = newf1;
		    cuddSatInc(f1->ref);
		    cuddSatInc(empty->ref);
		}
		cuddT(f) = newf1;
		f0 = cuddE(f);
		/* Insert f in x list. */
		posn = ddHash(newf1, f0, xshift);
		newxkeys++;
		newykeys--;
		f->next = xlist[posn];
		xlist[posn] = f;
	    } else {
		previous = f;
	    }
	    f = next;
	} /* while f */
    } /* for i */

    /* Set the appropriate fields in table. */
    table->subtableZ[x].keys     = newxkeys;
    table->subtableZ[y].keys     = newykeys;

    table->keysZ += newxkeys + newykeys - oldxkeys - oldykeys;

    /* Update univ section; univ[x] remains the same. */
    table->univ[y] = cuddT(table->univ[x]);

#if 0
    (void) fprintf(table->out,"x = %d  y = %d\n", x, y);
    (void) Cudd_DebugCheck(table);
    (void) Cudd_CheckKeys(table);
#endif

    return (table->keysZ);

zddSwapOutOfMem:
    (void) fprintf(table->err, "Error: cuddZddSwapInPlace out of memory\n");

    return (0);

} /* end of cuddZddLinearInPlace */


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

  Synopsis    [Given xLow <= x <= xHigh moves x up and down between the
  boundaries.]

  Description [Given xLow <= x <= xHigh moves x up and down between the
  boundaries. Finds the best position and does the required changes.
  Returns 1 if successful; 0 otherwise.]

  SideEffects [None]

  SeeAlso     []

******************************************************************************/
static int
cuddZddLinearAux(
  DdManager * table,
  int  x,
  int  xLow,
  int  xHigh)
{
    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 == xLow) {
	moveDown = cuddZddLinearDown(table, x, xHigh, NULL);
	/* At this point x --> xHigh. */
	if (moveDown == (Move *) CUDD_OUT_OF_MEM)
	    goto cuddZddLinearAuxOutOfMem;
	/* Move backward and stop at best position. */
	result = cuddZddLinearBackward(table, initial_size, moveDown);
	if (!result)
	    goto cuddZddLinearAuxOutOfMem;

    } else if (x == xHigh) {
	moveUp = cuddZddLinearUp(table, x, xLow, NULL);
	/* At this point x --> xLow. */
	if (moveUp == (Move *) CUDD_OUT_OF_MEM)
	    goto cuddZddLinearAuxOutOfMem;
	/* Move backward and stop at best position. */
	result = cuddZddLinearBackward(table, initial_size, moveUp);
	if (!result)
	    goto cuddZddLinearAuxOutOfMem;

    } else if ((x - xLow) > (xHigh - x)) { /* must go down first: shorter */
	moveDown = cuddZddLinearDown(table, x, xHigh, NULL);
	/* At this point x --> xHigh. */
	if (moveDown == (Move *) CUDD_OUT_OF_MEM)
	    goto cuddZddLinearAuxOutOfMem;
	moveUp = cuddZddUndoMoves(table,moveDown);
#ifdef DD_DEBUG
	assert(moveUp == NULL || moveUp->x == x);
#endif
	moveUp = cuddZddLinearUp(table, x, xLow, moveUp);
	if (moveUp == (Move *) CUDD_OUT_OF_MEM)
	    goto cuddZddLinearAuxOutOfMem;
	/* Move backward and stop at best position. */
	result = cuddZddLinearBackward(table, initial_size, moveUp);
	if (!result)
	    goto cuddZddLinearAuxOutOfMem;

    } else {
	moveUp = cuddZddLinearUp(table, x, xLow, NULL);
	/* At this point x --> xHigh. */
	if (moveUp == (Move *) CUDD_OUT_OF_MEM)
	    goto cuddZddLinearAuxOutOfMem;
	/* Then move up. */
	moveDown = cuddZddUndoMoves(table,moveUp);
#ifdef DD_DEBUG
	assert(moveDown == NULL || moveDown->y == x);
#endif
	moveDown = cuddZddLinearDown(table, x, xHigh, moveDown);
	if (moveDown == (Move *) CUDD_OUT_OF_MEM)
	    goto cuddZddLinearAuxOutOfMem;
	/* Move backward and stop at best position. */
	result = cuddZddLinearBackward(table, initial_size, moveDown);
	if (!result)
	    goto cuddZddLinearAuxOutOfMem;
    }

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

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

    return(0);

} /* end of cuddZddLinearAux */


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

  Synopsis    [Sifts a variable up applying the XOR transformation.]

  Description [Sifts a variable up applying the XOR
  transformation. Moves y up until either it reaches the bound (xLow)
  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 *
cuddZddLinearUp(
  DdManager * table,
  int  y,
  int  xLow,
  Move * prevMoves)
{
    Move	*moves;
    Move	*move;
    int		x;
    int		size, newsize;
    int		limitSize;

    moves = prevMoves;
    limitSize = table->keysZ;

    x = cuddZddNextLow(table, y);
    while (x >= xLow) {
	size = cuddZddSwapInPlace(table, x, y);
	if (size == 0)
	    goto cuddZddLinearUpOutOfMem;
	newsize = cuddZddLinearInPlace(table, x, y);
	if (newsize == 0)
	    goto cuddZddLinearUpOutOfMem;
	move = (Move *) cuddDynamicAllocNode(table);
	if (move == NULL)
	    goto cuddZddLinearUpOutOfMem;
	move->x = x;
	move->y = y;
	move->next = moves;
	moves = move;
	move->flags = CUDD_SWAP_MOVE;
	if (newsize > size) {
	    /* Undo transformation. The transformation we apply is
	    ** its own inverse. Hence, we just apply the transformation
	    ** again.
	    */
	    newsize = cuddZddLinearInPlace(table,x,y);
	    if (newsize == 0) goto cuddZddLinearUpOutOfMem;
#ifdef DD_DEBUG
	    if (newsize != size) {
		(void) fprintf(table->err,"Change in size after identity transformation! From %d to %d\n",size,newsize);
	    }
#endif
	} else {
	    size = newsize;
	    move->flags = CUDD_LINEAR_TRANSFORM_MOVE;
	}
	move->size = size;

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

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

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

} /* end of cuddZddLinearUp */


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

  Synopsis    [Sifts a variable down and applies the XOR transformation.]

  Description [Sifts a variable down. Moves x down until either it
  reaches the bound (xHigh) 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 *
cuddZddLinearDown(
  DdManager * table,
  int  x,
  int  xHigh,
  Move * prevMoves)
{
    Move	*moves;
    Move	*move;
    int		y;
    int		size, newsize;
    int		limitSize;

    moves = prevMoves;
    limitSize = table->keysZ;

    y = cuddZddNextHigh(table, x);
    while (y <= xHigh) {
	size = cuddZddSwapInPlace(table, x, y);
	if (size == 0)
	    goto cuddZddLinearDownOutOfMem;
	newsize = cuddZddLinearInPlace(table, x, y);
	if (newsize == 0)
	    goto cuddZddLinearDownOutOfMem;
	move = (Move *) cuddDynamicAllocNode(table);
	if (move == NULL)
	    goto cuddZddLinearDownOutOfMem;
	move->x = x;
	move->y = y;
	move->next = moves;
	moves = move;
	move->flags = CUDD_SWAP_MOVE;
	if (newsize > size) {
	    /* Undo transformation. The transformation we apply is
	    ** its own inverse. Hence, we just apply the transformation
	    ** again.
	    */
	    newsize = cuddZddLinearInPlace(table,x,y);
	    if (newsize == 0) goto cuddZddLinearDownOutOfMem;
	    if (newsize != size) {
		(void) fprintf(table->err,"Change in size after identity transformation! From %d to %d\n",size,newsize);
	    }
	} else {
	    size = newsize;
	    move->flags = CUDD_LINEAR_TRANSFORM_MOVE;
	}
	move->size = size;

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

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

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

} /* end of cuddZddLinearDown */


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

    /* Find the minimum size among moves. */
    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 (move->flags == CUDD_LINEAR_TRANSFORM_MOVE) {
	    res = cuddZddLinearInPlace(table,(int)move->x,(int)move->y);
	    if (!res) return(0);
	}
	res = cuddZddSwapInPlace(table, move->x, move->y);
	if (!res)
	    return(0);
	if (move->flags == CUDD_INVERSE_TRANSFORM_MOVE) {
	    res = cuddZddLinearInPlace(table,(int)move->x,(int)move->y);
	    if (!res) return(0);
	}
    }

    return(1);

} /* end of cuddZddLinearBackward */


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

  Synopsis    [Given a set of moves, returns the ZDD heap to the order
  in effect before the moves.]

  Description [Given a set of moves, returns the ZDD heap to the
  order in effect before the moves.  Returns 1 in case of success;
  0 otherwise.]

  SideEffects [None]

******************************************************************************/
static Move*
cuddZddUndoMoves(
  DdManager * table,
  Move * moves)
{
    Move *invmoves = NULL;
    Move *move;
    Move *invmove;
    int	size;

    for (move = moves; move != NULL; move = move->next) {
	invmove = (Move *) cuddDynamicAllocNode(table);
	if (invmove == NULL) goto cuddZddUndoMovesOutOfMem;
	invmove->x = move->x;
	invmove->y = move->y;
	invmove->next = invmoves;
	invmoves = invmove;
	if (move->flags == CUDD_SWAP_MOVE) {
	    invmove->flags = CUDD_SWAP_MOVE;
	    size = cuddZddSwapInPlace(table,(int)move->x,(int)move->y);
	    if (!size) goto cuddZddUndoMovesOutOfMem;
	} else if (move->flags == CUDD_LINEAR_TRANSFORM_MOVE) {
	    invmove->flags = CUDD_INVERSE_TRANSFORM_MOVE;
	    size = cuddZddLinearInPlace(table,(int)move->x,(int)move->y);
	    if (!size) goto cuddZddUndoMovesOutOfMem;
	    size = cuddZddSwapInPlace(table,(int)move->x,(int)move->y);
	    if (!size) goto cuddZddUndoMovesOutOfMem;
	} else { /* must be CUDD_INVERSE_TRANSFORM_MOVE */
#ifdef DD_DEBUG
	    (void) fprintf(table->err,"Unforseen event in ddUndoMoves!\n");
#endif
	    invmove->flags = CUDD_LINEAR_TRANSFORM_MOVE;
	    size = cuddZddSwapInPlace(table,(int)move->x,(int)move->y);
	    if (!size) goto cuddZddUndoMovesOutOfMem;
	    size = cuddZddLinearInPlace(table,(int)move->x,(int)move->y);
	    if (!size) goto cuddZddUndoMovesOutOfMem;
	}
	invmove->size = size;
    }

    return(invmoves);

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

} /* end of cuddZddUndoMoves */