src/bdd/cudd/cuddZddLin.c File Reference

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

Include dependency graph for cuddZddLin.c:

Go to the source code of this file.

Defines
#define	CUDD_SWAP_MOVE   0
#define	CUDD_LINEAR_TRANSFORM_MOVE   1
#define	CUDD_INVERSE_TRANSFORM_MOVE   2
Functions
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))
int	cuddZddLinearSifting (DdManager *table, int lower, int upper)
int	cuddZddLinearInPlace (DdManager *table, int x, int y)
static int	cuddZddLinearAux (DdManager *table, int x, int xLow, int xHigh)
static Move *	cuddZddLinearUp (DdManager *table, int y, int xLow, Move *prevMoves)
static Move *	cuddZddLinearDown (DdManager *table, int x, int xHigh, Move *prevMoves)
static int	cuddZddLinearBackward (DdManager *table, int size, Move *moves)
static Move *	cuddZddUndoMoves (DdManager *table, Move *moves)
Variables
static char rcsid[]	DD_UNUSED = "$Id: cuddZddLin.c,v 1.1.1.1 2003/02/24 22:23:54 wjiang Exp $"
int *	zdd_entry
int	zddTotalNumberSwapping
static int	zddTotalNumberLinearTr
static DdNode *	empty

---

Define Documentation

#define CUDD_INVERSE_TRANSFORM_MOVE   2

Definition at line 44 of file cuddZddLin.c.

#define CUDD_LINEAR_TRANSFORM_MOVE   1

Definition at line 43 of file cuddZddLin.c.

#define CUDD_SWAP_MOVE   0

CFile***********************************************************************

FileName [cuddZddLin.c]

PackageName [cudd]

Synopsis [Procedures for dynamic variable ordering of ZDDs.]

Description [Internal procedures included in this module:

• cuddZddLinearSifting()

Static procedures included in this module:

• cuddZddLinearInPlace()
• cuddZddLinerAux()
• cuddZddLinearUp()
• cuddZddLinearDown()
• cuddZddLinearBackward()
• cuddZddUndoMoves()

]

SeeAlso [cuddLinear.c cuddZddReord.c]

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.]

Definition at line 42 of file cuddZddLin.c.

---

Function Documentation

static Move* cuddZddUndoMoves ARGS

(

(DdManager *table, Move *moves)

)

[static]

static int cuddZddLinearBackward ARGS

(

(DdManager *table, int size, Move *moves)

)

[static]

static Move* cuddZddLinearDown ARGS

(

(DdManager *table, int x, int xHigh, Move *prevMoves)

)

[static]

static Move* cuddZddLinearUp ARGS

(

(DdManager *table, int y, int xLow, Move *prevMoves)

)

[static]

static int cuddZddLinearAux ARGS

(

(DdManager *table, int x, int xLow, int xHigh)

)

[static]

AutomaticStart

static int cuddZddLinearAux	(	DdManager *	table,
		int	x,
		int	xLow,
		int	xHigh
	)			[static]

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. Finds the best position and does the required changes. Returns 1 if successful; 0 otherwise.]

SideEffects [None]

SeeAlso []

Definition at line 545 of file cuddZddLin.c.

{
    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 int cuddZddLinearBackward	(	DdManager *	table,
		int	size,
		Move *	moves
	)			[static]

Function********************************************************************

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

Description [Given a set of moves, returns the ZDD 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]

SeeAlso []

Definition at line 841 of file cuddZddLin.c.

{
    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* cuddZddLinearDown	(	DdManager *	table,
		int	x,
		int	xHigh,
		Move *	prevMoves
	)			[static]

Function********************************************************************

Synopsis [Sifts a variable down and applies the XOR transformation.]

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

SideEffects [None]

SeeAlso []

Definition at line 757 of file cuddZddLin.c.

{
    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 */

int cuddZddLinearInPlace	(	DdManager *	table,
		int	x,
		int	y
	)

Function********************************************************************

Synopsis [Linearly combines two adjacent variables.]

Description [Linearly combines two adjacent 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. cuddZddLinearInPlace assumes that x < y. Returns the number of keys in the table if successful; 0 otherwise.]

SideEffects [None]

SeeAlso [cuddZddSwapInPlace cuddLinearInPlace]

Definition at line 223 of file cuddZddLin.c.

{
    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 */

int cuddZddLinearSifting	(	DdManager *	table,
		int	lower,
		int	upper
	)

AutomaticEnd Function********************************************************************

Synopsis [Implementation of the linear sifting algorithm for ZDDs.]

Description [Implementation of the linear sifting algorithm for ZDDs. Assumes that no dead nodes are present.

1. Order all the variables according to the number of entries in each unique table.
2. Sift the variable up and down and applies the XOR transformation, remembering each time the total size of the DD heap.
3. Select the best permutation.
4. Repeat 3 and 4 for all variables.

Returns 1 if successful; 0 otherwise.]

SideEffects [None]

SeeAlso []

Definition at line 124 of file cuddZddLin.c.

{
    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 */

static Move* cuddZddLinearUp	(	DdManager *	table,
		int	y,
		int	xLow,
		Move *	prevMoves
	)			[static]

Function********************************************************************

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

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

SideEffects [None]

SeeAlso []

Definition at line 672 of file cuddZddLin.c.

{
    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* cuddZddUndoMoves	(	DdManager *	table,
		Move *	moves
	)			[static]

Function********************************************************************

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

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

SideEffects [None]

Definition at line 889 of file cuddZddLin.c.

{
    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 */

---

Variable Documentation

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

Definition at line 61 of file cuddZddLin.c.

DdNode* empty [static]

Definition at line 67 of file cuddZddLin.c.

int* zdd_entry

Definition at line 77 of file cuddZddReord.c.

int zddTotalNumberLinearTr [static]

Definition at line 66 of file cuddZddLin.c.

int zddTotalNumberSwapping

Definition at line 79 of file cuddZddReord.c.