src/bdd/cudd/cuddZddLin.c

Go to the documentation of this file.

#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

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


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


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

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

extern  int     *zdd_entry;
extern  int     zddTotalNumberSwapping;
static  int     zddTotalNumberLinearTr;
static  DdNode  *empty;


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


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

static int cuddZddLinearAux ARGS((DdManager *table, int x, int xLow, int xHigh));
static Move * cuddZddLinearUp ARGS((DdManager *table, int y, int xLow, Move *prevMoves));
static Move * cuddZddLinearDown ARGS((DdManager *table, int x, int xHigh, Move *prevMoves));
static int cuddZddLinearBackward ARGS((DdManager *table, int size, Move *moves));
static Move* cuddZddUndoMoves ARGS((DdManager *table, Move *moves));

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


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




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

    size = table->sizeZ;
    empty = table->zero;

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

    for (i = 0; i < size; i++) {
        x = table->permZ[i];
        zdd_entry[i] = table->subtableZ[x].keys;
        var[i] = i;
    }

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

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

    FREE(var);
    FREE(zdd_entry);

    return(1);

cuddZddSiftingOutOfMem:

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

    return(0);

} /* end of cuddZddLinearSifting */


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


int
cuddZddLinearInPlace(
  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         i;
    int         posn;
    DdNode      *f, *f1, *f0, *f11, *f10, *f01, *f00;
    DdNode      *newf1, *newf0, *g, *next, *previous;
    DdNode      *special;

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

    zddTotalNumberLinearTr++;

    /* Get parameters of x subtable. */
    xindex   = table->invpermZ[x];
    xlist    = table->subtableZ[x].nodelist;
    oldxkeys = table->subtableZ[x].keys;
    xslots   = table->subtableZ[x].slots;
    xshift   = table->subtableZ[x].shift;
    newxkeys = 0;

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

    /* The nodes in the x layer are put in two chains.  The chain
    ** pointed by g holds the normal nodes. When re-expressed they stay
    ** in the x list. The chain pointed by special holds the elements
    ** that will move to the y list.
    */
    g = special = NULL;
    for (i = 0; i < xslots; i++) {
        f = xlist[i];
        if (f == NULL) continue;
        xlist[i] = NULL;
        while (f != NULL) {
            next = f->next;
            f1 = cuddT(f);
            /* if (f1->index == yindex) */ cuddSatDec(f1->ref);
            f0 = cuddE(f);
            /* if (f0->index == yindex) */ cuddSatDec(f0->ref);
            if ((int) f1->index == yindex && cuddE(f1) == empty &&
                (int) f0->index != yindex) {
                f->next = special;
                special = f;
            } else {
                f->next = g;
                g = f;
            }
            f = next;
        } /* while there are elements in the collision chain */
    } /* for each slot of the x subtable */

    /* Mark y nodes with pointers from above x. We mark them by
    **  changing their index to x.
    */
    for (i = 0; i < yslots; i++) {
        f = ylist[i];
        while (f != NULL) {
            if (f->ref != 0) {
                f->index = xindex;
            }
            f = f->next;
        } /* while there are elements in the collision chain */
    } /* for each slot of the y subtable */

    /* Move special nodes to the y list. */
    f = special;
    while (f != NULL) {
        next = f->next;
        f1 = cuddT(f);
        f11 = cuddT(f1);
        cuddT(f) = f11;
        cuddSatInc(f11->ref);
        f0 = cuddE(f);
        cuddSatInc(f0->ref);
        f->index = yindex;
        /* Insert at the beginning of the list so that it will be
        ** found first if there is a duplicate. The duplicate will
        ** eventually be moved or garbage collected. No node
        ** re-expression will add a pointer to it.
        */
        posn = ddHash(f11, f0, yshift);
        f->next = ylist[posn];
        ylist[posn] = f;
        newykeys++;
        f = next;
    }

    /* Take care of the remaining x nodes that must be re-expressed.
    ** They form a linked list pointed by g.
    */
    f = g;
    while (f != NULL) {
#ifdef DD_COUNT
        table->swapSteps++;
#endif
        next = f->next;
        /* Find f1, f0, f11, f10, f01, f00. */
        f1 = cuddT(f);
        if ((int) f1->index == yindex || (int) f1->index == xindex) {
            f11 = cuddT(f1); f10 = cuddE(f1);
        } else {
            f11 = empty; f10 = f1;
        }
        f0 = cuddE(f);
        if ((int) f0->index == yindex || (int) f0->index == xindex) {
            f01 = cuddT(f0); f00 = cuddE(f0);
        } else {
            f01 = empty; f00 = f0;
        }
        /* Create the new T child. */
        if (f01 == empty) {
            newf1 = f10;
            cuddSatInc(newf1->ref);
        } else {
            /* Check ylist for triple (yindex, f01, f10). */
            posn = ddHash(f01, f10, yshift);
            /* For each element newf1 in collision list ylist[posn]. */
            newf1 = ylist[posn];
            /* Search the collision chain skipping the marked nodes. */
            while (newf1 != NULL) {
                if (cuddT(newf1) == f01 && cuddE(newf1) == f10 &&
                    (int) newf1->index == yindex) {
                    cuddSatInc(newf1->ref);
                    break; /* match */
                }
                newf1 = newf1->next;
            } /* while newf1 */
            if (newf1 == NULL) {        /* no match */
                newf1 = cuddDynamicAllocNode(table);
                if (newf1 == NULL)
                    goto zddSwapOutOfMem;
                newf1->index = yindex; newf1->ref = 1;
                cuddT(newf1) = f01;
                cuddE(newf1) = f10;
                /* Insert newf1 in the collision list ylist[pos];
                ** increase the ref counts of f01 and f10
                */
                newykeys++;
                newf1->next = ylist[posn];
                ylist[posn] = newf1;
                cuddSatInc(f01->ref);
                cuddSatInc(f10->ref);
            }
        }
        cuddT(f) = newf1;

        /* Do the same for f0. */
        /* Create the new E child. */
        if (f11 == empty) {
            newf0 = f00;
            cuddSatInc(newf0->ref);
        } else {
            /* Check ylist for triple (yindex, f11, f00). */
            posn = ddHash(f11, f00, yshift);
            /* For each element newf0 in collision list ylist[posn]. */
            newf0 = ylist[posn];
            while (newf0 != NULL) {
                if (cuddT(newf0) == f11 && cuddE(newf0) == f00 &&
                    (int) newf0->index == yindex) {
                    cuddSatInc(newf0->ref);
                    break; /* match */
                }
                newf0 = newf0->next;
            } /* while newf0 */
            if (newf0 == NULL) {        /* no match */
                newf0 = cuddDynamicAllocNode(table);
                if (newf0 == NULL)
                    goto zddSwapOutOfMem;
                newf0->index = yindex; newf0->ref = 1;
                cuddT(newf0) = f11; cuddE(newf0) = f00;
                /* Insert newf0 in the collision list ylist[posn];
                ** increase the ref counts of f11 and f00.
                */
                newykeys++;
                newf0->next = ylist[posn];
                ylist[posn] = newf0;
                cuddSatInc(f11->ref);
                cuddSatInc(f00->ref);
            }
        }
        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++;
        f->next = xlist[posn];
        xlist[posn] = f;
        f = next;
    } /* while f != NULL */

    /* GC the y layer and move the marked nodes to the x list. */

    /* For each node f in ylist. */
    for (i = 0; i < yslots; i++) {
        previous = NULL;
        f = ylist[i];
        while (f != NULL) {
            next = f->next;
            if (f->ref == 0) {
                cuddSatDec(cuddT(f)->ref);
                cuddSatDec(cuddE(f)->ref);
                cuddDeallocNode(table, f);
                newykeys--;
                if (previous == NULL)
                    ylist[i] = next;
                else
                    previous->next = next;
            } else if ((int) f->index == xindex) { /* move marked node */
                if (previous == NULL)
                    ylist[i] = next;
                else
                    previous->next = next;
                f1 = cuddT(f);
                cuddSatDec(f1->ref);
                /* Check ylist for triple (yindex, f1, empty). */
                posn = ddHash(f1, empty, yshift);
                /* For each element newf1 in collision list ylist[posn]. */
                newf1 = ylist[posn];
                while (newf1 != NULL) {
                    if (cuddT(newf1) == f1 && cuddE(newf1) == empty &&
                        (int) newf1->index == yindex) {
                        cuddSatInc(newf1->ref);
                        break; /* match */
                    }
                    newf1 = newf1->next;
                } /* while newf1 */
                if (newf1 == NULL) {    /* no match */
                    newf1 = cuddDynamicAllocNode(table);
                    if (newf1 == NULL)
                        goto zddSwapOutOfMem;
                    newf1->index = yindex; newf1->ref = 1;
                    cuddT(newf1) = f1; cuddE(newf1) = empty;
                    /* Insert newf1 in the collision list ylist[posn];
                    ** increase the ref counts of f1 and empty.
                    */
                    newykeys++;
                    newf1->next = ylist[posn];
                    ylist[posn] = newf1;
                    if (posn == i && previous == NULL)
                        previous = newf1;
                    cuddSatInc(f1->ref);
                    cuddSatInc(empty->ref);
                }
                cuddT(f) = newf1;
                f0 = cuddE(f);
                /* Insert f in x list. */
                posn = ddHash(newf1, f0, xshift);
                newxkeys++;
                newykeys--;
                f->next = xlist[posn];
                xlist[posn] = f;
            } else {
                previous = f;
            }
            f = next;
        } /* while f */
    } /* for i */

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

    table->keysZ += newxkeys + newykeys - oldxkeys - oldykeys;

    /* Update univ section; univ[x] remains the same. */
    table->univ[y] = cuddT(table->univ[x]);

#if 0
    (void) fprintf(table->out,"x = %d  y = %d\n", x, y);
    (void) Cudd_DebugCheck(table);
    (void) Cudd_CheckKeys(table);
#endif

    return (table->keysZ);

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

    return (0);

} /* end of cuddZddLinearInPlace */


