distr/cudd/cuddZddLin.c

   1 /**CFile***********************************************************************
   2
   3   FileName    [cuddZddLin.c]
   4
   5   PackageName [cudd]
   6
   7   Synopsis    [Procedures for dynamic variable ordering of ZDDs.]
   8
   9   Description [Internal procedures included in this module:
  10                     <ul>
  11                     <li> cuddZddLinearSifting()
  12                     </ul>
  13                Static procedures included in this module:
  14                     <ul>
  15                     <li> cuddZddLinearInPlace()
  16                     <li> cuddZddLinerAux()
  17                     <li> cuddZddLinearUp()
  18                     <li> cuddZddLinearDown()
  19                     <li> cuddZddLinearBackward()
  20                     <li> cuddZddUndoMoves()
  21                     </ul>
  22               ]
  23
  24   SeeAlso     [cuddLinear.c cuddZddReord.c]
  25
  26   Author      [Fabio Somenzi]
  27
  28   Copyright   [Copyright (c) 1995-2004, Regents of the University of Colorado
  29
  30   All rights reserved.
  31
  32   Redistribution and use in source and binary forms, with or without
  33   modification, are permitted provided that the following conditions
  34   are met:
  35
  36   Redistributions of source code must retain the above copyright
  37   notice, this list of conditions and the following disclaimer.
  38
  39   Redistributions in binary form must reproduce the above copyright
  40   notice, this list of conditions and the following disclaimer in the
  41   documentation and/or other materials provided with the distribution.
  42
  43   Neither the name of the University of Colorado nor the names of its
  44   contributors may be used to endorse or promote products derived from
  45   this software without specific prior written permission.
  46
  47   THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS
  48   "AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT
  49   LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS
  50   FOR A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE
  51   COPYRIGHT OWNER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT,
  52   INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING,
  53   BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES;
  54   LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER
  55   CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT
  56   LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN
  57   ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE
  58   POSSIBILITY OF SUCH DAMAGE.]
  59
  60 ******************************************************************************/
  61
  62 #include "util.h"
  63 #include "cuddInt.h"
  64
  65 /*---------------------------------------------------------------------------*/
  66 /* Constant declarations                                                     */
  67 /*---------------------------------------------------------------------------*/
  68
  69 #define CUDD_SWAP_MOVE 0
  70 #define CUDD_LINEAR_TRANSFORM_MOVE 1
  71 #define CUDD_INVERSE_TRANSFORM_MOVE 2
  72
  73 /*---------------------------------------------------------------------------*/
  74 /* Stucture declarations                                                     */
  75 /*---------------------------------------------------------------------------*/
  76
  77
  78 /*---------------------------------------------------------------------------*/
  79 /* Type declarations                                                         */
  80 /*---------------------------------------------------------------------------*/
  81
  82
  83 /*---------------------------------------------------------------------------*/
  84 /* Variable declarations                                                     */
  85 /*---------------------------------------------------------------------------*/
  86
  87 #ifndef lint
  88 static char rcsid[] DD_UNUSED = "$Id: cuddZddLin.c,v 1.14 2004/08/13 18:04:53 fabio Exp $";
  89 #endif
  90
  91 extern  int     *zdd_entry;
  92 extern  int     zddTotalNumberSwapping;
  93 static  int     zddTotalNumberLinearTr;
  94 static  DdNode  *empty;
  95
  96
  97 /*---------------------------------------------------------------------------*/
  98 /* Macro declarations                                                        */
  99 /*---------------------------------------------------------------------------*/
 100
 101
 102 /**AutomaticStart*************************************************************/
 103
 104 /*---------------------------------------------------------------------------*/
 105 /* Static function prototypes                                                */
 106 /*---------------------------------------------------------------------------*/
 107
 108 static int cuddZddLinearInPlace (DdManager * table, int x, int y);
 109 static int cuddZddLinearAux (DdManager *table, int x, int xLow, int xHigh);
 110 static Move * cuddZddLinearUp (DdManager *table, int y, int xLow, Move *prevMoves);
 111 static Move * cuddZddLinearDown (DdManager *table, int x, int xHigh, Move *prevMoves);
 112 static int cuddZddLinearBackward (DdManager *table, int size, Move *moves);
 113 static Move* cuddZddUndoMoves (DdManager *table, Move *moves);
 114
 115 /**AutomaticEnd***************************************************************/
 116
 117
 118 /*---------------------------------------------------------------------------*/
 119 /* Definition of exported functions                                          */
 120 /*---------------------------------------------------------------------------*/
 121
 122
 123 /*---------------------------------------------------------------------------*/
 124 /* Definition of internal functions                                          */
 125 /*---------------------------------------------------------------------------*/
 126
 127
 128
 129
 130 /**Function********************************************************************
 131
 132   Synopsis    [Implementation of the linear sifting algorithm for ZDDs.]
 133
 134   Description [Implementation of the linear sifting algorithm for ZDDs.
 135   Assumes that no dead nodes are present.
 136     <ol>
 137     <li> Order all the variables according to the number of entries
 138     in each unique table.
 139     <li> Sift the variable up and down and applies the XOR transformation,
 140     remembering each time the total size of the DD heap.
 141     <li> Select the best permutation.
 142     <li> Repeat 3 and 4 for all variables.
 143     </ol>
 144   Returns 1 if successful; 0 otherwise.]
 145
 146   SideEffects [None]
 147
 148   SeeAlso     []
 149
 150 ******************************************************************************/
 151 int
 152 cuddZddLinearSifting(
 153   DdManager * table,
 154   int  lower,
 155   int  upper)
 156 {
 157     int i;
 158     int *var;
 159     int size;
 160     int x;
 161     int result;
 162 #ifdef DD_STATS
 163     int previousSize;
 164 #endif
 165
 166     size = table->sizeZ;
 167     empty = table->zero;
 168
 169     /* Find order in which to sift variables. */
 170     var = NULL;
 171     zdd_entry = ALLOC(int, size);
 172     if (zdd_entry == NULL) {
 173         table->errorCode = CUDD_MEMORY_OUT;
 174         goto cuddZddSiftingOutOfMem;
 175     }
 176     var = ALLOC(int, size);
 177     if (var == NULL) {
 178         table->errorCode = CUDD_MEMORY_OUT;
 179         goto cuddZddSiftingOutOfMem;
 180     }
 181
 182     for (i = 0; i < size; i++) {
 183         x = table->permZ[i];
 184         zdd_entry[i] = table->subtableZ[x].keys;
 185         var[i] = i;
 186     }
 187
 188     qsort((void *)var, size, sizeof(int), (DD_QSFP)cuddZddUniqueCompare);
 189
 190     /* Now sift. */
 191     for (i = 0; i < ddMin(table->siftMaxVar, size); i++) {
 192         if (zddTotalNumberSwapping >= table->siftMaxSwap)
 193             break;
 194         x = table->permZ[var[i]];
 195         if (x < lower || x > upper) continue;
 196 #ifdef DD_STATS
 197         previousSize = table->keysZ;
 198 #endif
 199         result = cuddZddLinearAux(table, x, lower, upper);
 200         if (!result)
 201             goto cuddZddSiftingOutOfMem;
 202 #ifdef DD_STATS
 203         if (table->keysZ < (unsigned) previousSize) {
 204             (void) fprintf(table->out,"-");
 205         } else if (table->keysZ > (unsigned) previousSize) {
 206             (void) fprintf(table->out,"+");     /* should never happen */
 207             (void) fprintf(table->out,"\nSize increased from %d to %d while sifting variable %d\n", previousSize, table->keysZ , var[i]);
 208         } else {
 209             (void) fprintf(table->out,"=");
 210         }
 211         fflush(table->out);
 212 #endif
 213     }
 214
 215     FREE(var);
 216     FREE(zdd_entry);
 217
 218     return(1);
 219
 220 cuddZddSiftingOutOfMem:
 221
 222     if (zdd_entry != NULL) FREE(zdd_entry);
 223     if (var != NULL) FREE(var);
 224
 225     return(0);
 226
 227 } /* end of cuddZddLinearSifting */
 228
 229
 230 /*---------------------------------------------------------------------------*/
 231 /* Definition of static functions                                            */
 232 /*---------------------------------------------------------------------------*/
 233
 234
 235 /**Function********************************************************************
 236
 237   Synopsis    [Linearly combines two adjacent variables.]
 238
 239   Description [Linearly combines two adjacent variables. It assumes
 240   that no dead nodes are present on entry to this procedure.  The
 241   procedure then guarantees that no dead nodes will be present when it
 242   terminates.  cuddZddLinearInPlace assumes that x &lt; y.  Returns the
 243   number of keys in the table if successful; 0 otherwise.]
 244
 245   SideEffects [None]
 246
 247   SeeAlso     [cuddZddSwapInPlace cuddLinearInPlace]
 248
 249 ******************************************************************************/
 250 static int
 251 cuddZddLinearInPlace(
 252   DdManager * table,
 253   int  x,
 254   int  y)
 255 {
 256     DdNodePtr *xlist, *ylist;
 257     int         xindex, yindex;
 258     int         xslots, yslots;
 259     int         xshift, yshift;
 260     int         oldxkeys, oldykeys;
 261     int         newxkeys, newykeys;
 262     int         i;
 263     int         posn;
 264     DdNode      *f, *f1, *f0, *f11, *f10, *f01, *f00;
 265     DdNode      *newf1, *newf0, *g, *next, *previous;
 266     DdNode      *special;
 267
 268 #ifdef DD_DEBUG
 269     assert(x < y);
 270     assert(cuddZddNextHigh(table,x) == y);
 271     assert(table->subtableZ[x].keys != 0);
 272     assert(table->subtableZ[y].keys != 0);
 273     assert(table->subtableZ[x].dead == 0);
 274     assert(table->subtableZ[y].dead == 0);
 275 #endif
 276
 277     zddTotalNumberLinearTr++;
 278
 279     /* Get parameters of x subtable. */
 280     xindex   = table->invpermZ[x];
 281     xlist    = table->subtableZ[x].nodelist;
 282     oldxkeys = table->subtableZ[x].keys;
 283     xslots   = table->subtableZ[x].slots;
 284     xshift   = table->subtableZ[x].shift;
 285     newxkeys = 0;
 286
 287     /* Get parameters of y subtable. */
 288     yindex   = table->invpermZ[y];
 289     ylist    = table->subtableZ[y].nodelist;
 290     oldykeys = table->subtableZ[y].keys;
 291     yslots   = table->subtableZ[y].slots;
 292     yshift   = table->subtableZ[y].shift;
 293     newykeys = oldykeys;
 294
 295     /* The nodes in the x layer are put in two chains.  The chain
 296     ** pointed by g holds the normal nodes. When re-expressed they stay
 297     ** in the x list. The chain pointed by special holds the elements
 298     ** that will move to the y list.
 299     */
 300     g = special = NULL;
 301     for (i = 0; i < xslots; i++) {
 302         f = xlist[i];
 303         if (f == NULL) continue;
 304         xlist[i] = NULL;
 305         while (f != NULL) {
 306             next = f->next;
 307             f1 = cuddT(f);
 308             /* if (f1->index == yindex) */ cuddSatDec(f1->ref);
 309             f0 = cuddE(f);
 310             /* if (f0->index == yindex) */ cuddSatDec(f0->ref);
 311             if ((int) f1->index == yindex && cuddE(f1) == empty &&
 312                 (int) f0->index != yindex) {
 313                 f->next = special;
 314                 special = f;
 315             } else {
 316                 f->next = g;
 317                 g = f;
 318             }
 319             f = next;
 320         } /* while there are elements in the collision chain */
 321     } /* for each slot of the x subtable */
 322
 323     /* Mark y nodes with pointers from above x. We mark them by
 324     **  changing their index to x.
 325     */
 326     for (i = 0; i < yslots; i++) {
 327         f = ylist[i];
 328         while (f != NULL) {
 329             if (f->ref != 0) {
 330                 f->index = xindex;
 331             }
 332             f = f->next;
 333         } /* while there are elements in the collision chain */
 334     } /* for each slot of the y subtable */
 335
 336     /* Move special nodes to the y list. */
 337     f = special;
 338     while (f != NULL) {
 339         next = f->next;
 340         f1 = cuddT(f);
 341         f11 = cuddT(f1);
 342         cuddT(f) = f11;
 343         cuddSatInc(f11->ref);
 344         f0 = cuddE(f);
 345         cuddSatInc(f0->ref);
 346         f->index = yindex;
 347         /* Insert at the beginning of the list so that it will be
 348         ** found first if there is a duplicate. The duplicate will
 349         ** eventually be moved or garbage collected. No node
 350         ** re-expression will add a pointer to it.
 351         */
 352         posn = ddHash(f11, f0, yshift);
 353         f->next = ylist[posn];
 354         ylist[posn] = f;
 355         newykeys++;
 356         f = next;
 357     }
 358
 359     /* Take care of the remaining x nodes that must be re-expressed.
 360     ** They form a linked list pointed by g.
 361     */
 362     f = g;
 363     while (f != NULL) {
 364 #ifdef DD_COUNT
 365         table->swapSteps++;
 366 #endif
 367         next = f->next;
 368         /* Find f1, f0, f11, f10, f01, f00. */
 369         f1 = cuddT(f);
 370         if ((int) f1->index == yindex || (int) f1->index == xindex) {
 371             f11 = cuddT(f1); f10 = cuddE(f1);
 372         } else {
 373             f11 = empty; f10 = f1;
 374         }
 375         f0 = cuddE(f);
 376         if ((int) f0->index == yindex || (int) f0->index == xindex) {
 377             f01 = cuddT(f0); f00 = cuddE(f0);
 378         } else {
 379             f01 = empty; f00 = f0;
 380         }
 381         /* Create the new T child. */
 382         if (f01 == empty) {
 383             newf1 = f10;
 384             cuddSatInc(newf1->ref);
 385         } else {
 386             /* Check ylist for triple (yindex, f01, f10). */
 387             posn = ddHash(f01, f10, yshift);
 388             /* For each element newf1 in collision list ylist[posn]. */
 389             newf1 = ylist[posn];
 390             /* Search the collision chain skipping the marked nodes. */
 391             while (newf1 != NULL) {
 392                 if (cuddT(newf1) == f01 && cuddE(newf1) == f10 &&
 393                     (int) newf1->index == yindex) {
 394                     cuddSatInc(newf1->ref);
 395                     break; /* match */
 396                 }
 397                 newf1 = newf1->next;
 398             } /* while newf1 */
 399             if (newf1 == NULL) {        /* no match */
 400                 newf1 = cuddDynamicAllocNode(table);
 401                 if (newf1 == NULL)
 402                     goto zddSwapOutOfMem;
 403                 newf1->index = yindex; newf1->ref = 1;
 404                 cuddT(newf1) = f01;
 405                 cuddE(newf1) = f10;
 406                 /* Insert newf1 in the collision list ylist[pos];
 407                 ** increase the ref counts of f01 and f10
 408                 */
 409                 newykeys++;
 410                 newf1->next = ylist[posn];
 411                 ylist[posn] = newf1;
 412                 cuddSatInc(f01->ref);
 413                 cuddSatInc(f10->ref);
 414             }
 415         }
 416         cuddT(f) = newf1;
 417
 418         /* Do the same for f0. */
 419         /* Create the new E child. */
 420         if (f11 == empty) {
 421             newf0 = f00;
 422             cuddSatInc(newf0->ref);
 423         } else {
 424             /* Check ylist for triple (yindex, f11, f00). */
 425             posn = ddHash(f11, f00, yshift);
 426             /* For each element newf0 in collision list ylist[posn]. */
 427             newf0 = ylist[posn];
 428             while (newf0 != NULL) {
 429                 if (cuddT(newf0) == f11 && cuddE(newf0) == f00 &&
 430                     (int) newf0->index == yindex) {
 431                     cuddSatInc(newf0->ref);
 432                     break; /* match */
 433                 }
 434                 newf0 = newf0->next;
 435             } /* while newf0 */
 436             if (newf0 == NULL) {        /* no match */
 437                 newf0 = cuddDynamicAllocNode(table);
 438                 if (newf0 == NULL)
 439                     goto zddSwapOutOfMem;
 440                 newf0->index = yindex; newf0->ref = 1;
 441                 cuddT(newf0) = f11; cuddE(newf0) = f00;
 442                 /* Insert newf0 in the collision list ylist[posn];
 443                 ** increase the ref counts of f11 and f00.
 444                 */
 445                 newykeys++;
 446                 newf0->next = ylist[posn];
 447                 ylist[posn] = newf0;
 448                 cuddSatInc(f11->ref);
 449                 cuddSatInc(f00->ref);
 450             }
 451         }
 452         cuddE(f) = newf0;
 453
 454         /* Re-insert the modified f in xlist.
 455         ** The modified f does not already exists in xlist.
 456         ** (Because of the uniqueness of the cofactors.)
 457         */
 458         posn = ddHash(newf1, newf0, xshift);
 459         newxkeys++;
 460         f->next = xlist[posn];
 461         xlist[posn] = f;
 462         f = next;
 463     } /* while f != NULL */
 464
 465     /* GC the y layer and move the marked nodes to the x list. */
 466
 467     /* For each node f in ylist. */
 468     for (i = 0; i < yslots; i++) {
 469         previous = NULL;
 470         f = ylist[i];
 471         while (f != NULL) {
 472             next = f->next;
 473             if (f->ref == 0) {
 474                 cuddSatDec(cuddT(f)->ref);
 475                 cuddSatDec(cuddE(f)->ref);
 476                 cuddDeallocNode(table, f);
 477                 newykeys--;
 478                 if (previous == NULL)
 479                     ylist[i] = next;
 480                 else
 481                     previous->next = next;
 482             } else if ((int) f->index == xindex) { /* move marked node */
 483                 if (previous == NULL)
 484                     ylist[i] = next;
 485                 else
 486                     previous->next = next;
 487                 f1 = cuddT(f);
 488                 cuddSatDec(f1->ref);
 489                 /* Check ylist for triple (yindex, f1, empty). */
 490                 posn = ddHash(f1, empty, yshift);
 491                 /* For each element newf1 in collision list ylist[posn]. */
 492                 newf1 = ylist[posn];
 493                 while (newf1 != NULL) {
 494                     if (cuddT(newf1) == f1 && cuddE(newf1) == empty &&
 495                         (int) newf1->index == yindex) {
 496                         cuddSatInc(newf1->ref);
 497                         break; /* match */
 498                     }
 499                     newf1 = newf1->next;
 500                 } /* while newf1 */
 501                 if (newf1 == NULL) {    /* no match */
 502                     newf1 = cuddDynamicAllocNode(table);
 503                     if (newf1 == NULL)
 504                         goto zddSwapOutOfMem;
 505                     newf1->index = yindex; newf1->ref = 1;
 506                     cuddT(newf1) = f1; cuddE(newf1) = empty;
 507                     /* Insert newf1 in the collision list ylist[posn];
 508                     ** increase the ref counts of f1 and empty.
 509                     */
 510                     newykeys++;
 511                     newf1->next = ylist[posn];
 512                     ylist[posn] = newf1;
 513                     if (posn == i && previous == NULL)
 514                         previous = newf1;
 515                     cuddSatInc(f1->ref);
 516                     cuddSatInc(empty->ref);
 517                 }
 518                 cuddT(f) = newf1;
 519                 f0 = cuddE(f);
 520                 /* Insert f in x list. */
 521                 posn = ddHash(newf1, f0, xshift);
 522                 newxkeys++;
 523                 newykeys--;
 524                 f->next = xlist[posn];
 525                 xlist[posn] = f;
 526             } else {
 527                 previous = f;
 528             }
 529             f = next;
 530         } /* while f */
 531     } /* for i */
 532
 533     /* Set the appropriate fields in table. */
 534     table->subtableZ[x].keys     = newxkeys;
 535     table->subtableZ[y].keys     = newykeys;
 536
 537     table->keysZ += newxkeys + newykeys - oldxkeys - oldykeys;
 538
 539     /* Update univ section; univ[x] remains the same. */
 540     table->univ[y] = cuddT(table->univ[x]);
 541
 542 #if 0
 543     (void) fprintf(table->out,"x = %d  y = %d\n", x, y);
 544     (void) Cudd_DebugCheck(table);
 545     (void) Cudd_CheckKeys(table);
 546 #endif
 547
 548     return (table->keysZ);
 549
 550 zddSwapOutOfMem:
 551     (void) fprintf(table->err, "Error: cuddZddSwapInPlace out of memory\n");
 552
 553     return (0);
 554
 555 } /* end of cuddZddLinearInPlace */
 556
 557
 558 /**Function********************************************************************
 559
 560   Synopsis    [Given xLow <= x <= xHigh moves x up and down between the
 561   boundaries.]
 562
 563   Description [Given xLow <= x <= xHigh moves x up and down between the
 564   boundaries. Finds the best position and does the required changes.
 565   Returns 1 if successful; 0 otherwise.]
 566
 567   SideEffects [None]
 568
 569   SeeAlso     []
 570
 571 ******************************************************************************/
 572 static int
 573 cuddZddLinearAux(
 574   DdManager * table,
 575   int  x,
 576   int  xLow,
 577   int  xHigh)
 578 {
 579     Move        *move;
 580     Move        *moveUp;        /* list of up move */
 581     Move        *moveDown;      /* list of down move */
 582
 583     int         initial_size;
 584     int         result;
 585
 586     initial_size = table->keysZ;
 587
 588 #ifdef DD_DEBUG
 589     assert(table->subtableZ[x].keys > 0);
 590 #endif
 591
 592     moveDown = NULL;
 593     moveUp = NULL;
 594
 595     if (x == xLow) {
 596         moveDown = cuddZddLinearDown(table, x, xHigh, NULL);
 597         /* At this point x --> xHigh. */
 598         if (moveDown == (Move *) CUDD_OUT_OF_MEM)
 599             goto cuddZddLinearAuxOutOfMem;
 600         /* Move backward and stop at best position. */
 601         result = cuddZddLinearBackward(table, initial_size, moveDown);
 602         if (!result)
 603             goto cuddZddLinearAuxOutOfMem;
 604
 605     } else if (x == xHigh) {
 606         moveUp = cuddZddLinearUp(table, x, xLow, NULL);
 607         /* At this point x --> xLow. */
 608         if (moveUp == (Move *) CUDD_OUT_OF_MEM)
 609             goto cuddZddLinearAuxOutOfMem;
 610         /* Move backward and stop at best position. */
 611         result = cuddZddLinearBackward(table, initial_size, moveUp);
 612         if (!result)
 613             goto cuddZddLinearAuxOutOfMem;
 614
 615     } else if ((x - xLow) > (xHigh - x)) { /* must go down first: shorter */
 616         moveDown = cuddZddLinearDown(table, x, xHigh, NULL);
 617         /* At this point x --> xHigh. */
 618         if (moveDown == (Move *) CUDD_OUT_OF_MEM)
 619             goto cuddZddLinearAuxOutOfMem;
 620         moveUp = cuddZddUndoMoves(table,moveDown);
 621 #ifdef DD_DEBUG
 622         assert(moveUp == NULL || moveUp->x == x);
 623 #endif
 624         moveUp = cuddZddLinearUp(table, x, xLow, moveUp);
 625         if (moveUp == (Move *) CUDD_OUT_OF_MEM)
 626             goto cuddZddLinearAuxOutOfMem;
 627         /* Move backward and stop at best position. */
 628         result = cuddZddLinearBackward(table, initial_size, moveUp);
 629         if (!result)
 630             goto cuddZddLinearAuxOutOfMem;
 631
 632     } else {
 633         moveUp = cuddZddLinearUp(table, x, xLow, NULL);
 634         /* At this point x --> xHigh. */
 635         if (moveUp == (Move *) CUDD_OUT_OF_MEM)
 636             goto cuddZddLinearAuxOutOfMem;
 637         /* Then move up. */
 638         moveDown = cuddZddUndoMoves(table,moveUp);
 639 #ifdef DD_DEBUG
 640         assert(moveDown == NULL || moveDown->y == x);
 641 #endif
 642         moveDown = cuddZddLinearDown(table, x, xHigh, moveDown);
 643         if (moveDown == (Move *) CUDD_OUT_OF_MEM)
 644             goto cuddZddLinearAuxOutOfMem;
 645         /* Move backward and stop at best position. */
 646         result = cuddZddLinearBackward(table, initial_size, moveDown);
 647         if (!result)
 648             goto cuddZddLinearAuxOutOfMem;
 649     }
 650
 651     while (moveDown != NULL) {
 652         move = moveDown->next;
 653         cuddDeallocMove(table, moveDown);
 654         moveDown = move;
 655     }
 656     while (moveUp != NULL) {
 657         move = moveUp->next;
 658         cuddDeallocMove(table, moveUp);
 659         moveUp = move;
 660     }
 661
 662     return(1);
 663
 664 cuddZddLinearAuxOutOfMem:
 665     if (moveDown != (Move *) CUDD_OUT_OF_MEM) {
 666         while (moveDown != NULL) {
 667             move = moveDown->next;
 668             cuddDeallocMove(table, moveDown);
 669             moveDown = move;
 670         }
 671     }
 672     if (moveUp != (Move *) CUDD_OUT_OF_MEM) {
 673         while (moveUp != NULL) {
 674             move = moveUp->next;
 675             cuddDeallocMove(table, moveUp);
 676             moveUp = move;
 677         }
 678     }
 679
 680     return(0);
 681
 682 } /* end of cuddZddLinearAux */
 683
 684
 685 /**Function********************************************************************
 686
 687   Synopsis    [Sifts a variable up applying the XOR transformation.]
 688
 689   Description [Sifts a variable up applying the XOR
 690   transformation. Moves y up until either it reaches the bound (xLow)
 691   or the size of the ZDD heap increases too much.  Returns the set of
 692   moves in case of success; NULL if memory is full.]
 693
 694   SideEffects [None]
 695
 696   SeeAlso     []
 697
 698 ******************************************************************************/
 699 static Move *
 700 cuddZddLinearUp(
 701   DdManager * table,
 702   int  y,
 703   int  xLow,
 704   Move * prevMoves)
 705 {
 706     Move        *moves;
 707     Move        *move;
 708     int         x;
 709     int         size, newsize;
 710     int         limitSize;
 711
 712     moves = prevMoves;
 713     limitSize = table->keysZ;
 714
 715     x = cuddZddNextLow(table, y);
 716     while (x >= xLow) {
 717         size = cuddZddSwapInPlace(table, x, y);
 718         if (size == 0)
 719             goto cuddZddLinearUpOutOfMem;
 720         newsize = cuddZddLinearInPlace(table, x, y);
 721         if (newsize == 0)
 722             goto cuddZddLinearUpOutOfMem;
 723         move = (Move *) cuddDynamicAllocNode(table);
 724         if (move == NULL)
 725             goto cuddZddLinearUpOutOfMem;
 726         move->x = x;
 727         move->y = y;
 728         move->next = moves;
 729         moves = move;
 730         move->flags = CUDD_SWAP_MOVE;
 731         if (newsize > size) {
 732             /* Undo transformation. The transformation we apply is
 733             ** its own inverse. Hence, we just apply the transformation
 734             ** again.
 735             */
 736             newsize = cuddZddLinearInPlace(table,x,y);
 737             if (newsize == 0) goto cuddZddLinearUpOutOfMem;
 738 #ifdef DD_DEBUG
 739             if (newsize != size) {
 740                 (void) fprintf(table->err,"Change in size after identity transformation! From %d to %d\n",size,newsize);
 741             }
 742 #endif
 743         } else {
 744             size = newsize;
 745             move->flags = CUDD_LINEAR_TRANSFORM_MOVE;
 746         }
 747         move->size = size;
 748
 749         if ((double)size > (double)limitSize * table->maxGrowth)
 750             break;
 751         if (size < limitSize)
 752             limitSize = size;
 753
 754         y = x;
 755         x = cuddZddNextLow(table, y);
 756     }
 757     return(moves);
 758
 759 cuddZddLinearUpOutOfMem:
 760     while (moves != NULL) {
 761         move = moves->next;
 762         cuddDeallocMove(table, moves);
 763         moves = move;
 764     }
 765     return((Move *) CUDD_OUT_OF_MEM);
 766
 767 } /* end of cuddZddLinearUp */
 768
 769
 770 /**Function********************************************************************
 771
 772   Synopsis    [Sifts a variable down and applies the XOR transformation.]
 773
 774   Description [Sifts a variable down. Moves x down until either it
 775   reaches the bound (xHigh) or the size of the ZDD heap increases too
 776   much. Returns the set of moves in case of success; NULL if memory is
 777   full.]
 778
 779   SideEffects [None]
 780
 781   SeeAlso     []
 782
 783 ******************************************************************************/
 784 static Move *
 785 cuddZddLinearDown(
 786   DdManager * table,
 787   int  x,
 788   int  xHigh,
 789   Move * prevMoves)
 790 {
 791     Move        *moves;
 792     Move        *move;
 793     int         y;
 794     int         size, newsize;
 795     int         limitSize;
 796
 797     moves = prevMoves;
 798     limitSize = table->keysZ;
 799
 800     y = cuddZddNextHigh(table, x);
 801     while (y <= xHigh) {
 802         size = cuddZddSwapInPlace(table, x, y);
 803         if (size == 0)
 804             goto cuddZddLinearDownOutOfMem;
 805         newsize = cuddZddLinearInPlace(table, x, y);
 806         if (newsize == 0)
 807             goto cuddZddLinearDownOutOfMem;
 808         move = (Move *) cuddDynamicAllocNode(table);
 809         if (move == NULL)
 810             goto cuddZddLinearDownOutOfMem;
 811         move->x = x;
 812         move->y = y;
 813         move->next = moves;
 814         moves = move;
 815         move->flags = CUDD_SWAP_MOVE;
 816         if (newsize > size) {
 817             /* Undo transformation. The transformation we apply is
 818             ** its own inverse. Hence, we just apply the transformation
 819             ** again.
 820             */
 821             newsize = cuddZddLinearInPlace(table,x,y);
 822             if (newsize == 0) goto cuddZddLinearDownOutOfMem;
 823             if (newsize != size) {
 824                 (void) fprintf(table->err,"Change in size after identity transformation! From %d to %d\n",size,newsize);
 825             }
 826         } else {
 827             size = newsize;
 828             move->flags = CUDD_LINEAR_TRANSFORM_MOVE;
 829         }
 830         move->size = size;
 831
 832         if ((double)size > (double)limitSize * table->maxGrowth)
 833             break;
 834         if (size < limitSize)
 835             limitSize = size;
 836
 837         x = y;
 838         y = cuddZddNextHigh(table, x);
 839     }
 840     return(moves);
 841
 842 cuddZddLinearDownOutOfMem:
 843     while (moves != NULL) {
 844         move = moves->next;
 845         cuddDeallocMove(table, moves);
 846         moves = move;
 847     }
 848     return((Move *) CUDD_OUT_OF_MEM);
 849
 850 } /* end of cuddZddLinearDown */
 851
 852
 853 /**Function********************************************************************
 854
 855   Synopsis    [Given a set of moves, returns the ZDD heap to the position
 856   giving the minimum size.]
 857
 858   Description [Given a set of moves, returns the ZDD heap to the
 859   position giving the minimum size. In case of ties, returns to the
 860   closest position giving the minimum size. Returns 1 in case of
 861   success; 0 otherwise.]
 862
 863   SideEffects [None]
 864
 865   SeeAlso     []
 866
 867 ******************************************************************************/
 868 static int
 869 cuddZddLinearBackward(
 870   DdManager * table,
 871   int  size,
 872   Move * moves)
 873 {
 874     Move        *move;
 875     int         res;
 876
 877     /* Find the minimum size among moves. */
 878     for (move = moves; move != NULL; move = move->next) {
 879         if (move->size < size) {
 880             size = move->size;
 881         }
 882     }
 883
 884     for (move = moves; move != NULL; move = move->next) {
 885         if (move->size == size) return(1);
 886         if (move->flags == CUDD_LINEAR_TRANSFORM_MOVE) {
 887             res = cuddZddLinearInPlace(table,(int)move->x,(int)move->y);
 888             if (!res) return(0);
 889         }
 890         res = cuddZddSwapInPlace(table, move->x, move->y);
 891         if (!res)
 892             return(0);
 893         if (move->flags == CUDD_INVERSE_TRANSFORM_MOVE) {
 894             res = cuddZddLinearInPlace(table,(int)move->x,(int)move->y);
 895             if (!res) return(0);
 896         }
 897     }
 898
 899     return(1);
 900
 901 } /* end of cuddZddLinearBackward */
 902
 903
 904 /**Function********************************************************************
 905
 906   Synopsis    [Given a set of moves, returns the ZDD heap to the order
 907   in effect before the moves.]
 908
 909   Description [Given a set of moves, returns the ZDD heap to the
 910   order in effect before the moves.  Returns 1 in case of success;
 911   0 otherwise.]
 912
 913   SideEffects [None]
 914
 915 ******************************************************************************/
 916 static Move*
 917 cuddZddUndoMoves(
 918   DdManager * table,
 919   Move * moves)
 920 {
 921     Move *invmoves = NULL;
 922     Move *move;
 923     Move *invmove;
 924     int size;
 925
 926     for (move = moves; move != NULL; move = move->next) {
 927         invmove = (Move *) cuddDynamicAllocNode(table);
 928         if (invmove == NULL) goto cuddZddUndoMovesOutOfMem;
 929         invmove->x = move->x;
 930         invmove->y = move->y;
 931         invmove->next = invmoves;
 932         invmoves = invmove;
 933         if (move->flags == CUDD_SWAP_MOVE) {
 934             invmove->flags = CUDD_SWAP_MOVE;
 935             size = cuddZddSwapInPlace(table,(int)move->x,(int)move->y);
 936             if (!size) goto cuddZddUndoMovesOutOfMem;
 937         } else if (move->flags == CUDD_LINEAR_TRANSFORM_MOVE) {
 938             invmove->flags = CUDD_INVERSE_TRANSFORM_MOVE;
 939             size = cuddZddLinearInPlace(table,(int)move->x,(int)move->y);
 940             if (!size) goto cuddZddUndoMovesOutOfMem;
 941             size = cuddZddSwapInPlace(table,(int)move->x,(int)move->y);
 942             if (!size) goto cuddZddUndoMovesOutOfMem;
 943         } else { /* must be CUDD_INVERSE_TRANSFORM_MOVE */
 944 #ifdef DD_DEBUG
 945             (void) fprintf(table->err,"Unforseen event in ddUndoMoves!\n");
 946 #endif
 947             invmove->flags = CUDD_LINEAR_TRANSFORM_MOVE;
 948             size = cuddZddSwapInPlace(table,(int)move->x,(int)move->y);
 949             if (!size) goto cuddZddUndoMovesOutOfMem;
 950             size = cuddZddLinearInPlace(table,(int)move->x,(int)move->y);
 951             if (!size) goto cuddZddUndoMovesOutOfMem;
 952         }
 953         invmove->size = size;
 954     }
 955
 956     return(invmoves);
 957
 958 cuddZddUndoMovesOutOfMem:
 959     while (invmoves != NULL) {
 960         move = invmoves->next;
 961         cuddDeallocMove(table, invmoves);
 962         invmoves = move;
 963     }
 964     return((Move *) CUDD_OUT_OF_MEM);
 965
 966 } /* end of cuddZddUndoMoves */
 967