cuddreorder.c

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

	    */
	    posn = ddHash(newf1, newf0, yshift);
	    newykeys++;
	    previousP = &(ylist[posn]);
	    tmp = *previousP;
	    while (newf1 < cuddT(tmp)) {
		previousP = &(tmp->next);
		tmp = *previousP;
	    }
	    while (newf1 == cuddT(tmp) && newf0 < cuddE(tmp)) {
		previousP = &(tmp->next);
		tmp = *previousP;
	    }
	    f->next = *previousP;
	    *previousP = 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 != sentinel) {
		next = f->next;
		if (f->ref == 0) {
		    tmp = cuddT(f);
		    cuddSatDec(tmp->ref);
		    tmp = Cudd_Regular(cuddE(f));
		    cuddSatDec(tmp->ref);
		    cuddDeallocNode(table,f);
		    newykeys--;
		} else {
		    *previousP = f;
		    previousP = &(f->next);
		}
		f = next;
	    } /* while f */
	    *previousP = sentinel;
	} /* for i */

#if DD_DEBUG
#if 0
	(void) fprintf(table->out,"Swapping %d and %d\n",x,y);
#endif
	count = 0;
	idcheck = 0;
	for (i = 0; i < yslots; i++) {
	    f = ylist[i];
	    while (f != sentinel) {
		count++;
		if (f->index != (DdHalfWord) yindex)
		    idcheck++;
		f = f->next;
	    }
	}
	if (count != newykeys) {
	    (void) fprintf(table->out,
			   "Error in finding newykeys\toldykeys = %d\tnewykeys = %d\tactual = %d\n",
			   oldykeys,newykeys,count);
	}
	if (idcheck != 0)
	    (void) fprintf(table->out,
			   "Error in id's of ylist\twrong id's = %d\n",
			   idcheck);
	count = 0;
	idcheck = 0;
	for (i = 0; i < xslots; i++) {
	    f = xlist[i];
	    while (f != sentinel) {
		count++;
		if (f->index != (DdHalfWord) xindex)
		    idcheck++;
		f = f->next;
	    }
	}
	if (count != newxkeys) {
	    (void) fprintf(table->out,
			   "Error in finding newxkeys\toldxkeys = %d \tnewxkeys = %d \tactual = %d\n",
			   oldxkeys,newxkeys,count);
	}
	if (idcheck != 0)
	    (void) fprintf(table->out,
			   "Error in id's of xlist\twrong id's = %d\n",
			   idcheck);
#endif

	isolated += (table->vars[xindex]->ref == 1) +
		    (table->vars[yindex]->ref == 1);
	table->isolated += isolated;
    }

    /* Set the appropriate fields in table. */
    table->subtables[x].nodelist = ylist;
    table->subtables[x].slots = yslots;
    table->subtables[x].shift = yshift;
    table->subtables[x].keys = newykeys;
    table->subtables[x].maxKeys = yslots * DD_MAX_SUBTABLE_DENSITY;
    i = table->subtables[x].bindVar;
    table->subtables[x].bindVar = table->subtables[y].bindVar;
    table->subtables[y].bindVar = i;
    /* Adjust filds for lazy sifting. */
    varType = table->subtables[x].varType;
    table->subtables[x].varType = table->subtables[y].varType;
    table->subtables[y].varType = varType;
    i = table->subtables[x].pairIndex;
    table->subtables[x].pairIndex = table->subtables[y].pairIndex;
    table->subtables[y].pairIndex = i;
    i = table->subtables[x].varHandled;
    table->subtables[x].varHandled = table->subtables[y].varHandled;
    table->subtables[y].varHandled = i;
    groupType = table->subtables[x].varToBeGrouped;
    table->subtables[x].varToBeGrouped = table->subtables[y].varToBeGrouped;
    table->subtables[y].varToBeGrouped = groupType;

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

    table->perm[xindex] = y; table->perm[yindex] = x;
    table->invperm[x] = yindex; table->invperm[y] = xindex;

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

    return(table->keys - table->isolated);

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

    return (0);

} /* end of cuddSwapInPlace */


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

  Synopsis    [Reorders BDD variables according to the order of the ZDD
  variables.]

  Description [Reorders BDD variables according to the order of the
  ZDD variables. This function can be called at the end of ZDD
  reordering to insure that the order of the BDD variables is
  consistent with the order of the ZDD variables. The number of ZDD
  variables must be a multiple of the number of BDD variables. Let
  <code>M</code> be the ratio of the two numbers. cuddBddAlignToZdd
  then considers the ZDD variables from <code>M*i</code> to
  <code>(M+1)*i-1</code> as corresponding to BDD variable
  <code>i</code>.  This function should be normally called from
  Cudd_zddReduceHeap, which clears the cache.  Returns 1 in case of
  success; 0 otherwise.]

  SideEffects [Changes the BDD variable order for all diagrams and performs
  garbage collection of the BDD unique table.]

  SeeAlso [Cudd_ShuffleHeap Cudd_zddReduceHeap]

