cuddLinear.c

/**CFile***********************************************************************

  FileName    [cuddLinear.c]

  PackageName [cudd]

  Synopsis    [Functions for DD reduction by linear transformations.]

  Description [ Internal procedures included in this module:
        <ul>
        <li> cuddLinearAndSifting()
        </ul>
    Static procedures included in this module:
        <ul>
        <li> ddLinearUniqueCompare()
        <li> ddLinearAndSiftingAux()
        <li> ddLinearAndSiftingUp()
        <li> ddLinearAndSiftingDown()
        <li> ddLinearAndSiftingBackward()
        <li> ddUndoMoves()
        <li> ddUpdateInteractionMatrix()
        <li> cuddLinearInPlace()
        <li> cuddInitLinear()
        <li> cuddResizeLinear()
        <li> cuddXorLinear()
        </ul>]

  Author      [Fabio Somenzi]

  Copyright   [This file was created at the University of Colorado at
  Boulder.  The University of Colorado at Boulder makes no warranty
  about the suitability of this software for any purpose.  It is
  presented on an AS IS basis.]

******************************************************************************/

#include "util_hack.h"
#include "cuddInt.h"

/*---------------------------------------------------------------------------*/
/* Constant declarations                                                     */
/*---------------------------------------------------------------------------*/

#define CUDD_SWAP_MOVE 0
#define CUDD_LINEAR_TRANSFORM_MOVE 1
#define CUDD_INVERSE_TRANSFORM_MOVE 2
#if SIZEOF_LONG == 8
#define BPL 64
#define LOGBPL 6
#else
#define BPL 32
#define LOGBPL 5
#endif

/*---------------------------------------------------------------------------*/
/* Stucture declarations                                                     */
/*---------------------------------------------------------------------------*/

/*---------------------------------------------------------------------------*/
/* Type declarations                                                         */
/*---------------------------------------------------------------------------*/

/*---------------------------------------------------------------------------*/
/* Variable declarations                                                     */
/*---------------------------------------------------------------------------*/

#ifndef lint
static char rcsid[] DD_UNUSED = "$Id: cuddLinear.c,v 1.1.1.1 2003/02/24 22:23:52 wjiang Exp $";
#endif

static    int    *entry;

#ifdef DD_STATS
extern    int    ddTotalNumberSwapping;
extern    int    ddTotalNISwaps;
static    int    ddTotalNumberLinearTr;
#endif

#ifdef DD_DEBUG
static    int    zero = 0;
#endif

/*---------------------------------------------------------------------------*/
/* Macro declarations                                                        */
/*---------------------------------------------------------------------------*/

/**AutomaticStart*************************************************************/

/*---------------------------------------------------------------------------*/
/* Static function prototypes                                                */
/*---------------------------------------------------------------------------*/

static int ddLinearUniqueCompare ARGS((int *ptrX, int *ptrY));
static int ddLinearAndSiftingAux ARGS((DdManager *table, int x, int xLow, int xHigh));
static Move * ddLinearAndSiftingUp ARGS((DdManager *table, int y, int xLow, Move *prevMoves));
static Move * ddLinearAndSiftingDown ARGS((DdManager *table, int x, int xHigh, Move *prevMoves));
static int ddLinearAndSiftingBackward ARGS((DdManager *table, int size, Move *moves));
static Move* ddUndoMoves ARGS((DdManager *table, Move *moves));
static int cuddLinearInPlace ARGS((DdManager *table, int x, int y));
static void ddUpdateInteractionMatrix ARGS((DdManager *table, int xindex, int yindex));
static int cuddInitLinear ARGS((DdManager *table));
static int cuddResizeLinear ARGS((DdManager *table));
static void cuddXorLinear ARGS((DdManager *table, int x, int y));

/**AutomaticEnd***************************************************************/


/*---------------------------------------------------------------------------*/
/* Definition of exported functions                                          */
/*---------------------------------------------------------------------------*/


/**Function********************************************************************
 
  Synopsis    [Prints the linear transform matrix.]

  Description [Prints the linear transform matrix. Returns 1 in case of
  success; 0 otherwise.]

  SideEffects [none]

  SeeAlso     []

******************************************************************************/
int
Cudd_PrintLinear(
  DdManager * table)
{
    int i,j,k;
    int retval;
    int nvars = table->linearSize;
    int wordsPerRow = ((nvars - 1) >> LOGBPL) + 1;
    long word;

    for (i = 0; i < nvars; i++) {
    for (j = 0; j < wordsPerRow; j++) {
        word = table->linear[i*wordsPerRow + j];
        for (k = 0; k < BPL; k++) {
        retval = fprintf(table->out,"%ld",word & 1);
        if (retval == 0) return(0);
        word >>= 1;
        }
    }
    retval = fprintf(table->out,"\n");
    if (retval == 0) return(0);
    }
    return(1);

} /* end of Cudd_PrintLinear */


