cuddlinear.c

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

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

    return(0);

} /* end of ddLinearAndSiftingAux */


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

  Synopsis    [Sifts a variable up and applies linear transformations.]

  Description [Sifts a variable up and applies linear transformations.
  Moves y up until either it reaches the bound (xLow) 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 *
ddLinearAndSiftingUp(
  DdManager * table,
  int  y,
  int  xLow,
  Move * prevMoves)
{
    Move	*moves;
    Move	*move;
    int		x;
    int		size, newsize;
    int		limitSize;
    int		xindex, yindex;
    int		isolated;
    int		L;	/* lower bound on DD size */
#ifdef DD_DEBUG
    int checkL;
    int z;
    int zindex;
#endif

    moves = prevMoves;
    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;
	if (L != checkL) {
	    (void) fprintf(table->out, "checkL(%d) != L(%d)\n",checkL,L);
	}
#endif
	size = cuddSwapInPlace(table,x,y);
	if (size == 0) goto ddLinearAndSiftingUpOutOfMem;
	newsize = cuddLinearInPlace(table,x,y);
	if (newsize == 0) goto ddLinearAndSiftingUpOutOfMem;
	move = (Move *) cuddDynamicAllocNode(table);
	if (move == NULL) goto ddLinearAndSiftingUpOutOfMem;
	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 = cuddLinearInPlace(table,x,y);
	    if (newsize == 0) goto ddLinearAndSiftingUpOutOfMem;
#ifdef DD_DEBUG
	    if (newsize != size) {
		(void) fprintf(table->out,"Change in size after identity transformation! From %d to %d\n",size,newsize);
	    }
#endif
	} else if (cuddTestInteract(table,xindex,yindex)) {
	    size = newsize;
	    move->flags = CUDD_LINEAR_TRANSFORM_MOVE;
	    ddUpdateInteractionMatrix(table,xindex,yindex);
	}
	move->size = size;
	/* Update the lower bound. */
	if (cuddTestInteract(table,xindex,yindex)) {
	    isolated = table->vars[xindex]->ref == 1;
	    L += table->subtables[y].keys - isolated;
	}
	if ((double) size > (double) limitSize * table->maxGrowth) break;
	if (size < limitSize) limitSize = size;
	y = x;
	x = cuddNextLow(table,y);
    }
    return(moves);

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

} /* end of ddLinearAndSiftingUp */
    

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

  Synopsis    [Sifts a variable down and applies linear transformations.]

  Description [Sifts a variable down and applies linear
  transformations. 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 *
ddLinearAndSiftingDown(
  DdManager * table,
  int  x,
  int  xHigh,
  Move * prevMoves)
{
    Move	*moves;
    Move	*move;
    int		y;
    int		size, newsize;
    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 = prevMoves;
    /* 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;
	    }
	}
	if (R != checkR) {
	    (void) fprintf(table->out, "checkR(%d) != R(%d)\n",checkR,R);
	}
#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 ddLinearAndSiftingDownOutOfMem; 
	newsize = cuddLinearInPlace(table,x,y);
	if (newsize == 0) goto ddLinearAndSiftingDownOutOfMem;
	move = (Move *) cuddDynamicAllocNode(table);
	if (move == NULL) goto ddLinearAndSiftingDownOutOfMem;
	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 = cuddLinearInPlace(table,x,y);
	    if (newsize == 0) goto ddLinearAndSiftingDownOutOfMem;
	    if (newsize != size) {
		(void) fprintf(table->out,"Change in size after identity transformation! From %d to %d\n",size,newsize);
	    }
	} else if (cuddTestInteract(table,xindex,yindex)) {
	    size = newsize;
	    move->flags = CUDD_LINEAR_TRANSFORM_MOVE;
	    ddUpdateInteractionMatrix(table,xindex,yindex);
	}
	move->size = size;
	if ((double) size > (double) limitSize * table->maxGrowth) break;
	if (size < limitSize) limitSize = size;
	x = y;
	y = cuddNextHigh(table,x);
    }
    return(moves);

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

} /* end of ddLinearAndSiftingDown */


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

  Synopsis    [Given a set of moves, returns the DD heap to the order
  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
ddLinearAndSiftingBackward(
  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);
	if (move->flags == CUDD_LINEAR_TRANSFORM_MOVE) {
	    res = cuddLinearInPlace(table,(int)move->x,(int)move->y);
	    if (!res) return(0);
	}
	res = cuddSwapInPlace(table,(int)move->x,(int)move->y);
	if (!res) return(0);
	if (move->flags == CUDD_INVERSE_TRANSFORM_MOVE) {
	    res = cuddLinearInPlace(table,(int)move->x,(int)move->y);
	    if (!res) return(0);
	}
    }

    return(1);

} /* end of ddLinearAndSiftingBackward */


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

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

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

  SideEffects [None]

******************************************************************************/
static Move*
ddUndoMoves(
  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 ddUndoMovesOutOfMem;
	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 = cuddSwapInPlace(table,(int)move->x,(int)move->y);
	    if (!size) goto ddUndoMovesOutOfMem;
	} else if (move->flags == CUDD_LINEAR_TRANSFORM_MOVE) {
	    invmove->flags = CUDD_INVERSE_TRANSFORM_MOVE;
	    size = cuddLinearInPlace(table,(int)move->x,(int)move->y);
	    if (!size) goto ddUndoMovesOutOfMem;
	    size = cuddSwapInPlace(table,(int)move->x,(int)move->y);
	    if (!size) goto ddUndoMovesOutOfMem;
	} 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 = cuddSwapInPlace(table,(int)move->x,(int)move->y);
	    if (!size) goto ddUndoMovesOutOfMem;
	    size = cuddLinearInPlace(table,(int)move->x,(int)move->y);
	    if (!size) goto ddUndoMovesOutOfMem;
	}
	invmove->size = size;
    }

    return(invmoves);

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

} /* end of ddUndoMoves */


