cuddgroup.c

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

  Synopsis    [Creates a group encompassing variables from x to y in the
  DD table.]

  Description [Creates a group encompassing variables from x to y in the
  DD table. In the current implementation it must be y == x+1.
  Returns 1 in case of success; 0 otherwise.]

  SideEffects [None]

******************************************************************************/
static void
ddCreateGroup(
  DdManager * table,
  int  x,
  int  y)
{
    int  gybot;

#ifdef DD_DEBUG
    assert(y == x+1);
#endif

    /* Find bottom of second group. */
    gybot = y;
    while ((unsigned) gybot < table->subtables[gybot].next)
	gybot = table->subtables[gybot].next;

    /* Link groups. */
    table->subtables[x].next = y;
    table->subtables[gybot].next = x;

    return;

} /* ddCreateGroup */


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

  Synopsis    [Sifts one variable up and down until it has taken all
  positions. Checks for aggregation.]

  Description [Sifts one variable up and down until it has taken all
  positions. Checks for aggregation. There may be at most two sweeps,
  even if the group grows.  Assumes that x is either an isolated
  variable, or it is the bottom of a group. All groups may not have
  been found. The variable being moved is returned to the best position
  seen during sifting.  Returns 1 in case of success; 0 otherwise.]

  SideEffects [None]

