cuddreorder.c

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

	    (void) fprintf(table->out,"+");	/* should never happen */
	    (void) fprintf(table->err,"\nSize increased from %d to %d while sifting variable %d\n", previousSize, table->keys - table->isolated, var[i]);
	} else {
	    (void) fprintf(table->out,"=");
	}
	fflush(table->out);
#endif
    }

    FREE(var);
    FREE(entry);

    return(1);

cuddSiftingOutOfMem:

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

    return(0); 

} /* end of cuddSifting */


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

******************************************************************************/
int
cuddSwapping(
  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->size && lower <= upper);
#endif

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

    for (i = 0; i < iterate; i++) {
	if (ddTotalNumberSwapping >= table->siftMaxSwap)
	    break;
	if (heuristic == CUDD_REORDER_RANDOM_PIVOT) {
	    max = -1;
	    for (j = lower; j <= upper; j++) {
		if ((keys = table->subtables[j].keys) > max) {
		    max = keys;
		    pivot = j;
		}
	    }

	    modulo = upper - pivot;
	    if (modulo == 0) {
		y = pivot;
	    } else{
		y = pivot + 1 + ((int) Cudd_Random() % modulo);
	    }

	    modulo = pivot - lower - 1;
	    if (modulo < 1) {
		x = lower;
	    } else{
		do {
		    x = (int) Cudd_Random() % modulo;
		} while (x == y);
	    }
	} else {
	    x = ((int) Cudd_Random() % nvars) + lower;
	    do {
		y = ((int) Cudd_Random() % nvars) + lower;
	    } while (x == y);
	}
	previousSize = table->keys - table->isolated;
	moves = ddSwapAny(table,x,y);
	if (moves == NULL) goto cuddSwappingOutOfMem;
	result = ddSiftingBackward(table,previousSize,moves);
	if (!result) goto cuddSwappingOutOfMem;
	while (moves != NULL) {
	    move = moves->next;
	    cuddDeallocNode(table, (DdNode *) moves);
	    moves = move;
	}
#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,"+");	/* should never happen */
	} else {
	    (void) fprintf(table->out,"=");
	}
	fflush(table->out);
#endif
#if 0
	(void) fprintf(table->out,"#:t_SWAPPING %8d: tmp size\n",
		       table->keys - table->isolated); 
#endif
    }

    return(1);

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

    return(0);

} /* end of cuddSwapping */


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

  Synopsis    [Finds the next subtable with a larger index.]

  Description [Finds the next subtable with a larger index. Returns the
  index.]

  SideEffects [None]

  SeeAlso     [cuddNextLow]

******************************************************************************/
int
cuddNextHigh(
  DdManager * table,
  int  x)
{
    return(x+1);

} /* end of cuddNextHigh */
    

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

  Synopsis    [Finds the next subtable with a smaller index.]

  Description [Finds the next subtable with a smaller index. Returns the
  index.]

  SideEffects [None]

  SeeAlso     [cuddNextHigh]

******************************************************************************/
int
cuddNextLow(
  DdManager * table,
  int  x)
{
    return(x-1);

} /* end of cuddNextLow */


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

  Synopsis    [Swaps two adjacent variables.]

  Description [Swaps two adjacent variables. It assumes that no dead
  nodes are present on entry to this procedure.  The procedure then
  guarantees that no dead nodes will be present when it terminates.
  cuddSwapInPlace assumes that x &lt; y.  Returns the number of keys in
  the table if successful; 0 otherwise.]

  SideEffects [None]

