diff options
Diffstat (limited to 'src/bdd/cudd/cuddWindow.c')
| -rw-r--r-- | src/bdd/cudd/cuddWindow.c | 727 |
1 files changed, 378 insertions, 349 deletions
diff --git a/src/bdd/cudd/cuddWindow.c b/src/bdd/cudd/cuddWindow.c index 62c92ff2..0a7c6705 100644 --- a/src/bdd/cudd/cuddWindow.c +++ b/src/bdd/cudd/cuddWindow.c @@ -4,30 +4,57 @@ PackageName [cudd] - Synopsis [Functions for window permutation] + Synopsis [Functions for variable reordering by window permutation.] Description [Internal procedures included in this module: - <ul> - <li> cuddWindowReorder() - </ul> - Static procedures included in this module: - <ul> - <li> ddWindow2() - <li> ddWindowConv2() - <li> ddPermuteWindow3() - <li> ddWindow3() - <li> ddWindowConv3() - <li> ddPermuteWindow4() - <li> ddWindow4() - <li> ddWindowConv4() - </ul>] + <ul> + <li> cuddWindowReorder() + </ul> + Static procedures included in this module: + <ul> + <li> ddWindow2() + <li> ddWindowConv2() + <li> ddPermuteWindow3() + <li> ddWindow3() + <li> ddWindowConv3() + <li> ddPermuteWindow4() + <li> ddWindow4() + <li> ddWindowConv4() + </ul>] Author [Fabio Somenzi] - Copyright [This file was created at the University of Colorado at - Boulder. The University of Colorado at Boulder makes no warranty - about the suitability of this software for any purpose. It is - presented on an AS IS basis.] + Copyright [Copyright (c) 1995-2004, Regents of the University of Colorado + + All rights reserved. + + Redistribution and use in source and binary forms, with or without + modification, are permitted provided that the following conditions + are met: + + Redistributions of source code must retain the above copyright + notice, this list of conditions and the following disclaimer. + + Redistributions in binary form must reproduce the above copyright + notice, this list of conditions and the following disclaimer in the + documentation and/or other materials provided with the distribution. + + Neither the name of the University of Colorado nor the names of its + contributors may be used to endorse or promote products derived from + this software without specific prior written permission. + + THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS + "AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT + LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS + FOR A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE + COPYRIGHT OWNER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, + INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, + BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; + LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER + CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT + LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN + ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE + POSSIBILITY OF SUCH DAMAGE.] ******************************************************************************/ @@ -37,6 +64,7 @@ ABC_NAMESPACE_IMPL_START + /*---------------------------------------------------------------------------*/ /* Constant declarations */ /*---------------------------------------------------------------------------*/ @@ -57,7 +85,7 @@ ABC_NAMESPACE_IMPL_START /*---------------------------------------------------------------------------*/ #ifndef lint -static char rcsid[] DD_UNUSED = "$Id: cuddWindow.c,v 1.1.1.1 2003/02/24 22:23:53 wjiang Exp $"; +static char rcsid[] DD_UNUSED = "$Id: cuddWindow.c,v 1.14 2009/02/20 02:14:58 fabio Exp $"; #endif #ifdef DD_STATS @@ -76,14 +104,14 @@ extern int ddTotalNISwaps; /* Static function prototypes */ /*---------------------------------------------------------------------------*/ -static int ddWindow2 ARGS((DdManager *table, int low, int high)); -static int ddWindowConv2 ARGS((DdManager *table, int low, int high)); -static int ddPermuteWindow3 ARGS((DdManager *table, int x)); -static int ddWindow3 ARGS((DdManager *table, int low, int high)); -static int ddWindowConv3 ARGS((DdManager *table, int low, int high)); -static int ddPermuteWindow4 ARGS((DdManager *table, int w)); -static int ddWindow4 ARGS((DdManager *table, int low, int high)); -static int ddWindowConv4 ARGS((DdManager *table, int low, int high)); +static int ddWindow2 (DdManager *table, int low, int high); +static int ddWindowConv2 (DdManager *table, int low, int high); +static int ddPermuteWindow3 (DdManager *table, int x); +static int ddWindow3 (DdManager *table, int low, int high); +static int ddWindowConv3 (DdManager *table, int low, int high); +static int ddPermuteWindow4 (DdManager *table, int w); +static int ddWindow4 (DdManager *table, int low, int high); +static int ddWindowConv4 (DdManager *table, int low, int high); /**AutomaticEnd***************************************************************/ @@ -125,39 +153,39 @@ cuddWindowReorder( switch (submethod) { case CUDD_REORDER_WINDOW2: - res = ddWindow2(table,low,high); - break; + res = ddWindow2(table,low,high); + break; case CUDD_REORDER_WINDOW3: - res = ddWindow3(table,low,high); - break; + res = ddWindow3(table,low,high); + break; case CUDD_REORDER_WINDOW4: - res = ddWindow4(table,low,high); - break; + res = ddWindow4(table,low,high); + break; case CUDD_REORDER_WINDOW2_CONV: - res = ddWindowConv2(table,low,high); - break; + res = ddWindowConv2(table,low,high); + break; case CUDD_REORDER_WINDOW3_CONV: - res = ddWindowConv3(table,low,high); + res = ddWindowConv3(table,low,high); #ifdef DD_DEBUG - supposedOpt = table->keys - table->isolated; - res = ddWindow3(table,low,high); - if (table->keys - table->isolated != (unsigned) supposedOpt) { - (void) fprintf(table->err, "Convergence failed! (%d != %d)\n", - table->keys - table->isolated, supposedOpt); - } + supposedOpt = table->keys - table->isolated; + res = ddWindow3(table,low,high); + if (table->keys - table->isolated != (unsigned) supposedOpt) { + (void) fprintf(table->err, "Convergence failed! (%d != %d)\n", + table->keys - table->isolated, supposedOpt); + } #endif - break; + break; case CUDD_REORDER_WINDOW4_CONV: - res = ddWindowConv4(table,low,high); + res = ddWindowConv4(table,low,high); #ifdef DD_DEBUG - supposedOpt = table->keys - table->isolated; - res = ddWindow4(table,low,high); - if (table->keys - table->isolated != (unsigned) supposedOpt) { - (void) fprintf(table->err,"Convergence failed! (%d != %d)\n", - table->keys - table->isolated, supposedOpt); - } + supposedOpt = table->keys - table->isolated; + res = ddWindow4(table,low,high); + if (table->keys - table->isolated != (unsigned) supposedOpt) { + (void) fprintf(table->err,"Convergence failed! (%d != %d)\n", + table->keys - table->isolated, supposedOpt); + } #endif - break; + break; default: return(0); } @@ -201,20 +229,20 @@ ddWindow2( res = table->keys - table->isolated; for (x = low; x < high; x++) { - size = res; - res = cuddSwapInPlace(table,x,x+1); - if (res == 0) return(0); - if (res >= size) { /* no improvement: undo permutation */ + size = res; res = cuddSwapInPlace(table,x,x+1); if (res == 0) return(0); - } + if (res >= size) { /* no improvement: undo permutation */ + res = cuddSwapInPlace(table,x,x+1); + if (res == 0) return(0); + } #ifdef DD_STATS - if (res < size) { - (void) fprintf(table->out,"-"); - } else { - (void) fprintf(table->out,"="); - } - fflush(table->out); + if (res < size) { + (void) fprintf(table->out,"-"); + } else { + (void) fprintf(table->out,"="); + } + fflush(table->out); #endif } @@ -258,52 +286,52 @@ ddWindowConv2( nwin = high-low; events = ABC_ALLOC(int,nwin); if (events == NULL) { - table->errorCode = CUDD_MEMORY_OUT; - return(0); + table->errorCode = CUDD_MEMORY_OUT; + return(0); } for (x=0; x<nwin; x++) { - events[x] = 1; + events[x] = 1; } res = table->keys - table->isolated; do { - newevent = 0; - for (x=0; x<nwin; x++) { - if (events[x]) { - size = res; - res = cuddSwapInPlace(table,x+low,x+low+1); - if (res == 0) { - ABC_FREE(events); - return(0); - } - if (res >= size) { /* no improvement: undo permutation */ - res = cuddSwapInPlace(table,x+low,x+low+1); - if (res == 0) { - ABC_FREE(events); - return(0); - } - } - if (res < size) { - if (x < nwin-1) events[x+1] = 1; - if (x > 0) events[x-1] = 1; - newevent = 1; - } - events[x] = 0; + newevent = 0; + for (x=0; x<nwin; x++) { + if (events[x]) { + size = res; + res = cuddSwapInPlace(table,x+low,x+low+1); + if (res == 0) { + ABC_FREE(events); + return(0); + } + if (res >= size) { /* no improvement: undo permutation */ + res = cuddSwapInPlace(table,x+low,x+low+1); + if (res == 0) { + ABC_FREE(events); + return(0); + } + } + if (res < size) { + if (x < nwin-1) events[x+1] = 1; + if (x > 0) events[x-1] = 1; + newevent = 1; + } + events[x] = 0; #ifdef DD_STATS - if (res < size) { - (void) fprintf(table->out,"-"); - } else { - (void) fprintf(table->out,"="); - } - fflush(table->out); + if (res < size) { + (void) fprintf(table->out,"-"); + } else { + (void) fprintf(table->out,"="); + } + fflush(table->out); #endif + } } - } #ifdef DD_STATS - if (newevent) { - (void) fprintf(table->out,"|"); - fflush(table->out); - } + if (newevent) { + (void) fprintf(table->out,"|"); + fflush(table->out); + } #endif } while (newevent); @@ -335,8 +363,8 @@ ddPermuteWindow3( int x) { int y,z; - int size,sizeNew; - int best; + int size,sizeNew; + int best; #ifdef DD_DEBUG assert(table->dead == 0); @@ -345,7 +373,7 @@ ddPermuteWindow3( size = table->keys - table->isolated; y = x+1; z = y+1; - + /* The permutation pattern is: ** (x,y)(y,z) ** repeated three times to get all 3! = 6 permutations. @@ -353,40 +381,40 @@ ddPermuteWindow3( #define ABC 1 best = ABC; -#define BAC 2 +#define BAC 2 sizeNew = cuddSwapInPlace(table,x,y); if (sizeNew < size) { - if (sizeNew == 0) return(0); - best = BAC; - size = sizeNew; + if (sizeNew == 0) return(0); + best = BAC; + size = sizeNew; } #define BCA 3 sizeNew = cuddSwapInPlace(table,y,z); if (sizeNew < size) { - if (sizeNew == 0) return(0); - best = BCA; - size = sizeNew; + if (sizeNew == 0) return(0); + best = BCA; + size = sizeNew; } #define CBA 4 sizeNew = cuddSwapInPlace(table,x,y); if (sizeNew < size) { - if (sizeNew == 0) return(0); - best = CBA; - size = sizeNew; + if (sizeNew == 0) return(0); + best = CBA; + size = sizeNew; } #define CAB 5 sizeNew = cuddSwapInPlace(table,y,z); if (sizeNew < size) { - if (sizeNew == 0) return(0); - best = CAB; - size = sizeNew; + if (sizeNew == 0) return(0); + best = CAB; + size = sizeNew; } #define ACB 6 sizeNew = cuddSwapInPlace(table,x,y); if (sizeNew < size) { - if (sizeNew == 0) return(0); - best = ACB; - size = sizeNew; + if (sizeNew == 0) return(0); + best = ACB; + size = sizeNew; } /* Now take the shortest route to the best permuytation. @@ -399,7 +427,7 @@ ddPermuteWindow3( case ACB: break; case BAC: if (!cuddSwapInPlace(table,y,z)) return(0); case CAB: if (!cuddSwapInPlace(table,x,y)) return(0); - break; + break; default: return(0); } @@ -441,15 +469,15 @@ ddWindow3( if (high-low < 2) return(ddWindow2(table,low,high)); for (x = low; x+1 < high; x++) { - res = ddPermuteWindow3(table,x); - if (res == 0) return(0); + res = ddPermuteWindow3(table,x); + if (res == 0) return(0); #ifdef DD_STATS - if (res == ABC) { - (void) fprintf(table->out,"="); - } else { - (void) fprintf(table->out,"-"); - } - fflush(table->out); + if (res == ABC) { + (void) fprintf(table->out,"="); + } else { + (void) fprintf(table->out,"-"); + } + fflush(table->out); #endif } @@ -492,60 +520,60 @@ ddWindowConv3( nwin = high-low-1; events = ABC_ALLOC(int,nwin); if (events == NULL) { - table->errorCode = CUDD_MEMORY_OUT; - return(0); + table->errorCode = CUDD_MEMORY_OUT; + return(0); } for (x=0; x<nwin; x++) { - events[x] = 1; + events[x] = 1; } do { - newevent = 0; - for (x=0; x<nwin; x++) { - if (events[x]) { - res = ddPermuteWindow3(table,x+low); - switch (res) { - case ABC: - break; - case BAC: - if (x < nwin-1) events[x+1] = 1; - if (x > 1) events[x-2] = 1; - newevent = 1; - break; - case BCA: - case CBA: - case CAB: - if (x < nwin-2) events[x+2] = 1; - if (x < nwin-1) events[x+1] = 1; - if (x > 0) events[x-1] = 1; - if (x > 1) events[x-2] = 1; - newevent = 1; - break; - case ACB: - if (x < nwin-2) events[x+2] = 1; - if (x > 0) events[x-1] = 1; - newevent = 1; - break; - default: - ABC_FREE(events); - return(0); - } - events[x] = 0; + newevent = 0; + for (x=0; x<nwin; x++) { + if (events[x]) { + res = ddPermuteWindow3(table,x+low); + switch (res) { + case ABC: + break; + case BAC: + if (x < nwin-1) events[x+1] = 1; + if (x > 1) events[x-2] = 1; + newevent = 1; + break; + case BCA: + case CBA: + case CAB: + if (x < nwin-2) events[x+2] = 1; + if (x < nwin-1) events[x+1] = 1; + if (x > 0) events[x-1] = 1; + if (x > 1) events[x-2] = 1; + newevent = 1; + break; + case ACB: + if (x < nwin-2) events[x+2] = 1; + if (x > 0) events[x-1] = 1; + newevent = 1; + break; + default: + ABC_FREE(events); + return(0); + } + events[x] = 0; #ifdef DD_STATS - if (res == ABC) { - (void) fprintf(table->out,"="); - } else { - (void) fprintf(table->out,"-"); - } - fflush(table->out); + if (res == ABC) { + (void) fprintf(table->out,"="); + } else { + (void) fprintf(table->out,"-"); + } + fflush(table->out); #endif + } } - } #ifdef DD_STATS - if (newevent) { - (void) fprintf(table->out,"|"); - fflush(table->out); - } + if (newevent) { + (void) fprintf(table->out,"|"); + fflush(table->out); + } #endif } while (newevent); @@ -575,8 +603,8 @@ ddPermuteWindow4( int w) { int x,y,z; - int size,sizeNew; - int best; + int size,sizeNew; + int best; #ifdef DD_DEBUG assert(table->dead == 0); @@ -585,7 +613,7 @@ ddPermuteWindow4( size = table->keys - table->isolated; x = w+1; y = x+1; z = y+1; - + /* The permutation pattern is: * (w,x)(y,z)(w,x)(x,y) * (y,z)(w,x)(y,z)(x,y) @@ -602,166 +630,166 @@ ddPermuteWindow4( #define ABCD 1 best = ABCD; -#define BACD 7 +#define BACD 7 sizeNew = cuddSwapInPlace(table,w,x); if (sizeNew < size) { - if (sizeNew == 0) return(0); - best = BACD; - size = sizeNew; + if (sizeNew == 0) return(0); + best = BACD; + size = sizeNew; } #define BADC 13 sizeNew = cuddSwapInPlace(table,y,z); if (sizeNew < size) { - if (sizeNew == 0) return(0); - best = BADC; - size = sizeNew; + if (sizeNew == 0) return(0); + best = BADC; + size = sizeNew; } #define ABDC 8 sizeNew = cuddSwapInPlace(table,w,x); if (sizeNew < size || (sizeNew == size && ABDC < best)) { - if (sizeNew == 0) return(0); - best = ABDC; - size = sizeNew; + if (sizeNew == 0) return(0); + best = ABDC; + size = sizeNew; } #define ADBC 14 sizeNew = cuddSwapInPlace(table,x,y); if (sizeNew < size) { - if (sizeNew == 0) return(0); - best = ADBC; - size = sizeNew; + if (sizeNew == 0) return(0); + best = ADBC; + size = sizeNew; } #define ADCB 9 sizeNew = cuddSwapInPlace(table,y,z); if (sizeNew < size || (sizeNew == size && ADCB < best)) { - if (sizeNew == 0) return(0); - best = ADCB; - size = sizeNew; + if (sizeNew == 0) return(0); + best = ADCB; + size = sizeNew; } #define DACB 15 sizeNew = cuddSwapInPlace(table,w,x); if (sizeNew < size) { - if (sizeNew == 0) return(0); - best = DACB; - size = sizeNew; + if (sizeNew == 0) return(0); + best = DACB; + size = sizeNew; } #define DABC 20 sizeNew = cuddSwapInPlace(table,y,z); if (sizeNew < size) { - if (sizeNew == 0) return(0); - best = DABC; - size = sizeNew; + if (sizeNew == 0) return(0); + best = DABC; + size = sizeNew; } #define DBAC 23 sizeNew = cuddSwapInPlace(table,x,y); if (sizeNew < size) { - if (sizeNew == 0) return(0); - best = DBAC; - size = sizeNew; + if (sizeNew == 0) return(0); + best = DBAC; + size = sizeNew; } #define BDAC 19 sizeNew = cuddSwapInPlace(table,w,x); if (sizeNew < size || (sizeNew == size && BDAC < best)) { - if (sizeNew == 0) return(0); - best = BDAC; - size = sizeNew; + if (sizeNew == 0) return(0); + best = BDAC; + size = sizeNew; } #define BDCA 21 sizeNew = cuddSwapInPlace(table,y,z); if (sizeNew < size || (sizeNew == size && BDCA < best)) { - if (sizeNew == 0) return(0); - best = BDCA; - size = sizeNew; + if (sizeNew == 0) return(0); + best = BDCA; + size = sizeNew; } #define DBCA 24 sizeNew = cuddSwapInPlace(table,w,x); if (sizeNew < size) { - if (sizeNew == 0) return(0); - best = DBCA; - size = sizeNew; + if (sizeNew == 0) return(0); + best = DBCA; + size = sizeNew; } #define DCBA 22 sizeNew = cuddSwapInPlace(table,x,y); if (sizeNew < size || (sizeNew == size && DCBA < best)) { - if (sizeNew == 0) return(0); - best = DCBA; - size = sizeNew; + if (sizeNew == 0) return(0); + best = DCBA; + size = sizeNew; } #define DCAB 18 sizeNew = cuddSwapInPlace(table,y,z); if (sizeNew < size || (sizeNew == size && DCAB < best)) { - if (sizeNew == 0) return(0); - best = DCAB; - size = sizeNew; + if (sizeNew == 0) return(0); + best = DCAB; + size = sizeNew; } #define CDAB 12 sizeNew = cuddSwapInPlace(table,w,x); if (sizeNew < size || (sizeNew == size && CDAB < best)) { - if (sizeNew == 0) return(0); - best = CDAB; - size = sizeNew; + if (sizeNew == 0) return(0); + best = CDAB; + size = sizeNew; } #define CDBA 17 sizeNew = cuddSwapInPlace(table,y,z); if (sizeNew < size || (sizeNew == size && CDBA < best)) { - if (sizeNew == 0) return(0); - best = CDBA; - size = sizeNew; + if (sizeNew == 0) return(0); + best = CDBA; + size = sizeNew; } #define CBDA 11 sizeNew = cuddSwapInPlace(table,x,y); if (sizeNew < size || (sizeNew == size && CBDA < best)) { - if (sizeNew == 0) return(0); - best = CBDA; - size = sizeNew; + if (sizeNew == 0) return(0); + best = CBDA; + size = sizeNew; } #define BCDA 16 sizeNew = cuddSwapInPlace(table,w,x); if (sizeNew < size || (sizeNew == size && BCDA < best)) { - if (sizeNew == 0) return(0); - best = BCDA; - size = sizeNew; + if (sizeNew == 0) return(0); + best = BCDA; + size = sizeNew; } #define BCAD 10 sizeNew = cuddSwapInPlace(table,y,z); if (sizeNew < size || (sizeNew == size && BCAD < best)) { - if (sizeNew == 0) return(0); - best = BCAD; - size = sizeNew; + if (sizeNew == 0) return(0); + best = BCAD; + size = sizeNew; } #define CBAD 5 sizeNew = cuddSwapInPlace(table,w,x); if (sizeNew < size || (sizeNew == size && CBAD < best)) { - if (sizeNew == 0) return(0); - best = CBAD; - size = sizeNew; + if (sizeNew == 0) return(0); + best = CBAD; + size = sizeNew; } #define CABD 3 sizeNew = cuddSwapInPlace(table,x,y); if (sizeNew < size || (sizeNew == size && CABD < best)) { - if (sizeNew == 0) return(0); - best = CABD; - size = sizeNew; + if (sizeNew == 0) return(0); + best = CABD; + size = sizeNew; } #define CADB 6 sizeNew = cuddSwapInPlace(table,y,z); if (sizeNew < size || (sizeNew == size && CADB < best)) { - if (sizeNew == 0) return(0); - best = CADB; - size = sizeNew; + if (sizeNew == 0) return(0); + best = CADB; + size = sizeNew; } #define ACDB 4 sizeNew = cuddSwapInPlace(table,w,x); if (sizeNew < size || (sizeNew == size && ACDB < best)) { - if (sizeNew == 0) return(0); - best = ACDB; - size = sizeNew; + if (sizeNew == 0) return(0); + best = ACDB; + size = sizeNew; } #define ACBD 2 sizeNew = cuddSwapInPlace(table,y,z); if (sizeNew < size || (sizeNew == size && ACBD < best)) { - if (sizeNew == 0) return(0); - best = ACBD; - size = sizeNew; + if (sizeNew == 0) return(0); + best = ACBD; + size = sizeNew; } /* Now take the shortest route to the best permutation. @@ -778,29 +806,29 @@ ddPermuteWindow4( case DCBA: if (!cuddSwapInPlace(table,y,z)) return(0); case BCDA: if (!cuddSwapInPlace(table,x,y)) return(0); case CBDA: if (!cuddSwapInPlace(table,w,x)) return(0); - if (!cuddSwapInPlace(table,x,y)) return(0); - if (!cuddSwapInPlace(table,y,z)) return(0); - break; + if (!cuddSwapInPlace(table,x,y)) return(0); + if (!cuddSwapInPlace(table,y,z)) return(0); + break; case DBAC: if (!cuddSwapInPlace(table,x,y)) return(0); case DCAB: if (!cuddSwapInPlace(table,w,x)) return(0); case DACB: if (!cuddSwapInPlace(table,y,z)) return(0); case BACD: if (!cuddSwapInPlace(table,x,y)) return(0); case CABD: if (!cuddSwapInPlace(table,w,x)) return(0); - break; + break; case DABC: if (!cuddSwapInPlace(table,y,z)) return(0); case BADC: if (!cuddSwapInPlace(table,x,y)) return(0); case CADB: if (!cuddSwapInPlace(table,w,x)) return(0); - if (!cuddSwapInPlace(table,y,z)) return(0); - break; + if (!cuddSwapInPlace(table,y,z)) return(0); + break; case BDAC: if (!cuddSwapInPlace(table,x,y)) return(0); case CDAB: if (!cuddSwapInPlace(table,w,x)) return(0); case ADCB: if (!cuddSwapInPlace(table,y,z)) return(0); case ABCD: if (!cuddSwapInPlace(table,x,y)) return(0); - break; + break; case BCAD: if (!cuddSwapInPlace(table,x,y)) return(0); case CBAD: if (!cuddSwapInPlace(table,w,x)) return(0); - if (!cuddSwapInPlace(table,x,y)) return(0); - break; + if (!cuddSwapInPlace(table,x,y)) return(0); + break; default: return(0); } @@ -842,15 +870,15 @@ ddWindow4( if (high-low < 3) return(ddWindow3(table,low,high)); for (w = low; w+2 < high; w++) { - res = ddPermuteWindow4(table,w); - if (res == 0) return(0); + res = ddPermuteWindow4(table,w); + if (res == 0) return(0); #ifdef DD_STATS - if (res == ABCD) { - (void) fprintf(table->out,"="); - } else { - (void) fprintf(table->out,"-"); - } - fflush(table->out); + if (res == ABCD) { + (void) fprintf(table->out,"="); + } else { + (void) fprintf(table->out,"-"); + } + fflush(table->out); #endif } @@ -893,102 +921,102 @@ ddWindowConv4( nwin = high-low-2; events = ABC_ALLOC(int,nwin); if (events == NULL) { - table->errorCode = CUDD_MEMORY_OUT; - return(0); + table->errorCode = CUDD_MEMORY_OUT; + return(0); } for (x=0; x<nwin; x++) { - events[x] = 1; + events[x] = 1; } do { - newevent = 0; - for (x=0; x<nwin; x++) { - if (events[x]) { - res = ddPermuteWindow4(table,x+low); - switch (res) { - case ABCD: - break; - case BACD: - if (x < nwin-1) events[x+1] = 1; - if (x > 2) events[x-3] = 1; - newevent = 1; - break; - case BADC: - if (x < nwin-3) events[x+3] = 1; - if (x < nwin-1) events[x+1] = 1; - if (x > 0) events[x-1] = 1; - if (x > 2) events[x-3] = 1; - newevent = 1; - break; - case ABDC: - if (x < nwin-3) events[x+3] = 1; - if (x > 0) events[x-1] = 1; - newevent = 1; - break; - case ADBC: - case ADCB: - case ACDB: - if (x < nwin-3) events[x+3] = 1; - if (x < nwin-2) events[x+2] = 1; - if (x > 0) events[x-1] = 1; - if (x > 1) events[x-2] = 1; - newevent = 1; - break; - case DACB: - case DABC: - case DBAC: - case BDAC: - case BDCA: - case DBCA: - case DCBA: - case DCAB: - case CDAB: - case CDBA: - case CBDA: - case BCDA: - case CADB: - if (x < nwin-3) events[x+3] = 1; - if (x < nwin-2) events[x+2] = 1; - if (x < nwin-1) events[x+1] = 1; - if (x > 0) events[x-1] = 1; - if (x > 1) events[x-2] = 1; - if (x > 2) events[x-3] = 1; - newevent = 1; - break; - case BCAD: - case CBAD: - case CABD: - if (x < nwin-2) events[x+2] = 1; - if (x < nwin-1) events[x+1] = 1; - if (x > 1) events[x-2] = 1; - if (x > 2) events[x-3] = 1; - newevent = 1; - break; - case ACBD: - if (x < nwin-2) events[x+2] = 1; - if (x > 1) events[x-2] = 1; - newevent = 1; - break; - default: - ABC_FREE(events); - return(0); - } - events[x] = 0; + newevent = 0; + for (x=0; x<nwin; x++) { + if (events[x]) { + res = ddPermuteWindow4(table,x+low); + switch (res) { + case ABCD: + break; + case BACD: + if (x < nwin-1) events[x+1] = 1; + if (x > 2) events[x-3] = 1; + newevent = 1; + break; + case BADC: + if (x < nwin-3) events[x+3] = 1; + if (x < nwin-1) events[x+1] = 1; + if (x > 0) events[x-1] = 1; + if (x > 2) events[x-3] = 1; + newevent = 1; + break; + case ABDC: + if (x < nwin-3) events[x+3] = 1; + if (x > 0) events[x-1] = 1; + newevent = 1; + break; + case ADBC: + case ADCB: + case ACDB: + if (x < nwin-3) events[x+3] = 1; + if (x < nwin-2) events[x+2] = 1; + if (x > 0) events[x-1] = 1; + if (x > 1) events[x-2] = 1; + newevent = 1; + break; + case DACB: + case DABC: + case DBAC: + case BDAC: + case BDCA: + case DBCA: + case DCBA: + case DCAB: + case CDAB: + case CDBA: + case CBDA: + case BCDA: + case CADB: + if (x < nwin-3) events[x+3] = 1; + if (x < nwin-2) events[x+2] = 1; + if (x < nwin-1) events[x+1] = 1; + if (x > 0) events[x-1] = 1; + if (x > 1) events[x-2] = 1; + if (x > 2) events[x-3] = 1; + newevent = 1; + break; + case BCAD: + case CBAD: + case CABD: + if (x < nwin-2) events[x+2] = 1; + if (x < nwin-1) events[x+1] = 1; + if (x > 1) events[x-2] = 1; + if (x > 2) events[x-3] = 1; + newevent = 1; + break; + case ACBD: + if (x < nwin-2) events[x+2] = 1; + if (x > 1) events[x-2] = 1; + newevent = 1; + break; + default: + ABC_FREE(events); + return(0); + } + events[x] = 0; #ifdef DD_STATS - if (res == ABCD) { - (void) fprintf(table->out,"="); - } else { - (void) fprintf(table->out,"-"); - } - fflush(table->out); + if (res == ABCD) { + (void) fprintf(table->out,"="); + } else { + (void) fprintf(table->out,"-"); + } + fflush(table->out); #endif + } } - } #ifdef DD_STATS - if (newevent) { - (void) fprintf(table->out,"|"); - fflush(table->out); - } + if (newevent) { + (void) fprintf(table->out,"|"); + fflush(table->out); + } #endif } while (newevent); @@ -998,5 +1026,6 @@ ddWindowConv4( } /* end of ddWindowConv4 */ + ABC_NAMESPACE_IMPL_END |