glu-2.2: src/cuBdd/cuddZddLin.c Source File

00001 
00062 #include "util.h"
00063 #include "cuddInt.h"
00064 
00065 /*---------------------------------------------------------------------------*/
00066 /* Constant declarations                                                     */
00067 /*---------------------------------------------------------------------------*/
00068 
00069 #define CUDD_SWAP_MOVE 0
00070 #define CUDD_LINEAR_TRANSFORM_MOVE 1
00071 #define CUDD_INVERSE_TRANSFORM_MOVE 2
00072 
00073 /*---------------------------------------------------------------------------*/
00074 /* Stucture declarations                                                     */
00075 /*---------------------------------------------------------------------------*/
00076 
00077 
00078 /*---------------------------------------------------------------------------*/
00079 /* Type declarations                                                         */
00080 /*---------------------------------------------------------------------------*/
00081 
00082 
00083 /*---------------------------------------------------------------------------*/
00084 /* Variable declarations                                                     */
00085 /*---------------------------------------------------------------------------*/
00086 
00087 #ifndef lint
00088 static char rcsid[] DD_UNUSED = "$Id: cuddZddLin.c,v 1.14 2004/08/13 18:04:53 fabio Exp $";
00089 #endif
00090 
00091 extern  int     *zdd_entry;
00092 extern  int     zddTotalNumberSwapping;
00093 static  int     zddTotalNumberLinearTr;
00094 static  DdNode  *empty;
00095 
00096 
00097 /*---------------------------------------------------------------------------*/
00098 /* Macro declarations                                                        */
00099 /*---------------------------------------------------------------------------*/
00100 
00101 
00104 /*---------------------------------------------------------------------------*/
00105 /* Static function prototypes                                                */
00106 /*---------------------------------------------------------------------------*/
00107 
00108 static int cuddZddLinearInPlace (DdManager * table, int x, int y);
00109 static int cuddZddLinearAux (DdManager *table, int x, int xLow, int xHigh);
00110 static Move * cuddZddLinearUp (DdManager *table, int y, int xLow, Move *prevMoves);
00111 static Move * cuddZddLinearDown (DdManager *table, int x, int xHigh, Move *prevMoves);
00112 static int cuddZddLinearBackward (DdManager *table, int size, Move *moves);
00113 static Move* cuddZddUndoMoves (DdManager *table, Move *moves);
00114 
00118 /*---------------------------------------------------------------------------*/
00119 /* Definition of exported functions                                          */
00120 /*---------------------------------------------------------------------------*/
00121 
00122 
00123 /*---------------------------------------------------------------------------*/
00124 /* Definition of internal functions                                          */
00125 /*---------------------------------------------------------------------------*/
00126 
00127 
00128 
00129 
00151 int
00152 cuddZddLinearSifting(
00153   DdManager * table,
00154   int  lower,
00155   int  upper)
00156 {
00157     int i;
00158     int *var;
00159     int size;
00160     int x;
00161     int result;
00162 #ifdef DD_STATS
00163     int previousSize;
00164 #endif
00165 
00166     size = table->sizeZ;
00167     empty = table->zero;
00168 
00169     /* Find order in which to sift variables. */
00170     var = NULL;
00171     zdd_entry = ALLOC(int, size);
00172     if (zdd_entry == NULL) {
00173         table->errorCode = CUDD_MEMORY_OUT;
00174         goto cuddZddSiftingOutOfMem;
00175     }
00176     var = ALLOC(int, size);
00177     if (var == NULL) {
00178         table->errorCode = CUDD_MEMORY_OUT;
00179         goto cuddZddSiftingOutOfMem;
00180     }
00181 
00182     for (i = 0; i < size; i++) {
00183         x = table->permZ[i];
00184         zdd_entry[i] = table->subtableZ[x].keys;
00185         var[i] = i;
00186     }
00187 
00188     qsort((void *)var, size, sizeof(int), (DD_QSFP)cuddZddUniqueCompare);
00189 
00190     /* Now sift. */
00191     for (i = 0; i < ddMin(table->siftMaxVar, size); i++) {
00192         if (zddTotalNumberSwapping >= table->siftMaxSwap)
00193             break;
00194         x = table->permZ[var[i]];
00195         if (x < lower || x > upper) continue;
00196 #ifdef DD_STATS
00197         previousSize = table->keysZ;
00198 #endif
00199         result = cuddZddLinearAux(table, x, lower, upper);
00200         if (!result)
00201             goto cuddZddSiftingOutOfMem;
00202 #ifdef DD_STATS
00203         if (table->keysZ < (unsigned) previousSize) {
00204             (void) fprintf(table->out,"-");
00205         } else if (table->keysZ > (unsigned) previousSize) {
00206             (void) fprintf(table->out,"+");     /* should never happen */
00207             (void) fprintf(table->out,"\nSize increased from %d to %d while sifting variable %d\n", previousSize, table->keysZ , var[i]);
00208         } else {
00209             (void) fprintf(table->out,"=");
00210         }
00211         fflush(table->out);
00212 #endif
00213     }
00214 
00215     FREE(var);
00216     FREE(zdd_entry);
00217 
00218     return(1);
00219 
00220 cuddZddSiftingOutOfMem:
00221 
00222     if (zdd_entry != NULL) FREE(zdd_entry);
00223     if (var != NULL) FREE(var);
00224 
00225     return(0);
00226 
00227 } /* end of cuddZddLinearSifting */
00228 
00229 
00230 /*---------------------------------------------------------------------------*/
00231 /* Definition of static functions                                            */
00232 /*---------------------------------------------------------------------------*/
00233 
00234 
00250 static int
00251 cuddZddLinearInPlace(
00252   DdManager * table,
00253   int  x,
00254   int  y)
00255 {
00256     DdNodePtr *xlist, *ylist;
00257     int         xindex, yindex;
00258     int         xslots, yslots;
00259     int         xshift, yshift;
00260     int         oldxkeys, oldykeys;
00261     int         newxkeys, newykeys;
00262     int         i;
00263     int         posn;
00264     DdNode      *f, *f1, *f0, *f11, *f10, *f01, *f00;
00265     DdNode      *newf1, *newf0, *g, *next, *previous;
00266     DdNode      *special;
00267 
00268 #ifdef DD_DEBUG
00269     assert(x < y);
00270     assert(cuddZddNextHigh(table,x) == y);
00271     assert(table->subtableZ[x].keys != 0);
00272     assert(table->subtableZ[y].keys != 0);
00273     assert(table->subtableZ[x].dead == 0);
00274     assert(table->subtableZ[y].dead == 0);
00275 #endif
00276 
00277     zddTotalNumberLinearTr++;
00278 
00279     /* Get parameters of x subtable. */
00280     xindex   = table->invpermZ[x];
00281     xlist    = table->subtableZ[x].nodelist;
00282     oldxkeys = table->subtableZ[x].keys;
00283     xslots   = table->subtableZ[x].slots;
00284     xshift   = table->subtableZ[x].shift;
00285     newxkeys = 0;
00286 
00287     /* Get parameters of y subtable. */
00288     yindex   = table->invpermZ[y];
00289     ylist    = table->subtableZ[y].nodelist;
00290     oldykeys = table->subtableZ[y].keys;
00291     yslots   = table->subtableZ[y].slots;
00292     yshift   = table->subtableZ[y].shift;
00293     newykeys = oldykeys;
00294 
00295     /* The nodes in the x layer are put in two chains.  The chain
00296     ** pointed by g holds the normal nodes. When re-expressed they stay
00297     ** in the x list. The chain pointed by special holds the elements
00298     ** that will move to the y list.
00299     */
00300     g = special = NULL;
00301     for (i = 0; i < xslots; i++) {
00302         f = xlist[i];
00303         if (f == NULL) continue;
00304         xlist[i] = NULL;
00305         while (f != NULL) {
00306             next = f->next;
00307             f1 = cuddT(f);
00308             /* if (f1->index == yindex) */ cuddSatDec(f1->ref);
00309             f0 = cuddE(f);
00310             /* if (f0->index == yindex) */ cuddSatDec(f0->ref);
00311             if ((int) f1->index == yindex && cuddE(f1) == empty &&
00312                 (int) f0->index != yindex) {
00313                 f->next = special;
00314                 special = f;
00315             } else {
00316                 f->next = g;
00317                 g = f;
00318             }
00319             f = next;
00320         } /* while there are elements in the collision chain */
00321     } /* for each slot of the x subtable */
00322 
00323     /* Mark y nodes with pointers from above x. We mark them by
00324     **  changing their index to x.
00325     */
00326     for (i = 0; i < yslots; i++) {
00327         f = ylist[i];
00328         while (f != NULL) {
00329             if (f->ref != 0) {
00330                 f->index = xindex;
00331             }
00332             f = f->next;
00333         } /* while there are elements in the collision chain */
00334     } /* for each slot of the y subtable */
00335 
00336     /* Move special nodes to the y list. */
00337     f = special;
00338     while (f != NULL) {
00339         next = f->next;
00340         f1 = cuddT(f);
00341         f11 = cuddT(f1);
00342         cuddT(f) = f11;
00343         cuddSatInc(f11->ref);
00344         f0 = cuddE(f);
00345         cuddSatInc(f0->ref);
00346         f->index = yindex;
00347         /* Insert at the beginning of the list so that it will be
00348         ** found first if there is a duplicate. The duplicate will
00349         ** eventually be moved or garbage collected. No node
00350         ** re-expression will add a pointer to it.
00351         */
00352         posn = ddHash(f11, f0, yshift);
00353         f->next = ylist[posn];
00354         ylist[posn] = f;
00355         newykeys++;
00356         f = next;
00357     }
00358 
00359     /* Take care of the remaining x nodes that must be re-expressed.
00360     ** They form a linked list pointed by g.
00361     */
00362     f = g;
00363     while (f != NULL) {
00364 #ifdef DD_COUNT
00365         table->swapSteps++;
00366 #endif
00367         next = f->next;
00368         /* Find f1, f0, f11, f10, f01, f00. */
00369         f1 = cuddT(f);
00370         if ((int) f1->index == yindex || (int) f1->index == xindex) {
00371             f11 = cuddT(f1); f10 = cuddE(f1);
00372         } else {
00373             f11 = empty; f10 = f1;
00374         }
00375         f0 = cuddE(f);
00376         if ((int) f0->index == yindex || (int) f0->index == xindex) {
00377             f01 = cuddT(f0); f00 = cuddE(f0);
00378         } else {
00379             f01 = empty; f00 = f0;
00380         }
00381         /* Create the new T child. */
00382         if (f01 == empty) {
00383             newf1 = f10;
00384             cuddSatInc(newf1->ref);
00385         } else {
00386             /* Check ylist for triple (yindex, f01, f10). */
00387             posn = ddHash(f01, f10, yshift);
00388             /* For each element newf1 in collision list ylist[posn]. */
00389             newf1 = ylist[posn];
00390             /* Search the collision chain skipping the marked nodes. */
00391             while (newf1 != NULL) {
00392                 if (cuddT(newf1) == f01 && cuddE(newf1) == f10 &&
00393                     (int) newf1->index == yindex) {
00394                     cuddSatInc(newf1->ref);
00395                     break; /* match */
00396                 }
00397                 newf1 = newf1->next;
00398             } /* while newf1 */
00399             if (newf1 == NULL) {        /* no match */
00400                 newf1 = cuddDynamicAllocNode(table);
00401                 if (newf1 == NULL)
00402                     goto zddSwapOutOfMem;
00403                 newf1->index = yindex; newf1->ref = 1;
00404                 cuddT(newf1) = f01;
00405                 cuddE(newf1) = f10;
00406                 /* Insert newf1 in the collision list ylist[pos];
00407                 ** increase the ref counts of f01 and f10
00408                 */
00409                 newykeys++;
00410                 newf1->next = ylist[posn];
00411                 ylist[posn] = newf1;
00412                 cuddSatInc(f01->ref);
00413                 cuddSatInc(f10->ref);
00414             }
00415         }
00416         cuddT(f) = newf1;
00417 
00418         /* Do the same for f0. */
00419         /* Create the new E child. */
00420         if (f11 == empty) {
00421             newf0 = f00;
00422             cuddSatInc(newf0->ref);
00423         } else {
00424             /* Check ylist for triple (yindex, f11, f00). */
00425             posn = ddHash(f11, f00, yshift);
00426             /* For each element newf0 in collision list ylist[posn]. */
00427             newf0 = ylist[posn];
00428             while (newf0 != NULL) {
00429                 if (cuddT(newf0) == f11 && cuddE(newf0) == f00 &&
00430                     (int) newf0->index == yindex) {
00431                     cuddSatInc(newf0->ref);
00432                     break; /* match */
00433                 }
00434                 newf0 = newf0->next;
00435             } /* while newf0 */
00436             if (newf0 == NULL) {        /* no match */
00437                 newf0 = cuddDynamicAllocNode(table);
00438                 if (newf0 == NULL)
00439                     goto zddSwapOutOfMem;
00440                 newf0->index = yindex; newf0->ref = 1;
00441                 cuddT(newf0) = f11; cuddE(newf0) = f00;
00442                 /* Insert newf0 in the collision list ylist[posn];
00443                 ** increase the ref counts of f11 and f00.
00444                 */
00445                 newykeys++;
00446                 newf0->next = ylist[posn];
00447                 ylist[posn] = newf0;
00448                 cuddSatInc(f11->ref);
00449                 cuddSatInc(f00->ref);
00450             }
00451         }
00452         cuddE(f) = newf0;
00453 
00454         /* Re-insert the modified f in xlist.
00455         ** The modified f does not already exists in xlist.
00456         ** (Because of the uniqueness of the cofactors.)
00457         */
00458         posn = ddHash(newf1, newf0, xshift);
00459         newxkeys++;
00460         f->next = xlist[posn];
00461         xlist[posn] = f;
00462         f = next;
00463     } /* while f != NULL */
00464 
00465     /* GC the y layer and move the marked nodes to the x list. */
00466 
00467     /* For each node f in ylist. */
00468     for (i = 0; i < yslots; i++) {
00469         previous = NULL;
00470         f = ylist[i];
00471         while (f != NULL) {
00472             next = f->next;
00473             if (f->ref == 0) {
00474                 cuddSatDec(cuddT(f)->ref);
00475                 cuddSatDec(cuddE(f)->ref);
00476                 cuddDeallocNode(table, f);
00477                 newykeys--;
00478                 if (previous == NULL)
00479                     ylist[i] = next;
00480                 else
00481                     previous->next = next;
00482             } else if ((int) f->index == xindex) { /* move marked node */
00483                 if (previous == NULL)
00484                     ylist[i] = next;
00485                 else
00486                     previous->next = next;
00487                 f1 = cuddT(f);
00488                 cuddSatDec(f1->ref);
00489                 /* Check ylist for triple (yindex, f1, empty). */
00490                 posn = ddHash(f1, empty, yshift);
00491                 /* For each element newf1 in collision list ylist[posn]. */
00492                 newf1 = ylist[posn];
00493                 while (newf1 != NULL) {
00494                     if (cuddT(newf1) == f1 && cuddE(newf1) == empty &&
00495                         (int) newf1->index == yindex) {
00496                         cuddSatInc(newf1->ref);
00497                         break; /* match */
00498                     }
00499                     newf1 = newf1->next;
00500                 } /* while newf1 */
00501                 if (newf1 == NULL) {    /* no match */
00502                     newf1 = cuddDynamicAllocNode(table);
00503                     if (newf1 == NULL)
00504                         goto zddSwapOutOfMem;
00505                     newf1->index = yindex; newf1->ref = 1;
00506                     cuddT(newf1) = f1; cuddE(newf1) = empty;
00507                     /* Insert newf1 in the collision list ylist[posn];
00508                     ** increase the ref counts of f1 and empty.
00509                     */
00510                     newykeys++;
00511                     newf1->next = ylist[posn];
00512                     ylist[posn] = newf1;
00513                     if (posn == i && previous == NULL)
00514                         previous = newf1;
00515                     cuddSatInc(f1->ref);
00516                     cuddSatInc(empty->ref);
00517                 }
00518                 cuddT(f) = newf1;
00519                 f0 = cuddE(f);
00520                 /* Insert f in x list. */
00521                 posn = ddHash(newf1, f0, xshift);
00522                 newxkeys++;
00523                 newykeys--;
00524                 f->next = xlist[posn];
00525                 xlist[posn] = f;
00526             } else {
00527                 previous = f;
00528             }
00529             f = next;
00530         } /* while f */
00531     } /* for i */
00532 
00533     /* Set the appropriate fields in table. */
00534     table->subtableZ[x].keys     = newxkeys;
00535     table->subtableZ[y].keys     = newykeys;
00536 
00537     table->keysZ += newxkeys + newykeys - oldxkeys - oldykeys;
00538 
00539     /* Update univ section; univ[x] remains the same. */
00540     table->univ[y] = cuddT(table->univ[x]);
00541 
00542 #if 0
00543     (void) fprintf(table->out,"x = %d  y = %d\n", x, y);
00544     (void) Cudd_DebugCheck(table);
00545     (void) Cudd_CheckKeys(table);
00546 #endif
00547 
00548     return (table->keysZ);
00549 
00550 zddSwapOutOfMem:
00551     (void) fprintf(table->err, "Error: cuddZddSwapInPlace out of memory\n");
00552 
00553     return (0);
00554 
00555 } /* end of cuddZddLinearInPlace */
00556 
00557 
00572 static int
00573 cuddZddLinearAux(
00574   DdManager * table,
00575   int  x,
00576   int  xLow,
00577   int  xHigh)
00578 {
00579     Move        *move;
00580     Move        *moveUp;        /* list of up move */
00581     Move        *moveDown;      /* list of down move */
00582 
00583     int         initial_size;
00584     int         result;
00585 
00586     initial_size = table->keysZ;
00587 
00588 #ifdef DD_DEBUG
00589     assert(table->subtableZ[x].keys > 0);
00590 #endif
00591 
00592     moveDown = NULL;
00593     moveUp = NULL;
00594 
00595     if (x == xLow) {
00596         moveDown = cuddZddLinearDown(table, x, xHigh, NULL);
00597         /* At this point x --> xHigh. */
00598         if (moveDown == (Move *) CUDD_OUT_OF_MEM)
00599             goto cuddZddLinearAuxOutOfMem;
00600         /* Move backward and stop at best position. */
00601         result = cuddZddLinearBackward(table, initial_size, moveDown);
00602         if (!result)
00603             goto cuddZddLinearAuxOutOfMem;
00604 
00605     } else if (x == xHigh) {
00606         moveUp = cuddZddLinearUp(table, x, xLow, NULL);
00607         /* At this point x --> xLow. */
00608         if (moveUp == (Move *) CUDD_OUT_OF_MEM)
00609             goto cuddZddLinearAuxOutOfMem;
00610         /* Move backward and stop at best position. */
00611         result = cuddZddLinearBackward(table, initial_size, moveUp);
00612         if (!result)
00613             goto cuddZddLinearAuxOutOfMem;
00614 
00615     } else if ((x - xLow) > (xHigh - x)) { /* must go down first: shorter */
00616         moveDown = cuddZddLinearDown(table, x, xHigh, NULL);
00617         /* At this point x --> xHigh. */
00618         if (moveDown == (Move *) CUDD_OUT_OF_MEM)
00619             goto cuddZddLinearAuxOutOfMem;
00620         moveUp = cuddZddUndoMoves(table,moveDown);
00621 #ifdef DD_DEBUG
00622         assert(moveUp == NULL || moveUp->x == x);
00623 #endif
00624         moveUp = cuddZddLinearUp(table, x, xLow, moveUp);
00625         if (moveUp == (Move *) CUDD_OUT_OF_MEM)
00626             goto cuddZddLinearAuxOutOfMem;
00627         /* Move backward and stop at best position. */
00628         result = cuddZddLinearBackward(table, initial_size, moveUp);
00629         if (!result)
00630             goto cuddZddLinearAuxOutOfMem;
00631 
00632     } else {
00633         moveUp = cuddZddLinearUp(table, x, xLow, NULL);
00634         /* At this point x --> xHigh. */
00635         if (moveUp == (Move *) CUDD_OUT_OF_MEM)
00636             goto cuddZddLinearAuxOutOfMem;
00637         /* Then move up. */
00638         moveDown = cuddZddUndoMoves(table,moveUp);
00639 #ifdef DD_DEBUG
00640         assert(moveDown == NULL || moveDown->y == x);
00641 #endif
00642         moveDown = cuddZddLinearDown(table, x, xHigh, moveDown);
00643         if (moveDown == (Move *) CUDD_OUT_OF_MEM)
00644             goto cuddZddLinearAuxOutOfMem;
00645         /* Move backward and stop at best position. */
00646         result = cuddZddLinearBackward(table, initial_size, moveDown);
00647         if (!result)
00648             goto cuddZddLinearAuxOutOfMem;
00649     }
00650 
00651     while (moveDown != NULL) {
00652         move = moveDown->next;
00653         cuddDeallocMove(table, moveDown);
00654         moveDown = move;
00655     }
00656     while (moveUp != NULL) {
00657         move = moveUp->next;
00658         cuddDeallocMove(table, moveUp);
00659         moveUp = move;
00660     }
00661 
00662     return(1);
00663 
00664 cuddZddLinearAuxOutOfMem:
00665     if (moveDown != (Move *) CUDD_OUT_OF_MEM) {
00666         while (moveDown != NULL) {
00667             move = moveDown->next;
00668             cuddDeallocMove(table, moveDown);
00669             moveDown = move;
00670         }
00671     }
00672     if (moveUp != (Move *) CUDD_OUT_OF_MEM) {
00673         while (moveUp != NULL) {
00674             move = moveUp->next;
00675             cuddDeallocMove(table, moveUp);
00676             moveUp = move;
00677         }
00678     }
00679 
00680     return(0);
00681 
00682 } /* end of cuddZddLinearAux */
00683 
00684 
00699 static Move *
00700 cuddZddLinearUp(
00701   DdManager * table,
00702   int  y,
00703   int  xLow,
00704   Move * prevMoves)
00705 {
00706     Move        *moves;
00707     Move        *move;
00708     int         x;
00709     int         size, newsize;
00710     int         limitSize;
00711 
00712     moves = prevMoves;
00713     limitSize = table->keysZ;
00714 
00715     x = cuddZddNextLow(table, y);
00716     while (x >= xLow) {
00717         size = cuddZddSwapInPlace(table, x, y);
00718         if (size == 0)
00719             goto cuddZddLinearUpOutOfMem;
00720         newsize = cuddZddLinearInPlace(table, x, y);
00721         if (newsize == 0)
00722             goto cuddZddLinearUpOutOfMem;
00723         move = (Move *) cuddDynamicAllocNode(table);
00724         if (move == NULL)
00725             goto cuddZddLinearUpOutOfMem;
00726         move->x = x;
00727         move->y = y;
00728         move->next = moves;
00729         moves = move;
00730         move->flags = CUDD_SWAP_MOVE;
00731         if (newsize > size) {
00732             /* Undo transformation. The transformation we apply is
00733             ** its own inverse. Hence, we just apply the transformation
00734             ** again.
00735             */
00736             newsize = cuddZddLinearInPlace(table,x,y);
00737             if (newsize == 0) goto cuddZddLinearUpOutOfMem;
00738 #ifdef DD_DEBUG
00739             if (newsize != size) {
00740                 (void) fprintf(table->err,"Change in size after identity transformation! From %d to %d\n",size,newsize);
00741             }
00742 #endif
00743         } else {
00744             size = newsize;
00745             move->flags = CUDD_LINEAR_TRANSFORM_MOVE;
00746         }
00747         move->size = size;
00748 
00749         if ((double)size > (double)limitSize * table->maxGrowth)
00750             break;
00751         if (size < limitSize)
00752             limitSize = size;
00753 
00754         y = x;
00755         x = cuddZddNextLow(table, y);
00756     }
00757     return(moves);
00758 
00759 cuddZddLinearUpOutOfMem:
00760     while (moves != NULL) {
00761         move = moves->next;
00762         cuddDeallocMove(table, moves);
00763         moves = move;
00764     }
00765     return((Move *) CUDD_OUT_OF_MEM);
00766 
00767 } /* end of cuddZddLinearUp */
00768 
00769 
00784 static Move *
00785 cuddZddLinearDown(
00786   DdManager * table,
00787   int  x,
00788   int  xHigh,
00789   Move * prevMoves)
00790 {
00791     Move        *moves;
00792     Move        *move;
00793     int         y;
00794     int         size, newsize;
00795     int         limitSize;
00796 
00797     moves = prevMoves;
00798     limitSize = table->keysZ;
00799 
00800     y = cuddZddNextHigh(table, x);
00801     while (y <= xHigh) {
00802         size = cuddZddSwapInPlace(table, x, y);
00803         if (size == 0)
00804             goto cuddZddLinearDownOutOfMem;
00805         newsize = cuddZddLinearInPlace(table, x, y);
00806         if (newsize == 0)
00807             goto cuddZddLinearDownOutOfMem;
00808         move = (Move *) cuddDynamicAllocNode(table);
00809         if (move == NULL)
00810             goto cuddZddLinearDownOutOfMem;
00811         move->x = x;
00812         move->y = y;
00813         move->next = moves;
00814         moves = move;
00815         move->flags = CUDD_SWAP_MOVE;
00816         if (newsize > size) {
00817             /* Undo transformation. The transformation we apply is
00818             ** its own inverse. Hence, we just apply the transformation
00819             ** again.
00820             */
00821             newsize = cuddZddLinearInPlace(table,x,y);
00822             if (newsize == 0) goto cuddZddLinearDownOutOfMem;
00823             if (newsize != size) {
00824                 (void) fprintf(table->err,"Change in size after identity transformation! From %d to %d\n",size,newsize);
00825             }
00826         } else {
00827             size = newsize;
00828             move->flags = CUDD_LINEAR_TRANSFORM_MOVE;
00829         }
00830         move->size = size;
00831 
00832         if ((double)size > (double)limitSize * table->maxGrowth)
00833             break;
00834         if (size < limitSize)
00835             limitSize = size;
00836 
00837         x = y;
00838         y = cuddZddNextHigh(table, x);
00839     }
00840     return(moves);
00841 
00842 cuddZddLinearDownOutOfMem:
00843     while (moves != NULL) {
00844         move = moves->next;
00845         cuddDeallocMove(table, moves);
00846         moves = move;
00847     }
00848     return((Move *) CUDD_OUT_OF_MEM);
00849 
00850 } /* end of cuddZddLinearDown */
00851 
00852 
00868 static int
00869 cuddZddLinearBackward(
00870   DdManager * table,
00871   int  size,
00872   Move * moves)
00873 {
00874     Move        *move;
00875     int         res;
00876 
00877     /* Find the minimum size among moves. */
00878     for (move = moves; move != NULL; move = move->next) {
00879         if (move->size < size) {
00880             size = move->size;
00881         }
00882     }
00883 
00884     for (move = moves; move != NULL; move = move->next) {
00885         if (move->size == size) return(1);
00886         if (move->flags == CUDD_LINEAR_TRANSFORM_MOVE) {
00887             res = cuddZddLinearInPlace(table,(int)move->x,(int)move->y);
00888             if (!res) return(0);
00889         }
00890         res = cuddZddSwapInPlace(table, move->x, move->y);
00891         if (!res)
00892             return(0);
00893         if (move->flags == CUDD_INVERSE_TRANSFORM_MOVE) {
00894             res = cuddZddLinearInPlace(table,(int)move->x,(int)move->y);
00895             if (!res) return(0);
00896         }
00897     }
00898 
00899     return(1);
00900 
00901 } /* end of cuddZddLinearBackward */
00902 
00903 
00916 static Move*
00917 cuddZddUndoMoves(
00918   DdManager * table,
00919   Move * moves)
00920 {
00921     Move *invmoves = NULL;
00922     Move *move;
00923     Move *invmove;
00924     int size;
00925 
00926     for (move = moves; move != NULL; move = move->next) {
00927         invmove = (Move *) cuddDynamicAllocNode(table);
00928         if (invmove == NULL) goto cuddZddUndoMovesOutOfMem;
00929         invmove->x = move->x;
00930         invmove->y = move->y;
00931         invmove->next = invmoves;
00932         invmoves = invmove;
00933         if (move->flags == CUDD_SWAP_MOVE) {
00934             invmove->flags = CUDD_SWAP_MOVE;
00935             size = cuddZddSwapInPlace(table,(int)move->x,(int)move->y);
00936             if (!size) goto cuddZddUndoMovesOutOfMem;
00937         } else if (move->flags == CUDD_LINEAR_TRANSFORM_MOVE) {
00938             invmove->flags = CUDD_INVERSE_TRANSFORM_MOVE;
00939             size = cuddZddLinearInPlace(table,(int)move->x,(int)move->y);
00940             if (!size) goto cuddZddUndoMovesOutOfMem;
00941             size = cuddZddSwapInPlace(table,(int)move->x,(int)move->y);
00942             if (!size) goto cuddZddUndoMovesOutOfMem;
00943         } else { /* must be CUDD_INVERSE_TRANSFORM_MOVE */
00944 #ifdef DD_DEBUG
00945             (void) fprintf(table->err,"Unforseen event in ddUndoMoves!\n");
00946 #endif
00947             invmove->flags = CUDD_LINEAR_TRANSFORM_MOVE;
00948             size = cuddZddSwapInPlace(table,(int)move->x,(int)move->y);
00949             if (!size) goto cuddZddUndoMovesOutOfMem;
00950             size = cuddZddLinearInPlace(table,(int)move->x,(int)move->y);
00951             if (!size) goto cuddZddUndoMovesOutOfMem;
00952         }
00953         invmove->size = size;
00954     }
00955 
00956     return(invmoves);
00957 
00958 cuddZddUndoMovesOutOfMem:
00959     while (invmoves != NULL) {
00960         move = invmoves->next;
00961         cuddDeallocMove(table, invmoves);
00962         invmoves = move;
00963     }
00964     return((Move *) CUDD_OUT_OF_MEM);
00965 
00966 } /* end of cuddZddUndoMoves */
00967