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

  Synopsis    [Sifts a variable down.]

  Description [Sifts a variable down. Moves x down until either it
  reaches the bound (xHigh) or the size of the DD heap increases too
  much. Returns the set of moves in case of success; NULL if memory is
  full.]

  SideEffects [None]

******************************************************************************/
Function
Synopsis    [Sifts a variable down.]

Description [Sifts a variable down. Moves x down until either it
reaches the bound (xHigh) or the size of the DD heap increases too
much. Returns the set of moves in case of success; NULL if memory is
full.]


Function Synopsis [ Sifts a variable down . ] Description [ Sifts a variable down . Moves x down until either it reaches the bound ( xHigh ) or the size of the DD heap increases too much . Returns the set of moves in case of success ; NULL if memory is full . ]
static Move *
ddSiftingDown(
  DdManager * table,
  int  x,
  int  xHigh)
{
    Move        *moves;
    Move        *move;
    int         y;
    int         size;
    int         R;      
    int         limitSize;
    int         xindex, yindex;
    int         isolated;
#ifdef DD_DEBUG
    int         checkR;
    int         z;
    int         zindex;
#endif
    moves = NULL;
    xindex = table->invperm[x];
    limitSize = size = table->keys - table->isolated;
    R = 0;
    for (y = xHigh; y > x; y--) {
        yindex = table->invperm[y];
        if (cuddTestInteract(table,xindex,yindex)) {
            isolated = table->vars[yindex]->ref == 1;
            R += table->subtables[y].keys - isolated;
        }
    }
    y = cuddNextHigh(table,x);
    while (y <= xHigh && size - R < limitSize) {
#ifdef DD_DEBUG
        checkR = 0;
        for (z = xHigh; z > x; z--) {
            zindex = table->invperm[z];
            if (cuddTestInteract(table,xindex,zindex)) {
                isolated = table->vars[zindex]->ref == 1;
                checkR += table->subtables[z].keys - isolated;
            }
        }
        assert(R == checkR);
#endif
        yindex = table->invperm[y];
        if (cuddTestInteract(table,xindex,yindex)) {
            isolated = table->vars[yindex]->ref == 1;
            R -= table->subtables[y].keys - isolated;
        }
        size = cuddSwapInPlace(table,x,y);
        if (size == 0) goto ddSiftingDownOutOfMem;
        move = (Move *) cuddDynamicAllocNode(table);
        if (move == NULL) goto ddSiftingDownOutOfMem;
        move->x = x;
        move->y = y;
        move->size = size;
        move->next = moves;
        moves = move;
        if ((double) size > (double) limitSize * table->maxGrowth) break;
        if (size < limitSize) limitSize = size;
        x = y;
        y = cuddNextHigh(table,x);
    }
    return(moves);
ddSiftingDownOutOfMem:
    while (moves != NULL) {
        move = moves->next;
        cuddDeallocMove(table, moves);
        moves = move;
    }
    return((Move *) CUDD_OUT_OF_MEM);
}
static Move * ddSiftingDown ( DdManager * table , int x , int xHigh ) { Move * moves ; Move * move ; int y ; int size ; int R ; int limitSize ; int xindex , yindex ; int isolated ; #ifdef DD_DEBUG int checkR ; int z ; int zindex ; #endif moves = NULL ; xindex = table -> invperm [ x ] ; limitSize = size = table -> keys - table -> isolated ; R = 0 ; for ( y = xHigh ; y > x ; y -- ) { yindex = table -> invperm [ y ] ; if ( cuddTestInteract ( table , xindex , yindex ) ) { isolated = table -> vars [ yindex ] -> ref == 1 ; R += table -> subtables [ y ] . keys - isolated ; } } y = cuddNextHigh ( table , x ) ; while ( y <= xHigh && size - R < limitSize ) { #ifdef DD_DEBUG checkR = 0 ; for ( z = xHigh ; z > x ; z -- ) { zindex = table -> invperm [ z ] ; if ( cuddTestInteract ( table , xindex , zindex ) ) { isolated = table -> vars [ zindex ] -> ref == 1 ; checkR += table -> subtables [ z ] . keys - isolated ; } } assert ( R == checkR ) ; #endif yindex = table -> invperm [ y ] ; if ( cuddTestInteract ( table , xindex , yindex ) ) { isolated = table -> vars [ yindex ] -> ref == 1 ; R -= table -> subtables [ y ] . keys - isolated ; } size = cuddSwapInPlace ( table , x , y ) ; if ( size == 0 ) goto ddSiftingDownOutOfMem ; move = ( Move * ) cuddDynamicAllocNode ( table ) ; if ( move == NULL ) goto ddSiftingDownOutOfMem ; move -> x = x ; move -> y = y ; move -> size = size ; move -> next = moves ; moves = move ; if ( ( double ) size > ( double ) limitSize * table -> maxGrowth ) break ; if ( size < limitSize ) limitSize = size ; x = y ; y = cuddNextHigh ( table , x ) ; } return ( moves ) ; ddSiftingDownOutOfMem : while ( moves != NULL ) { move = moves -> next ; cuddDeallocMove ( table , moves ) ; moves = move ; } return ( ( Move * ) CUDD_OUT_OF_MEM ) ; }
Function
Synopsis    [Sifts a variable down.]
Function Synopsis [ Sifts a variable down . ]
/* upper bound on node decrease */ /* Initialize R */ /* Update upper bound on node decrease. */