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

  Synopsis    [Sifts up a variable until either it reaches position xLow
  or the size of the DD heap increases too much.]

  Description [Sifts up a variable until either it reaches position
  xLow or the size of the DD heap increases too much. Assumes that y is
  the top of a group (or a singleton).  Checks y for aggregation to the
  adjacent variables. Records all the moves that are appended to the
  list of moves received as input and returned as a side effect.
  Returns 1 in case of success; 0 otherwise.]

  SideEffects [None]

******************************************************************************/
Function
Synopsis    [Sifts up a variable until either it reaches position xLow
or the size of the DD heap increases too much.]

Description [Sifts up a variable until either it reaches position
xLow or the size of the DD heap increases too much. Assumes that y is
the top of a group (or a singleton).  Checks y for aggregation to the
adjacent variables. Records all the moves that are appended to the
list of moves received as input and returned as a side effect.
Returns 1 in case of success; 0 otherwise.]


Function Synopsis [ Sifts up a variable until either it reaches position xLow or the size of the DD heap increases too much . ] Description [ Sifts up a variable until either it reaches position xLow or the size of the DD heap increases too much . Assumes that y is the top of a group ( or a singleton ) . Checks y for aggregation to the adjacent variables . Records all the moves that are appended to the list of moves received as input and returned as a side effect . Returns 1 in case of success ; 0 otherwise . ]
static int
zddGroupSiftingUp(
  DdManager * table,
  int  y,
  int  xLow,
  Move ** moves)
{
    Move *move;
    int  x;
    int  size;
    int  gxtop;
    int  limitSize;
    limitSize = table->keysZ;
    x = cuddZddNextLow(table,y);
    while (x >= xLow) {
        gxtop = table->subtableZ[x].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 zddGroupSiftingUpOutOfMem;
            move = (Move *)cuddDynamicAllocNode(table);
            if (move == NULL) goto zddGroupSiftingUpOutOfMem;
            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,"zddGroupSiftingUp (2 single groups):\n");
#endif
            if ((double) size > (double) limitSize * table->maxGrowth)
                return(1);
            if (size < limitSize) limitSize = size;
        } else { 
            size = zddGroupMove(table,x,y,moves);
            if (size == 0) goto zddGroupSiftingUpOutOfMem;
            if ((double) size > (double) limitSize * table->maxGrowth)
                return(1);
            if (size < limitSize) limitSize = size;
        }
        y = gxtop;
        x = cuddZddNextLow(table,y);
    }
    return(1);
zddGroupSiftingUpOutOfMem:
    while (*moves != NULL) {
        move = (*moves)->next;
        cuddDeallocMove(table, *moves);
        *moves = move;
    }
    return(0);
}
static int zddGroupSiftingUp ( DdManager * table , int y , int xLow , Move * * moves ) { Move * move ; int x ; int size ; int gxtop ; int limitSize ; limitSize = table -> keysZ ; x = cuddZddNextLow ( table , y ) ; while ( x >= xLow ) { gxtop = table -> subtableZ [ x ] . 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 zddGroupSiftingUpOutOfMem ; move = ( Move * ) cuddDynamicAllocNode ( table ) ; if ( move == NULL ) goto zddGroupSiftingUpOutOfMem ; 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 ; } else { size = zddGroupMove ( table , x , y , moves ) ; if ( size == 0 ) goto zddGroupSiftingUpOutOfMem ; if ( ( double ) size > ( double ) limitSize * table -> maxGrowth ) return ( 1 ) ; if ( size < limitSize ) limitSize = size ; } y = gxtop ; x = cuddZddNextLow ( table , y ) ; } return ( 1 ) ; zddGroupSiftingUpOutOfMem : while ( * moves != NULL ) { move = ( * moves ) -> next ; cuddDeallocMove ( table , * moves ) ; * moves = move ; } return ( 0 ) ; }
Function
Synopsis    [Sifts up a variable until either it reaches position xLow
or the size of the DD heap increases too much.]
Function Synopsis [ Sifts up a variable until either it reaches position xLow or the size of the DD heap increases too much . ]
/* x and y are self groups */ /* group move */