******************************************************************************/
int
cuddBddAlignToZdd(
  DdManager * table /* DD manager */)
{
    int *invperm;		/* permutation array */
    int M;			/* ratio of ZDD variables to BDD variables */
    int i;			/* loop index */
    int result;			/* return value */

    /* We assume that a ratio of 0 is OK. */
    if (table->size == 0)
	return(1);

    M = table->sizeZ / table->size;
    /* Check whether the number of ZDD variables is a multiple of the
    ** number of BDD variables.
    */
    if (M * table->size != table->sizeZ)
	return(0);
    /* Create and initialize the inverse permutation array. */
    invperm = ALLOC(int,table->size);
    if (invperm == NULL) {
	table->errorCode = CUDD_MEMORY_OUT;
	return(0);
    }
    for (i = 0; i < table->sizeZ; i += M) {
	int indexZ = table->invpermZ[i];
	int index  = indexZ / M;
	invperm[i / M] = index;
    }
    /* Eliminate dead nodes. Do not scan the cache again, because we
    ** assume that Cudd_zddReduceHeap has already cleared it.
    */
    cuddGarbageCollect(table,0);

    /* Initialize number of isolated projection functions. */
    table->isolated = 0;
    for (i = 0; i < table->size; i++) {
	if (table->vars[i]->ref == 1) table->isolated++;
    }

    /* Initialize the interaction matrix. */
    result = cuddInitInteract(table);
    if (result == 0) return(0);

    result = ddShuffle(table, invperm);
    FREE(invperm);
    /* Free interaction matrix. */
    FREE(table->interact);
    /* Fix the BDD variable group tree. */
    bddFixTree(table,table->tree);
    return(result);

} /* end of cuddBddAlignToZdd */

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

} /* end of ddUniqueCompare */


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

  Synopsis    [Swaps any two variables.]

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

  SideEffects [None]

******************************************************************************/
static Move *
ddSwapAny(
  DdManager * table,
  int  x,
  int  y)
{
    Move	*move, *moves;
    int		xRef,yRef;
    int		xNext,yNext;
    int		size;
    int		limitSize;
    int		tmp;

    if (x >y) {
	tmp = x; x = y; y = tmp;
    }

    xRef = x; yRef = y;

    xNext = cuddNextHigh(table,x);
    yNext = cuddNextLow(table,y);
    moves = NULL;
    limitSize = table->keys - table->isolated;

    for (;;) {
	if ( xNext == yNext) {
	    size = cuddSwapInPlace(table,x,xNext);
	    if (size == 0) goto ddSwapAnyOutOfMem;
	    move = (Move *) cuddDynamicAllocNode(table);			
	    if (move == NULL) goto ddSwapAnyOutOfMem;
	    move->x = x;
	    move->y = xNext;
	    move->size = size; 
	    move->next = moves;
	    moves = move;

	    size = cuddSwapInPlace(table,yNext,y);
	    if (size == 0) goto ddSwapAnyOutOfMem;
	    move = (Move *) cuddDynamicAllocNode(table);
	    if (move == NULL) goto ddSwapAnyOutOfMem;
	    move->x = yNext;
	    move->y = y;
	    move->size = size; 
	    move->next = moves;
	    moves = move;

	    size = cuddSwapInPlace(table,x,xNext);
	    if (size == 0) goto ddSwapAnyOutOfMem;
	    move = (Move *) cuddDynamicAllocNode(table);
	    if (move == NULL) goto ddSwapAnyOutOfMem;
	    move->x = x;
	    move->y = xNext;
	    move->size = size;
	    move->next = moves;
	    moves = move;

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

	} else if (x == yNext) {
	    
	    size = cuddSwapInPlace(table,x,xNext);
	    if (size == 0) goto ddSwapAnyOutOfMem;
	    move = (Move *) cuddDynamicAllocNode(table);
	    if (move == NULL) goto ddSwapAnyOutOfMem;
	    move->x = x;
	    move->y = xNext;
	    move->size = size;
	    move->next = moves;
	    moves = move;

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

	} else {
	    size = cuddSwapInPlace(table,x,xNext);
	    if (size == 0) goto ddSwapAnyOutOfMem;
	    move = (Move *) cuddDynamicAllocNode(table);
	    if (move == NULL) goto ddSwapAnyOutOfMem;
	    move->x = x;
	    move->y = xNext;
	    move->size = size; 
	    move->next = moves;
	    moves = move;

	    size = cuddSwapInPlace(table,yNext,y);
	    if (size == 0) goto ddSwapAnyOutOfMem;
	    move = (Move *) cuddDynamicAllocNode(table);
	    if (move == NULL) goto ddSwapAnyOutOfMem;
	    move->x = yNext;
	    move->y = y;
	    move->size = size;
	    move->next = moves;
	    moves = move;

	    x = xNext;
	    y = yNext;
	}

	xNext = cuddNextHigh(table,x);
	yNext = cuddNextLow(table,y);
	if (xNext > yRef) break;

	if ((double) size > table->maxGrowth * (double) limitSize) break;
	if (size < limitSize) limitSize = size;
    }
    if (yNext>=xRef) {
	size = cuddSwapInPlace(table,yNext,y);
	if (size == 0) goto ddSwapAnyOutOfMem;
	move = (Move *) cuddDynamicAllocNode(table);
	if (move == NULL) goto ddSwapAnyOutOfMem;
	move->x = yNext;
	move->y = y;
	move->size = size; 
	move->next = moves;
	moves = move;
    }

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

} /* end of ddSwapAny */


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

