distr/cudd/cuddZddReord.c

   1 /**CFile***********************************************************************
   2
   3   FileName    [cuddZddReord.c]
   4
   5   PackageName [cudd]
   6
   7   Synopsis    [Procedures for dynamic variable ordering of ZDDs.]
   8
   9   Description [External procedures included in this module:
  10                     <ul>
  11                     <li> Cudd_zddReduceHeap()
  12                     <li> Cudd_zddShuffleHeap()
  13                     </ul>
  14                Internal procedures included in this module:
  15                     <ul>
  16                     <li> cuddZddAlignToBdd()
  17                     <li> cuddZddNextHigh()
  18                     <li> cuddZddNextLow()
  19                     <li> cuddZddUniqueCompare()
  20                     <li> cuddZddSwapInPlace()
  21                     <li> cuddZddSwapping()
  22                     <li> cuddZddSifting()
  23                     </ul>
  24                Static procedures included in this module:
  25                     <ul>
  26                     <li> zddSwapAny()
  27                     <li> cuddZddSiftingAux()
  28                     <li> cuddZddSiftingUp()
  29                     <li> cuddZddSiftingDown()
  30                     <li> cuddZddSiftingBackward()
  31                     <li> zddReorderPreprocess()
  32                     <li> zddReorderPostprocess()
  33                     <li> zddShuffle()
  34                     <li> zddSiftUp()
  35                     </ul>
  36               ]
  37
  38   SeeAlso     []
  39
  40   Author      [Hyong-Kyoon Shin, In-Ho Moon]
  41
  42   Copyright   [Copyright (c) 1995-2004, Regents of the University of Colorado
  43
  44   All rights reserved.
  45
  46   Redistribution and use in source and binary forms, with or without
  47   modification, are permitted provided that the following conditions
  48   are met:
  49
  50   Redistributions of source code must retain the above copyright
  51   notice, this list of conditions and the following disclaimer.
  52
  53   Redistributions in binary form must reproduce the above copyright
  54   notice, this list of conditions and the following disclaimer in the
  55   documentation and/or other materials provided with the distribution.
  56
  57   Neither the name of the University of Colorado nor the names of its
  58   contributors may be used to endorse or promote products derived from
  59   this software without specific prior written permission.
  60
  61   THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS
  62   "AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT
  63   LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS
  64   FOR A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE
  65   COPYRIGHT OWNER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT,
  66   INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING,
  67   BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES;
  68   LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER
  69   CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT
  70   LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN
  71   ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE
  72   POSSIBILITY OF SUCH DAMAGE.]
  73
  74 ******************************************************************************/
  75
  76 #include "util.h"
  77 #include "cuddInt.h"
  78
  79 /*---------------------------------------------------------------------------*/
  80 /* Constant declarations                                                     */
  81 /*---------------------------------------------------------------------------*/
  82
  83 #define DD_MAX_SUBTABLE_SPARSITY 8
  84 #define DD_SHRINK_FACTOR 2
  85
  86 /*---------------------------------------------------------------------------*/
  87 /* Stucture declarations                                                     */
  88 /*---------------------------------------------------------------------------*/
  89
  90
  91 /*---------------------------------------------------------------------------*/
  92 /* Type declarations                                                         */
  93 /*---------------------------------------------------------------------------*/
  94
  95
  96 /*---------------------------------------------------------------------------*/
  97 /* Variable declarations                                                     */
  98 /*---------------------------------------------------------------------------*/
  99
 100 #ifndef lint
 101 static char rcsid[] DD_UNUSED = "$Id: cuddZddReord.c,v 1.47 2004/08/13 18:04:53 fabio Exp $";
 102 #endif
 103
 104 int     *zdd_entry;
 105
 106 int     zddTotalNumberSwapping;
 107
 108 static  DdNode  *empty;
 109
 110
 111 /*---------------------------------------------------------------------------*/
 112 /* Macro declarations                                                        */
 113 /*---------------------------------------------------------------------------*/
 114
 115
 116 /**AutomaticStart*************************************************************/
 117
 118 /*---------------------------------------------------------------------------*/
 119 /* Static function prototypes                                                */
 120 /*---------------------------------------------------------------------------*/
 121
 122 static Move * zddSwapAny (DdManager *table, int x, int y);
 123 static int cuddZddSiftingAux (DdManager *table, int x, int x_low, int x_high);
 124 static Move * cuddZddSiftingUp (DdManager *table, int x, int x_low, int initial_size);
 125 static Move * cuddZddSiftingDown (DdManager *table, int x, int x_high, int initial_size);
 126 static int cuddZddSiftingBackward (DdManager *table, Move *moves, int size);
 127 static void zddReorderPreprocess (DdManager *table);
 128 static int zddReorderPostprocess (DdManager *table);
 129 static int zddShuffle (DdManager *table, int *permutation);
 130 static int zddSiftUp (DdManager *table, int x, int xLow);
 131 static void zddFixTree (DdManager *table, MtrNode *treenode);
 132
 133 /**AutomaticEnd***************************************************************/
 134
 135
 136 /*---------------------------------------------------------------------------*/
 137 /* Definition of exported functions                                          */
 138 /*---------------------------------------------------------------------------*/
 139
 140
 141 /**Function********************************************************************
 142
 143   Synopsis    [Main dynamic reordering routine for ZDDs.]
 144
 145   Description [Main dynamic reordering routine for ZDDs.
 146   Calls one of the possible reordering procedures:
 147   <ul>
 148   <li>Swapping
 149   <li>Sifting
 150   <li>Symmetric Sifting
 151   </ul>
 152
 153   For sifting and symmetric sifting it is possible to request reordering
 154   to convergence.<p>
 155
 156   The core of all methods is the reordering procedure
 157   cuddZddSwapInPlace() which swaps two adjacent variables.
 158   Returns 1 in case of success; 0 otherwise. In the case of symmetric
 159   sifting (with and without convergence) returns 1 plus the number of
 160   symmetric variables, in case of success.]
 161
 162   SideEffects [Changes the variable order for all ZDDs and clears
 163   the cache.]
 164
 165 ******************************************************************************/
 166 int
 167 Cudd_zddReduceHeap(
 168   DdManager * table /* DD manager */,
 169   Cudd_ReorderingType heuristic /* method used for reordering */,
 170   int minsize /* bound below which no reordering occurs */)
 171 {
 172     DdHook       *hook;
 173     int          result;
 174     unsigned int nextDyn;
 175 #ifdef DD_STATS
 176     unsigned int initialSize;
 177     unsigned int finalSize;
 178 #endif
 179     long         localTime;
 180
 181     /* Don't reorder if there are too many dead nodes. */
 182     if (table->keysZ - table->deadZ < (unsigned) minsize)
 183         return(1);
 184
 185     if (heuristic == CUDD_REORDER_SAME) {
 186         heuristic = table->autoMethodZ;
 187     }
 188     if (heuristic == CUDD_REORDER_NONE) {
 189         return(1);
 190     }
 191
 192     /* This call to Cudd_zddReduceHeap does initiate reordering. Therefore
 193     ** we count it.
 194     */
 195     table->reorderings++;
 196     empty = table->zero;
 197
 198     localTime = util_cpu_time();
 199
 200     /* Run the hook functions. */
 201     hook = table->preReorderingHook;
 202     while (hook != NULL) {
 203         int res = (hook->f)(table, "ZDD", (void *)heuristic);
 204         if (res == 0) return(0);
 205         hook = hook->next;
 206     }
 207
 208     /* Clear the cache and collect garbage. */
 209     zddReorderPreprocess(table);
 210     zddTotalNumberSwapping = 0;
 211
 212 #ifdef DD_STATS
 213     initialSize = table->keysZ;
 214
 215     switch(heuristic) {
 216     case CUDD_REORDER_RANDOM:
 217     case CUDD_REORDER_RANDOM_PIVOT:
 218         (void) fprintf(table->out,"#:I_RANDOM  ");
 219         break;
 220     case CUDD_REORDER_SIFT:
 221     case CUDD_REORDER_SIFT_CONVERGE:
 222     case CUDD_REORDER_SYMM_SIFT:
 223     case CUDD_REORDER_SYMM_SIFT_CONV:
 224         (void) fprintf(table->out,"#:I_SIFTING ");
 225         break;
 226     case CUDD_REORDER_LINEAR:
 227     case CUDD_REORDER_LINEAR_CONVERGE:
 228         (void) fprintf(table->out,"#:I_LINSIFT ");
 229         break;
 230     default:
 231         (void) fprintf(table->err,"Unsupported ZDD reordering method\n");
 232         return(0);
 233     }
 234     (void) fprintf(table->out,"%8d: initial size",initialSize);
 235 #endif
 236
 237     result = cuddZddTreeSifting(table,heuristic);
 238
 239 #ifdef DD_STATS
 240     (void) fprintf(table->out,"\n");
 241     finalSize = table->keysZ;
 242     (void) fprintf(table->out,"#:F_REORDER %8d: final size\n",finalSize);
 243     (void) fprintf(table->out,"#:T_REORDER %8g: total time (sec)\n",
 244                    ((double)(util_cpu_time() - localTime)/1000.0));
 245     (void) fprintf(table->out,"#:N_REORDER %8d: total swaps\n",
 246                    zddTotalNumberSwapping);
 247 #endif
 248
 249     if (result == 0)
 250         return(0);
 251
 252     if (!zddReorderPostprocess(table))
 253         return(0);
 254
 255     if (table->realignZ) {
 256         if (!cuddBddAlignToZdd(table))
 257             return(0);
 258     }
 259
 260     nextDyn = table->keysZ * DD_DYN_RATIO;
 261     if (table->reorderings < 20 || nextDyn > table->nextDyn)
 262         table->nextDyn = nextDyn;
 263     else
 264         table->nextDyn += 20;
 265
 266     table->reordered = 1;
 267
 268     /* Run hook functions. */
 269     hook = table->postReorderingHook;
 270     while (hook != NULL) {
 271         int res = (hook->f)(table, "ZDD", (void *)localTime);
 272         if (res == 0) return(0);
 273         hook = hook->next;
 274     }
 275     /* Update cumulative reordering time. */
 276     table->reordTime += util_cpu_time() - localTime;
 277
 278     return(result);
 279
 280 } /* end of Cudd_zddReduceHeap */
 281
 282
 283 /**Function********************************************************************
 284
 285   Synopsis    [Reorders ZDD variables according to given permutation.]
 286
 287   Description [Reorders ZDD variables according to given permutation.
 288   The i-th entry of the permutation array contains the index of the variable
 289   that should be brought to the i-th level.  The size of the array should be
 290   equal or greater to the number of variables currently in use.
 291   Returns 1 in case of success; 0 otherwise.]
 292
 293   SideEffects [Changes the ZDD variable order for all diagrams and clears
 294   the cache.]
 295
 296   SeeAlso [Cudd_zddReduceHeap]
 297
 298 ******************************************************************************/
 299 int
 300 Cudd_zddShuffleHeap(
 301   DdManager * table /* DD manager */,
 302   int * permutation /* required variable permutation */)
 303 {
 304
 305     int result;
 306
 307     empty = table->zero;
 308     zddReorderPreprocess(table);
 309
 310     result = zddShuffle(table,permutation);
 311
 312     if (!zddReorderPostprocess(table)) return(0);
 313
 314     return(result);
 315
 316 } /* end of Cudd_zddShuffleHeap */
 317
 318
 319 /*---------------------------------------------------------------------------*/
 320 /* Definition of internal functions                                          */
 321 /*---------------------------------------------------------------------------*/
 322
 323
 324 /**Function********************************************************************
 325
 326   Synopsis    [Reorders ZDD variables according to the order of the BDD
 327   variables.]
 328
 329   Description [Reorders ZDD variables according to the order of the
 330   BDD variables. This function can be called at the end of BDD
 331   reordering to insure that the order of the ZDD variables is
 332   consistent with the order of the BDD variables. The number of ZDD
 333   variables must be a multiple of the number of BDD variables. Let
 334   <code>M</code> be the ratio of the two numbers. cuddZddAlignToBdd
 335   then considers the ZDD variables from <code>M*i</code> to
 336   <code>(M+1)*i-1</code> as corresponding to BDD variable
 337   <code>i</code>.  This function should be normally called from
 338   Cudd_ReduceHeap, which clears the cache.  Returns 1 in case of
 339   success; 0 otherwise.]
 340
 341   SideEffects [Changes the ZDD variable order for all diagrams and performs
 342   garbage collection of the ZDD unique table.]
 343
 344   SeeAlso [Cudd_zddShuffleHeap Cudd_ReduceHeap]
 345
 346 ******************************************************************************/
 347 int
 348 cuddZddAlignToBdd(
 349   DdManager * table /* DD manager */)
 350 {
 351     int *invpermZ;              /* permutation array */
 352     int M;                      /* ratio of ZDD variables to BDD variables */
 353     int i,j;                    /* loop indices */
 354     int result;                 /* return value */
 355
 356     /* We assume that a ratio of 0 is OK. */
 357     if (table->sizeZ == 0)
 358         return(1);
 359
 360     empty = table->zero;
 361     M = table->sizeZ / table->size;
 362     /* Check whether the number of ZDD variables is a multiple of the
 363     ** number of BDD variables.
 364     */
 365     if (M * table->size != table->sizeZ)
 366         return(0);
 367     /* Create and initialize the inverse permutation array. */
 368     invpermZ = ALLOC(int,table->sizeZ);
 369     if (invpermZ == NULL) {
 370         table->errorCode = CUDD_MEMORY_OUT;
 371         return(0);
 372     }
 373     for (i = 0; i < table->size; i++) {
 374         int index = table->invperm[i];
 375         int indexZ = index * M;
 376         int levelZ = table->permZ[indexZ];
 377         levelZ = (levelZ / M) * M;
 378         for (j = 0; j < M; j++) {
 379             invpermZ[M * i + j] = table->invpermZ[levelZ + j];
 380         }
 381     }
 382     /* Eliminate dead nodes. Do not scan the cache again, because we
 383     ** assume that Cudd_ReduceHeap has already cleared it.
 384     */
 385     cuddGarbageCollect(table,0);
 386
 387     result = zddShuffle(table, invpermZ);
 388     FREE(invpermZ);
 389     /* Fix the ZDD variable group tree. */
 390     zddFixTree(table,table->treeZ);
 391     return(result);
 392
 393 } /* end of cuddZddAlignToBdd */
 394
 395
 396 /**Function********************************************************************
 397
 398   Synopsis    [Finds the next subtable with a larger index.]
 399
 400   Description [Finds the next subtable with a larger index. Returns the
 401   index.]
 402
 403   SideEffects [None]
 404
 405   SeeAlso     []
 406
 407 ******************************************************************************/
 408 int
 409 cuddZddNextHigh(
 410   DdManager * table,
 411   int  x)
 412 {
 413     return(x + 1);
 414
 415 } /* end of cuddZddNextHigh */
 416
 417
 418 /**Function********************************************************************
 419
 420   Synopsis    [Finds the next subtable with a smaller index.]
 421
 422   Description [Finds the next subtable with a smaller index. Returns the
 423   index.]
 424
 425   SideEffects [None]
 426
 427   SeeAlso     []
 428
 429 ******************************************************************************/
 430 int
 431 cuddZddNextLow(
 432   DdManager * table,
 433   int  x)
 434 {
 435     return(x - 1);
 436
 437 } /* end of cuddZddNextLow */
 438
 439
 440 /**Function********************************************************************
 441
 442   Synopsis [Comparison function used by qsort.]
 443
 444   Description [Comparison function used by qsort to order the
 445   variables according to the number of keys in the subtables.
 446   Returns the difference in number of keys between the two
 447   variables being compared.]
 448
 449   SideEffects [None]
 450
 451   SeeAlso     []
 452
 453 ******************************************************************************/
 454 int
 455 cuddZddUniqueCompare(
 456   int * ptr_x,
 457   int * ptr_y)
 458 {
 459     return(zdd_entry[*ptr_y] - zdd_entry[*ptr_x]);
 460
 461 } /* end of cuddZddUniqueCompare */
 462
 463
 464 /**Function********************************************************************
 465
 466   Synopsis    [Swaps two adjacent variables.]
 467
 468   Description [Swaps two adjacent variables. It assumes that no dead
 469   nodes are present on entry to this procedure.  The procedure then
 470   guarantees that no dead nodes will be present when it terminates.
 471   cuddZddSwapInPlace assumes that x &lt; y.  Returns the number of keys in
 472   the table if successful; 0 otherwise.]
 473
 474   SideEffects [None]
 475
 476   SeeAlso     []
 477
 478 ******************************************************************************/
 479 int
 480 cuddZddSwapInPlace(
 481   DdManager * table,
 482   int  x,
 483   int  y)
 484 {
 485     DdNodePtr   *xlist, *ylist;
 486     int         xindex, yindex;
 487     int         xslots, yslots;
 488     int         xshift, yshift;
 489     int         oldxkeys, oldykeys;
 490     int         newxkeys, newykeys;
 491     int         i;
 492     int         posn;
 493     DdNode      *f, *f1, *f0, *f11, *f10, *f01, *f00;
 494     DdNode      *newf1, *newf0, *next;
 495     DdNodePtr   g, *lastP, *previousP;
 496
 497 #ifdef DD_DEBUG
 498     assert(x < y);
 499     assert(cuddZddNextHigh(table,x) == y);
 500     assert(table->subtableZ[x].keys != 0);
 501     assert(table->subtableZ[y].keys != 0);
 502     assert(table->subtableZ[x].dead == 0);
 503     assert(table->subtableZ[y].dead == 0);
 504 #endif
 505
 506     zddTotalNumberSwapping++;
 507
 508     /* Get parameters of x subtable. */
 509     xindex   = table->invpermZ[x];
 510     xlist    = table->subtableZ[x].nodelist;
 511     oldxkeys = table->subtableZ[x].keys;
 512     xslots   = table->subtableZ[x].slots;
 513     xshift   = table->subtableZ[x].shift;
 514     newxkeys = 0;
 515
 516     yindex   = table->invpermZ[y];
 517     ylist    = table->subtableZ[y].nodelist;
 518     oldykeys = table->subtableZ[y].keys;
 519     yslots   = table->subtableZ[y].slots;
 520     yshift   = table->subtableZ[y].shift;
 521     newykeys = oldykeys;
 522
 523     /* The nodes in the x layer that don't depend on y directly
 524     ** will stay there; the others are put in a chain.
 525     ** The chain is handled as a FIFO; g points to the beginning and
 526     ** last points to the end.
 527     */
 528
 529     g = NULL;
 530     lastP = &g;
 531     for (i = 0; i < xslots; i++) {
 532         previousP = &(xlist[i]);
 533         f = *previousP;
 534         while (f != NULL) {
 535             next = f->next;
 536             f1 = cuddT(f); f0 = cuddE(f);
 537             if ((f1->index != (DdHalfWord) yindex) &&
 538                 (f0->index != (DdHalfWord) yindex)) { /* stays */
 539                 newxkeys++;
 540                 *previousP = f;
 541                 previousP = &(f->next);
 542             } else {
 543                 f->index = yindex;
 544                 *lastP = f;
 545                 lastP = &(f->next);
 546             }
 547             f = next;
 548         } /* while there are elements in the collision chain */
 549         *previousP = NULL;
 550     } /* for each slot of the x subtable */
 551     *lastP = NULL;
 552
 553
 554 #ifdef DD_COUNT
 555     table->swapSteps += oldxkeys - newxkeys;
 556 #endif
 557     /* Take care of the x nodes that must be re-expressed.
 558     ** They form a linked list pointed by g. Their index has been
 559     ** changed to yindex already.
 560     */
 561     f = g;
 562     while (f != NULL) {
 563         next = f->next;
 564         /* Find f1, f0, f11, f10, f01, f00. */
 565         f1 = cuddT(f);
 566         if ((int) f1->index == yindex) {
 567             f11 = cuddT(f1); f10 = cuddE(f1);
 568         } else {
 569             f11 = empty; f10 = f1;
 570         }
 571         f0 = cuddE(f);
 572         if ((int) f0->index == yindex) {
 573             f01 = cuddT(f0); f00 = cuddE(f0);
 574         } else {
 575             f01 = empty; f00 = f0;
 576         }
 577
 578         /* Decrease ref count of f1. */
 579         cuddSatDec(f1->ref);
 580         /* Create the new T child. */
 581         if (f11 == empty) {
 582             if (f01 != empty) {
 583                 newf1 = f01;
 584                 cuddSatInc(newf1->ref);
 585             }
 586             /* else case was already handled when finding nodes
 587             ** with both children below level y
 588             */
 589         } else {
 590             /* Check xlist for triple (xindex, f11, f01). */
 591             posn = ddHash(f11, f01, xshift);
 592             /* For each element newf1 in collision list xlist[posn]. */
 593             newf1 = xlist[posn];
 594             while (newf1 != NULL) {
 595                 if (cuddT(newf1) == f11 && cuddE(newf1) == f01) {
 596                     cuddSatInc(newf1->ref);
 597                     break; /* match */
 598                 }
 599                 newf1 = newf1->next;
 600             } /* while newf1 */
 601             if (newf1 == NULL) {        /* no match */
 602                 newf1 = cuddDynamicAllocNode(table);
 603                 if (newf1 == NULL)
 604                     goto zddSwapOutOfMem;
 605                 newf1->index = xindex; newf1->ref = 1;
 606                 cuddT(newf1) = f11;
 607                 cuddE(newf1) = f01;
 608                 /* Insert newf1 in the collision list xlist[pos];
 609                 ** increase the ref counts of f11 and f01
 610                 */
 611                 newxkeys++;
 612                 newf1->next = xlist[posn];
 613                 xlist[posn] = newf1;
 614                 cuddSatInc(f11->ref);
 615                 cuddSatInc(f01->ref);
 616             }
 617         }
 618         cuddT(f) = newf1;
 619
 620         /* Do the same for f0. */
 621         /* Decrease ref count of f0. */
 622         cuddSatDec(f0->ref);
 623         /* Create the new E child. */
 624         if (f10 == empty) {
 625             newf0 = f00;
 626             cuddSatInc(newf0->ref);
 627         } else {
 628             /* Check xlist for triple (xindex, f10, f00). */
 629             posn = ddHash(f10, f00, xshift);
 630             /* For each element newf0 in collision list xlist[posn]. */
 631             newf0 = xlist[posn];
 632             while (newf0 != NULL) {
 633                 if (cuddT(newf0) == f10 && cuddE(newf0) == f00) {
 634                     cuddSatInc(newf0->ref);
 635                     break; /* match */
 636                 }
 637                 newf0 = newf0->next;
 638             } /* while newf0 */
 639             if (newf0 == NULL) {        /* no match */
 640                 newf0 = cuddDynamicAllocNode(table);
 641                 if (newf0 == NULL)
 642                     goto zddSwapOutOfMem;
 643                 newf0->index = xindex; newf0->ref = 1;
 644                 cuddT(newf0) = f10; cuddE(newf0) = f00;
 645                 /* Insert newf0 in the collision list xlist[posn];
 646                 ** increase the ref counts of f10 and f00.
 647                 */
 648                 newxkeys++;
 649                 newf0->next = xlist[posn];
 650                 xlist[posn] = newf0;
 651                 cuddSatInc(f10->ref);
 652                 cuddSatInc(f00->ref);
 653             }
 654         }
 655         cuddE(f) = newf0;
 656
 657         /* Insert the modified f in ylist.
 658         ** The modified f does not already exists in ylist.
 659         ** (Because of the uniqueness of the cofactors.)
 660         */
 661         posn = ddHash(newf1, newf0, yshift);
 662         newykeys++;
 663         f->next = ylist[posn];
 664         ylist[posn] = f;
 665         f = next;
 666     } /* while f != NULL */
 667
 668     /* GC the y layer. */
 669
 670     /* For each node f in ylist. */
 671     for (i = 0; i < yslots; i++) {
 672         previousP = &(ylist[i]);
 673         f = *previousP;
 674         while (f != NULL) {
 675             next = f->next;
 676             if (f->ref == 0) {
 677                 cuddSatDec(cuddT(f)->ref);
 678                 cuddSatDec(cuddE(f)->ref);
 679                 cuddDeallocNode(table, f);
 680                 newykeys--;
 681             } else {
 682                 *previousP = f;
 683                 previousP = &(f->next);
 684             }
 685             f = next;
 686         } /* while f */
 687         *previousP = NULL;
 688     } /* for i */
 689
 690     /* Set the appropriate fields in table. */
 691     table->subtableZ[x].nodelist = ylist;
 692     table->subtableZ[x].slots    = yslots;
 693     table->subtableZ[x].shift    = yshift;
 694     table->subtableZ[x].keys     = newykeys;
 695     table->subtableZ[x].maxKeys  = yslots * DD_MAX_SUBTABLE_DENSITY;
 696
 697     table->subtableZ[y].nodelist = xlist;
 698     table->subtableZ[y].slots    = xslots;
 699     table->subtableZ[y].shift    = xshift;
 700     table->subtableZ[y].keys     = newxkeys;
 701     table->subtableZ[y].maxKeys  = xslots * DD_MAX_SUBTABLE_DENSITY;
 702
 703     table->permZ[xindex] = y; table->permZ[yindex] = x;
 704     table->invpermZ[x] = yindex; table->invpermZ[y] = xindex;
 705
 706     table->keysZ += newxkeys + newykeys - oldxkeys - oldykeys;
 707
 708     /* Update univ section; univ[x] remains the same. */
 709     table->univ[y] = cuddT(table->univ[x]);
 710
 711     return (table->keysZ);
 712
 713 zddSwapOutOfMem:
 714     (void) fprintf(table->err, "Error: cuddZddSwapInPlace out of memory\n");
 715
 716     return (0);
 717
 718 } /* end of cuddZddSwapInPlace */
 719
 720
 721 /**Function********************************************************************
 722
 723   Synopsis    [Reorders variables by a sequence of (non-adjacent) swaps.]
 724
 725   Description [Implementation of Plessier's algorithm that reorders
 726   variables by a sequence of (non-adjacent) swaps.
 727     <ol>
 728     <li> Select two variables (RANDOM or HEURISTIC).
 729     <li> Permute these variables.
 730     <li> If the nodes have decreased accept the permutation.
 731     <li> Otherwise reconstruct the original heap.
 732     <li> Loop.
 733     </ol>
 734   Returns 1 in case of success; 0 otherwise.]
 735
 736   SideEffects [None]
 737
 738   SeeAlso     []
 739
 740 ******************************************************************************/
 741 int
 742 cuddZddSwapping(
 743   DdManager * table,
 744   int lower,
 745   int upper,
 746   Cudd_ReorderingType heuristic)
 747 {
 748     int i, j;
 749     int max, keys;
 750     int nvars;
 751     int x, y;
 752     int iterate;
 753     int previousSize;
 754     Move *moves, *move;
 755     int pivot;
 756     int modulo;
 757     int result;
 758
 759 #ifdef DD_DEBUG
 760     /* Sanity check */
 761     assert(lower >= 0 && upper < table->sizeZ && lower <= upper);
 762 #endif
 763
 764     nvars = upper - lower + 1;
 765     iterate = nvars;
 766
 767     for (i = 0; i < iterate; i++) {
 768         if (heuristic == CUDD_REORDER_RANDOM_PIVOT) {
 769             /* Find pivot <= id with maximum keys. */
 770             for (max = -1, j = lower; j <= upper; j++) {
 771                 if ((keys = table->subtableZ[j].keys) > max) {
 772                     max = keys;
 773                     pivot = j;
 774                 }
 775             }
 776
 777             modulo = upper - pivot;
 778             if (modulo == 0) {
 779                 y = pivot;      /* y = nvars-1 */
 780             } else {
 781                 /* y = random # from {pivot+1 .. nvars-1} */
 782                 y = pivot + 1 + (int) (Cudd_Random() % modulo);
 783             }
 784
 785             modulo = pivot - lower - 1;
 786             if (modulo < 1) {   /* if pivot = 1 or 0 */
 787                 x = lower;
 788             } else {
 789                 do { /* x = random # from {0 .. pivot-2} */
 790                     x = (int) Cudd_Random() % modulo;
 791                 } while (x == y);
 792                   /* Is this condition really needed, since x and y
 793                      are in regions separated by pivot? */
 794             }
 795         } else {
 796             x = (int) (Cudd_Random() % nvars) + lower;
 797             do {
 798                 y = (int) (Cudd_Random() % nvars) + lower;
 799             } while (x == y);
 800         }
 801
 802         previousSize = table->keysZ;
 803         moves = zddSwapAny(table, x, y);
 804         if (moves == NULL)
 805             goto cuddZddSwappingOutOfMem;
 806
 807         result = cuddZddSiftingBackward(table, moves, previousSize);
 808         if (!result)
 809             goto cuddZddSwappingOutOfMem;
 810
 811         while (moves != NULL) {
 812             move = moves->next;
 813             cuddDeallocMove(table, moves);
 814             moves = move;
 815         }
 816 #ifdef DD_STATS
 817         if (table->keysZ < (unsigned) previousSize) {
 818             (void) fprintf(table->out,"-");
 819         } else if (table->keysZ > (unsigned) previousSize) {
 820             (void) fprintf(table->out,"+");     /* should never happen */
 821         } else {
 822             (void) fprintf(table->out,"=");
 823         }
 824         fflush(table->out);
 825 #endif
 826     }
 827
 828     return(1);
 829
 830 cuddZddSwappingOutOfMem:
 831     while (moves != NULL) {
 832         move = moves->next;
 833         cuddDeallocMove(table, moves);
 834         moves = move;
 835     }
 836     return(0);
 837
 838 } /* end of cuddZddSwapping */
 839
 840
 841 /**Function********************************************************************
 842
 843   Synopsis    [Implementation of Rudell's sifting algorithm.]
 844
 845   Description [Implementation of Rudell's sifting algorithm.
 846   Assumes that no dead nodes are present.
 847     <ol>
 848     <li> Order all the variables according to the number of entries
 849     in each unique table.
 850     <li> Sift the variable up and down, remembering each time the
 851     total size of the DD heap.
 852     <li> Select the best permutation.
 853     <li> Repeat 3 and 4 for all variables.
 854     </ol>
 855   Returns 1 if successful; 0 otherwise.]
 856
 857   SideEffects [None]
 858
 859   SeeAlso     []
 860
 861 ******************************************************************************/
 862 int
 863 cuddZddSifting(
 864   DdManager * table,
 865   int  lower,
 866   int  upper)
 867 {
 868     int i;
 869     int *var;
 870     int size;
 871     int x;
 872     int result;
 873 #ifdef DD_STATS
 874     int previousSize;
 875 #endif
 876
 877     size = table->sizeZ;
 878
 879     /* Find order in which to sift variables. */
 880     var = NULL;
 881     zdd_entry = ALLOC(int, size);
 882     if (zdd_entry == NULL) {
 883         table->errorCode = CUDD_MEMORY_OUT;
 884         goto cuddZddSiftingOutOfMem;
 885     }
 886     var = ALLOC(int, size);
 887     if (var == NULL) {
 888         table->errorCode = CUDD_MEMORY_OUT;
 889         goto cuddZddSiftingOutOfMem;
 890     }
 891
 892     for (i = 0; i < size; i++) {
 893         x = table->permZ[i];
 894         zdd_entry[i] = table->subtableZ[x].keys;
 895         var[i] = i;
 896     }
 897
 898     qsort((void *)var, size, sizeof(int), (DD_QSFP)cuddZddUniqueCompare);
 899
 900     /* Now sift. */
 901     for (i = 0; i < ddMin(table->siftMaxVar, size); i++) {
 902         if (zddTotalNumberSwapping >= table->siftMaxSwap)
 903             break;
 904         x = table->permZ[var[i]];
 905         if (x < lower || x > upper) continue;
 906 #ifdef DD_STATS
 907         previousSize = table->keysZ;
 908 #endif
 909         result = cuddZddSiftingAux(table, x, lower, upper);
 910         if (!result)
 911             goto cuddZddSiftingOutOfMem;
 912 #ifdef DD_STATS
 913         if (table->keysZ < (unsigned) previousSize) {
 914             (void) fprintf(table->out,"-");
 915         } else if (table->keysZ > (unsigned) previousSize) {
 916             (void) fprintf(table->out,"+");     /* should never happen */
 917             (void) fprintf(table->out,"\nSize increased from %d to %d while sifting variable %d\n", previousSize, table->keysZ , var[i]);
 918         } else {
 919             (void) fprintf(table->out,"=");
 920         }
 921         fflush(table->out);
 922 #endif
 923     }
 924
 925     FREE(var);
 926     FREE(zdd_entry);
 927
 928     return(1);
 929
 930 cuddZddSiftingOutOfMem:
 931
 932     if (zdd_entry != NULL) FREE(zdd_entry);
 933     if (var != NULL) FREE(var);
 934
 935     return(0);
 936
 937 } /* end of cuddZddSifting */
 938
 939
 940 /*---------------------------------------------------------------------------*/
 941 /* Definition of static functions                                            */
 942 /*---------------------------------------------------------------------------*/
 943
 944
 945 /**Function********************************************************************
 946
 947   Synopsis    [Swaps any two variables.]
 948
 949   Description [Swaps any two variables. Returns the set of moves.]
 950
 951   SideEffects [None]
 952
 953   SeeAlso     []
 954
 955 ******************************************************************************/
 956 static Move *
 957 zddSwapAny(
 958   DdManager * table,
 959   int  x,
 960   int  y)
 961 {
 962     Move        *move, *moves;
 963     int         tmp, size;
 964     int         x_ref, y_ref;
 965     int         x_next, y_next;
 966     int         limit_size;
 967
 968     if (x > y) {        /* make x precede y */
 969         tmp = x; x = y; y = tmp;
 970     }
 971
 972     x_ref = x; y_ref = y;
 973
 974     x_next = cuddZddNextHigh(table, x);
 975     y_next = cuddZddNextLow(table, y);
 976     moves = NULL;
 977     limit_size = table->keysZ;
 978
 979     for (;;) {
 980         if (x_next == y_next) { /* x < x_next = y_next < y */
 981             size = cuddZddSwapInPlace(table, x, x_next);
 982             if (size == 0)
 983                 goto zddSwapAnyOutOfMem;
 984             move = (Move *) cuddDynamicAllocNode(table);
 985             if (move == NULL)
 986                 goto zddSwapAnyOutOfMem;
 987             move->x = x;
 988             move->y = x_next;
 989             move->size = size;
 990             move->next = moves;
 991             moves = move;
 992
 993             size = cuddZddSwapInPlace(table, y_next, y);
 994             if (size == 0)
 995                 goto zddSwapAnyOutOfMem;
 996             move = (Move *)cuddDynamicAllocNode(table);
 997             if (move == NULL)
 998                 goto zddSwapAnyOutOfMem;
 999             move->x = y_next;
1000             move->y = y;
1001             move->size = size;
1002             move->next = moves;
1003             moves = move;
1004
1005             size = cuddZddSwapInPlace(table, x, x_next);
1006             if (size == 0)
1007                 goto zddSwapAnyOutOfMem;
1008             move = (Move *)cuddDynamicAllocNode(table);
1009             if (move == NULL)
1010                 goto zddSwapAnyOutOfMem;
1011             move->x = x;
1012             move->y = x_next;
1013             move->size = size;
1014             move->next = moves;
1015             moves = move;
1016
1017             tmp = x; x = y; y = tmp;
1018
1019         } else if (x == y_next) { /* x = y_next < y = x_next */
1020             size = cuddZddSwapInPlace(table, x, x_next);
1021             if (size == 0)
1022                 goto zddSwapAnyOutOfMem;
1023             move = (Move *)cuddDynamicAllocNode(table);
1024             if (move == NULL)
1025                 goto zddSwapAnyOutOfMem;
1026             move->x = x;
1027             move->y = x_next;
1028             move->size = size;
1029             move->next = moves;
1030             moves = move;
1031
1032             tmp = x; x = y;  y = tmp;
1033         } else {
1034             size = cuddZddSwapInPlace(table, x, x_next);
1035             if (size == 0)
1036                 goto zddSwapAnyOutOfMem;
1037             move = (Move *)cuddDynamicAllocNode(table);
1038             if (move == NULL)
1039                 goto zddSwapAnyOutOfMem;
1040             move->x = x;
1041             move->y = x_next;
1042             move->size = size;
1043             move->next = moves;
1044             moves = move;
1045
1046             size = cuddZddSwapInPlace(table, y_next, y);
1047             if (size == 0)
1048                 goto zddSwapAnyOutOfMem;
1049             move = (Move *)cuddDynamicAllocNode(table);
1050             if (move == NULL)
1051                 goto zddSwapAnyOutOfMem;
1052             move->x = y_next;
1053             move->y = y;
1054             move->size = size;
1055             move->next = moves;
1056             moves = move;
1057
1058             x = x_next; y = y_next;
1059         }
1060
1061         x_next = cuddZddNextHigh(table, x);
1062         y_next = cuddZddNextLow(table, y);
1063         if (x_next > y_ref)
1064             break;      /* if x == y_ref */
1065
1066         if ((double) size > table->maxGrowth * (double) limit_size)
1067             break;
1068         if (size < limit_size)
1069             limit_size = size;
1070     }
1071     if (y_next >= x_ref) {
1072         size = cuddZddSwapInPlace(table, y_next, y);
1073         if (size == 0)
1074             goto zddSwapAnyOutOfMem;
1075         move = (Move *)cuddDynamicAllocNode(table);
1076         if (move == NULL)
1077             goto zddSwapAnyOutOfMem;
1078         move->x = y_next;
1079         move->y = y;
1080         move->size = size;
1081         move->next = moves;
1082         moves = move;
1083     }
1084
1085     return(moves);
1086
1087 zddSwapAnyOutOfMem:
1088     while (moves != NULL) {
1089         move = moves->next;
1090         cuddDeallocMove(table, moves);
1091         moves = move;
1092     }
1093     return(NULL);
1094
1095 } /* end of zddSwapAny */
1096
1097
1098 /**Function********************************************************************
1099
1100   Synopsis    [Given xLow <= x <= xHigh moves x up and down between the
1101   boundaries.]
1102
1103   Description [Given xLow <= x <= xHigh moves x up and down between the
1104   boundaries. Finds the best position and does the required changes.
1105   Returns 1 if successful; 0 otherwise.]
1106
1107   SideEffects [None]
1108
1109   SeeAlso     []
1110
1111 ******************************************************************************/
1112 static int
1113 cuddZddSiftingAux(
1114   DdManager * table,
1115   int  x,
1116   int  x_low,
1117   int  x_high)
1118 {
1119     Move        *move;
1120     Move        *moveUp;        /* list of up move */
1121     Move        *moveDown;      /* list of down move */
1122
1123     int         initial_size;
1124     int         result;
1125
1126     initial_size = table->keysZ;
1127
1128 #ifdef DD_DEBUG
1129     assert(table->subtableZ[x].keys > 0);
1130 #endif
1131
1132     moveDown = NULL;
1133     moveUp = NULL;
1134
1135     if (x == x_low) {
1136         moveDown = cuddZddSiftingDown(table, x, x_high, initial_size);
1137         /* after that point x --> x_high */
1138         if (moveDown == NULL)
1139             goto cuddZddSiftingAuxOutOfMem;
1140         result = cuddZddSiftingBackward(table, moveDown,
1141             initial_size);
1142         /* move backward and stop at best position */
1143         if (!result)
1144             goto cuddZddSiftingAuxOutOfMem;
1145
1146     }
1147     else if (x == x_high) {
1148         moveUp = cuddZddSiftingUp(table, x, x_low, initial_size);
1149         /* after that point x --> x_low */
1150         if (moveUp == NULL)
1151             goto cuddZddSiftingAuxOutOfMem;
1152         result = cuddZddSiftingBackward(table, moveUp, initial_size);
1153         /* move backward and stop at best position */
1154         if (!result)
1155             goto cuddZddSiftingAuxOutOfMem;
1156     }
1157     else if ((x - x_low) > (x_high - x)) {
1158         /* must go down first:shorter */
1159         moveDown = cuddZddSiftingDown(table, x, x_high, initial_size);
1160         /* after that point x --> x_high */
1161         if (moveDown == NULL)
1162             goto cuddZddSiftingAuxOutOfMem;
1163         moveUp = cuddZddSiftingUp(table, moveDown->y, x_low,
1164             initial_size);
1165         if (moveUp == NULL)
1166             goto cuddZddSiftingAuxOutOfMem;
1167         result = cuddZddSiftingBackward(table, moveUp, initial_size);
1168         /* move backward and stop at best position */
1169         if (!result)
1170             goto cuddZddSiftingAuxOutOfMem;
1171     }
1172     else {
1173         moveUp = cuddZddSiftingUp(table, x, x_low, initial_size);
1174         /* after that point x --> x_high */
1175         if (moveUp == NULL)
1176             goto cuddZddSiftingAuxOutOfMem;
1177         moveDown = cuddZddSiftingDown(table, moveUp->x, x_high,
1178             initial_size);
1179         /* then move up */
1180         if (moveDown == NULL)
1181             goto cuddZddSiftingAuxOutOfMem;
1182         result = cuddZddSiftingBackward(table, moveDown,
1183             initial_size);
1184         /* move backward and stop at best position */
1185         if (!result)
1186             goto cuddZddSiftingAuxOutOfMem;
1187     }
1188
1189     while (moveDown != NULL) {
1190         move = moveDown->next;
1191         cuddDeallocMove(table, moveDown);
1192         moveDown = move;
1193     }
1194     while (moveUp != NULL) {
1195         move = moveUp->next;
1196         cuddDeallocMove(table, moveUp);
1197         moveUp = move;
1198     }
1199
1200     return(1);
1201
1202 cuddZddSiftingAuxOutOfMem:
1203     while (moveDown != NULL) {
1204         move = moveDown->next;
1205         cuddDeallocMove(table, moveDown);
1206         moveDown = move;
1207     }
1208     while (moveUp != NULL) {
1209         move = moveUp->next;
1210         cuddDeallocMove(table, moveUp);
1211         moveUp = move;
1212     }
1213
1214     return(0);
1215
1216 } /* end of cuddZddSiftingAux */
1217
1218
1219 /**Function********************************************************************
1220
1221   Synopsis    [Sifts a variable up.]
1222
1223   Description [Sifts a variable up. Moves y up until either it reaches
1224   the bound (x_low) or the size of the ZDD heap increases too much.
1225   Returns the set of moves in case of success; NULL if memory is full.]
1226
1227   SideEffects [None]
1228
1229   SeeAlso     []
1230
1231 ******************************************************************************/
1232 static Move *
1233 cuddZddSiftingUp(
1234   DdManager * table,
1235   int  x,
1236   int  x_low,
1237   int  initial_size)
1238 {
1239     Move        *moves;
1240     Move        *move;
1241     int         y;
1242     int         size;
1243     int         limit_size = initial_size;
1244
1245     moves = NULL;
1246     y = cuddZddNextLow(table, x);
1247     while (y >= x_low) {
1248         size = cuddZddSwapInPlace(table, y, x);
1249         if (size == 0)
1250             goto cuddZddSiftingUpOutOfMem;
1251         move = (Move *)cuddDynamicAllocNode(table);
1252         if (move == NULL)
1253             goto cuddZddSiftingUpOutOfMem;
1254         move->x = y;
1255         move->y = x;
1256         move->size = size;
1257         move->next = moves;
1258         moves = move;
1259
1260         if ((double)size > (double)limit_size * table->maxGrowth)
1261             break;
1262         if (size < limit_size)
1263             limit_size = size;
1264
1265         x = y;
1266         y = cuddZddNextLow(table, x);
1267     }
1268     return(moves);
1269
1270 cuddZddSiftingUpOutOfMem:
1271     while (moves != NULL) {
1272         move = moves->next;
1273         cuddDeallocMove(table, moves);
1274         moves = move;
1275     }
1276     return(NULL);
1277
1278 } /* end of cuddZddSiftingUp */
1279
1280
1281 /**Function********************************************************************
1282
1283   Synopsis    [Sifts a variable down.]
1284
1285   Description [Sifts a variable down. Moves x down until either it
1286   reaches the bound (x_high) or the size of the ZDD heap increases too
1287   much. Returns the set of moves in case of success; NULL if memory is
1288   full.]
1289
1290   SideEffects [None]
1291
1292   SeeAlso     []
1293
1294 ******************************************************************************/
1295 static Move *
1296 cuddZddSiftingDown(
1297   DdManager * table,
1298   int  x,
1299   int  x_high,
1300   int  initial_size)
1301 {
1302     Move        *moves;
1303     Move        *move;
1304     int         y;
1305     int         size;
1306     int         limit_size = initial_size;
1307
1308     moves = NULL;
1309     y = cuddZddNextHigh(table, x);
1310     while (y <= x_high) {
1311         size = cuddZddSwapInPlace(table, x, y);
1312         if (size == 0)
1313             goto cuddZddSiftingDownOutOfMem;
1314         move = (Move *)cuddDynamicAllocNode(table);
1315         if (move == NULL)
1316             goto cuddZddSiftingDownOutOfMem;
1317         move->x = x;
1318         move->y = y;
1319         move->size = size;
1320         move->next = moves;
1321         moves = move;
1322
1323         if ((double)size > (double)limit_size * table->maxGrowth)
1324             break;
1325         if (size < limit_size)
1326             limit_size = size;
1327
1328         x = y;
1329         y = cuddZddNextHigh(table, x);
1330     }
1331     return(moves);
1332
1333 cuddZddSiftingDownOutOfMem:
1334     while (moves != NULL) {
1335         move = moves->next;
1336         cuddDeallocMove(table, moves);
1337         moves = move;
1338     }
1339     return(NULL);
1340
1341 } /* end of cuddZddSiftingDown */
1342
1343
1344 /**Function********************************************************************
1345
1346   Synopsis    [Given a set of moves, returns the ZDD heap to the position
1347   giving the minimum size.]
1348
1349   Description [Given a set of moves, returns the ZDD heap to the
1350   position giving the minimum size. In case of ties, returns to the
1351   closest position giving the minimum size. Returns 1 in case of
1352   success; 0 otherwise.]
1353
1354   SideEffects [None]
1355
1356   SeeAlso     []
1357
1358 ******************************************************************************/
1359 static int
1360 cuddZddSiftingBackward(
1361   DdManager * table,
1362   Move * moves,
1363   int  size)
1364 {
1365     int         i;
1366     int         i_best;
1367     Move        *move;
1368     int         res;
1369
1370     /* Find the minimum size among moves. */
1371     i_best = -1;
1372     for (move = moves, i = 0; move != NULL; move = move->next, i++) {
1373         if (move->size < size) {
1374             i_best = i;
1375             size = move->size;
1376         }
1377     }
1378
1379     for (move = moves, i = 0; move != NULL; move = move->next, i++) {
1380         if (i == i_best)
1381             break;
1382         res = cuddZddSwapInPlace(table, move->x, move->y);
1383         if (!res)
1384             return(0);
1385         if (i_best == -1 && res == size)
1386             break;
1387     }
1388
1389     return(1);
1390
1391 } /* end of cuddZddSiftingBackward */
1392
1393
1394 /**Function********************************************************************
1395
1396   Synopsis    [Prepares the ZDD heap for dynamic reordering.]
1397
1398   Description [Prepares the ZDD heap for dynamic reordering. Does
1399   garbage collection, to guarantee that there are no dead nodes;
1400   and clears the cache, which is invalidated by dynamic reordering.]
1401
1402   SideEffects [None]
1403
1404 ******************************************************************************/
1405 static void
1406 zddReorderPreprocess(
1407   DdManager * table)
1408 {
1409
1410     /* Clear the cache. */
1411     cuddCacheFlush(table);
1412
1413     /* Eliminate dead nodes. Do not scan the cache again. */
1414     cuddGarbageCollect(table,0);
1415
1416     return;
1417
1418 } /* end of ddReorderPreprocess */
1419
1420
1421 /**Function********************************************************************
1422
1423   Synopsis    [Shrinks almost empty ZDD subtables at the end of reordering
1424   to guarantee that they have a reasonable load factor.]
1425
1426   Description [Shrinks almost empty subtables at the end of reordering to
1427   guarantee that they have a reasonable load factor. However, if there many
1428   nodes are being reclaimed, then no resizing occurs. Returns 1 in case of
1429   success; 0 otherwise.]
1430
1431   SideEffects [None]
1432
1433 ******************************************************************************/
1434 static int
1435 zddReorderPostprocess(
1436   DdManager * table)
1437 {
1438     int i, j, posn;
1439     DdNodePtr *nodelist, *oldnodelist;
1440     DdNode *node, *next;
1441     unsigned int slots, oldslots;
1442     extern DD_OOMFP MMoutOfMemory;
1443     DD_OOMFP saveHandler;
1444
1445 #ifdef DD_VERBOSE
1446     (void) fflush(table->out);
1447 #endif
1448
1449     /* If we have very many reclaimed nodes, we do not want to shrink
1450     ** the subtables, because this will lead to more garbage
1451     ** collections. More garbage collections mean shorter mean life for
1452     ** nodes with zero reference count; hence lower probability of finding
1453     ** a result in the cache.
1454     */
1455     if (table->reclaimed > table->allocated * 0.5) return(1);
1456
1457     /* Resize subtables. */
1458     for (i = 0; i < table->sizeZ; i++) {
1459         int shift;
1460         oldslots = table->subtableZ[i].slots;
1461         if (oldslots < table->subtableZ[i].keys * DD_MAX_SUBTABLE_SPARSITY ||
1462             oldslots <= table->initSlots) continue;
1463         oldnodelist = table->subtableZ[i].nodelist;
1464         slots = oldslots >> 1;
1465         saveHandler = MMoutOfMemory;
1466         MMoutOfMemory = Cudd_OutOfMem;
1467         nodelist = ALLOC(DdNodePtr, slots);
1468         MMoutOfMemory = saveHandler;
1469         if (nodelist == NULL) {
1470             return(1);
1471         }
1472         table->subtableZ[i].nodelist = nodelist;
1473         table->subtableZ[i].slots = slots;
1474         table->subtableZ[i].shift++;
1475         table->subtableZ[i].maxKeys = slots * DD_MAX_SUBTABLE_DENSITY;
1476 #ifdef DD_VERBOSE
1477         (void) fprintf(table->err,
1478                        "shrunk layer %d (%d keys) from %d to %d slots\n",
1479                        i, table->subtableZ[i].keys, oldslots, slots);
1480 #endif
1481
1482         for (j = 0; (unsigned) j < slots; j++) {
1483             nodelist[j] = NULL;
1484         }
1485         shift = table->subtableZ[i].shift;
1486         for (j = 0; (unsigned) j < oldslots; j++) {
1487             node = oldnodelist[j];
1488             while (node != NULL) {
1489                 next = node->next;
1490                 posn = ddHash(cuddT(node), cuddE(node), shift);
1491                 node->next = nodelist[posn];
1492                 nodelist[posn] = node;
1493                 node = next;
1494             }
1495         }
1496         FREE(oldnodelist);
1497
1498         table->memused += (slots - oldslots) * sizeof(DdNode *);
1499         table->slots += slots - oldslots;
1500         table->minDead = (unsigned) (table->gcFrac * (double) table->slots);
1501         table->cacheSlack = (int) ddMin(table->maxCacheHard,
1502             DD_MAX_CACHE_TO_SLOTS_RATIO*table->slots) -
1503             2 * (int) table->cacheSlots;
1504     }
1505     /* We don't look at the constant subtable, because it is not
1506     ** affected by reordering.
1507     */
1508
1509     return(1);
1510
1511 } /* end of zddReorderPostprocess */
1512
1513
1514 /**Function********************************************************************
1515
1516   Synopsis    [Reorders ZDD variables according to a given permutation.]
1517
1518   Description [Reorders ZDD variables according to a given permutation.
1519   The i-th permutation array contains the index of the variable that
1520   should be brought to the i-th level. zddShuffle assumes that no
1521   dead nodes are present.  The reordering is achieved by a series of
1522   upward sifts.  Returns 1 if successful; 0 otherwise.]
1523
1524   SideEffects [None]
1525
1526   SeeAlso []
1527
1528 ******************************************************************************/
1529 static int
1530 zddShuffle(
1531   DdManager * table,
1532   int * permutation)
1533 {
1534     int         index;
1535     int         level;
1536     int         position;
1537     int         numvars;
1538     int         result;
1539 #ifdef DD_STATS
1540     long        localTime;
1541     int         initialSize;
1542     int         finalSize;
1543     int         previousSize;
1544 #endif
1545
1546     zddTotalNumberSwapping = 0;
1547 #ifdef DD_STATS
1548     localTime = util_cpu_time();
1549     initialSize = table->keysZ;
1550     (void) fprintf(table->out,"#:I_SHUFFLE %8d: initial size\n",
1551                    initialSize);
1552 #endif
1553
1554     numvars = table->sizeZ;
1555
1556     for (level = 0; level < numvars; level++) {
1557         index = permutation[level];
1558         position = table->permZ[index];
1559 #ifdef DD_STATS
1560         previousSize = table->keysZ;
1561 #endif
1562         result = zddSiftUp(table,position,level);
1563         if (!result) return(0);
1564 #ifdef DD_STATS
1565         if (table->keysZ < (unsigned) previousSize) {
1566             (void) fprintf(table->out,"-");
1567         } else if (table->keysZ > (unsigned) previousSize) {
1568             (void) fprintf(table->out,"+");     /* should never happen */
1569         } else {
1570             (void) fprintf(table->out,"=");
1571         }
1572         fflush(table->out);
1573 #endif
1574     }
1575
1576 #ifdef DD_STATS
1577     (void) fprintf(table->out,"\n");
1578     finalSize = table->keysZ;
1579     (void) fprintf(table->out,"#:F_SHUFFLE %8d: final size\n",finalSize);
1580     (void) fprintf(table->out,"#:T_SHUFFLE %8g: total time (sec)\n",
1581         ((double)(util_cpu_time() - localTime)/1000.0));
1582     (void) fprintf(table->out,"#:N_SHUFFLE %8d: total swaps\n",
1583                    zddTotalNumberSwapping);
1584 #endif
1585
1586     return(1);
1587
1588 } /* end of zddShuffle */
1589
1590
1591 /**Function********************************************************************
1592
1593   Synopsis    [Moves one ZDD variable up.]
1594
1595   Description [Takes a ZDD variable from position x and sifts it up to
1596   position xLow;  xLow should be less than or equal to x.
1597   Returns 1 if successful; 0 otherwise]
1598
1599   SideEffects [None]
1600
1601   SeeAlso     []
1602
1603 ******************************************************************************/
1604 static int
1605 zddSiftUp(
1606   DdManager * table,
1607   int  x,
1608   int  xLow)
1609 {
1610     int        y;
1611     int        size;
1612
1613     y = cuddZddNextLow(table,x);
1614     while (y >= xLow) {
1615         size = cuddZddSwapInPlace(table,y,x);
1616         if (size == 0) {
1617             return(0);
1618         }
1619         x = y;
1620         y = cuddZddNextLow(table,x);
1621     }
1622     return(1);
1623
1624 } /* end of zddSiftUp */
1625
1626
1627 /**Function********************************************************************
1628
1629   Synopsis    [Fixes the ZDD variable group tree after a shuffle.]
1630
1631   Description [Fixes the ZDD variable group tree after a
1632   shuffle. Assumes that the order of the variables in a terminal node
1633   has not been changed.]
1634
1635   SideEffects [Changes the ZDD variable group tree.]
1636
1637   SeeAlso     []
1638
1639 ******************************************************************************/
1640 static void
1641 zddFixTree(
1642   DdManager * table,
1643   MtrNode * treenode)
1644 {
1645     if (treenode == NULL) return;
1646     treenode->low = ((int) treenode->index < table->sizeZ) ?
1647         table->permZ[treenode->index] : treenode->index;
1648     if (treenode->child != NULL) {
1649         zddFixTree(table, treenode->child);
1650     }
1651     if (treenode->younger != NULL)
1652         zddFixTree(table, treenode->younger);
1653     if (treenode->parent != NULL && treenode->low < treenode->parent->low) {
1654         treenode->parent->low = treenode->low;
1655         treenode->parent->index = treenode->index;
1656     }
1657     return;
1658
1659 } /* end of zddFixTree */
1660