******************************************************************************/
int
cuddSwapInPlace(
  DdManager * table,
  int  x,
  int  y)
{
    DdNodePtr *xlist, *ylist;
    int    xindex, yindex;
    int    xslots, yslots;
    int    xshift, yshift;
    int    oldxkeys, oldykeys;
    int    newxkeys, newykeys;
    int    comple, newcomplement;
    int    i;
    Cudd_VariableType varType;
    Cudd_LazyGroupType groupType;
    int    posn;
    int    isolated;
    DdNode *f,*f0,*f1,*f01,*f00,*f11,*f10,*newf1,*newf0;
    DdNode *g,*next;
    DdNodePtr *previousP;
    DdNode *tmp;
    DdNode *sentinel = &(table->sentinel);
    extern void (*MMoutOfMemory)(long);
    void (*saveHandler)(long);

#if DD_DEBUG
    int    count,idcheck;
#endif

#ifdef DD_DEBUG
    assert(x < y);
    assert(cuddNextHigh(table,x) == y);
    assert(table->subtables[x].keys != 0);
    assert(table->subtables[y].keys != 0);
    assert(table->subtables[x].dead == 0);
    assert(table->subtables[y].dead == 0);
#endif

    ddTotalNumberSwapping++;

    /* Get parameters of x subtable. */
    xindex = table->invperm[x];
    xlist = table->subtables[x].nodelist; 
    oldxkeys = table->subtables[x].keys;
    xslots = table->subtables[x].slots;
    xshift = table->subtables[x].shift;

    /* Get parameters of y subtable. */
    yindex = table->invperm[y];
    ylist = table->subtables[y].nodelist;
    oldykeys = table->subtables[y].keys;
    yslots = table->subtables[y].slots;
    yshift = table->subtables[y].shift;

    if (!cuddTestInteract(table,xindex,yindex)) {
#ifdef DD_STATS
	ddTotalNISwaps++;
#endif
	newxkeys = oldxkeys;
	newykeys = oldykeys;
    } else {
	newxkeys = 0;
	newykeys = oldykeys;

	/* Check whether the two projection functions involved in this
	** swap are isolated. At the end, we'll be able to tell how many
	** isolated projection functions are there by checking only these
	** two functions again. This is done to eliminate the isolated
	** projection functions from the node count.
	*/
	isolated = - ((table->vars[xindex]->ref == 1) +
		     (table->vars[yindex]->ref == 1));

	/* The nodes in the x layer that do not depend on
	** y will stay there; the others are put in a chain.
	** The chain is handled as a LIFO; g points to the beginning.
	*/
	g = NULL;
	if ((oldxkeys >= xslots || (unsigned) xslots == table->initSlots) &&
	    oldxkeys <= DD_MAX_SUBTABLE_DENSITY * xslots) {
	    for (i = 0; i < xslots; i++) {
		previousP = &(xlist[i]);
		f = *previousP;
		while (f != sentinel) {
		    next = f->next;
		    f1 = cuddT(f); f0 = cuddE(f);
		    if (f1->index != (DdHalfWord) yindex &&
			Cudd_Regular(f0)->index != (DdHalfWord) yindex) {
			/* stays */
			newxkeys++;
			*previousP = f;
			previousP = &(f->next);
		    } else {
			f->index = yindex;
			f->next = g;
			g = f;
		    }
		    f = next;
		} /* while there are elements in the collision chain */
		*previousP = sentinel;
	    } /* for each slot of the x subtable */
	} else {		/* resize xlist */
	    DdNode *h = NULL;
	    DdNodePtr *newxlist;
	    unsigned int newxslots;
	    int newxshift;
	    /* Empty current xlist. Nodes that stay go to list h;
	    ** nodes that move go to list g. */
	    for (i = 0; i < xslots; i++) {
		f = xlist[i];
		while (f != sentinel) {
		    next = f->next;
		    f1 = cuddT(f); f0 = cuddE(f);
		    if (f1->index != (DdHalfWord) yindex &&
			Cudd_Regular(f0)->index != (DdHalfWord) yindex) {
			/* stays */
			f->next = h;
			h = f;
			newxkeys++;
		    } else {
			f->index = yindex;
			f->next = g;
			g = f;
		    }
		    f = next;
		} /* while there are elements in the collision chain */
	    } /* for each slot of the x subtable */
	    /* Decide size of new subtable. */
	    if (oldxkeys > DD_MAX_SUBTABLE_DENSITY * xslots) {
		newxshift = xshift - 1;
		newxslots = xslots << 1;
	    } else {
		newxshift = xshift + 1;
		newxslots = xslots >> 1;
	    }
	    /* Try to allocate new table. Be ready to back off. */
	    saveHandler = MMoutOfMemory;
	    MMoutOfMemory = Cudd_OutOfMem;
	    newxlist = ALLOC(DdNodePtr, newxslots);
	    MMoutOfMemory = saveHandler;
	    if (newxlist == NULL) {
		(void) fprintf(table->err, "Unable to resize subtable %d for lack of memory\n", i);
		newxlist = xlist;
		newxslots = xslots;
		newxshift = xshift;
	    } else {
		table->slots += (newxslots - xslots);
		table->minDead = (unsigned)
		    (table->gcFrac * (double) table->slots);
		table->cacheSlack = (int)
		    ddMin(table->maxCacheHard, DD_MAX_CACHE_TO_SLOTS_RATIO
			  * table->slots) - 2 * (int) table->cacheSlots;
		table->memused += (newxslots - xslots) * sizeof(DdNodePtr);
		FREE(xlist);
		xslots =  newxslots;
		xshift = newxshift;
		xlist = newxlist;
	    }
	    /* Initialize new subtable. */
	    for (i = 0; i < xslots; i++) {
		xlist[i] = sentinel;
	    }
	    /* Move nodes that were parked in list h to their new home. */
	    f = h;
	    while (f != NULL) {
		next = f->next;
		f1 = cuddT(f);
		f0 = cuddE(f);
		/* Check xlist for pair (f11,f01). */
		posn = ddHash(f1, f0, xshift);
		/* For each element tmp in collision list xlist[posn]. */
		previousP = &(xlist[posn]);
		tmp = *previousP;
		while (f1 < cuddT(tmp)) {
		    previousP = &(tmp->next);
		    tmp = *previousP;
		}
		while (f1 == cuddT(tmp) && f0 < cuddE(tmp)) {
		    previousP = &(tmp->next);
		    tmp = *previousP;
		}
		f->next = *previousP;
		*previousP = f;
		f = next;
	    }
	}

#ifdef DD_COUNT
	table->swapSteps += oldxkeys - newxkeys;
#endif
	/* Take care of the x nodes that must be re-expressed.
	** They form a linked list pointed by g. Their index has been
	** already changed to yindex.
	*/
	f = g;
	while (f != NULL) {
	    next = f->next;
	    /* Find f1, f0, f11, f10, f01, f00. */
	    f1 = cuddT(f);
#ifdef DD_DEBUG
	    assert(!(Cudd_IsComplement(f1)));
#endif
	    if ((int) f1->index == yindex) {
		f11 = cuddT(f1); f10 = cuddE(f1);
	    } else {
		f11 = f10 = f1;
	    }
#ifdef DD_DEBUG
	    assert(!(Cudd_IsComplement(f11)));
#endif
	    f0 = cuddE(f);
	    comple = Cudd_IsComplement(f0);
	    f0 = Cudd_Regular(f0);
	    if ((int) f0->index == yindex) {
		f01 = cuddT(f0); f00 = cuddE(f0);
	    } else {
		f01 = f00 = f0;
	    }
	    if (comple) {
		f01 = Cudd_Not(f01);
		f00 = Cudd_Not(f00);
	    }
	    /* Decrease ref count of f1. */
	    cuddSatDec(f1->ref);
	    /* Create the new T child. */
	    if (f11 == f01) {
		newf1 = f11;
		cuddSatInc(newf1->ref);
	    } else {
		/* Check xlist for triple (xindex,f11,f01). */
		posn = ddHash(f11, f01, xshift);
		/* For each element newf1 in collision list xlist[posn]. */
		previousP = &(xlist[posn]);
		newf1 = *previousP;
		while (f11 < cuddT(newf1)) {
		    previousP = &(newf1->next);
		    newf1 = *previousP;
		}
		while (f11 == cuddT(newf1) && f01 < cuddE(newf1)) {
		    previousP = &(newf1->next);
		    newf1 = *previousP;
		}
		if (cuddT(newf1) == f11 && cuddE(newf1) == f01) {
		    cuddSatInc(newf1->ref);
		} else { /* no match */
		    newf1 = cuddDynamicAllocNode(table);
		    if (newf1 == NULL)
			goto cuddSwapOutOfMem;
		    newf1->index = xindex; newf1->ref = 1;
		    cuddT(newf1) = f11;
		    cuddE(newf1) = f01;
		    /* Insert newf1 in the collision list xlist[posn];
		    ** increase the ref counts of f11 and f01.
		    */
		    newxkeys++;
		    newf1->next = *previousP;
		    *previousP = newf1;
		    cuddSatInc(f11->ref);
		    tmp = Cudd_Regular(f01);
		    cuddSatInc(tmp->ref);
		}
	    }
	    cuddT(f) = newf1;
#ifdef DD_DEBUG
	    assert(!(Cudd_IsComplement(newf1)));
#endif

	    /* Do the same for f0, keeping complement dots into account. */
	    /* Decrease ref count of f0. */
	    tmp = Cudd_Regular(f0);
	    cuddSatDec(tmp->ref);
	    /* Create the new E child. */
	    if (f10 == f00) {
		newf0 = f00;
		tmp = Cudd_Regular(newf0);
		cuddSatInc(tmp->ref); 
	    } else {
		/* make sure f10 is regular */
		newcomplement = Cudd_IsComplement(f10);
		if (newcomplement) {
		    f10 = Cudd_Not(f10);
		    f00 = Cudd_Not(f00);
		}
		/* Check xlist for triple (xindex,f10,f00). */
		posn = ddHash(f10, f00, xshift);
		/* For each element newf0 in collision list xlist[posn]. */
		previousP = &(xlist[posn]);
		newf0 = *previousP;
		while (f10 < cuddT(newf0)) {
		    previousP = &(newf0->next);
		    newf0 = *previousP;
		}
		while (f10 == cuddT(newf0) && f00 < cuddE(newf0)) {
		    previousP = &(newf0->next);
		    newf0 = *previousP;
		}
		if (cuddT(newf0) == f10 && cuddE(newf0) == f00) {
		    cuddSatInc(newf0->ref); 
		} else { /* no match */
		    newf0 = cuddDynamicAllocNode(table);
		    if (newf0 == NULL)
			goto cuddSwapOutOfMem;
		    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 = *previousP;
		    *previousP = newf0;
		    cuddSatInc(f10->ref);
		    tmp = Cudd_Regular(f00);
		    cuddSatInc(tmp->ref);
		}
		if (newcomplement) {
		    newf0 = Cudd_Not(newf0);
		}
	    }
	    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.)