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

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

  Description [Moves x up until either it reaches the bound (xLow) or
  the size of the DD heap increases too much. Assumes that x is the top
  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 up until either it reaches the bound (xLow) or
the size of the DD heap increases too much.]

Description [Moves x up until either it reaches the bound (xLow) or
the size of the DD heap increases too much. Assumes that x is the top
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 up until either it reaches the bound ( xLow ) or the size of the DD heap increases too much . ] Description [ Moves x up until either it reaches the bound ( xLow ) or the size of the DD heap increases too much . Assumes that x is the top 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 *
ddSymmSiftingUp(
  DdManager * table,
  int  y,
  int  xLow)
{
    Move *moves;
    Move *move;
    int  x;
    int  size;
    int  i;
    int  gxtop,gybot;
    int  limitSize;
    int  xindex, yindex;
    int  zindex;
    int  z;
    int  isolated;
    int  L;     
#ifdef DD_DEBUG
    int  checkL;
#endif
    moves = NULL;
    yindex = table->invperm[y];
    limitSize = L = table->keys - table->isolated;
    gybot = y;
    while ((unsigned) gybot < table->subtables[gybot].next)
        gybot = table->subtables[gybot].next;
    for (z = xLow + 1; z <= gybot; z++) {
        zindex = table->invperm[z];
        if (zindex == yindex || cuddTestInteract(table,zindex,yindex)) {
            isolated = table->vars[zindex]->ref == 1;
            L -= table->subtables[z].keys - isolated;
        }
    }
    x = cuddNextLow(table,y);
    while (x >= xLow && L <= limitSize) {
#ifdef DD_DEBUG
        gybot = y;
        while ((unsigned) gybot < table->subtables[gybot].next)
            gybot = table->subtables[gybot].next;
        checkL = table->keys - table->isolated;
        for (z = xLow + 1; z <= gybot; z++) {
            zindex = table->invperm[z];
            if (zindex == yindex || cuddTestInteract(table,zindex,yindex)) {
                isolated = table->vars[zindex]->ref == 1;
                checkL -= table->subtables[z].keys - isolated;
            }
        }
        assert(L == checkL);
#endif
        gxtop = table->subtables[x].next;
        if (cuddSymmCheck(table,x,y)) {
            table->subtables[x].next = y;
            i = table->subtables[y].next;
            while (table->subtables[i].next != (unsigned) y)
                i = table->subtables[i].next;
            table->subtables[i].next = gxtop;
        } else if (table->subtables[x].next == (unsigned) x &&
                   table->subtables[y].next == (unsigned) y) {
            xindex = table->invperm[x];
            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 ddSymmSiftingUpOutOfMem;
            if (cuddTestInteract(table,xindex,yindex)) {
                isolated = table->vars[xindex]->ref == 1;
                L += table->subtables[y].keys - isolated;
            }
            move = (Move *) cuddDynamicAllocNode(table);
            if (move == NULL) goto ddSymmSiftingUpOutOfMem;
            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 { 
            size = ddSymmGroupMove(table,x,y,&moves);
            if (size == 0) goto ddSymmSiftingUpOutOfMem;
            z = moves->y;
            do {
                zindex = table->invperm[z];
                if (cuddTestInteract(table,zindex,yindex)) {
                    isolated = table->vars[zindex]->ref == 1;
                    L += table->subtables[z].keys - isolated;
                }
                z = table->subtables[z].next;
            } while (z != (int) moves->y);
            if ((double) size > (double) limitSize * table->maxGrowth)
                return(moves);
            if (size < limitSize) limitSize = size;
        }
        y = gxtop;
        x = cuddNextLow(table,y);
    }
    return(moves);
ddSymmSiftingUpOutOfMem:
    while (moves != NULL) {
        move = moves->next;
        cuddDeallocMove(table, moves);
        moves = move;
    }
    return(MV_OOM);
}
static Move * ddSymmSiftingUp ( DdManager * table , int y , int xLow ) { Move * moves ; Move * move ; int x ; int size ; int i ; int gxtop , gybot ; int limitSize ; int xindex , yindex ; int zindex ; int z ; int isolated ; int L ; #ifdef DD_DEBUG int checkL ; #endif moves = NULL ; yindex = table -> invperm [ y ] ; limitSize = L = table -> keys - table -> isolated ; gybot = y ; while ( ( unsigned ) gybot < table -> subtables [ gybot ] . next ) gybot = table -> subtables [ gybot ] . next ; for ( z = xLow + 1 ; z <= gybot ; z ++ ) { zindex = table -> invperm [ z ] ; if ( zindex == yindex || cuddTestInteract ( table , zindex , yindex ) ) { isolated = table -> vars [ zindex ] -> ref == 1 ; L -= table -> subtables [ z ] . keys - isolated ; } } x = cuddNextLow ( table , y ) ; while ( x >= xLow && L <= limitSize ) { #ifdef DD_DEBUG gybot = y ; while ( ( unsigned ) gybot < table -> subtables [ gybot ] . next ) gybot = table -> subtables [ gybot ] . next ; checkL = table -> keys - table -> isolated ; for ( z = xLow + 1 ; z <= gybot ; z ++ ) { zindex = table -> invperm [ z ] ; if ( zindex == yindex || cuddTestInteract ( table , zindex , yindex ) ) { isolated = table -> vars [ zindex ] -> ref == 1 ; checkL -= table -> subtables [ z ] . keys - isolated ; } } assert ( L == checkL ) ; #endif gxtop = table -> subtables [ x ] . next ; if ( cuddSymmCheck ( table , x , y ) ) { table -> subtables [ x ] . next = y ; i = table -> subtables [ y ] . next ; while ( table -> subtables [ i ] . next != ( unsigned ) y ) i = table -> subtables [ i ] . next ; table -> subtables [ i ] . next = gxtop ; } else if ( table -> subtables [ x ] . next == ( unsigned ) x && table -> subtables [ y ] . next == ( unsigned ) y ) { xindex = table -> invperm [ x ] ; 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 ddSymmSiftingUpOutOfMem ; if ( cuddTestInteract ( table , xindex , yindex ) ) { isolated = table -> vars [ xindex ] -> ref == 1 ; L += table -> subtables [ y ] . keys - isolated ; } move = ( Move * ) cuddDynamicAllocNode ( table ) ; if ( move == NULL ) goto ddSymmSiftingUpOutOfMem ; 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 { size = ddSymmGroupMove ( table , x , y , & moves ) ; if ( size == 0 ) goto ddSymmSiftingUpOutOfMem ; z = moves -> y ; do { zindex = table -> invperm [ z ] ; if ( cuddTestInteract ( table , zindex , yindex ) ) { isolated = table -> vars [ zindex ] -> ref == 1 ; L += table -> subtables [ z ] . keys - isolated ; } z = table -> subtables [ z ] . next ; } while ( z != ( int ) moves -> y ) ; if ( ( double ) size > ( double ) limitSize * table -> maxGrowth ) return ( moves ) ; if ( size < limitSize ) limitSize = size ; } y = gxtop ; x = cuddNextLow ( table , y ) ; } return ( moves ) ; ddSymmSiftingUpOutOfMem : while ( moves != NULL ) { move = moves -> next ; cuddDeallocMove ( table , moves ) ; moves = move ; } return ( MV_OOM ) ; }
Function
Synopsis    [Moves x up until either it reaches the bound (xLow) or
the size of the DD heap increases too much.]
Function Synopsis [ Moves x up until either it reaches the bound ( xLow ) or the size of the DD heap increases too much . ]
/* lower bound on DD size */ /* Initialize the lower bound.
    ** The part of the DD below the bottom of y' group will not change.
    ** The part of the DD above y that does not interact with y will not
    ** change. The rest may vanish in the best case, except for
    ** the nodes at level xLow, which will not vanish, regardless.
    */ /* Symmetry found, attach symm groups */ /* x and y have self symmetry */ /* Update the lower bound. */ /* Group move */ /* Update the lower bound. */