glu-2.2: src/cuBdd/cuddWindow.c Source File

00001 
00061 #include "util.h"
00062 #include "cuddInt.h"
00063 
00064 /*---------------------------------------------------------------------------*/
00065 /* Constant declarations                                                     */
00066 /*---------------------------------------------------------------------------*/
00067 
00068 
00069 /*---------------------------------------------------------------------------*/
00070 /* Stucture declarations                                                     */
00071 /*---------------------------------------------------------------------------*/
00072 
00073 
00074 /*---------------------------------------------------------------------------*/
00075 /* Type declarations                                                         */
00076 /*---------------------------------------------------------------------------*/
00077 
00078 
00079 /*---------------------------------------------------------------------------*/
00080 /* Variable declarations                                                     */
00081 /*---------------------------------------------------------------------------*/
00082 
00083 #ifndef lint
00084 static char rcsid[] DD_UNUSED = "$Id: cuddWindow.c,v 1.14 2009/02/20 02:14:58 fabio Exp $";
00085 #endif
00086 
00087 #ifdef DD_STATS
00088 extern  int     ddTotalNumberSwapping;
00089 extern  int     ddTotalNISwaps;
00090 #endif
00091 
00092 /*---------------------------------------------------------------------------*/
00093 /* Macro declarations                                                        */
00094 /*---------------------------------------------------------------------------*/
00095 
00096 
00099 /*---------------------------------------------------------------------------*/
00100 /* Static function prototypes                                                */
00101 /*---------------------------------------------------------------------------*/
00102 
00103 static int ddWindow2 (DdManager *table, int low, int high);
00104 static int ddWindowConv2 (DdManager *table, int low, int high);
00105 static int ddPermuteWindow3 (DdManager *table, int x);
00106 static int ddWindow3 (DdManager *table, int low, int high);
00107 static int ddWindowConv3 (DdManager *table, int low, int high);
00108 static int ddPermuteWindow4 (DdManager *table, int w);
00109 static int ddWindow4 (DdManager *table, int low, int high);
00110 static int ddWindowConv4 (DdManager *table, int low, int high);
00111 
00115 /*---------------------------------------------------------------------------*/
00116 /* Definition of exported functions                                          */
00117 /*---------------------------------------------------------------------------*/
00118 
00119 /*---------------------------------------------------------------------------*/
00120 /* Definition of internal functions                                          */
00121 /*---------------------------------------------------------------------------*/
00122 
00123 
00137 int
00138 cuddWindowReorder(
00139   DdManager * table /* DD table */,
00140   int low /* lowest index to reorder */,
00141   int high /* highest index to reorder */,
00142   Cudd_ReorderingType submethod /* window reordering option */)
00143 {
00144 
00145     int res;
00146 #ifdef DD_DEBUG
00147     int supposedOpt;
00148 #endif
00149 
00150     switch (submethod) {
00151     case CUDD_REORDER_WINDOW2:
00152         res = ddWindow2(table,low,high);
00153         break;
00154     case CUDD_REORDER_WINDOW3:
00155         res = ddWindow3(table,low,high);
00156         break;
00157     case CUDD_REORDER_WINDOW4:
00158         res = ddWindow4(table,low,high);
00159         break;
00160     case CUDD_REORDER_WINDOW2_CONV:
00161         res = ddWindowConv2(table,low,high);
00162         break;
00163     case CUDD_REORDER_WINDOW3_CONV:
00164         res = ddWindowConv3(table,low,high);
00165 #ifdef DD_DEBUG
00166         supposedOpt = table->keys - table->isolated;
00167         res = ddWindow3(table,low,high);
00168         if (table->keys - table->isolated != (unsigned) supposedOpt) {
00169             (void) fprintf(table->err, "Convergence failed! (%d != %d)\n",
00170                            table->keys - table->isolated, supposedOpt);
00171         }
00172 #endif
00173         break;
00174     case CUDD_REORDER_WINDOW4_CONV:
00175         res = ddWindowConv4(table,low,high);
00176 #ifdef DD_DEBUG
00177         supposedOpt = table->keys - table->isolated;
00178         res = ddWindow4(table,low,high);
00179         if (table->keys - table->isolated != (unsigned) supposedOpt) {
00180             (void) fprintf(table->err,"Convergence failed! (%d != %d)\n",
00181                            table->keys - table->isolated, supposedOpt);
00182         }
00183 #endif
00184         break;
00185     default: return(0);
00186     }
00187 
00188     return(res);
00189 
00190 } /* end of cuddWindowReorder */
00191 
00192 
00193 /*---------------------------------------------------------------------------*/
00194 /* Definition of static functions                                            */
00195 /*---------------------------------------------------------------------------*/
00196 
00209 static int
00210 ddWindow2(
00211   DdManager * table,
00212   int  low,
00213   int  high)
00214 {
00215 
00216     int x;
00217     int res;
00218     int size;
00219 
00220 #ifdef DD_DEBUG
00221     assert(low >= 0 && high < table->size);
00222 #endif
00223 
00224     if (high-low < 1) return(0);
00225 
00226     res = table->keys - table->isolated;
00227     for (x = low; x < high; x++) {
00228         size = res;
00229         res = cuddSwapInPlace(table,x,x+1);
00230         if (res == 0) return(0);
00231         if (res >= size) { /* no improvement: undo permutation */
00232             res = cuddSwapInPlace(table,x,x+1);
00233             if (res == 0) return(0);
00234         }
00235 #ifdef DD_STATS
00236         if (res < size) {
00237             (void) fprintf(table->out,"-");
00238         } else {
00239             (void) fprintf(table->out,"=");
00240         }
00241         fflush(table->out);
00242 #endif
00243     }
00244 
00245     return(1);
00246 
00247 } /* end of ddWindow2 */
00248 
00249 
00263 static int
00264 ddWindowConv2(
00265   DdManager * table,
00266   int  low,
00267   int  high)
00268 {
00269     int x;
00270     int res;
00271     int nwin;
00272     int newevent;
00273     int *events;
00274     int size;
00275 
00276 #ifdef DD_DEBUG
00277     assert(low >= 0 && high < table->size);
00278 #endif
00279 
00280     if (high-low < 1) return(ddWindowConv2(table,low,high));
00281 
00282     nwin = high-low;
00283     events = ALLOC(int,nwin);
00284     if (events == NULL) {
00285         table->errorCode = CUDD_MEMORY_OUT;
00286         return(0);
00287     }
00288     for (x=0; x<nwin; x++) {
00289         events[x] = 1;
00290     }
00291 
00292     res = table->keys - table->isolated;
00293     do {
00294         newevent = 0;
00295         for (x=0; x<nwin; x++) {
00296             if (events[x]) {
00297                 size = res;
00298                 res = cuddSwapInPlace(table,x+low,x+low+1);
00299                 if (res == 0) {
00300                     FREE(events);
00301                     return(0);
00302                 }
00303                 if (res >= size) { /* no improvement: undo permutation */
00304                     res = cuddSwapInPlace(table,x+low,x+low+1);
00305                     if (res == 0) {
00306                         FREE(events);
00307                         return(0);
00308                     }
00309                 }
00310                 if (res < size) {
00311                     if (x < nwin-1)     events[x+1] = 1;
00312                     if (x > 0)          events[x-1] = 1;
00313                     newevent = 1;
00314                 }
00315                 events[x] = 0;
00316 #ifdef DD_STATS
00317                 if (res < size) {
00318                     (void) fprintf(table->out,"-");
00319                 } else {
00320                     (void) fprintf(table->out,"=");
00321                 }
00322                 fflush(table->out);
00323 #endif
00324             }
00325         }
00326 #ifdef DD_STATS
00327         if (newevent) {
00328             (void) fprintf(table->out,"|");
00329             fflush(table->out);
00330         }
00331 #endif
00332     } while (newevent);
00333 
00334     FREE(events);
00335 
00336     return(1);
00337 
00338 } /* end of ddWindowConv3 */
00339 
00340 
00356 static int
00357 ddPermuteWindow3(
00358   DdManager * table,
00359   int  x)
00360 {
00361     int y,z;
00362     int size,sizeNew;
00363     int best;
00364 
00365 #ifdef DD_DEBUG
00366     assert(table->dead == 0);
00367     assert(x+2 < table->size);
00368 #endif
00369 
00370     size = table->keys - table->isolated;
00371     y = x+1; z = y+1;
00372 
00373     /* The permutation pattern is:
00374     ** (x,y)(y,z)
00375     ** repeated three times to get all 3! = 6 permutations.
00376     */
00377 #define ABC 1
00378     best = ABC;
00379 
00380 #define BAC 2
00381     sizeNew = cuddSwapInPlace(table,x,y);
00382     if (sizeNew < size) {
00383         if (sizeNew == 0) return(0);
00384         best = BAC;
00385         size = sizeNew;
00386     }
00387 #define BCA 3
00388     sizeNew = cuddSwapInPlace(table,y,z);
00389     if (sizeNew < size) {
00390         if (sizeNew == 0) return(0);
00391         best = BCA;
00392         size = sizeNew;
00393     }
00394 #define CBA 4
00395     sizeNew = cuddSwapInPlace(table,x,y);
00396     if (sizeNew < size) {
00397         if (sizeNew == 0) return(0);
00398         best = CBA;
00399         size = sizeNew;
00400     }
00401 #define CAB 5
00402     sizeNew = cuddSwapInPlace(table,y,z);
00403     if (sizeNew < size) {
00404         if (sizeNew == 0) return(0);
00405         best = CAB;
00406         size = sizeNew;
00407     }
00408 #define ACB 6
00409     sizeNew = cuddSwapInPlace(table,x,y);
00410     if (sizeNew < size) {
00411         if (sizeNew == 0) return(0);
00412         best = ACB;
00413         size = sizeNew;
00414     }
00415 
00416     /* Now take the shortest route to the best permuytation.
00417     ** The initial permutation is ACB.
00418     */
00419     switch(best) {
00420     case BCA: if (!cuddSwapInPlace(table,y,z)) return(0);
00421     case CBA: if (!cuddSwapInPlace(table,x,y)) return(0);
00422     case ABC: if (!cuddSwapInPlace(table,y,z)) return(0);
00423     case ACB: break;
00424     case BAC: if (!cuddSwapInPlace(table,y,z)) return(0);
00425     case CAB: if (!cuddSwapInPlace(table,x,y)) return(0);
00426                break;
00427     default: return(0);
00428     }
00429 
00430 #ifdef DD_DEBUG
00431     assert(table->keys - table->isolated == (unsigned) size);
00432 #endif
00433 
00434     return(best);
00435 
00436 } /* end of ddPermuteWindow3 */
00437 
00438 
00451 static int
00452 ddWindow3(
00453   DdManager * table,
00454   int  low,
00455   int  high)
00456 {
00457 
00458     int x;
00459     int res;
00460 
00461 #ifdef DD_DEBUG
00462     assert(low >= 0 && high < table->size);
00463 #endif
00464 
00465     if (high-low < 2) return(ddWindow2(table,low,high));
00466 
00467     for (x = low; x+1 < high; x++) {
00468         res = ddPermuteWindow3(table,x);
00469         if (res == 0) return(0);
00470 #ifdef DD_STATS
00471         if (res == ABC) {
00472             (void) fprintf(table->out,"=");
00473         } else {
00474             (void) fprintf(table->out,"-");
00475         }
00476         fflush(table->out);
00477 #endif
00478     }
00479 
00480     return(1);
00481 
00482 } /* end of ddWindow3 */
00483 
00484 
00498 static int
00499 ddWindowConv3(
00500   DdManager * table,
00501   int  low,
00502   int  high)
00503 {
00504     int x;
00505     int res;
00506     int nwin;
00507     int newevent;
00508     int *events;
00509 
00510 #ifdef DD_DEBUG
00511     assert(low >= 0 && high < table->size);
00512 #endif
00513 
00514     if (high-low < 2) return(ddWindowConv2(table,low,high));
00515 
00516     nwin = high-low-1;
00517     events = ALLOC(int,nwin);
00518     if (events == NULL) {
00519         table->errorCode = CUDD_MEMORY_OUT;
00520         return(0);
00521     }
00522     for (x=0; x<nwin; x++) {
00523         events[x] = 1;
00524     }
00525 
00526     do {
00527         newevent = 0;
00528         for (x=0; x<nwin; x++) {
00529             if (events[x]) {
00530                 res = ddPermuteWindow3(table,x+low);
00531                 switch (res) {
00532                 case ABC:
00533                     break;
00534                 case BAC:
00535                     if (x < nwin-1)     events[x+1] = 1;
00536                     if (x > 1)          events[x-2] = 1;
00537                     newevent = 1;
00538                     break;
00539                 case BCA:
00540                 case CBA:
00541                 case CAB:
00542                     if (x < nwin-2)     events[x+2] = 1;
00543                     if (x < nwin-1)     events[x+1] = 1;
00544                     if (x > 0)          events[x-1] = 1;
00545                     if (x > 1)          events[x-2] = 1;
00546                     newevent = 1;
00547                     break;
00548                 case ACB:
00549                     if (x < nwin-2)     events[x+2] = 1;
00550                     if (x > 0)          events[x-1] = 1;
00551                     newevent = 1;
00552                     break;
00553                 default:
00554                     FREE(events);
00555                     return(0);
00556                 }
00557                 events[x] = 0;
00558 #ifdef DD_STATS
00559                 if (res == ABC) {
00560                     (void) fprintf(table->out,"=");
00561                 } else {
00562                     (void) fprintf(table->out,"-");
00563                 }
00564                 fflush(table->out);
00565 #endif
00566             }
00567         }
00568 #ifdef DD_STATS
00569         if (newevent) {
00570             (void) fprintf(table->out,"|");
00571             fflush(table->out);
00572         }
00573 #endif
00574     } while (newevent);
00575 
00576     FREE(events);
00577 
00578     return(1);
00579 
00580 } /* end of ddWindowConv3 */
00581 
00582 
00596 static int
00597 ddPermuteWindow4(
00598   DdManager * table,
00599   int  w)
00600 {
00601     int x,y,z;
00602     int size,sizeNew;
00603     int best;
00604 
00605 #ifdef DD_DEBUG
00606     assert(table->dead == 0);
00607     assert(w+3 < table->size);
00608 #endif
00609 
00610     size = table->keys - table->isolated;
00611     x = w+1; y = x+1; z = y+1;
00612 
00613     /* The permutation pattern is:
00614      * (w,x)(y,z)(w,x)(x,y)
00615      * (y,z)(w,x)(y,z)(x,y)
00616      * repeated three times to get all 4! = 24 permutations.
00617      * This gives a hamiltonian circuit of Cayley's graph.
00618      * The codes to the permutation are assigned in topological order.
00619      * The permutations at lower distance from the final permutation are
00620      * assigned lower codes. This way we can choose, between
00621      * permutations that give the same size, one that requires the minimum
00622      * number of swaps from the final permutation of the hamiltonian circuit.
00623      * There is an exception to this rule: ABCD is given Code 1, to
00624      * avoid oscillation when convergence is sought.
00625      */
00626 #define ABCD 1
00627     best = ABCD;
00628 
00629 #define BACD 7
00630     sizeNew = cuddSwapInPlace(table,w,x);
00631     if (sizeNew < size) {
00632         if (sizeNew == 0) return(0);
00633         best = BACD;
00634         size = sizeNew;
00635     }
00636 #define BADC 13
00637     sizeNew = cuddSwapInPlace(table,y,z);
00638     if (sizeNew < size) {
00639         if (sizeNew == 0) return(0);
00640         best = BADC;
00641         size = sizeNew;
00642     }
00643 #define ABDC 8
00644     sizeNew = cuddSwapInPlace(table,w,x);
00645     if (sizeNew < size || (sizeNew == size && ABDC < best)) {
00646         if (sizeNew == 0) return(0);
00647         best = ABDC;
00648         size = sizeNew;
00649     }
00650 #define ADBC 14
00651     sizeNew = cuddSwapInPlace(table,x,y);
00652     if (sizeNew < size) {
00653         if (sizeNew == 0) return(0);
00654         best = ADBC;
00655         size = sizeNew;
00656     }
00657 #define ADCB 9
00658     sizeNew = cuddSwapInPlace(table,y,z);
00659     if (sizeNew < size || (sizeNew == size && ADCB < best)) {
00660         if (sizeNew == 0) return(0);
00661         best = ADCB;
00662         size = sizeNew;
00663     }
00664 #define DACB 15
00665     sizeNew = cuddSwapInPlace(table,w,x);
00666     if (sizeNew < size) {
00667         if (sizeNew == 0) return(0);
00668         best = DACB;
00669         size = sizeNew;
00670     }
00671 #define DABC 20
00672     sizeNew = cuddSwapInPlace(table,y,z);
00673     if (sizeNew < size) {
00674         if (sizeNew == 0) return(0);
00675         best = DABC;
00676         size = sizeNew;
00677     }
00678 #define DBAC 23
00679     sizeNew = cuddSwapInPlace(table,x,y);
00680     if (sizeNew < size) {
00681         if (sizeNew == 0) return(0);
00682         best = DBAC;
00683         size = sizeNew;
00684     }
00685 #define BDAC 19
00686     sizeNew = cuddSwapInPlace(table,w,x);
00687     if (sizeNew < size || (sizeNew == size && BDAC < best)) {
00688         if (sizeNew == 0) return(0);
00689         best = BDAC;
00690         size = sizeNew;
00691     }
00692 #define BDCA 21
00693     sizeNew = cuddSwapInPlace(table,y,z);
00694     if (sizeNew < size || (sizeNew == size && BDCA < best)) {
00695         if (sizeNew == 0) return(0);
00696         best = BDCA;
00697         size = sizeNew;
00698     }
00699 #define DBCA 24
00700     sizeNew = cuddSwapInPlace(table,w,x);
00701     if (sizeNew < size) {
00702         if (sizeNew == 0) return(0);
00703         best = DBCA;
00704         size = sizeNew;
00705     }
00706 #define DCBA 22
00707     sizeNew = cuddSwapInPlace(table,x,y);
00708     if (sizeNew < size || (sizeNew == size && DCBA < best)) {
00709         if (sizeNew == 0) return(0);
00710         best = DCBA;
00711         size = sizeNew;
00712     }
00713 #define DCAB 18
00714     sizeNew = cuddSwapInPlace(table,y,z);
00715     if (sizeNew < size || (sizeNew == size && DCAB < best)) {
00716         if (sizeNew == 0) return(0);
00717         best = DCAB;
00718         size = sizeNew;
00719     }
00720 #define CDAB 12
00721     sizeNew = cuddSwapInPlace(table,w,x);
00722     if (sizeNew < size || (sizeNew == size && CDAB < best)) {
00723         if (sizeNew == 0) return(0);
00724         best = CDAB;
00725         size = sizeNew;
00726     }
00727 #define CDBA 17
00728     sizeNew = cuddSwapInPlace(table,y,z);
00729     if (sizeNew < size || (sizeNew == size && CDBA < best)) {
00730         if (sizeNew == 0) return(0);
00731         best = CDBA;
00732         size = sizeNew;
00733     }
00734 #define CBDA 11
00735     sizeNew = cuddSwapInPlace(table,x,y);
00736     if (sizeNew < size || (sizeNew == size && CBDA < best)) {
00737         if (sizeNew == 0) return(0);
00738         best = CBDA;
00739         size = sizeNew;
00740     }
00741 #define BCDA 16
00742     sizeNew = cuddSwapInPlace(table,w,x);
00743     if (sizeNew < size || (sizeNew == size && BCDA < best)) {
00744         if (sizeNew == 0) return(0);
00745         best = BCDA;
00746         size = sizeNew;
00747     }
00748 #define BCAD 10
00749     sizeNew = cuddSwapInPlace(table,y,z);
00750     if (sizeNew < size || (sizeNew == size && BCAD < best)) {
00751         if (sizeNew == 0) return(0);
00752         best = BCAD;
00753         size = sizeNew;
00754     }
00755 #define CBAD 5
00756     sizeNew = cuddSwapInPlace(table,w,x);
00757     if (sizeNew < size || (sizeNew == size && CBAD < best)) {
00758         if (sizeNew == 0) return(0);
00759         best = CBAD;
00760         size = sizeNew;
00761     }
00762 #define CABD 3
00763     sizeNew = cuddSwapInPlace(table,x,y);
00764     if (sizeNew < size || (sizeNew == size && CABD < best)) {
00765         if (sizeNew == 0) return(0);
00766         best = CABD;
00767         size = sizeNew;
00768     }
00769 #define CADB 6
00770     sizeNew = cuddSwapInPlace(table,y,z);
00771     if (sizeNew < size || (sizeNew == size && CADB < best)) {
00772         if (sizeNew == 0) return(0);
00773         best = CADB;
00774         size = sizeNew;
00775     }
00776 #define ACDB 4
00777     sizeNew = cuddSwapInPlace(table,w,x);
00778     if (sizeNew < size || (sizeNew == size && ACDB < best)) {
00779         if (sizeNew == 0) return(0);
00780         best = ACDB;
00781         size = sizeNew;
00782     }
00783 #define ACBD 2
00784     sizeNew = cuddSwapInPlace(table,y,z);
00785     if (sizeNew < size || (sizeNew == size && ACBD < best)) {
00786         if (sizeNew == 0) return(0);
00787         best = ACBD;
00788         size = sizeNew;
00789     }
00790 
00791     /* Now take the shortest route to the best permutation.
00792     ** The initial permutation is ACBD.
00793     */
00794     switch(best) {
00795     case DBCA: if (!cuddSwapInPlace(table,y,z)) return(0);
00796     case BDCA: if (!cuddSwapInPlace(table,x,y)) return(0);
00797     case CDBA: if (!cuddSwapInPlace(table,w,x)) return(0);
00798     case ADBC: if (!cuddSwapInPlace(table,y,z)) return(0);
00799     case ABDC: if (!cuddSwapInPlace(table,x,y)) return(0);
00800     case ACDB: if (!cuddSwapInPlace(table,y,z)) return(0);
00801     case ACBD: break;
00802     case DCBA: if (!cuddSwapInPlace(table,y,z)) return(0);
00803     case BCDA: if (!cuddSwapInPlace(table,x,y)) return(0);
00804     case CBDA: if (!cuddSwapInPlace(table,w,x)) return(0);
00805                if (!cuddSwapInPlace(table,x,y)) return(0);
00806                if (!cuddSwapInPlace(table,y,z)) return(0);
00807                break;
00808     case DBAC: if (!cuddSwapInPlace(table,x,y)) return(0);
00809     case DCAB: if (!cuddSwapInPlace(table,w,x)) return(0);
00810     case DACB: if (!cuddSwapInPlace(table,y,z)) return(0);
00811     case BACD: if (!cuddSwapInPlace(table,x,y)) return(0);
00812     case CABD: if (!cuddSwapInPlace(table,w,x)) return(0);
00813                break;
00814     case DABC: if (!cuddSwapInPlace(table,y,z)) return(0);
00815     case BADC: if (!cuddSwapInPlace(table,x,y)) return(0);
00816     case CADB: if (!cuddSwapInPlace(table,w,x)) return(0);
00817                if (!cuddSwapInPlace(table,y,z)) return(0);
00818                break;
00819     case BDAC: if (!cuddSwapInPlace(table,x,y)) return(0);
00820     case CDAB: if (!cuddSwapInPlace(table,w,x)) return(0);
00821     case ADCB: if (!cuddSwapInPlace(table,y,z)) return(0);
00822     case ABCD: if (!cuddSwapInPlace(table,x,y)) return(0);
00823                break;
00824     case BCAD: if (!cuddSwapInPlace(table,x,y)) return(0);
00825     case CBAD: if (!cuddSwapInPlace(table,w,x)) return(0);
00826                if (!cuddSwapInPlace(table,x,y)) return(0);
00827                break;
00828     default: return(0);
00829     }
00830 
00831 #ifdef DD_DEBUG
00832     assert(table->keys - table->isolated == (unsigned) size);
00833 #endif
00834 
00835     return(best);
00836 
00837 } /* end of ddPermuteWindow4 */
00838 
00839 
00852 static int
00853 ddWindow4(
00854   DdManager * table,
00855   int  low,
00856   int  high)
00857 {
00858 
00859     int w;
00860     int res;
00861 
00862 #ifdef DD_DEBUG
00863     assert(low >= 0 && high < table->size);
00864 #endif
00865 
00866     if (high-low < 3) return(ddWindow3(table,low,high));
00867 
00868     for (w = low; w+2 < high; w++) {
00869         res = ddPermuteWindow4(table,w);
00870         if (res == 0) return(0);
00871 #ifdef DD_STATS
00872         if (res == ABCD) {
00873             (void) fprintf(table->out,"=");
00874         } else {
00875             (void) fprintf(table->out,"-");
00876         }
00877         fflush(table->out);
00878 #endif
00879     }
00880 
00881     return(1);
00882 
00883 } /* end of ddWindow4 */
00884 
00885 
00899 static int
00900 ddWindowConv4(
00901   DdManager * table,
00902   int  low,
00903   int  high)
00904 {
00905     int x;
00906     int res;
00907     int nwin;
00908     int newevent;
00909     int *events;
00910 
00911 #ifdef DD_DEBUG
00912     assert(low >= 0 && high < table->size);
00913 #endif
00914 
00915     if (high-low < 3) return(ddWindowConv3(table,low,high));
00916 
00917     nwin = high-low-2;
00918     events = ALLOC(int,nwin);
00919     if (events == NULL) {
00920         table->errorCode = CUDD_MEMORY_OUT;
00921         return(0);
00922     }
00923     for (x=0; x<nwin; x++) {
00924         events[x] = 1;
00925     }
00926 
00927     do {
00928         newevent = 0;
00929         for (x=0; x<nwin; x++) {
00930             if (events[x]) {
00931                 res = ddPermuteWindow4(table,x+low);
00932                 switch (res) {
00933                 case ABCD:
00934                     break;
00935                 case BACD:
00936                     if (x < nwin-1)     events[x+1] = 1;
00937                     if (x > 2)          events[x-3] = 1;
00938                     newevent = 1;
00939                     break;
00940                 case BADC:
00941                     if (x < nwin-3)     events[x+3] = 1;
00942                     if (x < nwin-1)     events[x+1] = 1;
00943                     if (x > 0)          events[x-1] = 1;
00944                     if (x > 2)          events[x-3] = 1;
00945                     newevent = 1;
00946                     break;
00947                 case ABDC:
00948                     if (x < nwin-3)     events[x+3] = 1;
00949                     if (x > 0)          events[x-1] = 1;
00950                     newevent = 1;
00951                     break;
00952                 case ADBC:
00953                 case ADCB:
00954                 case ACDB:
00955                     if (x < nwin-3)     events[x+3] = 1;
00956                     if (x < nwin-2)     events[x+2] = 1;
00957                     if (x > 0)          events[x-1] = 1;
00958                     if (x > 1)          events[x-2] = 1;
00959                     newevent = 1;
00960                     break;
00961                 case DACB:
00962                 case DABC:
00963                 case DBAC:
00964                 case BDAC:
00965                 case BDCA:
00966                 case DBCA:
00967                 case DCBA:
00968                 case DCAB:
00969                 case CDAB:
00970                 case CDBA:
00971                 case CBDA:
00972                 case BCDA:
00973                 case CADB:
00974                     if (x < nwin-3)     events[x+3] = 1;
00975                     if (x < nwin-2)     events[x+2] = 1;
00976                     if (x < nwin-1)     events[x+1] = 1;
00977                     if (x > 0)          events[x-1] = 1;
00978                     if (x > 1)          events[x-2] = 1;
00979                     if (x > 2)          events[x-3] = 1;
00980                     newevent = 1;
00981                     break;
00982                 case BCAD:
00983                 case CBAD:
00984                 case CABD:
00985                     if (x < nwin-2)     events[x+2] = 1;
00986                     if (x < nwin-1)     events[x+1] = 1;
00987                     if (x > 1)          events[x-2] = 1;
00988                     if (x > 2)          events[x-3] = 1;
00989                     newevent = 1;
00990                     break;
00991                 case ACBD:
00992                     if (x < nwin-2)     events[x+2] = 1;
00993                     if (x > 1)          events[x-2] = 1;
00994                     newevent = 1;
00995                     break;
00996                 default:
00997                     FREE(events);
00998                     return(0);
00999                 }
01000                 events[x] = 0;
01001 #ifdef DD_STATS
01002                 if (res == ABCD) {
01003                     (void) fprintf(table->out,"=");
01004                 } else {
01005                     (void) fprintf(table->out,"-");
01006                 }
01007                 fflush(table->out);
01008 #endif
01009             }
01010         }
01011 #ifdef DD_STATS
01012         if (newevent) {
01013             (void) fprintf(table->out,"|");
01014             fflush(table->out);
01015         }
01016 #endif
01017     } while (newevent);
01018 
01019     FREE(events);
01020 
01021     return(1);
01022 
01023 } /* end of ddWindowConv4 */