cuddzddreord.c

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

	    f01 = cuddT(f0); f00 = cuddE(f0);
	} else {
	    f01 = empty; f00 = f0;
	}

	/* Decrease ref count of f1. */
	cuddSatDec(f1->ref);
	/* Create the new T child. */
	if (f11 == empty) {
	    if (f01 != empty) {
		newf1 = f01;
		cuddSatInc(newf1->ref);
	    }
	    /* else case was already handled when finding nodes
	    ** with both children below level y
	    */
	} else {
	    /* Check xlist for triple (xindex, f11, f01). */
	    posn = ddHash(f11, f01, xshift);
	    /* For each element newf1 in collision list xlist[posn]. */
	    newf1 = xlist[posn];
	    while (newf1 != NULL) {
		if (cuddT(newf1) == f11 && cuddE(newf1) == f01) {
		    cuddSatInc(newf1->ref);
		    break; /* match */
		}
		newf1 = newf1->next;
	    } /* while newf1 */
	    if (newf1 == NULL) {	/* no match */
		newf1 = cuddDynamicAllocNode(table);
		if (newf1 == NULL)
		    goto zddSwapOutOfMem;
		newf1->index = xindex; newf1->ref = 1;
		cuddT(newf1) = f11;
		cuddE(newf1) = f01;
		/* Insert newf1 in the collision list xlist[pos];
		** increase the ref counts of f11 and f01
		*/
		newxkeys++;
		newf1->next = xlist[posn];
		xlist[posn] = newf1;
		cuddSatInc(f11->ref);
		cuddSatInc(f01->ref);
	    }
	}
	cuddT(f) = newf1;

	/* Do the same for f0. */
	/* Decrease ref count of f0. */
	cuddSatDec(f0->ref);
	/* Create the new E child. */
	if (f10 == empty) {
	    newf0 = f00;
	    cuddSatInc(newf0->ref);
	} else {
	    /* Check xlist for triple (xindex, f10, f00). */
	    posn = ddHash(f10, f00, xshift);
	    /* For each element newf0 in collision list xlist[posn]. */
	    newf0 = xlist[posn];
	    while (newf0 != NULL) {
		if (cuddT(newf0) == f10 && cuddE(newf0) == f00) {
		    cuddSatInc(newf0->ref);
		    break; /* match */
		}
		newf0 = newf0->next;
	    } /* while newf0 */
	    if (newf0 == NULL) {	/* no match */
		newf0 = cuddDynamicAllocNode(table);
		if (newf0 == NULL)
		    goto zddSwapOutOfMem;
		newf0->index = xindex; newf0->ref = 1;
		cuddT(newf0) = f10; cuddE(newf0) = f00;
		/* Insert newf0 in the collision list xlist[posn];
		** increase the ref counts of f10 and f00.
		*/
		newxkeys++;
		newf0->next = xlist[posn];
		xlist[posn] = newf0;
		cuddSatInc(f10->ref);
		cuddSatInc(f00->ref);
	    }
	}
	cuddE(f) = newf0;

	/* Insert the modified f in ylist.
	** The modified f does not already exists in ylist.
	** (Because of the uniqueness of the cofactors.)
	*/
	posn = ddHash(newf1, newf0, yshift);
	newykeys++;
	f->next = ylist[posn];
	ylist[posn] = f;
	f = next;
    } /* while f != NULL */

    /* GC the y layer. */

    /* For each node f in ylist. */
    for (i = 0; i < yslots; i++) {
	previousP = &(ylist[i]);
	f = *previousP;
	while (f != NULL) {
	    next = f->next;
	    if (f->ref == 0) {
		cuddSatDec(cuddT(f)->ref);
		cuddSatDec(cuddE(f)->ref);
		cuddDeallocNode(table, f);
		newykeys--;
	    } else {
		*previousP = f;
		previousP = &(f->next);
	    }
	    f = next;
	} /* while f */
	*previousP = NULL;
    } /* for i */

    /* Set the appropriate fields in table. */
    table->subtableZ[x].nodelist = ylist;
    table->subtableZ[x].slots    = yslots;
    table->subtableZ[x].shift    = yshift;
    table->subtableZ[x].keys     = newykeys;
    table->subtableZ[x].maxKeys  = yslots * DD_MAX_SUBTABLE_DENSITY;

    table->subtableZ[y].nodelist = xlist;
    table->subtableZ[y].slots    = xslots;
    table->subtableZ[y].shift    = xshift;
    table->subtableZ[y].keys     = newxkeys;
    table->subtableZ[y].maxKeys  = xslots * DD_MAX_SUBTABLE_DENSITY;

    table->permZ[xindex] = y; table->permZ[yindex] = x;
    table->invpermZ[x] = yindex; table->invpermZ[y] = xindex;

    table->keysZ += newxkeys + newykeys - oldxkeys - oldykeys;

    /* Update univ section; univ[x] remains the same. */
    table->univ[y] = cuddT(table->univ[x]);

    return (table->keysZ);

