cuddsymmetry.c

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

    int		symgroups;
    int		classes;
    int		initialSize;
#ifdef DD_STATS
    int		previousSize;
#endif

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

    size = table->size;

    /* Find order in which to sift variables. */
    var = NULL;
    entry = ALLOC(int,size);
    if (entry == NULL) {
	table->errorCode = CUDD_MEMORY_OUT;
	goto ddSymmSiftingConvOutOfMem;
    }
    var = ALLOC(int,size);
    if (var == NULL) {
	table->errorCode = CUDD_MEMORY_OUT;
	goto ddSymmSiftingConvOutOfMem;
    }

    for (i = 0; i < size; i++) {
	x = table->perm[i];
	entry[i] = table->subtables[x].keys;
	var[i] = i;
    }

    qsort((void *)var,size,sizeof(int),(int (*)(const void *, const void *))ddSymmUniqueCompare);

    /* Initialize the symmetry of each subtable to itself
    ** for first pass of converging symmetric sifting.
    */
    for (i = lower; i <= upper; i++) {
	table->subtables[i].next = i;
    }

    for (i = 0; i < ddMin(table->siftMaxVar, table->size); i++) {
	if (ddTotalNumberSwapping >= table->siftMaxSwap)
	    break;
	x = table->perm[var[i]];
	if (x < lower || x > upper) continue;
	/* Only sift if not in symmetry group already. */
	if (table->subtables[x].next == (unsigned) x) {
#ifdef DD_STATS
	    previousSize = table->keys - table->isolated;
#endif
	    result = ddSymmSiftingAux(table,x,lower,upper);
	    if (!result) goto ddSymmSiftingConvOutOfMem;
#ifdef DD_STATS
	    if (table->keys < (unsigned) previousSize + table->isolated) {
		(void) fprintf(table->out,"-");
	    } else if (table->keys > (unsigned) previousSize +
		       table->isolated) {
		(void) fprintf(table->out,"+");
	    } else {
		(void) fprintf(table->out,"=");
	    }
	    fflush(table->out);
#endif
	}
    }

    /* Sifting now until convergence. */
    while ((unsigned) initialSize > table->keys - table->isolated) {
	initialSize = table->keys - table->isolated;
#ifdef DD_STATS
	(void) fprintf(table->out,"\n");
#endif
        /* Here we consider only one representative for each symmetry class. */
	for (x = lower, classes = 0; x <= upper; x++, classes++) {
	    while ((unsigned) x < table->subtables[x].next) {
		x = table->subtables[x].next;
	    }
	    /* Here x is the largest index in a group.
	    ** Groups consist of adjacent variables.
	    ** Hence, the next increment of x will move it to a new group.
	    */
	    i = table->invperm[x];
	    entry[i] = table->subtables[x].keys;
	    var[classes] = i;
	}

	qsort((void *)var,classes,sizeof(int),(int (*)(const void *, const void *))ddSymmUniqueCompare);

	/* Now sift. */
	for (i = 0; i < ddMin(table->siftMaxVar,classes); i++) {
	    if (ddTotalNumberSwapping >= table->siftMaxSwap)
		break;
	    x = table->perm[var[i]];
	    if ((unsigned) x >= table->subtables[x].next) {
#ifdef DD_STATS
		previousSize = table->keys - table->isolated;
#endif
		result = ddSymmSiftingConvAux(table,x,lower,upper);
		if (!result ) goto ddSymmSiftingConvOutOfMem;
#ifdef DD_STATS
		if (table->keys < (unsigned) previousSize + table->isolated) {
		    (void) fprintf(table->out,"-");
		} else if (table->keys > (unsigned) previousSize +
			   table->isolated) {
		    (void) fprintf(table->out,"+");
		} else {
		    (void) fprintf(table->out,"=");
		}
		fflush(table->out);
#endif
	    }
	} /* for */
    }

    ddSymmSummary(table, lower, upper, &symvars, &symgroups);

#ifdef DD_STATS
    (void) fprintf(table->out, "\n#:S_SIFTING %8d: symmetric variables\n",
		   symvars);
    (void) fprintf(table->out, "#:G_SIFTING %8d: symmetric groups",
		   symgroups);
#endif

    FREE(var);
    FREE(entry);

    return(1+symvars);

ddSymmSiftingConvOutOfMem:

    if (entry != NULL) FREE(entry);
    if (var != NULL) FREE(var);

    return(0);

} /* end of cuddSymmSiftingConv */


