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

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

  Description [Moves x down until either it reaches the bound (xHigh)
  or the size of the DD 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; MV_OOM if memory is full.]

  SideEffects [None]

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

Description [Moves x down until either it reaches the bound (xHigh)
or the size of the DD 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; MV_OOM if memory is full.]


Function Synopsis [ Moves x down until either it reaches the bound ( xHigh ) or the size of the DD heap increases too much . ] Description [ Moves x down until either it reaches the bound ( xHigh ) or the size of the DD 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 ; MV_OOM if memory is full . ]
static Move *
ddSymmSiftingDown(
  DdManager * table,
  int  x,
  int  xHigh)
{
    Move *moves;
    Move *move;
    int  y;
    int  size;
    int  limitSize;
    int  gxtop,gybot;
    int  R;     
    int  xindex, yindex;
    int  isolated;
    int  z;
    int  zindex;
#ifdef DD_DEBUG
    int  checkR;
#endif
    moves = NULL;
    xindex = table->invperm[x];
    gxtop = table->subtables[x].next;
    limitSize = size = table->keys - table->isolated;
    R = 0;
    for (z = xHigh; z > gxtop; z--) {
        zindex = table->invperm[z];
        if (zindex == xindex || cuddTestInteract(table,xindex,zindex)) {
            isolated = table->vars[zindex]->ref == 1;
            R += table->subtables[z].keys - isolated;
        }
    }
    y = cuddNextHigh(table,x);
    while (y <= xHigh && size - R < limitSize) {
#ifdef DD_DEBUG
        gxtop = table->subtables[x].next;
        checkR = 0;
        for (z = xHigh; z > gxtop; z--) {
            zindex = table->invperm[z];
            if (zindex == xindex || cuddTestInteract(table,xindex,zindex)) {
                isolated = table->vars[zindex]->ref == 1;
                checkR += table->subtables[z].keys - isolated;
            }
        }
        assert(R == checkR);
#endif
        gybot = table->subtables[y].next;
        while (table->subtables[gybot].next != (unsigned) y)
            gybot = table->subtables[gybot].next;
        if (cuddSymmCheck(table,x,y)) {
            gxtop = table->subtables[x].next;
            table->subtables[x].next = y;
            table->subtables[gybot].next = gxtop;
        } else if (table->subtables[x].next == (unsigned) x &&
                   table->subtables[y].next == (unsigned) y) {
            yindex = table->invperm[y];
            if (cuddTestInteract(table,xindex,yindex)) {
                isolated = table->vars[yindex]->ref == 1;
                R -= table->subtables[y].keys - isolated;
            }
            size = cuddSwapInPlace(table,x,y);
#ifdef DD_DEBUG
            assert(table->subtables[x].next == (unsigned) x);
            assert(table->subtables[y].next == (unsigned) y);
#endif
            if (size == 0) goto ddSymmSiftingDownOutOfMem;
            move = (Move *) cuddDynamicAllocNode(table);
            if (move == NULL) goto ddSymmSiftingDownOutOfMem;
            move->x = x;
            move->y = y;
            move->size = size;
            move->next = moves;
            moves = move;
            if ((double) size > (double) limitSize * table->maxGrowth)
                return(moves);
            if (size < limitSize) limitSize = size;
        } else { 
            gxtop = table->subtables[x].next;
            z = gxtop + 1;
            do {
                zindex = table->invperm[z];
                if (zindex == xindex || cuddTestInteract(table,xindex,zindex)) {
                    isolated = table->vars[zindex]->ref == 1;
                    R -= table->subtables[z].keys - isolated;
                }
                z++;
            } while (z <= gybot);
            size = ddSymmGroupMove(table,x,y,&moves);
            if (size == 0) goto ddSymmSiftingDownOutOfMem;
            if ((double) size > (double) limitSize * table->maxGrowth)
                return(moves);
            if (size < limitSize) limitSize = size;
            gxtop = table->subtables[gybot].next;
            for (z = gxtop + 1; z <= gybot; z++) {
                zindex = table->invperm[z];
                if (zindex == xindex || cuddTestInteract(table,xindex,zindex)) {
                    isolated = table->vars[zindex]->ref == 1;
                    R += table->subtables[z].keys - isolated;
                }
            }
        }
        x = gybot;
        y = cuddNextHigh(table,x);
    }
    return(moves);
ddSymmSiftingDownOutOfMem:
    while (moves != NULL) {
        move = moves->next;
        cuddDeallocMove(table, moves);
        moves = move;
    }
    return(MV_OOM);
}
static Move * ddSymmSiftingDown ( DdManager * table , int x , int xHigh ) { Move * moves ; Move * move ; int y ; int size ; int limitSize ; int gxtop , gybot ; int R ; int xindex , yindex ; int isolated ; int z ; int zindex ; #ifdef DD_DEBUG int checkR ; #endif moves = NULL ; xindex = table -> invperm [ x ] ; gxtop = table -> subtables [ x ] . next ; limitSize = size = table -> keys - table -> isolated ; R = 0 ; for ( z = xHigh ; z > gxtop ; z -- ) { zindex = table -> invperm [ z ] ; if ( zindex == xindex || cuddTestInteract ( table , xindex , zindex ) ) { isolated = table -> vars [ zindex ] -> ref == 1 ; R += table -> subtables [ z ] . keys - isolated ; } } y = cuddNextHigh ( table , x ) ; while ( y <= xHigh && size - R < limitSize ) { #ifdef DD_DEBUG gxtop = table -> subtables [ x ] . next ; checkR = 0 ; for ( z = xHigh ; z > gxtop ; z -- ) { zindex = table -> invperm [ z ] ; if ( zindex == xindex || cuddTestInteract ( table , xindex , zindex ) ) { isolated = table -> vars [ zindex ] -> ref == 1 ; checkR += table -> subtables [ z ] . keys - isolated ; } } assert ( R == checkR ) ; #endif gybot = table -> subtables [ y ] . next ; while ( table -> subtables [ gybot ] . next != ( unsigned ) y ) gybot = table -> subtables [ gybot ] . next ; if ( cuddSymmCheck ( table , x , y ) ) { gxtop = table -> subtables [ x ] . next ; table -> subtables [ x ] . next = y ; table -> subtables [ gybot ] . next = gxtop ; } else if ( table -> subtables [ x ] . next == ( unsigned ) x && table -> subtables [ y ] . next == ( unsigned ) y ) { yindex = table -> invperm [ y ] ; if ( cuddTestInteract ( table , xindex , yindex ) ) { isolated = table -> vars [ yindex ] -> ref == 1 ; R -= table -> subtables [ y ] . keys - isolated ; } size = cuddSwapInPlace ( table , x , y ) ; #ifdef DD_DEBUG assert ( table -> subtables [ x ] . next == ( unsigned ) x ) ; assert ( table -> subtables [ y ] . next == ( unsigned ) y ) ; #endif if ( size == 0 ) goto ddSymmSiftingDownOutOfMem ; move = ( Move * ) cuddDynamicAllocNode ( table ) ; if ( move == NULL ) goto ddSymmSiftingDownOutOfMem ; move -> x = x ; move -> y = y ; move -> size = size ; move -> next = moves ; moves = move ; if ( ( double ) size > ( double ) limitSize * table -> maxGrowth ) return ( moves ) ; if ( size < limitSize ) limitSize = size ; } else { gxtop = table -> subtables [ x ] . next ; z = gxtop + 1 ; do { zindex = table -> invperm [ z ] ; if ( zindex == xindex || cuddTestInteract ( table , xindex , zindex ) ) { isolated = table -> vars [ zindex ] -> ref == 1 ; R -= table -> subtables [ z ] . keys - isolated ; } z ++ ; } while ( z <= gybot ) ; size = ddSymmGroupMove ( table , x , y , & moves ) ; if ( size == 0 ) goto ddSymmSiftingDownOutOfMem ; if ( ( double ) size > ( double ) limitSize * table -> maxGrowth ) return ( moves ) ; if ( size < limitSize ) limitSize = size ; gxtop = table -> subtables [ gybot ] . next ; for ( z = gxtop + 1 ; z <= gybot ; z ++ ) { zindex = table -> invperm [ z ] ; if ( zindex == xindex || cuddTestInteract ( table , xindex , zindex ) ) { isolated = table -> vars [ zindex ] -> ref == 1 ; R += table -> subtables [ z ] . keys - isolated ; } } } x = gybot ; y = cuddNextHigh ( table , x ) ; } return ( moves ) ; ddSymmSiftingDownOutOfMem : while ( moves != NULL ) { move = moves -> next ; cuddDeallocMove ( table , moves ) ; moves = move ; } return ( MV_OOM ) ; }
Function
Synopsis    [Moves x down until either it reaches the bound (xHigh) or
the size of the DD heap increases too much.]
Function Synopsis [ Moves x down until either it reaches the bound ( xHigh ) or the size of the DD heap increases too much . ]
/* upper bound on node decrease */ /* Initialize R */ /* Symmetry found, attach symm groups */ /* x and y have self symmetry */ /* Update upper bound on node decrease. */ /* Group move */ /* Update upper bound on node decrease: first phase. */ /* Update upper bound on node decrease: second phase. */