cuddgroup.c

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

#ifdef DD_DEBUG
    int  checkR;
#endif

    /* If the group consists of simple variables, there is no point in
    ** sifting it down. This check is redundant if the projection functions
    ** do not have external references, because the computation of the
    ** lower bound takes care of the problem.  It is necessary otherwise to
    ** prevent the sifting down of simple variables. */
    y = x;
    allVars = 1;
    do {
	if (table->subtables[y].keys != 1) {
	    allVars = 0;
	    break;
	}
	y = table->subtables[y].next;
    } while (table->subtables[y].next != (unsigned) x);
    if (allVars)
	return(1);
    
    /* 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;
	}
    }

    originalLevel = x;			/* for lazy sifting */

    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
	/* Find bottom of y group. */
        gybot = table->subtables[y].next;
        while (table->subtables[gybot].next != (unsigned) y)
            gybot = table->subtables[gybot].next;

        if (checkFunction(table,x,y)) {
	    /* Group found: attach groups and record move. */
	    gxtop = table->subtables[x].next;
	    table->subtables[x].next = y;
	    table->subtables[gybot].next = gxtop;
	    move = (Move *)cuddDynamicAllocNode(table);
	    if (move == NULL) goto ddGroupSiftingDownOutOfMem;
	    move->x = x;
	    move->y = y;
	    move->flags = MTR_NEWNODE;
	    move->size = table->keys - table->isolated;
	    move->next = *moves;
	    *moves = move;
        } else if (table->subtables[x].next == (unsigned) x &&
		   table->subtables[y].next == (unsigned) y) {
            /* x and y are self groups */
	    /* 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 ddGroupSiftingDownOutOfMem;

	    /* Record move. */
            move = (Move *) cuddDynamicAllocNode(table);
            if (move == NULL) goto ddGroupSiftingDownOutOfMem;
            move->x = x;
            move->y = y;
	    move->flags = MTR_DEFAULT;
            move->size = size;
            move->next = *moves;
            *moves = move;

#ifdef DD_DEBUG
            if (pr > 0) (void) fprintf(table->out,
				       "ddGroupSiftingDown (2 single groups):\n");
#endif
            if ((double) size > (double) limitSize * table->maxGrowth)
                return(1);
            if (size < limitSize) limitSize = size;

            x = y;
            y = cuddNextHigh(table,x);
        } 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 = ddGroupMove(table,x,y,moves);
            if (size == 0) goto ddGroupSiftingDownOutOfMem;
            if ((double) size > (double) limitSize * table->maxGrowth)
		return(1);
            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(1);

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

    return(0);

} /* end of ddGroupSiftingDown */


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

  Synopsis    [Swaps two groups and records the move.]

  Description [Swaps two groups and records the move. Returns the
  number of keys in the DD table in case of success; 0 otherwise.]

  SideEffects [None]

