abc70930: src/bdd/cudd/cuddWindow.c Source File

00001 
00034 #include "util_hack.h"
00035 #include "cuddInt.h"
00036 
00037 /*---------------------------------------------------------------------------*/
00038 /* Constant declarations                                                     */
00039 /*---------------------------------------------------------------------------*/
00040 
00041 
00042 /*---------------------------------------------------------------------------*/
00043 /* Stucture declarations                                                     */
00044 /*---------------------------------------------------------------------------*/
00045 
00046 
00047 /*---------------------------------------------------------------------------*/
00048 /* Type declarations                                                         */
00049 /*---------------------------------------------------------------------------*/
00050 
00051 
00052 /*---------------------------------------------------------------------------*/
00053 /* Variable declarations                                                     */
00054 /*---------------------------------------------------------------------------*/
00055 
00056 #ifndef lint
00057 static char rcsid[] DD_UNUSED = "$Id: cuddWindow.c,v 1.1.1.1 2003/02/24 22:23:53 wjiang Exp $";
00058 #endif
00059 
00060 #ifdef DD_STATS
00061 extern  int     ddTotalNumberSwapping;
00062 extern  int     ddTotalNISwaps;
00063 #endif
00064 
00065 /*---------------------------------------------------------------------------*/
00066 /* Macro declarations                                                        */
00067 /*---------------------------------------------------------------------------*/
00068 
00069 
00072 /*---------------------------------------------------------------------------*/
00073 /* Static function prototypes                                                */
00074 /*---------------------------------------------------------------------------*/
00075 
00076 static int ddWindow2 ARGS((DdManager *table, int low, int high));
00077 static int ddWindowConv2 ARGS((DdManager *table, int low, int high));
00078 static int ddPermuteWindow3 ARGS((DdManager *table, int x));
00079 static int ddWindow3 ARGS((DdManager *table, int low, int high));
00080 static int ddWindowConv3 ARGS((DdManager *table, int low, int high));
00081 static int ddPermuteWindow4 ARGS((DdManager *table, int w));
00082 static int ddWindow4 ARGS((DdManager *table, int low, int high));
00083 static int ddWindowConv4 ARGS((DdManager *table, int low, int high));
00084 
00088 /*---------------------------------------------------------------------------*/
00089 /* Definition of exported functions                                          */
00090 /*---------------------------------------------------------------------------*/
00091 
00092 /*---------------------------------------------------------------------------*/
00093 /* Definition of internal functions                                          */
00094 /*---------------------------------------------------------------------------*/
00095 
00096 
00110 int
00111 cuddWindowReorder(
00112   DdManager * table /* DD table */,
00113   int low /* lowest index to reorder */,
00114   int high /* highest index to reorder */,
00115   Cudd_ReorderingType submethod /* window reordering option */)
00116 {
00117 
00118     int res;
00119 #ifdef DD_DEBUG
00120     int supposedOpt;
00121 #endif
00122 
00123     switch (submethod) {
00124     case CUDD_REORDER_WINDOW2:
00125         res = ddWindow2(table,low,high);
00126         break;
00127     case CUDD_REORDER_WINDOW3:
00128         res = ddWindow3(table,low,high);
00129         break;
00130     case CUDD_REORDER_WINDOW4:
00131         res = ddWindow4(table,low,high);
00132         break;
00133     case CUDD_REORDER_WINDOW2_CONV:
00134         res = ddWindowConv2(table,low,high);
00135         break;
00136     case CUDD_REORDER_WINDOW3_CONV:
00137         res = ddWindowConv3(table,low,high);
00138 #ifdef DD_DEBUG
00139         supposedOpt = table->keys - table->isolated;
00140         res = ddWindow3(table,low,high);
00141         if (table->keys - table->isolated != (unsigned) supposedOpt) {
00142             (void) fprintf(table->err, "Convergence failed! (%d != %d)\n",
00143                            table->keys - table->isolated, supposedOpt);
00144         }
00145 #endif
00146         break;
00147     case CUDD_REORDER_WINDOW4_CONV:
00148         res = ddWindowConv4(table,low,high);
00149 #ifdef DD_DEBUG
00150         supposedOpt = table->keys - table->isolated;
00151         res = ddWindow4(table,low,high);
00152         if (table->keys - table->isolated != (unsigned) supposedOpt) {
00153             (void) fprintf(table->err,"Convergence failed! (%d != %d)\n",
00154                            table->keys - table->isolated, supposedOpt);
00155         }
00156 #endif
00157         break;
00158     default: return(0);
00159     }
00160 
00161     return(res);
00162 
00163 } /* end of cuddWindowReorder */
00164 
00165 
00166 /*---------------------------------------------------------------------------*/
00167 /* Definition of static functions                                            */
00168 /*---------------------------------------------------------------------------*/
00169 
00182 static int
00183 ddWindow2(
00184   DdManager * table,
00185   int  low,
00186   int  high)
00187 {
00188 
00189     int x;
00190     int res;
00191     int size;
00192 
00193 #ifdef DD_DEBUG
00194     assert(low >= 0 && high < table->size);
00195 #endif
00196 
00197     if (high-low < 1) return(0);
00198 
00199     res = table->keys - table->isolated;
00200     for (x = low; x < high; x++) {
00201         size = res;
00202         res = cuddSwapInPlace(table,x,x+1);
00203         if (res == 0) return(0);
00204         if (res >= size) { /* no improvement: undo permutation */
00205             res = cuddSwapInPlace(table,x,x+1);
00206             if (res == 0) return(0);
00207         }
00208 #ifdef DD_STATS
00209         if (res < size) {
00210             (void) fprintf(table->out,"-");
00211         } else {
00212             (void) fprintf(table->out,"=");
00213         }
00214         fflush(table->out);
00215 #endif
00216     }
00217 
00218     return(1);
00219 
00220 } /* end of ddWindow2 */
00221 
00222 
00236 static int
00237 ddWindowConv2(
00238   DdManager * table,
00239   int  low,
00240   int  high)
00241 {
00242     int x;
00243     int res;
00244     int nwin;
00245     int newevent;
00246     int *events;
00247     int size;
00248 
00249 #ifdef DD_DEBUG
00250     assert(low >= 0 && high < table->size);
00251 #endif
00252 
00253     if (high-low < 1) return(ddWindowConv2(table,low,high));
00254 
00255     nwin = high-low;
00256     events = ALLOC(int,nwin);
00257     if (events == NULL) {
00258         table->errorCode = CUDD_MEMORY_OUT;
00259         return(0);
00260     }
00261     for (x=0; x<nwin; x++) {
00262         events[x] = 1;
00263     }
00264 
00265     res = table->keys - table->isolated;
00266     do {
00267         newevent = 0;
00268         for (x=0; x<nwin; x++) {
00269             if (events[x]) {
00270                 size = res;
00271                 res = cuddSwapInPlace(table,x+low,x+low+1);
00272                 if (res == 0) {
00273                     FREE(events);
00274                     return(0);
00275                 }
00276                 if (res >= size) { /* no improvement: undo permutation */
00277                     res = cuddSwapInPlace(table,x+low,x+low+1);
00278                     if (res == 0) {
00279                         FREE(events);
00280                         return(0);
00281                     }
00282                 }
00283                 if (res < size) {
00284                     if (x < nwin-1)     events[x+1] = 1;
00285                     if (x > 0)          events[x-1] = 1;
00286                     newevent = 1;
00287                 }
00288                 events[x] = 0;
00289 #ifdef DD_STATS
00290                 if (res < size) {
00291                     (void) fprintf(table->out,"-");
00292                 } else {
00293                     (void) fprintf(table->out,"=");
00294                 }
00295                 fflush(table->out);
00296 #endif
00297             }
00298         }
00299 #ifdef DD_STATS
00300         if (newevent) {
00301             (void) fprintf(table->out,"|");
00302             fflush(table->out);
00303         }
00304 #endif
00305     } while (newevent);
00306 
00307     FREE(events);
00308 
00309     return(1);
00310 
00311 } /* end of ddWindowConv3 */
00312 
00313 
00329 static int
00330 ddPermuteWindow3(
00331   DdManager * table,
00332   int  x)
00333 {
00334     int y,z;
00335     int size,sizeNew;
00336     int best;
00337 
00338 #ifdef DD_DEBUG
00339     assert(table->dead == 0);
00340     assert(x+2 < table->size);
00341 #endif
00342 
00343     size = table->keys - table->isolated;
00344     y = x+1; z = y+1;
00345     
00346     /* The permutation pattern is:
00347     ** (x,y)(y,z)
00348     ** repeated three times to get all 3! = 6 permutations.
00349     */
00350 #define ABC 1
00351     best = ABC;
00352 
00353 #define BAC 2
00354     sizeNew = cuddSwapInPlace(table,x,y);
00355     if (sizeNew < size) {
00356         if (sizeNew == 0) return(0);
00357         best = BAC;
00358         size = sizeNew;
00359     }
00360 #define BCA 3
00361     sizeNew = cuddSwapInPlace(table,y,z);
00362     if (sizeNew < size) {
00363         if (sizeNew == 0) return(0);
00364         best = BCA;
00365         size = sizeNew;
00366     }
00367 #define CBA 4
00368     sizeNew = cuddSwapInPlace(table,x,y);
00369     if (sizeNew < size) {
00370         if (sizeNew == 0) return(0);
00371         best = CBA;
00372         size = sizeNew;
00373     }
00374 #define CAB 5
00375     sizeNew = cuddSwapInPlace(table,y,z);
00376     if (sizeNew < size) {
00377         if (sizeNew == 0) return(0);
00378         best = CAB;
00379         size = sizeNew;
00380     }
00381 #define ACB 6
00382     sizeNew = cuddSwapInPlace(table,x,y);
00383     if (sizeNew < size) {
00384         if (sizeNew == 0) return(0);
00385         best = ACB;
00386         size = sizeNew;
00387     }
00388 
00389     /* Now take the shortest route to the best permuytation.
00390     ** The initial permutation is ACB.
00391     */
00392     switch(best) {
00393     case BCA: if (!cuddSwapInPlace(table,y,z)) return(0);
00394     case CBA: if (!cuddSwapInPlace(table,x,y)) return(0);
00395     case ABC: if (!cuddSwapInPlace(table,y,z)) return(0);
00396     case ACB: break;
00397     case BAC: if (!cuddSwapInPlace(table,y,z)) return(0);
00398     case CAB: if (!cuddSwapInPlace(table,x,y)) return(0);
00399                break;
00400     default: return(0);
00401     }
00402 
00403 #ifdef DD_DEBUG
00404     assert(table->keys - table->isolated == (unsigned) size);
00405 #endif
00406 
00407     return(best);
00408 
00409 } /* end of ddPermuteWindow3 */
00410 
00411 
00424 static int
00425 ddWindow3(
00426   DdManager * table,
00427   int  low,
00428   int  high)
00429 {
00430 
00431     int x;
00432     int res;
00433 
00434 #ifdef DD_DEBUG
00435     assert(low >= 0 && high < table->size);
00436 #endif
00437 
00438     if (high-low < 2) return(ddWindow2(table,low,high));
00439 
00440     for (x = low; x+1 < high; x++) {
00441         res = ddPermuteWindow3(table,x);
00442         if (res == 0) return(0);
00443 #ifdef DD_STATS
00444         if (res == ABC) {
00445             (void) fprintf(table->out,"=");
00446         } else {
00447             (void) fprintf(table->out,"-");
00448         }
00449         fflush(table->out);
00450 #endif
00451     }
00452 
00453     return(1);
00454 
00455 } /* end of ddWindow3 */
00456 
00457 
00471 static int
00472 ddWindowConv3(
00473   DdManager * table,
00474   int  low,
00475   int  high)
00476 {
00477     int x;
00478     int res;
00479     int nwin;
00480     int newevent;
00481     int *events;
00482 
00483 #ifdef DD_DEBUG
00484     assert(low >= 0 && high < table->size);
00485 #endif
00486 
00487     if (high-low < 2) return(ddWindowConv2(table,low,high));
00488 
00489     nwin = high-low-1;
00490     events = ALLOC(int,nwin);
00491     if (events == NULL) {
00492         table->errorCode = CUDD_MEMORY_OUT;
00493         return(0);
00494     }
00495     for (x=0; x<nwin; x++) {
00496         events[x] = 1;
00497     }
00498 
00499     do {
00500         newevent = 0;
00501         for (x=0; x<nwin; x++) {
00502             if (events[x]) {
00503                 res = ddPermuteWindow3(table,x+low);
00504                 switch (res) {
00505                 case ABC:
00506                     break;
00507                 case BAC:
00508                     if (x < nwin-1)     events[x+1] = 1;
00509                     if (x > 1)          events[x-2] = 1;
00510                     newevent = 1;
00511                     break;
00512                 case BCA:
00513                 case CBA:
00514                 case CAB:
00515                     if (x < nwin-2)     events[x+2] = 1;
00516                     if (x < nwin-1)     events[x+1] = 1;
00517                     if (x > 0)          events[x-1] = 1;
00518                     if (x > 1)          events[x-2] = 1;
00519                     newevent = 1;
00520                     break;
00521                 case ACB:
00522                     if (x < nwin-2)     events[x+2] = 1;
00523                     if (x > 0)          events[x-1] = 1;
00524                     newevent = 1;
00525                     break;
00526                 default:
00527                     FREE(events);
00528                     return(0);
00529                 }
00530                 events[x] = 0;
00531 #ifdef DD_STATS
00532                 if (res == ABC) {
00533                     (void) fprintf(table->out,"=");
00534                 } else {
00535                     (void) fprintf(table->out,"-");
00536                 }
00537                 fflush(table->out);
00538 #endif
00539             }
00540         }
00541 #ifdef DD_STATS
00542         if (newevent) {
00543             (void) fprintf(table->out,"|");
00544             fflush(table->out);
00545         }
00546 #endif
00547     } while (newevent);
00548 
00549     FREE(events);
00550 
00551     return(1);
00552 
00553 } /* end of ddWindowConv3 */
00554 
00555 
00569 static int
00570 ddPermuteWindow4(
00571   DdManager * table,
00572   int  w)
00573 {
00574     int x,y,z;
00575     int size,sizeNew;
00576     int best;
00577 
00578 #ifdef DD_DEBUG
00579     assert(table->dead == 0);
00580     assert(w+3 < table->size);
00581 #endif
00582 
00583     size = table->keys - table->isolated;
00584     x = w+1; y = x+1; z = y+1;
00585     
00586     /* The permutation pattern is:
00587      * (w,x)(y,z)(w,x)(x,y)
00588      * (y,z)(w,x)(y,z)(x,y)
00589      * repeated three times to get all 4! = 24 permutations.
00590      * This gives a hamiltonian circuit of Cayley's graph.
00591      * The codes to the permutation are assigned in topological order.
00592      * The permutations at lower distance from the final permutation are
00593      * assigned lower codes. This way we can choose, between
00594      * permutations that give the same size, one that requires the minimum
00595      * number of swaps from the final permutation of the hamiltonian circuit.
00596      * There is an exception to this rule: ABCD is given Code 1, to
00597      * avoid oscillation when convergence is sought.
00598      */
00599 #define ABCD 1
00600     best = ABCD;
00601 
00602 #define BACD 7
00603     sizeNew = cuddSwapInPlace(table,w,x);
00604     if (sizeNew < size) {
00605         if (sizeNew == 0) return(0);
00606         best = BACD;
00607         size = sizeNew;
00608     }
00609 #define BADC 13
00610     sizeNew = cuddSwapInPlace(table,y,z);
00611     if (sizeNew < size) {
00612         if (sizeNew == 0) return(0);
00613         best = BADC;
00614         size = sizeNew;
00615     }
00616 #define ABDC 8
00617     sizeNew = cuddSwapInPlace(table,w,x);
00618     if (sizeNew < size || (sizeNew == size && ABDC < best)) {
00619         if (sizeNew == 0) return(0);
00620         best = ABDC;
00621         size = sizeNew;
00622     }
00623 #define ADBC 14
00624     sizeNew = cuddSwapInPlace(table,x,y);
00625     if (sizeNew < size) {
00626         if (sizeNew == 0) return(0);
00627         best = ADBC;
00628         size = sizeNew;
00629     }
00630 #define ADCB 9
00631     sizeNew = cuddSwapInPlace(table,y,z);
00632     if (sizeNew < size || (sizeNew == size && ADCB < best)) {
00633         if (sizeNew == 0) return(0);
00634         best = ADCB;
00635         size = sizeNew;
00636     }
00637 #define DACB 15
00638     sizeNew = cuddSwapInPlace(table,w,x);
00639     if (sizeNew < size) {
00640         if (sizeNew == 0) return(0);
00641         best = DACB;
00642         size = sizeNew;
00643     }
00644 #define DABC 20
00645     sizeNew = cuddSwapInPlace(table,y,z);
00646     if (sizeNew < size) {
00647         if (sizeNew == 0) return(0);
00648         best = DABC;
00649         size = sizeNew;
00650     }
00651 #define DBAC 23
00652     sizeNew = cuddSwapInPlace(table,x,y);
00653     if (sizeNew < size) {
00654         if (sizeNew == 0) return(0);
00655         best = DBAC;
00656         size = sizeNew;
00657     }
00658 #define BDAC 19
00659     sizeNew = cuddSwapInPlace(table,w,x);
00660     if (sizeNew < size || (sizeNew == size && BDAC < best)) {
00661         if (sizeNew == 0) return(0);
00662         best = BDAC;
00663         size = sizeNew;
00664     }
00665 #define BDCA 21
00666     sizeNew = cuddSwapInPlace(table,y,z);
00667     if (sizeNew < size || (sizeNew == size && BDCA < best)) {
00668         if (sizeNew == 0) return(0);
00669         best = BDCA;
00670         size = sizeNew;
00671     }
00672 #define DBCA 24
00673     sizeNew = cuddSwapInPlace(table,w,x);
00674     if (sizeNew < size) {
00675         if (sizeNew == 0) return(0);
00676         best = DBCA;
00677         size = sizeNew;
00678     }
00679 #define DCBA 22
00680     sizeNew = cuddSwapInPlace(table,x,y);
00681     if (sizeNew < size || (sizeNew == size && DCBA < best)) {
00682         if (sizeNew == 0) return(0);
00683         best = DCBA;
00684         size = sizeNew;
00685     }
00686 #define DCAB 18
00687     sizeNew = cuddSwapInPlace(table,y,z);
00688     if (sizeNew < size || (sizeNew == size && DCAB < best)) {
00689         if (sizeNew == 0) return(0);
00690         best = DCAB;
00691         size = sizeNew;
00692     }
00693 #define CDAB 12
00694     sizeNew = cuddSwapInPlace(table,w,x);
00695     if (sizeNew < size || (sizeNew == size && CDAB < best)) {
00696         if (sizeNew == 0) return(0);
00697         best = CDAB;
00698         size = sizeNew;
00699     }
00700 #define CDBA 17
00701     sizeNew = cuddSwapInPlace(table,y,z);
00702     if (sizeNew < size || (sizeNew == size && CDBA < best)) {
00703         if (sizeNew == 0) return(0);
00704         best = CDBA;
00705         size = sizeNew;
00706     }
00707 #define CBDA 11
00708     sizeNew = cuddSwapInPlace(table,x,y);
00709     if (sizeNew < size || (sizeNew == size && CBDA < best)) {
00710         if (sizeNew == 0) return(0);
00711         best = CBDA;
00712         size = sizeNew;
00713     }
00714 #define BCDA 16
00715     sizeNew = cuddSwapInPlace(table,w,x);
00716     if (sizeNew < size || (sizeNew == size && BCDA < best)) {
00717         if (sizeNew == 0) return(0);
00718         best = BCDA;
00719         size = sizeNew;
00720     }
00721 #define BCAD 10
00722     sizeNew = cuddSwapInPlace(table,y,z);
00723     if (sizeNew < size || (sizeNew == size && BCAD < best)) {
00724         if (sizeNew == 0) return(0);
00725         best = BCAD;
00726         size = sizeNew;
00727     }
00728 #define CBAD 5
00729     sizeNew = cuddSwapInPlace(table,w,x);
00730     if (sizeNew < size || (sizeNew == size && CBAD < best)) {
00731         if (sizeNew == 0) return(0);
00732         best = CBAD;
00733         size = sizeNew;
00734     }
00735 #define CABD 3
00736     sizeNew = cuddSwapInPlace(table,x,y);
00737     if (sizeNew < size || (sizeNew == size && CABD < best)) {
00738         if (sizeNew == 0) return(0);
00739         best = CABD;
00740         size = sizeNew;
00741     }
00742 #define CADB 6
00743     sizeNew = cuddSwapInPlace(table,y,z);
00744     if (sizeNew < size || (sizeNew == size && CADB < best)) {
00745         if (sizeNew == 0) return(0);
00746         best = CADB;
00747         size = sizeNew;
00748     }
00749 #define ACDB 4
00750     sizeNew = cuddSwapInPlace(table,w,x);
00751     if (sizeNew < size || (sizeNew == size && ACDB < best)) {
00752         if (sizeNew == 0) return(0);
00753         best = ACDB;
00754         size = sizeNew;
00755     }
00756 #define ACBD 2
00757     sizeNew = cuddSwapInPlace(table,y,z);
00758     if (sizeNew < size || (sizeNew == size && ACBD < best)) {
00759         if (sizeNew == 0) return(0);
00760         best = ACBD;
00761         size = sizeNew;
00762     }
00763 
00764     /* Now take the shortest route to the best permutation.
00765     ** The initial permutation is ACBD.
00766     */
00767     switch(best) {
00768     case DBCA: if (!cuddSwapInPlace(table,y,z)) return(0);
00769     case BDCA: if (!cuddSwapInPlace(table,x,y)) return(0);
00770     case CDBA: if (!cuddSwapInPlace(table,w,x)) return(0);
00771     case ADBC: if (!cuddSwapInPlace(table,y,z)) return(0);
00772     case ABDC: if (!cuddSwapInPlace(table,x,y)) return(0);
00773     case ACDB: if (!cuddSwapInPlace(table,y,z)) return(0);
00774     case ACBD: break;
00775     case DCBA: if (!cuddSwapInPlace(table,y,z)) return(0);
00776     case BCDA: if (!cuddSwapInPlace(table,x,y)) return(0);
00777     case CBDA: if (!cuddSwapInPlace(table,w,x)) return(0);
00778                if (!cuddSwapInPlace(table,x,y)) return(0);
00779                if (!cuddSwapInPlace(table,y,z)) return(0);
00780                break;
00781     case DBAC: if (!cuddSwapInPlace(table,x,y)) return(0);
00782     case DCAB: if (!cuddSwapInPlace(table,w,x)) return(0);
00783     case DACB: if (!cuddSwapInPlace(table,y,z)) return(0);
00784     case BACD: if (!cuddSwapInPlace(table,x,y)) return(0);
00785     case CABD: if (!cuddSwapInPlace(table,w,x)) return(0);
00786                break;
00787     case DABC: if (!cuddSwapInPlace(table,y,z)) return(0);
00788     case BADC: if (!cuddSwapInPlace(table,x,y)) return(0);
00789     case CADB: if (!cuddSwapInPlace(table,w,x)) return(0);
00790                if (!cuddSwapInPlace(table,y,z)) return(0);
00791                break;
00792     case BDAC: if (!cuddSwapInPlace(table,x,y)) return(0);
00793     case CDAB: if (!cuddSwapInPlace(table,w,x)) return(0);
00794     case ADCB: if (!cuddSwapInPlace(table,y,z)) return(0);
00795     case ABCD: if (!cuddSwapInPlace(table,x,y)) return(0);
00796                break;
00797     case BCAD: if (!cuddSwapInPlace(table,x,y)) return(0);
00798     case CBAD: if (!cuddSwapInPlace(table,w,x)) return(0);
00799                if (!cuddSwapInPlace(table,x,y)) return(0);
00800                break;
00801     default: return(0);
00802     }
00803 
00804 #ifdef DD_DEBUG
00805     assert(table->keys - table->isolated == (unsigned) size);
00806 #endif
00807 
00808     return(best);
00809 
00810 } /* end of ddPermuteWindow4 */
00811 
00812 
00825 static int
00826 ddWindow4(
00827   DdManager * table,
00828   int  low,
00829   int  high)
00830 {
00831 
00832     int w;
00833     int res;
00834 
00835 #ifdef DD_DEBUG
00836     assert(low >= 0 && high < table->size);
00837 #endif
00838 
00839     if (high-low < 3) return(ddWindow3(table,low,high));
00840 
00841     for (w = low; w+2 < high; w++) {
00842         res = ddPermuteWindow4(table,w);
00843         if (res == 0) return(0);
00844 #ifdef DD_STATS
00845         if (res == ABCD) {
00846             (void) fprintf(table->out,"=");
00847         } else {
00848             (void) fprintf(table->out,"-");
00849         }
00850         fflush(table->out);
00851 #endif
00852     }
00853 
00854     return(1);
00855 
00856 } /* end of ddWindow4 */
00857 
00858 
00872 static int
00873 ddWindowConv4(
00874   DdManager * table,
00875   int  low,
00876   int  high)
00877 {
00878     int x;
00879     int res;
00880     int nwin;
00881     int newevent;
00882     int *events;
00883 
00884 #ifdef DD_DEBUG
00885     assert(low >= 0 && high < table->size);
00886 #endif
00887 
00888     if (high-low < 3) return(ddWindowConv3(table,low,high));
00889 
00890     nwin = high-low-2;
00891     events = ALLOC(int,nwin);
00892     if (events == NULL) {
00893         table->errorCode = CUDD_MEMORY_OUT;
00894         return(0);
00895     }
00896     for (x=0; x<nwin; x++) {
00897         events[x] = 1;
00898     }
00899 
00900     do {
00901         newevent = 0;
00902         for (x=0; x<nwin; x++) {
00903             if (events[x]) {
00904                 res = ddPermuteWindow4(table,x+low);
00905                 switch (res) {
00906                 case ABCD:
00907                     break;
00908                 case BACD:
00909                     if (x < nwin-1)     events[x+1] = 1;
00910                     if (x > 2)          events[x-3] = 1;
00911                     newevent = 1;
00912                     break;
00913                 case BADC:
00914                     if (x < nwin-3)     events[x+3] = 1;
00915                     if (x < nwin-1)     events[x+1] = 1;
00916                     if (x > 0)          events[x-1] = 1;
00917                     if (x > 2)          events[x-3] = 1;
00918                     newevent = 1;
00919                     break;
00920                 case ABDC:
00921                     if (x < nwin-3)     events[x+3] = 1;
00922                     if (x > 0)          events[x-1] = 1;
00923                     newevent = 1;
00924                     break;
00925                 case ADBC:
00926                 case ADCB:
00927                 case ACDB:
00928                     if (x < nwin-3)     events[x+3] = 1;
00929                     if (x < nwin-2)     events[x+2] = 1;
00930                     if (x > 0)          events[x-1] = 1;
00931                     if (x > 1)          events[x-2] = 1;
00932                     newevent = 1;
00933                     break;
00934                 case DACB:
00935                 case DABC:
00936                 case DBAC:
00937                 case BDAC:
00938                 case BDCA:
00939                 case DBCA:
00940                 case DCBA:
00941                 case DCAB:
00942                 case CDAB:
00943                 case CDBA:
00944                 case CBDA:
00945                 case BCDA:
00946                 case CADB:
00947                     if (x < nwin-3)     events[x+3] = 1;
00948                     if (x < nwin-2)     events[x+2] = 1;
00949                     if (x < nwin-1)     events[x+1] = 1;
00950                     if (x > 0)          events[x-1] = 1;
00951                     if (x > 1)          events[x-2] = 1;
00952                     if (x > 2)          events[x-3] = 1;
00953                     newevent = 1;
00954                     break;
00955                 case BCAD:
00956                 case CBAD:
00957                 case CABD:
00958                     if (x < nwin-2)     events[x+2] = 1;
00959                     if (x < nwin-1)     events[x+1] = 1;
00960                     if (x > 1)          events[x-2] = 1;
00961                     if (x > 2)          events[x-3] = 1;
00962                     newevent = 1;
00963                     break;
00964                 case ACBD:
00965                     if (x < nwin-2)     events[x+2] = 1;
00966                     if (x > 1)          events[x-2] = 1;
00967                     newevent = 1;
00968                     break;
00969                 default:
00970                     FREE(events);
00971                     return(0);
00972                 }
00973                 events[x] = 0;
00974 #ifdef DD_STATS
00975                 if (res == ABCD) {
00976                     (void) fprintf(table->out,"=");
00977                 } else {
00978                     (void) fprintf(table->out,"-");
00979                 }
00980                 fflush(table->out);
00981 #endif
00982             }
00983         }
00984 #ifdef DD_STATS
00985         if (newevent) {
00986             (void) fprintf(table->out,"|");
00987             fflush(table->out);
00988         }
00989 #endif
00990     } while (newevent);
00991 
00992     FREE(events);
00993 
00994     return(1);
00995 
00996 } /* end of ddWindowConv4 */
00997