******************************************************************************/
static int
ddSiftingAux(
  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;

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

    moveDown = NULL;
    moveUp = NULL;

    if (x == xLow) {
	moveDown = ddSiftingDown(table,x,xHigh);
	/* At this point x --> xHigh unless bounding occurred. */
	if (moveDown == (Move *) CUDD_OUT_OF_MEM) goto ddSiftingAuxOutOfMem;
	/* Move backward and stop at best position. */	
	result = ddSiftingBackward(table,initialSize,moveDown);
	if (!result) goto ddSiftingAuxOutOfMem;

    } else if (x == xHigh) {
	moveUp = ddSiftingUp(table,x,xLow);
	/* At this point x --> xLow unless bounding occurred. */
	if (moveUp == (Move *) CUDD_OUT_OF_MEM) goto ddSiftingAuxOutOfMem;
	/* Move backward and stop at best position. */
	result = ddSiftingBackward(table,initialSize,moveUp);
	if (!result) goto ddSiftingAuxOutOfMem;

    } else if ((x - xLow) > (xHigh - x)) { /* must go down first: shorter */
	moveDown = ddSiftingDown(table,x,xHigh);
	/* At this point x --> xHigh unless bounding occurred. */
	if (moveDown == (Move *) CUDD_OUT_OF_MEM) goto ddSiftingAuxOutOfMem;
	if (moveDown != NULL) {
	    x = moveDown->y;
	}
	moveUp = ddSiftingUp(table,x,xLow);
	if (moveUp == (Move *) CUDD_OUT_OF_MEM) goto ddSiftingAuxOutOfMem;
	/* Move backward and stop at best position */	
	result = ddSiftingBackward(table,initialSize,moveUp);
	if (!result) goto ddSiftingAuxOutOfMem;

    } else { /* must go up first: shorter */
	moveUp = ddSiftingUp(table,x,xLow);
	/* At this point x --> xLow unless bounding occurred. */
	if (moveUp == (Move *) CUDD_OUT_OF_MEM) goto ddSiftingAuxOutOfMem;
	if (moveUp != NULL) {
	    x = moveUp->x;
	}
	moveDown = ddSiftingDown(table,x,xHigh);
	if (moveDown == (Move *) CUDD_OUT_OF_MEM) goto ddSiftingAuxOutOfMem;
	/* Move backward and stop at best position. */	
	result = ddSiftingBackward(table,initialSize,moveDown);
	if (!result) goto ddSiftingAuxOutOfMem;
    }

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

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

    return(0);

} /* end of ddSiftingAux */


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

  Synopsis    [Sifts a variable up.]

  Description [Sifts a variable up. Moves y up until either it reaches
  the bound (xLow) or the size of the DD heap increases too much.
  Returns the set of moves in case of success; NULL if memory is full.]

  SideEffects [None]

******************************************************************************/
static Move *
ddSiftingUp(
  DdManager * table,
  int  y,
  int  xLow)
{
    Move	*moves;
    Move	*move;
    int		x;
    int		size;
    int		limitSize;
    int		xindex, yindex;
    int		isolated;
    int		L;	/* lower bound on DD size */
#ifdef DD_DEBUG
    int checkL;
    int z;
    int zindex;
#endif