cuddzddgroup.c

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

	    } while (result != 0);
	    break;
	case CUDD_REORDER_SYMM_SIFT:
	    result = cuddZddSymmSifting(table,lower,upper);
	    break;
	case CUDD_REORDER_SYMM_SIFT_CONV:
	    result = cuddZddSymmSiftingConv(table,lower,upper);
	    break;
	case CUDD_REORDER_GROUP_SIFT:
	    result = zddGroupSifting(table,lower,upper);
	    break;
	case CUDD_REORDER_LINEAR:
	    result = cuddZddLinearSifting(table,lower,upper);
	    break;
	case CUDD_REORDER_LINEAR_CONVERGE:
	    do {
		initialSize = table->keysZ;
		result = cuddZddLinearSifting(table,lower,upper);
		if (initialSize <= table->keysZ)
		    break;
#ifdef DD_STATS
		else
		    (void) fprintf(table->out,"\n");
#endif
	    } while (result != 0);
	    break;
	default:
	    return(0);
	}
    }

    /* Create a single group for all the variables that were sifted,
    ** so that they will be treated as a single block by successive
    ** invocations of zddGroupSifting.
    */
    zddMergeGroups(table,treenode,lower,upper);

#ifdef DD_DEBUG
    if (pr > 0) (void) fprintf(table->out,"zddReorderChildren:");
#endif

    return(result);

} /* end of zddReorderChildren */


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

  Synopsis    [Finds the lower and upper bounds of the group represented
  by treenode.]

  Description [Finds the lower and upper bounds of the group represented
  by treenode.  The high and low fields of treenode are indices.  From
  those we need to derive the current positions, and find maximum and
  minimum.]

  SideEffects [The bounds are returned as side effects.]

  SeeAlso     []

******************************************************************************/
static void
zddFindNodeHiLo(
  DdManager * table,
  MtrNode * treenode,
  int * lower,
  int * upper)
{
    int low;
    int high;

    /* Check whether no variables in this group already exist.
    ** If so, return immediately. The calling procedure will know from
    ** the values of upper that no reordering is needed.
    */
    if ((int) treenode->low >= table->sizeZ) {
	*lower = table->sizeZ;
	*upper = -1;
	return;
    }

    *lower = low = (unsigned int) table->permZ[treenode->index];
    high = (int) (low + treenode->size - 1);

    if (high >= table->sizeZ) {
	/* This is the case of a partially existing group. The aim is to
	** reorder as many variables as safely possible.  If the tree
	** node is terminal, we just reorder the subset of the group
	** that is currently in existence.  If the group has
	** subgroups, then we only reorder those subgroups that are
	** fully instantiated.  This way we avoid breaking up a group.
	*/
	MtrNode *auxnode = treenode->child;
	if (auxnode == NULL) {
	    *upper = (unsigned int) table->sizeZ - 1;
	} else {
	    /* Search the subgroup that strands the table->sizeZ line.
	    ** If the first group starts at 0 and goes past table->sizeZ
	    ** upper will get -1, thus correctly signaling that no reordering
	    ** should take place.
	    */
	    while (auxnode != NULL) {
		int thisLower = table->permZ[auxnode->low];
		int thisUpper = thisLower + auxnode->size - 1;
		if (thisUpper >= table->sizeZ && thisLower < table->sizeZ)
		    *upper = (unsigned int) thisLower - 1;
		auxnode = auxnode->younger;
	    }
	}
    } else {
	/* Normal case: All the variables of the group exist. */
	*upper = (unsigned int) high;
    }

#ifdef DD_DEBUG
    /* Make sure that all variables in group are contiguous. */
    assert(treenode->size >= *upper - *lower + 1);
#endif

    return;

} /* end of zddFindNodeHiLo */


/**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
zddUniqueCompareGroup(
  int * ptrX,
  int * ptrY)
{
#if 0
    if (entry[*ptrY] == entry[*ptrX]) {
	return((*ptrX) - (*ptrY));
    }
#endif
    return(entry[*ptrY] - entry[*ptrX]);

} /* end of zddUniqueCompareGroup */


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

  Synopsis    [Sifts from treenode->low to treenode->high.]

  Description [Sifts from treenode->low to treenode->high. If
  croupcheck == CUDD_GROUP_CHECK7, it checks for group creation at the
  end of the initial sifting. If a group is created, it is then sifted
  again. After sifting one variable, the group that contains it is
  dissolved.  Returns 1 in case of success; 0 otherwise.]

  SideEffects [None]

