Version abc70930

1 files changed, 0 insertions, 1333 deletions

diff --git a/src/bdd/cudd/cuddLinear.c b/src/bdd/cudd/cuddLinear.c
deleted file mode 100644
index 7f6b3678..00000000
--- a/src/bdd/cudd/cuddLinear.c
+++ /dev/null
@@ -1,1333 +0,0 @@
-/**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;
-    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 */
-