distr/cudd/cuddWindow.c

   1 /**CFile***********************************************************************
   2
   3   FileName    [cuddWindow.c]
   4
   5   PackageName [cudd]
   6
   7   Synopsis    [Functions for variable reordering by window permutation.]
   8
   9   Description [Internal procedures included in this module:
  10                 <ul>
  11                 <li> cuddWindowReorder()
  12                 </ul>
  13         Static procedures included in this module:
  14                 <ul>
  15                 <li> ddWindow2()
  16                 <li> ddWindowConv2()
  17                 <li> ddPermuteWindow3()
  18                 <li> ddWindow3()
  19                 <li> ddWindowConv3()
  20                 <li> ddPermuteWindow4()
  21                 <li> ddWindow4()
  22                 <li> ddWindowConv4()
  23                 </ul>]
  24
  25   Author      [Fabio Somenzi]
  26
  27   Copyright   [Copyright (c) 1995-2004, Regents of the University of Colorado
  28
  29   All rights reserved.
  30
  31   Redistribution and use in source and binary forms, with or without
  32   modification, are permitted provided that the following conditions
  33   are met:
  34
  35   Redistributions of source code must retain the above copyright
  36   notice, this list of conditions and the following disclaimer.
  37
  38   Redistributions in binary form must reproduce the above copyright
  39   notice, this list of conditions and the following disclaimer in the
  40   documentation and/or other materials provided with the distribution.
  41
  42   Neither the name of the University of Colorado nor the names of its
  43   contributors may be used to endorse or promote products derived from
  44   this software without specific prior written permission.
  45
  46   THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS
  47   "AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT
  48   LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS
  49   FOR A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE
  50   COPYRIGHT OWNER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT,
  51   INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING,
  52   BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES;
  53   LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER
  54   CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT
  55   LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN
  56   ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE
  57   POSSIBILITY OF SUCH DAMAGE.]
  58
  59 ******************************************************************************/
  60
  61 #include "util.h"
  62 #include "cuddInt.h"
  63
  64 /*---------------------------------------------------------------------------*/
  65 /* Constant declarations                                                     */
  66 /*---------------------------------------------------------------------------*/
  67
  68
  69 /*---------------------------------------------------------------------------*/
  70 /* Stucture declarations                                                     */
  71 /*---------------------------------------------------------------------------*/
  72
  73
  74 /*---------------------------------------------------------------------------*/
  75 /* Type declarations                                                         */
  76 /*---------------------------------------------------------------------------*/
  77
  78
  79 /*---------------------------------------------------------------------------*/
  80 /* Variable declarations                                                     */
  81 /*---------------------------------------------------------------------------*/
  82
  83 #ifndef lint
  84 static char rcsid[] DD_UNUSED = "$Id: cuddWindow.c,v 1.14 2009/02/20 02:14:58 fabio Exp $";
  85 #endif
  86
  87 #ifdef DD_STATS
  88 extern  int     ddTotalNumberSwapping;
  89 extern  int     ddTotalNISwaps;
  90 #endif
  91
  92 /*---------------------------------------------------------------------------*/
  93 /* Macro declarations                                                        */
  94 /*---------------------------------------------------------------------------*/
  95
  96
  97 /**AutomaticStart*************************************************************/
  98
  99 /*---------------------------------------------------------------------------*/
 100 /* Static function prototypes                                                */
 101 /*---------------------------------------------------------------------------*/
 102
 103 static int ddWindow2 (DdManager *table, int low, int high);
 104 static int ddWindowConv2 (DdManager *table, int low, int high);
 105 static int ddPermuteWindow3 (DdManager *table, int x);
 106 static int ddWindow3 (DdManager *table, int low, int high);
 107 static int ddWindowConv3 (DdManager *table, int low, int high);
 108 static int ddPermuteWindow4 (DdManager *table, int w);
 109 static int ddWindow4 (DdManager *table, int low, int high);
 110 static int ddWindowConv4 (DdManager *table, int low, int high);
 111
 112 /**AutomaticEnd***************************************************************/
 113
 114
 115 /*---------------------------------------------------------------------------*/
 116 /* Definition of exported functions                                          */
 117 /*---------------------------------------------------------------------------*/
 118
 119 /*---------------------------------------------------------------------------*/
 120 /* Definition of internal functions                                          */
 121 /*---------------------------------------------------------------------------*/
 122
 123
 124 /**Function********************************************************************
 125
 126   Synopsis    [Reorders by applying the method of the sliding window.]
 127
 128   Description [Reorders by applying the method of the sliding window.
 129   Tries all possible permutations to the variables in a window that
 130   slides from low to high. The size of the window is determined by
 131   submethod.  Assumes that no dead nodes are present.  Returns 1 in
 132   case of success; 0 otherwise.]
 133
 134   SideEffects [None]
 135
 136 ******************************************************************************/
 137 int
 138 cuddWindowReorder(
 139   DdManager * table /* DD table */,
 140   int low /* lowest index to reorder */,
 141   int high /* highest index to reorder */,
 142   Cudd_ReorderingType submethod /* window reordering option */)
 143 {
 144
 145     int res;
 146 #ifdef DD_DEBUG
 147     int supposedOpt;
 148 #endif
 149
 150     switch (submethod) {
 151     case CUDD_REORDER_WINDOW2:
 152         res = ddWindow2(table,low,high);
 153         break;
 154     case CUDD_REORDER_WINDOW3:
 155         res = ddWindow3(table,low,high);
 156         break;
 157     case CUDD_REORDER_WINDOW4:
 158         res = ddWindow4(table,low,high);
 159         break;
 160     case CUDD_REORDER_WINDOW2_CONV:
 161         res = ddWindowConv2(table,low,high);
 162         break;
 163     case CUDD_REORDER_WINDOW3_CONV:
 164         res = ddWindowConv3(table,low,high);
 165 #ifdef DD_DEBUG
 166         supposedOpt = table->keys - table->isolated;
 167         res = ddWindow3(table,low,high);
 168         if (table->keys - table->isolated != (unsigned) supposedOpt) {
 169             (void) fprintf(table->err, "Convergence failed! (%d != %d)\n",
 170                            table->keys - table->isolated, supposedOpt);
 171         }
 172 #endif
 173         break;
 174     case CUDD_REORDER_WINDOW4_CONV:
 175         res = ddWindowConv4(table,low,high);
 176 #ifdef DD_DEBUG
 177         supposedOpt = table->keys - table->isolated;
 178         res = ddWindow4(table,low,high);
 179         if (table->keys - table->isolated != (unsigned) supposedOpt) {
 180             (void) fprintf(table->err,"Convergence failed! (%d != %d)\n",
 181                            table->keys - table->isolated, supposedOpt);
 182         }
 183 #endif
 184         break;
 185     default: return(0);
 186     }
 187
 188     return(res);
 189
 190 } /* end of cuddWindowReorder */
 191
 192
 193 /*---------------------------------------------------------------------------*/
 194 /* Definition of static functions                                            */
 195 /*---------------------------------------------------------------------------*/
 196
 197 /**Function********************************************************************
 198
 199   Synopsis    [Reorders by applying a sliding window of width 2.]
 200
 201   Description [Reorders by applying a sliding window of width 2.
 202   Tries both permutations of the variables in a window
 203   that slides from low to high.  Assumes that no dead nodes are
 204   present.  Returns 1 in case of success; 0 otherwise.]
 205
 206   SideEffects [None]
 207
 208 ******************************************************************************/
 209 static int
 210 ddWindow2(
 211   DdManager * table,
 212   int  low,
 213   int  high)
 214 {
 215
 216     int x;
 217     int res;
 218     int size;
 219
 220 #ifdef DD_DEBUG
 221     assert(low >= 0 && high < table->size);
 222 #endif
 223
 224     if (high-low < 1) return(0);
 225
 226     res = table->keys - table->isolated;
 227     for (x = low; x < high; x++) {
 228         size = res;
 229         res = cuddSwapInPlace(table,x,x+1);
 230         if (res == 0) return(0);
 231         if (res >= size) { /* no improvement: undo permutation */
 232             res = cuddSwapInPlace(table,x,x+1);
 233             if (res == 0) return(0);
 234         }
 235 #ifdef DD_STATS
 236         if (res < size) {
 237             (void) fprintf(table->out,"-");
 238         } else {
 239             (void) fprintf(table->out,"=");
 240         }
 241         fflush(table->out);
 242 #endif
 243     }
 244
 245     return(1);
 246
 247 } /* end of ddWindow2 */
 248
 249
 250 /**Function********************************************************************
 251
 252   Synopsis    [Reorders by repeatedly applying a sliding window of width 2.]
 253
 254   Description [Reorders by repeatedly applying a sliding window of width
 255   2. Tries both permutations of the variables in a window
 256   that slides from low to high.  Assumes that no dead nodes are
 257   present.  Uses an event-driven approach to determine convergence.
 258   Returns 1 in case of success; 0 otherwise.]
 259
 260   SideEffects [None]
 261
 262 ******************************************************************************/
 263 static int
 264 ddWindowConv2(
 265   DdManager * table,
 266   int  low,
 267   int  high)
 268 {
 269     int x;
 270     int res;
 271     int nwin;
 272     int newevent;
 273     int *events;
 274     int size;
 275
 276 #ifdef DD_DEBUG
 277     assert(low >= 0 && high < table->size);
 278 #endif
 279
 280     if (high-low < 1) return(ddWindowConv2(table,low,high));
 281
 282     nwin = high-low;
 283     events = ALLOC(int,nwin);
 284     if (events == NULL) {
 285         table->errorCode = CUDD_MEMORY_OUT;
 286         return(0);
 287     }
 288     for (x=0; x<nwin; x++) {
 289         events[x] = 1;
 290     }
 291
 292     res = table->keys - table->isolated;
 293     do {
 294         newevent = 0;
 295         for (x=0; x<nwin; x++) {
 296             if (events[x]) {
 297                 size = res;
 298                 res = cuddSwapInPlace(table,x+low,x+low+1);
 299                 if (res == 0) {
 300                     FREE(events);
 301                     return(0);
 302                 }
 303                 if (res >= size) { /* no improvement: undo permutation */
 304                     res = cuddSwapInPlace(table,x+low,x+low+1);
 305                     if (res == 0) {
 306                         FREE(events);
 307                         return(0);
 308                     }
 309                 }
 310                 if (res < size) {
 311                     if (x < nwin-1)     events[x+1] = 1;
 312                     if (x > 0)          events[x-1] = 1;
 313                     newevent = 1;
 314                 }
 315                 events[x] = 0;
 316 #ifdef DD_STATS
 317                 if (res < size) {
 318                     (void) fprintf(table->out,"-");
 319                 } else {
 320                     (void) fprintf(table->out,"=");
 321                 }
 322                 fflush(table->out);
 323 #endif
 324             }
 325         }
 326 #ifdef DD_STATS
 327         if (newevent) {
 328             (void) fprintf(table->out,"|");
 329             fflush(table->out);
 330         }
 331 #endif
 332     } while (newevent);
 333
 334     FREE(events);
 335
 336     return(1);
 337
 338 } /* end of ddWindowConv3 */
 339
 340
 341 /**Function********************************************************************
 342
 343   Synopsis [Tries all the permutations of the three variables between
 344   x and x+2 and retains the best.]
 345
 346   Description [Tries all the permutations of the three variables between
 347   x and x+2 and retains the best. Assumes that no dead nodes are
 348   present.  Returns the index of the best permutation (1-6) in case of
 349   success; 0 otherwise.Assumes that no dead nodes are present.  Returns
 350   the index of the best permutation (1-6) in case of success; 0
 351   otherwise.]
 352
 353   SideEffects [None]
 354
 355 ******************************************************************************/
 356 static int
 357 ddPermuteWindow3(
 358   DdManager * table,
 359   int  x)
 360 {
 361     int y,z;
 362     int size,sizeNew;
 363     int best;
 364
 365 #ifdef DD_DEBUG
 366     assert(table->dead == 0);
 367     assert(x+2 < table->size);
 368 #endif
 369
 370     size = table->keys - table->isolated;
 371     y = x+1; z = y+1;
 372
 373     /* The permutation pattern is:
 374     ** (x,y)(y,z)
 375     ** repeated three times to get all 3! = 6 permutations.
 376     */
 377 #define ABC 1
 378     best = ABC;
 379
 380 #define BAC 2
 381     sizeNew = cuddSwapInPlace(table,x,y);
 382     if (sizeNew < size) {
 383         if (sizeNew == 0) return(0);
 384         best = BAC;
 385         size = sizeNew;
 386     }
 387 #define BCA 3
 388     sizeNew = cuddSwapInPlace(table,y,z);
 389     if (sizeNew < size) {
 390         if (sizeNew == 0) return(0);
 391         best = BCA;
 392         size = sizeNew;
 393     }
 394 #define CBA 4
 395     sizeNew = cuddSwapInPlace(table,x,y);
 396     if (sizeNew < size) {
 397         if (sizeNew == 0) return(0);
 398         best = CBA;
 399         size = sizeNew;
 400     }
 401 #define CAB 5
 402     sizeNew = cuddSwapInPlace(table,y,z);
 403     if (sizeNew < size) {
 404         if (sizeNew == 0) return(0);
 405         best = CAB;
 406         size = sizeNew;
 407     }
 408 #define ACB 6
 409     sizeNew = cuddSwapInPlace(table,x,y);
 410     if (sizeNew < size) {
 411         if (sizeNew == 0) return(0);
 412         best = ACB;
 413         size = sizeNew;
 414     }
 415
 416     /* Now take the shortest route to the best permuytation.
 417     ** The initial permutation is ACB.
 418     */
 419     switch(best) {
 420     case BCA: if (!cuddSwapInPlace(table,y,z)) return(0);
 421     case CBA: if (!cuddSwapInPlace(table,x,y)) return(0);
 422     case ABC: if (!cuddSwapInPlace(table,y,z)) return(0);
 423     case ACB: break;
 424     case BAC: if (!cuddSwapInPlace(table,y,z)) return(0);
 425     case CAB: if (!cuddSwapInPlace(table,x,y)) return(0);
 426                break;
 427     default: return(0);
 428     }
 429
 430 #ifdef DD_DEBUG
 431     assert(table->keys - table->isolated == (unsigned) size);
 432 #endif
 433
 434     return(best);
 435
 436 } /* end of ddPermuteWindow3 */
 437
 438
 439 /**Function********************************************************************
 440
 441   Synopsis    [Reorders by applying a sliding window of width 3.]
 442
 443   Description [Reorders by applying a sliding window of width 3.
 444   Tries all possible permutations to the variables in a
 445   window that slides from low to high.  Assumes that no dead nodes are
 446   present.  Returns 1 in case of success; 0 otherwise.]
 447
 448   SideEffects [None]
 449
 450 ******************************************************************************/
 451 static int
 452 ddWindow3(
 453   DdManager * table,
 454   int  low,
 455   int  high)
 456 {
 457
 458     int x;
 459     int res;
 460
 461 #ifdef DD_DEBUG
 462     assert(low >= 0 && high < table->size);
 463 #endif
 464
 465     if (high-low < 2) return(ddWindow2(table,low,high));
 466
 467     for (x = low; x+1 < high; x++) {
 468         res = ddPermuteWindow3(table,x);
 469         if (res == 0) return(0);
 470 #ifdef DD_STATS
 471         if (res == ABC) {
 472             (void) fprintf(table->out,"=");
 473         } else {
 474             (void) fprintf(table->out,"-");
 475         }
 476         fflush(table->out);
 477 #endif
 478     }
 479
 480     return(1);
 481
 482 } /* end of ddWindow3 */
 483
 484
 485 /**Function********************************************************************
 486
 487   Synopsis    [Reorders by repeatedly applying a sliding window of width 3.]
 488
 489   Description [Reorders by repeatedly applying a sliding window of width
 490   3. Tries all possible permutations to the variables in a
 491   window that slides from low to high.  Assumes that no dead nodes are
 492   present.  Uses an event-driven approach to determine convergence.
 493   Returns 1 in case of success; 0 otherwise.]
 494
 495   SideEffects [None]
 496
 497 ******************************************************************************/
 498 static int
 499 ddWindowConv3(
 500   DdManager * table,
 501   int  low,
 502   int  high)
 503 {
 504     int x;
 505     int res;
 506     int nwin;
 507     int newevent;
 508     int *events;
 509
 510 #ifdef DD_DEBUG
 511     assert(low >= 0 && high < table->size);
 512 #endif
 513
 514     if (high-low < 2) return(ddWindowConv2(table,low,high));
 515
 516     nwin = high-low-1;
 517     events = ALLOC(int,nwin);
 518     if (events == NULL) {
 519         table->errorCode = CUDD_MEMORY_OUT;
 520         return(0);
 521     }
 522     for (x=0; x<nwin; x++) {
 523         events[x] = 1;
 524     }
 525
 526     do {
 527         newevent = 0;
 528         for (x=0; x<nwin; x++) {
 529             if (events[x]) {
 530                 res = ddPermuteWindow3(table,x+low);
 531                 switch (res) {
 532                 case ABC:
 533                     break;
 534                 case BAC:
 535                     if (x < nwin-1)     events[x+1] = 1;
 536                     if (x > 1)          events[x-2] = 1;
 537                     newevent = 1;
 538                     break;
 539                 case BCA:
 540                 case CBA:
 541                 case CAB:
 542                     if (x < nwin-2)     events[x+2] = 1;
 543                     if (x < nwin-1)     events[x+1] = 1;
 544                     if (x > 0)          events[x-1] = 1;
 545                     if (x > 1)          events[x-2] = 1;
 546                     newevent = 1;
 547                     break;
 548                 case ACB:
 549                     if (x < nwin-2)     events[x+2] = 1;
 550                     if (x > 0)          events[x-1] = 1;
 551                     newevent = 1;
 552                     break;
 553                 default:
 554                     FREE(events);
 555                     return(0);
 556                 }
 557                 events[x] = 0;
 558 #ifdef DD_STATS
 559                 if (res == ABC) {
 560                     (void) fprintf(table->out,"=");
 561                 } else {
 562                     (void) fprintf(table->out,"-");
 563                 }
 564                 fflush(table->out);
 565 #endif
 566             }
 567         }
 568 #ifdef DD_STATS
 569         if (newevent) {
 570             (void) fprintf(table->out,"|");
 571             fflush(table->out);
 572         }
 573 #endif
 574     } while (newevent);
 575
 576     FREE(events);
 577
 578     return(1);
 579
 580 } /* end of ddWindowConv3 */
 581
 582
 583 /**Function********************************************************************
 584
 585   Synopsis [Tries all the permutations of the four variables between w
 586   and w+3 and retains the best.]
 587
 588   Description [Tries all the permutations of the four variables between
 589   w and w+3 and retains the best. Assumes that no dead nodes are
 590   present.  Returns the index of the best permutation (1-24) in case of
 591   success; 0 otherwise.]
 592
 593   SideEffects [None]
 594
 595 ******************************************************************************/
 596 static int
 597 ddPermuteWindow4(
 598   DdManager * table,
 599   int  w)
 600 {
 601     int x,y,z;
 602     int size,sizeNew;
 603     int best;
 604
 605 #ifdef DD_DEBUG
 606     assert(table->dead == 0);
 607     assert(w+3 < table->size);
 608 #endif
 609
 610     size = table->keys - table->isolated;
 611     x = w+1; y = x+1; z = y+1;
 612
 613     /* The permutation pattern is:
 614      * (w,x)(y,z)(w,x)(x,y)
 615      * (y,z)(w,x)(y,z)(x,y)
 616      * repeated three times to get all 4! = 24 permutations.
 617      * This gives a hamiltonian circuit of Cayley's graph.
 618      * The codes to the permutation are assigned in topological order.
 619      * The permutations at lower distance from the final permutation are
 620      * assigned lower codes. This way we can choose, between
 621      * permutations that give the same size, one that requires the minimum
 622      * number of swaps from the final permutation of the hamiltonian circuit.
 623      * There is an exception to this rule: ABCD is given Code 1, to
 624      * avoid oscillation when convergence is sought.
 625      */
 626 #define ABCD 1
 627     best = ABCD;
 628
 629 #define BACD 7
 630     sizeNew = cuddSwapInPlace(table,w,x);
 631     if (sizeNew < size) {
 632         if (sizeNew == 0) return(0);
 633         best = BACD;
 634         size = sizeNew;
 635     }
 636 #define BADC 13
 637     sizeNew = cuddSwapInPlace(table,y,z);
 638     if (sizeNew < size) {
 639         if (sizeNew == 0) return(0);
 640         best = BADC;
 641         size = sizeNew;
 642     }
 643 #define ABDC 8
 644     sizeNew = cuddSwapInPlace(table,w,x);
 645     if (sizeNew < size || (sizeNew == size && ABDC < best)) {
 646         if (sizeNew == 0) return(0);
 647         best = ABDC;
 648         size = sizeNew;
 649     }
 650 #define ADBC 14
 651     sizeNew = cuddSwapInPlace(table,x,y);
 652     if (sizeNew < size) {
 653         if (sizeNew == 0) return(0);
 654         best = ADBC;
 655         size = sizeNew;
 656     }
 657 #define ADCB 9
 658     sizeNew = cuddSwapInPlace(table,y,z);
 659     if (sizeNew < size || (sizeNew == size && ADCB < best)) {
 660         if (sizeNew == 0) return(0);
 661         best = ADCB;
 662         size = sizeNew;
 663     }
 664 #define DACB 15
 665     sizeNew = cuddSwapInPlace(table,w,x);
 666     if (sizeNew < size) {
 667         if (sizeNew == 0) return(0);
 668         best = DACB;
 669         size = sizeNew;
 670     }
 671 #define DABC 20
 672     sizeNew = cuddSwapInPlace(table,y,z);
 673     if (sizeNew < size) {
 674         if (sizeNew == 0) return(0);
 675         best = DABC;
 676         size = sizeNew;
 677     }
 678 #define DBAC 23
 679     sizeNew = cuddSwapInPlace(table,x,y);
 680     if (sizeNew < size) {
 681         if (sizeNew == 0) return(0);
 682         best = DBAC;
 683         size = sizeNew;
 684     }
 685 #define BDAC 19
 686     sizeNew = cuddSwapInPlace(table,w,x);
 687     if (sizeNew < size || (sizeNew == size && BDAC < best)) {
 688         if (sizeNew == 0) return(0);
 689         best = BDAC;
 690         size = sizeNew;
 691     }
 692 #define BDCA 21
 693     sizeNew = cuddSwapInPlace(table,y,z);
 694     if (sizeNew < size || (sizeNew == size && BDCA < best)) {
 695         if (sizeNew == 0) return(0);
 696         best = BDCA;
 697         size = sizeNew;
 698     }
 699 #define DBCA 24
 700     sizeNew = cuddSwapInPlace(table,w,x);
 701     if (sizeNew < size) {
 702         if (sizeNew == 0) return(0);
 703         best = DBCA;
 704         size = sizeNew;
 705     }
 706 #define DCBA 22
 707     sizeNew = cuddSwapInPlace(table,x,y);
 708     if (sizeNew < size || (sizeNew == size && DCBA < best)) {
 709         if (sizeNew == 0) return(0);
 710         best = DCBA;
 711         size = sizeNew;
 712     }
 713 #define DCAB 18
 714     sizeNew = cuddSwapInPlace(table,y,z);
 715     if (sizeNew < size || (sizeNew == size && DCAB < best)) {
 716         if (sizeNew == 0) return(0);
 717         best = DCAB;
 718         size = sizeNew;
 719     }
 720 #define CDAB 12
 721     sizeNew = cuddSwapInPlace(table,w,x);
 722     if (sizeNew < size || (sizeNew == size && CDAB < best)) {
 723         if (sizeNew == 0) return(0);
 724         best = CDAB;
 725         size = sizeNew;
 726     }
 727 #define CDBA 17
 728     sizeNew = cuddSwapInPlace(table,y,z);
 729     if (sizeNew < size || (sizeNew == size && CDBA < best)) {
 730         if (sizeNew == 0) return(0);
 731         best = CDBA;
 732         size = sizeNew;
 733     }
 734 #define CBDA 11
 735     sizeNew = cuddSwapInPlace(table,x,y);
 736     if (sizeNew < size || (sizeNew == size && CBDA < best)) {
 737         if (sizeNew == 0) return(0);
 738         best = CBDA;
 739         size = sizeNew;
 740     }
 741 #define BCDA 16
 742     sizeNew = cuddSwapInPlace(table,w,x);
 743     if (sizeNew < size || (sizeNew == size && BCDA < best)) {
 744         if (sizeNew == 0) return(0);
 745         best = BCDA;
 746         size = sizeNew;
 747     }
 748 #define BCAD 10
 749     sizeNew = cuddSwapInPlace(table,y,z);
 750     if (sizeNew < size || (sizeNew == size && BCAD < best)) {
 751         if (sizeNew == 0) return(0);
 752         best = BCAD;
 753         size = sizeNew;
 754     }
 755 #define CBAD 5
 756     sizeNew = cuddSwapInPlace(table,w,x);
 757     if (sizeNew < size || (sizeNew == size && CBAD < best)) {
 758         if (sizeNew == 0) return(0);
 759         best = CBAD;
 760         size = sizeNew;
 761     }
 762 #define CABD 3
 763     sizeNew = cuddSwapInPlace(table,x,y);
 764     if (sizeNew < size || (sizeNew == size && CABD < best)) {
 765         if (sizeNew == 0) return(0);
 766         best = CABD;
 767         size = sizeNew;
 768     }
 769 #define CADB 6
 770     sizeNew = cuddSwapInPlace(table,y,z);
 771     if (sizeNew < size || (sizeNew == size && CADB < best)) {
 772         if (sizeNew == 0) return(0);
 773         best = CADB;
 774         size = sizeNew;
 775     }
 776 #define ACDB 4
 777     sizeNew = cuddSwapInPlace(table,w,x);
 778     if (sizeNew < size || (sizeNew == size && ACDB < best)) {
 779         if (sizeNew == 0) return(0);
 780         best = ACDB;
 781         size = sizeNew;
 782     }
 783 #define ACBD 2
 784     sizeNew = cuddSwapInPlace(table,y,z);
 785     if (sizeNew < size || (sizeNew == size && ACBD < best)) {
 786         if (sizeNew == 0) return(0);
 787         best = ACBD;
 788         size = sizeNew;
 789     }
 790
 791     /* Now take the shortest route to the best permutation.
 792     ** The initial permutation is ACBD.
 793     */
 794     switch(best) {
 795     case DBCA: if (!cuddSwapInPlace(table,y,z)) return(0);
 796     case BDCA: if (!cuddSwapInPlace(table,x,y)) return(0);
 797     case CDBA: if (!cuddSwapInPlace(table,w,x)) return(0);
 798     case ADBC: if (!cuddSwapInPlace(table,y,z)) return(0);
 799     case ABDC: if (!cuddSwapInPlace(table,x,y)) return(0);
 800     case ACDB: if (!cuddSwapInPlace(table,y,z)) return(0);
 801     case ACBD: break;
 802     case DCBA: if (!cuddSwapInPlace(table,y,z)) return(0);
 803     case BCDA: if (!cuddSwapInPlace(table,x,y)) return(0);
 804     case CBDA: if (!cuddSwapInPlace(table,w,x)) return(0);
 805                if (!cuddSwapInPlace(table,x,y)) return(0);
 806                if (!cuddSwapInPlace(table,y,z)) return(0);
 807                break;
 808     case DBAC: if (!cuddSwapInPlace(table,x,y)) return(0);
 809     case DCAB: if (!cuddSwapInPlace(table,w,x)) return(0);
 810     case DACB: if (!cuddSwapInPlace(table,y,z)) return(0);
 811     case BACD: if (!cuddSwapInPlace(table,x,y)) return(0);
 812     case CABD: if (!cuddSwapInPlace(table,w,x)) return(0);
 813                break;
 814     case DABC: if (!cuddSwapInPlace(table,y,z)) return(0);
 815     case BADC: if (!cuddSwapInPlace(table,x,y)) return(0);
 816     case CADB: if (!cuddSwapInPlace(table,w,x)) return(0);
 817                if (!cuddSwapInPlace(table,y,z)) return(0);
 818                break;
 819     case BDAC: if (!cuddSwapInPlace(table,x,y)) return(0);
 820     case CDAB: if (!cuddSwapInPlace(table,w,x)) return(0);
 821     case ADCB: if (!cuddSwapInPlace(table,y,z)) return(0);
 822     case ABCD: if (!cuddSwapInPlace(table,x,y)) return(0);
 823                break;
 824     case BCAD: if (!cuddSwapInPlace(table,x,y)) return(0);
 825     case CBAD: if (!cuddSwapInPlace(table,w,x)) return(0);
 826                if (!cuddSwapInPlace(table,x,y)) return(0);
 827                break;
 828     default: return(0);
 829     }
 830
 831 #ifdef DD_DEBUG
 832     assert(table->keys - table->isolated == (unsigned) size);
 833 #endif
 834
 835     return(best);
 836
 837 } /* end of ddPermuteWindow4 */
 838
 839
 840 /**Function********************************************************************
 841
 842   Synopsis    [Reorders by applying a sliding window of width 4.]
 843
 844   Description [Reorders by applying a sliding window of width 4.
 845   Tries all possible permutations to the variables in a
 846   window that slides from low to high.  Assumes that no dead nodes are
 847   present.  Returns 1 in case of success; 0 otherwise.]
 848
 849   SideEffects [None]
 850
 851 ******************************************************************************/
 852 static int
 853 ddWindow4(
 854   DdManager * table,
 855   int  low,
 856   int  high)
 857 {
 858
 859     int w;
 860     int res;
 861
 862 #ifdef DD_DEBUG
 863     assert(low >= 0 && high < table->size);
 864 #endif
 865
 866     if (high-low < 3) return(ddWindow3(table,low,high));
 867
 868     for (w = low; w+2 < high; w++) {
 869         res = ddPermuteWindow4(table,w);
 870         if (res == 0) return(0);
 871 #ifdef DD_STATS
 872         if (res == ABCD) {
 873             (void) fprintf(table->out,"=");
 874         } else {
 875             (void) fprintf(table->out,"-");
 876         }
 877         fflush(table->out);
 878 #endif
 879     }
 880
 881     return(1);
 882
 883 } /* end of ddWindow4 */
 884
 885
 886 /**Function********************************************************************
 887
 888   Synopsis    [Reorders by repeatedly applying a sliding window of width 4.]
 889
 890   Description [Reorders by repeatedly applying a sliding window of width
 891   4. Tries all possible permutations to the variables in a
 892   window that slides from low to high.  Assumes that no dead nodes are
 893   present.  Uses an event-driven approach to determine convergence.
 894   Returns 1 in case of success; 0 otherwise.]
 895
 896   SideEffects [None]
 897
 898 ******************************************************************************/
 899 static int
 900 ddWindowConv4(
 901   DdManager * table,
 902   int  low,
 903   int  high)
 904 {
 905     int x;
 906     int res;
 907     int nwin;
 908     int newevent;
 909     int *events;
 910
 911 #ifdef DD_DEBUG
 912     assert(low >= 0 && high < table->size);
 913 #endif
 914
 915     if (high-low < 3) return(ddWindowConv3(table,low,high));
 916
 917     nwin = high-low-2;
 918     events = ALLOC(int,nwin);
 919     if (events == NULL) {
 920         table->errorCode = CUDD_MEMORY_OUT;
 921         return(0);
 922     }
 923     for (x=0; x<nwin; x++) {
 924         events[x] = 1;
 925     }
 926
 927     do {
 928         newevent = 0;
 929         for (x=0; x<nwin; x++) {
 930             if (events[x]) {
 931                 res = ddPermuteWindow4(table,x+low);
 932                 switch (res) {
 933                 case ABCD:
 934                     break;
 935                 case BACD:
 936                     if (x < nwin-1)     events[x+1] = 1;
 937                     if (x > 2)          events[x-3] = 1;
 938                     newevent = 1;
 939                     break;
 940                 case BADC:
 941                     if (x < nwin-3)     events[x+3] = 1;
 942                     if (x < nwin-1)     events[x+1] = 1;
 943                     if (x > 0)          events[x-1] = 1;
 944                     if (x > 2)          events[x-3] = 1;
 945                     newevent = 1;
 946                     break;
 947                 case ABDC:
 948                     if (x < nwin-3)     events[x+3] = 1;
 949                     if (x > 0)          events[x-1] = 1;
 950                     newevent = 1;
 951                     break;
 952                 case ADBC:
 953                 case ADCB:
 954                 case ACDB:
 955                     if (x < nwin-3)     events[x+3] = 1;
 956                     if (x < nwin-2)     events[x+2] = 1;
 957                     if (x > 0)          events[x-1] = 1;
 958                     if (x > 1)          events[x-2] = 1;
 959                     newevent = 1;
 960                     break;
 961                 case DACB:
 962                 case DABC:
 963                 case DBAC:
 964                 case BDAC:
 965                 case BDCA:
 966                 case DBCA:
 967                 case DCBA:
 968                 case DCAB:
 969                 case CDAB:
 970                 case CDBA:
 971                 case CBDA:
 972                 case BCDA:
 973                 case CADB:
 974                     if (x < nwin-3)     events[x+3] = 1;
 975                     if (x < nwin-2)     events[x+2] = 1;
 976                     if (x < nwin-1)     events[x+1] = 1;
 977                     if (x > 0)          events[x-1] = 1;
 978                     if (x > 1)          events[x-2] = 1;
 979                     if (x > 2)          events[x-3] = 1;
 980                     newevent = 1;
 981                     break;
 982                 case BCAD:
 983                 case CBAD:
 984                 case CABD:
 985                     if (x < nwin-2)     events[x+2] = 1;
 986                     if (x < nwin-1)     events[x+1] = 1;
 987                     if (x > 1)          events[x-2] = 1;
 988                     if (x > 2)          events[x-3] = 1;
 989                     newevent = 1;
 990                     break;
 991                 case ACBD:
 992                     if (x < nwin-2)     events[x+2] = 1;
 993                     if (x > 1)          events[x-2] = 1;
 994                     newevent = 1;
 995                     break;
 996                 default:
 997                     FREE(events);
 998                     return(0);
 999                 }
1000                 events[x] = 0;
1001 #ifdef DD_STATS
1002                 if (res == ABCD) {
1003                     (void) fprintf(table->out,"=");
1004                 } else {
1005                     (void) fprintf(table->out,"-");
1006                 }
1007                 fflush(table->out);
1008 #endif
1009             }
1010         }
1011 #ifdef DD_STATS
1012         if (newevent) {
1013             (void) fprintf(table->out,"|");
1014             fflush(table->out);
1015         }
1016 #endif
1017     } while (newevent);
1018
1019     FREE(events);
1020
1021     return(1);
1022
1023 } /* end of ddWindowConv4 */