******************************************************************************/
static int
ddGroupSiftingAux(
  DdManager * table,
  int  x,
  int  xLow,
  int  xHigh,
  int (*checkFunction)(DdManager *, int, int),
  int lazyFlag)
{
    Move *move;
    Move *moves;	/* list of moves */
    int  initialSize;
    int  result;
    int  y;
    int  topbot;

#ifdef DD_DEBUG
    if (pr > 0) (void) fprintf(table->out,
			       "ddGroupSiftingAux from %d to %d\n",xLow,xHigh);
    assert((unsigned) x >= table->subtables[x].next); /* x is bottom of group */
#endif

    initialSize = table->keys - table->isolated;
    moves = NULL;

    originalSize = initialSize;		/* for lazy sifting */

    /* If we have a singleton, we check for aggregation in both
    ** directions before we sift.
    */
    if ((unsigned) x == table->subtables[x].next) {
	/* Will go down first, unless x == xHigh:
	** Look for aggregation above x.
	*/
	for (y = x; y > xLow; y--) {
	    if (!checkFunction(table,y-1,y))
		break;
	    topbot = table->subtables[y-1].next; /* find top of y-1's group */
	    table->subtables[y-1].next = y;
	    table->subtables[x].next = topbot; /* x is bottom of group so its */
					       /* next is top of y-1's group */
	    y = topbot + 1; /* add 1 for y--; new y is top of group */
	}
	/* Will go up first unless x == xlow:
	** Look for aggregation below x.
	*/
	for (y = x; y < xHigh; y++) {
	    if (!checkFunction(table,y,y+1))
		break;
	    /* find bottom of y+1's group */
	    topbot = y + 1;
	    while ((unsigned) topbot < table->subtables[topbot].next) {
		topbot = table->subtables[topbot].next;
	    }
	    table->subtables[topbot].next = table->subtables[y].next;
	    table->subtables[y].next = y + 1;
	    y = topbot - 1; /* subtract 1 for y++; new y is bottom of group */
	}
    }

    /* Now x may be in the middle of a group.
    ** Find bottom of x's group.
    */
    while ((unsigned) x < table->subtables[x].next)
	x = table->subtables[x].next;

    originalLevel = x;			/* for lazy sifting */

    if (x == xLow) { /* Sift down */
#ifdef DD_DEBUG
	/* x must be a singleton */
	assert((unsigned) x == table->subtables[x].next);
#endif
	if (x == xHigh) return(1);	/* just one variable */

        if (!ddGroupSiftingDown(table,x,xHigh,checkFunction,&moves))
            goto ddGroupSiftingAuxOutOfMem;
	/* at this point x == xHigh, unless early term */

	/* move backward and stop at best position */
	result = ddGroupSiftingBackward(table,moves,initialSize,
					DD_SIFT_DOWN,lazyFlag);
#ifdef DD_DEBUG
	assert(table->keys - table->isolated <= (unsigned) initialSize);
#endif
        if (!result) goto ddGroupSiftingAuxOutOfMem;

    } else if (cuddNextHigh(table,x) > xHigh) { /* Sift up */
#ifdef DD_DEBUG
	/* x is bottom of group */
        assert((unsigned) x >= table->subtables[x].next);
#endif
        /* Find top of x's group */
        x = table->subtables[x].next;

        if (!ddGroupSiftingUp(table,x,xLow,checkFunction,&moves))
            goto ddGroupSiftingAuxOutOfMem;
	/* at this point x == xLow, unless early term */

	/* move backward and stop at best position */
	result = ddGroupSiftingBackward(table,moves,initialSize,
					DD_SIFT_UP,lazyFlag);
#ifdef DD_DEBUG
	assert(table->keys - table->isolated <= (unsigned) initialSize);
#endif
        if (!result) goto ddGroupSiftingAuxOutOfMem;

    } else if (x - xLow > xHigh - x) { /* must go down first: shorter */
        if (!ddGroupSiftingDown(table,x,xHigh,checkFunction,&moves))
            goto ddGroupSiftingAuxOutOfMem;
	/* at this point x == xHigh, unless early term */

        /* Find top of group */
	if (moves) {
	    x = moves->y;
	}
	while ((unsigned) x < table->subtables[x].next)
	    x = table->subtables[x].next;
	x = table->subtables[x].next;
#ifdef DD_DEBUG
        /* x should be the top of a group */
        assert((unsigned) x <= table->subtables[x].next);
#endif

        if (!ddGroupSiftingUp(table,x,xLow,checkFunction,&moves))
            goto ddGroupSiftingAuxOutOfMem;

	/* move backward and stop at best position */
	result = ddGroupSiftingBackward(table,moves,initialSize,
					DD_SIFT_UP,lazyFlag);
#ifdef DD_DEBUG
	assert(table->keys - table->isolated <= (unsigned) initialSize);
#endif
        if (!result) goto ddGroupSiftingAuxOutOfMem;

    } else { /* moving up first: shorter */
        /* Find top of x's group */
        x = table->subtables[x].next;

        if (!ddGroupSiftingUp(table,x,xLow,checkFunction,&moves))
            goto ddGroupSiftingAuxOutOfMem;
	/* at this point x == xHigh, unless early term */

        if (moves) {
	    x = moves->x;
	}
	while ((unsigned) x < table->subtables[x].next)
	    x = table->subtables[x].next;
#ifdef DD_DEBUG
        /* x is bottom of a group */
        assert((unsigned) x >= table->subtables[x].next);
#endif

        if (!ddGroupSiftingDown(table,x,xHigh,checkFunction,&moves))
            goto ddGroupSiftingAuxOutOfMem;

	/* move backward and stop at best position */
	result = ddGroupSiftingBackward(table,moves,initialSize,
					DD_SIFT_DOWN,lazyFlag);
#ifdef DD_DEBUG
	assert(table->keys - table->isolated <= (unsigned) initialSize);
#endif
        if (!result) goto ddGroupSiftingAuxOutOfMem;
    }

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

    return(1);

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

    return(0);

} /* end of ddGroupSiftingAux */


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

  Synopsis    [Sifts up a variable until either it reaches position xLow
  or the size of the DD heap increases too much.]

  Description [Sifts up a variable until either it reaches position
  xLow or the size of the DD heap increases too much. Assumes that y is
  the top of a group (or a singleton).  Checks y for aggregation to the
  adjacent variables. Records all the moves that are appended to the
  list of moves received as input and returned as a side effect.
  Returns 1 in case of success; 0 otherwise.]

  SideEffects [None]

