abc/src/bdd/cudd/cuddReorder.c
/**Function********************************************************************

  Synopsis    [Reorders variables by a sequence of (non-adjacent) swaps.]

  Description [Implementation of Plessier's algorithm that reorders
  variables by a sequence of (non-adjacent) swaps.
    <ol>
    <li> Select two variables (RANDOM or HEURISTIC).
    <li> Permute these variables.
    <li> If the nodes have decreased accept the permutation.
    <li> Otherwise reconstruct the original heap.
    <li> Loop.
    </ol>
  Returns 1 in case of success; 0 otherwise.]

  SideEffects [None]

******************************************************************************/
Function
Synopsis    [Reorders variables by a sequence of (non-adjacent) swaps.]

Description [Implementation of Plessier's algorithm that reorders
variables by a sequence of (non-adjacent) swaps.

 Select two variables (RANDOM or HEURISTIC).
 Permute these variables.
 If the nodes have decreased accept the permutation.
 Otherwise reconstruct the original heap.
 Loop.

Returns 1 in case of success; 0 otherwise.]


Function Synopsis [ Reorders variables by a sequence of ( non - adjacent ) swaps . ] Description [ Implementation of Plessier ' s algorithm that reorders variables by a sequence of ( non - adjacent ) swaps . Select two variables ( RANDOM or HEURISTIC ) . Permute these variables . If the nodes have decreased accept the permutation . Otherwise reconstruct the original heap . Loop . Returns 1 in case of success ; 0 otherwise . ]
int
cuddSwapping(
  DdManager * table,
  int lower,
  int upper,
  Cudd_ReorderingType heuristic)
{
    int i, j;
    int max, keys;
    int nvars;
    int x, y;
    int iterate;
    int previousSize;
    Move *moves, *move;
    int pivot = -1;
    int modulo;
    int result;
#ifdef DD_DEBUG
    assert(lower >= 0 && upper < table->size && lower <= upper);
#endif
    nvars = upper - lower + 1;
    iterate = nvars;
    for (i = 0; i < iterate; i++) {
        if (ddTotalNumberSwapping >= table->siftMaxSwap)
            break;
        if (heuristic == CUDD_REORDER_RANDOM_PIVOT) {
            max = -1;
            for (j = lower; j <= upper; j++) {
                if ((keys = table->subtables[j].keys) > max) {
                    max = keys;
                    pivot = j;
                }
            }
            modulo = upper - pivot;
            if (modulo == 0) {
                y = pivot;
            } else{
                y = pivot + 1 + ((int) Cudd_Random() % modulo);
            }
            modulo = pivot - lower - 1;
            if (modulo < 1) {
                x = lower;
            } else{
                do {
                    x = (int) Cudd_Random() % modulo;
                } while (x == y);
            }
        } else {
            x = ((int) Cudd_Random() % nvars) + lower;
            do {
                y = ((int) Cudd_Random() % nvars) + lower;
            } while (x == y);
        }
        previousSize = table->keys - table->isolated;
        moves = ddSwapAny(table,x,y);
        if (moves == NULL) goto cuddSwappingOutOfMem;
        result = ddSiftingBackward(table,previousSize,moves);
        if (!result) goto cuddSwappingOutOfMem;
        while (moves != NULL) {
            move = moves->next;
            cuddDeallocMove(table, moves);
            moves = move;
        }
#ifdef DD_STATS
        if (table->keys < (unsigned) previousSize + table->isolated) {
            (void) fprintf(table->out,"-");
        } else if (table->keys > (unsigned) previousSize + table->isolated) {
            (void) fprintf(table->out,"+");     
        } else {
            (void) fprintf(table->out,"=");
        }
        fflush(table->out);
#endif
#if 0
        (void) fprintf(table->out,"#:t_SWAPPING %8d: tmp size\n",
                       table->keys - table->isolated);
#endif
    }
    return(1);
cuddSwappingOutOfMem:
    while (moves != NULL) {
        move = moves->next;
        cuddDeallocMove(table, moves);
        moves = move;
    }
    return(0);
}
int cuddSwapping ( DdManager * table , int lower , int upper , Cudd_ReorderingType heuristic ) { int i , j ; int max , keys ; int nvars ; int x , y ; int iterate ; int previousSize ; Move * moves , * move ; int pivot = -1 ; int modulo ; int result ; #ifdef DD_DEBUG assert ( lower >= 0 && upper < table -> size && lower <= upper ) ; #endif nvars = upper - lower + 1 ; iterate = nvars ; for ( i = 0 ; i < iterate ; i ++ ) { if ( ddTotalNumberSwapping >= table -> siftMaxSwap ) break ; if ( heuristic == CUDD_REORDER_RANDOM_PIVOT ) { max = -1 ; for ( j = lower ; j <= upper ; j ++ ) { if ( ( keys = table -> subtables [ j ] . keys ) > max ) { max = keys ; pivot = j ; } } modulo = upper - pivot ; if ( modulo == 0 ) { y = pivot ; } else { y = pivot + 1 + ( ( int ) Cudd_Random ( ) % modulo ) ; } modulo = pivot - lower - 1 ; if ( modulo < 1 ) { x = lower ; } else { do { x = ( int ) Cudd_Random ( ) % modulo ; } while ( x == y ) ; } } else { x = ( ( int ) Cudd_Random ( ) % nvars ) + lower ; do { y = ( ( int ) Cudd_Random ( ) % nvars ) + lower ; } while ( x == y ) ; } previousSize = table -> keys - table -> isolated ; moves = ddSwapAny ( table , x , y ) ; if ( moves == NULL ) goto cuddSwappingOutOfMem ; result = ddSiftingBackward ( table , previousSize , moves ) ; if ( ! result ) goto cuddSwappingOutOfMem ; while ( moves != NULL ) { move = moves -> next ; cuddDeallocMove ( table , moves ) ; moves = move ; } #ifdef DD_STATS if ( table -> keys < ( unsigned ) previousSize + table -> isolated ) { ( void ) fprintf ( table -> out , " " ) ; } else if ( table -> keys > ( unsigned ) previousSize + table -> isolated ) { ( void ) fprintf ( table -> out , " " ) ; } else { ( void ) fprintf ( table -> out , " " ) ; } fflush ( table -> out ) ; #endif #if 0 ( void ) fprintf ( table -> out , " \n " , table -> keys - table -> isolated ) ; #endif } return ( 1 ) ; cuddSwappingOutOfMem : while ( moves != NULL ) { move = moves -> next ; cuddDeallocMove ( table , moves ) ; moves = move ; } return ( 0 ) ; }
Function
Synopsis    [Reorders variables by a sequence of (non-adjacent) swaps.]
Function Synopsis [ Reorders variables by a sequence of ( non - adjacent ) swaps . ]
/* Sanity check */ /* should never happen */