diff options
author | Alan Mishchenko <alanmi@berkeley.edu> | 2005-07-29 08:01:00 -0700 |
---|---|---|
committer | Alan Mishchenko <alanmi@berkeley.edu> | 2005-07-29 08:01:00 -0700 |
commit | 888e5bed5d7f56a5d86d91a6e8e88f3e5a3454dc (patch) | |
tree | 11d48c9e9069f54dc300c3571ae63c744c802c50 /src/bdd/cudd/cuddWindow.c | |
parent | 7f94414388cce67bd3cc1a6d6269f0ed31ed0d06 (diff) | |
download | abc-888e5bed5d7f56a5d86d91a6e8e88f3e5a3454dc.tar.gz abc-888e5bed5d7f56a5d86d91a6e8e88f3e5a3454dc.tar.bz2 abc-888e5bed5d7f56a5d86d91a6e8e88f3e5a3454dc.zip |
Version abc50729
Diffstat (limited to 'src/bdd/cudd/cuddWindow.c')
-rw-r--r-- | src/bdd/cudd/cuddWindow.c | 997 |
1 files changed, 997 insertions, 0 deletions
diff --git a/src/bdd/cudd/cuddWindow.c b/src/bdd/cudd/cuddWindow.c new file mode 100644 index 00000000..3e6d5686 --- /dev/null +++ b/src/bdd/cudd/cuddWindow.c @@ -0,0 +1,997 @@ +/**CFile*********************************************************************** + + FileName [cuddWindow.c] + + PackageName [cudd] + + Synopsis [Functions for 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>] + + 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.] + +******************************************************************************/ + +#include "util.h" +#include "cuddInt.h" + +/*---------------------------------------------------------------------------*/ +/* Constant declarations */ +/*---------------------------------------------------------------------------*/ + + +/*---------------------------------------------------------------------------*/ +/* Stucture declarations */ +/*---------------------------------------------------------------------------*/ + + +/*---------------------------------------------------------------------------*/ +/* Type declarations */ +/*---------------------------------------------------------------------------*/ + + +/*---------------------------------------------------------------------------*/ +/* Variable declarations */ +/*---------------------------------------------------------------------------*/ + +#ifndef lint +static char rcsid[] DD_UNUSED = "$Id: cuddWindow.c,v 1.1.1.1 2003/02/24 22:23:53 wjiang Exp $"; +#endif + +#ifdef DD_STATS +extern int ddTotalNumberSwapping; +extern int ddTotalNISwaps; +#endif + +/*---------------------------------------------------------------------------*/ +/* Macro declarations */ +/*---------------------------------------------------------------------------*/ + + +/**AutomaticStart*************************************************************/ + +/*---------------------------------------------------------------------------*/ +/* 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)); + +/**AutomaticEnd***************************************************************/ + + +/*---------------------------------------------------------------------------*/ +/* Definition of exported functions */ +/*---------------------------------------------------------------------------*/ + +/*---------------------------------------------------------------------------*/ +/* Definition of internal functions */ +/*---------------------------------------------------------------------------*/ + + +/**Function******************************************************************** + + Synopsis [Reorders by applying the method of the sliding window.] + + Description [Reorders by applying the method of the sliding window. + Tries all possible permutations to the variables in a window that + slides from low to high. The size of the window is determined by + submethod. Assumes that no dead nodes are present. Returns 1 in + case of success; 0 otherwise.] + + SideEffects [None] + +******************************************************************************/ +int +cuddWindowReorder( + DdManager * table /* DD table */, + int low /* lowest index to reorder */, + int high /* highest index to reorder */, + Cudd_ReorderingType submethod /* window reordering option */) +{ + + int res; +#ifdef DD_DEBUG + int supposedOpt; +#endif + + switch (submethod) { + case CUDD_REORDER_WINDOW2: + res = ddWindow2(table,low,high); + break; + case CUDD_REORDER_WINDOW3: + res = ddWindow3(table,low,high); + break; + case CUDD_REORDER_WINDOW4: + res = ddWindow4(table,low,high); + break; + case CUDD_REORDER_WINDOW2_CONV: + res = ddWindowConv2(table,low,high); + break; + case CUDD_REORDER_WINDOW3_CONV: + 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); + } +#endif + break; + case CUDD_REORDER_WINDOW4_CONV: + 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); + } +#endif + break; + default: return(0); + } + + return(res); + +} /* end of cuddWindowReorder */ + + +/*---------------------------------------------------------------------------*/ +/* Definition of static functions */ +/*---------------------------------------------------------------------------*/ + +/**Function******************************************************************** + + Synopsis [Reorders by applying a sliding window of width 2.] + + Description [Reorders by applying a sliding window of width 2. + Tries both permutations of the variables in a window + that slides from low to high. Assumes that no dead nodes are + present. Returns 1 in case of success; 0 otherwise.] + + SideEffects [None] + +******************************************************************************/ +static int +ddWindow2( + DdManager * table, + int low, + int high) +{ + + int x; + int res; + int size; + +#ifdef DD_DEBUG + assert(low >= 0 && high < table->size); +#endif + + if (high-low < 1) return(0); + + 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 */ + 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); +#endif + } + + return(1); + +} /* end of ddWindow2 */ + + +/**Function******************************************************************** + + Synopsis [Reorders by repeatedly applying a sliding window of width 2.] + + Description [Reorders by repeatedly applying a sliding window of width + 2. Tries both permutations of the variables in a window + that slides from low to high. Assumes that no dead nodes are + present. Uses an event-driven approach to determine convergence. + Returns 1 in case of success; 0 otherwise.] + + SideEffects [None] + +******************************************************************************/ +static int +ddWindowConv2( + DdManager * table, + int low, + int high) +{ + int x; + int res; + int nwin; + int newevent; + int *events; + int size; + +#ifdef DD_DEBUG + assert(low >= 0 && high < table->size); +#endif + + if (high-low < 1) return(ddWindowConv2(table,low,high)); + + nwin = high-low; + events = ALLOC(int,nwin); + if (events == NULL) { + table->errorCode = CUDD_MEMORY_OUT; + return(0); + } + for (x=0; x<nwin; x++) { + 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) { + FREE(events); + return(0); + } + if (res >= size) { /* no improvement: undo permutation */ + res = cuddSwapInPlace(table,x+low,x+low+1); + if (res == 0) { + 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); +#endif + } + } +#ifdef DD_STATS + if (newevent) { + (void) fprintf(table->out,"|"); + fflush(table->out); + } +#endif + } while (newevent); + + FREE(events); + + return(1); + +} /* end of ddWindowConv3 */ + + +/**Function******************************************************************** + + Synopsis [Tries all the permutations of the three variables between + x and x+2 and retains the best.] + + Description [Tries all the permutations of the three variables between + x and x+2 and retains the best. Assumes that no dead nodes are + present. Returns the index of the best permutation (1-6) in case of + success; 0 otherwise.Assumes that no dead nodes are present. Returns + the index of the best permutation (1-6) in case of success; 0 + otherwise.] + + SideEffects [None] + +******************************************************************************/ +static int +ddPermuteWindow3( + DdManager * table, + int x) +{ + int y,z; + int size,sizeNew; + int best; + +#ifdef DD_DEBUG + assert(table->dead == 0); + assert(x+2 < table->size); +#endif + + 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. + */ +#define ABC 1 + best = ABC; + +#define BAC 2 + sizeNew = cuddSwapInPlace(table,x,y); + if (sizeNew < size) { + 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; + } +#define CBA 4 + sizeNew = cuddSwapInPlace(table,x,y); + if (sizeNew < size) { + 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; + } +#define ACB 6 + sizeNew = cuddSwapInPlace(table,x,y); + if (sizeNew < size) { + if (sizeNew == 0) return(0); + best = ACB; + size = sizeNew; + } + + /* Now take the shortest route to the best permuytation. + ** The initial permutation is ACB. + */ + switch(best) { + case BCA: if (!cuddSwapInPlace(table,y,z)) return(0); + case CBA: if (!cuddSwapInPlace(table,x,y)) return(0); + case ABC: if (!cuddSwapInPlace(table,y,z)) return(0); + case ACB: break; + case BAC: if (!cuddSwapInPlace(table,y,z)) return(0); + case CAB: if (!cuddSwapInPlace(table,x,y)) return(0); + break; + default: return(0); + } + +#ifdef DD_DEBUG + assert(table->keys - table->isolated == (unsigned) size); +#endif + + return(best); + +} /* end of ddPermuteWindow3 */ + + +/**Function******************************************************************** + + Synopsis [Reorders by applying a sliding window of width 3.] + + Description [Reorders by applying a sliding window of width 3. + Tries all possible permutations to the variables in a + window that slides from low to high. Assumes that no dead nodes are + present. Returns 1 in case of success; 0 otherwise.] + + SideEffects [None] + +******************************************************************************/ +static int +ddWindow3( + DdManager * table, + int low, + int high) +{ + + int x; + int res; + +#ifdef DD_DEBUG + assert(low >= 0 && high < table->size); +#endif + + 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); +#ifdef DD_STATS + if (res == ABC) { + (void) fprintf(table->out,"="); + } else { + (void) fprintf(table->out,"-"); + } + fflush(table->out); +#endif + } + + return(1); + +} /* end of ddWindow3 */ + + +/**Function******************************************************************** + + Synopsis [Reorders by repeatedly applying a sliding window of width 3.] + + Description [Reorders by repeatedly applying a sliding window of width + 3. Tries all possible permutations to the variables in a + window that slides from low to high. Assumes that no dead nodes are + present. Uses an event-driven approach to determine convergence. + Returns 1 in case of success; 0 otherwise.] + + SideEffects [None] + +******************************************************************************/ +static int +ddWindowConv3( + DdManager * table, + int low, + int high) +{ + int x; + int res; + int nwin; + int newevent; + int *events; + +#ifdef DD_DEBUG + assert(low >= 0 && high < table->size); +#endif + + if (high-low < 2) return(ddWindowConv2(table,low,high)); + + nwin = high-low-1; + events = ALLOC(int,nwin); + if (events == NULL) { + table->errorCode = CUDD_MEMORY_OUT; + return(0); + } + for (x=0; x<nwin; x++) { + 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: + 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); +#endif + } + } +#ifdef DD_STATS + if (newevent) { + (void) fprintf(table->out,"|"); + fflush(table->out); + } +#endif + } while (newevent); + + FREE(events); + + return(1); + +} /* end of ddWindowConv3 */ + + +/**Function******************************************************************** + + Synopsis [Tries all the permutations of the four variables between w + and w+3 and retains the best.] + + Description [Tries all the permutations of the four variables between + w and w+3 and retains the best. Assumes that no dead nodes are + present. Returns the index of the best permutation (1-24) in case of + success; 0 otherwise.] + + SideEffects [None] + +******************************************************************************/ +static int +ddPermuteWindow4( + DdManager * table, + int w) +{ + int x,y,z; + int size,sizeNew; + int best; + +#ifdef DD_DEBUG + assert(table->dead == 0); + assert(w+3 < table->size); +#endif + + 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) + * repeated three times to get all 4! = 24 permutations. + * This gives a hamiltonian circuit of Cayley's graph. + * The codes to the permutation are assigned in topological order. + * The permutations at lower distance from the final permutation are + * assigned lower codes. This way we can choose, between + * permutations that give the same size, one that requires the minimum + * number of swaps from the final permutation of the hamiltonian circuit. + * There is an exception to this rule: ABCD is given Code 1, to + * avoid oscillation when convergence is sought. + */ +#define ABCD 1 + best = ABCD; + +#define BACD 7 + sizeNew = cuddSwapInPlace(table,w,x); + if (sizeNew < size) { + 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; + } +#define ABDC 8 + sizeNew = cuddSwapInPlace(table,w,x); + if (sizeNew < size || (sizeNew == size && ABDC < best)) { + 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; + } +#define ADCB 9 + sizeNew = cuddSwapInPlace(table,y,z); + if (sizeNew < size || (sizeNew == size && ADCB < best)) { + 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; + } +#define DABC 20 + sizeNew = cuddSwapInPlace(table,y,z); + if (sizeNew < size) { + 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; + } +#define BDAC 19 + sizeNew = cuddSwapInPlace(table,w,x); + if (sizeNew < size || (sizeNew == size && BDAC < best)) { + 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; + } +#define DBCA 24 + sizeNew = cuddSwapInPlace(table,w,x); + if (sizeNew < size) { + 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; + } +#define DCAB 18 + sizeNew = cuddSwapInPlace(table,y,z); + if (sizeNew < size || (sizeNew == size && DCAB < best)) { + 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; + } +#define CDBA 17 + sizeNew = cuddSwapInPlace(table,y,z); + if (sizeNew < size || (sizeNew == size && CDBA < best)) { + 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; + } +#define BCDA 16 + sizeNew = cuddSwapInPlace(table,w,x); + if (sizeNew < size || (sizeNew == size && BCDA < best)) { + 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; + } +#define CBAD 5 + sizeNew = cuddSwapInPlace(table,w,x); + if (sizeNew < size || (sizeNew == size && CBAD < best)) { + 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; + } +#define CADB 6 + sizeNew = cuddSwapInPlace(table,y,z); + if (sizeNew < size || (sizeNew == size && CADB < best)) { + 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; + } +#define ACBD 2 + sizeNew = cuddSwapInPlace(table,y,z); + if (sizeNew < size || (sizeNew == size && ACBD < best)) { + if (sizeNew == 0) return(0); + best = ACBD; + size = sizeNew; + } + + /* Now take the shortest route to the best permutation. + ** The initial permutation is ACBD. + */ + switch(best) { + case DBCA: if (!cuddSwapInPlace(table,y,z)) return(0); + case BDCA: if (!cuddSwapInPlace(table,x,y)) return(0); + case CDBA: if (!cuddSwapInPlace(table,w,x)) return(0); + case ADBC: if (!cuddSwapInPlace(table,y,z)) return(0); + case ABDC: if (!cuddSwapInPlace(table,x,y)) return(0); + case ACDB: if (!cuddSwapInPlace(table,y,z)) return(0); + case ACBD: break; + 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; + 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; + 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; + 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; + 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; + default: return(0); + } + +#ifdef DD_DEBUG + assert(table->keys - table->isolated == (unsigned) size); +#endif + + return(best); + +} /* end of ddPermuteWindow4 */ + + +/**Function******************************************************************** + + Synopsis [Reorders by applying a sliding window of width 4.] + + Description [Reorders by applying a sliding window of width 4. + Tries all possible permutations to the variables in a + window that slides from low to high. Assumes that no dead nodes are + present. Returns 1 in case of success; 0 otherwise.] + + SideEffects [None] + +******************************************************************************/ +static int +ddWindow4( + DdManager * table, + int low, + int high) +{ + + int w; + int res; + +#ifdef DD_DEBUG + assert(low >= 0 && high < table->size); +#endif + + 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); +#ifdef DD_STATS + if (res == ABCD) { + (void) fprintf(table->out,"="); + } else { + (void) fprintf(table->out,"-"); + } + fflush(table->out); +#endif + } + + return(1); + +} /* end of ddWindow4 */ + + +/**Function******************************************************************** + + Synopsis [Reorders by repeatedly applying a sliding window of width 4.] + + Description [Reorders by repeatedly applying a sliding window of width + 4. Tries all possible permutations to the variables in a + window that slides from low to high. Assumes that no dead nodes are + present. Uses an event-driven approach to determine convergence. + Returns 1 in case of success; 0 otherwise.] + + SideEffects [None] + +******************************************************************************/ +static int +ddWindowConv4( + DdManager * table, + int low, + int high) +{ + int x; + int res; + int nwin; + int newevent; + int *events; + +#ifdef DD_DEBUG + assert(low >= 0 && high < table->size); +#endif + + if (high-low < 3) return(ddWindowConv3(table,low,high)); + + nwin = high-low-2; + events = ALLOC(int,nwin); + if (events == NULL) { + table->errorCode = CUDD_MEMORY_OUT; + return(0); + } + for (x=0; x<nwin; x++) { + 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: + 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); +#endif + } + } +#ifdef DD_STATS + if (newevent) { + (void) fprintf(table->out,"|"); + fflush(table->out); + } +#endif + } while (newevent); + + FREE(events); + + return(1); + +} /* end of ddWindowConv4 */ + |