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

  Synopsis    [Sifts one variable up and down until it has taken all
  positions. Checks for aggregation.]

  Description [Sifts one variable up and down until it has taken all
  positions. Checks for aggregation. There may be at most two sweeps,
  even if the group grows.  Assumes that x is either an isolated
  variable, or it is the bottom of a group. All groups may not have
  been found. The variable being moved is returned to the best position
  seen during sifting.  Returns 1 in case of success; 0 otherwise.]

  SideEffects [None]

******************************************************************************/
Function
Synopsis    [Sifts one variable up and down until it has taken all
positions. Checks for aggregation.]

Description [Sifts one variable up and down until it has taken all
positions. Checks for aggregation. There may be at most two sweeps,
even if the group grows.  Assumes that x is either an isolated
variable, or it is the bottom of a group. All groups may not have
been found. The variable being moved is returned to the best position
seen during sifting.  Returns 1 in case of success; 0 otherwise.]


Function Synopsis [ Sifts one variable up and down until it has taken all positions . Checks for aggregation . ] Description [ Sifts one variable up and down until it has taken all positions . Checks for aggregation . There may be at most two sweeps even if the group grows . Assumes that x is either an isolated variable or it is the bottom of a group . All groups may not have been found . The variable being moved is returned to the best position seen during sifting . Returns 1 in case of success ; 0 otherwise . ]
static int
ddGroupSiftingAux(
  DdManager * table,
  int  x,
  int  xLow,
  int  xHigh,
  DD_CHKFP checkFunction,
  int lazyFlag)
{
    Move *move;
    Move *moves;        
    int  initialSize;
    int  result;
    int  y;
    int  topbot;
#ifdef DD_DEBUG
    if (pr > 0) (void) fprintf(table->out,
                               "ddGroupSiftingAux from %d to %d\n",xLow,xHigh);
    assert((unsigned) x >= table->subtables[x].next); 
#endif
    initialSize = table->keys - table->isolated;
    moves = NULL;
    originalSize = initialSize;         
    if ((unsigned) x == table->subtables[x].next) {
        for (y = x; y > xLow; y--) {
            if (!checkFunction(table,y-1,y))
                break;
            topbot = table->subtables[y-1].next; 
            table->subtables[y-1].next = y;
            table->subtables[x].next = topbot; 
            y = topbot + 1; 
        }
        for (y = x; y < xHigh; y++) {
            if (!checkFunction(table,y,y+1))
                break;
            topbot = y + 1;
            while ((unsigned) topbot < table->subtables[topbot].next) {
                topbot = table->subtables[topbot].next;
            }
            table->subtables[topbot].next = table->subtables[y].next;
            table->subtables[y].next = y + 1;
            y = topbot - 1; 
        }
    }
    while ((unsigned) x < table->subtables[x].next)
        x = table->subtables[x].next;
    if (x == xLow) { 
#ifdef DD_DEBUG
        assert((unsigned) x == table->subtables[x].next);
#endif
        if (x == xHigh) return(1);      
        if (!ddGroupSiftingDown(table,x,xHigh,checkFunction,&moves))
            goto ddGroupSiftingAuxOutOfMem;
        result = ddGroupSiftingBackward(table,moves,initialSize,
                                        DD_SIFT_DOWN,lazyFlag);
#ifdef DD_DEBUG
        assert(table->keys - table->isolated <= (unsigned) initialSize);
#endif
        if (!result) goto ddGroupSiftingAuxOutOfMem;
    } else if (cuddNextHigh(table,x) > xHigh) { 
#ifdef DD_DEBUG
        assert((unsigned) x >= table->subtables[x].next);
#endif
        x = table->subtables[x].next;
        if (!ddGroupSiftingUp(table,x,xLow,checkFunction,&moves))
            goto ddGroupSiftingAuxOutOfMem;
        result = ddGroupSiftingBackward(table,moves,initialSize,
                                        DD_SIFT_UP,lazyFlag);
#ifdef DD_DEBUG
        assert(table->keys - table->isolated <= (unsigned) initialSize);
#endif
        if (!result) goto ddGroupSiftingAuxOutOfMem;
    } else if (x - xLow > xHigh - x) { 
        if (!ddGroupSiftingDown(table,x,xHigh,checkFunction,&moves))
            goto ddGroupSiftingAuxOutOfMem;
        if (moves) {
            x = moves->y;
        }
        while ((unsigned) x < table->subtables[x].next)
            x = table->subtables[x].next;
        x = table->subtables[x].next;
#ifdef DD_DEBUG
        assert((unsigned) x <= table->subtables[x].next);
#endif
        if (!ddGroupSiftingUp(table,x,xLow,checkFunction,&moves))
            goto ddGroupSiftingAuxOutOfMem;
        result = ddGroupSiftingBackward(table,moves,initialSize,
                                        DD_SIFT_UP,lazyFlag);
#ifdef DD_DEBUG
        assert(table->keys - table->isolated <= (unsigned) initialSize);
#endif
        if (!result) goto ddGroupSiftingAuxOutOfMem;
    } else { 
        x = table->subtables[x].next;
        if (!ddGroupSiftingUp(table,x,xLow,checkFunction,&moves))
            goto ddGroupSiftingAuxOutOfMem;
        if (moves) {
            x = moves->x;
        }
        while ((unsigned) x < table->subtables[x].next)
            x = table->subtables[x].next;
#ifdef DD_DEBUG
        assert((unsigned) x >= table->subtables[x].next);
#endif
        if (!ddGroupSiftingDown(table,x,xHigh,checkFunction,&moves))
            goto ddGroupSiftingAuxOutOfMem;
        result = ddGroupSiftingBackward(table,moves,initialSize,
                                        DD_SIFT_DOWN,lazyFlag);
#ifdef DD_DEBUG
        assert(table->keys - table->isolated <= (unsigned) initialSize);
#endif
        if (!result) goto ddGroupSiftingAuxOutOfMem;
    }
    while (moves != NULL) {
        move = moves->next;
        cuddDeallocMove(table, moves);
        moves = move;
    }
    return(1);
ddGroupSiftingAuxOutOfMem:
    while (moves != NULL) {
        move = moves->next;
        cuddDeallocMove(table, moves);
        moves = move;
    }
    return(0);
}
static int ddGroupSiftingAux ( DdManager * table , int x , int xLow , int xHigh , DD_CHKFP checkFunction , int lazyFlag ) { Move * move ; Move * moves ; int initialSize ; int result ; int y ; int topbot ; #ifdef DD_DEBUG if ( pr > 0 ) ( void ) fprintf ( table -> out , " \n " , xLow , xHigh ) ; assert ( ( unsigned ) x >= table -> subtables [ x ] . next ) ; #endif initialSize = table -> keys - table -> isolated ; moves = NULL ; originalSize = initialSize ; if ( ( unsigned ) x == table -> subtables [ x ] . next ) { for ( y = x ; y > xLow ; y -- ) { if ( ! checkFunction ( table , y - 1 , y ) ) break ; topbot = table -> subtables [ y - 1 ] . next ; table -> subtables [ y - 1 ] . next = y ; table -> subtables [ x ] . next = topbot ; y = topbot + 1 ; } for ( y = x ; y < xHigh ; y ++ ) { if ( ! checkFunction ( table , y , y + 1 ) ) break ; topbot = y + 1 ; while ( ( unsigned ) topbot < table -> subtables [ topbot ] . next ) { topbot = table -> subtables [ topbot ] . next ; } table -> subtables [ topbot ] . next = table -> subtables [ y ] . next ; table -> subtables [ y ] . next = y + 1 ; y = topbot - 1 ; } } while ( ( unsigned ) x < table -> subtables [ x ] . next ) x = table -> subtables [ x ] . next ; if ( x == xLow ) { #ifdef DD_DEBUG assert ( ( unsigned ) x == table -> subtables [ x ] . next ) ; #endif if ( x == xHigh ) return ( 1 ) ; if ( ! ddGroupSiftingDown ( table , x , xHigh , checkFunction , & moves ) ) goto ddGroupSiftingAuxOutOfMem ; result = ddGroupSiftingBackward ( table , moves , initialSize , DD_SIFT_DOWN , lazyFlag ) ; #ifdef DD_DEBUG assert ( table -> keys - table -> isolated <= ( unsigned ) initialSize ) ; #endif if ( ! result ) goto ddGroupSiftingAuxOutOfMem ; } else if ( cuddNextHigh ( table , x ) > xHigh ) { #ifdef DD_DEBUG assert ( ( unsigned ) x >= table -> subtables [ x ] . next ) ; #endif x = table -> subtables [ x ] . next ; if ( ! ddGroupSiftingUp ( table , x , xLow , checkFunction , & moves ) ) goto ddGroupSiftingAuxOutOfMem ; result = ddGroupSiftingBackward ( table , moves , initialSize , DD_SIFT_UP , lazyFlag ) ; #ifdef DD_DEBUG assert ( table -> keys - table -> isolated <= ( unsigned ) initialSize ) ; #endif if ( ! result ) goto ddGroupSiftingAuxOutOfMem ; } else if ( x - xLow > xHigh - x ) { if ( ! ddGroupSiftingDown ( table , x , xHigh , checkFunction , & moves ) ) goto ddGroupSiftingAuxOutOfMem ; if ( moves ) { x = moves -> y ; } while ( ( unsigned ) x < table -> subtables [ x ] . next ) x = table -> subtables [ x ] . next ; x = table -> subtables [ x ] . next ; #ifdef DD_DEBUG assert ( ( unsigned ) x <= table -> subtables [ x ] . next ) ; #endif if ( ! ddGroupSiftingUp ( table , x , xLow , checkFunction , & moves ) ) goto ddGroupSiftingAuxOutOfMem ; result = ddGroupSiftingBackward ( table , moves , initialSize , DD_SIFT_UP , lazyFlag ) ; #ifdef DD_DEBUG assert ( table -> keys - table -> isolated <= ( unsigned ) initialSize ) ; #endif if ( ! result ) goto ddGroupSiftingAuxOutOfMem ; } else { x = table -> subtables [ x ] . next ; if ( ! ddGroupSiftingUp ( table , x , xLow , checkFunction , & moves ) ) goto ddGroupSiftingAuxOutOfMem ; if ( moves ) { x = moves -> x ; } while ( ( unsigned ) x < table -> subtables [ x ] . next ) x = table -> subtables [ x ] . next ; #ifdef DD_DEBUG assert ( ( unsigned ) x >= table -> subtables [ x ] . next ) ; #endif if ( ! ddGroupSiftingDown ( table , x , xHigh , checkFunction , & moves ) ) goto ddGroupSiftingAuxOutOfMem ; result = ddGroupSiftingBackward ( table , moves , initialSize , DD_SIFT_DOWN , lazyFlag ) ; #ifdef DD_DEBUG assert ( table -> keys - table -> isolated <= ( unsigned ) initialSize ) ; #endif if ( ! result ) goto ddGroupSiftingAuxOutOfMem ; } while ( moves != NULL ) { move = moves -> next ; cuddDeallocMove ( table , moves ) ; moves = move ; } return ( 1 ) ; ddGroupSiftingAuxOutOfMem : while ( moves != NULL ) { move = moves -> next ; cuddDeallocMove ( table , moves ) ; moves = move ; } return ( 0 ) ; }
Function
Synopsis    [Sifts one variable up and down until it has taken all
positions.
Function Synopsis [ Sifts one variable up and down until it has taken all positions .
/* list of moves */ /* x is bottom of group */ /* for lazy sifting */ /* If we have a singleton, we check for aggregation in both
    ** directions before we sift.
    */ /* Will go down first, unless x == xHigh:
        ** Look for aggregation above x.
        */ /* find top of y-1's group */ /* x is bottom of group so its */ /* next is top of y-1's group */ /* add 1 for y--; new y is top of group */ /* Will go up first unless x == xlow:
        ** Look for aggregation below x.
        */ /* find bottom of y+1's group */ /* subtract 1 for y++; new y is bottom of group */ /* Now x may be in the middle of a group.
    ** Find bottom of x's group.
    */ /* Sift down */ /* x must be a singleton */ /* just one variable */ /* at this point x == xHigh, unless early term */ /* move backward and stop at best position */ /* Sift up */ /* x is bottom of group */ /* Find top of x's group */ /* at this point x == xLow, unless early term */ /* move backward and stop at best position */ /* must go down first: shorter */ /* at this point x == xHigh, unless early term */ /* Find top of group */ /* x should be the top of a group */ /* move backward and stop at best position */ /* moving up first: shorter */ /* Find top of x's group */ /* at this point x == xHigh, unless early term */ /* x is bottom of a group */ /* move backward and stop at best position */