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

  Synopsis [Moves x down until either it reaches the bound (x_high) or
  the size of the ZDD heap increases too much.]

  Description [Moves x down until either it reaches the bound (x_high)
  or the size of the ZDD heap increases too much. Assumes that x is the
  bottom of a symmetry group. Checks x for symmetry to the adjacent
  variables. If symmetry is found, the symmetry group of x is merged
  with the symmetry group of the other variable. Returns the set of
  moves in case of success; ZDD_MV_OOM if memory is full.]

  SideEffects [None]

  SeeAlso     []

******************************************************************************/
Function
Synopsis [Moves x down until either it reaches the bound (x_high) or
the size of the ZDD heap increases too much.]

Description [Moves x down until either it reaches the bound (x_high)
or the size of the ZDD heap increases too much. Assumes that x is the
bottom of a symmetry group. Checks x for symmetry to the adjacent
variables. If symmetry is found, the symmetry group of x is merged
with the symmetry group of the other variable. Returns the set of
moves in case of success; ZDD_MV_OOM if memory is full.]




Function Synopsis [ Moves x down until either it reaches the bound ( x_high ) or the size of the ZDD heap increases too much . ] Description [ Moves x down until either it reaches the bound ( x_high ) or the size of the ZDD heap increases too much . Assumes that x is the bottom of a symmetry group . Checks x for symmetry to the adjacent variables . If symmetry is found the symmetry group of x is merged with the symmetry group of the other variable . Returns the set of moves in case of success ; ZDD_MV_OOM if memory is full . ]
static Move *
cuddZddSymmSifting_down(
  DdManager * table,
  int  x,
  int  x_high,
  int  initial_size)
{
    Move        *moves;
    Move        *move;
    int         y;
    int         size;
    int         limit_size = initial_size;
    int         i, gxtop, gybot;
    moves = NULL;
    y = cuddZddNextHigh(table, x);
    while (y <= x_high) {
        gybot = table->subtableZ[y].next;
        while (table->subtableZ[gybot].next != (unsigned) y)
            gybot = table->subtableZ[gybot].next;
        if (cuddZddSymmCheck(table, x, y)) {
            gxtop = table->subtableZ[x].next;
            table->subtableZ[x].next = y;
            i = table->subtableZ[y].next;
            while (table->subtableZ[i].next != (unsigned) y)
                i = table->subtableZ[i].next;
            table->subtableZ[i].next = gxtop;
        }
        else if ((table->subtableZ[x].next == (unsigned) x) &&
            (table->subtableZ[y].next == (unsigned) y)) {
            size = cuddZddSwapInPlace(table, x, y);
            if (size == 0)
                goto cuddZddSymmSifting_downOutOfMem;
            move = (Move *)cuddDynamicAllocNode(table);
            if (move == NULL)
                goto cuddZddSymmSifting_downOutOfMem;
            move->x = x;
            move->y = y;
            move->size = size;
            move->next = moves;
            moves = move;
            if ((double)size >
                (double)limit_size * table->maxGrowth)
                return(moves);
            if (size < limit_size)
                limit_size = size;
            x = y;
            y = cuddZddNextHigh(table, x);
        }
        else { 
            size = zdd_group_move(table, x, y, &moves);
            if ((double)size >
                (double)limit_size * table->maxGrowth)
                return(moves);
            if (size < limit_size)
                limit_size = size;
        }
        x = gybot;
        y = cuddZddNextHigh(table, x);
    }
    return(moves);
cuddZddSymmSifting_downOutOfMem:
    while (moves != NULL) {
        move = moves->next;
        cuddDeallocMove(table, moves);
        moves = move;
    }
    return(ZDD_MV_OOM);
}
static Move * cuddZddSymmSifting_down ( DdManager * table , int x , int x_high , int initial_size ) { Move * moves ; Move * move ; int y ; int size ; int limit_size = initial_size ; int i , gxtop , gybot ; moves = NULL ; y = cuddZddNextHigh ( table , x ) ; while ( y <= x_high ) { gybot = table -> subtableZ [ y ] . next ; while ( table -> subtableZ [ gybot ] . next != ( unsigned ) y ) gybot = table -> subtableZ [ gybot ] . next ; if ( cuddZddSymmCheck ( table , x , y ) ) { gxtop = table -> subtableZ [ x ] . next ; table -> subtableZ [ x ] . next = y ; i = table -> subtableZ [ y ] . next ; while ( table -> subtableZ [ i ] . next != ( unsigned ) y ) i = table -> subtableZ [ i ] . next ; table -> subtableZ [ i ] . next = gxtop ; } else if ( ( table -> subtableZ [ x ] . next == ( unsigned ) x ) && ( table -> subtableZ [ y ] . next == ( unsigned ) y ) ) { size = cuddZddSwapInPlace ( table , x , y ) ; if ( size == 0 ) goto cuddZddSymmSifting_downOutOfMem ; move = ( Move * ) cuddDynamicAllocNode ( table ) ; if ( move == NULL ) goto cuddZddSymmSifting_downOutOfMem ; move -> x = x ; move -> y = y ; move -> size = size ; move -> next = moves ; moves = move ; if ( ( double ) size > ( double ) limit_size * table -> maxGrowth ) return ( moves ) ; if ( size < limit_size ) limit_size = size ; x = y ; y = cuddZddNextHigh ( table , x ) ; } else { size = zdd_group_move ( table , x , y , & moves ) ; if ( ( double ) size > ( double ) limit_size * table -> maxGrowth ) return ( moves ) ; if ( size < limit_size ) limit_size = size ; } x = gybot ; y = cuddZddNextHigh ( table , x ) ; } return ( moves ) ; cuddZddSymmSifting_downOutOfMem : while ( moves != NULL ) { move = moves -> next ; cuddDeallocMove ( table , moves ) ; moves = move ; } return ( ZDD_MV_OOM ) ; }
Function
Synopsis [Moves x down until either it reaches the bound (x_high) or
the size of the ZDD heap increases too much.]
Function Synopsis [ Moves x down until either it reaches the bound ( x_high ) or the size of the ZDD heap increases too much . ]
/* Symmetry found, attach symm groups */ /* x and y have self symmetry */ /* Group move */