distr/cudd/cuddSymmetry.c

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