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

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


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