diff options
Diffstat (limited to 'abc70930/src/bdd/cudd/cuddZddLin.c')
-rw-r--r-- | abc70930/src/bdd/cudd/cuddZddLin.c | 939 |
1 files changed, 0 insertions, 939 deletions
diff --git a/abc70930/src/bdd/cudd/cuddZddLin.c b/abc70930/src/bdd/cudd/cuddZddLin.c deleted file mode 100644 index ef2cd298..00000000 --- a/abc70930/src/bdd/cudd/cuddZddLin.c +++ /dev/null @@ -1,939 +0,0 @@ -/**CFile*********************************************************************** - - FileName [cuddZddLin.c] - - PackageName [cudd] - - Synopsis [Procedures for dynamic variable ordering of ZDDs.] - - Description [Internal procedures included in this module: - <ul> - <li> cuddZddLinearSifting() - </ul> - Static procedures included in this module: - <ul> - <li> cuddZddLinearInPlace() - <li> cuddZddLinerAux() - <li> cuddZddLinearUp() - <li> cuddZddLinearDown() - <li> cuddZddLinearBackward() - <li> cuddZddUndoMoves() - </ul> - ] - - SeeAlso [cuddLinear.c cuddZddReord.c] - - Author [Fabio Somenzi] - - Copyright [ This file was created at the University of Colorado at - Boulder. The University of Colorado at Boulder makes no warranty - about the suitability of this software for any purpose. It is - presented on an AS IS basis.] - -******************************************************************************/ - -#include "util_hack.h" -#include "cuddInt.h" - -/*---------------------------------------------------------------------------*/ -/* Constant declarations */ -/*---------------------------------------------------------------------------*/ - -#define CUDD_SWAP_MOVE 0 -#define CUDD_LINEAR_TRANSFORM_MOVE 1 -#define CUDD_INVERSE_TRANSFORM_MOVE 2 - -/*---------------------------------------------------------------------------*/ -/* Stucture declarations */ -/*---------------------------------------------------------------------------*/ - - -/*---------------------------------------------------------------------------*/ -/* Type declarations */ -/*---------------------------------------------------------------------------*/ - - -/*---------------------------------------------------------------------------*/ -/* Variable declarations */ -/*---------------------------------------------------------------------------*/ - -#ifndef lint -static char rcsid[] DD_UNUSED = "$Id: cuddZddLin.c,v 1.1.1.1 2003/02/24 22:23:54 wjiang Exp $"; -#endif - -extern int *zdd_entry; -extern int zddTotalNumberSwapping; -static int zddTotalNumberLinearTr; -static DdNode *empty; - - -/*---------------------------------------------------------------------------*/ -/* Macro declarations */ -/*---------------------------------------------------------------------------*/ - - -/**AutomaticStart*************************************************************/ - -/*---------------------------------------------------------------------------*/ -/* Static function prototypes */ -/*---------------------------------------------------------------------------*/ - -static int cuddZddLinearAux ARGS((DdManager *table, int x, int xLow, int xHigh)); -static Move * cuddZddLinearUp ARGS((DdManager *table, int y, int xLow, Move *prevMoves)); -static Move * cuddZddLinearDown ARGS((DdManager *table, int x, int xHigh, Move *prevMoves)); -static int cuddZddLinearBackward ARGS((DdManager *table, int size, Move *moves)); -static Move* cuddZddUndoMoves ARGS((DdManager *table, Move *moves)); - -/**AutomaticEnd***************************************************************/ - - -/*---------------------------------------------------------------------------*/ -/* Definition of exported functions */ -/*---------------------------------------------------------------------------*/ - - -/*---------------------------------------------------------------------------*/ -/* Definition of internal functions */ -/*---------------------------------------------------------------------------*/ - - - - -/**Function******************************************************************** - - Synopsis [Implementation of the linear sifting algorithm for ZDDs.] - - Description [Implementation of the linear sifting algorithm for ZDDs. - 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 and applies the XOR transformation, - 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 -cuddZddLinearSifting( - 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; - empty = table->zero; - - /* 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 = cuddZddLinearAux(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 cuddZddLinearSifting */ - - -/*---------------------------------------------------------------------------*/ -/* Definition of static functions */ -/*---------------------------------------------------------------------------*/ - - -/**Function******************************************************************** - - Synopsis [Linearly combines two adjacent variables.] - - Description [Linearly combines 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. cuddZddLinearInPlace assumes that x < y. Returns the - number of keys in the table if successful; 0 otherwise.] - - SideEffects [None] - - SeeAlso [cuddZddSwapInPlace cuddLinearInPlace] - -******************************************************************************/ -int -cuddZddLinearInPlace( - 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 i; - int posn; - DdNode *f, *f1, *f0, *f11, *f10, *f01, *f00; - DdNode *newf1, *newf0, *g, *next, *previous; - DdNode *special; - -#ifdef DD_DEBUG - assert(x < y); - assert(cuddZddNextHigh(table,x) == y); - assert(table->subtableZ[x].keys != 0); - assert(table->subtableZ[y].keys != 0); - assert(table->subtableZ[x].dead == 0); - assert(table->subtableZ[y].dead == 0); -#endif - - zddTotalNumberLinearTr++; - - /* Get parameters of x subtable. */ - xindex = table->invpermZ[x]; - xlist = table->subtableZ[x].nodelist; - oldxkeys = table->subtableZ[x].keys; - xslots = table->subtableZ[x].slots; - xshift = table->subtableZ[x].shift; - newxkeys = 0; - - /* Get parameters of y subtable. */ - yindex = table->invpermZ[y]; - ylist = table->subtableZ[y].nodelist; - oldykeys = table->subtableZ[y].keys; - yslots = table->subtableZ[y].slots; - yshift = table->subtableZ[y].shift; - newykeys = oldykeys; - - /* The nodes in the x layer are put in two chains. The chain - ** pointed by g holds the normal nodes. When re-expressed they stay - ** in the x list. The chain pointed by special holds the elements - ** that will move to the y list. - */ - g = special = NULL; - for (i = 0; i < xslots; i++) { - f = xlist[i]; - if (f == NULL) continue; - xlist[i] = NULL; - while (f != NULL) { - next = f->next; - f1 = cuddT(f); - /* if (f1->index == yindex) */ cuddSatDec(f1->ref); - f0 = cuddE(f); - /* if (f0->index == yindex) */ cuddSatDec(f0->ref); - if ((int) f1->index == yindex && cuddE(f1) == empty && - (int) f0->index != yindex) { - f->next = special; - special = f; - } else { - f->next = g; - g = f; - } - f = next; - } /* while there are elements in the collision chain */ - } /* for each slot of the x subtable */ - - /* Mark y nodes with pointers from above x. We mark them by - ** changing their index to x. - */ - for (i = 0; i < yslots; i++) { - f = ylist[i]; - while (f != NULL) { - if (f->ref != 0) { - f->index = xindex; - } - f = f->next; - } /* while there are elements in the collision chain */ - } /* for each slot of the y subtable */ - - /* Move special nodes to the y list. */ - f = special; - while (f != NULL) { - next = f->next; - f1 = cuddT(f); - f11 = cuddT(f1); - cuddT(f) = f11; - cuddSatInc(f11->ref); - f0 = cuddE(f); - cuddSatInc(f0->ref); - f->index = yindex; - /* Insert at the beginning of the list so that it will be - ** found first if there is a duplicate. The duplicate will - ** eventually be moved or garbage collected. No node - ** re-expression will add a pointer to it. - */ - posn = ddHash(f11, f0, yshift); - f->next = ylist[posn]; - ylist[posn] = f; - newykeys++; - f = next; - } - - /* Take care of the remaining x nodes that must be re-expressed. - ** They form a linked list pointed by g. - */ - f = g; - while (f != NULL) { -#ifdef DD_COUNT - table->swapSteps++; -#endif - next = f->next; - /* Find f1, f0, f11, f10, f01, f00. */ - f1 = cuddT(f); - if ((int) f1->index == yindex || (int) f1->index == xindex) { - f11 = cuddT(f1); f10 = cuddE(f1); - } else { - f11 = empty; f10 = f1; - } - f0 = cuddE(f); - if ((int) f0->index == yindex || (int) f0->index == xindex) { - f01 = cuddT(f0); f00 = cuddE(f0); - } else { - f01 = empty; f00 = f0; - } - /* Create the new T child. */ - if (f01 == empty) { - newf1 = f10; - cuddSatInc(newf1->ref); - } else { - /* Check ylist for triple (yindex, f01, f10). */ - posn = ddHash(f01, f10, yshift); - /* For each element newf1 in collision list ylist[posn]. */ - newf1 = ylist[posn]; - /* Search the collision chain skipping the marked nodes. */ - while (newf1 != NULL) { - if (cuddT(newf1) == f01 && cuddE(newf1) == f10 && - (int) newf1->index == yindex) { - 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 = yindex; newf1->ref = 1; - cuddT(newf1) = f01; - cuddE(newf1) = f10; - /* Insert newf1 in the collision list ylist[pos]; - ** increase the ref counts of f01 and f10 - */ - newykeys++; - newf1->next = ylist[posn]; - ylist[posn] = newf1; - cuddSatInc(f01->ref); - cuddSatInc(f10->ref); - } - } - cuddT(f) = newf1; - - /* Do the same for f0. */ - /* Create the new E child. */ - if (f11 == empty) { - newf0 = f00; - cuddSatInc(newf0->ref); - } else { - /* Check ylist for triple (yindex, f11, f00). */ - posn = ddHash(f11, f00, yshift); - /* For each element newf0 in collision list ylist[posn]. */ - newf0 = ylist[posn]; - while (newf0 != NULL) { - if (cuddT(newf0) == f11 && cuddE(newf0) == f00 && - (int) newf0->index == yindex) { - 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 = yindex; newf0->ref = 1; - cuddT(newf0) = f11; cuddE(newf0) = f00; - /* Insert newf0 in the collision list ylist[posn]; - ** increase the ref counts of f11 and f00. - */ - newykeys++; - newf0->next = ylist[posn]; - ylist[posn] = newf0; - cuddSatInc(f11->ref); - cuddSatInc(f00->ref); - } - } - cuddE(f) = newf0; - - /* Re-insert the modified f in xlist. - ** The modified f does not already exists in xlist. - ** (Because of the uniqueness of the cofactors.) - */ - posn = ddHash(newf1, newf0, xshift); - newxkeys++; - f->next = xlist[posn]; - xlist[posn] = f; - f = next; - } /* while f != NULL */ - - /* GC the y layer and move the marked nodes to the x list. */ - - /* For each node f in ylist. */ - for (i = 0; i < yslots; i++) { - previous = NULL; - f = ylist[i]; - while (f != NULL) { - next = f->next; - if (f->ref == 0) { - cuddSatDec(cuddT(f)->ref); - cuddSatDec(cuddE(f)->ref); - cuddDeallocNode(table, f); - newykeys--; - if (previous == NULL) - ylist[i] = next; - else - previous->next = next; - } else if ((int) f->index == xindex) { /* move marked node */ - if (previous == NULL) - ylist[i] = next; - else - previous->next = next; - f1 = cuddT(f); - cuddSatDec(f1->ref); - /* Check ylist for triple (yindex, f1, empty). */ - posn = ddHash(f1, empty, yshift); - /* For each element newf1 in collision list ylist[posn]. */ - newf1 = ylist[posn]; - while (newf1 != NULL) { - if (cuddT(newf1) == f1 && cuddE(newf1) == empty && - (int) newf1->index == yindex) { - 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 = yindex; newf1->ref = 1; - cuddT(newf1) = f1; cuddE(newf1) = empty; - /* Insert newf1 in the collision list ylist[posn]; - ** increase the ref counts of f1 and empty. - */ - newykeys++; - newf1->next = ylist[posn]; - ylist[posn] = newf1; - if (posn == i && previous == NULL) - previous = newf1; - cuddSatInc(f1->ref); - cuddSatInc(empty->ref); - } - cuddT(f) = newf1; - f0 = cuddE(f); - /* Insert f in x list. */ - posn = ddHash(newf1, f0, xshift); - newxkeys++; - newykeys--; - f->next = xlist[posn]; - xlist[posn] = f; - } else { - previous = f; - } - f = next; - } /* while f */ - } /* for i */ - - /* Set the appropriate fields in table. */ - table->subtableZ[x].keys = newxkeys; - table->subtableZ[y].keys = newykeys; - - table->keysZ += newxkeys + newykeys - oldxkeys - oldykeys; - - /* Update univ section; univ[x] remains the same. */ - table->univ[y] = cuddT(table->univ[x]); - -#if 0 - (void) fprintf(table->out,"x = %d y = %d\n", x, y); - (void) Cudd_DebugCheck(table); - (void) Cudd_CheckKeys(table); -#endif - - return (table->keysZ); - -zddSwapOutOfMem: - (void) fprintf(table->err, "Error: cuddZddSwapInPlace out of memory\n"); - - return (0); - -} /* end of cuddZddLinearInPlace */ - - -/**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 -cuddZddLinearAux( - DdManager * table, - int x, - int xLow, - int xHigh) -{ - Move *move; - Move *moveUp; /* list of up move */ - Move *moveDown; /* list of down move */ - - int initial_size; - int result; - - initial_size = table->keysZ; - -#ifdef DD_DEBUG - assert(table->subtableZ[x].keys > 0); -#endif - - moveDown = NULL; - moveUp = NULL; - - if (x == xLow) { - moveDown = cuddZddLinearDown(table, x, xHigh, NULL); - /* At this point x --> xHigh. */ - if (moveDown == (Move *) CUDD_OUT_OF_MEM) - goto cuddZddLinearAuxOutOfMem; - /* Move backward and stop at best position. */ - result = cuddZddLinearBackward(table, initial_size, moveDown); - if (!result) - goto cuddZddLinearAuxOutOfMem; - - } else if (x == xHigh) { - moveUp = cuddZddLinearUp(table, x, xLow, NULL); - /* At this point x --> xLow. */ - if (moveUp == (Move *) CUDD_OUT_OF_MEM) - goto cuddZddLinearAuxOutOfMem; - /* Move backward and stop at best position. */ - result = cuddZddLinearBackward(table, initial_size, moveUp); - if (!result) - goto cuddZddLinearAuxOutOfMem; - - } else if ((x - xLow) > (xHigh - x)) { /* must go down first: shorter */ - moveDown = cuddZddLinearDown(table, x, xHigh, NULL); - /* At this point x --> xHigh. */ - if (moveDown == (Move *) CUDD_OUT_OF_MEM) - goto cuddZddLinearAuxOutOfMem; - moveUp = cuddZddUndoMoves(table,moveDown); -#ifdef DD_DEBUG - assert(moveUp == NULL || moveUp->x == x); -#endif - moveUp = cuddZddLinearUp(table, x, xLow, moveUp); - if (moveUp == (Move *) CUDD_OUT_OF_MEM) - goto cuddZddLinearAuxOutOfMem; - /* Move backward and stop at best position. */ - result = cuddZddLinearBackward(table, initial_size, moveUp); - if (!result) - goto cuddZddLinearAuxOutOfMem; - - } else { - moveUp = cuddZddLinearUp(table, x, xLow, NULL); - /* At this point x --> xHigh. */ - if (moveUp == (Move *) CUDD_OUT_OF_MEM) - goto cuddZddLinearAuxOutOfMem; - /* Then move up. */ - moveDown = cuddZddUndoMoves(table,moveUp); -#ifdef DD_DEBUG - assert(moveDown == NULL || moveDown->y == x); -#endif - moveDown = cuddZddLinearDown(table, x, xHigh, moveDown); - if (moveDown == (Move *) CUDD_OUT_OF_MEM) - goto cuddZddLinearAuxOutOfMem; - /* Move backward and stop at best position. */ - result = cuddZddLinearBackward(table, initial_size, moveDown); - if (!result) - goto cuddZddLinearAuxOutOfMem; - } - - 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); - -cuddZddLinearAuxOutOfMem: - 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 cuddZddLinearAux */ - - -/**Function******************************************************************** - - Synopsis [Sifts a variable up applying the XOR transformation.] - - Description [Sifts a variable up applying the XOR - transformation. Moves y up until either it reaches the bound (xLow) - or the size of the ZDD heap increases too much. Returns the set of - moves in case of success; NULL if memory is full.] - - SideEffects [None] - - SeeAlso [] - -******************************************************************************/ -static Move * -cuddZddLinearUp( - DdManager * table, - int y, - int xLow, - Move * prevMoves) -{ - Move *moves; - Move *move; - int x; - int size, newsize; - int limitSize; - - moves = prevMoves; - limitSize = table->keysZ; - - x = cuddZddNextLow(table, y); - while (x >= xLow) { - size = cuddZddSwapInPlace(table, x, y); - if (size == 0) - goto cuddZddLinearUpOutOfMem; - newsize = cuddZddLinearInPlace(table, x, y); - if (newsize == 0) - goto cuddZddLinearUpOutOfMem; - move = (Move *) cuddDynamicAllocNode(table); - if (move == NULL) - goto cuddZddLinearUpOutOfMem; - move->x = x; - move->y = y; - move->next = moves; - moves = move; - move->flags = CUDD_SWAP_MOVE; - if (newsize > size) { - /* Undo transformation. The transformation we apply is - ** its own inverse. Hence, we just apply the transformation - ** again. - */ - newsize = cuddZddLinearInPlace(table,x,y); - if (newsize == 0) goto cuddZddLinearUpOutOfMem; -#ifdef DD_DEBUG - if (newsize != size) { - (void) fprintf(table->err,"Change in size after identity transformation! From %d to %d\n",size,newsize); - } -#endif - } else { - size = newsize; - move->flags = CUDD_LINEAR_TRANSFORM_MOVE; - } - move->size = size; - - if ((double)size > (double)limitSize * table->maxGrowth) - break; - if (size < limitSize) - limitSize = size; - - y = x; - x = cuddZddNextLow(table, y); - } - return(moves); - -cuddZddLinearUpOutOfMem: - while (moves != NULL) { - move = moves->next; - cuddDeallocNode(table, (DdNode *)moves); - moves = move; - } - return((Move *) CUDD_OUT_OF_MEM); - -} /* end of cuddZddLinearUp */ - - -/**Function******************************************************************** - - Synopsis [Sifts a variable down and applies the XOR transformation.] - - Description [Sifts a variable down. Moves x down until either it - reaches the bound (xHigh) or the size of the ZDD heap increases too - much. Returns the set of moves in case of success; NULL if memory is - full.] - - SideEffects [None] - - SeeAlso [] - -******************************************************************************/ -static Move * -cuddZddLinearDown( - DdManager * table, - int x, - int xHigh, - Move * prevMoves) -{ - Move *moves; - Move *move; - int y; - int size, newsize; - int limitSize; - - moves = prevMoves; - limitSize = table->keysZ; - - y = cuddZddNextHigh(table, x); - while (y <= xHigh) { - size = cuddZddSwapInPlace(table, x, y); - if (size == 0) - goto cuddZddLinearDownOutOfMem; - newsize = cuddZddLinearInPlace(table, x, y); - if (newsize == 0) - goto cuddZddLinearDownOutOfMem; - move = (Move *) cuddDynamicAllocNode(table); - if (move == NULL) - goto cuddZddLinearDownOutOfMem; - move->x = x; - move->y = y; - move->next = moves; - moves = move; - move->flags = CUDD_SWAP_MOVE; - if (newsize > size) { - /* Undo transformation. The transformation we apply is - ** its own inverse. Hence, we just apply the transformation - ** again. - */ - newsize = cuddZddLinearInPlace(table,x,y); - if (newsize == 0) goto cuddZddLinearDownOutOfMem; - if (newsize != size) { - (void) fprintf(table->err,"Change in size after identity transformation! From %d to %d\n",size,newsize); - } - } else { - size = newsize; - move->flags = CUDD_LINEAR_TRANSFORM_MOVE; - } - move->size = size; - - if ((double)size > (double)limitSize * table->maxGrowth) - break; - if (size < limitSize) - limitSize = size; - - x = y; - y = cuddZddNextHigh(table, x); - } - return(moves); - -cuddZddLinearDownOutOfMem: - while (moves != NULL) { - move = moves->next; - cuddDeallocNode(table, (DdNode *)moves); - moves = move; - } - return((Move *) CUDD_OUT_OF_MEM); - -} /* end of cuddZddLinearDown */ - - -/**Function******************************************************************** - - Synopsis [Given a set of moves, returns the ZDD heap to the position - giving the minimum size.] - - Description [Given a set of moves, returns the ZDD heap to the - position giving the minimum size. In case of ties, returns to the - closest position giving the minimum size. Returns 1 in case of - success; 0 otherwise.] - - SideEffects [None] - - SeeAlso [] - -******************************************************************************/ -static int -cuddZddLinearBackward( - DdManager * table, - int size, - Move * moves) -{ - Move *move; - int res; - - /* Find the minimum size among moves. */ - for (move = moves; move != NULL; move = move->next) { - if (move->size < size) { - size = move->size; - } - } - - for (move = moves; move != NULL; move = move->next) { - if (move->size == size) return(1); - if (move->flags == CUDD_LINEAR_TRANSFORM_MOVE) { - res = cuddZddLinearInPlace(table,(int)move->x,(int)move->y); - if (!res) return(0); - } - res = cuddZddSwapInPlace(table, move->x, move->y); - if (!res) - return(0); - if (move->flags == CUDD_INVERSE_TRANSFORM_MOVE) { - res = cuddZddLinearInPlace(table,(int)move->x,(int)move->y); - if (!res) return(0); - } - } - - return(1); - -} /* end of cuddZddLinearBackward */ - - -/**Function******************************************************************** - - Synopsis [Given a set of moves, returns the ZDD heap to the order - in effect before the moves.] - - Description [Given a set of moves, returns the ZDD heap to the - order in effect before the moves. Returns 1 in case of success; - 0 otherwise.] - - SideEffects [None] - -******************************************************************************/ -static Move* -cuddZddUndoMoves( - DdManager * table, - Move * moves) -{ - Move *invmoves = NULL; - Move *move; - Move *invmove; - int size; - - for (move = moves; move != NULL; move = move->next) { - invmove = (Move *) cuddDynamicAllocNode(table); - if (invmove == NULL) goto cuddZddUndoMovesOutOfMem; - invmove->x = move->x; - invmove->y = move->y; - invmove->next = invmoves; - invmoves = invmove; - if (move->flags == CUDD_SWAP_MOVE) { - invmove->flags = CUDD_SWAP_MOVE; - size = cuddZddSwapInPlace(table,(int)move->x,(int)move->y); - if (!size) goto cuddZddUndoMovesOutOfMem; - } else if (move->flags == CUDD_LINEAR_TRANSFORM_MOVE) { - invmove->flags = CUDD_INVERSE_TRANSFORM_MOVE; - size = cuddZddLinearInPlace(table,(int)move->x,(int)move->y); - if (!size) goto cuddZddUndoMovesOutOfMem; - size = cuddZddSwapInPlace(table,(int)move->x,(int)move->y); - if (!size) goto cuddZddUndoMovesOutOfMem; - } else { /* must be CUDD_INVERSE_TRANSFORM_MOVE */ -#ifdef DD_DEBUG - (void) fprintf(table->err,"Unforseen event in ddUndoMoves!\n"); -#endif - invmove->flags = CUDD_LINEAR_TRANSFORM_MOVE; - size = cuddZddSwapInPlace(table,(int)move->x,(int)move->y); - if (!size) goto cuddZddUndoMovesOutOfMem; - size = cuddZddLinearInPlace(table,(int)move->x,(int)move->y); - if (!size) goto cuddZddUndoMovesOutOfMem; - } - invmove->size = size; - } - - return(invmoves); - -cuddZddUndoMovesOutOfMem: - while (invmoves != NULL) { - move = invmoves->next; - cuddDeallocNode(table, (DdNode *) invmoves); - invmoves = move; - } - return((Move *) CUDD_OUT_OF_MEM); - -} /* end of cuddZddUndoMoves */ - |