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

  Synopsis    [Sifts a variable up.]

  Description [Sifts a variable up. Moves y up until either it reaches
  the bound (xLow) 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 up.]

Description [Sifts a variable up. Moves y up until either it reaches
the bound (xLow) 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 up . ] Description [ Sifts a variable up . Moves y up until either it reaches the bound ( xLow ) 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 *
ddSiftingUp(
  DdManager * table,
  int  y,
  int  xLow)
{
    Move        *moves;
    Move        *move;
    int         x;
    int         size;
    int         limitSize;
    int         xindex, yindex;
    int         isolated;
    int         L;      
#ifdef DD_DEBUG
    int checkL;
    int z;
    int zindex;
#endif
    moves = NULL;
    yindex = table->invperm[y];
    limitSize = L = table->keys - table->isolated;
    for (x = xLow + 1; x < y; x++) {
        xindex = table->invperm[x];
        if (cuddTestInteract(table,xindex,yindex)) {
            isolated = table->vars[xindex]->ref == 1;
            L -= table->subtables[x].keys - isolated;
        }
    }
    isolated = table->vars[yindex]->ref == 1;
    L -= table->subtables[y].keys - isolated;
    x = cuddNextLow(table,y);
    while (x >= xLow && L <= limitSize) {
        xindex = table->invperm[x];
#ifdef DD_DEBUG
        checkL = table->keys - table->isolated;
        for (z = xLow + 1; z < y; z++) {
            zindex = table->invperm[z];
            if (cuddTestInteract(table,zindex,yindex)) {
                isolated = table->vars[zindex]->ref == 1;
                checkL -= table->subtables[z].keys - isolated;
            }
        }
        isolated = table->vars[yindex]->ref == 1;
        checkL -= table->subtables[y].keys - isolated;
        assert(L == checkL);
#endif
        size = cuddSwapInPlace(table,x,y);
        if (size == 0) goto ddSiftingUpOutOfMem;
        if (cuddTestInteract(table,xindex,yindex)) {
            isolated = table->vars[xindex]->ref == 1;
            L += table->subtables[y].keys - isolated;
        }
        move = (Move *) cuddDynamicAllocNode(table);
        if (move == NULL) goto ddSiftingUpOutOfMem;
        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;
        y = x;
        x = cuddNextLow(table,y);
    }
    return(moves);
ddSiftingUpOutOfMem:
    while (moves != NULL) {
        move = moves->next;
        cuddDeallocMove(table, moves);
        moves = move;
    }
    return((Move *) CUDD_OUT_OF_MEM);
}
static Move * ddSiftingUp ( DdManager * table , int y , int xLow ) { Move * moves ; Move * move ; int x ; int size ; int limitSize ; int xindex , yindex ; int isolated ; int L ; #ifdef DD_DEBUG int checkL ; int z ; int zindex ; #endif moves = NULL ; yindex = table -> invperm [ y ] ; limitSize = L = table -> keys - table -> isolated ; for ( x = xLow + 1 ; x < y ; x ++ ) { xindex = table -> invperm [ x ] ; if ( cuddTestInteract ( table , xindex , yindex ) ) { isolated = table -> vars [ xindex ] -> ref == 1 ; L -= table -> subtables [ x ] . keys - isolated ; } } isolated = table -> vars [ yindex ] -> ref == 1 ; L -= table -> subtables [ y ] . keys - isolated ; x = cuddNextLow ( table , y ) ; while ( x >= xLow && L <= limitSize ) { xindex = table -> invperm [ x ] ; #ifdef DD_DEBUG checkL = table -> keys - table -> isolated ; for ( z = xLow + 1 ; z < y ; z ++ ) { zindex = table -> invperm [ z ] ; if ( cuddTestInteract ( table , zindex , yindex ) ) { isolated = table -> vars [ zindex ] -> ref == 1 ; checkL -= table -> subtables [ z ] . keys - isolated ; } } isolated = table -> vars [ yindex ] -> ref == 1 ; checkL -= table -> subtables [ y ] . keys - isolated ; assert ( L == checkL ) ; #endif size = cuddSwapInPlace ( table , x , y ) ; if ( size == 0 ) goto ddSiftingUpOutOfMem ; if ( cuddTestInteract ( table , xindex , yindex ) ) { isolated = table -> vars [ xindex ] -> ref == 1 ; L += table -> subtables [ y ] . keys - isolated ; } move = ( Move * ) cuddDynamicAllocNode ( table ) ; if ( move == NULL ) goto ddSiftingUpOutOfMem ; 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 ; y = x ; x = cuddNextLow ( table , y ) ; } return ( moves ) ; ddSiftingUpOutOfMem : while ( moves != NULL ) { move = moves -> next ; cuddDeallocMove ( table , moves ) ; moves = move ; } return ( ( Move * ) CUDD_OUT_OF_MEM ) ; }
Function
Synopsis    [Sifts a variable up.]
Function Synopsis [ Sifts a variable up . ]
/* lower bound on DD size */ /* Initialize the lower bound.
    ** The part of the DD below y will not change.
    ** The part of the DD above y that does not interact with y will not
    ** change. The rest may vanish in the best case, except for
    ** the nodes at level xLow, which will not vanish, regardless.
    */ /* Update the lower bound. */