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

  Synopsis [Swaps two groups.]

  Description [Swaps two groups. x is assumed to be the bottom variable
  of the first group. y is assumed to be the top variable of the second
  group.  Updates the list of moves. Returns the number of keys in the
  table if successful; 0 otherwise.]

  SideEffects [None]

  SeeAlso     []

******************************************************************************/
Function
Synopsis [Swaps two groups.]

Description [Swaps two groups. x is assumed to be the bottom variable
of the first group. y is assumed to be the top variable of the second
group.  Updates the list of moves. Returns the number of keys in the
table if successful; 0 otherwise.]




Function Synopsis [ Swaps two groups . ] Description [ Swaps two groups . x is assumed to be the bottom variable of the first group . y is assumed to be the top variable of the second group . Updates the list of moves . Returns the number of keys in the table if successful ; 0 otherwise . ]
static int
zdd_group_move(
  DdManager * table,
  int  x,
  int  y,
  Move ** moves)
{
    Move        *move;
    int         size;
    int         i, temp, gxtop, gxbot, gybot, yprev;
    int         swapx = -1, swapy = -1;
#ifdef DD_DEBUG
    assert(x < y);      
#endif
    gxtop = table->subtableZ[x].next;
    gxbot = x;
    gybot = table->subtableZ[y].next;
    while (table->subtableZ[gybot].next != (unsigned) y)
        gybot = table->subtableZ[gybot].next;
    yprev = gybot;
    while (x <= y) {
        while (y > gxtop) {
            temp = table->subtableZ[x].next;
            if (temp == x)
                temp = y;
            i = gxtop;
            for (;;) {
                if (table->subtableZ[i].next == (unsigned) x) {
                    table->subtableZ[i].next = y;
                    break;
                } else {
                    i = table->subtableZ[i].next;
                }
            }
            if (table->subtableZ[y].next != (unsigned) y) {
                table->subtableZ[x].next = table->subtableZ[y].next;
            } else {
                table->subtableZ[x].next = x;
            }
            if (yprev != y) {
                table->subtableZ[yprev].next = x;
            } else {
                yprev = x;
            }
            table->subtableZ[y].next = temp;
            size = cuddZddSwapInPlace(table, x, y);
            if (size == 0)
                goto zdd_group_moveOutOfMem;
            swapx = x;
            swapy = y;
            y = x;
            x--;
        } 
        if (table->subtableZ[y].next <= (unsigned) y) {
            gybot = y;
        } else {
            y = table->subtableZ[y].next;
        }
        yprev = gxtop;
        gxtop++;
        gxbot++;
        x = gxbot;
    } 
    move = (Move *)cuddDynamicAllocNode(table);
    if (move == NULL)
        goto zdd_group_moveOutOfMem;
    move->x = swapx;
    move->y = swapy;
    move->size = table->keysZ;
    move->next = *moves;
    *moves = move;
    return(table->keysZ);
zdd_group_moveOutOfMem:
    while (*moves != NULL) {
        move = (*moves)->next;
        cuddDeallocMove(table, *moves);
        *moves = move;
    }
    return(0);
}
static int zdd_group_move ( DdManager * table , int x , int y , Move * * moves ) { Move * move ; int size ; int i , temp , gxtop , gxbot , gybot , yprev ; int swapx = -1 , swapy = -1 ; #ifdef DD_DEBUG assert ( x < y ) ; #endif gxtop = table -> subtableZ [ x ] . next ; gxbot = x ; gybot = table -> subtableZ [ y ] . next ; while ( table -> subtableZ [ gybot ] . next != ( unsigned ) y ) gybot = table -> subtableZ [ gybot ] . next ; yprev = gybot ; while ( x <= y ) { while ( y > gxtop ) { temp = table -> subtableZ [ x ] . next ; if ( temp == x ) temp = y ; i = gxtop ; for ( ; ; ) { if ( table -> subtableZ [ i ] . next == ( unsigned ) x ) { table -> subtableZ [ i ] . next = y ; break ; } else { i = table -> subtableZ [ i ] . next ; } } if ( table -> subtableZ [ y ] . next != ( unsigned ) y ) { table -> subtableZ [ x ] . next = table -> subtableZ [ y ] . next ; } else { table -> subtableZ [ x ] . next = x ; } if ( yprev != y ) { table -> subtableZ [ yprev ] . next = x ; } else { yprev = x ; } table -> subtableZ [ y ] . next = temp ; size = cuddZddSwapInPlace ( table , x , y ) ; if ( size == 0 ) goto zdd_group_moveOutOfMem ; swapx = x ; swapy = y ; y = x ; x -- ; } if ( table -> subtableZ [ y ] . next <= ( unsigned ) y ) { gybot = y ; } else { y = table -> subtableZ [ y ] . next ; } yprev = gxtop ; gxtop ++ ; gxbot ++ ; x = gxbot ; } move = ( Move * ) cuddDynamicAllocNode ( table ) ; if ( move == NULL ) goto zdd_group_moveOutOfMem ; move -> x = swapx ; move -> y = swapy ; move -> size = table -> keysZ ; move -> next = * moves ; * moves = move ; return ( table -> keysZ ) ; zdd_group_moveOutOfMem : while ( * moves != NULL ) { move = ( * moves ) -> next ; cuddDeallocMove ( table , * moves ) ; * moves = move ; } return ( 0 ) ; }
Function
Synopsis [Swaps two groups.]
Function Synopsis [ Swaps two groups . ]
/* we assume that x < y */ /* Find top and bottom for the two groups. */ /* Set correct symmetries. */ /* while y > gxtop */ /* Trying to find the next y. */ /* while x <= y, end of group movement */