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

  Synopsis    [Sifts down a variable until it reaches position xHigh.]

  Description [Sifts down a variable until it reaches position xHigh.
  Assumes that x is the bottom of a group (or a singleton).  Records
  all the moves.  Returns 1 in case of success; 0 otherwise.]

  SideEffects [None]

******************************************************************************/
Function
Synopsis    [Sifts down a variable until it reaches position xHigh.]

Description [Sifts down a variable until it reaches position xHigh.
Assumes that x is the bottom of a group (or a singleton).  Records
all the moves.  Returns 1 in case of success; 0 otherwise.]


Function Synopsis [ Sifts down a variable until it reaches position xHigh . ] Description [ Sifts down a variable until it reaches position xHigh . Assumes that x is the bottom of a group ( or a singleton ) . Records all the moves . Returns 1 in case of success ; 0 otherwise . ]
static int
zddGroupSiftingDown(
  DdManager * table,
  int  x,
  int  xHigh,
  Move ** moves)
{
    Move *move;
    int  y;
    int  size;
    int  limitSize;
    int  gybot;
    limitSize = size = table->keysZ;
    y = cuddZddNextHigh(table,x);
    while (y <= xHigh) {
        gybot = table->subtableZ[y].next;
        while (table->subtableZ[gybot].next != (unsigned) y)
            gybot = table->subtableZ[gybot].next;
        if (table->subtableZ[x].next == (unsigned) x &&
            table->subtableZ[y].next == (unsigned) y) {
            size = cuddZddSwapInPlace(table,x,y);
#ifdef DD_DEBUG
            assert(table->subtableZ[x].next == (unsigned) x);
            assert(table->subtableZ[y].next == (unsigned) y);
#endif
            if (size == 0) goto zddGroupSiftingDownOutOfMem;
            move = (Move *) cuddDynamicAllocNode(table);
            if (move == NULL) goto zddGroupSiftingDownOutOfMem;
            move->x = x;
            move->y = y;
            move->flags = MTR_DEFAULT;
            move->size = size;
            move->next = *moves;
            *moves = move;
#ifdef DD_DEBUG
            if (pr > 0) (void) fprintf(table->out,"zddGroupSiftingDown (2 single groups):\n");
#endif
            if ((double) size > (double) limitSize * table->maxGrowth)
                return(1);
            if (size < limitSize) limitSize = size;
            x = y;
            y = cuddZddNextHigh(table,x);
        } else { 
            size = zddGroupMove(table,x,y,moves);
            if (size == 0) goto zddGroupSiftingDownOutOfMem;
            if ((double) size > (double) limitSize * table->maxGrowth)
                return(1);
            if (size < limitSize) limitSize = size;
        }
        x = gybot;
        y = cuddZddNextHigh(table,x);
    }
    return(1);
zddGroupSiftingDownOutOfMem:
    while (*moves != NULL) {
        move = (*moves)->next;
        cuddDeallocMove(table, *moves);
        *moves = move;
    }
    return(0);
}
static int zddGroupSiftingDown ( DdManager * table , int x , int xHigh , Move * * moves ) { Move * move ; int y ; int size ; int limitSize ; int gybot ; limitSize = size = table -> keysZ ; y = cuddZddNextHigh ( table , x ) ; while ( y <= xHigh ) { gybot = table -> subtableZ [ y ] . next ; while ( table -> subtableZ [ gybot ] . next != ( unsigned ) y ) gybot = table -> subtableZ [ gybot ] . next ; if ( table -> subtableZ [ x ] . next == ( unsigned ) x && table -> subtableZ [ y ] . next == ( unsigned ) y ) { size = cuddZddSwapInPlace ( table , x , y ) ; #ifdef DD_DEBUG assert ( table -> subtableZ [ x ] . next == ( unsigned ) x ) ; assert ( table -> subtableZ [ y ] . next == ( unsigned ) y ) ; #endif if ( size == 0 ) goto zddGroupSiftingDownOutOfMem ; move = ( Move * ) cuddDynamicAllocNode ( table ) ; if ( move == NULL ) goto zddGroupSiftingDownOutOfMem ; move -> x = x ; move -> y = y ; move -> flags = MTR_DEFAULT ; move -> size = size ; move -> next = * moves ; * moves = move ; #ifdef DD_DEBUG if ( pr > 0 ) ( void ) fprintf ( table -> out , " \n " ) ; #endif if ( ( double ) size > ( double ) limitSize * table -> maxGrowth ) return ( 1 ) ; if ( size < limitSize ) limitSize = size ; x = y ; y = cuddZddNextHigh ( table , x ) ; } else { size = zddGroupMove ( table , x , y , moves ) ; if ( size == 0 ) goto zddGroupSiftingDownOutOfMem ; if ( ( double ) size > ( double ) limitSize * table -> maxGrowth ) return ( 1 ) ; if ( size < limitSize ) limitSize = size ; } x = gybot ; y = cuddZddNextHigh ( table , x ) ; } return ( 1 ) ; zddGroupSiftingDownOutOfMem : while ( * moves != NULL ) { move = ( * moves ) -> next ; cuddDeallocMove ( table , * moves ) ; * moves = move ; } return ( 0 ) ; }
Function
Synopsis    [Sifts down a variable until it reaches position xHigh.]
Function Synopsis [ Sifts down a variable until it reaches position xHigh . ]
/* Initialize R */ /* Find bottom of y group. */ /* x and y are self groups */ /* Record move. */ /* Group move */