/**Function********************************************************************
 
  Synopsis    [Reads an entry of the linear transform matrix.]

  Description [Reads an entry of the linear transform matrix.]

  SideEffects [none]

  SeeAlso     []

******************************************************************************/
int
Cudd_ReadLinear(
  DdManager * table /* CUDD manager */,
  int  x /* row index */,
  int  y /* column index */)
{
    int nvars = table->size;
    int wordsPerRow = ((nvars - 1) >> LOGBPL) + 1;
    long word;
    int bit;
    int result;

    assert(table->size == table->linearSize);

    word = wordsPerRow * x + (y >> LOGBPL);
    bit  = y & (BPL-1);
    result = (int) ((table->linear[word] >> bit) & 1);
    return(result);

} /* end of Cudd_ReadLinear */


/*---------------------------------------------------------------------------*/
/* Definition of internal functions                                          */
/*---------------------------------------------------------------------------*/


/**Function********************************************************************

  Synopsis    [BDD reduction based on combination of sifting and linear
  transformations.]

  Description [BDD reduction based on combination of sifting and linear
  transformations.  Assumes that no dead nodes are present.
    <ol>
    <li> Order all the variables according to the number of entries
    in each unique table.
    <li> Sift the variable up and down, remembering each time the
    total size of the DD heap. At each position, linear transformation
    of the two adjacent variables is tried and is accepted if it reduces
    the size of the DD.
    <li> Select the best permutation.
    <li> Repeat 3 and 4 for all variables.
    </ol>
  Returns 1 if successful; 0 otherwise.]

  SideEffects [None]

******************************************************************************/
int
cuddLinearAndSifting(
  DdManager * table,
  int  lower,
  int  upper)
{
    int        i;
    int        *var;
    int        size;
    int        x;
    int        result;
#ifdef DD_STATS
    int        previousSize;
#endif

#ifdef DD_STATS
    ddTotalNumberLinearTr = 0;
#endif

    size = table->size;

    var = NULL;
    entry = NULL;
    if (table->linear == NULL) {
    result = cuddInitLinear(table);
    if (result == 0) goto cuddLinearAndSiftingOutOfMem; 
#if 0
    (void) fprintf(table->out,"\n");
    result = Cudd_PrintLinear(table);
    if (result == 0) goto cuddLinearAndSiftingOutOfMem; 
#endif
    } else if (table->size != table->linearSize) {
    result = cuddResizeLinear(table);
    if (result == 0) goto cuddLinearAndSiftingOutOfMem; 
#if 0
    (void) fprintf(table->out,"\n");
    result = Cudd_PrintLinear(table);
    if (result == 0) goto cuddLinearAndSiftingOutOfMem; 
#endif
    }

    /* Find order in which to sift variables. */
    entry = ALLOC(int,size);
    if (entry == NULL) {
    table->errorCode = CUDD_MEMORY_OUT;
    goto cuddLinearAndSiftingOutOfMem;
    }
    var = ALLOC(int,size);
    if (var == NULL) {
    table->errorCode = CUDD_MEMORY_OUT;
    goto cuddLinearAndSiftingOutOfMem;
    }

    for (i = 0; i < size; i++) {
    x = table->perm[i];
    entry[i] = table->subtables[x].keys;
    var[i] = i;
    }

    qsort((void *)var,size,sizeof(int),(int (*)(const void *, const void *))ddLinearUniqueCompare);

    /* Now sift. */
    for (i = 0; i < ddMin(table->siftMaxVar,size); i++) {
    x = table->perm[var[i]];
    if (x < lower || x > upper) continue;
#ifdef DD_STATS
    previousSize = table->keys - table->isolated;
#endif
    result = ddLinearAndSiftingAux(table,x,lower,upper);
    if (!result) goto cuddLinearAndSiftingOutOfMem; 
#ifdef DD_STATS
    if (table->keys < (unsigned) previousSize + table->isolated) {
        (void) fprintf(table->out,"-");
    } else if (table->keys > (unsigned) previousSize + table->isolated) {
        (void) fprintf(table->out,"+");    /* should never happen */
        (void) fprintf(table->out,"\nSize increased from %d to %d while sifting variable %d\n", previousSize, table->keys - table->isolated, var[i]);
    } else {
        (void) fprintf(table->out,"=");
    }
    fflush(table->out);
#endif
#ifdef DD_DEBUG
    (void) Cudd_DebugCheck(table);
#endif
    }

    FREE(var);
    FREE(entry);

#ifdef DD_STATS
    (void) fprintf(table->out,"\n#:L_LINSIFT %8d: linear trans.",
           ddTotalNumberLinearTr);
#endif

    return(1);

cuddLinearAndSiftingOutOfMem:

    if (entry != NULL) FREE(entry);
    if (var != NULL) FREE(var);

    return(0); 

} /* end of cuddLinearAndSifting */


/*---------------------------------------------------------------------------*/
/* Definition of static functions                                            */
/*---------------------------------------------------------------------------*/


/**Function********************************************************************

  Synopsis    [Comparison function used by qsort.]

  Description [Comparison function used by qsort to order the
  variables according to the number of keys in the subtables.
  Returns the difference in number of keys between the two
  variables being compared.]

  SideEffects [None]

******************************************************************************/
static int
ddLinearUniqueCompare(
  int * ptrX,
  int * ptrY)
{
#if 0
    if (entry[*ptrY] == entry[*ptrX]) {
    return((*ptrX) - (*ptrY));
    }
#endif
    return(entry[*ptrY] - entry[*ptrX]);

} /* end of ddLinearUniqueCompare */