******************************************************************************/
static int
zddGroupSifting(
  DdManager * table,
  int  lower,
  int  upper)
{
    int		*var;
    int		i,j,x,xInit;
    int		nvars;
    int		classes;
    int		result;
    int		*sifted;
#ifdef DD_STATS
    unsigned	previousSize;
#endif
    int		xindex;

    nvars = table->sizeZ;

    /* Order variables to sift. */
    entry = NULL;
    sifted = NULL;
    var = ALLOC(int,nvars);
    if (var == NULL) {
	table->errorCode = CUDD_MEMORY_OUT;
	goto zddGroupSiftingOutOfMem;
    }
    entry = ALLOC(int,nvars);
    if (entry == NULL) {
	table->errorCode = CUDD_MEMORY_OUT;
	goto zddGroupSiftingOutOfMem;
    }
    sifted = ALLOC(int,nvars);
    if (sifted == NULL) {
	table->errorCode = CUDD_MEMORY_OUT;
	goto zddGroupSiftingOutOfMem;
    }

    /* Here we consider only one representative for each group. */
    for (i = 0, classes = 0; i < nvars; i++) {
	sifted[i] = 0;
	x = table->permZ[i];
	if ((unsigned) x >= table->subtableZ[x].next) {
	    entry[i] = table->subtableZ[x].keys;
	    var[classes] = i;
	    classes++;
	}
    }

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

    /* Now sift. */
    for (i = 0; i < ddMin(table->siftMaxVar,classes); i++) {
	if (zddTotalNumberSwapping >= table->siftMaxSwap)
	    break;
	xindex = var[i];
	if (sifted[xindex] == 1) /* variable already sifted as part of group */
	    continue;
        x = table->permZ[xindex]; /* find current level of this variable */
	if (x < lower || x > upper)
	    continue;
#ifdef DD_STATS
	previousSize = table->keysZ;
#endif
#ifdef DD_DEBUG
	/* x is bottom of group */
        assert((unsigned) x >= table->subtableZ[x].next);
#endif
	result = zddGroupSiftingAux(table,x,lower,upper);
	if (!result) goto zddGroupSiftingOutOfMem;

#ifdef DD_STATS
	if (table->keysZ < previousSize) {
	    (void) fprintf(table->out,"-");
	} else if (table->keysZ > previousSize) {
	    (void) fprintf(table->out,"+");
	} else {
	    (void) fprintf(table->out,"=");
	}
	fflush(table->out);
#endif

	/* Mark variables in the group just sifted. */
	x = table->permZ[xindex];
	if ((unsigned) x != table->subtableZ[x].next) {
	    xInit = x;
	    do {
		j = table->invpermZ[x];
		sifted[j] = 1;
		x = table->subtableZ[x].next;
	    } while (x != xInit);
	}

#ifdef DD_DEBUG
	if (pr > 0) (void) fprintf(table->out,"zddGroupSifting:");
#endif
    } /* for */

    FREE(sifted);
    FREE(var);
    FREE(entry);

    return(1);

zddGroupSiftingOutOfMem:
    if (entry != NULL)	FREE(entry);
    if (var != NULL)	FREE(var);
    if (sifted != NULL)	FREE(sifted);

    return(0);

} /* end of zddGroupSifting */


/**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
zddGroupSiftingAux(
  DdManager * table,
  int  x,
  int  xLow,
  int  xHigh)
{
    Move *move;
    Move *moves;	/* list of moves */
    int  initialSize;
    int  result;


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

    initialSize = table->keysZ;
    moves = NULL;

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

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

	/* move backward and stop at best position */
	result = zddGroupSiftingBackward(table,moves,initialSize);
#ifdef DD_DEBUG
	assert(table->keysZ <= (unsigned) initialSize);
#endif
        if (!result) goto zddGroupSiftingAuxOutOfMem;

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

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

	/* move backward and stop at best position */
	result = zddGroupSiftingBackward(table,moves,initialSize);
#ifdef DD_DEBUG
	assert(table->keysZ <= (unsigned) initialSize);
#endif
        if (!result) goto zddGroupSiftingAuxOutOfMem;

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

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

        if (!zddGroupSiftingUp(table,x,xLow,&moves))
            goto zddGroupSiftingAuxOutOfMem;

	/* move backward and stop at best position */
	result = zddGroupSiftingBackward(table,moves,initialSize);
#ifdef DD_DEBUG
	assert(table->keysZ <= (unsigned) initialSize);
#endif
        if (!result) goto zddGroupSiftingAuxOutOfMem;

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

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

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

        if (!zddGroupSiftingDown(table,x,xHigh,&moves))
            goto zddGroupSiftingAuxOutOfMem;

	/* move backward and stop at best position */
	result = zddGroupSiftingBackward(table,moves,initialSize);
#ifdef DD_DEBUG
	assert(table->keysZ <= (unsigned) initialSize);
#endif
        if (!result) goto zddGroupSiftingAuxOutOfMem;
    }

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

    return(1);

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

    return(0);

} /* end of zddGroupSiftingAux */


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