cuddsymmetry.c

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

	finalGroupSize = i - x + 1;

	if (initGroupSize == finalGroupSize) {
	    /* No new symmetries detected, go back to best position */
	    result = ddSymmSiftingBackward(table,moveDown,initialSize);
	} else {
	    while (moveUp != NULL) {
		move = moveUp->next;
		cuddDeallocNode(table, (DdNode *) moveUp);
		moveUp = move;
	    }
	    initialSize = table->keys - table->isolated;
	    moveUp = ddSymmSiftingUp(table,x,xLow);
	    result = ddSymmSiftingBackward(table,moveUp,initialSize);
	}
	if (!result) goto ddSymmSiftingAuxOutOfMem;
    }

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

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

    return(0);

} /* end of ddSymmSiftingAux */


/**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.
  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]

******************************************************************************/
static int
ddSymmSiftingConvAux(
  DdManager * table,
  int  x,
  int  xLow,
  int  xHigh)
{
    Move *move;
    Move *moveUp;	/* list of up moves */
    Move *moveDown;	/* list of down moves */
    int	 initialSize;
    int	 result;
    int  i;
    int  initGroupSize, finalGroupSize;


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

    moveDown = NULL;
    moveUp = NULL;

    if (x == xLow) { /* Sift down */
#ifdef DD_DEBUG
	/* x is bottom of symmetry group */
	assert((unsigned) x >= table->subtables[x].next);
#endif
        i = table->subtables[x].next;
	initGroupSize = x - i + 1;

	moveDown = ddSymmSiftingDown(table,x,xHigh);
	/* at this point x == xHigh, unless early term */
	if (moveDown == MV_OOM) goto ddSymmSiftingConvAuxOutOfMem;
	if (moveDown == NULL) return(1);

	x = moveDown->y;
	i = x;
	while ((unsigned) i < table->subtables[i].next) {
	    i = table->subtables[i].next;
	}
#ifdef DD_DEBUG
	/* x should be the top of the symmetric group and i the bottom */
	assert((unsigned) i >= table->subtables[i].next);
	assert((unsigned) x == table->subtables[i].next);
#endif
	finalGroupSize = i - x + 1;

	if (initGroupSize == finalGroupSize) {
	    /* No new symmetries detected, go back to best position */
	    result = ddSymmSiftingBackward(table,moveDown,initialSize);
	} else {
	    initialSize = table->keys - table->isolated;
	    moveUp = ddSymmSiftingUp(table,x,xLow);
	    result = ddSymmSiftingBackward(table,moveUp,initialSize);
	}
	if (!result) goto ddSymmSiftingConvAuxOutOfMem;

    } else if (cuddNextHigh(table,x) > xHigh) { /* Sift up */
	/* Find top of x's symm group */
	while ((unsigned) x < table->subtables[x].next)
	    x = table->subtables[x].next;
	i = x;				/* bottom */
	x = table->subtables[x].next;	/* top */

	if (x == xLow) return(1);

	initGroupSize = i - x + 1;

	moveUp = ddSymmSiftingUp(table,x,xLow);
	    /* at this point x == xLow, unless early term */
	if (moveUp == MV_OOM) goto ddSymmSiftingConvAuxOutOfMem;
	if (moveUp == NULL) return(1);

	x = moveUp->x;
	i = table->subtables[x].next;
#ifdef DD_DEBUG
	/* x should be the bottom of the symmetry group and i the top */
	assert((unsigned) x >= table->subtables[x].next);
	assert((unsigned) i == table->subtables[x].next);
#endif
	finalGroupSize = x - i + 1;

	if (initGroupSize == finalGroupSize) {
	    /* No new symmetry groups detected, return to best position */
	    result = ddSymmSiftingBackward(table,moveUp,initialSize);
	} else {
	    initialSize = table->keys - table->isolated;
	    moveDown = ddSymmSiftingDown(table,x,xHigh);
	    result = ddSymmSiftingBackward(table,moveDown,initialSize);
	}
	if (!result)
	    goto ddSymmSiftingConvAuxOutOfMem;

    } else if ((x - xLow) > (xHigh - x)) { /* must go down first: shorter */
	moveDown = ddSymmSiftingDown(table,x,xHigh);
	    /* at this point x == xHigh, unless early term */
	if (moveDown == MV_OOM) goto ddSymmSiftingConvAuxOutOfMem;

	if (moveDown != NULL) {
	    x = moveDown->y;
	    i = x;
	    while ((unsigned) i < table->subtables[i].next) {
		i = table->subtables[i].next;
	    }
	} else {
	    while ((unsigned) x < table->subtables[x].next)
		x = table->subtables[x].next;
	    i = x;
	    x = table->subtables[x].next;
	}
#ifdef DD_DEBUG
        /* x should be the top of the symmetry group and i the bottom */
	assert((unsigned) i >= table->subtables[i].next);
	assert((unsigned) x == table->subtables[i].next);
#endif
	initGroupSize = i - x + 1;

	moveUp = ddSymmSiftingUp(table,x,xLow);
	if (moveUp == MV_OOM) goto ddSymmSiftingConvAuxOutOfMem;

	if (moveUp != NULL) {
	    x = moveUp->x;
	    i = table->subtables[x].next;
	} else {
	    i = x;
	    while ((unsigned) x < table->subtables[x].next)
		x = table->subtables[x].next;
	}
#ifdef DD_DEBUG
	/* x should be the bottom of the symmetry group and i the top */
	assert((unsigned) x >= table->subtables[x].next);
	assert((unsigned) i == table->subtables[x].next);
#endif
	finalGroupSize = x - i + 1;

	if (initGroupSize == finalGroupSize) {
	    /* No new symmetry groups detected, return to best position */
	    result = ddSymmSiftingBackward(table,moveUp,initialSize);
	} else {
	    while (moveDown != NULL) {
		move = moveDown->next;
		cuddDeallocNode(table, (DdNode *) moveDown);
		moveDown = move;
	    }
	    initialSize = table->keys - table->isolated;
	    moveDown = ddSymmSiftingDown(table,x,xHigh);
	    result = ddSymmSiftingBackward(table,moveDown,initialSize);
	}
	if (!result) goto ddSymmSiftingConvAuxOutOfMem;

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

	moveUp = ddSymmSiftingUp(table,x,xLow);
	/* at this point x == xHigh, unless early term */
	if (moveUp == MV_OOM) goto ddSymmSiftingConvAuxOutOfMem;

	if (moveUp != NULL) {
	    x = moveUp->x;
	    i = table->subtables[x].next;
	} else {
	    i = x;
	    while ((unsigned) x < table->subtables[x].next)
		x = table->subtables[x].next;
	}
#ifdef DD_DEBUG
        /* x is bottom of the symmetry group and i is top */
        assert((unsigned) x >= table->subtables[x].next);
        assert((unsigned) i == table->subtables[x].next);
#endif
        initGroupSize = x - i + 1;

	moveDown = ddSymmSiftingDown(table,x,xHigh);
	if (moveDown == MV_OOM) goto ddSymmSiftingConvAuxOutOfMem;

	if (moveDown != NULL) {
	    x = moveDown->y;
	    i = x;
	    while ((unsigned) i < table->subtables[i].next) {
		i = table->subtables[i].next;
	    }
	} else {
	    i = x;
	    x = table->subtables[x].next;
	}
#ifdef DD_DEBUG
	/* x should be the top of the symmetry group and i the bottom */
	assert((unsigned) i >= table->subtables[i].next);
	assert((unsigned) x == table->subtables[i].next);
#endif
	finalGroupSize = i - x + 1;

	if (initGroupSize == finalGroupSize) {
	    /* No new symmetries detected, go back to best position */
	    result = ddSymmSiftingBackward(table,moveDown,initialSize);
	} else {
	    while (moveUp != NULL) {
		move = moveUp->next;
		cuddDeallocNode(table, (DdNode *) moveUp);
		moveUp = move;
	    }
	    initialSize = table->keys - table->isolated;
	    moveUp = ddSymmSiftingUp(table,x,xLow);
	    result = ddSymmSiftingBackward(table,moveUp,initialSize);
	}
	if (!result) goto ddSymmSiftingConvAuxOutOfMem;
    }

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

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

    return(0);

} /* end of ddSymmSiftingConvAux */


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

  Synopsis    [Moves x up until either it reaches the bound (xLow) or
  the size of the DD heap increases too much.]

  Description [Moves x up until either it reaches the bound (xLow) or
  the size of the DD heap increases too much. Assumes that x is the top
  of a symmetry group.  Checks x for symmetry to the adjacent
  variables. If symmetry is found, the symmetry group of x is merged
  with the symmetry group of the other variable. Returns the set of
  moves in case of success; MV_OOM if memory is full.]

  SideEffects [None]

******************************************************************************/
static Move *
ddSymmSiftingUp(
  DdManager * table,
  int  y,
  int  xLow)
{
    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


    moves = NULL;
    yindex = table->invperm[y];

    /* Initialize the lower bound.
    ** The part of the DD below the bottom of y' group 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;
    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;
	}
    }

    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;
	    }
	}
	assert(L == checkL);
#endif
	gxtop = table->subtables[x].next;
	if (cuddSymmCheck(table,x,y)) {
	    /* Symmetry found, attach symm 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;
	} else if (table->subtables[x].next == (unsigned) x &&
		   table->subtables[y].next == (unsigned) y) {
	    /* x and y have self symmetry */
	    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 ddSymmSiftingUpOutOfMem;
	    /* 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 ddSymmSiftingUpOutOfMem;
	    move->x = x;
	    move->y = y;
	    move->size = size;
	    move->next = moves;
	    moves = move;
	    if ((double) size > (double) limitSize * table->maxGrowth)
		return(moves);
	    if (size < limitSize) limitSize = size;
	} else { /* Group move */
	    size = ddSymmGroupMove(table,x,y,&moves);