distr/cudd/cuddZddSymm.c

   1 /**CFile***********************************************************************
   2
   3   FileName    [cuddZddSymm.c]
   4
   5   PackageName [cudd]
   6
   7   Synopsis    [Functions for symmetry-based ZDD variable reordering.]
   8
   9   Description [External procedures included in this module:
  10                     <ul>
  11                     <li> Cudd_zddSymmProfile()
  12                     </ul>
  13                Internal procedures included in this module:
  14                     <ul>
  15                     <li> cuddZddSymmCheck()
  16                     <li> cuddZddSymmSifting()
  17                     <li> cuddZddSymmSiftingConv()
  18                     </ul>
  19                Static procedures included in this module:
  20                     <ul>
  21                     <li> cuddZddUniqueCompare()
  22                     <li> cuddZddSymmSiftingAux()
  23                     <li> cuddZddSymmSiftingConvAux()
  24                     <li> cuddZddSymmSifting_up()
  25                     <li> cuddZddSymmSifting_down()
  26                     <li> zdd_group_move()
  27                     <li> cuddZddSymmSiftingBackward()
  28                     <li> zdd_group_move_backward()
  29                     </ul>
  30               ]
  31
  32   SeeAlso     [cuddSymmetry.c]
  33
  34   Author      [Hyong-Kyoon Shin, In-Ho Moon]
  35
  36   Copyright   [Copyright (c) 1995-2004, Regents of the University of Colorado
  37
  38   All rights reserved.
  39
  40   Redistribution and use in source and binary forms, with or without
  41   modification, are permitted provided that the following conditions
  42   are met:
  43
  44   Redistributions of source code must retain the above copyright
  45   notice, this list of conditions and the following disclaimer.
  46
  47   Redistributions in binary form must reproduce the above copyright
  48   notice, this list of conditions and the following disclaimer in the
  49   documentation and/or other materials provided with the distribution.
  50
  51   Neither the name of the University of Colorado nor the names of its
  52   contributors may be used to endorse or promote products derived from
  53   this software without specific prior written permission.
  54
  55   THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS
  56   "AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT
  57   LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS
  58   FOR A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE
  59   COPYRIGHT OWNER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT,
  60   INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING,
  61   BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES;
  62   LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER
  63   CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT
  64   LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN
  65   ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE
  66   POSSIBILITY OF SUCH DAMAGE.]
  67
  68 ******************************************************************************/
  69
  70 #include "util.h"
  71 #include "cuddInt.h"
  72
  73 /*---------------------------------------------------------------------------*/
  74 /* Constant declarations                                                     */
  75 /*---------------------------------------------------------------------------*/
  76
  77 #define ZDD_MV_OOM (Move *)1
  78
  79 /*---------------------------------------------------------------------------*/
  80 /* Stucture declarations                                                     */
  81 /*---------------------------------------------------------------------------*/
  82
  83 /*---------------------------------------------------------------------------*/
  84 /* Type declarations                                                         */
  85 /*---------------------------------------------------------------------------*/
  86
  87 /*---------------------------------------------------------------------------*/
  88 /* Variable declarations                                                     */
  89 /*---------------------------------------------------------------------------*/
  90
  91 #ifndef lint
  92 static char rcsid[] DD_UNUSED = "$Id: cuddZddSymm.c,v 1.29 2004/08/13 18:04:54 fabio Exp $";
  93 #endif
  94
  95 extern int      *zdd_entry;
  96
  97 extern int      zddTotalNumberSwapping;
  98
  99 static DdNode   *empty;
 100
 101 /*---------------------------------------------------------------------------*/
 102 /* Macro declarations                                                        */
 103 /*---------------------------------------------------------------------------*/
 104
 105
 106 /**AutomaticStart*************************************************************/
 107
 108 /*---------------------------------------------------------------------------*/
 109 /* Static function prototypes                                                */
 110 /*---------------------------------------------------------------------------*/
 111
 112 static int cuddZddSymmSiftingAux (DdManager *table, int x, int x_low, int x_high);
 113 static int cuddZddSymmSiftingConvAux (DdManager *table, int x, int x_low, int x_high);
 114 static Move * cuddZddSymmSifting_up (DdManager *table, int x, int x_low, int initial_size);
 115 static Move * cuddZddSymmSifting_down (DdManager *table, int x, int x_high, int initial_size);
 116 static int cuddZddSymmSiftingBackward (DdManager *table, Move *moves, int size);
 117 static int zdd_group_move (DdManager *table, int x, int y, Move **moves);
 118 static int zdd_group_move_backward (DdManager *table, int x, int y);
 119 static void cuddZddSymmSummary (DdManager *table, int lower, int upper, int *symvars, int *symgroups);
 120
 121 /**AutomaticEnd***************************************************************/
 122
 123
 124 /*---------------------------------------------------------------------------*/
 125 /* Definition of exported functions                                          */
 126 /*---------------------------------------------------------------------------*/
 127
 128
 129 /**Function********************************************************************
 130
 131   Synopsis [Prints statistics on symmetric ZDD variables.]
 132
 133   Description []
 134
 135   SideEffects [None]
 136
 137   SeeAlso     []
 138
 139 ******************************************************************************/
 140 void
 141 Cudd_zddSymmProfile(
 142   DdManager * table,
 143   int  lower,
 144   int  upper)
 145 {
 146     int         i, x, gbot;
 147     int         TotalSymm = 0;
 148     int         TotalSymmGroups = 0;
 149
 150     for (i = lower; i < upper; i++) {
 151         if (table->subtableZ[i].next != (unsigned) i) {
 152             x = i;
 153             (void) fprintf(table->out,"Group:");
 154             do {
 155                 (void) fprintf(table->out,"  %d", table->invpermZ[x]);
 156                 TotalSymm++;
 157                 gbot = x;
 158                 x = table->subtableZ[x].next;
 159             } while (x != i);
 160             TotalSymmGroups++;
 161 #ifdef DD_DEBUG
 162             assert(table->subtableZ[gbot].next == (unsigned) i);
 163 #endif
 164             i = gbot;
 165             (void) fprintf(table->out,"\n");
 166         }
 167     }
 168     (void) fprintf(table->out,"Total Symmetric = %d\n", TotalSymm);
 169     (void) fprintf(table->out,"Total Groups = %d\n", TotalSymmGroups);
 170
 171 } /* end of Cudd_zddSymmProfile */
 172
 173
 174 /*---------------------------------------------------------------------------*/
 175 /* Definition of internal functions                                          */
 176 /*---------------------------------------------------------------------------*/
 177
 178
 179 /**Function********************************************************************
 180
 181   Synopsis [Checks for symmetry of x and y.]
 182
 183   Description [Checks for symmetry of x and y. Ignores projection
 184   functions, unless they are isolated. Returns 1 in case of
 185   symmetry; 0 otherwise.]
 186
 187   SideEffects [None]
 188
 189   SeeAlso     []
 190
 191 ******************************************************************************/
 192 int
 193 cuddZddSymmCheck(
 194   DdManager * table,
 195   int  x,
 196   int  y)
 197 {
 198     int         i;
 199     DdNode      *f, *f0, *f1, *f01, *f00, *f11, *f10;
 200     int         yindex;
 201     int         xsymmy = 1;
 202     int         xsymmyp = 1;
 203     int         arccount = 0;
 204     int         TotalRefCount = 0;
 205     int         symm_found;
 206
 207     empty = table->zero;
 208
 209     yindex = table->invpermZ[y];
 210     for (i = table->subtableZ[x].slots - 1; i >= 0; i--) {
 211         f = table->subtableZ[x].nodelist[i];
 212         while (f != NULL) {
 213             /* Find f1, f0, f11, f10, f01, f00 */
 214             f1 = cuddT(f);
 215             f0 = cuddE(f);
 216             if ((int) f1->index == yindex) {
 217                 f11 = cuddT(f1);
 218                 f10 = cuddE(f1);
 219                 if (f10 != empty)
 220                     arccount++;
 221             } else {
 222                 if ((int) f0->index != yindex) {
 223                     return(0); /* f bypasses layer y */
 224                 }
 225                 f11 = empty;
 226                 f10 = f1;
 227             }
 228             if ((int) f0->index == yindex) {
 229                 f01 = cuddT(f0);
 230                 f00 = cuddE(f0);
 231                 if (f00 != empty)
 232                     arccount++;
 233             } else {
 234                 f01 = empty;
 235                 f00 = f0;
 236             }
 237             if (f01 != f10)
 238                 xsymmy = 0;
 239             if (f11 != f00)
 240                 xsymmyp = 0;
 241             if ((xsymmy == 0) && (xsymmyp == 0))
 242                 return(0);
 243
 244             f = f->next;
 245         } /* for each element of the collision list */
 246     } /* for each slot of the subtable */
 247
 248     /* Calculate the total reference counts of y
 249     ** whose else arc is not empty.
 250     */
 251     for (i = table->subtableZ[y].slots - 1; i >= 0; i--) {
 252         f = table->subtableZ[y].nodelist[i];
 253         while (f != NIL(DdNode)) {
 254             if (cuddE(f) != empty)
 255                 TotalRefCount += f->ref;
 256             f = f->next;
 257         }
 258     }
 259
 260     symm_found = (arccount == TotalRefCount);
 261 #if defined(DD_DEBUG) && defined(DD_VERBOSE)
 262     if (symm_found) {
 263         int xindex = table->invpermZ[x];
 264         (void) fprintf(table->out,
 265                        "Found symmetry! x =%d\ty = %d\tPos(%d,%d)\n",
 266                        xindex,yindex,x,y);
 267     }
 268 #endif
 269
 270     return(symm_found);
 271
 272 } /* end cuddZddSymmCheck */
 273
 274
 275 /**Function********************************************************************
 276
 277   Synopsis [Symmetric sifting algorithm for ZDDs.]
 278
 279   Description [Symmetric sifting algorithm.
 280   Assumes that no dead nodes are present.
 281     <ol>
 282     <li> Order all the variables according to the number of entries in
 283     each unique subtable.
 284     <li> Sift the variable up and down, remembering each time the total
 285     size of the ZDD heap and grouping variables that are symmetric.
 286     <li> Select the best permutation.
 287     <li> Repeat 3 and 4 for all variables.
 288     </ol>
 289   Returns 1 plus the number of symmetric variables if successful; 0
 290   otherwise.]
 291
 292   SideEffects [None]
 293
 294   SeeAlso     [cuddZddSymmSiftingConv]
 295
 296 ******************************************************************************/
 297 int
 298 cuddZddSymmSifting(
 299   DdManager * table,
 300   int  lower,
 301   int  upper)
 302 {
 303     int         i;
 304     int         *var;
 305     int         nvars;
 306     int         x;
 307     int         result;
 308     int         symvars;
 309     int         symgroups;
 310     int         iteration;
 311 #ifdef DD_STATS
 312     int         previousSize;
 313 #endif
 314
 315     nvars = table->sizeZ;
 316
 317     /* Find order in which to sift variables. */
 318     var = NULL;
 319     zdd_entry = ALLOC(int, nvars);
 320     if (zdd_entry == NULL) {
 321         table->errorCode = CUDD_MEMORY_OUT;
 322         goto cuddZddSymmSiftingOutOfMem;
 323     }
 324     var = ALLOC(int, nvars);
 325     if (var == NULL) {
 326         table->errorCode = CUDD_MEMORY_OUT;
 327         goto cuddZddSymmSiftingOutOfMem;
 328     }
 329
 330     for (i = 0; i < nvars; i++) {
 331         x = table->permZ[i];
 332         zdd_entry[i] = table->subtableZ[x].keys;
 333         var[i] = i;
 334     }
 335
 336     qsort((void *)var, nvars, sizeof(int), (DD_QSFP)cuddZddUniqueCompare);
 337
 338     /* Initialize the symmetry of each subtable to itself. */
 339     for (i = lower; i <= upper; i++)
 340         table->subtableZ[i].next = i;
 341
 342     iteration = ddMin(table->siftMaxVar, nvars);
 343     for (i = 0; i < iteration; i++) {
 344         if (zddTotalNumberSwapping >= table->siftMaxSwap)
 345             break;
 346         x = table->permZ[var[i]];
 347 #ifdef DD_STATS
 348         previousSize = table->keysZ;
 349 #endif
 350         if (x < lower || x > upper) continue;
 351         if (table->subtableZ[x].next == (unsigned) x) {
 352             result = cuddZddSymmSiftingAux(table, x, lower, upper);
 353             if (!result)
 354                 goto cuddZddSymmSiftingOutOfMem;
 355 #ifdef DD_STATS
 356             if (table->keysZ < (unsigned) previousSize) {
 357                 (void) fprintf(table->out,"-");
 358             } else if (table->keysZ > (unsigned) previousSize) {
 359                 (void) fprintf(table->out,"+");
 360 #ifdef DD_VERBOSE
 361                 (void) fprintf(table->out,"\nSize increased from %d to %d while sifting variable %d\n", previousSize, table->keysZ, var[i]);
 362 #endif
 363             } else {
 364                 (void) fprintf(table->out,"=");
 365             }
 366             fflush(table->out);
 367 #endif
 368         }
 369     }
 370
 371     FREE(var);
 372     FREE(zdd_entry);
 373
 374     cuddZddSymmSummary(table, lower, upper, &symvars, &symgroups);
 375
 376 #ifdef DD_STATS
 377     (void) fprintf(table->out,"\n#:S_SIFTING %8d: symmetric variables\n",symvars);
 378     (void) fprintf(table->out,"#:G_SIFTING %8d: symmetric groups\n",symgroups);
 379 #endif
 380
 381     return(1+symvars);
 382
 383 cuddZddSymmSiftingOutOfMem:
 384
 385     if (zdd_entry != NULL)
 386         FREE(zdd_entry);
 387     if (var != NULL)
 388         FREE(var);
 389
 390     return(0);
 391
 392 } /* end of cuddZddSymmSifting */
 393
 394
 395 /**Function********************************************************************
 396
 397   Synopsis [Symmetric sifting to convergence algorithm for ZDDs.]
 398
 399   Description [Symmetric sifting to convergence algorithm for ZDDs.
 400   Assumes that no dead nodes are present.
 401     <ol>
 402     <li> Order all the variables according to the number of entries in
 403     each unique subtable.
 404     <li> Sift the variable up and down, remembering each time the total
 405     size of the ZDD heap and grouping variables that are symmetric.
 406     <li> Select the best permutation.
 407     <li> Repeat 3 and 4 for all variables.
 408     <li> Repeat 1-4 until no further improvement.
 409     </ol>
 410   Returns 1 plus the number of symmetric variables if successful; 0
 411   otherwise.]
 412
 413   SideEffects [None]
 414
 415   SeeAlso     [cuddZddSymmSifting]
 416
 417 ******************************************************************************/
 418 int
 419 cuddZddSymmSiftingConv(
 420   DdManager * table,
 421   int  lower,
 422   int  upper)
 423 {
 424     int         i;
 425     int         *var;
 426     int         nvars;
 427     int         initialSize;
 428     int         x;
 429     int         result;
 430     int         symvars;
 431     int         symgroups;
 432     int         classes;
 433     int         iteration;
 434 #ifdef DD_STATS
 435     int         previousSize;
 436 #endif
 437
 438     initialSize = table->keysZ;
 439
 440     nvars = table->sizeZ;
 441
 442     /* Find order in which to sift variables. */
 443     var = NULL;
 444     zdd_entry = ALLOC(int, nvars);
 445     if (zdd_entry == NULL) {
 446         table->errorCode = CUDD_MEMORY_OUT;
 447         goto cuddZddSymmSiftingConvOutOfMem;
 448     }
 449     var = ALLOC(int, nvars);
 450     if (var == NULL) {
 451         table->errorCode = CUDD_MEMORY_OUT;
 452         goto cuddZddSymmSiftingConvOutOfMem;
 453     }
 454
 455     for (i = 0; i < nvars; i++) {
 456         x = table->permZ[i];
 457         zdd_entry[i] = table->subtableZ[x].keys;
 458         var[i] = i;
 459     }
 460
 461     qsort((void *)var, nvars, sizeof(int), (DD_QSFP)cuddZddUniqueCompare);
 462
 463     /* Initialize the symmetry of each subtable to itself
 464     ** for first pass of converging symmetric sifting.
 465     */
 466     for (i = lower; i <= upper; i++)
 467         table->subtableZ[i].next = i;
 468
 469     iteration = ddMin(table->siftMaxVar, table->sizeZ);
 470     for (i = 0; i < iteration; i++) {
 471         if (zddTotalNumberSwapping >= table->siftMaxSwap)
 472             break;
 473         x = table->permZ[var[i]];
 474         if (x < lower || x > upper) continue;
 475         /* Only sift if not in symmetry group already. */
 476         if (table->subtableZ[x].next == (unsigned) x) {
 477 #ifdef DD_STATS
 478             previousSize = table->keysZ;
 479 #endif
 480             result = cuddZddSymmSiftingAux(table, x, lower, upper);
 481             if (!result)
 482                 goto cuddZddSymmSiftingConvOutOfMem;
 483 #ifdef DD_STATS
 484             if (table->keysZ < (unsigned) previousSize) {
 485                 (void) fprintf(table->out,"-");
 486             } else if (table->keysZ > (unsigned) previousSize) {
 487                 (void) fprintf(table->out,"+");
 488 #ifdef DD_VERBOSE
 489                 (void) fprintf(table->out,"\nSize increased from %d to %d while sifting variable %d\n", previousSize, table->keysZ, var[i]);
 490 #endif
 491             } else {
 492                 (void) fprintf(table->out,"=");
 493             }
 494             fflush(table->out);
 495 #endif
 496         }
 497     }
 498
 499     /* Sifting now until convergence. */
 500     while ((unsigned) initialSize > table->keysZ) {
 501         initialSize = table->keysZ;
 502 #ifdef DD_STATS
 503         (void) fprintf(table->out,"\n");
 504 #endif
 505         /* Here we consider only one representative for each symmetry class. */
 506         for (x = lower, classes = 0; x <= upper; x++, classes++) {
 507             while ((unsigned) x < table->subtableZ[x].next)
 508                 x = table->subtableZ[x].next;
 509             /* Here x is the largest index in a group.
 510             ** Groups consists of adjacent variables.
 511             ** Hence, the next increment of x will move it to a new group.
 512             */
 513             i = table->invpermZ[x];
 514             zdd_entry[i] = table->subtableZ[x].keys;
 515             var[classes] = i;
 516         }
 517
 518         qsort((void *)var,classes,sizeof(int),(DD_QSFP)cuddZddUniqueCompare);
 519
 520         /* Now sift. */
 521         iteration = ddMin(table->siftMaxVar, nvars);
 522         for (i = 0; i < iteration; i++) {
 523             if (zddTotalNumberSwapping >= table->siftMaxSwap)
 524                 break;
 525             x = table->permZ[var[i]];
 526             if ((unsigned) x >= table->subtableZ[x].next) {
 527 #ifdef DD_STATS
 528                 previousSize = table->keysZ;
 529 #endif
 530                 result = cuddZddSymmSiftingConvAux(table, x, lower, upper);
 531                 if (!result)
 532                     goto cuddZddSymmSiftingConvOutOfMem;
 533 #ifdef DD_STATS
 534                 if (table->keysZ < (unsigned) previousSize) {
 535                     (void) fprintf(table->out,"-");
 536                 } else if (table->keysZ > (unsigned) previousSize) {
 537                     (void) fprintf(table->out,"+");
 538 #ifdef DD_VERBOSE
 539                 (void) fprintf(table->out,"\nSize increased from %d to %d while sifting variable %d\n", previousSize, table->keysZ, var[i]);
 540 #endif
 541                 } else {
 542                     (void) fprintf(table->out,"=");
 543                 }
 544                 fflush(table->out);
 545 #endif
 546             }
 547         } /* for */
 548     }
 549
 550     cuddZddSymmSummary(table, lower, upper, &symvars, &symgroups);
 551
 552 #ifdef DD_STATS
 553     (void) fprintf(table->out,"\n#:S_SIFTING %8d: symmetric variables\n",
 554                    symvars);
 555     (void) fprintf(table->out,"#:G_SIFTING %8d: symmetric groups\n",
 556                    symgroups);
 557 #endif
 558
 559     FREE(var);
 560     FREE(zdd_entry);
 561
 562     return(1+symvars);
 563
 564 cuddZddSymmSiftingConvOutOfMem:
 565
 566     if (zdd_entry != NULL)
 567         FREE(zdd_entry);
 568     if (var != NULL)
 569         FREE(var);
 570
 571     return(0);
 572
 573 } /* end of cuddZddSymmSiftingConv */
 574
 575
 576 /*---------------------------------------------------------------------------*/
 577 /* Definition of static functions                                            */
 578 /*---------------------------------------------------------------------------*/
 579
 580
 581 /**Function********************************************************************
 582
 583   Synopsis [Given x_low <= x <= x_high moves x up and down between the
 584   boundaries.]
 585
 586   Description [Given x_low <= x <= x_high moves x up and down between the
 587   boundaries. Finds the best position and does the required changes.
 588   Assumes that x is not part of a symmetry group. Returns 1 if
 589   successful; 0 otherwise.]
 590
 591   SideEffects [None]
 592
 593   SeeAlso     []
 594
 595 ******************************************************************************/
 596 static int
 597 cuddZddSymmSiftingAux(
 598   DdManager * table,
 599   int  x,
 600   int  x_low,
 601   int  x_high)
 602 {
 603     Move *move;
 604     Move *move_up;      /* list of up move */
 605     Move *move_down;    /* list of down move */
 606     int  initial_size;
 607     int  result;
 608     int  i;
 609     int  topbot;        /* index to either top or bottom of symmetry group */
 610     int  init_group_size, final_group_size;
 611
 612     initial_size = table->keysZ;
 613
 614     move_down = NULL;
 615     move_up = NULL;
 616
 617     /* Look for consecutive symmetries above x. */
 618     for (i = x; i > x_low; i--) {
 619         if (!cuddZddSymmCheck(table, i - 1, i))
 620             break;
 621         /* find top of i-1's symmetry */
 622         topbot = table->subtableZ[i - 1].next;
 623         table->subtableZ[i - 1].next = i;
 624         table->subtableZ[x].next = topbot;
 625         /* x is bottom of group so its symmetry is top of i-1's
 626            group */
 627         i = topbot + 1; /* add 1 for i--, new i is top of symm group */
 628     }
 629     /* Look for consecutive symmetries below x. */
 630     for (i = x; i < x_high; i++) {
 631         if (!cuddZddSymmCheck(table, i, i + 1))
 632             break;
 633         /* find bottom of i+1's symm group */
 634         topbot = i + 1;
 635         while ((unsigned) topbot < table->subtableZ[topbot].next)
 636             topbot = table->subtableZ[topbot].next;
 637
 638         table->subtableZ[topbot].next = table->subtableZ[i].next;
 639         table->subtableZ[i].next = i + 1;
 640         i = topbot - 1; /* add 1 for i++,
 641                            new i is bottom of symm group */
 642     }
 643
 644     /* Now x maybe in the middle of a symmetry group. */
 645     if (x == x_low) { /* Sift down */
 646         /* Find bottom of x's symm group */
 647         while ((unsigned) x < table->subtableZ[x].next)
 648             x = table->subtableZ[x].next;
 649
 650         i = table->subtableZ[x].next;
 651         init_group_size = x - i + 1;
 652
 653         move_down = cuddZddSymmSifting_down(table, x, x_high,
 654             initial_size);
 655         /* after that point x --> x_high, unless early term */
 656         if (move_down == ZDD_MV_OOM)
 657             goto cuddZddSymmSiftingAuxOutOfMem;
 658
 659         if (move_down == NULL ||
 660             table->subtableZ[move_down->y].next != move_down->y) {
 661             /* symmetry detected may have to make another complete
 662                pass */
 663             if (move_down != NULL)
 664                 x = move_down->y;
 665             else
 666                 x = table->subtableZ[x].next;
 667             i = x;
 668             while ((unsigned) i < table->subtableZ[i].next) {
 669                 i = table->subtableZ[i].next;
 670             }
 671             final_group_size = i - x + 1;
 672
 673             if (init_group_size == final_group_size) {
 674                 /* No new symmetry groups detected,
 675                    return to best position */
 676                 result = cuddZddSymmSiftingBackward(table,
 677                     move_down, initial_size);
 678             }
 679             else {
 680                 initial_size = table->keysZ;
 681                 move_up = cuddZddSymmSifting_up(table, x, x_low,
 682                     initial_size);
 683                 result = cuddZddSymmSiftingBackward(table, move_up,
 684                     initial_size);
 685             }
 686         }
 687         else {
 688             result = cuddZddSymmSiftingBackward(table, move_down,
 689                 initial_size);
 690             /* move backward and stop at best position */
 691         }
 692         if (!result)
 693             goto cuddZddSymmSiftingAuxOutOfMem;
 694     }
 695     else if (x == x_high) { /* Sift up */
 696         /* Find top of x's symm group */
 697         while ((unsigned) x < table->subtableZ[x].next)
 698             x = table->subtableZ[x].next;
 699         x = table->subtableZ[x].next;
 700
 701         i = x;
 702         while ((unsigned) i < table->subtableZ[i].next) {
 703             i = table->subtableZ[i].next;
 704         }
 705         init_group_size = i - x + 1;
 706
 707         move_up = cuddZddSymmSifting_up(table, x, x_low, initial_size);
 708         /* after that point x --> x_low, unless early term */
 709         if (move_up == ZDD_MV_OOM)
 710             goto cuddZddSymmSiftingAuxOutOfMem;
 711
 712         if (move_up == NULL ||
 713             table->subtableZ[move_up->x].next != move_up->x) {
 714             /* symmetry detected may have to make another complete
 715                 pass */
 716             if (move_up != NULL)
 717                 x = move_up->x;
 718             else {
 719                 while ((unsigned) x < table->subtableZ[x].next)
 720                     x = table->subtableZ[x].next;
 721             }
 722             i = table->subtableZ[x].next;
 723             final_group_size = x - i + 1;
 724
 725             if (init_group_size == final_group_size) {
 726                 /* No new symmetry groups detected,
 727                    return to best position */
 728                 result = cuddZddSymmSiftingBackward(table, move_up,
 729                     initial_size);
 730             }
 731             else {
 732                 initial_size = table->keysZ;
 733                 move_down = cuddZddSymmSifting_down(table, x, x_high,
 734                     initial_size);
 735                 result = cuddZddSymmSiftingBackward(table, move_down,
 736                     initial_size);
 737             }
 738         }
 739         else {
 740             result = cuddZddSymmSiftingBackward(table, move_up,
 741                 initial_size);
 742             /* move backward and stop at best position */
 743         }
 744         if (!result)
 745             goto cuddZddSymmSiftingAuxOutOfMem;
 746     }
 747     else if ((x - x_low) > (x_high - x)) { /* must go down first:
 748                                                 shorter */
 749         /* Find bottom of x's symm group */
 750         while ((unsigned) x < table->subtableZ[x].next)
 751             x = table->subtableZ[x].next;
 752
 753         move_down = cuddZddSymmSifting_down(table, x, x_high,
 754             initial_size);
 755         /* after that point x --> x_high, unless early term */
 756         if (move_down == ZDD_MV_OOM)
 757             goto cuddZddSymmSiftingAuxOutOfMem;
 758
 759         if (move_down != NULL) {
 760             x = move_down->y;
 761         }
 762         else {
 763             x = table->subtableZ[x].next;
 764         }
 765         i = x;
 766         while ((unsigned) i < table->subtableZ[i].next) {
 767             i = table->subtableZ[i].next;
 768         }
 769         init_group_size = i - x + 1;
 770
 771         move_up = cuddZddSymmSifting_up(table, x, x_low, initial_size);
 772         if (move_up == ZDD_MV_OOM)
 773             goto cuddZddSymmSiftingAuxOutOfMem;
 774
 775         if (move_up == NULL ||
 776             table->subtableZ[move_up->x].next != move_up->x) {
 777             /* symmetry detected may have to make another complete
 778                pass */
 779             if (move_up != NULL) {
 780                 x = move_up->x;
 781             }
 782             else {
 783                 while ((unsigned) x < table->subtableZ[x].next)
 784                     x = table->subtableZ[x].next;
 785             }
 786             i = table->subtableZ[x].next;
 787             final_group_size = x - i + 1;
 788
 789             if (init_group_size == final_group_size) {
 790                 /* No new symmetry groups detected,
 791                    return to best position */
 792                 result = cuddZddSymmSiftingBackward(table, move_up,
 793                     initial_size);
 794             }
 795             else {
 796                 while (move_down != NULL) {
 797                     move = move_down->next;
 798                     cuddDeallocMove(table, move_down);
 799                     move_down = move;
 800                 }
 801                 initial_size = table->keysZ;
 802                 move_down = cuddZddSymmSifting_down(table, x, x_high,
 803                     initial_size);
 804                 result = cuddZddSymmSiftingBackward(table, move_down,
 805                     initial_size);
 806             }
 807         }
 808         else {
 809             result = cuddZddSymmSiftingBackward(table, move_up,
 810                 initial_size);
 811             /* move backward and stop at best position */
 812         }
 813         if (!result)
 814             goto cuddZddSymmSiftingAuxOutOfMem;
 815     }
 816     else { /* moving up first:shorter */
 817         /* Find top of x's symmetry group */
 818         while ((unsigned) x < table->subtableZ[x].next)
 819             x = table->subtableZ[x].next;
 820         x = table->subtableZ[x].next;
 821
 822         move_up = cuddZddSymmSifting_up(table, x, x_low, initial_size);
 823         /* after that point x --> x_high, unless early term */
 824         if (move_up == ZDD_MV_OOM)
 825             goto cuddZddSymmSiftingAuxOutOfMem;
 826
 827         if (move_up != NULL) {
 828             x = move_up->x;
 829         }
 830         else {
 831             while ((unsigned) x < table->subtableZ[x].next)
 832                 x = table->subtableZ[x].next;
 833         }
 834         i = table->subtableZ[x].next;
 835         init_group_size = x - i + 1;
 836
 837         move_down = cuddZddSymmSifting_down(table, x, x_high,
 838             initial_size);
 839         if (move_down == ZDD_MV_OOM)
 840             goto cuddZddSymmSiftingAuxOutOfMem;
 841
 842         if (move_down == NULL ||
 843             table->subtableZ[move_down->y].next != move_down->y) {
 844             /* symmetry detected may have to make another complete
 845                pass */
 846             if (move_down != NULL) {
 847                 x = move_down->y;
 848             }
 849             else {
 850                 x = table->subtableZ[x].next;
 851             }
 852             i = x;
 853             while ((unsigned) i < table->subtableZ[i].next) {
 854                 i = table->subtableZ[i].next;
 855             }
 856             final_group_size = i - x + 1;
 857
 858             if (init_group_size == final_group_size) {
 859                 /* No new symmetries detected,
 860                    go back to best position */
 861                 result = cuddZddSymmSiftingBackward(table, move_down,
 862                     initial_size);
 863             }
 864             else {
 865                 while (move_up != NULL) {
 866                     move = move_up->next;
 867                     cuddDeallocMove(table, move_up);
 868                     move_up = move;
 869                 }
 870                 initial_size = table->keysZ;
 871                 move_up = cuddZddSymmSifting_up(table, x, x_low,
 872                     initial_size);
 873                 result = cuddZddSymmSiftingBackward(table, move_up,
 874                     initial_size);
 875             }
 876         }
 877         else {
 878             result = cuddZddSymmSiftingBackward(table, move_down,
 879                 initial_size);
 880             /* move backward and stop at best position */
 881         }
 882         if (!result)
 883             goto cuddZddSymmSiftingAuxOutOfMem;
 884     }
 885
 886     while (move_down != NULL) {
 887         move = move_down->next;
 888         cuddDeallocMove(table, move_down);
 889         move_down = move;
 890     }
 891     while (move_up != NULL) {
 892         move = move_up->next;
 893         cuddDeallocMove(table, move_up);
 894         move_up = move;
 895     }
 896
 897     return(1);
 898
 899 cuddZddSymmSiftingAuxOutOfMem:
 900     if (move_down != ZDD_MV_OOM) {
 901         while (move_down != NULL) {
 902             move = move_down->next;
 903             cuddDeallocMove(table, move_down);
 904             move_down = move;
 905         }
 906     }
 907     if (move_up != ZDD_MV_OOM) {
 908         while (move_up != NULL) {
 909             move = move_up->next;
 910             cuddDeallocMove(table, move_up);
 911             move_up = move;
 912         }
 913     }
 914
 915     return(0);
 916
 917 } /* end of cuddZddSymmSiftingAux */
 918
 919
 920 /**Function********************************************************************
 921
 922   Synopsis [Given x_low <= x <= x_high moves x up and down between the
 923   boundaries.]
 924
 925   Description [Given x_low <= x <= x_high moves x up and down between the
 926   boundaries. Finds the best position and does the required changes.
 927   Assumes that x is either an isolated variable, or it is the bottom of
 928   a symmetry group. All symmetries may not have been found, because of
 929   exceeded growth limit. Returns 1 if successful; 0 otherwise.]
 930
 931   SideEffects [None]
 932
 933   SeeAlso     []
 934
 935 ******************************************************************************/
 936 static int
 937 cuddZddSymmSiftingConvAux(
 938   DdManager * table,
 939   int  x,
 940   int  x_low,
 941   int  x_high)
 942 {
 943     Move        *move;
 944     Move        *move_up;       /* list of up move */
 945     Move        *move_down;     /* list of down move */
 946     int         initial_size;
 947     int         result;
 948     int         i;
 949     int         init_group_size, final_group_size;
 950
 951     initial_size = table->keysZ;
 952
 953     move_down = NULL;
 954     move_up = NULL;
 955
 956     if (x == x_low) { /* Sift down */
 957         i = table->subtableZ[x].next;
 958         init_group_size = x - i + 1;
 959
 960         move_down = cuddZddSymmSifting_down(table, x, x_high,
 961             initial_size);
 962         /* after that point x --> x_high, unless early term */
 963         if (move_down == ZDD_MV_OOM)
 964             goto cuddZddSymmSiftingConvAuxOutOfMem;
 965
 966         if (move_down == NULL ||
 967             table->subtableZ[move_down->y].next != move_down->y) {
 968             /* symmetry detected may have to make another complete
 969                 pass */
 970             if (move_down != NULL)
 971                 x = move_down->y;
 972             else {
 973                 while ((unsigned) x < table->subtableZ[x].next)
 974                     x = table->subtableZ[x].next;
 975                 x = table->subtableZ[x].next;
 976             }
 977             i = x;
 978             while ((unsigned) i < table->subtableZ[i].next) {
 979                 i = table->subtableZ[i].next;
 980             }
 981             final_group_size = i - x + 1;
 982
 983             if (init_group_size == final_group_size) {
 984                 /* No new symmetries detected,
 985                    go back to best position */
 986                 result = cuddZddSymmSiftingBackward(table, move_down,
 987                     initial_size);
 988             }
 989             else {
 990                 initial_size = table->keysZ;
 991                 move_up = cuddZddSymmSifting_up(table, x, x_low,
 992                     initial_size);
 993                 result = cuddZddSymmSiftingBackward(table, move_up,
 994                     initial_size);
 995             }
 996         }
 997         else {
 998             result = cuddZddSymmSiftingBackward(table, move_down,
 999                 initial_size);
1000             /* move backward and stop at best position */
1001         }
1002         if (!result)
1003             goto cuddZddSymmSiftingConvAuxOutOfMem;
1004     }
1005     else if (x == x_high) { /* Sift up */
1006         /* Find top of x's symm group */
1007         while ((unsigned) x < table->subtableZ[x].next)
1008             x = table->subtableZ[x].next;
1009         x = table->subtableZ[x].next;
1010
1011         i = x;
1012         while ((unsigned) i < table->subtableZ[i].next) {
1013             i = table->subtableZ[i].next;
1014         }
1015         init_group_size = i - x + 1;
1016
1017         move_up = cuddZddSymmSifting_up(table, x, x_low, initial_size);
1018         /* after that point x --> x_low, unless early term */
1019         if (move_up == ZDD_MV_OOM)
1020             goto cuddZddSymmSiftingConvAuxOutOfMem;
1021
1022         if (move_up == NULL ||
1023             table->subtableZ[move_up->x].next != move_up->x) {
1024             /* symmetry detected may have to make another complete
1025                pass */
1026             if (move_up != NULL)
1027                 x = move_up->x;
1028             else {
1029                 while ((unsigned) x < table->subtableZ[x].next)
1030                     x = table->subtableZ[x].next;
1031             }
1032             i = table->subtableZ[x].next;
1033             final_group_size = x - i + 1;
1034
1035             if (init_group_size == final_group_size) {
1036                 /* No new symmetry groups detected,
1037                    return to best position */
1038                 result = cuddZddSymmSiftingBackward(table, move_up,
1039                     initial_size);
1040             }
1041             else {
1042                 initial_size = table->keysZ;
1043                 move_down = cuddZddSymmSifting_down(table, x, x_high,
1044                     initial_size);
1045                 result = cuddZddSymmSiftingBackward(table, move_down,
1046                     initial_size);
1047             }
1048         }
1049         else {
1050             result = cuddZddSymmSiftingBackward(table, move_up,
1051                 initial_size);
1052             /* move backward and stop at best position */
1053         }
1054         if (!result)
1055             goto cuddZddSymmSiftingConvAuxOutOfMem;
1056     }
1057     else if ((x - x_low) > (x_high - x)) { /* must go down first:
1058                                                 shorter */
1059         move_down = cuddZddSymmSifting_down(table, x, x_high,
1060             initial_size);
1061         /* after that point x --> x_high */
1062         if (move_down == ZDD_MV_OOM)
1063             goto cuddZddSymmSiftingConvAuxOutOfMem;
1064
1065         if (move_down != NULL) {
1066             x = move_down->y;
1067         }
1068         else {
1069             while ((unsigned) x < table->subtableZ[x].next)
1070                 x = table->subtableZ[x].next;
1071             x = table->subtableZ[x].next;
1072         }
1073         i = x;
1074         while ((unsigned) i < table->subtableZ[i].next) {
1075             i = table->subtableZ[i].next;
1076         }
1077         init_group_size = i - x + 1;
1078
1079         move_up = cuddZddSymmSifting_up(table, x, x_low, initial_size);
1080         if (move_up == ZDD_MV_OOM)
1081             goto cuddZddSymmSiftingConvAuxOutOfMem;
1082
1083         if (move_up == NULL ||
1084             table->subtableZ[move_up->x].next != move_up->x) {
1085             /* symmetry detected may have to make another complete
1086                pass */
1087             if (move_up != NULL) {
1088                 x = move_up->x;
1089             }
1090             else {
1091                 while ((unsigned) x < table->subtableZ[x].next)
1092                     x = table->subtableZ[x].next;
1093             }
1094             i = table->subtableZ[x].next;
1095             final_group_size = x - i + 1;
1096
1097             if (init_group_size == final_group_size) {
1098                 /* No new symmetry groups detected,
1099                    return to best position */
1100                 result = cuddZddSymmSiftingBackward(table, move_up,
1101                     initial_size);
1102             }
1103             else {
1104                 while (move_down != NULL) {
1105                     move = move_down->next;
1106                     cuddDeallocMove(table, move_down);
1107                     move_down = move;
1108                 }
1109                 initial_size = table->keysZ;
1110                 move_down = cuddZddSymmSifting_down(table, x, x_high,
1111                     initial_size);
1112                 result = cuddZddSymmSiftingBackward(table, move_down,
1113                     initial_size);
1114             }
1115         }
1116         else {
1117             result = cuddZddSymmSiftingBackward(table, move_up,
1118                 initial_size);
1119             /* move backward and stop at best position */
1120         }
1121         if (!result)
1122             goto cuddZddSymmSiftingConvAuxOutOfMem;
1123     }
1124     else { /* moving up first:shorter */
1125         /* Find top of x's symmetry group */
1126         x = table->subtableZ[x].next;
1127
1128         move_up = cuddZddSymmSifting_up(table, x, x_low, initial_size);
1129         /* after that point x --> x_high, unless early term */
1130         if (move_up == ZDD_MV_OOM)
1131             goto cuddZddSymmSiftingConvAuxOutOfMem;
1132
1133         if (move_up != NULL) {
1134             x = move_up->x;
1135         }
1136         else {
1137             while ((unsigned) x < table->subtableZ[x].next)
1138                 x = table->subtableZ[x].next;
1139         }
1140         i = table->subtableZ[x].next;
1141         init_group_size = x - i + 1;
1142
1143         move_down = cuddZddSymmSifting_down(table, x, x_high,
1144             initial_size);
1145         if (move_down == ZDD_MV_OOM)
1146             goto cuddZddSymmSiftingConvAuxOutOfMem;
1147
1148         if (move_down == NULL ||
1149             table->subtableZ[move_down->y].next != move_down->y) {
1150             /* symmetry detected may have to make another complete
1151                pass */
1152             if (move_down != NULL) {
1153                 x = move_down->y;
1154             }
1155             else {
1156                 while ((unsigned) x < table->subtableZ[x].next)
1157                     x = table->subtableZ[x].next;
1158                 x = table->subtableZ[x].next;
1159             }
1160             i = x;
1161             while ((unsigned) i < table->subtableZ[i].next) {
1162                 i = table->subtableZ[i].next;
1163             }
1164             final_group_size = i - x + 1;
1165
1166             if (init_group_size == final_group_size) {
1167                 /* No new symmetries detected,
1168                    go back to best position */
1169                 result = cuddZddSymmSiftingBackward(table, move_down,
1170                     initial_size);
1171             }
1172             else {
1173                 while (move_up != NULL) {
1174                     move = move_up->next;
1175                     cuddDeallocMove(table, move_up);
1176                     move_up = move;
1177                 }
1178                 initial_size = table->keysZ;
1179                 move_up = cuddZddSymmSifting_up(table, x, x_low,
1180                     initial_size);
1181                 result = cuddZddSymmSiftingBackward(table, move_up,
1182                     initial_size);
1183             }
1184         }
1185         else {
1186             result = cuddZddSymmSiftingBackward(table, move_down,
1187                 initial_size);
1188             /* move backward and stop at best position */
1189         }
1190         if (!result)
1191             goto cuddZddSymmSiftingConvAuxOutOfMem;
1192     }
1193
1194     while (move_down != NULL) {
1195         move = move_down->next;
1196         cuddDeallocMove(table, move_down);
1197         move_down = move;
1198     }
1199     while (move_up != NULL) {
1200         move = move_up->next;
1201         cuddDeallocMove(table, move_up);
1202         move_up = move;
1203     }
1204
1205     return(1);
1206
1207 cuddZddSymmSiftingConvAuxOutOfMem:
1208     if (move_down != ZDD_MV_OOM) {
1209         while (move_down != NULL) {
1210             move = move_down->next;
1211             cuddDeallocMove(table, move_down);
1212             move_down = move;
1213         }
1214     }
1215     if (move_up != ZDD_MV_OOM) {
1216         while (move_up != NULL) {
1217             move = move_up->next;
1218             cuddDeallocMove(table, move_up);
1219             move_up = move;
1220         }
1221     }
1222
1223     return(0);
1224
1225 } /* end of cuddZddSymmSiftingConvAux */
1226
1227
1228 /**Function********************************************************************
1229
1230   Synopsis [Moves x up until either it reaches the bound (x_low) or
1231   the size of the ZDD heap increases too much.]
1232
1233   Description [Moves x up until either it reaches the bound (x_low) or
1234   the size of the ZDD heap increases too much. Assumes that x is the top
1235   of a symmetry group.  Checks x for symmetry to the adjacent
1236   variables. If symmetry is found, the symmetry group of x is merged
1237   with the symmetry group of the other variable. Returns the set of
1238   moves in case of success; ZDD_MV_OOM if memory is full.]
1239
1240   SideEffects [None]
1241
1242   SeeAlso     []
1243
1244 ******************************************************************************/
1245 static Move *
1246 cuddZddSymmSifting_up(
1247   DdManager * table,
1248   int  x,
1249   int  x_low,
1250   int  initial_size)
1251 {
1252     Move        *moves;
1253     Move        *move;
1254     int         y;
1255     int         size;
1256     int         limit_size = initial_size;
1257     int         i, gytop;
1258
1259     moves = NULL;
1260     y = cuddZddNextLow(table, x);
1261     while (y >= x_low) {
1262         gytop = table->subtableZ[y].next;
1263         if (cuddZddSymmCheck(table, y, x)) {
1264             /* Symmetry found, attach symm groups */
1265             table->subtableZ[y].next = x;
1266             i = table->subtableZ[x].next;
1267             while (table->subtableZ[i].next != (unsigned) x)
1268                 i = table->subtableZ[i].next;
1269             table->subtableZ[i].next = gytop;
1270         }
1271         else if ((table->subtableZ[x].next == (unsigned) x) &&
1272             (table->subtableZ[y].next == (unsigned) y)) {
1273             /* x and y have self symmetry */
1274             size = cuddZddSwapInPlace(table, y, x);
1275             if (size == 0)
1276                 goto cuddZddSymmSifting_upOutOfMem;
1277             move = (Move *)cuddDynamicAllocNode(table);
1278             if (move == NULL)
1279                 goto cuddZddSymmSifting_upOutOfMem;
1280             move->x = y;
1281             move->y = x;
1282             move->size = size;
1283             move->next = moves;
1284             moves = move;
1285             if ((double)size >
1286                 (double)limit_size * table->maxGrowth)
1287                 return(moves);
1288             if (size < limit_size)
1289                 limit_size = size;
1290         }
1291         else { /* Group move */
1292             size = zdd_group_move(table, y, x, &moves);
1293             if ((double)size >
1294                 (double)limit_size * table->maxGrowth)
1295                 return(moves);
1296             if (size < limit_size)
1297                 limit_size = size;
1298         }
1299         x = gytop;
1300         y = cuddZddNextLow(table, x);
1301     }
1302
1303     return(moves);
1304
1305 cuddZddSymmSifting_upOutOfMem:
1306     while (moves != NULL) {
1307         move = moves->next;
1308         cuddDeallocMove(table, moves);
1309         moves = move;
1310     }
1311     return(ZDD_MV_OOM);
1312
1313 } /* end of cuddZddSymmSifting_up */
1314
1315
1316 /**Function********************************************************************
1317
1318   Synopsis [Moves x down until either it reaches the bound (x_high) or
1319   the size of the ZDD heap increases too much.]
1320
1321   Description [Moves x down until either it reaches the bound (x_high)
1322   or the size of the ZDD heap increases too much. Assumes that x is the
1323   bottom of a symmetry group. Checks x for symmetry to the adjacent
1324   variables. If symmetry is found, the symmetry group of x is merged
1325   with the symmetry group of the other variable. Returns the set of
1326   moves in case of success; ZDD_MV_OOM if memory is full.]
1327
1328   SideEffects [None]
1329
1330   SeeAlso     []
1331
1332 ******************************************************************************/
1333 static Move *
1334 cuddZddSymmSifting_down(
1335   DdManager * table,
1336   int  x,
1337   int  x_high,
1338   int  initial_size)
1339 {
1340     Move        *moves;
1341     Move        *move;
1342     int         y;
1343     int         size;
1344     int         limit_size = initial_size;
1345     int         i, gxtop, gybot;
1346
1347     moves = NULL;
1348     y = cuddZddNextHigh(table, x);
1349     while (y <= x_high) {
1350         gybot = table->subtableZ[y].next;
1351         while (table->subtableZ[gybot].next != (unsigned) y)
1352             gybot = table->subtableZ[gybot].next;
1353         if (cuddZddSymmCheck(table, x, y)) {
1354             /* Symmetry found, attach symm groups */
1355             gxtop = table->subtableZ[x].next;
1356             table->subtableZ[x].next = y;
1357             i = table->subtableZ[y].next;
1358             while (table->subtableZ[i].next != (unsigned) y)
1359                 i = table->subtableZ[i].next;
1360             table->subtableZ[i].next = gxtop;
1361         }
1362         else if ((table->subtableZ[x].next == (unsigned) x) &&
1363             (table->subtableZ[y].next == (unsigned) y)) {
1364             /* x and y have self symmetry */
1365             size = cuddZddSwapInPlace(table, x, y);
1366             if (size == 0)
1367                 goto cuddZddSymmSifting_downOutOfMem;
1368             move = (Move *)cuddDynamicAllocNode(table);
1369             if (move == NULL)
1370                 goto cuddZddSymmSifting_downOutOfMem;
1371             move->x = x;
1372             move->y = y;
1373             move->size = size;
1374             move->next = moves;
1375             moves = move;
1376             if ((double)size >
1377                 (double)limit_size * table->maxGrowth)
1378                 return(moves);
1379             if (size < limit_size)
1380                 limit_size = size;
1381             x = y;
1382             y = cuddZddNextHigh(table, x);
1383         }
1384         else { /* Group move */
1385             size = zdd_group_move(table, x, y, &moves);
1386             if ((double)size >
1387                 (double)limit_size * table->maxGrowth)
1388                 return(moves);
1389             if (size < limit_size)
1390                 limit_size = size;
1391         }
1392         x = gybot;
1393         y = cuddZddNextHigh(table, x);
1394     }
1395
1396     return(moves);
1397
1398 cuddZddSymmSifting_downOutOfMem:
1399     while (moves != NULL) {
1400         move = moves->next;
1401         cuddDeallocMove(table, moves);
1402         moves = move;
1403     }
1404     return(ZDD_MV_OOM);
1405
1406 } /* end of cuddZddSymmSifting_down */
1407
1408
1409 /**Function********************************************************************
1410
1411   Synopsis [Given a set of moves, returns the ZDD heap to the position
1412   giving the minimum size.]
1413
1414   Description [Given a set of moves, returns the ZDD heap to the
1415   position giving the minimum size. In case of ties, returns to the
1416   closest position giving the minimum size. Returns 1 in case of
1417   success; 0 otherwise.]
1418
1419   SideEffects [None]
1420
1421   SeeAlso     []
1422
1423 ******************************************************************************/
1424 static int
1425 cuddZddSymmSiftingBackward(
1426   DdManager * table,
1427   Move * moves,
1428   int  size)
1429 {
1430     int         i;
1431     int         i_best;
1432     Move        *move;
1433     int         res;
1434
1435     i_best = -1;
1436     for (move = moves, i = 0; move != NULL; move = move->next, i++) {
1437         if (move->size < size) {
1438             i_best = i;
1439             size = move->size;
1440         }
1441     }
1442
1443     for (move = moves, i = 0; move != NULL; move = move->next, i++) {
1444         if (i == i_best) break;
1445         if ((table->subtableZ[move->x].next == move->x) &&
1446             (table->subtableZ[move->y].next == move->y)) {
1447             res = cuddZddSwapInPlace(table, move->x, move->y);
1448             if (!res) return(0);
1449         }
1450         else { /* Group move necessary */
1451             res = zdd_group_move_backward(table, move->x, move->y);
1452         }
1453         if (i_best == -1 && res == size)
1454             break;
1455     }
1456
1457     return(1);
1458
1459 } /* end of cuddZddSymmSiftingBackward */
1460
1461
1462 /**Function********************************************************************
1463
1464   Synopsis [Swaps two groups.]
1465
1466   Description [Swaps two groups. x is assumed to be the bottom variable
1467   of the first group. y is assumed to be the top variable of the second
1468   group.  Updates the list of moves. Returns the number of keys in the
1469   table if successful; 0 otherwise.]
1470
1471   SideEffects [None]
1472
1473   SeeAlso     []
1474
1475 ******************************************************************************/
1476 static int
1477 zdd_group_move(
1478   DdManager * table,
1479   int  x,
1480   int  y,
1481   Move ** moves)
1482 {
1483     Move        *move;
1484     int         size;
1485     int         i, temp, gxtop, gxbot, gybot, yprev;
1486     int         swapx, swapy;
1487
1488 #ifdef DD_DEBUG
1489     assert(x < y);      /* we assume that x < y */
1490 #endif
1491     /* Find top and bottom for the two groups. */
1492     gxtop = table->subtableZ[x].next;
1493     gxbot = x;
1494     gybot = table->subtableZ[y].next;
1495     while (table->subtableZ[gybot].next != (unsigned) y)
1496         gybot = table->subtableZ[gybot].next;
1497     yprev = gybot;
1498
1499     while (x <= y) {
1500         while (y > gxtop) {
1501             /* Set correct symmetries. */
1502             temp = table->subtableZ[x].next;
1503             if (temp == x)
1504                 temp = y;
1505             i = gxtop;
1506             for (;;) {
1507                 if (table->subtableZ[i].next == (unsigned) x) {
1508                     table->subtableZ[i].next = y;
1509                     break;
1510                 } else {
1511                     i = table->subtableZ[i].next;
1512                 }
1513             }
1514             if (table->subtableZ[y].next != (unsigned) y) {
1515                 table->subtableZ[x].next = table->subtableZ[y].next;
1516             } else {
1517                 table->subtableZ[x].next = x;
1518             }
1519
1520             if (yprev != y) {
1521                 table->subtableZ[yprev].next = x;
1522             } else {
1523                 yprev = x;
1524             }
1525             table->subtableZ[y].next = temp;
1526
1527             size = cuddZddSwapInPlace(table, x, y);
1528             if (size == 0)
1529                 goto zdd_group_moveOutOfMem;
1530             swapx = x;
1531             swapy = y;
1532             y = x;
1533             x--;
1534         } /* while y > gxtop */
1535
1536         /* Trying to find the next y. */
1537         if (table->subtableZ[y].next <= (unsigned) y) {
1538             gybot = y;
1539         } else {
1540             y = table->subtableZ[y].next;
1541         }
1542
1543         yprev = gxtop;
1544         gxtop++;
1545         gxbot++;
1546         x = gxbot;
1547     } /* while x <= y, end of group movement */
1548     move = (Move *)cuddDynamicAllocNode(table);
1549     if (move == NULL)
1550         goto zdd_group_moveOutOfMem;
1551     move->x = swapx;
1552     move->y = swapy;
1553     move->size = table->keysZ;
1554     move->next = *moves;
1555     *moves = move;
1556
1557     return(table->keysZ);
1558
1559 zdd_group_moveOutOfMem:
1560     while (*moves != NULL) {
1561         move = (*moves)->next;
1562         cuddDeallocMove(table, *moves);
1563         *moves = move;
1564     }
1565     return(0);
1566
1567 } /* end of zdd_group_move */
1568
1569
1570 /**Function********************************************************************
1571
1572   Synopsis [Undoes the swap of two groups.]
1573
1574   Description [Undoes the swap of two groups. x is assumed to be the
1575   bottom variable of the first group. y is assumed to be the top
1576   variable of the second group.  Returns 1 if successful; 0 otherwise.]
1577
1578   SideEffects [None]
1579
1580   SeeAlso     []
1581
1582 ******************************************************************************/
1583 static int
1584 zdd_group_move_backward(
1585   DdManager * table,
1586   int  x,
1587   int  y)
1588 {
1589     int        size;
1590     int        i, temp, gxtop, gxbot, gybot, yprev;
1591
1592 #ifdef DD_DEBUG
1593     assert(x < y);      /* we assume that x < y */
1594 #endif
1595     /* Find top and bottom of the two groups. */
1596     gxtop = table->subtableZ[x].next;
1597     gxbot = x;
1598     gybot = table->subtableZ[y].next;
1599     while (table->subtableZ[gybot].next != (unsigned) y)
1600         gybot = table->subtableZ[gybot].next;
1601     yprev = gybot;
1602
1603     while (x <= y) {
1604         while (y > gxtop) {
1605             /* Set correct symmetries. */
1606             temp = table->subtableZ[x].next;
1607             if (temp == x)
1608                 temp = y;
1609             i = gxtop;
1610             for (;;) {
1611                 if (table->subtableZ[i].next == (unsigned) x) {
1612                     table->subtableZ[i].next = y;
1613                     break;
1614                 } else {
1615                     i = table->subtableZ[i].next;
1616                 }
1617             }
1618             if (table->subtableZ[y].next != (unsigned) y) {
1619                 table->subtableZ[x].next = table->subtableZ[y].next;
1620             } else {
1621                 table->subtableZ[x].next = x;
1622             }
1623
1624             if (yprev != y) {
1625                 table->subtableZ[yprev].next = x;
1626             } else {
1627                 yprev = x;
1628             }
1629             table->subtableZ[y].next = temp;
1630
1631             size = cuddZddSwapInPlace(table, x, y);
1632             if (size == 0)
1633                 return(0);
1634             y = x;
1635             x--;
1636         } /* while y > gxtop */
1637
1638         /* Trying to find the next y. */
1639         if (table->subtableZ[y].next <= (unsigned) y) {
1640             gybot = y;
1641         } else {
1642             y = table->subtableZ[y].next;
1643         }
1644
1645         yprev = gxtop;
1646         gxtop++;
1647         gxbot++;
1648         x = gxbot;
1649     } /* while x <= y, end of group movement backward */
1650
1651     return(size);
1652
1653 } /* end of zdd_group_move_backward */
1654
1655
1656 /**Function********************************************************************
1657
1658   Synopsis    [Counts numbers of symmetric variables and symmetry
1659   groups.]
1660
1661   Description []
1662
1663   SideEffects [None]
1664
1665 ******************************************************************************/
1666 static void
1667 cuddZddSymmSummary(
1668   DdManager * table,
1669   int  lower,
1670   int  upper,
1671   int * symvars,
1672   int * symgroups)
1673 {
1674     int i,x,gbot;
1675     int TotalSymm = 0;
1676     int TotalSymmGroups = 0;
1677
1678     for (i = lower; i <= upper; i++) {
1679         if (table->subtableZ[i].next != (unsigned) i) {
1680             TotalSymmGroups++;
1681             x = i;
1682             do {
1683                 TotalSymm++;
1684                 gbot = x;
1685                 x = table->subtableZ[x].next;
1686             } while (x != i);
1687 #ifdef DD_DEBUG
1688             assert(table->subtableZ[gbot].next == (unsigned) i);
1689 #endif
1690             i = gbot;
1691         }
1692     }
1693     *symvars = TotalSymm;
1694     *symgroups = TotalSymmGroups;
1695
1696     return;
1697
1698 } /* end of cuddZddSymmSummary */
1699