******************************************************************************/
static int
ddGroupSiftingUp(
  DdManager * table,
  int  y,
  int  xLow,
  int (*checkFunction)(DdManager *, int, int),
  Move ** moves)
{
    Move *move;
    int  x;
    int  size;
    int  i;
    int  gxtop,gybot;
    int  limitSize;
    int  xindex, yindex;
    int  zindex;
    int  z;
    int  isolated;
    int  L;	/* lower bound on DD size */
#ifdef DD_DEBUG
    int  checkL;
#endif

    yindex = table->invperm[y];

    /* Initialize the lower bound.
    ** The part of the DD below the bottom of y's group will not change.
    ** The part of the DD above y that does not interact with any
    ** variable of y's group will not change.
    ** The rest may vanish in the best case, except for
    ** the nodes at level xLow, which will not vanish, regardless.
    ** What we use here is not really a lower bound, because we ignore
    ** the interactions with all variables except y.
    */
    limitSize = L = table->keys - table->isolated;
    gybot = y;
    while ((unsigned) gybot < table->subtables[gybot].next)
	gybot = table->subtables[gybot].next;
    for (z = xLow + 1; z <= gybot; z++) {
	zindex = table->invperm[z];
	if (zindex == yindex || cuddTestInteract(table,zindex,yindex)) {
	    isolated = table->vars[zindex]->ref == 1;
	    L -= table->subtables[z].keys - isolated;
	}
    }

    originalLevel = y;			/* for lazy sifting */

    x = cuddNextLow(table,y);
    while (x >= xLow && L <= limitSize) {
#ifdef DD_DEBUG
	gybot = y;
	while ((unsigned) gybot < table->subtables[gybot].next)
	    gybot = table->subtables[gybot].next;
	checkL = table->keys - table->isolated;
	for (z = xLow + 1; z <= gybot; z++) {
	    zindex = table->invperm[z];
	    if (zindex == yindex || cuddTestInteract(table,zindex,yindex)) {
		isolated = table->vars[zindex]->ref == 1;
		checkL -= table->subtables[z].keys - isolated;
	    }
	}
	if (pr > 0 && L != checkL) {
	    (void) fprintf(table->out,
			   "Inaccurate lower bound: L = %d checkL = %d\n",
			   L, checkL);
	}
#endif
        gxtop = table->subtables[x].next;
        if (checkFunction(table,x,y)) {
	    /* Group found, attach groups */
	    table->subtables[x].next = y;
	    i = table->subtables[y].next;
	    while (table->subtables[i].next != (unsigned) y)
		i = table->subtables[i].next;
	    table->subtables[i].next = gxtop;
	    move = (Move *)cuddDynamicAllocNode(table);
	    if (move == NULL) goto ddGroupSiftingUpOutOfMem;
	    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 */
	    xindex = table->invperm[x];
            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 ddGroupSiftingUpOutOfMem;
	    /* Update the lower bound. */
	    if (cuddTestInteract(table,xindex,yindex)) {
		isolated = table->vars[xindex]->ref == 1;
		L += table->subtables[y].keys - isolated;
	    }
            move = (Move *)cuddDynamicAllocNode(table);
            if (move == NULL) goto ddGroupSiftingUpOutOfMem;
            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,
				       "ddGroupSiftingUp (2 single groups):\n");
#endif
            if ((double) size > (double) limitSize * table->maxGrowth)
		return(1);
            if (size < limitSize) limitSize = size;
        } else { /* Group move */
            size = ddGroupMove(table,x,y,moves);
	    if (size == 0) goto ddGroupSiftingUpOutOfMem;
	    /* Update the lower bound. */
	    z = (*moves)->y;
	    do {
		zindex = table->invperm[z];
		if (cuddTestInteract(table,zindex,yindex)) {
		    isolated = table->vars[zindex]->ref == 1;
		    L += table->subtables[z].keys - isolated;
		}
		z = table->subtables[z].next;
	    } while (z != (int) (*moves)->y);
            if ((double) size > (double) limitSize * table->maxGrowth)
		return(1);
            if (size < limitSize) limitSize = size;
        }
        y = gxtop;
        x = cuddNextLow(table,y);
    }

    return(1);

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

} /* end of ddGroupSiftingUp */


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

  Synopsis    [Sifts down a variable until it reaches position xHigh.]

  Description [Sifts down a variable until it reaches position xHigh.
  Assumes that x is the bottom of a group (or a singleton).  Records
  all the moves.  Returns 1 in case of success; 0 otherwise.]

  SideEffects [None]

******************************************************************************/
static int
ddGroupSiftingDown(
  DdManager * table,
  int  x,
  int  xHigh,
  int (*checkFunction)(DdManager *, int, int),
  Move ** moves)
{
    Move *move;
    int  y;
    int  size;
    int  limitSize;
    int  gxtop,gybot;
    int  R;	/* upper bound on node decrease */
    int  xindex, yindex;
    int  isolated, allVars;
    int  z;
    int  zindex;