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

  Synopsis    [Sifts a variable up applying the XOR transformation.]

  Description [Sifts a variable up applying the XOR
  transformation. Moves y up until either it reaches the bound (xLow)
  or the size of the ZDD heap increases too much.  Returns the set of
  moves in case of success; NULL if memory is full.]

  SideEffects [None]

  SeeAlso     []

******************************************************************************/
Function
Synopsis    [Sifts a variable up applying the XOR transformation.]

Description [Sifts a variable up applying the XOR
transformation. Moves y up until either it reaches the bound (xLow)
or the size of the ZDD heap increases too much.  Returns the set of
moves in case of success; NULL if memory is full.]




Function Synopsis [ Sifts a variable up applying the XOR transformation . ] Description [ Sifts a variable up applying the XOR transformation . Moves y up until either it reaches the bound ( xLow ) or the size of the ZDD heap increases too much . Returns the set of moves in case of success ; NULL if memory is full . ]
static Move *
cuddZddLinearUp(
  DdManager * table,
  int  y,
  int  xLow,
  Move * prevMoves)
{
    Move        *moves;
    Move        *move;
    int         x;
    int         size, newsize;
    int         limitSize;
    moves = prevMoves;
    limitSize = table->keysZ;
    x = cuddZddNextLow(table, y);
    while (x >= xLow) {
        size = cuddZddSwapInPlace(table, x, y);
        if (size == 0)
            goto cuddZddLinearUpOutOfMem;
        newsize = cuddZddLinearInPlace(table, x, y);
        if (newsize == 0)
            goto cuddZddLinearUpOutOfMem;
        move = (Move *) cuddDynamicAllocNode(table);
        if (move == NULL)
            goto cuddZddLinearUpOutOfMem;
        move->x = x;
        move->y = y;
        move->next = moves;
        moves = move;
        move->flags = CUDD_SWAP_MOVE;
        if (newsize > size) {
            newsize = cuddZddLinearInPlace(table,x,y);
            if (newsize == 0) goto cuddZddLinearUpOutOfMem;
#ifdef DD_DEBUG
            if (newsize != size) {
                (void) fprintf(table->err,"Change in size after identity transformation! From %d to %d\n",size,newsize);
            }
#endif
        } else {
            size = newsize;
            move->flags = CUDD_LINEAR_TRANSFORM_MOVE;
        }
        move->size = size;
        if ((double)size > (double)limitSize * table->maxGrowth)
            break;
        if (size < limitSize)
            limitSize = size;
        y = x;
        x = cuddZddNextLow(table, y);
    }
    return(moves);
cuddZddLinearUpOutOfMem:
    while (moves != NULL) {
        move = moves->next;
        cuddDeallocMove(table, moves);
        moves = move;
    }
    return((Move *) CUDD_OUT_OF_MEM);
}
static Move * cuddZddLinearUp ( DdManager * table , int y , int xLow , Move * prevMoves ) { Move * moves ; Move * move ; int x ; int size , newsize ; int limitSize ; moves = prevMoves ; limitSize = table -> keysZ ; x = cuddZddNextLow ( table , y ) ; while ( x >= xLow ) { size = cuddZddSwapInPlace ( table , x , y ) ; if ( size == 0 ) goto cuddZddLinearUpOutOfMem ; newsize = cuddZddLinearInPlace ( table , x , y ) ; if ( newsize == 0 ) goto cuddZddLinearUpOutOfMem ; move = ( Move * ) cuddDynamicAllocNode ( table ) ; if ( move == NULL ) goto cuddZddLinearUpOutOfMem ; move -> x = x ; move -> y = y ; move -> next = moves ; moves = move ; move -> flags = CUDD_SWAP_MOVE ; if ( newsize > size ) { newsize = cuddZddLinearInPlace ( table , x , y ) ; if ( newsize == 0 ) goto cuddZddLinearUpOutOfMem ; #ifdef DD_DEBUG if ( newsize != size ) { ( void ) fprintf ( table -> err , " \n " , size , newsize ) ; } #endif } else { size = newsize ; move -> flags = CUDD_LINEAR_TRANSFORM_MOVE ; } move -> size = size ; if ( ( double ) size > ( double ) limitSize * table -> maxGrowth ) break ; if ( size < limitSize ) limitSize = size ; y = x ; x = cuddZddNextLow ( table , y ) ; } return ( moves ) ; cuddZddLinearUpOutOfMem : while ( moves != NULL ) { move = moves -> next ; cuddDeallocMove ( table , moves ) ; moves = move ; } return ( ( Move * ) CUDD_OUT_OF_MEM ) ; }
Function
Synopsis    [Sifts a variable up applying the XOR transformation.]
Function Synopsis [ Sifts a variable up applying the XOR transformation . ]
/* Undo transformation. The transformation we apply is
            ** its own inverse. Hence, we just apply the transformation
            ** again.
            */