/**Function********************************************************************

  Synopsis    [Given xLow <= x <= xHigh moves x up and down between the
  boundaries.]

  Description [Given xLow <= x <= xHigh moves x up and down between the
  boundaries. At each step a linear transformation is tried, and, if it
  decreases the size of the DD, it is accepted. Finds the best position
  and does the required changes.  Returns 1 if successful; 0 otherwise.]

  SideEffects [None]

******************************************************************************/
static int
ddLinearAndSiftingAux(
  DdManager * table,
  int  x,
  int  xLow,
  int  xHigh)
{

    Move    *move;
    Move    *moveUp;        /* list of up moves */
    Move    *moveDown;        /* list of down moves */
    int        initialSize;
    int        result;

    initialSize = table->keys - table->isolated;

    moveDown = NULL;
    moveUp = NULL;

    if (x == xLow) {
    moveDown = ddLinearAndSiftingDown(table,x,xHigh,NULL);
    /* At this point x --> xHigh unless bounding occurred. */
    if (moveDown == (Move *) CUDD_OUT_OF_MEM) goto ddLinearAndSiftingAuxOutOfMem;
    /* Move backward and stop at best position. */    
    result = ddLinearAndSiftingBackward(table,initialSize,moveDown);
    if (!result) goto ddLinearAndSiftingAuxOutOfMem;

    } else if (x == xHigh) {
    moveUp = ddLinearAndSiftingUp(table,x,xLow,NULL);
    /* At this point x --> xLow unless bounding occurred. */
    if (moveUp == (Move *) CUDD_OUT_OF_MEM) goto ddLinearAndSiftingAuxOutOfMem;
    /* Move backward and stop at best position. */
    result = ddLinearAndSiftingBackward(table,initialSize,moveUp);
    if (!result) goto ddLinearAndSiftingAuxOutOfMem;

    } else if ((x - xLow) > (xHigh - x)) { /* must go down first: shorter */
    moveDown = ddLinearAndSiftingDown(table,x,xHigh,NULL);
    /* At this point x --> xHigh unless bounding occurred. */
    if (moveDown == (Move *) CUDD_OUT_OF_MEM) goto ddLinearAndSiftingAuxOutOfMem;
    moveUp = ddUndoMoves(table,moveDown);
#ifdef DD_DEBUG
    assert(moveUp == NULL || moveUp->x == x);
#endif
    moveUp = ddLinearAndSiftingUp(table,x,xLow,moveUp);
    if (moveUp == (Move *) CUDD_OUT_OF_MEM) goto ddLinearAndSiftingAuxOutOfMem;
    /* Move backward and stop at best position. */    
    result = ddLinearAndSiftingBackward(table,initialSize,moveUp);
    if (!result) goto ddLinearAndSiftingAuxOutOfMem;

    } else { /* must go up first: shorter */
    moveUp = ddLinearAndSiftingUp(table,x,xLow,NULL);
    /* At this point x --> xLow unless bounding occurred. */
    if (moveUp == (Move *) CUDD_OUT_OF_MEM) goto ddLinearAndSiftingAuxOutOfMem;
    moveDown = ddUndoMoves(table,moveUp);
#ifdef DD_DEBUG
    assert(moveDown == NULL || moveDown->y == x);
#endif
    moveDown = ddLinearAndSiftingDown(table,x,xHigh,moveDown);
    if (moveDown == (Move *) CUDD_OUT_OF_MEM) goto ddLinearAndSiftingAuxOutOfMem;
    /* Move backward and stop at best position. */    
    result = ddLinearAndSiftingBackward(table,initialSize,moveDown);
    if (!result) goto ddLinearAndSiftingAuxOutOfMem;
    }

    while (moveDown != NULL) {
    move = moveDown->next;
    cuddDeallocNode(table, (DdNode *) moveDown);
    moveDown = move;
    }
    while (moveUp != NULL) {
    move = moveUp->next;
    cuddDeallocNode(table, (DdNode *) moveUp);
    moveUp = move;
    }

    return(1);

ddLinearAndSiftingAuxOutOfMem:
    while (moveDown != NULL) {
    move = moveDown->next;
    cuddDeallocNode(table, (DdNode *) moveDown);
    moveDown = move;
    }
    while (moveUp != NULL) {
    move = moveUp->next;
    cuddDeallocNode(table, (DdNode *) moveUp);
    moveUp = move;
    }

    return(0);

} /* end of ddLinearAndSiftingAux */