/*---------------------------------------------------------------------------*/
/* Definition of static functions                                            */
/*---------------------------------------------------------------------------*/


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

  Synopsis    [Comparison function used by qsort.]

  Description [Comparison function used by qsort to order the variables
  according to the number of keys in the subtables.
  Returns the difference in number of keys between the two
  variables being compared.]

  SideEffects [None]

******************************************************************************/
static int
ddSymmUniqueCompare(
  int * ptrX,
  int * ptrY)
{
#if 0
    if (entry[*ptrY] == entry[*ptrX]) {
	return((*ptrX) - (*ptrY));
    }
#endif
    return(entry[*ptrY] - entry[*ptrX]);

} /* end of ddSymmUniqueCompare */


/**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 not part of a symmetry group. Returns 1 if
  successful; 0 otherwise.]

  SideEffects [None]

******************************************************************************/
static int
ddSymmSiftingAux(
  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  topbot;	/* index to either top or bottom of symmetry group */
    int  initGroupSize, finalGroupSize;


#ifdef DD_DEBUG
    /* check for previously detected symmetry */
    assert(table->subtables[x].next == (unsigned) x);
#endif

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

    moveDown = NULL;
    moveUp = NULL;

    if ((x - xLow) > (xHigh - x)) {
	/* Will go down first, unless x == xHigh:
	** Look for consecutive symmetries above x.
	*/
	for (i = x; i > xLow; i--) {
	    if (!cuddSymmCheck(table,i-1,i))
		break;
	    topbot = table->subtables[i-1].next; /* find top of i-1's group */
	    table->subtables[i-1].next = i;
	    table->subtables[x].next = topbot; /* x is bottom of group so its */
					       /* next is top of i-1's group */
	    i = topbot + 1; /* add 1 for i--; new i is top of symm group */
	}
    } else {
	/* Will go up first unless x == xlow:
	** Look for consecutive symmetries below x.
	*/
	for (i = x; i < xHigh; i++) {
	    if (!cuddSymmCheck(table,i,i+1))
		break;
	    /* find bottom of i+1's symm group */
	    topbot = i + 1;
	    while ((unsigned) topbot < table->subtables[topbot].next) {
		topbot = table->subtables[topbot].next;
	    }
	    table->subtables[topbot].next = table->subtables[i].next;
	    table->subtables[i].next = i + 1;
	    i = topbot - 1; /* subtract 1 for i++; new i is bottom of group */
	}
    }

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

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

	initGroupSize = 1;

	moveDown = ddSymmSiftingDown(table,x,xHigh);
	    /* after this point x --> xHigh, unless early term */
	if (moveDown == MV_OOM) goto ddSymmSiftingAuxOutOfMem;
	if (moveDown == NULL) return(1);

	x = moveDown->y;
	/* Find bottom of x's group */
	i = x;
	while ((unsigned) i < table->subtables[i].next) {
	    i = table->subtables[i].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 symmetry groups detected, return 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 ddSymmSiftingAuxOutOfMem;

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

	if (x == xLow) return(1); /* just one big group */

	initGroupSize = i - x + 1;

	moveUp = ddSymmSiftingUp(table,x,xLow);
	    /* after this point x --> xLow, unless early term */
	if (moveUp == MV_OOM) goto ddSymmSiftingAuxOutOfMem;
	if (moveUp == NULL) return(1);

	x = moveUp->x;
	/* Find top of x's group */
	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 ddSymmSiftingAuxOutOfMem;

    } 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 ddSymmSiftingAuxOutOfMem;

	if (moveDown != NULL) {
	    x = moveDown->y;	/* x is top here */
	    i = x;
	    while ((unsigned) i < table->subtables[i].next) {
		i = table->subtables[i].next;
	    }
	} else {
	    i = x;
	    while ((unsigned) i < table->subtables[i].next) {
		i = table->subtables[i].next;
	    }
	    x = table->subtables[i].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 ddSymmSiftingAuxOutOfMem;

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

    } 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 ddSymmSiftingAuxOutOfMem;

	if (moveUp != NULL) {
	    x = moveUp->x;
	    i = table->subtables[x].next;
	} else {
	    while ((unsigned) x < table->subtables[x].next)
		x = table->subtables[x].next;
	    i = 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 ddSymmSiftingAuxOutOfMem;

	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