distr/cudd/cuddZddGroup.c

   1 /**CFile***********************************************************************
   2
   3   FileName    [cuddZddGroup.c]
   4
   5   PackageName [cudd]
   6
   7   Synopsis    [Functions for ZDD group sifting.]
   8
   9   Description [External procedures included in this file:
  10                 <ul>
  11                 <li> Cudd_MakeZddTreeNode()
  12                 </ul>
  13         Internal procedures included in this file:
  14                 <ul>
  15                 <li> cuddZddTreeSifting()
  16                 </ul>
  17         Static procedures included in this module:
  18                 <ul>
  19                 <li> zddTreeSiftingAux()
  20                 <li> zddCountInternalMtrNodes()
  21                 <li> zddReorderChildren()
  22                 <li> zddFindNodeHiLo()
  23                 <li> zddUniqueCompareGroup()
  24                 <li> zddGroupSifting()
  25                 <li> zddGroupSiftingAux()
  26                 <li> zddGroupSiftingUp()
  27                 <li> zddGroupSiftingDown()
  28                 <li> zddGroupMove()
  29                 <li> zddGroupMoveBackward()
  30                 <li> zddGroupSiftingBackward()
  31                 <li> zddMergeGroups()
  32                 </ul>]
  33
  34   Author      [Fabio Somenzi]
  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 /*---------------------------------------------------------------------------*/
  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: cuddZddGroup.c,v 1.20 2009/02/19 16:25:36 fabio Exp $";
  91 #endif
  92
  93 static  int     *entry;
  94 extern  int     zddTotalNumberSwapping;
  95 #ifdef DD_STATS
  96 static  int     extsymmcalls;
  97 static  int     extsymm;
  98 static  int     secdiffcalls;
  99 static  int     secdiff;
 100 static  int     secdiffmisfire;
 101 #endif
 102 #ifdef DD_DEBUG
 103 static  int     pr = 0; /* flag to enable printing while debugging */
 104                         /* by depositing a 1 into it */
 105 #endif
 106
 107 /*---------------------------------------------------------------------------*/
 108 /* Macro declarations                                                        */
 109 /*---------------------------------------------------------------------------*/
 110
 111 /**AutomaticStart*************************************************************/
 112
 113 /*---------------------------------------------------------------------------*/
 114 /* Static function prototypes                                                */
 115 /*---------------------------------------------------------------------------*/
 116
 117 static int zddTreeSiftingAux (DdManager *table, MtrNode *treenode, Cudd_ReorderingType method);
 118 #ifdef DD_STATS
 119 static int zddCountInternalMtrNodes (DdManager *table, MtrNode *treenode);
 120 #endif
 121 static int zddReorderChildren (DdManager *table, MtrNode *treenode, Cudd_ReorderingType method);
 122 static void zddFindNodeHiLo (DdManager *table, MtrNode *treenode, int *lower, int *upper);
 123 static int zddUniqueCompareGroup (int *ptrX, int *ptrY);
 124 static int zddGroupSifting (DdManager *table, int lower, int upper);
 125 static int zddGroupSiftingAux (DdManager *table, int x, int xLow, int xHigh);
 126 static int zddGroupSiftingUp (DdManager *table, int y, int xLow, Move **moves);
 127 static int zddGroupSiftingDown (DdManager *table, int x, int xHigh, Move **moves);
 128 static int zddGroupMove (DdManager *table, int x, int y, Move **moves);
 129 static int zddGroupMoveBackward (DdManager *table, int x, int y);
 130 static int zddGroupSiftingBackward (DdManager *table, Move *moves, int size);
 131 static void zddMergeGroups (DdManager *table, MtrNode *treenode, int low, int high);
 132
 133 /**AutomaticEnd***************************************************************/
 134
 135
 136 /*---------------------------------------------------------------------------*/
 137 /* Definition of exported functions                                          */
 138 /*---------------------------------------------------------------------------*/
 139
 140
 141 /**Function********************************************************************
 142
 143   Synopsis    [Creates a new ZDD variable group.]
 144
 145   Description [Creates a new ZDD variable group. The group starts at
 146   variable and contains size variables. The parameter low is the index
 147   of the first variable. If the variable already exists, its current
 148   position in the order is known to the manager. If the variable does
 149   not exist yet, the position is assumed to be the same as the index.
 150   The group tree is created if it does not exist yet.
 151   Returns a pointer to the group if successful; NULL otherwise.]
 152
 153   SideEffects [The ZDD variable tree is changed.]
 154
 155   SeeAlso     [Cudd_MakeTreeNode]
 156
 157 ******************************************************************************/
 158 MtrNode *
 159 Cudd_MakeZddTreeNode(
 160   DdManager * dd /* manager */,
 161   unsigned int  low /* index of the first group variable */,
 162   unsigned int  size /* number of variables in the group */,
 163   unsigned int  type /* MTR_DEFAULT or MTR_FIXED */)
 164 {
 165     MtrNode *group;
 166     MtrNode *tree;
 167     unsigned int level;
 168
 169     /* If the variable does not exist yet, the position is assumed to be
 170     ** the same as the index. Therefore, applications that rely on
 171     ** Cudd_bddNewVarAtLevel or Cudd_addNewVarAtLevel to create new
 172     ** variables have to create the variables before they group them.
 173     */
 174     level = (low < (unsigned int) dd->sizeZ) ? dd->permZ[low] : low;
 175
 176     if (level + size - 1> (int) MTR_MAXHIGH)
 177         return(NULL);
 178
 179     /* If the tree does not exist yet, create it. */
 180     tree = dd->treeZ;
 181     if (tree == NULL) {
 182         dd->treeZ = tree = Mtr_InitGroupTree(0, dd->sizeZ);
 183         if (tree == NULL)
 184             return(NULL);
 185         tree->index = dd->invpermZ[0];
 186     }
 187
 188     /* Extend the upper bound of the tree if necessary. This allows the
 189     ** application to create groups even before the variables are created.
 190     */
 191     tree->size = ddMax(tree->size, level + size);
 192
 193     /* Create the group. */
 194     group = Mtr_MakeGroup(tree, level, size, type);
 195     if (group == NULL)
 196         return(NULL);
 197
 198     /* Initialize the index field to the index of the variable currently
 199     ** in position low. This field will be updated by the reordering
 200     ** procedure to provide a handle to the group once it has been moved.
 201     */
 202     group->index = (MtrHalfWord) low;
 203
 204     return(group);
 205
 206 } /* end of Cudd_MakeZddTreeNode */
 207
 208
 209 /*---------------------------------------------------------------------------*/
 210 /* Definition of internal functions                                          */
 211 /*---------------------------------------------------------------------------*/
 212
 213
 214 /**Function********************************************************************
 215
 216   Synopsis    [Tree sifting algorithm for ZDDs.]
 217
 218   Description [Tree sifting algorithm for ZDDs. Assumes that a tree
 219   representing a group hierarchy is passed as a parameter. It then
 220   reorders each group in postorder fashion by calling
 221   zddTreeSiftingAux.  Assumes that no dead nodes are present.  Returns
 222   1 if successful; 0 otherwise.]
 223
 224   SideEffects [None]
 225
 226 ******************************************************************************/
 227 int
 228 cuddZddTreeSifting(
 229   DdManager * table /* DD table */,
 230   Cudd_ReorderingType method /* reordering method for the groups of leaves */)
 231 {
 232     int i;
 233     int nvars;
 234     int result;
 235     int tempTree;
 236
 237     /* If no tree is provided we create a temporary one in which all
 238     ** variables are in a single group. After reordering this tree is
 239     ** destroyed.
 240     */
 241     tempTree = table->treeZ == NULL;
 242     if (tempTree) {
 243         table->treeZ = Mtr_InitGroupTree(0,table->sizeZ);
 244         table->treeZ->index = table->invpermZ[0];
 245     }
 246     nvars = table->sizeZ;
 247
 248 #ifdef DD_DEBUG
 249     if (pr > 0 && !tempTree)
 250         (void) fprintf(table->out,"cuddZddTreeSifting:");
 251     Mtr_PrintGroups(table->treeZ,pr <= 0);
 252 #endif
 253 #if 0
 254     /* Debugging code. */
 255     if (table->tree && table->treeZ) {
 256         (void) fprintf(table->out,"\n");
 257         Mtr_PrintGroups(table->tree, 0);
 258         cuddPrintVarGroups(table,table->tree,0,0);
 259         for (i = 0; i < table->size; i++) {
 260             (void) fprintf(table->out,"%s%d",
 261                            (i == 0) ? "" : ",", table->invperm[i]);
 262         }
 263         (void) fprintf(table->out,"\n");
 264         for (i = 0; i < table->size; i++) {
 265             (void) fprintf(table->out,"%s%d",
 266                            (i == 0) ? "" : ",", table->perm[i]);
 267         }
 268         (void) fprintf(table->out,"\n\n");
 269         Mtr_PrintGroups(table->treeZ,0);
 270         cuddPrintVarGroups(table,table->treeZ,1,0);
 271         for (i = 0; i < table->sizeZ; i++) {
 272             (void) fprintf(table->out,"%s%d",
 273                            (i == 0) ? "" : ",", table->invpermZ[i]);
 274         }
 275         (void) fprintf(table->out,"\n");
 276         for (i = 0; i < table->sizeZ; i++) {
 277             (void) fprintf(table->out,"%s%d",
 278                            (i == 0) ? "" : ",", table->permZ[i]);
 279         }
 280         (void) fprintf(table->out,"\n");
 281     }
 282     /* End of debugging code. */
 283 #endif
 284 #ifdef DD_STATS
 285     extsymmcalls = 0;
 286     extsymm = 0;
 287     secdiffcalls = 0;
 288     secdiff = 0;
 289     secdiffmisfire = 0;
 290
 291     (void) fprintf(table->out,"\n");
 292     if (!tempTree)
 293         (void) fprintf(table->out,"#:IM_NODES  %8d: group tree nodes\n",
 294                        zddCountInternalMtrNodes(table,table->treeZ));
 295 #endif
 296
 297     /* Initialize the group of each subtable to itself. Initially
 298     ** there are no groups. Groups are created according to the tree
 299     ** structure in postorder fashion.
 300     */
 301     for (i = 0; i < nvars; i++)
 302         table->subtableZ[i].next = i;
 303
 304     /* Reorder. */
 305     result = zddTreeSiftingAux(table, table->treeZ, method);
 306
 307 #ifdef DD_STATS         /* print stats */
 308     if (!tempTree && method == CUDD_REORDER_GROUP_SIFT &&
 309         (table->groupcheck == CUDD_GROUP_CHECK7 ||
 310          table->groupcheck == CUDD_GROUP_CHECK5)) {
 311         (void) fprintf(table->out,"\nextsymmcalls = %d\n",extsymmcalls);
 312         (void) fprintf(table->out,"extsymm = %d",extsymm);
 313     }
 314     if (!tempTree && method == CUDD_REORDER_GROUP_SIFT &&
 315         table->groupcheck == CUDD_GROUP_CHECK7) {
 316         (void) fprintf(table->out,"\nsecdiffcalls = %d\n",secdiffcalls);
 317         (void) fprintf(table->out,"secdiff = %d\n",secdiff);
 318         (void) fprintf(table->out,"secdiffmisfire = %d",secdiffmisfire);
 319     }
 320 #endif
 321
 322     if (tempTree)
 323         Cudd_FreeZddTree(table);
 324     return(result);
 325
 326 } /* end of cuddZddTreeSifting */
 327
 328
 329 /*---------------------------------------------------------------------------*/
 330 /* Definition of static functions                                            */
 331 /*---------------------------------------------------------------------------*/
 332
 333
 334 /**Function********************************************************************
 335
 336   Synopsis    [Visits the group tree and reorders each group.]
 337
 338   Description [Recursively visits the group tree and reorders each
 339   group in postorder fashion.  Returns 1 if successful; 0 otherwise.]
 340
 341   SideEffects [None]
 342
 343 ******************************************************************************/
 344 static int
 345 zddTreeSiftingAux(
 346   DdManager * table,
 347   MtrNode * treenode,
 348   Cudd_ReorderingType method)
 349 {
 350     MtrNode  *auxnode;
 351     int res;
 352
 353 #ifdef DD_DEBUG
 354     Mtr_PrintGroups(treenode,1);
 355 #endif
 356
 357     auxnode = treenode;
 358     while (auxnode != NULL) {
 359         if (auxnode->child != NULL) {
 360             if (!zddTreeSiftingAux(table, auxnode->child, method))
 361                 return(0);
 362             res = zddReorderChildren(table, auxnode, CUDD_REORDER_GROUP_SIFT);
 363             if (res == 0)
 364                 return(0);
 365         } else if (auxnode->size > 1) {
 366             if (!zddReorderChildren(table, auxnode, method))
 367                 return(0);
 368         }
 369         auxnode = auxnode->younger;
 370     }
 371
 372     return(1);
 373
 374 } /* end of zddTreeSiftingAux */
 375
 376
 377 #ifdef DD_STATS
 378 /**Function********************************************************************
 379
 380   Synopsis    [Counts the number of internal nodes of the group tree.]
 381
 382   Description [Counts the number of internal nodes of the group tree.
 383   Returns the count.]
 384
 385   SideEffects [None]
 386
 387 ******************************************************************************/
 388 static int
 389 zddCountInternalMtrNodes(
 390   DdManager * table,
 391   MtrNode * treenode)
 392 {
 393     MtrNode *auxnode;
 394     int     count,nodeCount;
 395
 396
 397     nodeCount = 0;
 398     auxnode = treenode;
 399     while (auxnode != NULL) {
 400         if (!(MTR_TEST(auxnode,MTR_TERMINAL))) {
 401             nodeCount++;
 402             count = zddCountInternalMtrNodes(table,auxnode->child);
 403             nodeCount += count;
 404         }
 405         auxnode = auxnode->younger;
 406     }
 407
 408     return(nodeCount);
 409
 410 } /* end of zddCountInternalMtrNodes */
 411 #endif
 412
 413
 414 /**Function********************************************************************
 415
 416   Synopsis    [Reorders the children of a group tree node according to
 417   the options.]
 418
 419   Description [Reorders the children of a group tree node according to
 420   the options. After reordering puts all the variables in the group
 421   and/or its descendents in a single group. This allows hierarchical
 422   reordering.  If the variables in the group do not exist yet, simply
 423   does nothing. Returns 1 if successful; 0 otherwise.]
 424
 425   SideEffects [None]
 426
 427 ******************************************************************************/
 428 static int
 429 zddReorderChildren(
 430   DdManager * table,
 431   MtrNode * treenode,
 432   Cudd_ReorderingType method)
 433 {
 434     int lower;
 435     int upper;
 436     int result;
 437     unsigned int initialSize;
 438
 439     zddFindNodeHiLo(table,treenode,&lower,&upper);
 440     /* If upper == -1 these variables do not exist yet. */
 441     if (upper == -1)
 442         return(1);
 443
 444     if (treenode->flags == MTR_FIXED) {
 445         result = 1;
 446     } else {
 447 #ifdef DD_STATS
 448         (void) fprintf(table->out," ");
 449 #endif
 450         switch (method) {
 451         case CUDD_REORDER_RANDOM:
 452         case CUDD_REORDER_RANDOM_PIVOT:
 453             result = cuddZddSwapping(table,lower,upper,method);
 454             break;
 455         case CUDD_REORDER_SIFT:
 456             result = cuddZddSifting(table,lower,upper);
 457             break;
 458         case CUDD_REORDER_SIFT_CONVERGE:
 459             do {
 460                 initialSize = table->keysZ;
 461                 result = cuddZddSifting(table,lower,upper);
 462                 if (initialSize <= table->keysZ)
 463                     break;
 464 #ifdef DD_STATS
 465                 else
 466                     (void) fprintf(table->out,"\n");
 467 #endif
 468             } while (result != 0);
 469             break;
 470         case CUDD_REORDER_SYMM_SIFT:
 471             result = cuddZddSymmSifting(table,lower,upper);
 472             break;
 473         case CUDD_REORDER_SYMM_SIFT_CONV:
 474             result = cuddZddSymmSiftingConv(table,lower,upper);
 475             break;
 476         case CUDD_REORDER_GROUP_SIFT:
 477             result = zddGroupSifting(table,lower,upper);
 478             break;
 479         case CUDD_REORDER_LINEAR:
 480             result = cuddZddLinearSifting(table,lower,upper);
 481             break;
 482         case CUDD_REORDER_LINEAR_CONVERGE:
 483             do {
 484                 initialSize = table->keysZ;
 485                 result = cuddZddLinearSifting(table,lower,upper);
 486                 if (initialSize <= table->keysZ)
 487                     break;
 488 #ifdef DD_STATS
 489                 else
 490                     (void) fprintf(table->out,"\n");
 491 #endif
 492             } while (result != 0);
 493             break;
 494         default:
 495             return(0);
 496         }
 497     }
 498
 499     /* Create a single group for all the variables that were sifted,
 500     ** so that they will be treated as a single block by successive
 501     ** invocations of zddGroupSifting.
 502     */
 503     zddMergeGroups(table,treenode,lower,upper);
 504
 505 #ifdef DD_DEBUG
 506     if (pr > 0) (void) fprintf(table->out,"zddReorderChildren:");
 507 #endif
 508
 509     return(result);
 510
 511 } /* end of zddReorderChildren */
 512
 513
 514 /**Function********************************************************************
 515
 516   Synopsis    [Finds the lower and upper bounds of the group represented
 517   by treenode.]
 518
 519   Description [Finds the lower and upper bounds of the group represented
 520   by treenode.  The high and low fields of treenode are indices.  From
 521   those we need to derive the current positions, and find maximum and
 522   minimum.]
 523
 524   SideEffects [The bounds are returned as side effects.]
 525
 526   SeeAlso     []
 527
 528 ******************************************************************************/
 529 static void
 530 zddFindNodeHiLo(
 531   DdManager * table,
 532   MtrNode * treenode,
 533   int * lower,
 534   int * upper)
 535 {
 536     int low;
 537     int high;
 538
 539     /* Check whether no variables in this group already exist.
 540     ** If so, return immediately. The calling procedure will know from
 541     ** the values of upper that no reordering is needed.
 542     */
 543     if ((int) treenode->low >= table->sizeZ) {
 544         *lower = table->sizeZ;
 545         *upper = -1;
 546         return;
 547     }
 548
 549     *lower = low = (unsigned int) table->permZ[treenode->index];
 550     high = (int) (low + treenode->size - 1);
 551
 552     if (high >= table->sizeZ) {
 553         /* This is the case of a partially existing group. The aim is to
 554         ** reorder as many variables as safely possible.  If the tree
 555         ** node is terminal, we just reorder the subset of the group
 556         ** that is currently in existence.  If the group has
 557         ** subgroups, then we only reorder those subgroups that are
 558         ** fully instantiated.  This way we avoid breaking up a group.
 559         */
 560         MtrNode *auxnode = treenode->child;
 561         if (auxnode == NULL) {
 562             *upper = (unsigned int) table->sizeZ - 1;
 563         } else {
 564             /* Search the subgroup that strands the table->sizeZ line.
 565             ** If the first group starts at 0 and goes past table->sizeZ
 566             ** upper will get -1, thus correctly signaling that no reordering
 567             ** should take place.
 568             */
 569             while (auxnode != NULL) {
 570                 int thisLower = table->permZ[auxnode->low];
 571                 int thisUpper = thisLower + auxnode->size - 1;
 572                 if (thisUpper >= table->sizeZ && thisLower < table->sizeZ)
 573                     *upper = (unsigned int) thisLower - 1;
 574                 auxnode = auxnode->younger;
 575             }
 576         }
 577     } else {
 578         /* Normal case: All the variables of the group exist. */
 579         *upper = (unsigned int) high;
 580     }
 581
 582 #ifdef DD_DEBUG
 583     /* Make sure that all variables in group are contiguous. */
 584     assert(treenode->size >= *upper - *lower + 1);
 585 #endif
 586
 587     return;
 588
 589 } /* end of zddFindNodeHiLo */
 590
 591
 592 /**Function********************************************************************
 593
 594   Synopsis    [Comparison function used by qsort.]
 595
 596   Description [Comparison function used by qsort to order the variables
 597   according to the number of keys in the subtables.  Returns the
 598   difference in number of keys between the two variables being
 599   compared.]
 600
 601   SideEffects [None]
 602
 603 ******************************************************************************/
 604 static int
 605 zddUniqueCompareGroup(
 606   int * ptrX,
 607   int * ptrY)
 608 {
 609 #if 0
 610     if (entry[*ptrY] == entry[*ptrX]) {
 611         return((*ptrX) - (*ptrY));
 612     }
 613 #endif
 614     return(entry[*ptrY] - entry[*ptrX]);
 615
 616 } /* end of zddUniqueCompareGroup */
 617
 618
 619 /**Function********************************************************************
 620
 621   Synopsis    [Sifts from treenode->low to treenode->high.]
 622
 623   Description [Sifts from treenode->low to treenode->high. If
 624   croupcheck == CUDD_GROUP_CHECK7, it checks for group creation at the
 625   end of the initial sifting. If a group is created, it is then sifted
 626   again. After sifting one variable, the group that contains it is
 627   dissolved.  Returns 1 in case of success; 0 otherwise.]
 628
 629   SideEffects [None]
 630
 631 ******************************************************************************/
 632 static int
 633 zddGroupSifting(
 634   DdManager * table,
 635   int  lower,
 636   int  upper)
 637 {
 638     int         *var;
 639     int         i,j,x,xInit;
 640     int         nvars;
 641     int         classes;
 642     int         result;
 643     int         *sifted;
 644 #ifdef DD_STATS
 645     unsigned    previousSize;
 646 #endif
 647     int         xindex;
 648
 649     nvars = table->sizeZ;
 650
 651     /* Order variables to sift. */
 652     entry = NULL;
 653     sifted = NULL;
 654     var = ALLOC(int,nvars);
 655     if (var == NULL) {
 656         table->errorCode = CUDD_MEMORY_OUT;
 657         goto zddGroupSiftingOutOfMem;
 658     }
 659     entry = ALLOC(int,nvars);
 660     if (entry == NULL) {
 661         table->errorCode = CUDD_MEMORY_OUT;
 662         goto zddGroupSiftingOutOfMem;
 663     }
 664     sifted = ALLOC(int,nvars);
 665     if (sifted == NULL) {
 666         table->errorCode = CUDD_MEMORY_OUT;
 667         goto zddGroupSiftingOutOfMem;
 668     }
 669
 670     /* Here we consider only one representative for each group. */
 671     for (i = 0, classes = 0; i < nvars; i++) {
 672         sifted[i] = 0;
 673         x = table->permZ[i];
 674         if ((unsigned) x >= table->subtableZ[x].next) {
 675             entry[i] = table->subtableZ[x].keys;
 676             var[classes] = i;
 677             classes++;
 678         }
 679     }
 680
 681     qsort((void *)var,classes,sizeof(int),(DD_QSFP)zddUniqueCompareGroup);
 682
 683     /* Now sift. */
 684     for (i = 0; i < ddMin(table->siftMaxVar,classes); i++) {
 685         if (zddTotalNumberSwapping >= table->siftMaxSwap)
 686             break;
 687         xindex = var[i];
 688         if (sifted[xindex] == 1) /* variable already sifted as part of group */
 689             continue;
 690         x = table->permZ[xindex]; /* find current level of this variable */
 691         if (x < lower || x > upper)
 692             continue;
 693 #ifdef DD_STATS
 694         previousSize = table->keysZ;
 695 #endif
 696 #ifdef DD_DEBUG
 697         /* x is bottom of group */
 698         assert((unsigned) x >= table->subtableZ[x].next);
 699 #endif
 700         result = zddGroupSiftingAux(table,x,lower,upper);
 701         if (!result) goto zddGroupSiftingOutOfMem;
 702
 703 #ifdef DD_STATS
 704         if (table->keysZ < previousSize) {
 705             (void) fprintf(table->out,"-");
 706         } else if (table->keysZ > previousSize) {
 707             (void) fprintf(table->out,"+");
 708         } else {
 709             (void) fprintf(table->out,"=");
 710         }
 711         fflush(table->out);
 712 #endif
 713
 714         /* Mark variables in the group just sifted. */
 715         x = table->permZ[xindex];
 716         if ((unsigned) x != table->subtableZ[x].next) {
 717             xInit = x;
 718             do {
 719                 j = table->invpermZ[x];
 720                 sifted[j] = 1;
 721                 x = table->subtableZ[x].next;
 722             } while (x != xInit);
 723         }
 724
 725 #ifdef DD_DEBUG
 726         if (pr > 0) (void) fprintf(table->out,"zddGroupSifting:");
 727 #endif
 728     } /* for */
 729
 730     FREE(sifted);
 731     FREE(var);
 732     FREE(entry);
 733
 734     return(1);
 735
 736 zddGroupSiftingOutOfMem:
 737     if (entry != NULL)  FREE(entry);
 738     if (var != NULL)    FREE(var);
 739     if (sifted != NULL) FREE(sifted);
 740
 741     return(0);
 742
 743 } /* end of zddGroupSifting */
 744
 745
 746 /**Function********************************************************************
 747
 748   Synopsis    [Sifts one variable up and down until it has taken all
 749   positions. Checks for aggregation.]
 750
 751   Description [Sifts one variable up and down until it has taken all
 752   positions. Checks for aggregation. There may be at most two sweeps,
 753   even if the group grows.  Assumes that x is either an isolated
 754   variable, or it is the bottom of a group. All groups may not have
 755   been found. The variable being moved is returned to the best position
 756   seen during sifting.  Returns 1 in case of success; 0 otherwise.]
 757
 758   SideEffects [None]
 759
 760 ******************************************************************************/
 761 static int
 762 zddGroupSiftingAux(
 763   DdManager * table,
 764   int  x,
 765   int  xLow,
 766   int  xHigh)
 767 {
 768     Move *move;
 769     Move *moves;        /* list of moves */
 770     int  initialSize;
 771     int  result;
 772
 773
 774 #ifdef DD_DEBUG
 775     if (pr > 0) (void) fprintf(table->out,"zddGroupSiftingAux from %d to %d\n",xLow,xHigh);
 776     assert((unsigned) x >= table->subtableZ[x].next); /* x is bottom of group */
 777 #endif
 778
 779     initialSize = table->keysZ;
 780     moves = NULL;
 781
 782     if (x == xLow) { /* Sift down */
 783 #ifdef DD_DEBUG
 784         /* x must be a singleton */
 785         assert((unsigned) x == table->subtableZ[x].next);
 786 #endif
 787         if (x == xHigh) return(1);      /* just one variable */
 788
 789         if (!zddGroupSiftingDown(table,x,xHigh,&moves))
 790             goto zddGroupSiftingAuxOutOfMem;
 791         /* at this point x == xHigh, unless early term */
 792
 793         /* move backward and stop at best position */
 794         result = zddGroupSiftingBackward(table,moves,initialSize);
 795 #ifdef DD_DEBUG
 796         assert(table->keysZ <= (unsigned) initialSize);
 797 #endif
 798         if (!result) goto zddGroupSiftingAuxOutOfMem;
 799
 800     } else if (cuddZddNextHigh(table,x) > xHigh) { /* Sift up */
 801 #ifdef DD_DEBUG
 802         /* x is bottom of group */
 803         assert((unsigned) x >= table->subtableZ[x].next);
 804 #endif
 805         /* Find top of x's group */
 806         x = table->subtableZ[x].next;
 807
 808         if (!zddGroupSiftingUp(table,x,xLow,&moves))
 809             goto zddGroupSiftingAuxOutOfMem;
 810         /* at this point x == xLow, unless early term */
 811
 812         /* move backward and stop at best position */
 813         result = zddGroupSiftingBackward(table,moves,initialSize);
 814 #ifdef DD_DEBUG
 815         assert(table->keysZ <= (unsigned) initialSize);
 816 #endif
 817         if (!result) goto zddGroupSiftingAuxOutOfMem;
 818
 819     } else if (x - xLow > xHigh - x) { /* must go down first: shorter */
 820         if (!zddGroupSiftingDown(table,x,xHigh,&moves))
 821             goto zddGroupSiftingAuxOutOfMem;
 822         /* at this point x == xHigh, unless early term */
 823
 824         /* Find top of group */
 825         if (moves) {
 826             x = moves->y;
 827         }
 828         while ((unsigned) x < table->subtableZ[x].next)
 829             x = table->subtableZ[x].next;
 830         x = table->subtableZ[x].next;
 831 #ifdef DD_DEBUG
 832         /* x should be the top of a group */
 833         assert((unsigned) x <= table->subtableZ[x].next);
 834 #endif
 835
 836         if (!zddGroupSiftingUp(table,x,xLow,&moves))
 837             goto zddGroupSiftingAuxOutOfMem;
 838
 839         /* move backward and stop at best position */
 840         result = zddGroupSiftingBackward(table,moves,initialSize);
 841 #ifdef DD_DEBUG
 842         assert(table->keysZ <= (unsigned) initialSize);
 843 #endif
 844         if (!result) goto zddGroupSiftingAuxOutOfMem;
 845
 846     } else { /* moving up first: shorter */
 847         /* Find top of x's group */
 848         x = table->subtableZ[x].next;
 849
 850         if (!zddGroupSiftingUp(table,x,xLow,&moves))
 851             goto zddGroupSiftingAuxOutOfMem;
 852         /* at this point x == xHigh, unless early term */
 853
 854         if (moves) {
 855             x = moves->x;
 856         }
 857         while ((unsigned) x < table->subtableZ[x].next)
 858             x = table->subtableZ[x].next;
 859 #ifdef DD_DEBUG
 860         /* x is bottom of a group */
 861         assert((unsigned) x >= table->subtableZ[x].next);
 862 #endif
 863
 864         if (!zddGroupSiftingDown(table,x,xHigh,&moves))
 865             goto zddGroupSiftingAuxOutOfMem;
 866
 867         /* move backward and stop at best position */
 868         result = zddGroupSiftingBackward(table,moves,initialSize);
 869 #ifdef DD_DEBUG
 870         assert(table->keysZ <= (unsigned) initialSize);
 871 #endif
 872         if (!result) goto zddGroupSiftingAuxOutOfMem;
 873     }
 874
 875     while (moves != NULL) {
 876         move = moves->next;
 877         cuddDeallocMove(table, moves);
 878         moves = move;
 879     }
 880
 881     return(1);
 882
 883 zddGroupSiftingAuxOutOfMem:
 884     while (moves != NULL) {
 885         move = moves->next;
 886         cuddDeallocMove(table, moves);
 887         moves = move;
 888     }
 889
 890     return(0);
 891
 892 } /* end of zddGroupSiftingAux */
 893
 894
 895 /**Function********************************************************************
 896
 897   Synopsis    [Sifts up a variable until either it reaches position xLow
 898   or the size of the DD heap increases too much.]
 899
 900   Description [Sifts up a variable until either it reaches position
 901   xLow or the size of the DD heap increases too much. Assumes that y is
 902   the top of a group (or a singleton).  Checks y for aggregation to the
 903   adjacent variables. Records all the moves that are appended to the
 904   list of moves received as input and returned as a side effect.
 905   Returns 1 in case of success; 0 otherwise.]
 906
 907   SideEffects [None]
 908
 909 ******************************************************************************/
 910 static int
 911 zddGroupSiftingUp(
 912   DdManager * table,
 913   int  y,
 914   int  xLow,
 915   Move ** moves)
 916 {
 917     Move *move;
 918     int  x;
 919     int  size;
 920     int  gxtop;
 921     int  limitSize;
 922
 923     limitSize = table->keysZ;
 924
 925     x = cuddZddNextLow(table,y);
 926     while (x >= xLow) {
 927         gxtop = table->subtableZ[x].next;
 928         if (table->subtableZ[x].next == (unsigned) x &&
 929             table->subtableZ[y].next == (unsigned) y) {
 930             /* x and y are self groups */
 931             size = cuddZddSwapInPlace(table,x,y);
 932 #ifdef DD_DEBUG
 933             assert(table->subtableZ[x].next == (unsigned) x);
 934             assert(table->subtableZ[y].next == (unsigned) y);
 935 #endif
 936             if (size == 0) goto zddGroupSiftingUpOutOfMem;
 937             move = (Move *)cuddDynamicAllocNode(table);
 938             if (move == NULL) goto zddGroupSiftingUpOutOfMem;
 939             move->x = x;
 940             move->y = y;
 941             move->flags = MTR_DEFAULT;
 942             move->size = size;
 943             move->next = *moves;
 944             *moves = move;
 945
 946 #ifdef DD_DEBUG
 947             if (pr > 0) (void) fprintf(table->out,"zddGroupSiftingUp (2 single groups):\n");
 948 #endif
 949             if ((double) size > (double) limitSize * table->maxGrowth)
 950                 return(1);
 951             if (size < limitSize) limitSize = size;
 952         } else { /* group move */
 953             size = zddGroupMove(table,x,y,moves);
 954             if (size == 0) goto zddGroupSiftingUpOutOfMem;
 955             if ((double) size > (double) limitSize * table->maxGrowth)
 956                 return(1);
 957             if (size < limitSize) limitSize = size;
 958         }
 959         y = gxtop;
 960         x = cuddZddNextLow(table,y);
 961     }
 962
 963     return(1);
 964
 965 zddGroupSiftingUpOutOfMem:
 966     while (*moves != NULL) {
 967         move = (*moves)->next;
 968         cuddDeallocMove(table, *moves);
 969         *moves = move;
 970     }
 971     return(0);
 972
 973 } /* end of zddGroupSiftingUp */
 974
 975
 976 /**Function********************************************************************
 977
 978   Synopsis    [Sifts down a variable until it reaches position xHigh.]
 979
 980   Description [Sifts down a variable until it reaches position xHigh.
 981   Assumes that x is the bottom of a group (or a singleton).  Records
 982   all the moves.  Returns 1 in case of success; 0 otherwise.]
 983
 984   SideEffects [None]
 985
 986 ******************************************************************************/
 987 static int
 988 zddGroupSiftingDown(
 989   DdManager * table,
 990   int  x,
 991   int  xHigh,
 992   Move ** moves)
 993 {
 994     Move *move;
 995     int  y;
 996     int  size;
 997     int  limitSize;
 998     int  gybot;
 999
1000
1001     /* Initialize R */
1002     limitSize = size = table->keysZ;
1003     y = cuddZddNextHigh(table,x);
1004     while (y <= xHigh) {
1005         /* Find bottom of y group. */
1006         gybot = table->subtableZ[y].next;
1007         while (table->subtableZ[gybot].next != (unsigned) y)
1008             gybot = table->subtableZ[gybot].next;
1009
1010         if (table->subtableZ[x].next == (unsigned) x &&
1011             table->subtableZ[y].next == (unsigned) y) {
1012             /* x and y are self groups */
1013             size = cuddZddSwapInPlace(table,x,y);
1014 #ifdef DD_DEBUG
1015             assert(table->subtableZ[x].next == (unsigned) x);
1016             assert(table->subtableZ[y].next == (unsigned) y);
1017 #endif
1018             if (size == 0) goto zddGroupSiftingDownOutOfMem;
1019
1020             /* Record move. */
1021             move = (Move *) cuddDynamicAllocNode(table);
1022             if (move == NULL) goto zddGroupSiftingDownOutOfMem;
1023             move->x = x;
1024             move->y = y;
1025             move->flags = MTR_DEFAULT;
1026             move->size = size;
1027             move->next = *moves;
1028             *moves = move;
1029
1030 #ifdef DD_DEBUG
1031             if (pr > 0) (void) fprintf(table->out,"zddGroupSiftingDown (2 single groups):\n");
1032 #endif
1033             if ((double) size > (double) limitSize * table->maxGrowth)
1034                 return(1);
1035             if (size < limitSize) limitSize = size;
1036             x = y;
1037             y = cuddZddNextHigh(table,x);
1038         } else { /* Group move */
1039             size = zddGroupMove(table,x,y,moves);
1040             if (size == 0) goto zddGroupSiftingDownOutOfMem;
1041             if ((double) size > (double) limitSize * table->maxGrowth)
1042                 return(1);
1043             if (size < limitSize) limitSize = size;
1044         }
1045         x = gybot;
1046         y = cuddZddNextHigh(table,x);
1047     }
1048
1049     return(1);
1050
1051 zddGroupSiftingDownOutOfMem:
1052     while (*moves != NULL) {
1053         move = (*moves)->next;
1054         cuddDeallocMove(table, *moves);
1055         *moves = move;
1056     }
1057
1058     return(0);
1059
1060 } /* end of zddGroupSiftingDown */
1061
1062
1063 /**Function********************************************************************
1064
1065   Synopsis    [Swaps two groups and records the move.]
1066
1067   Description [Swaps two groups and records the move. Returns the
1068   number of keys in the DD table in case of success; 0 otherwise.]
1069
1070   SideEffects [None]
1071
1072 ******************************************************************************/
1073 static int
1074 zddGroupMove(
1075   DdManager * table,
1076   int  x,
1077   int  y,
1078   Move ** moves)
1079 {
1080     Move *move;
1081     int  size;
1082     int  i,j,xtop,xbot,xsize,ytop,ybot,ysize,newxtop;
1083     int  swapx,swapy;
1084 #if defined(DD_DEBUG) && defined(DD_VERBOSE)
1085     int  initialSize,bestSize;
1086 #endif
1087
1088 #ifdef DD_DEBUG
1089     /* We assume that x < y */
1090     assert(x < y);
1091 #endif
1092     /* Find top, bottom, and size for the two groups. */
1093     xbot = x;
1094     xtop = table->subtableZ[x].next;
1095     xsize = xbot - xtop + 1;
1096     ybot = y;
1097     while ((unsigned) ybot < table->subtableZ[ybot].next)
1098         ybot = table->subtableZ[ybot].next;
1099     ytop = y;
1100     ysize = ybot - ytop + 1;
1101
1102 #if defined(DD_DEBUG) && defined(DD_VERBOSE)
1103     initialSize = bestSize = table->keysZ;
1104 #endif
1105     /* Sift the variables of the second group up through the first group */
1106     for (i = 1; i <= ysize; i++) {
1107         for (j = 1; j <= xsize; j++) {
1108             size = cuddZddSwapInPlace(table,x,y);
1109             if (size == 0) goto zddGroupMoveOutOfMem;
1110 #if defined(DD_DEBUG) && defined(DD_VERBOSE)
1111             if (size < bestSize)
1112                 bestSize = size;
1113 #endif
1114             swapx = x; swapy = y;
1115             y = x;
1116             x = cuddZddNextLow(table,y);
1117         }
1118         y = ytop + i;
1119         x = cuddZddNextLow(table,y);
1120     }
1121 #if defined(DD_DEBUG) && defined(DD_VERBOSE)
1122     if ((bestSize < initialSize) && (bestSize < size))
1123         (void) fprintf(table->out,"Missed local minimum: initialSize:%d  bestSize:%d  finalSize:%d\n",initialSize,bestSize,size);
1124 #endif
1125
1126     /* fix groups */
1127     y = xtop; /* ytop is now where xtop used to be */
1128     for (i = 0; i < ysize - 1; i++) {
1129         table->subtableZ[y].next = cuddZddNextHigh(table,y);
1130         y = cuddZddNextHigh(table,y);
1131     }
1132     table->subtableZ[y].next = xtop; /* y is bottom of its group, join */
1133                                     /* it to top of its group */
1134     x = cuddZddNextHigh(table,y);
1135     newxtop = x;
1136     for (i = 0; i < xsize - 1; i++) {
1137         table->subtableZ[x].next = cuddZddNextHigh(table,x);
1138         x = cuddZddNextHigh(table,x);
1139     }
1140     table->subtableZ[x].next = newxtop; /* x is bottom of its group, join */
1141                                     /* it to top of its group */
1142 #ifdef DD_DEBUG
1143     if (pr > 0) (void) fprintf(table->out,"zddGroupMove:\n");
1144 #endif
1145
1146     /* Store group move */
1147     move = (Move *) cuddDynamicAllocNode(table);
1148     if (move == NULL) goto zddGroupMoveOutOfMem;
1149     move->x = swapx;
1150     move->y = swapy;
1151     move->flags = MTR_DEFAULT;
1152     move->size = table->keysZ;
1153     move->next = *moves;
1154     *moves = move;
1155
1156     return(table->keysZ);
1157
1158 zddGroupMoveOutOfMem:
1159     while (*moves != NULL) {
1160         move = (*moves)->next;
1161         cuddDeallocMove(table, *moves);
1162         *moves = move;
1163     }
1164     return(0);
1165
1166 } /* end of zddGroupMove */
1167
1168
1169 /**Function********************************************************************
1170
1171   Synopsis    [Undoes the swap two groups.]
1172
1173   Description [Undoes the swap two groups.  Returns 1 in case of
1174   success; 0 otherwise.]
1175
1176   SideEffects [None]
1177
1178 ******************************************************************************/
1179 static int
1180 zddGroupMoveBackward(
1181   DdManager * table,
1182   int  x,
1183   int  y)
1184 {
1185     int size;
1186     int i,j,xtop,xbot,xsize,ytop,ybot,ysize,newxtop;
1187
1188
1189 #ifdef DD_DEBUG
1190     /* We assume that x < y */
1191     assert(x < y);
1192 #endif
1193
1194     /* Find top, bottom, and size for the two groups. */
1195     xbot = x;
1196     xtop = table->subtableZ[x].next;
1197     xsize = xbot - xtop + 1;
1198     ybot = y;
1199     while ((unsigned) ybot < table->subtableZ[ybot].next)
1200         ybot = table->subtableZ[ybot].next;
1201     ytop = y;
1202     ysize = ybot - ytop + 1;
1203
1204     /* Sift the variables of the second group up through the first group */
1205     for (i = 1; i <= ysize; i++) {
1206         for (j = 1; j <= xsize; j++) {
1207             size = cuddZddSwapInPlace(table,x,y);
1208             if (size == 0)
1209                 return(0);
1210             y = x;
1211             x = cuddZddNextLow(table,y);
1212         }
1213         y = ytop + i;
1214         x = cuddZddNextLow(table,y);
1215     }
1216
1217     /* fix groups */
1218     y = xtop;
1219     for (i = 0; i < ysize - 1; i++) {
1220         table->subtableZ[y].next = cuddZddNextHigh(table,y);
1221         y = cuddZddNextHigh(table,y);
1222     }
1223     table->subtableZ[y].next = xtop; /* y is bottom of its group, join */
1224                                     /* to its top */
1225     x = cuddZddNextHigh(table,y);
1226     newxtop = x;
1227     for (i = 0; i < xsize - 1; i++) {
1228         table->subtableZ[x].next = cuddZddNextHigh(table,x);
1229         x = cuddZddNextHigh(table,x);
1230     }
1231     table->subtableZ[x].next = newxtop; /* x is bottom of its group, join */
1232                                     /* to its top */
1233 #ifdef DD_DEBUG
1234     if (pr > 0) (void) fprintf(table->out,"zddGroupMoveBackward:\n");
1235 #endif
1236
1237     return(1);
1238
1239 } /* end of zddGroupMoveBackward */
1240
1241
1242 /**Function********************************************************************
1243
1244   Synopsis    [Determines the best position for a variables and returns
1245   it there.]
1246
1247   Description [Determines the best position for a variables and returns
1248   it there.  Returns 1 in case of success; 0 otherwise.]
1249
1250   SideEffects [None]
1251
1252 ******************************************************************************/
1253 static int
1254 zddGroupSiftingBackward(
1255   DdManager * table,
1256   Move * moves,
1257   int  size)
1258 {
1259     Move *move;
1260     int  res;
1261
1262
1263     for (move = moves; move != NULL; move = move->next) {
1264         if (move->size < size) {
1265             size = move->size;
1266         }
1267     }
1268
1269     for (move = moves; move != NULL; move = move->next) {
1270         if (move->size == size) return(1);
1271         if ((table->subtableZ[move->x].next == move->x) &&
1272         (table->subtableZ[move->y].next == move->y)) {
1273             res = cuddZddSwapInPlace(table,(int)move->x,(int)move->y);
1274             if (!res) return(0);
1275 #ifdef DD_DEBUG
1276             if (pr > 0) (void) fprintf(table->out,"zddGroupSiftingBackward:\n");
1277             assert(table->subtableZ[move->x].next == move->x);
1278             assert(table->subtableZ[move->y].next == move->y);
1279 #endif
1280         } else { /* Group move necessary */
1281             res = zddGroupMoveBackward(table,(int)move->x,(int)move->y);
1282             if (!res) return(0);
1283         }
1284     }
1285
1286     return(1);
1287
1288 } /* end of zddGroupSiftingBackward */
1289
1290
1291 /**Function********************************************************************
1292
1293   Synopsis    [Merges groups in the DD table.]
1294
1295   Description [Creates a single group from low to high and adjusts the
1296   idex field of the tree node.]
1297
1298   SideEffects [None]
1299
1300 ******************************************************************************/
1301 static void
1302 zddMergeGroups(
1303   DdManager * table,
1304   MtrNode * treenode,
1305   int  low,
1306   int  high)
1307 {
1308     int i;
1309     MtrNode *auxnode;
1310     int saveindex;
1311     int newindex;
1312
1313     /* Merge all variables from low to high in one group, unless
1314     ** this is the topmost group. In such a case we do not merge lest
1315     ** we lose the symmetry information. */
1316     if (treenode != table->treeZ) {
1317         for (i = low; i < high; i++)
1318             table->subtableZ[i].next = i+1;
1319         table->subtableZ[high].next = low;
1320     }
1321
1322     /* Adjust the index fields of the tree nodes. If a node is the
1323     ** first child of its parent, then the parent may also need adjustment. */
1324     saveindex = treenode->index;
1325     newindex = table->invpermZ[low];
1326     auxnode = treenode;
1327     do {
1328         auxnode->index = newindex;
1329         if (auxnode->parent == NULL ||
1330                 (int) auxnode->parent->index != saveindex)
1331             break;
1332         auxnode = auxnode->parent;
1333     } while (1);
1334     return;
1335
1336 } /* end of zddMergeGroups */