/**Function********************************************************************

  Synopsis    [Sifts a variable up and applies linear transformations.]

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

  SideEffects [None]

******************************************************************************/
static Move *
ddLinearAndSiftingUp(
  DdManager * table,
  int  y,
  int  xLow,
  Move * prevMoves)
{
    Move    *moves;
    Move    *move;
    int        x;
    int        size, newsize;
    int        limitSize;
    int        xindex, yindex;
    int        isolated;
    int        L;    /* lower bound on DD size */
#ifdef DD_DEBUG
    int checkL;
    int z;
    int zindex;
#endif

    moves = prevMoves;
    yindex = table->invperm[y];

    /* Initialize the lower bound.
    ** The part of the DD below y 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.
    */
    limitSize = L = table->keys - table->isolated;
    for (x = xLow + 1; x < y; x++) {
    xindex = table->invperm[x];
    if (cuddTestInteract(table,xindex,yindex)) {
        isolated = table->vars[xindex]->ref == 1;
        L -= table->subtables[x].keys - isolated;
    }
    }
    isolated = table->vars[yindex]->ref == 1;
    L -= table->subtables[y].keys - isolated;

    x = cuddNextLow(table,y);
    while (x >= xLow && L <= limitSize) {
    xindex = table->invperm[x];
#ifdef DD_DEBUG
    checkL = table->keys - table->isolated;
    for (z = xLow + 1; z < y; z++) {
        zindex = table->invperm[z];
        if (cuddTestInteract(table,zindex,yindex)) {
        isolated = table->vars[zindex]->ref == 1;
        checkL -= table->subtables[z].keys - isolated;
        }
    }
    isolated = table->vars[yindex]->ref == 1;
    checkL -= table->subtables[y].keys - isolated;
    if (L != checkL) {
        (void) fprintf(table->out, "checkL(%d) != L(%d)\n",checkL,L);
    }
#endif
    size = cuddSwapInPlace(table,x,y);
    if (size == 0) goto ddLinearAndSiftingUpOutOfMem;
    newsize = cuddLinearInPlace(table,x,y);
    if (newsize == 0) goto ddLinearAndSiftingUpOutOfMem;
    move = (Move *) cuddDynamicAllocNode(table);
    if (move == NULL) goto ddLinearAndSiftingUpOutOfMem;
    move->x = x;
    move->y = y;
    move->next = moves;
    moves = move;
    move->flags = CUDD_SWAP_MOVE;
    if (newsize >= size) {
        /* Undo transformation. The transformation we apply is
        ** its own inverse. Hence, we just apply the transformation
        ** again.
        */
        newsize = cuddLinearInPlace(table,x,y);
        if (newsize == 0) goto ddLinearAndSiftingUpOutOfMem;
#ifdef DD_DEBUG
        if (newsize != size) {
        (void) fprintf(table->out,"Change in size after identity transformation! From %d to %d\n",size,newsize);
        }
#endif
    } else if (cuddTestInteract(table,xindex,yindex)) {
        size = newsize;
        move->flags = CUDD_LINEAR_TRANSFORM_MOVE;
        ddUpdateInteractionMatrix(table,xindex,yindex);
    }
    move->size = size;
    /* Update the lower bound. */
    if (cuddTestInteract(table,xindex,yindex)) {
        isolated = table->vars[xindex]->ref == 1;
        L += table->subtables[y].keys - isolated;
    }
    if ((double) size > (double) limitSize * table->maxGrowth) break;
    if (size < limitSize) limitSize = size;
    y = x;
    x = cuddNextLow(table,y);
    }
    return(moves);

ddLinearAndSiftingUpOutOfMem:
    while (moves != NULL) {
    move = moves->next;
    cuddDeallocNode(table, (DdNode *) moves);
    moves = move;
    }
    return((Move *) CUDD_OUT_OF_MEM);

} /* end of ddLinearAndSiftingUp */
    

/**Function********************************************************************

  Synopsis    [Sifts a variable down and applies linear transformations.]

  Description [Sifts a variable down and applies linear
  transformations. Moves x down until either it reaches the bound
  (xHigh) or the size of the DD heap increases too much. Returns the
  set of moves in case of success; NULL if memory is full.]

  SideEffects [None]

******************************************************************************/
static Move *
ddLinearAndSiftingDown(
  DdManager * table,
  int  x,
  int  xHigh,
  Move * prevMoves)
{
    Move    *moves;
    Move    *move;
    int        y;
    int        size, newsize;
    int        R;    /* upper bound on node decrease */
    int        limitSize;
    int        xindex, yindex;
    int        isolated;
#ifdef DD_DEBUG
    int        checkR;
    int        z;
    int        zindex;
#endif

    moves = prevMoves;
    /* Initialize R */
    xindex = table->invperm[x];
    limitSize = size = table->keys - table->isolated;
    R = 0;
    for (y = xHigh; y > x; y--) {
    yindex = table->invperm[y];
    if (cuddTestInteract(table,xindex,yindex)) {
        isolated = table->vars[yindex]->ref == 1;
        R += table->subtables[y].keys - isolated;
    }
    }

    y = cuddNextHigh(table,x);
    while (y <= xHigh && size - R < limitSize) {
#ifdef DD_DEBUG
    checkR = 0;
    for (z = xHigh; z > x; z--) {
        zindex = table->invperm[z];
        if (cuddTestInteract(table,xindex,zindex)) {
        isolated = table->vars[zindex]->ref == 1;
        checkR += table->subtables[z].keys - isolated;
        }
    }
    if (R != checkR) {
        (void) fprintf(table->out, "checkR(%d) != R(%d)\n",checkR,R);
    }
#endif
    /* Update upper bound on node decrease. */
    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);
    if (size == 0) goto ddLinearAndSiftingDownOutOfMem; 
    newsize = cuddLinearInPlace(table,x,y);
    if (newsize == 0) goto ddLinearAndSiftingDownOutOfMem;
    move = (Move *) cuddDynamicAllocNode(table);
    if (move == NULL) goto ddLinearAndSiftingDownOutOfMem;
    move->x = x;
    move->y = y;
    move->next = moves;
    moves = move;
    move->flags = CUDD_SWAP_MOVE;
    if (newsize >= size) {
        /* Undo transformation. The transformation we apply is
        ** its own inverse. Hence, we just apply the transformation
        ** again.
        */
        newsize = cuddLinearInPlace(table,x,y);
        if (newsize == 0) goto ddLinearAndSiftingDownOutOfMem;
        if (newsize != size) {
        (void) fprintf(table->out,"Change in size after identity transformation! From %d to %d\n",size,newsize);
        }
    } else if (cuddTestInteract(table,xindex,yindex)) {
        size = newsize;
        move->flags = CUDD_LINEAR_TRANSFORM_MOVE;
        ddUpdateInteractionMatrix(table,xindex,yindex);
    }
    move->size = size;
    if ((double) size > (double) limitSize * table->maxGrowth) break;
    if (size < limitSize) limitSize = size;
    x = y;
    y = cuddNextHigh(table,x);
    }
    return(moves);

