abc/src/bdd/cudd/cuddZddGroup.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
zddGroupSiftingAux(
  DdManager * table,
  int  x,
  int  xLow,
  int  xHigh)
{
    Move *move;
    Move *moves;        
    int  initialSize;
    int  result;
#ifdef DD_DEBUG
    if (pr > 0) (void) fprintf(table->out,"zddGroupSiftingAux from %d to %d\n",xLow,xHigh);
    assert((unsigned) x >= table->subtableZ[x].next); 
#endif
    initialSize = table->keysZ;
    moves = NULL;
    if (x == xLow) { 
#ifdef DD_DEBUG
        assert((unsigned) x == table->subtableZ[x].next);
#endif
        if (x == xHigh) return(1);      
        if (!zddGroupSiftingDown(table,x,xHigh,&moves))
            goto zddGroupSiftingAuxOutOfMem;
        result = zddGroupSiftingBackward(table,moves,initialSize);
#ifdef DD_DEBUG
        assert(table->keysZ <= (unsigned) initialSize);
#endif
        if (!result) goto zddGroupSiftingAuxOutOfMem;
    } else if (cuddZddNextHigh(table,x) > xHigh) { 
#ifdef DD_DEBUG
        assert((unsigned) x >= table->subtableZ[x].next);
#endif
        x = table->subtableZ[x].next;
        if (!zddGroupSiftingUp(table,x,xLow,&moves))
            goto zddGroupSiftingAuxOutOfMem;
        result = zddGroupSiftingBackward(table,moves,initialSize);
#ifdef DD_DEBUG
        assert(table->keysZ <= (unsigned) initialSize);
#endif
        if (!result) goto zddGroupSiftingAuxOutOfMem;
    } else if (x - xLow > xHigh - x) { 
        if (!zddGroupSiftingDown(table,x,xHigh,&moves))
            goto zddGroupSiftingAuxOutOfMem;
        if (moves) {
            x = moves->y;
        }
        while ((unsigned) x < table->subtableZ[x].next)
            x = table->subtableZ[x].next;
        x = table->subtableZ[x].next;
#ifdef DD_DEBUG
        assert((unsigned) x <= table->subtableZ[x].next);
#endif
        if (!zddGroupSiftingUp(table,x,xLow,&moves))
            goto zddGroupSiftingAuxOutOfMem;
        result = zddGroupSiftingBackward(table,moves,initialSize);
#ifdef DD_DEBUG
        assert(table->keysZ <= (unsigned) initialSize);
#endif
        if (!result) goto zddGroupSiftingAuxOutOfMem;
    } else { 
        x = table->subtableZ[x].next;
        if (!zddGroupSiftingUp(table,x,xLow,&moves))
            goto zddGroupSiftingAuxOutOfMem;
        if (moves) {
            x = moves->x;
        }
        while ((unsigned) x < table->subtableZ[x].next)
            x = table->subtableZ[x].next;
#ifdef DD_DEBUG
        assert((unsigned) x >= table->subtableZ[x].next);
#endif
        if (!zddGroupSiftingDown(table,x,xHigh,&moves))
            goto zddGroupSiftingAuxOutOfMem;
        result = zddGroupSiftingBackward(table,moves,initialSize);
#ifdef DD_DEBUG
        assert(table->keysZ <= (unsigned) initialSize);
#endif
        if (!result) goto zddGroupSiftingAuxOutOfMem;
    }
    while (moves != NULL) {
        move = moves->next;
        cuddDeallocMove(table, moves);
        moves = move;
    }
    return(1);
zddGroupSiftingAuxOutOfMem:
    while (moves != NULL) {
        move = moves->next;
        cuddDeallocMove(table, moves);
        moves = move;
    }
    return(0);
}
static int zddGroupSiftingAux ( DdManager * table , int x , int xLow , int xHigh ) { Move * move ; Move * moves ; int initialSize ; int result ; #ifdef DD_DEBUG if ( pr > 0 ) ( void ) fprintf ( table -> out , " \n " , xLow , xHigh ) ; assert ( ( unsigned ) x >= table -> subtableZ [ x ] . next ) ; #endif initialSize = table -> keysZ ; moves = NULL ; if ( x == xLow ) { #ifdef DD_DEBUG assert ( ( unsigned ) x == table -> subtableZ [ x ] . next ) ; #endif if ( x == xHigh ) return ( 1 ) ; if ( ! zddGroupSiftingDown ( table , x , xHigh , & moves ) ) goto zddGroupSiftingAuxOutOfMem ; result = zddGroupSiftingBackward ( table , moves , initialSize ) ; #ifdef DD_DEBUG assert ( table -> keysZ <= ( unsigned ) initialSize ) ; #endif if ( ! result ) goto zddGroupSiftingAuxOutOfMem ; } else if ( cuddZddNextHigh ( table , x ) > xHigh ) { #ifdef DD_DEBUG assert ( ( unsigned ) x >= table -> subtableZ [ x ] . next ) ; #endif x = table -> subtableZ [ x ] . next ; if ( ! zddGroupSiftingUp ( table , x , xLow , & moves ) ) goto zddGroupSiftingAuxOutOfMem ; result = zddGroupSiftingBackward ( table , moves , initialSize ) ; #ifdef DD_DEBUG assert ( table -> keysZ <= ( unsigned ) initialSize ) ; #endif if ( ! result ) goto zddGroupSiftingAuxOutOfMem ; } else if ( x - xLow > xHigh - x ) { if ( ! zddGroupSiftingDown ( table , x , xHigh , & moves ) ) goto zddGroupSiftingAuxOutOfMem ; if ( moves ) { x = moves -> y ; } while ( ( unsigned ) x < table -> subtableZ [ x ] . next ) x = table -> subtableZ [ x ] . next ; x = table -> subtableZ [ x ] . next ; #ifdef DD_DEBUG assert ( ( unsigned ) x <= table -> subtableZ [ x ] . next ) ; #endif if ( ! zddGroupSiftingUp ( table , x , xLow , & moves ) ) goto zddGroupSiftingAuxOutOfMem ; result = zddGroupSiftingBackward ( table , moves , initialSize ) ; #ifdef DD_DEBUG assert ( table -> keysZ <= ( unsigned ) initialSize ) ; #endif if ( ! result ) goto zddGroupSiftingAuxOutOfMem ; } else { x = table -> subtableZ [ x ] . next ; if ( ! zddGroupSiftingUp ( table , x , xLow , & moves ) ) goto zddGroupSiftingAuxOutOfMem ; if ( moves ) { x = moves -> x ; } while ( ( unsigned ) x < table -> subtableZ [ x ] . next ) x = table -> subtableZ [ x ] . next ; #ifdef DD_DEBUG assert ( ( unsigned ) x >= table -> subtableZ [ x ] . next ) ; #endif if ( ! zddGroupSiftingDown ( table , x , xHigh , & moves ) ) goto zddGroupSiftingAuxOutOfMem ; result = zddGroupSiftingBackward ( table , moves , initialSize ) ; #ifdef DD_DEBUG assert ( table -> keysZ <= ( unsigned ) initialSize ) ; #endif if ( ! result ) goto zddGroupSiftingAuxOutOfMem ; } while ( moves != NULL ) { move = moves -> next ; cuddDeallocMove ( table , moves ) ; moves = move ; } return ( 1 ) ; zddGroupSiftingAuxOutOfMem : 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 */ /* 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 */