zddSwapOutOfMem:
    (void) fprintf(table->err, "Error: cuddZddSwapInPlace out of memory\n");

    return (0);

} /* end of cuddZddSwapInPlace */


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

  Synopsis    [Reorders variables by a sequence of (non-adjacent) swaps.]

  Description [Implementation of Plessier's algorithm that reorders
  variables by a sequence of (non-adjacent) swaps.
    <ol>
    <li> Select two variables (RANDOM or HEURISTIC).
    <li> Permute these variables.
    <li> If the nodes have decreased accept the permutation.
    <li> Otherwise reconstruct the original heap.
    <li> Loop.
    </ol>
  Returns 1 in case of success; 0 otherwise.]

  SideEffects [None]

  SeeAlso     []

******************************************************************************/
int
cuddZddSwapping(
  DdManager * table,
  int lower,
  int upper,
  Cudd_ReorderingType heuristic)
{
    int	i, j;
    int max, keys;
    int nvars;
    int	x, y;
    int iterate;
    int previousSize;
    Move *moves, *move;
    int	pivot;
    int modulo;
    int result;

#ifdef DD_DEBUG
    /* Sanity check */
    assert(lower >= 0 && upper < table->sizeZ && lower <= upper);
#endif

    nvars = upper - lower + 1;
    iterate = nvars;

    for (i = 0; i < iterate; i++) {
	if (heuristic == CUDD_REORDER_RANDOM_PIVOT) {
	    /* Find pivot <= id with maximum keys. */
	    for (max = -1, j = lower; j <= upper; j++) {
		if ((keys = table->subtableZ[j].keys) > max) {
		    max = keys;
		    pivot = j;
		}
	    }

	    modulo = upper - pivot;
	    if (modulo == 0) {
		y = pivot;	/* y = nvars-1 */
	    } else {
		/* y = random # from {pivot+1 .. nvars-1} */
		y = pivot + 1 + (int) (Cudd_Random() % modulo);
	    }

	    modulo = pivot - lower - 1;
	    if (modulo < 1) {	/* if pivot = 1 or 0 */
		x = lower;
	    } else {
		do { /* x = random # from {0 .. pivot-2} */
		    x = (int) Cudd_Random() % modulo;
		} while (x == y);
		  /* Is this condition really needed, since x and y
		     are in regions separated by pivot? */
	    }
	} else {
	    x = (int) (Cudd_Random() % nvars) + lower;
	    do {
		y = (int) (Cudd_Random() % nvars) + lower;
	    } while (x == y);
	}

	previousSize = table->keysZ;
	moves = zddSwapAny(table, x, y);
	if (moves == NULL)
	    goto cuddZddSwappingOutOfMem;

	result = cuddZddSiftingBackward(table, moves, previousSize);
	if (!result)
	    goto cuddZddSwappingOutOfMem;

	while (moves != NULL) {
	    move = moves->next;
	    cuddDeallocNode(table, (DdNode *) moves);
	    moves = move;
	}
#ifdef DD_STATS
	if (table->keysZ < (unsigned) previousSize) {
	    (void) fprintf(table->out,"-");
	} else if (table->keysZ > (unsigned) previousSize) {
	    (void) fprintf(table->out,"+");	/* should never happen */
	} else {
	    (void) fprintf(table->out,"=");
	}
	fflush(table->out);
#endif
    }

    return(1);

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

} /* end of cuddZddSwapping */


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

  Synopsis    [Implementation of Rudell's sifting algorithm.]

  Description [Implementation of Rudell's sifting algorithm.
  Assumes that no dead nodes are present.
    <ol>
    <li> Order all the variables according to the number of entries
    in each unique table.
    <li> Sift the variable up and down, remembering each time the
    total size of the DD heap.
    <li> Select the best permutation.
    <li> Repeat 3 and 4 for all variables.
    </ol>
  Returns 1 if successful; 0 otherwise.]

  SideEffects [None]

  SeeAlso     []

******************************************************************************/
int
cuddZddSifting(
  DdManager * table,
  int  lower,
  int  upper)
{
    int	i;
    int	*var;
    int	size;
    int	x;
    int	result;
#ifdef DD_STATS
    int	previousSize;
#endif

    size = table->sizeZ;

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

    for (i = 0; i < size; i++) {
	x = table->permZ[i];
	zdd_entry[i] = table->subtableZ[x].keys;
	var[i] = i;
    }

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

    /* Now sift. */
    for (i = 0; i < ddMin(table->siftMaxVar, size); i++) {
	if (zddTotalNumberSwapping >= table->siftMaxSwap)
	    break;
	x = table->permZ[var[i]];
	if (x < lower || x > upper) continue;
#ifdef DD_STATS
	previousSize = table->keysZ;
#endif
	result = cuddZddSiftingAux(table, x, lower, upper);
	if (!result)
	    goto cuddZddSiftingOutOfMem;
#ifdef DD_STATS
	if (table->keysZ < (unsigned) previousSize) {
	    (void) fprintf(table->out,"-");
	} else if (table->keysZ > (unsigned) previousSize) {
	    (void) fprintf(table->out,"+");	/* should never happen */
	    (void) fprintf(table->out,"\nSize increased from %d to %d while sifting variable %d\n", previousSize, table->keysZ , var[i]);
	} else {
	    (void) fprintf(table->out,"=");
	}
	fflush(table->out);
#endif
    }

    FREE(var);
    FREE(zdd_entry);

    return(1);

cuddZddSiftingOutOfMem:

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

    return(0);

} /* end of cuddZddSifting */


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


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

  Synopsis    [Swaps any two variables.]

  Description [Swaps any two variables. Returns the set of moves.]

  SideEffects [None]

  SeeAlso     []

******************************************************************************/
static Move *
zddSwapAny(
  DdManager * table,
  int  x,
  int  y)
{
    Move	*move, *moves;
    int		tmp, size;
    int		x_ref, y_ref;
    int		x_next, y_next;
    int		limit_size;

    if (x > y) {	/* make x precede y */
	tmp = x; x = y;	y = tmp;
    }

    x_ref = x; y_ref = y;

    x_next = cuddZddNextHigh(table, x);
    y_next = cuddZddNextLow(table, y);
    moves = NULL;
    limit_size = table->keysZ;

    for (;;) {
	if (x_next == y_next) {	/* x < x_next = y_next < y */
	    size = cuddZddSwapInPlace(table, x, x_next);
	    if (size == 0)
		goto zddSwapAnyOutOfMem;
	    move = (Move *) cuddDynamicAllocNode(table);
	    if (move == NULL)
		goto zddSwapAnyOutOfMem;
	    move->x = x;
	    move->y = x_next;
	    move->size = size;
	    move->next = moves;
	    moves = move;

	    size = cuddZddSwapInPlace(table, y_next, y);
	    if (size == 0)
		goto zddSwapAnyOutOfMem;
	    move = (Move *)cuddDynamicAllocNode(table);
	    if (move == NULL)
		goto zddSwapAnyOutOfMem;
	    move->x = y_next;
	    move->y = y;
	    move->size = size;
	    move->next = moves;
	    moves = move;

	    size = cuddZddSwapInPlace(table, x, x_next);
	    if (size == 0)
		goto zddSwapAnyOutOfMem;
	    move = (Move *)cuddDynamicAllocNode(table);
	    if (move == NULL)
		goto zddSwapAnyOutOfMem;
	    move->x = x;
	    move->y = x_next;
	    move->size = size;
	    move->next = moves;
	    moves = move;

	    tmp = x; x = y; y = tmp;

	} else if (x == y_next) { /* x = y_next < y = x_next */
	    size = cuddZddSwapInPlace(table, x, x_next);
	    if (size == 0)
		goto zddSwapAnyOutOfMem;
	    move = (Move *)cuddDynamicAllocNode(table);
	    if (move == NULL)
		goto zddSwapAnyOutOfMem;
	    move->x = x;
	    move->y = x_next;
	    move->size = size;
	    move->next = moves;
	    moves = move;

	    tmp = x; x = y;  y = tmp;
	} else {
	    size = cuddZddSwapInPlace(table, x, x_next);
	    if (size == 0)
		goto zddSwapAnyOutOfMem;
	    move = (Move *)cuddDynamicAllocNode(table);
	    if (move == NULL)
		goto zddSwapAnyOutOfMem;
	    move->x = x;
	    move->y = x_next;
	    move->size = size;
	    move->next = moves;
	    moves = move;

	    size = cuddZddSwapInPlace(table, y_next, y);
	    if (size == 0)
		goto zddSwapAnyOutOfMem;
	    move = (Move *)cuddDynamicAllocNode(table);
	    if (move == NULL)
		goto zddSwapAnyOutOfMem;
	    move->x = y_next;
	    move->y = y;
	    move->size = size;
	    move->next = moves;
	    moves = move;

	    x = x_next; y = y_next;
	}

	x_next = cuddZddNextHigh(table, x);
	y_next = cuddZddNextLow(table, y);
	if (x_next > y_ref)
	    break;	/* if x == y_ref */

	if ((double) size > table->maxGrowth * (double) limit_size)
	    break;
	if (size < limit_size)
	    limit_size = size;
    }
    if (y_next >= x_ref) {
	size = cuddZddSwapInPlace(table, y_next, y);
	if (size == 0)
	    goto zddSwapAnyOutOfMem;
	move = (Move *)cuddDynamicAllocNode(table);
	if (move == NULL)
	    goto zddSwapAnyOutOfMem;
	move->x = y_next;
	move->y = y;
	move->size = size;
	move->next = moves;
	moves = move;
    }

    return(moves);

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

} /* end of zddSwapAny */


/**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.
  Returns 1 if successful; 0 otherwise.]

  SideEffects [None]

  SeeAlso     []

******************************************************************************/
static int
cuddZddSiftingAux(
  DdManager * table,
  int  x,
  int  x_low,
  int  x_high)