ddLinearAndSiftingDownOutOfMem:
    while (moves != NULL) {
    move = moves->next;
    cuddDeallocNode(table, (DdNode *) moves);
    moves = move;
    }
    return((Move *) CUDD_OUT_OF_MEM);

} /* end of ddLinearAndSiftingDown */


/**Function********************************************************************

  Synopsis    [Given a set of moves, returns the DD heap to the order
  giving the minimum size.]

  Description [Given a set of moves, returns the DD heap to the
  position giving the minimum size. In case of ties, returns to the
  closest position giving the minimum size. Returns 1 in case of
  success; 0 otherwise.]

  SideEffects [None]

******************************************************************************/
static int
ddLinearAndSiftingBackward(
  DdManager * table,
  int  size,
  Move * moves)
{
    Move *move;
    int    res;

    for (move = moves; move != NULL; move = move->next) {
    if (move->size < size) {
        size = move->size;
    }
    }

    for (move = moves; move != NULL; move = move->next) {
    if (move->size == size) return(1);
    if (move->flags == CUDD_LINEAR_TRANSFORM_MOVE) {
        res = cuddLinearInPlace(table,(int)move->x,(int)move->y);
        if (!res) return(0);
    }
    res = cuddSwapInPlace(table,(int)move->x,(int)move->y);
    if (!res) return(0);
    if (move->flags == CUDD_INVERSE_TRANSFORM_MOVE) {
        res = cuddLinearInPlace(table,(int)move->x,(int)move->y);
        if (!res) return(0);
    }
    }

    return(1);

} /* end of ddLinearAndSiftingBackward */


/**Function********************************************************************

  Synopsis    [Given a set of moves, returns the DD heap to the order
  in effect before the moves.]

  Description [Given a set of moves, returns the DD heap to the
  order in effect before the moves.  Returns 1 in case of success;
  0 otherwise.]

  SideEffects [None]

******************************************************************************/
static Move*
ddUndoMoves(
  DdManager * table,
  Move * moves)
{
    Move *invmoves = NULL;
    Move *move;
    Move *invmove;
    int    size;

    for (move = moves; move != NULL; move = move->next) {
    invmove = (Move *) cuddDynamicAllocNode(table);
    if (invmove == NULL) goto ddUndoMovesOutOfMem;
    invmove->x = move->x;
    invmove->y = move->y;
    invmove->next = invmoves;
    invmoves = invmove;
    if (move->flags == CUDD_SWAP_MOVE) {
        invmove->flags = CUDD_SWAP_MOVE;
        size = cuddSwapInPlace(table,(int)move->x,(int)move->y);
        if (!size) goto ddUndoMovesOutOfMem;
    } else if (move->flags == CUDD_LINEAR_TRANSFORM_MOVE) {
        invmove->flags = CUDD_INVERSE_TRANSFORM_MOVE;
        size = cuddLinearInPlace(table,(int)move->x,(int)move->y);
        if (!size) goto ddUndoMovesOutOfMem;
        size = cuddSwapInPlace(table,(int)move->x,(int)move->y);
        if (!size) goto ddUndoMovesOutOfMem;
    } else { /* must be CUDD_INVERSE_TRANSFORM_MOVE */
#ifdef DD_DEBUG
        (void) fprintf(table->err,"Unforseen event in ddUndoMoves!\n");
#endif
        invmove->flags = CUDD_LINEAR_TRANSFORM_MOVE;
        size = cuddSwapInPlace(table,(int)move->x,(int)move->y);
        if (!size) goto ddUndoMovesOutOfMem;
        size = cuddLinearInPlace(table,(int)move->x,(int)move->y);
        if (!size) goto ddUndoMovesOutOfMem;
    }
    invmove->size = size;
    }

    return(invmoves);

ddUndoMovesOutOfMem:
    while (invmoves != NULL) {
    move = invmoves->next;
    cuddDeallocNode(table, (DdNode *) invmoves);
    invmoves = move;
    }
    return((Move *) CUDD_OUT_OF_MEM);

} /* end of ddUndoMoves */


