abc/src/bdd/cudd/cuddSymmetry.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]

******************************************************************************/
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
ddSymmGroupMove(
  DdManager * table,
  int  x,
  int  y,
  Move ** moves)
{
    Move *move;
    int  size = -1;
    int  i,j;
    int  xtop,xbot,xsize,ytop,ybot,ysize,newxtop;
    int  swapx = -1,swapy = -1;
#ifdef DD_DEBUG
    assert(x < y);      
#endif
    xbot = x;
    xtop = table->subtables[x].next;
    xsize = xbot - xtop + 1;
    ybot = y;
    while ((unsigned) ybot < table->subtables[ybot].next)
        ybot = table->subtables[ybot].next;
    ytop = y;
    ysize = ybot - ytop + 1;
    for (i = 1; i <= ysize; i++) {
        for (j = 1; j <= xsize; j++) {
            size = cuddSwapInPlace(table,x,y);
            if (size == 0) return(0);
            swapx = x; swapy = y;
            y = x;
            x = y - 1;
        }
        y = ytop + i;
        x = y - 1;
    }
    y = xtop; 
    for (i = 0; i < ysize-1 ; i++) {
        table->subtables[y].next = y + 1;
        y = y + 1;
    }
    table->subtables[y].next = xtop; 
    x = y + 1;
    newxtop = x;
    for (i = 0; i < xsize - 1 ; i++) {
        table->subtables[x].next = x + 1;
        x = x + 1;
    }
    table->subtables[x].next = newxtop; 
    move = (Move *) cuddDynamicAllocNode(table);
    if (move == NULL) return(0);
    move->x = swapx;
    move->y = swapy;
    move->size = size;
    move->next = *moves;
    *moves = move;
    return(size);
}
static int ddSymmGroupMove ( DdManager * table , int x , int y , Move * * moves ) { Move * move ; int size = -1 ; int i , j ; int xtop , xbot , xsize , ytop , ybot , ysize , newxtop ; int swapx = -1 , swapy = -1 ; #ifdef DD_DEBUG assert ( x < y ) ; #endif xbot = x ; xtop = table -> subtables [ x ] . next ; xsize = xbot - xtop + 1 ; ybot = y ; while ( ( unsigned ) ybot < table -> subtables [ ybot ] . next ) ybot = table -> subtables [ ybot ] . next ; ytop = y ; ysize = ybot - ytop + 1 ; for ( i = 1 ; i <= ysize ; i ++ ) { for ( j = 1 ; j <= xsize ; j ++ ) { size = cuddSwapInPlace ( table , x , y ) ; if ( size == 0 ) return ( 0 ) ; swapx = x ; swapy = y ; y = x ; x = y - 1 ; } y = ytop + i ; x = y - 1 ; } y = xtop ; for ( i = 0 ; i < ysize - 1 ; i ++ ) { table -> subtables [ y ] . next = y + 1 ; y = y + 1 ; } table -> subtables [ y ] . next = xtop ; x = y + 1 ; newxtop = x ; for ( i = 0 ; i < xsize - 1 ; i ++ ) { table -> subtables [ x ] . next = x + 1 ; x = x + 1 ; } table -> subtables [ x ] . next = newxtop ; move = ( Move * ) cuddDynamicAllocNode ( table ) ; if ( move == NULL ) return ( 0 ) ; move -> x = swapx ; move -> y = swapy ; move -> size = size ; move -> next = * moves ; * moves = move ; return ( size ) ; }
Function
Synopsis    [Swaps two groups.]
Function Synopsis [ Swaps two groups . ]
/* we assume that x < y */ /* Find top, bottom, and size for the two groups. */ /* Sift the variables of the second group up through the first group. */ /* fix symmetries */ /* ytop is now where xtop used to be */ /* y is bottom of its group, join */ /* its symmetry to top of its group */ /* x is bottom of its group, join */ /* its symmetry to top of its group */ /* Store group move */