static int
cuddZddLinearAux(
  DdManager * table,
  int  x,
  int  xLow,
  int  xHigh)
{
    Move        *move;
    Move        *moveUp;        /* list of up move */
    Move        *moveDown;      /* list of down move */

    int         initial_size;
    int         result;

    initial_size = table->keysZ;

#ifdef DD_DEBUG
    assert(table->subtableZ[x].keys > 0);
#endif

    moveDown = NULL;
    moveUp = NULL;

    if (x == xLow) {
        moveDown = cuddZddLinearDown(table, x, xHigh, NULL);
        /* At this point x --> xHigh. */
        if (moveDown == (Move *) CUDD_OUT_OF_MEM)
            goto cuddZddLinearAuxOutOfMem;
        /* Move backward and stop at best position. */
        result = cuddZddLinearBackward(table, initial_size, moveDown);
        if (!result)
            goto cuddZddLinearAuxOutOfMem;

    } else if (x == xHigh) {
        moveUp = cuddZddLinearUp(table, x, xLow, NULL);
        /* At this point x --> xLow. */
        if (moveUp == (Move *) CUDD_OUT_OF_MEM)
            goto cuddZddLinearAuxOutOfMem;
        /* Move backward and stop at best position. */
        result = cuddZddLinearBackward(table, initial_size, moveUp);
        if (!result)
            goto cuddZddLinearAuxOutOfMem;

    } else if ((x - xLow) > (xHigh - x)) { /* must go down first: shorter */
        moveDown = cuddZddLinearDown(table, x, xHigh, NULL);
        /* At this point x --> xHigh. */
        if (moveDown == (Move *) CUDD_OUT_OF_MEM)
            goto cuddZddLinearAuxOutOfMem;
        moveUp = cuddZddUndoMoves(table,moveDown);
#ifdef DD_DEBUG
        assert(moveUp == NULL || moveUp->x == x);
#endif
        moveUp = cuddZddLinearUp(table, x, xLow, moveUp);
        if (moveUp == (Move *) CUDD_OUT_OF_MEM)
            goto cuddZddLinearAuxOutOfMem;
        /* Move backward and stop at best position. */
        result = cuddZddLinearBackward(table, initial_size, moveUp);
        if (!result)
            goto cuddZddLinearAuxOutOfMem;

    } else {
        moveUp = cuddZddLinearUp(table, x, xLow, NULL);
        /* At this point x --> xHigh. */
        if (moveUp == (Move *) CUDD_OUT_OF_MEM)
            goto cuddZddLinearAuxOutOfMem;
        /* Then move up. */
        moveDown = cuddZddUndoMoves(table,moveUp);
#ifdef DD_DEBUG
        assert(moveDown == NULL || moveDown->y == x);
#endif
        moveDown = cuddZddLinearDown(table, x, xHigh, moveDown);
        if (moveDown == (Move *) CUDD_OUT_OF_MEM)
            goto cuddZddLinearAuxOutOfMem;
        /* Move backward and stop at best position. */
        result = cuddZddLinearBackward(table, initial_size, moveDown);
        if (!result)
            goto cuddZddLinearAuxOutOfMem;
    }

    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);

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

    return(0);

} /* end of cuddZddLinearAux */


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) {
            /* Undo transformation. The transformation we apply is
            ** its own inverse. Hence, we just apply the transformation
            ** again.
            */
            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;
        cuddDeallocNode(table, (DdNode *)moves);
        moves = move;
    }
    return((Move *) CUDD_OUT_OF_MEM);

} /* end of cuddZddLinearUp */