/**Function********************************************************************
 
  Synopsis    [Linearly combines two adjacent variables.]

  Description [Linearly combines two adjacent variables. Specifically,
  replaces the top variable with the exclusive nor of the two variables.
  It assumes that no dead nodes are present on entry to this
  procedure.  The procedure then guarantees that no dead nodes will be
  present when it terminates.  cuddLinearInPlace assumes that x &lt;
  y.  Returns the number of keys in the table if successful; 0
  otherwise.]

  SideEffects [The two subtables corrresponding to variables x and y are
  modified. The global counters of the unique table are also affected.]

  SeeAlso     [cuddSwapInPlace]

******************************************************************************/
static int
cuddLinearInPlace(
  DdManager * table,
  int  x,
  int  y)
{
    DdNodePtr *xlist, *ylist;
    int    xindex, yindex;
    int    xslots, yslots;
    int    xshift, yshift;
    int    oldxkeys, oldykeys;
    int    newxkeys, newykeys;
    int    comple, newcomplement;
    int    i;
    int    posn;
    int    isolated;
    DdNode *f,*f0,*f1,*f01,*f00,*f11,*f10,*newf1,*newf0;
    DdNode *g,*next,*last = NULL; // Suppress "might be used uninitialized"
    DdNodePtr *previousP;
    DdNode *tmp;
    DdNode *sentinel = &(table->sentinel);
#if DD_DEBUG
    int    count, idcheck;
#endif

#ifdef DD_DEBUG
    assert(x < y);
    assert(cuddNextHigh(table,x) == y);
    assert(table->subtables[x].keys != 0);
    assert(table->subtables[y].keys != 0);
    assert(table->subtables[x].dead == 0);
    assert(table->subtables[y].dead == 0);
#endif

    xindex = table->invperm[x];
    yindex = table->invperm[y];

    if (cuddTestInteract(table,xindex,yindex)) {
#ifdef DD_STATS
    ddTotalNumberLinearTr++;
#endif
    /* Get parameters of x subtable. */
    xlist = table->subtables[x].nodelist; 
    oldxkeys = table->subtables[x].keys;
    xslots = table->subtables[x].slots;
    xshift = table->subtables[x].shift;

    /* Get parameters of y subtable. */
    ylist = table->subtables[y].nodelist;
    oldykeys = table->subtables[y].keys;
    yslots = table->subtables[y].slots;
    yshift = table->subtables[y].shift;

    newxkeys = 0;
    newykeys = oldykeys;

    /* Check whether the two projection functions involved in this
    ** swap are isolated. At the end, we'll be able to tell how many
    ** isolated projection functions are there by checking only these
    ** two functions again. This is done to eliminate the isolated
    ** projection functions from the node count.
    */
    isolated = - ((table->vars[xindex]->ref == 1) +
             (table->vars[yindex]->ref == 1));

    /* The nodes in the x layer are put in a chain.
    ** The chain is handled as a FIFO; g points to the beginning and
    ** last points to the end.
    */
    g = NULL;
    for (i = 0; i < xslots; i++) {
        f = xlist[i];
        if (f == sentinel) continue;
        xlist[i] = sentinel;
        if (g == NULL) {
        g = f;
        } else {
        last->next = f;
        }
        while ((next = f->next) != sentinel) {
        f = next;
        } /* while there are elements in the collision chain */
        last = f;
    } /* for each slot of the x subtable */
    last->next = NULL;

#ifdef DD_COUNT
    table->swapSteps += oldxkeys;
#endif
    /* Take care of the x nodes that must be re-expressed.
    ** They form a linked list pointed by g.
    */
    f = g;
    while (f != NULL) {
        next = f->next;
        /* Find f1, f0, f11, f10, f01, f00. */
        f1 = cuddT(f);
#ifdef DD_DEBUG
        assert(!(Cudd_IsComplement(f1)));
#endif
        if ((int) f1->index == yindex) {
        f11 = cuddT(f1); f10 = cuddE(f1);
        } else {
        f11 = f10 = f1;
        }
#ifdef DD_DEBUG
        assert(!(Cudd_IsComplement(f11)));
#endif
        f0 = cuddE(f);
        comple = Cudd_IsComplement(f0);
        f0 = Cudd_Regular(f0);
        if ((int) f0->index == yindex) {
        f01 = cuddT(f0); f00 = cuddE(f0);
        } else {
        f01 = f00 = f0;
        }
        if (comple) {
        f01 = Cudd_Not(f01);
        f00 = Cudd_Not(f00);
        }
        /* Decrease ref count of f1. */
        cuddSatDec(f1->ref);
        /* Create the new T child. */
        if (f11 == f00) {
        newf1 = f11;
        cuddSatInc(newf1->ref);
        } else {
        /* Check ylist for triple (yindex,f11,f00). */
        posn = ddHash(f11, f00, yshift);
        /* For each element newf1 in collision list ylist[posn]. */
        previousP = &(ylist[posn]);
        newf1 = *previousP;
        while (f11 < cuddT(newf1)) {
            previousP = &(newf1->next);
            newf1 = *previousP;
        }
        while (f11 == cuddT(newf1) && f00 < cuddE(newf1)) {
            previousP = &(newf1->next);
            newf1 = *previousP;
        }
        if (cuddT(newf1) == f11 && cuddE(newf1) == f00) {
            cuddSatInc(newf1->ref);
        } else { /* no match */
            newf1 = cuddDynamicAllocNode(table);
            if (newf1 == NULL)
            goto cuddLinearOutOfMem;
            newf1->index = yindex; newf1->ref = 1;
            cuddT(newf1) = f11;
            cuddE(newf1) = f00;
            /* Insert newf1 in the collision list ylist[posn];
            ** increase the ref counts of f11 and f00.
            */
            newykeys++;
            newf1->next = *previousP;
            *previousP = newf1;
            cuddSatInc(f11->ref);
            tmp = Cudd_Regular(f00);
            cuddSatInc(tmp->ref);
        }
        }
        cuddT(f) = newf1;
#ifdef DD_DEBUG
        assert(!(Cudd_IsComplement(newf1)));
#endif

        /* Do the same for f0, keeping complement dots into account. */
        /* decrease ref count of f0 */
        tmp = Cudd_Regular(f0);
        cuddSatDec(tmp->ref);
        /* create the new E child */
        if (f01 == f10) {
        newf0 = f01;
        tmp = Cudd_Regular(newf0);
        cuddSatInc(tmp->ref); 
        } else {
        /* make sure f01 is regular */
        newcomplement = Cudd_IsComplement(f01);
        if (newcomplement) {
            f01 = Cudd_Not(f01);
            f10 = Cudd_Not(f10);
        }
        /* Check ylist for triple (yindex,f01,f10). */
        posn = ddHash(f01, f10, yshift);
        /* For each element newf0 in collision list ylist[posn]. */
        previousP = &(ylist[posn]);
        newf0 = *previousP;
        while (f01 < cuddT(newf0)) {
            previousP = &(newf0->next);
            newf0 = *previousP;
        }
        while (f01 == cuddT(newf0) && f10 < cuddE(newf0)) {
            previousP = &(newf0->next);
            newf0 = *previousP;
        }
        if (cuddT(newf0) == f01 && cuddE(newf0) == f10) {
            cuddSatInc(newf0->ref); 
        } else { /* no match */
            newf0 = cuddDynamicAllocNode(table);
            if (newf0 == NULL)
            goto cuddLinearOutOfMem;
            newf0->index = yindex; newf0->ref = 1;
            cuddT(newf0) = f01;
            cuddE(newf0) = f10;
            /* Insert newf0 in the collision list ylist[posn];
            ** increase the ref counts of f01 and f10.
            */
            newykeys++;
            newf0->next = *previousP;
            *previousP = newf0;
            cuddSatInc(f01->ref);
            tmp = Cudd_Regular(f10);
            cuddSatInc(tmp->ref);
        }
        if (newcomplement) {
            newf0 = Cudd_Not(newf0);
        }
        }
        cuddE(f) = newf0;

        /* Re-insert the modified f in xlist.
        ** The modified f does not already exists in xlist.
        ** (Because of the uniqueness of the cofactors.)
        */
        posn = ddHash(newf1, newf0, xshift);
        newxkeys++;
        previousP = &(xlist[posn]);
        tmp = *previousP;
        while (newf1 < cuddT(tmp)) {
        previousP = &(tmp->next);
        tmp = *previousP;
        }
        while (newf1 == cuddT(tmp) && newf0 < cuddE(tmp)) {
        previousP = &(tmp->next);
        tmp = *previousP;
        }
        f->next = *previousP;
        *previousP = f;
        f = next;
    } /* while f != NULL */

    /* GC the y layer. */

    /* For each node f in ylist. */
    for (i = 0; i < yslots; i++) {
        previousP = &(ylist[i]);
        f = *previousP;
        while (f != sentinel) {
        next = f->next;
        if (f->ref == 0) {
            tmp = cuddT(f);
            cuddSatDec(tmp->ref);
            tmp = Cudd_Regular(cuddE(f));
            cuddSatDec(tmp->ref);
            cuddDeallocNode(table,f);
            newykeys--;
        } else {
            *previousP = f;
            previousP = &(f->next);
        }
        f = next;
        } /* while f */
        *previousP = sentinel;
    } /* for every collision list */

#if DD_DEBUG
#if 0
    (void) fprintf(table->out,"Linearly combining %d and %d\n",x,y);
#endif
    count = 0;
    idcheck = 0;
    for (i = 0; i < yslots; i++) {
        f = ylist[i];
        while (f != sentinel) {
        count++;
        if (f->index != (DdHalfWord) yindex)
            idcheck++;
        f = f->next;
        }
    }
    if (count != newykeys) {
        fprintf(table->err,"Error in finding newykeys\toldykeys = %d\tnewykeys = %d\tactual = %d\n",oldykeys,newykeys,count);
    }
    if (idcheck != 0)
        fprintf(table->err,"Error in id's of ylist\twrong id's = %d\n",idcheck);
    count = 0;
    idcheck = 0;
    for (i = 0; i < xslots; i++) {
        f = xlist[i];
        while (f != sentinel) {
        count++;
        if (f->index != (DdHalfWord) xindex)
            idcheck++;
        f = f->next;
        }
    }
    if (count != newxkeys || newxkeys != oldxkeys) {
        fprintf(table->err,"Error in finding newxkeys\toldxkeys = %d \tnewxkeys = %d \tactual = %d\n",oldxkeys,newxkeys,count);
    }
    if (idcheck != 0)
        fprintf(table->err,"Error in id's of xlist\twrong id's = %d\n",idcheck);
#endif

    isolated += (table->vars[xindex]->ref == 1) +
            (table->vars[yindex]->ref == 1);
    table->isolated += isolated;

    /* Set the appropriate fields in table. */
    table->subtables[y].keys = newykeys;

    /* Here we should update the linear combination table
    ** to record that x <- x EXNOR y. This is done by complementing
    ** the (x,y) entry of the table.
    */

    table->keys += newykeys - oldykeys;

    cuddXorLinear(table,xindex,yindex);
    }

#ifdef DD_DEBUG
    if (zero) {
    (void) Cudd_DebugCheck(table);
    }
#endif

    return(table->keys - table->isolated);

cuddLinearOutOfMem:
    (void) fprintf(table->err,"Error: cuddLinearInPlace out of memory\n");

    return (0);

} /* end of cuddLinearInPlace */