******************************************************************************/
static int
ddGroupMove(
  DdManager * table,
  int  x,
  int  y,
  Move ** moves)
{
    Move *move;
    int  size;
    int  i,j,xtop,xbot,xsize,ytop,ybot,ysize,newxtop;
    int  swapx,swapy;
#if defined(DD_DEBUG) && defined(DD_VERBOSE)
    int  initialSize,bestSize;
#endif

#if DD_DEBUG
    /* We assume that x < y */
    assert(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;

#if defined(DD_DEBUG) && defined(DD_VERBOSE)
    initialSize = bestSize = table->keys - table->isolated;
#endif
    /* 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) goto ddGroupMoveOutOfMem;
#if defined(DD_DEBUG) && defined(DD_VERBOSE)
	    if (size < bestSize)
		bestSize = size;
#endif
            swapx = x; swapy = y;
            y = x;
            x = cuddNextLow(table,y);
        }
        y = ytop + i;
        x = cuddNextLow(table,y);
    }
#if defined(DD_DEBUG) && defined(DD_VERBOSE)
    if ((bestSize < initialSize) && (bestSize < size))
	(void) fprintf(table->out,"Missed local minimum: initialSize:%d  bestSize:%d  finalSize:%d\n",initialSize,bestSize,size);
#endif

    /* fix groups */
    y = xtop; /* ytop is now where xtop used to be */
    for (i = 0; i < ysize - 1; i++) {
        table->subtables[y].next = cuddNextHigh(table,y);
        y = cuddNextHigh(table,y);
    }
    table->subtables[y].next = xtop; /* y is bottom of its group, join */
                                    /* it to top of its group */
    x = cuddNextHigh(table,y);
    newxtop = x;
    for (i = 0; i < xsize - 1; i++) {
        table->subtables[x].next = cuddNextHigh(table,x);
        x = cuddNextHigh(table,x);
    }
    table->subtables[x].next = newxtop; /* x is bottom of its group, join */
                                    /* it to top of its group */
#ifdef DD_DEBUG
    if (pr > 0) (void) fprintf(table->out,"ddGroupMove:\n");
#endif

    /* Store group move */
    move = (Move *) cuddDynamicAllocNode(table);
    if (move == NULL) goto ddGroupMoveOutOfMem;
    move->x = swapx;
    move->y = swapy;
    move->flags = MTR_DEFAULT;
    move->size = table->keys - table->isolated;
    move->next = *moves;
    *moves = move;

    return(table->keys - table->isolated);

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

} /* end of ddGroupMove */


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

  Synopsis    [Undoes the swap two groups.]

  Description [Undoes the swap two groups.  Returns 1 in case of
  success; 0 otherwise.]

  SideEffects [None]

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


#if DD_DEBUG
    /* We assume that x < y */
    assert(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 = cuddNextLow(table,y);
    }

    /* fix groups */
    y = xtop;
    for (i = 0; i < ysize - 1; i++) {
        table->subtables[y].next = cuddNextHigh(table,y);
        y = cuddNextHigh(table,y);
    }
    table->subtables[y].next = xtop; /* y is bottom of its group, join */
                                    /* to its top */
    x = cuddNextHigh(table,y);
    newxtop = x;
    for (i = 0; i < xsize - 1; i++) {
        table->subtables[x].next = cuddNextHigh(table,x);
        x = cuddNextHigh(table,x);
    }
    table->subtables[x].next = newxtop; /* x is bottom of its group, join */
                                    /* to its top */
#ifdef DD_DEBUG
    if (pr > 0) (void) fprintf(table->out,"ddGroupMoveBackward:\n");
#endif

    return(1);

} /* end of ddGroupMoveBackward */


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

  Synopsis    [Determines the best position for a variables and returns
  it there.]

  Description [Determines the best position for a variables and returns
  it there.  Returns 1 in case of success; 0 otherwise.]

  SideEffects [None]

******************************************************************************/
static int
ddGroupSiftingBackward(
  DdManager * table,
  Move * moves,
  int  size,
  int  upFlag, 
  int  lazyFlag)
{
    Move *move;
    int  res;
    Move *end_move;
    int diff, tmp_diff;
    int index, pairlev;

    if (lazyFlag) {
	end_move = NULL;

	/* Find the minimum size, and the earliest position at which it
        ** was achieved. */
	for (move = moves; move != NULL; move = move->next) {
	    if (move->size < size) {
		size = move->size;
		end_move = move;
	    } else if (move->size == size) {
		if (end_move == NULL) end_move = move;
	    } 
	}

	/* Find among the moves that give minimum size the one that
        ** minimizes the distance from the corresponding variable. */
	if (moves != NULL) {
	    diff = Cudd_ReadSize(table) + 1;
	    index = (upFlag == 1) ? 
		    table->invperm[moves->x] : table->invperm[moves->y];
	    pairlev = table->perm[Cudd_bddReadPairIndex(table, index)];

	    for (move = moves; move != NULL; move = move->next) {
		if (move->size == size) {
		    if (upFlag == 1) {
			tmp_diff = (move->x > pairlev) ? 
				    move->x - pairlev : pairlev - move->x;
		    } else {
			tmp_diff = (move->y > pairlev) ?
				    move->y - pairlev : pairlev - move->y;
		    }
		    if (tmp_diff < diff) {
			diff = tmp_diff;
			end_move = move;
		    } 
		}
	    }
	}
    } else {
	/* Find the minimum size. */
	for (move = moves; move != NULL; move = move->next) {
	    if (move->size < size) {
		size = move->size;
	    } 
	}
    }

    /* In case of lazy sifting, end_move identifies the position at
    ** which we want to stop.  Otherwise, we stop as soon as we meet
    ** the minimum size. */
    for (move = moves; move != NULL; move = move->next) {
	if (lazyFlag) {
	    if (move == end_move) return(1);
	} else {
	    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);
            if (!res) return(0);
#ifdef DD_DEBUG
            if (pr > 0) (void) fprintf(table->out,"ddGroupSiftingBackward:\n");
            assert(table->subtables[move->x].next == move->x);
            assert(table->subtables[move->y].next == move->y);
#endif
        } else { /* Group move necessary */
	    if (move->flags == MTR_NEWNODE) {
		ddDissolveGroup(table,(int)move->x,(int)move->y);
	    } else {
		res = ddGroupMoveBackward(table,(int)move->x,(int)move->y);
		if (!res) return(0);
	    }
        }

    }