/**Function********************************************************************
 
  Synopsis    [Linearly combines two adjacent variables.]

  Description [Linearly combines two adjacent variables. Specifically,
  replaces the top variable with the exclusive nor of the two variables.
  It assumes that no dead nodes are present on entry to this
  procedure.  The procedure then guarantees that no dead nodes will be
  present when it terminates.  cuddLinearInPlace assumes that x &lt;
  y.  Returns the number of keys in the table if successful; 0
  otherwise.]

  SideEffects [The two subtables corrresponding to variables x and y are
  modified. The global counters of the unique table are also affected.]

  SeeAlso     [cuddSwapInPlace]

******************************************************************************/
static int
cuddLinearInPlace(
  DdManager * table,
  int  x,
  int  y)
{
    DdNodePtr *xlist, *ylist;
    int    xindex, yindex;
    int    xslots, yslots;
    int    xshift, yshift;
    int    oldxkeys, oldykeys;
    int    newxkeys, newykeys;
    int    comple, newcomplement;
    int    i;
    int    posn;
    int    isolated;
    DdNode *f,*f0,*f1,*f01,*f00,*f11,*f10,*newf1,*newf0;
    DdNode *g,*next,*last;
    DdNodePtr *previousP;
    DdNode *tmp;
    DdNode *sentinel = &(table->sentinel);
#if DD_DEBUG
    int    count, idcheck;
#endif

#ifdef DD_DEBUG
    assert(x < y);
    assert(cuddNextHigh(table,x) == y);
    assert(table->subtables[x].keys != 0);
    assert(table->subtables[y].keys != 0);
    assert(table->subtables[x].dead == 0);
    assert(table->subtables[y].dead == 0);
#endif

    xindex = table->invperm[x];
    yindex = table->invperm[y];

    if (cuddTestInteract(table,xindex,yindex)) {
#ifdef DD_STATS
	ddTotalNumberLinearTr++;
#endif
	/* Get parameters of x subtable. */
	xlist = table->subtables[x].nodelist; 
	oldxkeys = table->subtables[x].keys;
	xslots = table->subtables[x].slots;
	xshift = table->subtables[x].shift;

	/* Get parameters of y subtable. */
	ylist = table->subtables[y].nodelist;
	oldykeys = table->subtables[y].keys;
	yslots = table->subtables[y].slots;
	yshift = table->subtables[y].shift;

	newxkeys = 0;
	newykeys = oldykeys;

	/* Check whether the two projection functions involved in this
	** swap are isolated. At the end, we'll be able to tell how many
	** isolated projection functions are there by checking only these
	** two functions again. This is done to eliminate the isolated
	** projection functions from the node count.
	*/
	isolated = - ((table->vars[xindex]->ref == 1) +
		     (table->vars[yindex]->ref == 1));

	/* The nodes in the x layer are put in a chain.
	** The chain is handled as a FIFO; g points to the beginning and
	** last points to the end.
	*/