abc/src/bdd/cudd/cuddWindow.c
/**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]

******************************************************************************/
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.]


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 . ]
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 = ABC_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) {
                    ABC_FREE(events);
                    return(0);
                }
                if (res >= size) { 
                    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);
#endif
            }
        }
#ifdef DD_STATS
        if (newevent) {
            (void) fprintf(table->out,"|");
            fflush(table->out);
        }
#endif
    } while (newevent);
    ABC_FREE(events);
    return(1);
}
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 = ABC_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 ) { ABC_FREE ( events ) ; return ( 0 ) ; } if ( res >= size ) { 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 ) ; #endif } } #ifdef DD_STATS if ( newevent ) { ( void ) fprintf ( table -> out , " " ) ; fflush ( table -> out ) ; } #endif } while ( newevent ) ; ABC_FREE ( events ) ; return ( 1 ) ; }
Function
Synopsis    [Reorders by repeatedly applying a sliding window of width 2.]
Function Synopsis [ Reorders by repeatedly applying a sliding window of width 2 . ]
/* no improvement: undo permutation */