static Move *
cuddZddLinearDown(
  DdManager * table,
  int  x,
  int  xHigh,
  Move * prevMoves)
{
    Move        *moves;
    Move        *move;
    int         y;
    int         size, newsize;
    int         limitSize;

    moves = prevMoves;
    limitSize = table->keysZ;

    y = cuddZddNextHigh(table, x);
    while (y <= xHigh) {
        size = cuddZddSwapInPlace(table, x, y);
        if (size == 0)
            goto cuddZddLinearDownOutOfMem;
        newsize = cuddZddLinearInPlace(table, x, y);
        if (newsize == 0)
            goto cuddZddLinearDownOutOfMem;
        move = (Move *) cuddDynamicAllocNode(table);
        if (move == NULL)
            goto cuddZddLinearDownOutOfMem;
        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 = cuddZddLinearInPlace(table,x,y);
            if (newsize == 0) goto cuddZddLinearDownOutOfMem;
            if (newsize != size) {
                (void) fprintf(table->err,"Change in size after identity transformation! From %d to %d\n",size,newsize);
            }
        } 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;

        x = y;
        y = cuddZddNextHigh(table, x);
    }
    return(moves);

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

} /* end of cuddZddLinearDown */


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

    /* Find the minimum size among moves. */
    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 = cuddZddLinearInPlace(table,(int)move->x,(int)move->y);
            if (!res) return(0);
        }
        res = cuddZddSwapInPlace(table, move->x, move->y);
        if (!res)
            return(0);
        if (move->flags == CUDD_INVERSE_TRANSFORM_MOVE) {
            res = cuddZddLinearInPlace(table,(int)move->x,(int)move->y);
            if (!res) return(0);
        }
    }

    return(1);

} /* end of cuddZddLinearBackward */


static Move*
cuddZddUndoMoves(
  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 cuddZddUndoMovesOutOfMem;
        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 = cuddZddSwapInPlace(table,(int)move->x,(int)move->y);
            if (!size) goto cuddZddUndoMovesOutOfMem;
        } else if (move->flags == CUDD_LINEAR_TRANSFORM_MOVE) {
            invmove->flags = CUDD_INVERSE_TRANSFORM_MOVE;
            size = cuddZddLinearInPlace(table,(int)move->x,(int)move->y);
            if (!size) goto cuddZddUndoMovesOutOfMem;
            size = cuddZddSwapInPlace(table,(int)move->x,(int)move->y);
            if (!size) goto cuddZddUndoMovesOutOfMem;
        } 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 = cuddZddSwapInPlace(table,(int)move->x,(int)move->y);
            if (!size) goto cuddZddUndoMovesOutOfMem;
            size = cuddZddLinearInPlace(table,(int)move->x,(int)move->y);
            if (!size) goto cuddZddUndoMovesOutOfMem;
        }
        invmove->size = size;
    }

    return(invmoves);

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

} /* end of cuddZddUndoMoves */

---