/**Function********************************************************************
 
  Synopsis    [Updates the interaction matrix.]

  Description []

  SideEffects [none]

  SeeAlso     []

******************************************************************************/
static void
ddUpdateInteractionMatrix(
  DdManager * table,
  int  xindex,
  int  yindex)
{
    int i;
    for (i = 0; i < yindex; i++) {
    if (i != xindex && cuddTestInteract(table,i,yindex)) {
        if (i < xindex) {
        cuddSetInteract(table,i,xindex);
        } else {
        cuddSetInteract(table,xindex,i);
        }
    }
    }
    for (i = yindex+1; i < table->size; i++) {
    if (i != xindex && cuddTestInteract(table,yindex,i)) {
        if (i < xindex) {
        cuddSetInteract(table,i,xindex);
        } else {
        cuddSetInteract(table,xindex,i);
        }
    }
    }

} /* end of ddUpdateInteractionMatrix */


/**Function********************************************************************
 
  Synopsis    [Initializes the linear transform matrix.]

  Description []

  SideEffects [none]

  SeeAlso     []

******************************************************************************/
static int
cuddInitLinear(
  DdManager * table)
{
    int words;
    int wordsPerRow;
    int nvars;
    int word;
    int bit;
    int i;
    long *linear;

    nvars = table->size;
    wordsPerRow = ((nvars - 1) >> LOGBPL) + 1;
    words = wordsPerRow * nvars;
    table->linear = linear = ALLOC(long,words);
    if (linear == NULL) {
    table->errorCode = CUDD_MEMORY_OUT;
    return(0);
    }
    table->memused += words * sizeof(long);
    table->linearSize = nvars;
    for (i = 0; i < words; i++) linear[i] = 0;
    for (i = 0; i < nvars; i++) {
    word = wordsPerRow * i + (i >> LOGBPL);
    bit  = i & (BPL-1);
    linear[word] = 1 << bit;
    }
    return(1);

} /* end of cuddInitLinear */


