distr/cudd/cuddReorder.c

   1 /**CFile***********************************************************************
   2
   3   FileName    [cuddReorder.c]
   4
   5   PackageName [cudd]
   6
   7   Synopsis    [Functions for dynamic variable reordering.]
   8
   9   Description [External procedures included in this file:
  10                 <ul>
  11                 <li> Cudd_ReduceHeap()
  12                 <li> Cudd_ShuffleHeap()
  13                 </ul>
  14         Internal procedures included in this module:
  15                 <ul>
  16                 <li> cuddDynamicAllocNode()
  17                 <li> cuddSifting()
  18                 <li> cuddSwapping()
  19                 <li> cuddNextHigh()
  20                 <li> cuddNextLow()
  21                 <li> cuddSwapInPlace()
  22                 <li> cuddBddAlignToZdd()
  23                 </ul>
  24         Static procedures included in this module:
  25                 <ul>
  26                 <li> ddUniqueCompare()
  27                 <li> ddSwapAny()
  28                 <li> ddSiftingAux()
  29                 <li> ddSiftingUp()
  30                 <li> ddSiftingDown()
  31                 <li> ddSiftingBackward()
  32                 <li> ddReorderPreprocess()
  33                 <li> ddReorderPostprocess()
  34                 <li> ddShuffle()
  35                 <li> ddSiftUp()
  36                 <li> bddFixTree()
  37                 </ul>]
  38
  39   Author      [Shipra Panda, Bernard Plessier, Fabio Somenzi]
  40
  41   Copyright   [Copyright (c) 1995-2004, Regents of the University of Colorado
  42
  43   All rights reserved.
  44
  45   Redistribution and use in source and binary forms, with or without
  46   modification, are permitted provided that the following conditions
  47   are met:
  48
  49   Redistributions of source code must retain the above copyright
  50   notice, this list of conditions and the following disclaimer.
  51
  52   Redistributions in binary form must reproduce the above copyright
  53   notice, this list of conditions and the following disclaimer in the
  54   documentation and/or other materials provided with the distribution.
  55
  56   Neither the name of the University of Colorado nor the names of its
  57   contributors may be used to endorse or promote products derived from
  58   this software without specific prior written permission.
  59
  60   THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS
  61   "AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT
  62   LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS
  63   FOR A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE
  64   COPYRIGHT OWNER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT,
  65   INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING,
  66   BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES;
  67   LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER
  68   CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT
  69   LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN
  70   ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE
  71   POSSIBILITY OF SUCH DAMAGE.]
  72
  73 ******************************************************************************/
  74
  75 #include "util.h"
  76 #include "cuddInt.h"
  77
  78 /*---------------------------------------------------------------------------*/
  79 /* Constant declarations                                                     */
  80 /*---------------------------------------------------------------------------*/
  81
  82 #define DD_MAX_SUBTABLE_SPARSITY 8
  83 #define DD_SHRINK_FACTOR 2
  84
  85 /*---------------------------------------------------------------------------*/
  86 /* Stucture declarations                                                     */
  87 /*---------------------------------------------------------------------------*/
  88
  89 /*---------------------------------------------------------------------------*/
  90 /* Type declarations                                                         */
  91 /*---------------------------------------------------------------------------*/
  92
  93 /*---------------------------------------------------------------------------*/
  94 /* Variable declarations                                                     */
  95 /*---------------------------------------------------------------------------*/
  96
  97 #ifndef lint
  98 static char rcsid[] DD_UNUSED = "$Id: cuddReorder.c,v 1.69 2009/02/21 18:24:10 fabio Exp $";
  99 #endif
 100
 101 static  int     *entry;
 102
 103 int     ddTotalNumberSwapping;
 104 #ifdef DD_STATS
 105 int     ddTotalNISwaps;
 106 #endif
 107
 108 /*---------------------------------------------------------------------------*/
 109 /* Macro declarations                                                        */
 110 /*---------------------------------------------------------------------------*/
 111
 112 /**AutomaticStart*************************************************************/
 113
 114 /*---------------------------------------------------------------------------*/
 115 /* Static function prototypes                                                */
 116 /*---------------------------------------------------------------------------*/
 117
 118 static int ddUniqueCompare (int *ptrX, int *ptrY);
 119 static Move * ddSwapAny (DdManager *table, int x, int y);
 120 static int ddSiftingAux (DdManager *table, int x, int xLow, int xHigh);
 121 static Move * ddSiftingUp (DdManager *table, int y, int xLow);
 122 static Move * ddSiftingDown (DdManager *table, int x, int xHigh);
 123 static int ddSiftingBackward (DdManager *table, int size, Move *moves);
 124 static int ddReorderPreprocess (DdManager *table);
 125 static int ddReorderPostprocess (DdManager *table);
 126 static int ddShuffle (DdManager *table, int *permutation);
 127 static int ddSiftUp (DdManager *table, int x, int xLow);
 128 static void bddFixTree (DdManager *table, MtrNode *treenode);
 129 static int ddUpdateMtrTree (DdManager *table, MtrNode *treenode, int *perm, int *invperm);
 130 static int ddCheckPermuation (DdManager *table, MtrNode *treenode, int *perm, int *invperm);
 131
 132 /**AutomaticEnd***************************************************************/
 133
 134
 135 /*---------------------------------------------------------------------------*/
 136 /* Definition of exported functions                                          */
 137 /*---------------------------------------------------------------------------*/
 138
 139
 140 /**Function********************************************************************
 141
 142   Synopsis    [Main dynamic reordering routine.]
 143
 144   Description [Main dynamic reordering routine.
 145   Calls one of the possible reordering procedures:
 146   <ul>
 147   <li>Swapping
 148   <li>Sifting
 149   <li>Symmetric Sifting
 150   <li>Group Sifting
 151   <li>Window Permutation
 152   <li>Simulated Annealing
 153   <li>Genetic Algorithm
 154   <li>Dynamic Programming (exact)
 155   </ul>
 156
 157   For sifting, symmetric sifting, group sifting, and window
 158   permutation it is possible to request reordering to convergence.<p>
 159
 160   The core of all methods is the reordering procedure
 161   cuddSwapInPlace() which swaps two adjacent variables and is based
 162   on Rudell's paper.
 163   Returns 1 in case of success; 0 otherwise. In the case of symmetric
 164   sifting (with and without convergence) returns 1 plus the number of
 165   symmetric variables, in case of success.]
 166
 167   SideEffects [Changes the variable order for all diagrams and clears
 168   the cache.]
 169
 170 ******************************************************************************/
 171 int
 172 Cudd_ReduceHeap(
 173   DdManager * table /* DD manager */,
 174   Cudd_ReorderingType heuristic /* method used for reordering */,
 175   int  minsize /* bound below which no reordering occurs */)
 176 {
 177     DdHook *hook;
 178     int result;
 179     unsigned int nextDyn;
 180 #ifdef DD_STATS
 181     unsigned int initialSize;
 182     unsigned int finalSize;
 183 #endif
 184     long localTime;
 185
 186     /* Don't reorder if there are too many dead nodes. */
 187     if (table->keys - table->dead < (unsigned) minsize)
 188         return(1);
 189
 190     if (heuristic == CUDD_REORDER_SAME) {
 191         heuristic = table->autoMethod;
 192     }
 193     if (heuristic == CUDD_REORDER_NONE) {
 194         return(1);
 195     }
 196
 197     /* This call to Cudd_ReduceHeap does initiate reordering. Therefore
 198     ** we count it.
 199     */
 200     table->reorderings++;
 201
 202     localTime = util_cpu_time();
 203
 204     /* Run the hook functions. */
 205     hook = table->preReorderingHook;
 206     while (hook != NULL) {
 207         int res = (hook->f)(table, "BDD", (void *)heuristic);
 208         if (res == 0) return(0);
 209         hook = hook->next;
 210     }
 211
 212     if (!ddReorderPreprocess(table)) return(0);
 213     ddTotalNumberSwapping = 0;
 214
 215     if (table->keys > table->peakLiveNodes) {
 216         table->peakLiveNodes = table->keys;
 217     }
 218 #ifdef DD_STATS
 219     initialSize = table->keys - table->isolated;
 220     ddTotalNISwaps = 0;
 221
 222     switch(heuristic) {
 223     case CUDD_REORDER_RANDOM:
 224     case CUDD_REORDER_RANDOM_PIVOT:
 225         (void) fprintf(table->out,"#:I_RANDOM  ");
 226         break;
 227     case CUDD_REORDER_SIFT:
 228     case CUDD_REORDER_SIFT_CONVERGE:
 229     case CUDD_REORDER_SYMM_SIFT:
 230     case CUDD_REORDER_SYMM_SIFT_CONV:
 231     case CUDD_REORDER_GROUP_SIFT:
 232     case CUDD_REORDER_GROUP_SIFT_CONV:
 233         (void) fprintf(table->out,"#:I_SIFTING ");
 234         break;
 235     case CUDD_REORDER_WINDOW2:
 236     case CUDD_REORDER_WINDOW3:
 237     case CUDD_REORDER_WINDOW4:
 238     case CUDD_REORDER_WINDOW2_CONV:
 239     case CUDD_REORDER_WINDOW3_CONV:
 240     case CUDD_REORDER_WINDOW4_CONV:
 241         (void) fprintf(table->out,"#:I_WINDOW  ");
 242         break;
 243     case CUDD_REORDER_ANNEALING:
 244         (void) fprintf(table->out,"#:I_ANNEAL  ");
 245         break;
 246     case CUDD_REORDER_GENETIC:
 247         (void) fprintf(table->out,"#:I_GENETIC ");
 248         break;
 249     case CUDD_REORDER_LINEAR:
 250     case CUDD_REORDER_LINEAR_CONVERGE:
 251         (void) fprintf(table->out,"#:I_LINSIFT ");
 252         break;
 253     case CUDD_REORDER_EXACT:
 254         (void) fprintf(table->out,"#:I_EXACT   ");
 255         break;
 256     default:
 257         return(0);
 258     }
 259     (void) fprintf(table->out,"%8d: initial size",initialSize);
 260 #endif
 261
 262     /* See if we should use alternate threshold for maximum growth. */
 263     if (table->reordCycle && table->reorderings % table->reordCycle == 0) {
 264         double saveGrowth = table->maxGrowth;
 265         table->maxGrowth = table->maxGrowthAlt;
 266         result = cuddTreeSifting(table,heuristic);
 267         table->maxGrowth = saveGrowth;
 268     } else {
 269         result = cuddTreeSifting(table,heuristic);
 270     }
 271
 272 #ifdef DD_STATS
 273     (void) fprintf(table->out,"\n");
 274     finalSize = table->keys - table->isolated;
 275     (void) fprintf(table->out,"#:F_REORDER %8d: final size\n",finalSize);
 276     (void) fprintf(table->out,"#:T_REORDER %8g: total time (sec)\n",
 277                    ((double)(util_cpu_time() - localTime)/1000.0));
 278     (void) fprintf(table->out,"#:N_REORDER %8d: total swaps\n",
 279                    ddTotalNumberSwapping);
 280     (void) fprintf(table->out,"#:M_REORDER %8d: NI swaps\n",ddTotalNISwaps);
 281 #endif
 282
 283     if (result == 0)
 284         return(0);
 285
 286     if (!ddReorderPostprocess(table))
 287         return(0);
 288
 289     if (table->realign) {
 290         if (!cuddZddAlignToBdd(table))
 291             return(0);
 292     }
 293
 294     nextDyn = (table->keys - table->constants.keys + 1) *
 295               DD_DYN_RATIO + table->constants.keys;
 296     if (table->reorderings < 20 || nextDyn > table->nextDyn)
 297         table->nextDyn = nextDyn;
 298     else
 299         table->nextDyn += 20;
 300     table->reordered = 1;
 301
 302     /* Run hook functions. */
 303     hook = table->postReorderingHook;
 304     while (hook != NULL) {
 305         int res = (hook->f)(table, "BDD", (void *)localTime);
 306         if (res == 0) return(0);
 307         hook = hook->next;
 308     }
 309     /* Update cumulative reordering time. */
 310     table->reordTime += util_cpu_time() - localTime;
 311
 312     return(result);
 313
 314 } /* end of Cudd_ReduceHeap */
 315
 316
 317 /**Function********************************************************************
 318
 319   Synopsis    [Reorders variables according to given permutation.]
 320
 321   Description [Reorders variables according to given permutation.
 322   The i-th entry of the permutation array contains the index of the variable
 323   that should be brought to the i-th level.  The size of the array should be
 324   equal or greater to the number of variables currently in use.
 325   Returns 1 in case of success; 0 otherwise.]
 326
 327   SideEffects [Changes the variable order for all diagrams and clears
 328   the cache.]
 329
 330   SeeAlso [Cudd_ReduceHeap]
 331
 332 ******************************************************************************/
 333 int
 334 Cudd_ShuffleHeap(
 335   DdManager * table /* DD manager */,
 336   int * permutation /* required variable permutation */)
 337 {
 338
 339     int result;
 340     int i;
 341     int identity = 1;
 342     int *perm;
 343
 344     /* Don't waste time in case of identity permutation. */
 345     for (i = 0; i < table->size; i++) {
 346         if (permutation[i] != table->invperm[i]) {
 347             identity = 0;
 348             break;
 349         }
 350     }
 351     if (identity == 1) {
 352         return(1);
 353     }
 354     if (!ddReorderPreprocess(table)) return(0);
 355     if (table->keys > table->peakLiveNodes) {
 356         table->peakLiveNodes = table->keys;
 357     }
 358
 359     perm = ALLOC(int, table->size);
 360     for (i = 0; i < table->size; i++)
 361         perm[permutation[i]] = i;
 362     if (!ddCheckPermuation(table,table->tree,perm,permutation)) {
 363         FREE(perm);
 364         return(0);
 365     }
 366     if (!ddUpdateMtrTree(table,table->tree,perm,permutation)) {
 367         FREE(perm);
 368         return(0);
 369     }
 370     FREE(perm);
 371
 372     result = ddShuffle(table,permutation);
 373
 374     if (!ddReorderPostprocess(table)) return(0);
 375
 376     return(result);
 377
 378 } /* end of Cudd_ShuffleHeap */
 379
 380
 381 /*---------------------------------------------------------------------------*/
 382 /* Definition of internal functions                                          */
 383 /*---------------------------------------------------------------------------*/
 384
 385
 386 /**Function********************************************************************
 387
 388   Synopsis    [Dynamically allocates a Node.]
 389
 390   Description [Dynamically allocates a Node. This procedure is similar
 391   to cuddAllocNode in Cudd_Table.c, but it does not attempt garbage
 392   collection, because during reordering there are no dead nodes.
 393   Returns a pointer to a new node if successful; NULL is memory is
 394   full.]
 395
 396   SideEffects [None]
 397
 398   SeeAlso     [cuddAllocNode]
 399
 400 ******************************************************************************/
 401 DdNode *
 402 cuddDynamicAllocNode(
 403   DdManager * table)
 404 {
 405     int     i;
 406     DdNodePtr *mem;
 407     DdNode *list, *node;
 408     extern DD_OOMFP MMoutOfMemory;
 409     DD_OOMFP saveHandler;
 410
 411     if (table->nextFree == NULL) {        /* free list is empty */
 412         /* Try to allocate a new block. */
 413         saveHandler = MMoutOfMemory;
 414         MMoutOfMemory = Cudd_OutOfMem;
 415         mem = (DdNodePtr *) ALLOC(DdNode, DD_MEM_CHUNK + 1);
 416         MMoutOfMemory = saveHandler;
 417         if (mem == NULL && table->stash != NULL) {
 418             FREE(table->stash);
 419             table->stash = NULL;
 420             /* Inhibit resizing of tables. */
 421             table->maxCacheHard = table->cacheSlots - 1;
 422             table->cacheSlack = - (int) (table->cacheSlots + 1);
 423             for (i = 0; i < table->size; i++) {
 424                 table->subtables[i].maxKeys <<= 2;
 425             }
 426             mem = (DdNodePtr *) ALLOC(DdNode,DD_MEM_CHUNK + 1);
 427         }
 428         if (mem == NULL) {
 429             /* Out of luck. Call the default handler to do
 430             ** whatever it specifies for a failed malloc.  If this
 431             ** handler returns, then set error code, print
 432             ** warning, and return. */
 433             (*MMoutOfMemory)(sizeof(DdNode)*(DD_MEM_CHUNK + 1));
 434             table->errorCode = CUDD_MEMORY_OUT;
 435 #ifdef DD_VERBOSE
 436             (void) fprintf(table->err,
 437                            "cuddDynamicAllocNode: out of memory");
 438             (void) fprintf(table->err,"Memory in use = %lu\n",
 439                            table->memused);
 440 #endif
 441             return(NULL);
 442         } else {        /* successful allocation; slice memory */
 443             unsigned long offset;
 444             table->memused += (DD_MEM_CHUNK + 1) * sizeof(DdNode);
 445             mem[0] = (DdNode *) table->memoryList;
 446             table->memoryList = mem;
 447
 448             /* Here we rely on the fact that the size of a DdNode is a
 449             ** power of 2 and a multiple of the size of a pointer.
 450             ** If we align one node, all the others will be aligned
 451             ** as well. */
 452             offset = (unsigned long) mem & (sizeof(DdNode) - 1);
 453             mem += (sizeof(DdNode) - offset) / sizeof(DdNodePtr);
 454 #ifdef DD_DEBUG
 455             assert(((unsigned long) mem & (sizeof(DdNode) - 1)) == 0);
 456 #endif
 457             list = (DdNode *) mem;
 458
 459             i = 1;
 460             do {
 461                 list[i - 1].ref = 0;
 462                 list[i - 1].next = &list[i];
 463             } while (++i < DD_MEM_CHUNK);
 464
 465             list[DD_MEM_CHUNK-1].ref = 0;
 466             list[DD_MEM_CHUNK - 1].next = NULL;
 467
 468             table->nextFree = &list[0];
 469         }
 470     } /* if free list empty */
 471
 472     node = table->nextFree;
 473     table->nextFree = node->next;
 474     return (node);
 475
 476 } /* end of cuddDynamicAllocNode */
 477
 478
 479 /**Function********************************************************************
 480
 481   Synopsis    [Implementation of Rudell's sifting algorithm.]
 482
 483   Description [Implementation of Rudell's sifting algorithm.
 484   Assumes that no dead nodes are present.
 485     <ol>
 486     <li> Order all the variables according to the number of entries
 487     in each unique table.
 488     <li> Sift the variable up and down, remembering each time the
 489     total size of the DD heap.
 490     <li> Select the best permutation.
 491     <li> Repeat 3 and 4 for all variables.
 492     </ol>
 493   Returns 1 if successful; 0 otherwise.]
 494
 495   SideEffects [None]
 496
 497 ******************************************************************************/
 498 int
 499 cuddSifting(
 500   DdManager * table,
 501   int  lower,
 502   int  upper)
 503 {
 504     int i;
 505     int *var;
 506     int size;
 507     int x;
 508     int result;
 509 #ifdef DD_STATS
 510     int previousSize;
 511 #endif
 512
 513     size = table->size;
 514
 515     /* Find order in which to sift variables. */
 516     var = NULL;
 517     entry = ALLOC(int,size);
 518     if (entry == NULL) {
 519         table->errorCode = CUDD_MEMORY_OUT;
 520         goto cuddSiftingOutOfMem;
 521     }
 522     var = ALLOC(int,size);
 523     if (var == NULL) {
 524         table->errorCode = CUDD_MEMORY_OUT;
 525         goto cuddSiftingOutOfMem;
 526     }
 527
 528     for (i = 0; i < size; i++) {
 529         x = table->perm[i];
 530         entry[i] = table->subtables[x].keys;
 531         var[i] = i;
 532     }
 533
 534     qsort((void *)var,size,sizeof(int),(DD_QSFP)ddUniqueCompare);
 535
 536     /* Now sift. */
 537     for (i = 0; i < ddMin(table->siftMaxVar,size); i++) {
 538         if (ddTotalNumberSwapping >= table->siftMaxSwap)
 539             break;
 540         x = table->perm[var[i]];
 541
 542         if (x < lower || x > upper || table->subtables[x].bindVar == 1)
 543             continue;
 544 #ifdef DD_STATS
 545         previousSize = table->keys - table->isolated;
 546 #endif
 547         result = ddSiftingAux(table, x, lower, upper);
 548         if (!result) goto cuddSiftingOutOfMem;
 549 #ifdef DD_STATS
 550         if (table->keys < (unsigned) previousSize + table->isolated) {
 551             (void) fprintf(table->out,"-");
 552         } else if (table->keys > (unsigned) previousSize + table->isolated) {
 553             (void) fprintf(table->out,"+");     /* should never happen */
 554             (void) fprintf(table->err,"\nSize increased from %d to %d while sifting variable %d\n", previousSize, table->keys - table->isolated, var[i]);
 555         } else {
 556             (void) fprintf(table->out,"=");
 557         }
 558         fflush(table->out);
 559 #endif
 560     }
 561
 562     FREE(var);
 563     FREE(entry);
 564
 565     return(1);
 566
 567 cuddSiftingOutOfMem:
 568
 569     if (entry != NULL) FREE(entry);
 570     if (var != NULL) FREE(var);
 571
 572     return(0);
 573
 574 } /* end of cuddSifting */
 575
 576
 577 /**Function********************************************************************
 578
 579   Synopsis    [Reorders variables by a sequence of (non-adjacent) swaps.]
 580
 581   Description [Implementation of Plessier's algorithm that reorders
 582   variables by a sequence of (non-adjacent) swaps.
 583     <ol>
 584     <li> Select two variables (RANDOM or HEURISTIC).
 585     <li> Permute these variables.
 586     <li> If the nodes have decreased accept the permutation.
 587     <li> Otherwise reconstruct the original heap.
 588     <li> Loop.
 589     </ol>
 590   Returns 1 in case of success; 0 otherwise.]
 591
 592   SideEffects [None]
 593
 594 ******************************************************************************/
 595 int
 596 cuddSwapping(
 597   DdManager * table,
 598   int lower,
 599   int upper,
 600   Cudd_ReorderingType heuristic)
 601 {
 602     int i, j;
 603     int max, keys;
 604     int nvars;
 605     int x, y;
 606     int iterate;
 607     int previousSize;
 608     Move *moves, *move;
 609     int pivot;
 610     int modulo;
 611     int result;
 612
 613 #ifdef DD_DEBUG
 614     /* Sanity check */
 615     assert(lower >= 0 && upper < table->size && lower <= upper);
 616 #endif
 617
 618     nvars = upper - lower + 1;
 619     iterate = nvars;
 620
 621     for (i = 0; i < iterate; i++) {
 622         if (ddTotalNumberSwapping >= table->siftMaxSwap)
 623             break;
 624         if (heuristic == CUDD_REORDER_RANDOM_PIVOT) {
 625             max = -1;
 626             for (j = lower; j <= upper; j++) {
 627                 if ((keys = table->subtables[j].keys) > max) {
 628                     max = keys;
 629                     pivot = j;
 630                 }
 631             }
 632
 633             modulo = upper - pivot;
 634             if (modulo == 0) {
 635                 y = pivot;
 636             } else{
 637                 y = pivot + 1 + ((int) Cudd_Random() % modulo);
 638             }
 639
 640             modulo = pivot - lower - 1;
 641             if (modulo < 1) {
 642                 x = lower;
 643             } else{
 644                 do {
 645                     x = (int) Cudd_Random() % modulo;
 646                 } while (x == y);
 647             }
 648         } else {
 649             x = ((int) Cudd_Random() % nvars) + lower;
 650             do {
 651                 y = ((int) Cudd_Random() % nvars) + lower;
 652             } while (x == y);
 653         }
 654         previousSize = table->keys - table->isolated;
 655         moves = ddSwapAny(table,x,y);
 656         if (moves == NULL) goto cuddSwappingOutOfMem;
 657         result = ddSiftingBackward(table,previousSize,moves);
 658         if (!result) goto cuddSwappingOutOfMem;
 659         while (moves != NULL) {
 660             move = moves->next;
 661             cuddDeallocMove(table, moves);
 662             moves = move;
 663         }
 664 #ifdef DD_STATS
 665         if (table->keys < (unsigned) previousSize + table->isolated) {
 666             (void) fprintf(table->out,"-");
 667         } else if (table->keys > (unsigned) previousSize + table->isolated) {
 668             (void) fprintf(table->out,"+");     /* should never happen */
 669         } else {
 670             (void) fprintf(table->out,"=");
 671         }
 672         fflush(table->out);
 673 #endif
 674 #if 0
 675         (void) fprintf(table->out,"#:t_SWAPPING %8d: tmp size\n",
 676                        table->keys - table->isolated);
 677 #endif
 678     }
 679
 680     return(1);
 681
 682 cuddSwappingOutOfMem:
 683     while (moves != NULL) {
 684         move = moves->next;
 685         cuddDeallocMove(table, moves);
 686         moves = move;
 687     }
 688
 689     return(0);
 690
 691 } /* end of cuddSwapping */
 692
 693
 694 /**Function********************************************************************
 695
 696   Synopsis    [Finds the next subtable with a larger index.]
 697
 698   Description [Finds the next subtable with a larger index. Returns the
 699   index.]
 700
 701   SideEffects [None]
 702
 703   SeeAlso     [cuddNextLow]
 704
 705 ******************************************************************************/
 706 int
 707 cuddNextHigh(
 708   DdManager * table,
 709   int  x)
 710 {
 711     return(x+1);
 712
 713 } /* end of cuddNextHigh */
 714
 715
 716 /**Function********************************************************************
 717
 718   Synopsis    [Finds the next subtable with a smaller index.]
 719
 720   Description [Finds the next subtable with a smaller index. Returns the
 721   index.]
 722
 723   SideEffects [None]
 724
 725   SeeAlso     [cuddNextHigh]
 726
 727 ******************************************************************************/
 728 int
 729 cuddNextLow(
 730   DdManager * table,
 731   int  x)
 732 {
 733     return(x-1);
 734
 735 } /* end of cuddNextLow */
 736
 737
 738 /**Function********************************************************************
 739
 740   Synopsis    [Swaps two adjacent variables.]
 741
 742   Description [Swaps two adjacent variables. It assumes that no dead
 743   nodes are present on entry to this procedure.  The procedure then
 744   guarantees that no dead nodes will be present when it terminates.
 745   cuddSwapInPlace assumes that x &lt; y.  Returns the number of keys in
 746   the table if successful; 0 otherwise.]
 747
 748   SideEffects [None]
 749
 750 ******************************************************************************/
 751 int
 752 cuddSwapInPlace(
 753   DdManager * table,
 754   int  x,
 755   int  y)
 756 {
 757     DdNodePtr *xlist, *ylist;
 758     int    xindex, yindex;
 759     int    xslots, yslots;
 760     int    xshift, yshift;
 761     int    oldxkeys, oldykeys;
 762     int    newxkeys, newykeys;
 763     int    comple, newcomplement;
 764     int    i;
 765     Cudd_VariableType varType;
 766     Cudd_LazyGroupType groupType;
 767     int    posn;
 768     int    isolated;
 769     DdNode *f,*f0,*f1,*f01,*f00,*f11,*f10,*newf1,*newf0;
 770     DdNode *g,*next;
 771     DdNodePtr *previousP;
 772     DdNode *tmp;
 773     DdNode *sentinel = &(table->sentinel);
 774     extern DD_OOMFP MMoutOfMemory;
 775     DD_OOMFP saveHandler;
 776
 777 #ifdef DD_DEBUG
 778     int    count,idcheck;
 779 #endif
 780
 781 #ifdef DD_DEBUG
 782     assert(x < y);
 783     assert(cuddNextHigh(table,x) == y);
 784     assert(table->subtables[x].keys != 0);
 785     assert(table->subtables[y].keys != 0);
 786     assert(table->subtables[x].dead == 0);
 787     assert(table->subtables[y].dead == 0);
 788 #endif
 789
 790     ddTotalNumberSwapping++;
 791
 792     /* Get parameters of x subtable. */
 793     xindex = table->invperm[x];
 794     xlist = table->subtables[x].nodelist;
 795     oldxkeys = table->subtables[x].keys;
 796     xslots = table->subtables[x].slots;
 797     xshift = table->subtables[x].shift;
 798
 799     /* Get parameters of y subtable. */
 800     yindex = table->invperm[y];
 801     ylist = table->subtables[y].nodelist;
 802     oldykeys = table->subtables[y].keys;
 803     yslots = table->subtables[y].slots;
 804     yshift = table->subtables[y].shift;
 805
 806     if (!cuddTestInteract(table,xindex,yindex)) {
 807 #ifdef DD_STATS
 808         ddTotalNISwaps++;
 809 #endif
 810         newxkeys = oldxkeys;
 811         newykeys = oldykeys;
 812     } else {
 813         newxkeys = 0;
 814         newykeys = oldykeys;
 815
 816         /* Check whether the two projection functions involved in this
 817         ** swap are isolated. At the end, we'll be able to tell how many
 818         ** isolated projection functions are there by checking only these
 819         ** two functions again. This is done to eliminate the isolated
 820         ** projection functions from the node count.
 821         */
 822         isolated = - ((table->vars[xindex]->ref == 1) +
 823                      (table->vars[yindex]->ref == 1));
 824
 825         /* The nodes in the x layer that do not depend on
 826         ** y will stay there; the others are put in a chain.
 827         ** The chain is handled as a LIFO; g points to the beginning.
 828         */
 829         g = NULL;
 830         if ((oldxkeys >= xslots || (unsigned) xslots == table->initSlots) &&
 831             oldxkeys <= DD_MAX_SUBTABLE_DENSITY * xslots) {
 832             for (i = 0; i < xslots; i++) {
 833                 previousP = &(xlist[i]);
 834                 f = *previousP;
 835                 while (f != sentinel) {
 836                     next = f->next;
 837                     f1 = cuddT(f); f0 = cuddE(f);
 838                     if (f1->index != (DdHalfWord) yindex &&
 839                         Cudd_Regular(f0)->index != (DdHalfWord) yindex) {
 840                         /* stays */
 841                         newxkeys++;
 842                         *previousP = f;
 843                         previousP = &(f->next);
 844                     } else {
 845                         f->index = yindex;
 846                         f->next = g;
 847                         g = f;
 848                     }
 849                     f = next;
 850                 } /* while there are elements in the collision chain */
 851                 *previousP = sentinel;
 852             } /* for each slot of the x subtable */
 853         } else {                /* resize xlist */
 854             DdNode *h = NULL;
 855             DdNodePtr *newxlist;
 856             unsigned int newxslots;
 857             int newxshift;
 858             /* Empty current xlist. Nodes that stay go to list h;
 859             ** nodes that move go to list g. */
 860             for (i = 0; i < xslots; i++) {
 861                 f = xlist[i];
 862                 while (f != sentinel) {
 863                     next = f->next;
 864                     f1 = cuddT(f); f0 = cuddE(f);
 865                     if (f1->index != (DdHalfWord) yindex &&
 866                         Cudd_Regular(f0)->index != (DdHalfWord) yindex) {
 867                         /* stays */
 868                         f->next = h;
 869                         h = f;
 870                         newxkeys++;
 871                     } else {
 872                         f->index = yindex;
 873                         f->next = g;
 874                         g = f;
 875                     }
 876                     f = next;
 877                 } /* while there are elements in the collision chain */
 878             } /* for each slot of the x subtable */
 879             /* Decide size of new subtable. */
 880             newxshift = xshift;
 881             newxslots = xslots;
 882             while ((unsigned) oldxkeys > DD_MAX_SUBTABLE_DENSITY * newxslots) {
 883                 newxshift--;
 884                 newxslots <<= 1;
 885             }
 886             while ((unsigned) oldxkeys < newxslots &&
 887                    newxslots > table->initSlots) {
 888                 newxshift++;
 889                 newxslots >>= 1;
 890             }
 891             /* Try to allocate new table. Be ready to back off. */
 892             saveHandler = MMoutOfMemory;
 893             MMoutOfMemory = Cudd_OutOfMem;
 894             newxlist = ALLOC(DdNodePtr, newxslots);
 895             MMoutOfMemory = saveHandler;
 896             if (newxlist == NULL) {
 897                 (void) fprintf(table->err, "Unable to resize subtable %d for lack of memory\n", i);
 898                 newxlist = xlist;
 899                 newxslots = xslots;
 900                 newxshift = xshift;
 901             } else {
 902                 table->slots += ((int) newxslots - xslots);
 903                 table->minDead = (unsigned)
 904                     (table->gcFrac * (double) table->slots);
 905                 table->cacheSlack = (int)
 906                     ddMin(table->maxCacheHard, DD_MAX_CACHE_TO_SLOTS_RATIO
 907                           * table->slots) - 2 * (int) table->cacheSlots;
 908                 table->memused +=
 909                     ((int) newxslots - xslots) * sizeof(DdNodePtr);
 910                 FREE(xlist);
 911                 xslots =  newxslots;
 912                 xshift = newxshift;
 913                 xlist = newxlist;
 914             }
 915             /* Initialize new subtable. */
 916             for (i = 0; i < xslots; i++) {
 917                 xlist[i] = sentinel;
 918             }
 919             /* Move nodes that were parked in list h to their new home. */
 920             f = h;
 921             while (f != NULL) {
 922                 next = f->next;
 923                 f1 = cuddT(f);
 924                 f0 = cuddE(f);
 925                 /* Check xlist for pair (f11,f01). */
 926                 posn = ddHash(f1, f0, xshift);
 927                 /* For each element tmp in collision list xlist[posn]. */
 928                 previousP = &(xlist[posn]);
 929                 tmp = *previousP;
 930                 while (f1 < cuddT(tmp)) {
 931                     previousP = &(tmp->next);
 932                     tmp = *previousP;
 933                 }
 934                 while (f1 == cuddT(tmp) && f0 < cuddE(tmp)) {
 935                     previousP = &(tmp->next);
 936                     tmp = *previousP;
 937                 }
 938                 f->next = *previousP;
 939                 *previousP = f;
 940                 f = next;
 941             }
 942         }
 943
 944 #ifdef DD_COUNT
 945         table->swapSteps += oldxkeys - newxkeys;
 946 #endif
 947         /* Take care of the x nodes that must be re-expressed.
 948         ** They form a linked list pointed by g. Their index has been
 949         ** already changed to yindex.
 950         */
 951         f = g;
 952         while (f != NULL) {
 953             next = f->next;
 954             /* Find f1, f0, f11, f10, f01, f00. */
 955             f1 = cuddT(f);
 956 #ifdef DD_DEBUG
 957             assert(!(Cudd_IsComplement(f1)));
 958 #endif
 959             if ((int) f1->index == yindex) {
 960                 f11 = cuddT(f1); f10 = cuddE(f1);
 961             } else {
 962                 f11 = f10 = f1;
 963             }
 964 #ifdef DD_DEBUG
 965             assert(!(Cudd_IsComplement(f11)));
 966 #endif
 967             f0 = cuddE(f);
 968             comple = Cudd_IsComplement(f0);
 969             f0 = Cudd_Regular(f0);
 970             if ((int) f0->index == yindex) {
 971                 f01 = cuddT(f0); f00 = cuddE(f0);
 972             } else {
 973                 f01 = f00 = f0;
 974             }
 975             if (comple) {
 976                 f01 = Cudd_Not(f01);
 977                 f00 = Cudd_Not(f00);
 978             }
 979             /* Decrease ref count of f1. */
 980             cuddSatDec(f1->ref);
 981             /* Create the new T child. */
 982             if (f11 == f01) {
 983                 newf1 = f11;
 984                 cuddSatInc(newf1->ref);
 985             } else {
 986                 /* Check xlist for triple (xindex,f11,f01). */
 987                 posn = ddHash(f11, f01, xshift);
 988                 /* For each element newf1 in collision list xlist[posn]. */
 989                 previousP = &(xlist[posn]);
 990                 newf1 = *previousP;
 991                 while (f11 < cuddT(newf1)) {
 992                     previousP = &(newf1->next);
 993                     newf1 = *previousP;
 994                 }
 995                 while (f11 == cuddT(newf1) && f01 < cuddE(newf1)) {
 996                     previousP = &(newf1->next);
 997                     newf1 = *previousP;
 998                 }
 999                 if (cuddT(newf1) == f11 && cuddE(newf1) == f01) {
1000                     cuddSatInc(newf1->ref);
1001                 } else { /* no match */
1002                     newf1 = cuddDynamicAllocNode(table);
1003                     if (newf1 == NULL)
1004                         goto cuddSwapOutOfMem;
1005                     newf1->index = xindex; newf1->ref = 1;
1006                     cuddT(newf1) = f11;
1007                     cuddE(newf1) = f01;
1008                     /* Insert newf1 in the collision list xlist[posn];
1009                     ** increase the ref counts of f11 and f01.
1010                     */
1011                     newxkeys++;
1012                     newf1->next = *previousP;
1013                     *previousP = newf1;
1014                     cuddSatInc(f11->ref);
1015                     tmp = Cudd_Regular(f01);
1016                     cuddSatInc(tmp->ref);
1017                 }
1018             }
1019             cuddT(f) = newf1;
1020 #ifdef DD_DEBUG
1021             assert(!(Cudd_IsComplement(newf1)));
1022 #endif
1023
1024             /* Do the same for f0, keeping complement dots into account. */
1025             /* Decrease ref count of f0. */
1026             tmp = Cudd_Regular(f0);
1027             cuddSatDec(tmp->ref);
1028             /* Create the new E child. */
1029             if (f10 == f00) {
1030                 newf0 = f00;
1031                 tmp = Cudd_Regular(newf0);
1032                 cuddSatInc(tmp->ref);
1033             } else {
1034                 /* make sure f10 is regular */
1035                 newcomplement = Cudd_IsComplement(f10);
1036                 if (newcomplement) {
1037                     f10 = Cudd_Not(f10);
1038                     f00 = Cudd_Not(f00);
1039                 }
1040                 /* Check xlist for triple (xindex,f10,f00). */
1041                 posn = ddHash(f10, f00, xshift);
1042                 /* For each element newf0 in collision list xlist[posn]. */
1043                 previousP = &(xlist[posn]);
1044                 newf0 = *previousP;
1045                 while (f10 < cuddT(newf0)) {
1046                     previousP = &(newf0->next);
1047                     newf0 = *previousP;
1048                 }
1049                 while (f10 == cuddT(newf0) && f00 < cuddE(newf0)) {
1050                     previousP = &(newf0->next);
1051                     newf0 = *previousP;
1052                 }
1053                 if (cuddT(newf0) == f10 && cuddE(newf0) == f00) {
1054                     cuddSatInc(newf0->ref);
1055                 } else { /* no match */
1056                     newf0 = cuddDynamicAllocNode(table);
1057                     if (newf0 == NULL)
1058                         goto cuddSwapOutOfMem;
1059                     newf0->index = xindex; newf0->ref = 1;
1060                     cuddT(newf0) = f10;
1061                     cuddE(newf0) = f00;
1062                     /* Insert newf0 in the collision list xlist[posn];
1063                     ** increase the ref counts of f10 and f00.
1064                     */
1065                     newxkeys++;
1066                     newf0->next = *previousP;
1067                     *previousP = newf0;
1068                     cuddSatInc(f10->ref);
1069                     tmp = Cudd_Regular(f00);
1070                     cuddSatInc(tmp->ref);
1071                 }
1072                 if (newcomplement) {
1073                     newf0 = Cudd_Not(newf0);
1074                 }
1075             }
1076             cuddE(f) = newf0;
1077
1078             /* Insert the modified f in ylist.
1079             ** The modified f does not already exists in ylist.
1080             ** (Because of the uniqueness of the cofactors.)
1081             */
1082             posn = ddHash(newf1, newf0, yshift);
1083             newykeys++;
1084             previousP = &(ylist[posn]);
1085             tmp = *previousP;
1086             while (newf1 < cuddT(tmp)) {
1087                 previousP = &(tmp->next);
1088                 tmp = *previousP;
1089             }
1090             while (newf1 == cuddT(tmp) && newf0 < cuddE(tmp)) {
1091                 previousP = &(tmp->next);
1092                 tmp = *previousP;
1093             }
1094             f->next = *previousP;
1095             *previousP = f;
1096             f = next;
1097         } /* while f != NULL */
1098
1099         /* GC the y layer. */
1100
1101         /* For each node f in ylist. */
1102         for (i = 0; i < yslots; i++) {
1103             previousP = &(ylist[i]);
1104             f = *previousP;
1105             while (f != sentinel) {
1106                 next = f->next;
1107                 if (f->ref == 0) {
1108                     tmp = cuddT(f);
1109                     cuddSatDec(tmp->ref);
1110                     tmp = Cudd_Regular(cuddE(f));
1111                     cuddSatDec(tmp->ref);
1112                     cuddDeallocNode(table,f);
1113                     newykeys--;
1114                 } else {
1115                     *previousP = f;
1116                     previousP = &(f->next);
1117                 }
1118                 f = next;
1119             } /* while f */
1120             *previousP = sentinel;
1121         } /* for i */
1122
1123 #ifdef DD_DEBUG
1124 #if 0
1125         (void) fprintf(table->out,"Swapping %d and %d\n",x,y);
1126 #endif
1127         count = 0;
1128         idcheck = 0;
1129         for (i = 0; i < yslots; i++) {
1130             f = ylist[i];
1131             while (f != sentinel) {
1132                 count++;
1133                 if (f->index != (DdHalfWord) yindex)
1134                     idcheck++;
1135                 f = f->next;
1136             }
1137         }
1138         if (count != newykeys) {
1139             (void) fprintf(table->out,
1140                            "Error in finding newykeys\toldykeys = %d\tnewykeys = %d\tactual = %d\n",
1141                            oldykeys,newykeys,count);
1142         }
1143         if (idcheck != 0)
1144             (void) fprintf(table->out,
1145                            "Error in id's of ylist\twrong id's = %d\n",
1146                            idcheck);
1147         count = 0;
1148         idcheck = 0;
1149         for (i = 0; i < xslots; i++) {
1150             f = xlist[i];
1151             while (f != sentinel) {
1152                 count++;
1153                 if (f->index != (DdHalfWord) xindex)
1154                     idcheck++;
1155                 f = f->next;
1156             }
1157         }
1158         if (count != newxkeys) {
1159             (void) fprintf(table->out,
1160                            "Error in finding newxkeys\toldxkeys = %d \tnewxkeys = %d \tactual = %d\n",
1161                            oldxkeys,newxkeys,count);
1162         }
1163         if (idcheck != 0)
1164             (void) fprintf(table->out,
1165                            "Error in id's of xlist\twrong id's = %d\n",
1166                            idcheck);
1167 #endif
1168
1169         isolated += (table->vars[xindex]->ref == 1) +
1170                     (table->vars[yindex]->ref == 1);
1171         table->isolated += isolated;
1172     }
1173
1174     /* Set the appropriate fields in table. */
1175     table->subtables[x].nodelist = ylist;
1176     table->subtables[x].slots = yslots;
1177     table->subtables[x].shift = yshift;
1178     table->subtables[x].keys = newykeys;
1179     table->subtables[x].maxKeys = yslots * DD_MAX_SUBTABLE_DENSITY;
1180     i = table->subtables[x].bindVar;
1181     table->subtables[x].bindVar = table->subtables[y].bindVar;
1182     table->subtables[y].bindVar = i;
1183     /* Adjust filds for lazy sifting. */
1184     varType = table->subtables[x].varType;
1185     table->subtables[x].varType = table->subtables[y].varType;
1186     table->subtables[y].varType = varType;
1187     i = table->subtables[x].pairIndex;
1188     table->subtables[x].pairIndex = table->subtables[y].pairIndex;
1189     table->subtables[y].pairIndex = i;
1190     i = table->subtables[x].varHandled;
1191     table->subtables[x].varHandled = table->subtables[y].varHandled;
1192     table->subtables[y].varHandled = i;
1193     groupType = table->subtables[x].varToBeGrouped;
1194     table->subtables[x].varToBeGrouped = table->subtables[y].varToBeGrouped;
1195     table->subtables[y].varToBeGrouped = groupType;
1196
1197     table->subtables[y].nodelist = xlist;
1198     table->subtables[y].slots = xslots;
1199     table->subtables[y].shift = xshift;
1200     table->subtables[y].keys = newxkeys;
1201     table->subtables[y].maxKeys = xslots * DD_MAX_SUBTABLE_DENSITY;
1202
1203     table->perm[xindex] = y; table->perm[yindex] = x;
1204     table->invperm[x] = yindex; table->invperm[y] = xindex;
1205
1206     table->keys += newxkeys + newykeys - oldxkeys - oldykeys;
1207
1208     return(table->keys - table->isolated);
1209
1210 cuddSwapOutOfMem:
1211     (void) fprintf(table->err,"Error: cuddSwapInPlace out of memory\n");
1212
1213     return (0);
1214
1215 } /* end of cuddSwapInPlace */
1216
1217
1218 /**Function********************************************************************
1219
1220   Synopsis    [Reorders BDD variables according to the order of the ZDD
1221   variables.]
1222
1223   Description [Reorders BDD variables according to the order of the
1224   ZDD variables. This function can be called at the end of ZDD
1225   reordering to insure that the order of the BDD variables is
1226   consistent with the order of the ZDD variables. The number of ZDD
1227   variables must be a multiple of the number of BDD variables. Let
1228   <code>M</code> be the ratio of the two numbers. cuddBddAlignToZdd
1229   then considers the ZDD variables from <code>M*i</code> to
1230   <code>(M+1)*i-1</code> as corresponding to BDD variable
1231   <code>i</code>.  This function should be normally called from
1232   Cudd_zddReduceHeap, which clears the cache.  Returns 1 in case of
1233   success; 0 otherwise.]
1234
1235   SideEffects [Changes the BDD variable order for all diagrams and performs
1236   garbage collection of the BDD unique table.]
1237
1238   SeeAlso [Cudd_ShuffleHeap Cudd_zddReduceHeap]
1239
1240 ******************************************************************************/
1241 int
1242 cuddBddAlignToZdd(
1243   DdManager * table /* DD manager */)
1244 {
1245     int *invperm;               /* permutation array */
1246     int M;                      /* ratio of ZDD variables to BDD variables */
1247     int i;                      /* loop index */
1248     int result;                 /* return value */
1249
1250     /* We assume that a ratio of 0 is OK. */
1251     if (table->size == 0)
1252         return(1);
1253
1254     M = table->sizeZ / table->size;
1255     /* Check whether the number of ZDD variables is a multiple of the
1256     ** number of BDD variables.
1257     */
1258     if (M * table->size != table->sizeZ)
1259         return(0);
1260     /* Create and initialize the inverse permutation array. */
1261     invperm = ALLOC(int,table->size);
1262     if (invperm == NULL) {
1263         table->errorCode = CUDD_MEMORY_OUT;
1264         return(0);
1265     }
1266     for (i = 0; i < table->sizeZ; i += M) {
1267         int indexZ = table->invpermZ[i];
1268         int index  = indexZ / M;
1269         invperm[i / M] = index;
1270     }
1271     /* Eliminate dead nodes. Do not scan the cache again, because we
1272     ** assume that Cudd_zddReduceHeap has already cleared it.
1273     */
1274     cuddGarbageCollect(table,0);
1275
1276     /* Initialize number of isolated projection functions. */
1277     table->isolated = 0;
1278     for (i = 0; i < table->size; i++) {
1279         if (table->vars[i]->ref == 1) table->isolated++;
1280     }
1281
1282     /* Initialize the interaction matrix. */
1283     result = cuddInitInteract(table);
1284     if (result == 0) return(0);
1285
1286     result = ddShuffle(table, invperm);
1287     FREE(invperm);
1288     /* Free interaction matrix. */
1289     FREE(table->interact);
1290     /* Fix the BDD variable group tree. */
1291     bddFixTree(table,table->tree);
1292     return(result);
1293
1294 } /* end of cuddBddAlignToZdd */
1295
1296 /*---------------------------------------------------------------------------*/
1297 /* Definition of static functions                                            */
1298 /*---------------------------------------------------------------------------*/
1299
1300
1301 /**Function********************************************************************
1302
1303   Synopsis    [Comparison function used by qsort.]
1304
1305   Description [Comparison function used by qsort to order the
1306   variables according to the number of keys in the subtables.
1307   Returns the difference in number of keys between the two
1308   variables being compared.]
1309
1310   SideEffects [None]
1311
1312 ******************************************************************************/
1313 static int
1314 ddUniqueCompare(
1315   int * ptrX,
1316   int * ptrY)
1317 {
1318 #if 0
1319     if (entry[*ptrY] == entry[*ptrX]) {
1320         return((*ptrX) - (*ptrY));
1321     }
1322 #endif
1323     return(entry[*ptrY] - entry[*ptrX]);
1324
1325 } /* end of ddUniqueCompare */
1326
1327
1328 /**Function********************************************************************
1329
1330   Synopsis    [Swaps any two variables.]
1331
1332   Description [Swaps any two variables. Returns the set of moves.]
1333
1334   SideEffects [None]
1335
1336 ******************************************************************************/
1337 static Move *
1338 ddSwapAny(
1339   DdManager * table,
1340   int  x,
1341   int  y)
1342 {
1343     Move        *move, *moves;
1344     int         xRef,yRef;
1345     int         xNext,yNext;
1346     int         size;
1347     int         limitSize;
1348     int         tmp;
1349
1350     if (x >y) {
1351         tmp = x; x = y; y = tmp;
1352     }
1353
1354     xRef = x; yRef = y;
1355
1356     xNext = cuddNextHigh(table,x);
1357     yNext = cuddNextLow(table,y);
1358     moves = NULL;
1359     limitSize = table->keys - table->isolated;
1360
1361     for (;;) {
1362         if ( xNext == yNext) {
1363             size = cuddSwapInPlace(table,x,xNext);
1364             if (size == 0) goto ddSwapAnyOutOfMem;
1365             move = (Move *) cuddDynamicAllocNode(table);
1366             if (move == NULL) goto ddSwapAnyOutOfMem;
1367             move->x = x;
1368             move->y = xNext;
1369             move->size = size;
1370             move->next = moves;
1371             moves = move;
1372
1373             size = cuddSwapInPlace(table,yNext,y);
1374             if (size == 0) goto ddSwapAnyOutOfMem;
1375             move = (Move *) cuddDynamicAllocNode(table);
1376             if (move == NULL) goto ddSwapAnyOutOfMem;
1377             move->x = yNext;
1378             move->y = y;
1379             move->size = size;
1380             move->next = moves;
1381             moves = move;
1382
1383             size = cuddSwapInPlace(table,x,xNext);
1384             if (size == 0) goto ddSwapAnyOutOfMem;
1385             move = (Move *) cuddDynamicAllocNode(table);
1386             if (move == NULL) goto ddSwapAnyOutOfMem;
1387             move->x = x;
1388             move->y = xNext;
1389             move->size = size;
1390             move->next = moves;
1391             moves = move;
1392
1393             tmp = x; x = y; y = tmp;
1394
1395         } else if (x == yNext) {
1396
1397             size = cuddSwapInPlace(table,x,xNext);
1398             if (size == 0) goto ddSwapAnyOutOfMem;
1399             move = (Move *) cuddDynamicAllocNode(table);
1400             if (move == NULL) goto ddSwapAnyOutOfMem;
1401             move->x = x;
1402             move->y = xNext;
1403             move->size = size;
1404             move->next = moves;
1405             moves = move;
1406
1407             tmp = x; x = y; y = tmp;
1408
1409         } else {
1410             size = cuddSwapInPlace(table,x,xNext);
1411             if (size == 0) goto ddSwapAnyOutOfMem;
1412             move = (Move *) cuddDynamicAllocNode(table);
1413             if (move == NULL) goto ddSwapAnyOutOfMem;
1414             move->x = x;
1415             move->y = xNext;
1416             move->size = size;
1417             move->next = moves;
1418             moves = move;
1419
1420             size = cuddSwapInPlace(table,yNext,y);
1421             if (size == 0) goto ddSwapAnyOutOfMem;
1422             move = (Move *) cuddDynamicAllocNode(table);
1423             if (move == NULL) goto ddSwapAnyOutOfMem;
1424             move->x = yNext;
1425             move->y = y;
1426             move->size = size;
1427             move->next = moves;
1428             moves = move;
1429
1430             x = xNext;
1431             y = yNext;
1432         }
1433
1434         xNext = cuddNextHigh(table,x);
1435         yNext = cuddNextLow(table,y);
1436         if (xNext > yRef) break;
1437
1438         if ((double) size > table->maxGrowth * (double) limitSize) break;
1439         if (size < limitSize) limitSize = size;
1440     }
1441     if (yNext>=xRef) {
1442         size = cuddSwapInPlace(table,yNext,y);
1443         if (size == 0) goto ddSwapAnyOutOfMem;
1444         move = (Move *) cuddDynamicAllocNode(table);
1445         if (move == NULL) goto ddSwapAnyOutOfMem;
1446         move->x = yNext;
1447         move->y = y;
1448         move->size = size;
1449         move->next = moves;
1450         moves = move;
1451     }
1452
1453     return(moves);
1454
1455 ddSwapAnyOutOfMem:
1456     while (moves != NULL) {
1457         move = moves->next;
1458         cuddDeallocMove(table, moves);
1459         moves = move;
1460     }
1461     return(NULL);
1462
1463 } /* end of ddSwapAny */
1464
1465
1466 /**Function********************************************************************
1467
1468   Synopsis    [Given xLow <= x <= xHigh moves x up and down between the
1469   boundaries.]
1470
1471   Description [Given xLow <= x <= xHigh moves x up and down between the
1472   boundaries. Finds the best position and does the required changes.
1473   Returns 1 if successful; 0 otherwise.]
1474
1475   SideEffects [None]
1476
1477 ******************************************************************************/
1478 static int
1479 ddSiftingAux(
1480   DdManager * table,
1481   int  x,
1482   int  xLow,
1483   int  xHigh)
1484 {
1485
1486     Move        *move;
1487     Move        *moveUp;                /* list of up moves */
1488     Move        *moveDown;              /* list of down moves */
1489     int         initialSize;
1490     int         result;
1491
1492     initialSize = table->keys - table->isolated;
1493
1494     moveDown = NULL;
1495     moveUp = NULL;
1496
1497     if (x == xLow) {
1498         moveDown = ddSiftingDown(table,x,xHigh);
1499         /* At this point x --> xHigh unless bounding occurred. */
1500         if (moveDown == (Move *) CUDD_OUT_OF_MEM) goto ddSiftingAuxOutOfMem;
1501         /* Move backward and stop at best position. */
1502         result = ddSiftingBackward(table,initialSize,moveDown);
1503         if (!result) goto ddSiftingAuxOutOfMem;
1504
1505     } else if (x == xHigh) {
1506         moveUp = ddSiftingUp(table,x,xLow);
1507         /* At this point x --> xLow unless bounding occurred. */
1508         if (moveUp == (Move *) CUDD_OUT_OF_MEM) goto ddSiftingAuxOutOfMem;
1509         /* Move backward and stop at best position. */
1510         result = ddSiftingBackward(table,initialSize,moveUp);
1511         if (!result) goto ddSiftingAuxOutOfMem;
1512
1513     } else if ((x - xLow) > (xHigh - x)) { /* must go down first: shorter */
1514         moveDown = ddSiftingDown(table,x,xHigh);
1515         /* At this point x --> xHigh unless bounding occurred. */
1516         if (moveDown == (Move *) CUDD_OUT_OF_MEM) goto ddSiftingAuxOutOfMem;
1517         if (moveDown != NULL) {
1518             x = moveDown->y;
1519         }
1520         moveUp = ddSiftingUp(table,x,xLow);
1521         if (moveUp == (Move *) CUDD_OUT_OF_MEM) goto ddSiftingAuxOutOfMem;
1522         /* Move backward and stop at best position */
1523         result = ddSiftingBackward(table,initialSize,moveUp);
1524         if (!result) goto ddSiftingAuxOutOfMem;
1525
1526     } else { /* must go up first: shorter */
1527         moveUp = ddSiftingUp(table,x,xLow);
1528         /* At this point x --> xLow unless bounding occurred. */
1529         if (moveUp == (Move *) CUDD_OUT_OF_MEM) goto ddSiftingAuxOutOfMem;
1530         if (moveUp != NULL) {
1531             x = moveUp->x;
1532         }
1533         moveDown = ddSiftingDown(table,x,xHigh);
1534         if (moveDown == (Move *) CUDD_OUT_OF_MEM) goto ddSiftingAuxOutOfMem;
1535         /* Move backward and stop at best position. */
1536         result = ddSiftingBackward(table,initialSize,moveDown);
1537         if (!result) goto ddSiftingAuxOutOfMem;
1538     }
1539
1540     while (moveDown != NULL) {
1541         move = moveDown->next;
1542         cuddDeallocMove(table, moveDown);
1543         moveDown = move;
1544     }
1545     while (moveUp != NULL) {
1546         move = moveUp->next;
1547         cuddDeallocMove(table, moveUp);
1548         moveUp = move;
1549     }
1550
1551     return(1);
1552
1553 ddSiftingAuxOutOfMem:
1554     if (moveDown != (Move *) CUDD_OUT_OF_MEM) {
1555         while (moveDown != NULL) {
1556             move = moveDown->next;
1557             cuddDeallocMove(table, moveDown);
1558             moveDown = move;
1559         }
1560     }
1561     if (moveUp != (Move *) CUDD_OUT_OF_MEM) {
1562         while (moveUp != NULL) {
1563             move = moveUp->next;
1564             cuddDeallocMove(table, moveUp);
1565             moveUp = move;
1566         }
1567     }
1568
1569     return(0);
1570
1571 } /* end of ddSiftingAux */
1572
1573
1574 /**Function********************************************************************
1575
1576   Synopsis    [Sifts a variable up.]
1577
1578   Description [Sifts a variable up. Moves y up until either it reaches
1579   the bound (xLow) or the size of the DD heap increases too much.
1580   Returns the set of moves in case of success; NULL if memory is full.]
1581
1582   SideEffects [None]
1583
1584 ******************************************************************************/
1585 static Move *
1586 ddSiftingUp(
1587   DdManager * table,
1588   int  y,
1589   int  xLow)
1590 {
1591     Move        *moves;
1592     Move        *move;
1593     int         x;
1594     int         size;
1595     int         limitSize;
1596     int         xindex, yindex;
1597     int         isolated;
1598     int         L;      /* lower bound on DD size */
1599 #ifdef DD_DEBUG
1600     int checkL;
1601     int z;
1602     int zindex;
1603 #endif
1604
1605     moves = NULL;
1606     yindex = table->invperm[y];
1607
1608     /* Initialize the lower bound.
1609     ** The part of the DD below y will not change.
1610     ** The part of the DD above y that does not interact with y will not
1611     ** change. The rest may vanish in the best case, except for
1612     ** the nodes at level xLow, which will not vanish, regardless.
1613     */
1614     limitSize = L = table->keys - table->isolated;
1615     for (x = xLow + 1; x < y; x++) {
1616         xindex = table->invperm[x];
1617         if (cuddTestInteract(table,xindex,yindex)) {
1618             isolated = table->vars[xindex]->ref == 1;
1619             L -= table->subtables[x].keys - isolated;
1620         }
1621     }
1622     isolated = table->vars[yindex]->ref == 1;
1623     L -= table->subtables[y].keys - isolated;
1624
1625     x = cuddNextLow(table,y);
1626     while (x >= xLow && L <= limitSize) {
1627         xindex = table->invperm[x];
1628 #ifdef DD_DEBUG
1629         checkL = table->keys - table->isolated;
1630         for (z = xLow + 1; z < y; z++) {
1631             zindex = table->invperm[z];
1632             if (cuddTestInteract(table,zindex,yindex)) {
1633                 isolated = table->vars[zindex]->ref == 1;
1634                 checkL -= table->subtables[z].keys - isolated;
1635             }
1636         }
1637         isolated = table->vars[yindex]->ref == 1;
1638         checkL -= table->subtables[y].keys - isolated;
1639         assert(L == checkL);
1640 #endif
1641         size = cuddSwapInPlace(table,x,y);
1642         if (size == 0) goto ddSiftingUpOutOfMem;
1643         /* Update the lower bound. */
1644         if (cuddTestInteract(table,xindex,yindex)) {
1645             isolated = table->vars[xindex]->ref == 1;
1646             L += table->subtables[y].keys - isolated;
1647         }
1648         move = (Move *) cuddDynamicAllocNode(table);
1649         if (move == NULL) goto ddSiftingUpOutOfMem;
1650         move->x = x;
1651         move->y = y;
1652         move->size = size;
1653         move->next = moves;
1654         moves = move;
1655         if ((double) size > (double) limitSize * table->maxGrowth) break;
1656         if (size < limitSize) limitSize = size;
1657         y = x;
1658         x = cuddNextLow(table,y);
1659     }
1660     return(moves);
1661
1662 ddSiftingUpOutOfMem:
1663     while (moves != NULL) {
1664         move = moves->next;
1665         cuddDeallocMove(table, moves);
1666         moves = move;
1667     }
1668     return((Move *) CUDD_OUT_OF_MEM);
1669
1670 } /* end of ddSiftingUp */
1671
1672
1673 /**Function********************************************************************
1674
1675   Synopsis    [Sifts a variable down.]
1676
1677   Description [Sifts a variable down. Moves x down until either it
1678   reaches the bound (xHigh) or the size of the DD heap increases too
1679   much. Returns the set of moves in case of success; NULL if memory is
1680   full.]
1681
1682   SideEffects [None]
1683
1684 ******************************************************************************/
1685 static Move *
1686 ddSiftingDown(
1687   DdManager * table,
1688   int  x,
1689   int  xHigh)
1690 {
1691     Move        *moves;
1692     Move        *move;
1693     int         y;
1694     int         size;
1695     int         R;      /* upper bound on node decrease */
1696     int         limitSize;
1697     int         xindex, yindex;
1698     int         isolated;
1699 #ifdef DD_DEBUG
1700     int         checkR;
1701     int         z;
1702     int         zindex;
1703 #endif
1704
1705     moves = NULL;
1706     /* Initialize R */
1707     xindex = table->invperm[x];
1708     limitSize = size = table->keys - table->isolated;
1709     R = 0;
1710     for (y = xHigh; y > x; y--) {
1711         yindex = table->invperm[y];
1712         if (cuddTestInteract(table,xindex,yindex)) {
1713             isolated = table->vars[yindex]->ref == 1;
1714             R += table->subtables[y].keys - isolated;
1715         }
1716     }
1717
1718     y = cuddNextHigh(table,x);
1719     while (y <= xHigh && size - R < limitSize) {
1720 #ifdef DD_DEBUG
1721         checkR = 0;
1722         for (z = xHigh; z > x; z--) {
1723             zindex = table->invperm[z];
1724             if (cuddTestInteract(table,xindex,zindex)) {
1725                 isolated = table->vars[zindex]->ref == 1;
1726                 checkR += table->subtables[z].keys - isolated;
1727             }
1728         }
1729         assert(R == checkR);
1730 #endif
1731         /* Update upper bound on node decrease. */
1732         yindex = table->invperm[y];
1733         if (cuddTestInteract(table,xindex,yindex)) {
1734             isolated = table->vars[yindex]->ref == 1;
1735             R -= table->subtables[y].keys - isolated;
1736         }
1737         size = cuddSwapInPlace(table,x,y);
1738         if (size == 0) goto ddSiftingDownOutOfMem;
1739         move = (Move *) cuddDynamicAllocNode(table);
1740         if (move == NULL) goto ddSiftingDownOutOfMem;
1741         move->x = x;
1742         move->y = y;
1743         move->size = size;
1744         move->next = moves;
1745         moves = move;
1746         if ((double) size > (double) limitSize * table->maxGrowth) break;
1747         if (size < limitSize) limitSize = size;
1748         x = y;
1749         y = cuddNextHigh(table,x);
1750     }
1751     return(moves);
1752
1753 ddSiftingDownOutOfMem:
1754     while (moves != NULL) {
1755         move = moves->next;
1756         cuddDeallocMove(table, moves);
1757         moves = move;
1758     }
1759     return((Move *) CUDD_OUT_OF_MEM);
1760
1761 } /* end of ddSiftingDown */
1762
1763
1764 /**Function********************************************************************
1765
1766   Synopsis    [Given a set of moves, returns the DD heap to the position
1767   giving the minimum size.]
1768
1769   Description [Given a set of moves, returns the DD heap to the
1770   position giving the minimum size. In case of ties, returns to the
1771   closest position giving the minimum size. Returns 1 in case of
1772   success; 0 otherwise.]
1773
1774   SideEffects [None]
1775
1776 ******************************************************************************/
1777 static int
1778 ddSiftingBackward(
1779   DdManager * table,
1780   int  size,
1781   Move * moves)
1782 {
1783     Move *move;
1784     int res;
1785
1786     for (move = moves; move != NULL; move = move->next) {
1787         if (move->size < size) {
1788             size = move->size;
1789         }
1790     }
1791
1792     for (move = moves; move != NULL; move = move->next) {
1793         if (move->size == size) return(1);
1794         res = cuddSwapInPlace(table,(int)move->x,(int)move->y);
1795         if (!res) return(0);
1796     }
1797
1798     return(1);
1799
1800 } /* end of ddSiftingBackward */
1801
1802
1803 /**Function********************************************************************
1804
1805   Synopsis    [Prepares the DD heap for dynamic reordering.]
1806
1807   Description [Prepares the DD heap for dynamic reordering. Does
1808   garbage collection, to guarantee that there are no dead nodes;
1809   clears the cache, which is invalidated by dynamic reordering; initializes
1810   the number of isolated projection functions; and initializes the
1811   interaction matrix.  Returns 1 in case of success; 0 otherwise.]
1812
1813   SideEffects [None]
1814
1815 ******************************************************************************/
1816 static int
1817 ddReorderPreprocess(
1818   DdManager * table)
1819 {
1820     int i;
1821     int res;
1822
1823     /* Clear the cache. */
1824     cuddCacheFlush(table);
1825     cuddLocalCacheClearAll(table);
1826
1827     /* Eliminate dead nodes. Do not scan the cache again. */
1828     cuddGarbageCollect(table,0);
1829
1830     /* Initialize number of isolated projection functions. */
1831     table->isolated = 0;
1832     for (i = 0; i < table->size; i++) {
1833         if (table->vars[i]->ref == 1) table->isolated++;
1834     }
1835
1836     /* Initialize the interaction matrix. */
1837     res = cuddInitInteract(table);
1838     if (res == 0) return(0);
1839
1840     return(1);
1841
1842 } /* end of ddReorderPreprocess */
1843
1844
1845 /**Function********************************************************************
1846
1847   Synopsis    [Cleans up at the end of reordering.]
1848
1849   Description []
1850
1851   SideEffects [None]
1852
1853 ******************************************************************************/
1854 static int
1855 ddReorderPostprocess(
1856   DdManager * table)
1857 {
1858
1859 #ifdef DD_VERBOSE
1860     (void) fflush(table->out);
1861 #endif
1862
1863     /* Free interaction matrix. */
1864     FREE(table->interact);
1865
1866     return(1);
1867
1868 } /* end of ddReorderPostprocess */
1869
1870
1871 /**Function********************************************************************
1872
1873   Synopsis    [Reorders variables according to a given permutation.]
1874
1875   Description [Reorders variables according to a given permutation.
1876   The i-th permutation array contains the index of the variable that
1877   should be brought to the i-th level. ddShuffle assumes that no
1878   dead nodes are present and that the interaction matrix is properly
1879   initialized.  The reordering is achieved by a series of upward sifts.
1880   Returns 1 if successful; 0 otherwise.]
1881
1882   SideEffects [None]
1883
1884   SeeAlso []
1885
1886 ******************************************************************************/
1887 static int
1888 ddShuffle(
1889   DdManager * table,
1890   int * permutation)
1891 {
1892     int         index;
1893     int         level;
1894     int         position;
1895     int         numvars;
1896     int         result;
1897 #ifdef DD_STATS
1898     long        localTime;
1899     int         initialSize;
1900     int         finalSize;
1901     int         previousSize;
1902 #endif
1903
1904     ddTotalNumberSwapping = 0;
1905 #ifdef DD_STATS
1906     localTime = util_cpu_time();
1907     initialSize = table->keys - table->isolated;
1908     (void) fprintf(table->out,"#:I_SHUFFLE %8d: initial size\n",
1909                    initialSize);
1910     ddTotalNISwaps = 0;
1911 #endif
1912
1913     numvars = table->size;
1914
1915     for (level = 0; level < numvars; level++) {
1916         index = permutation[level];
1917         position = table->perm[index];
1918 #ifdef DD_STATS
1919         previousSize = table->keys - table->isolated;
1920 #endif
1921         result = ddSiftUp(table,position,level);
1922         if (!result) return(0);
1923 #ifdef DD_STATS
1924         if (table->keys < (unsigned) previousSize + table->isolated) {
1925             (void) fprintf(table->out,"-");
1926         } else if (table->keys > (unsigned) previousSize + table->isolated) {
1927             (void) fprintf(table->out,"+");     /* should never happen */
1928         } else {
1929             (void) fprintf(table->out,"=");
1930         }
1931         fflush(table->out);
1932 #endif
1933     }
1934
1935 #ifdef DD_STATS
1936     (void) fprintf(table->out,"\n");
1937     finalSize = table->keys - table->isolated;
1938     (void) fprintf(table->out,"#:F_SHUFFLE %8d: final size\n",finalSize);
1939     (void) fprintf(table->out,"#:T_SHUFFLE %8g: total time (sec)\n",
1940         ((double)(util_cpu_time() - localTime)/1000.0));
1941     (void) fprintf(table->out,"#:N_SHUFFLE %8d: total swaps\n",
1942                    ddTotalNumberSwapping);
1943     (void) fprintf(table->out,"#:M_SHUFFLE %8d: NI swaps\n",ddTotalNISwaps);
1944 #endif
1945
1946     return(1);
1947
1948 } /* end of ddShuffle */
1949
1950
1951 /**Function********************************************************************
1952
1953   Synopsis    [Moves one variable up.]
1954
1955   Description [Takes a variable from position x and sifts it up to
1956   position xLow;  xLow should be less than or equal to x.
1957   Returns 1 if successful; 0 otherwise]
1958
1959   SideEffects [None]
1960
1961   SeeAlso     []
1962
1963 ******************************************************************************/
1964 static int
1965 ddSiftUp(
1966   DdManager * table,
1967   int  x,
1968   int  xLow)
1969 {
1970     int        y;
1971     int        size;
1972
1973     y = cuddNextLow(table,x);
1974     while (y >= xLow) {
1975         size = cuddSwapInPlace(table,y,x);
1976         if (size == 0) {
1977             return(0);
1978         }
1979         x = y;
1980         y = cuddNextLow(table,x);
1981     }
1982     return(1);
1983
1984 } /* end of ddSiftUp */
1985
1986
1987 /**Function********************************************************************
1988
1989   Synopsis    [Fixes the BDD variable group tree after a shuffle.]
1990
1991   Description [Fixes the BDD variable group tree after a
1992   shuffle. Assumes that the order of the variables in a terminal node
1993   has not been changed.]
1994
1995   SideEffects [Changes the BDD variable group tree.]
1996
1997   SeeAlso     []
1998
1999 ******************************************************************************/
2000 static void
2001 bddFixTree(
2002   DdManager * table,
2003   MtrNode * treenode)
2004 {
2005     if (treenode == NULL) return;
2006     treenode->low = ((int) treenode->index < table->size) ?
2007         table->perm[treenode->index] : treenode->index;
2008     if (treenode->child != NULL) {
2009         bddFixTree(table, treenode->child);
2010     }
2011     if (treenode->younger != NULL)
2012         bddFixTree(table, treenode->younger);
2013     if (treenode->parent != NULL && treenode->low < treenode->parent->low) {
2014         treenode->parent->low = treenode->low;
2015         treenode->parent->index = treenode->index;
2016     }
2017     return;
2018
2019 } /* end of bddFixTree */
2020
2021
2022 /**Function********************************************************************
2023
2024   Synopsis    [Updates the BDD variable group tree before a shuffle.]
2025
2026   Description [Updates the BDD variable group tree before a shuffle.
2027   Returns 1 if successful; 0 otherwise.]
2028
2029   SideEffects [Changes the BDD variable group tree.]
2030
2031   SeeAlso     []
2032
2033 ******************************************************************************/
2034 static int
2035 ddUpdateMtrTree(
2036   DdManager * table,
2037   MtrNode * treenode,
2038   int * perm,
2039   int * invperm)
2040 {
2041     unsigned int i, size;
2042     int index, level, minLevel, maxLevel, minIndex;
2043
2044     if (treenode == NULL) return(1);
2045
2046     minLevel = CUDD_MAXINDEX;
2047     maxLevel = 0;
2048     minIndex = -1;
2049     /* i : level */
2050     for (i = treenode->low; i < treenode->low + treenode->size; i++) {
2051         index = table->invperm[i];
2052         level = perm[index];
2053         if (level < minLevel) {
2054             minLevel = level;
2055             minIndex = index;
2056         }
2057         if (level > maxLevel)
2058             maxLevel = level;
2059     }
2060     size = maxLevel - minLevel + 1;
2061     if (minIndex == -1) return(0);
2062     if (size == treenode->size) {
2063         treenode->low = minLevel;
2064         treenode->index = minIndex;
2065     } else {
2066         return(0);
2067     }
2068
2069     if (treenode->child != NULL) {
2070         if (!ddUpdateMtrTree(table, treenode->child, perm, invperm))
2071             return(0);
2072     }
2073     if (treenode->younger != NULL) {
2074         if (!ddUpdateMtrTree(table, treenode->younger, perm, invperm))
2075             return(0);
2076     }
2077     return(1);
2078 }
2079
2080
2081 /**Function********************************************************************
2082
2083   Synopsis    [Checks the BDD variable group tree before a shuffle.]
2084
2085   Description [Checks the BDD variable group tree before a shuffle.
2086   Returns 1 if successful; 0 otherwise.]
2087
2088   SideEffects [Changes the BDD variable group tree.]
2089
2090   SeeAlso     []
2091
2092 ******************************************************************************/
2093 static int
2094 ddCheckPermuation(
2095   DdManager * table,
2096   MtrNode * treenode,
2097   int * perm,
2098   int * invperm)
2099 {
2100     unsigned int i, size;
2101     int index, level, minLevel, maxLevel;
2102
2103     if (treenode == NULL) return(1);
2104
2105     minLevel = table->size;
2106     maxLevel = 0;
2107     /* i : level */
2108     for (i = treenode->low; i < treenode->low + treenode->size; i++) {
2109         index = table->invperm[i];
2110         level = perm[index];
2111         if (level < minLevel)
2112             minLevel = level;
2113         if (level > maxLevel)
2114             maxLevel = level;
2115     }
2116     size = maxLevel - minLevel + 1;
2117     if (size != treenode->size)
2118         return(0);
2119
2120     if (treenode->child != NULL) {
2121         if (!ddCheckPermuation(table, treenode->child, perm, invperm))
2122             return(0);
2123     }
2124     if (treenode->younger != NULL) {
2125         if (!ddCheckPermuation(table, treenode->younger, perm, invperm))
2126             return(0);
2127     }
2128     return(1);
2129 }