/**Function********************************************************************
 
  Synopsis    [Resizes the linear transform matrix.]

  Description []

  SideEffects [none]

  SeeAlso     []

******************************************************************************/
static int
cuddResizeLinear(
  DdManager * table)
{
    int words,oldWords;
    int wordsPerRow,oldWordsPerRow;
    int nvars,oldNvars;
    int word,oldWord;
    int bit;
    int i,j;
    long *linear,*oldLinear;

    oldNvars = table->linearSize;
    oldWordsPerRow = ((oldNvars - 1) >> LOGBPL) + 1;
    oldWords = oldWordsPerRow * oldNvars;
    oldLinear = table->linear;

    nvars = table->size;
    wordsPerRow = ((nvars - 1) >> LOGBPL) + 1;
    words = wordsPerRow * nvars;
    table->linear = linear = ALLOC(long,words);
    if (linear == NULL) {
    table->errorCode = CUDD_MEMORY_OUT;
    return(0);
    }
    table->memused += (words - oldWords) * sizeof(long);
    for (i = 0; i < words; i++) linear[i] = 0;

    /* Copy old matrix. */
    for (i = 0; i < oldNvars; i++) {
    for (j = 0; j < oldWordsPerRow; j++) {
        oldWord = oldWordsPerRow * i + j;
        word = wordsPerRow * i + j;
        linear[word] = oldLinear[oldWord];
    }
    }
    FREE(oldLinear);

    /* Add elements to the diagonal. */
    for (i = oldNvars; i < nvars; i++) {
    word = wordsPerRow * i + (i >> LOGBPL);
    bit  = i & (BPL-1);
    linear[word] = 1 << bit;
    }
    table->linearSize = nvars;

    return(1);

} /* end of cuddResizeLinear */


/**Function********************************************************************
 
  Synopsis    [XORs two rows of the linear transform matrix.]

  Description [XORs two rows of the linear transform matrix and replaces
  the first row with the result.]

  SideEffects [none]

  SeeAlso     []

******************************************************************************/
static void
cuddXorLinear(
  DdManager * table,
  int  x,
  int  y)
{
    int i;
    int nvars = table->size;
    int wordsPerRow = ((nvars - 1) >> LOGBPL) + 1;
    int xstart = wordsPerRow * x;
    int ystart = wordsPerRow * y;
    long *linear = table->linear;

    for (i = 0; i < wordsPerRow; i++) {
    linear[xstart+i] ^= linear[ystart+i];
    }

} /* end of cuddXorLinear */