src/bdd/cudd/cuddZddGroup.c File Reference

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

Include dependency graph for cuddZddGroup.c:

Go to the source code of this file.

Functions
static int zddTreeSiftingAux	ARGS ((DdManager *table, MtrNode *treenode, Cudd_ReorderingType method))
static void zddFindNodeHiLo	ARGS ((DdManager *table, MtrNode *treenode, int *lower, int *upper))
static int zddUniqueCompareGroup	ARGS ((int *ptrX, int *ptrY))
static int zddGroupSifting	ARGS ((DdManager *table, int lower, int upper))
static int zddGroupSiftingAux	ARGS ((DdManager *table, int x, int xLow, int xHigh))
static int zddGroupSiftingUp	ARGS ((DdManager *table, int y, int xLow, Move **moves))
static int zddGroupSiftingDown	ARGS ((DdManager *table, int x, int xHigh, Move **moves))
static int zddGroupMove	ARGS ((DdManager *table, int x, int y, Move **moves))
static int zddGroupMoveBackward	ARGS ((DdManager *table, int x, int y))
static int zddGroupSiftingBackward	ARGS ((DdManager *table, Move *moves, int size))
static void zddMergeGroups	ARGS ((DdManager *table, MtrNode *treenode, int low, int high))
MtrNode *	Cudd_MakeZddTreeNode (DdManager *dd, unsigned int low, unsigned int size, unsigned int type)
int	cuddZddTreeSifting (DdManager *table, Cudd_ReorderingType method)
static int	zddTreeSiftingAux (DdManager *table, MtrNode *treenode, Cudd_ReorderingType method)
static int	zddReorderChildren (DdManager *table, MtrNode *treenode, Cudd_ReorderingType method)
static void	zddFindNodeHiLo (DdManager *table, MtrNode *treenode, int *lower, int *upper)
static int	zddUniqueCompareGroup (int *ptrX, int *ptrY)
static int	zddGroupSifting (DdManager *table, int lower, int upper)
static int	zddGroupSiftingAux (DdManager *table, int x, int xLow, int xHigh)
static int	zddGroupSiftingUp (DdManager *table, int y, int xLow, Move **moves)
static int	zddGroupSiftingDown (DdManager *table, int x, int xHigh, Move **moves)
static int	zddGroupMove (DdManager *table, int x, int y, Move **moves)
static int	zddGroupMoveBackward (DdManager *table, int x, int y)
static int	zddGroupSiftingBackward (DdManager *table, Move *moves, int size)
static void	zddMergeGroups (DdManager *table, MtrNode *treenode, int low, int high)
Variables
static char rcsid[]	DD_UNUSED = "$Id: cuddZddGroup.c,v 1.1.1.1 2003/02/24 22:23:54 wjiang Exp $"
static int *	entry
int	zddTotalNumberSwapping

---

Function Documentation

static void zddMergeGroups ARGS

(

(DdManager *table, MtrNode *treenode, int low, int high)

)

[static]

static int zddGroupSiftingBackward ARGS

(

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

)

[static]

static int zddGroupMoveBackward ARGS

(

(DdManager *table, int x, int y)

)

[static]

static int zddGroupMove ARGS

(

(DdManager *table, int x, int y, Move **moves)

)

[static]

static int zddGroupSiftingDown ARGS

(

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

)

[static]

static int zddGroupSiftingUp ARGS

(

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

)

[static]

static int zddGroupSiftingAux ARGS

(

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

)

[static]

static int zddGroupSifting ARGS

(

(DdManager *table, int lower, int upper)

)

[static]

static int zddUniqueCompareGroup ARGS

(

(int *ptrX, int *ptrY)

)

[static]

static void zddFindNodeHiLo ARGS

(

(DdManager *table, MtrNode *treenode, int *lower, int *upper)

)

[static]

static int zddReorderChildren ARGS

(

(DdManager *table, MtrNode *treenode, Cudd_ReorderingType method)

)

[static]

AutomaticStart

MtrNode* Cudd_MakeZddTreeNode	(	DdManager *	dd,
		unsigned int	low,
		unsigned int	size,
		unsigned int	type
	)

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

Synopsis [Creates a new ZDD variable group.]

Description [Creates a new ZDD variable group. The group starts at variable and contains size variables. The parameter low is the index of the first variable. If the variable already exists, its current position in the order is known to the manager. If the variable does not exist yet, the position is assumed to be the same as the index. The group tree is created if it does not exist yet. Returns a pointer to the group if successful; NULL otherwise.]

SideEffects [The ZDD variable tree is changed.]

SeeAlso [Cudd_MakeTreeNode]

Definition at line 132 of file cuddZddGroup.c.

{
    MtrNode *group;
    MtrNode *tree;
    unsigned int level;

    /* If the variable does not exist yet, the position is assumed to be
    ** the same as the index. Therefore, applications that rely on
    ** Cudd_bddNewVarAtLevel or Cudd_addNewVarAtLevel to create new
    ** variables have to create the variables before they group them.
    */
    level = (low < (unsigned int) dd->sizeZ) ? dd->permZ[low] : low;

    if (level + size - 1> (int) MTR_MAXHIGH)
        return(NULL);

    /* If the tree does not exist yet, create it. */
    tree = dd->treeZ;
    if (tree == NULL) {
        dd->treeZ = tree = Mtr_InitGroupTree(0, dd->sizeZ);
        if (tree == NULL)
            return(NULL);
        tree->index = dd->invpermZ[0];
    }

    /* Extend the upper bound of the tree if necessary. This allows the
    ** application to create groups even before the variables are created.
    */
    tree->size = ddMax(tree->size, level + size);

    /* Create the group. */
    group = Mtr_MakeGroup(tree, level, size, type);
    if (group == NULL)
        return(NULL);

    /* Initialize the index field to the index of the variable currently
    ** in position low. This field will be updated by the reordering
    ** procedure to provide a handle to the group once it has been moved.
    */
    group->index = (MtrHalfWord) low;

    return(group);

} /* end of Cudd_MakeZddTreeNode */

int cuddZddTreeSifting	(	DdManager *	table,
		Cudd_ReorderingType	method
	)

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

Synopsis [Tree sifting algorithm for ZDDs.]

Description [Tree sifting algorithm for ZDDs. Assumes that a tree representing a group hierarchy is passed as a parameter. It then reorders each group in postorder fashion by calling zddTreeSiftingAux. Assumes that no dead nodes are present. Returns 1 if successful; 0 otherwise.]

SideEffects [None]

Definition at line 201 of file cuddZddGroup.c.

{
    int i;
    int nvars;
    int result;
    int tempTree;

    /* If no tree is provided we create a temporary one in which all
    ** variables are in a single group. After reordering this tree is
    ** destroyed.
    */
    tempTree = table->treeZ == NULL;
    if (tempTree) {
        table->treeZ = Mtr_InitGroupTree(0,table->sizeZ);
        table->treeZ->index = table->invpermZ[0];
    }
    nvars = table->sizeZ;

#ifdef DD_DEBUG
    if (pr > 0 && !tempTree)
        (void) fprintf(table->out,"cuddZddTreeSifting:");
    Mtr_PrintGroups(table->treeZ,pr <= 0);
#endif
#if 0
    /* Debugging code. */
    if (table->tree && table->treeZ) {
        (void) fprintf(table->out,"\n");
        Mtr_PrintGroups(table->tree, 0);
        cuddPrintVarGroups(table,table->tree,0,0);
        for (i = 0; i < table->size; i++) {
            (void) fprintf(table->out,"%s%d",
                           (i == 0) ? "" : ",", table->invperm[i]);
        }
        (void) fprintf(table->out,"\n");
        for (i = 0; i < table->size; i++) {
            (void) fprintf(table->out,"%s%d",
                           (i == 0) ? "" : ",", table->perm[i]);
        }
        (void) fprintf(table->out,"\n\n");
        Mtr_PrintGroups(table->treeZ,0);
        cuddPrintVarGroups(table,table->treeZ,1,0);
        for (i = 0; i < table->sizeZ; i++) {
            (void) fprintf(table->out,"%s%d",
                           (i == 0) ? "" : ",", table->invpermZ[i]);
        }
        (void) fprintf(table->out,"\n");
        for (i = 0; i < table->sizeZ; i++) {
            (void) fprintf(table->out,"%s%d",
                           (i == 0) ? "" : ",", table->permZ[i]);
        }
        (void) fprintf(table->out,"\n");
    }
    /* End of debugging code. */
#endif
#ifdef DD_STATS
    extsymmcalls = 0;
    extsymm = 0;
    secdiffcalls = 0;
    secdiff = 0;
    secdiffmisfire = 0;

    (void) fprintf(table->out,"\n");
    if (!tempTree)
        (void) fprintf(table->out,"#:IM_NODES  %8d: group tree nodes\n",
                       zddCountInternalMtrNodes(table,table->treeZ));
#endif

    /* Initialize the group of each subtable to itself. Initially
    ** there are no groups. Groups are created according to the tree
    ** structure in postorder fashion.
    */
    for (i = 0; i < nvars; i++)
        table->subtableZ[i].next = i;

    /* Reorder. */
    result = zddTreeSiftingAux(table, table->treeZ, method);

#ifdef DD_STATS         /* print stats */
    if (!tempTree && method == CUDD_REORDER_GROUP_SIFT &&
        (table->groupcheck == CUDD_GROUP_CHECK7 ||
         table->groupcheck == CUDD_GROUP_CHECK5)) {
        (void) fprintf(table->out,"\nextsymmcalls = %d\n",extsymmcalls);
        (void) fprintf(table->out,"extsymm = %d",extsymm);
    }
    if (!tempTree && method == CUDD_REORDER_GROUP_SIFT &&
        table->groupcheck == CUDD_GROUP_CHECK7) {
        (void) fprintf(table->out,"\nsecdiffcalls = %d\n",secdiffcalls);
        (void) fprintf(table->out,"secdiff = %d\n",secdiff);
        (void) fprintf(table->out,"secdiffmisfire = %d",secdiffmisfire);
    }
#endif

    if (tempTree)
        Cudd_FreeZddTree(table);
    return(result);

} /* end of cuddZddTreeSifting */

static void zddFindNodeHiLo	(	DdManager *	table,
		MtrNode *	treenode,
		int *	lower,
		int *	upper
	)			[static]

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

Synopsis [Finds the lower and upper bounds of the group represented by treenode.]

Description [Finds the lower and upper bounds of the group represented by treenode. The high and low fields of treenode are indices. From those we need to derive the current positions, and find maximum and minimum.]

SideEffects [The bounds are returned as side effects.]

SeeAlso []

Definition at line 503 of file cuddZddGroup.c.

{
    int low;
    int high;

    /* Check whether no variables in this group already exist.
    ** If so, return immediately. The calling procedure will know from
    ** the values of upper that no reordering is needed.
    */
    if ((int) treenode->low >= table->sizeZ) {
        *lower = table->sizeZ;
        *upper = -1;
        return;
    }

    *lower = low = (unsigned int) table->permZ[treenode->index];
    high = (int) (low + treenode->size - 1);

    if (high >= table->sizeZ) {
        /* This is the case of a partially existing group. The aim is to
        ** reorder as many variables as safely possible.  If the tree
        ** node is terminal, we just reorder the subset of the group
        ** that is currently in existence.  If the group has
        ** subgroups, then we only reorder those subgroups that are
        ** fully instantiated.  This way we avoid breaking up a group.
        */
        MtrNode *auxnode = treenode->child;
        if (auxnode == NULL) {
            *upper = (unsigned int) table->sizeZ - 1;
        } else {
            /* Search the subgroup that strands the table->sizeZ line.
            ** If the first group starts at 0 and goes past table->sizeZ
            ** upper will get -1, thus correctly signaling that no reordering
            ** should take place.
            */
            while (auxnode != NULL) {
                int thisLower = table->permZ[auxnode->low];
                int thisUpper = thisLower + auxnode->size - 1;
                if (thisUpper >= table->sizeZ && thisLower < table->sizeZ)
                    *upper = (unsigned int) thisLower - 1;
                auxnode = auxnode->younger;
            }
        }
    } else {
        /* Normal case: All the variables of the group exist. */
        *upper = (unsigned int) high;
    }

#ifdef DD_DEBUG
    /* Make sure that all variables in group are contiguous. */
    assert(treenode->size >= *upper - *lower + 1);
#endif

    return;

} /* end of zddFindNodeHiLo */

static int zddGroupMove	(	DdManager *	table,
		int	x,
		int	y,
		Move **	moves
	)			[static]

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

Synopsis [Swaps two groups and records the move.]

Description [Swaps two groups and records the move. Returns the number of keys in the DD table in case of success; 0 otherwise.]

SideEffects [None]

Definition at line 1054 of file cuddZddGroup.c.

{
    Move *move;
    int  size;
    int  i,j,xtop,xbot,xsize,ytop,ybot,ysize,newxtop;
    int  swapx,swapy;
#if defined(DD_DEBUG) && defined(DD_VERBOSE)
    int  initialSize,bestSize;
#endif

#if DD_DEBUG
    /* We assume that x < y */
    assert(x < y);
#endif
    /* Find top, bottom, and size for the two groups. */
    xbot = x;
    xtop = table->subtableZ[x].next;
    xsize = xbot - xtop + 1;
    ybot = y;
    while ((unsigned) ybot < table->subtableZ[ybot].next)
        ybot = table->subtableZ[ybot].next;
    ytop = y;
    ysize = ybot - ytop + 1;

#if defined(DD_DEBUG) && defined(DD_VERBOSE)
    initialSize = bestSize = table->keysZ;
#endif
    /* Sift the variables of the second group up through the first group */
    for (i = 1; i <= ysize; i++) {
        for (j = 1; j <= xsize; j++) {
            size = cuddZddSwapInPlace(table,x,y);
            if (size == 0) goto zddGroupMoveOutOfMem;
#if defined(DD_DEBUG) && defined(DD_VERBOSE)
            if (size < bestSize)
                bestSize = size;
#endif
            swapx = x; swapy = y;
            y = x;
            x = cuddZddNextLow(table,y);
        }
        y = ytop + i;
        x = cuddZddNextLow(table,y);
    }
#if defined(DD_DEBUG) && defined(DD_VERBOSE)
    if ((bestSize < initialSize) && (bestSize < size))
        (void) fprintf(table->out,"Missed local minimum: initialSize:%d  bestSize:%d  finalSize:%d\n",initialSize,bestSize,size);
#endif

    /* fix groups */
    y = xtop; /* ytop is now where xtop used to be */
    for (i = 0; i < ysize - 1; i++) {
        table->subtableZ[y].next = cuddZddNextHigh(table,y);
        y = cuddZddNextHigh(table,y);
    }
    table->subtableZ[y].next = xtop; /* y is bottom of its group, join */
                                    /* it to top of its group */
    x = cuddZddNextHigh(table,y);
    newxtop = x;
    for (i = 0; i < xsize - 1; i++) {
        table->subtableZ[x].next = cuddZddNextHigh(table,x);
        x = cuddZddNextHigh(table,x);
    }
    table->subtableZ[x].next = newxtop; /* x is bottom of its group, join */
                                    /* it to top of its group */
#ifdef DD_DEBUG
    if (pr > 0) (void) fprintf(table->out,"zddGroupMove:\n");
#endif

    /* Store group move */
    move = (Move *) cuddDynamicAllocNode(table);
    if (move == NULL) goto zddGroupMoveOutOfMem;
    move->x = swapx;
    move->y = swapy;
    move->flags = MTR_DEFAULT;
    move->size = table->keysZ;
    move->next = *moves;
    *moves = move;

    return(table->keysZ);

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

} /* end of zddGroupMove */

static int zddGroupMoveBackward	(	DdManager *	table,
		int	x,
		int	y
	)			[static]

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

Synopsis [Undoes the swap two groups.]

Description [Undoes the swap two groups. Returns 1 in case of success; 0 otherwise.]

SideEffects [None]

Definition at line 1160 of file cuddZddGroup.c.

{
    int size;
    int i,j,xtop,xbot,xsize,ytop,ybot,ysize,newxtop;


#if DD_DEBUG
    /* We assume that x < y */
    assert(x < y);
#endif

    /* Find top, bottom, and size for the two groups. */
    xbot = x;
    xtop = table->subtableZ[x].next;
    xsize = xbot - xtop + 1;
    ybot = y;
    while ((unsigned) ybot < table->subtableZ[ybot].next)
        ybot = table->subtableZ[ybot].next;
    ytop = y;
    ysize = ybot - ytop + 1;

    /* Sift the variables of the second group up through the first group */
    for (i = 1; i <= ysize; i++) {
        for (j = 1; j <= xsize; j++) {
            size = cuddZddSwapInPlace(table,x,y);
            if (size == 0)
                return(0);
            y = x;
            x = cuddZddNextLow(table,y);
        }
        y = ytop + i;
        x = cuddZddNextLow(table,y);
    }

    /* fix groups */
    y = xtop;
    for (i = 0; i < ysize - 1; i++) {
        table->subtableZ[y].next = cuddZddNextHigh(table,y);
        y = cuddZddNextHigh(table,y);
    }
    table->subtableZ[y].next = xtop; /* y is bottom of its group, join */
                                    /* to its top */
    x = cuddZddNextHigh(table,y);
    newxtop = x;
    for (i = 0; i < xsize - 1; i++) {
        table->subtableZ[x].next = cuddZddNextHigh(table,x);
        x = cuddZddNextHigh(table,x);
    }
    table->subtableZ[x].next = newxtop; /* x is bottom of its group, join */
                                    /* to its top */
#ifdef DD_DEBUG
    if (pr > 0) (void) fprintf(table->out,"zddGroupMoveBackward:\n");
#endif

    return(1);

} /* end of zddGroupMoveBackward */

static int zddGroupSifting	(	DdManager *	table,
		int	lower,
		int	upper
	)			[static]

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

Synopsis [Sifts from treenode->low to treenode->high.]

Description [Sifts from treenode->low to treenode->high. If croupcheck == CUDD_GROUP_CHECK7, it checks for group creation at the end of the initial sifting. If a group is created, it is then sifted again. After sifting one variable, the group that contains it is dissolved. Returns 1 in case of success; 0 otherwise.]

SideEffects [None]

Definition at line 606 of file cuddZddGroup.c.

{
    int         *var;
    int         i,j,x,xInit;
    int         nvars;
    int         classes;
    int         result;
    int         *sifted;
#ifdef DD_STATS
    unsigned    previousSize;
#endif
    int         xindex;

    nvars = table->sizeZ;

    /* Order variables to sift. */
    entry = NULL;
    sifted = NULL;
    var = ALLOC(int,nvars);
    if (var == NULL) {
        table->errorCode = CUDD_MEMORY_OUT;
        goto zddGroupSiftingOutOfMem;
    }
    entry = ALLOC(int,nvars);
    if (entry == NULL) {
        table->errorCode = CUDD_MEMORY_OUT;
        goto zddGroupSiftingOutOfMem;
    }
    sifted = ALLOC(int,nvars);
    if (sifted == NULL) {
        table->errorCode = CUDD_MEMORY_OUT;
        goto zddGroupSiftingOutOfMem;
    }

    /* Here we consider only one representative for each group. */
    for (i = 0, classes = 0; i < nvars; i++) {
        sifted[i] = 0;
        x = table->permZ[i];
        if ((unsigned) x >= table->subtableZ[x].next) {
            entry[i] = table->subtableZ[x].keys;
            var[classes] = i;
            classes++;
        }
    }

    qsort((void *)var,classes,sizeof(int),(int (*)(const void *, const void *))zddUniqueCompareGroup);

    /* Now sift. */
    for (i = 0; i < ddMin(table->siftMaxVar,classes); i++) {
        if (zddTotalNumberSwapping >= table->siftMaxSwap)
            break;
        xindex = var[i];
        if (sifted[xindex] == 1) /* variable already sifted as part of group */
            continue;
        x = table->permZ[xindex]; /* find current level of this variable */
        if (x < lower || x > upper)
            continue;
#ifdef DD_STATS
        previousSize = table->keysZ;
#endif
#ifdef DD_DEBUG
        /* x is bottom of group */
        assert((unsigned) x >= table->subtableZ[x].next);
#endif
        result = zddGroupSiftingAux(table,x,lower,upper);
        if (!result) goto zddGroupSiftingOutOfMem;

#ifdef DD_STATS
        if (table->keysZ < previousSize) {
            (void) fprintf(table->out,"-");
        } else if (table->keysZ > previousSize) {
            (void) fprintf(table->out,"+");
        } else {
            (void) fprintf(table->out,"=");
        }
        fflush(table->out);
#endif

        /* Mark variables in the group just sifted. */
        x = table->permZ[xindex];
        if ((unsigned) x != table->subtableZ[x].next) {
            xInit = x;
            do {
                j = table->invpermZ[x];
                sifted[j] = 1;
                x = table->subtableZ[x].next;
            } while (x != xInit);
        }

#ifdef DD_DEBUG
        if (pr > 0) (void) fprintf(table->out,"zddGroupSifting:");
#endif
    } /* for */

    FREE(sifted);
    FREE(var);
    FREE(entry);

    return(1);

zddGroupSiftingOutOfMem:
    if (entry != NULL)  FREE(entry);
    if (var != NULL)    FREE(var);
    if (sifted != NULL) FREE(sifted);

    return(0);

} /* end of zddGroupSifting */

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

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

Synopsis [Sifts one variable up and down until it has taken all positions. Checks for aggregation.]

Description [Sifts one variable up and down until it has taken all positions. Checks for aggregation. There may be at most two sweeps, even if the group grows. Assumes that x is either an isolated variable, or it is the bottom of a group. All groups may not have been found. The variable being moved is returned to the best position seen during sifting. Returns 1 in case of success; 0 otherwise.]

SideEffects [None]

Definition at line 735 of file cuddZddGroup.c.

{
    Move *move;
    Move *moves;        /* list of moves */
    int  initialSize;
    int  result;


#ifdef DD_DEBUG
    if (pr > 0) (void) fprintf(table->out,"zddGroupSiftingAux from %d to %d\n",xLow,xHigh);
    assert((unsigned) x >= table->subtableZ[x].next); /* x is bottom of group */
#endif

    initialSize = table->keysZ;
    moves = NULL;

    if (x == xLow) { /* Sift down */
#ifdef DD_DEBUG
        /* x must be a singleton */
        assert((unsigned) x == table->subtableZ[x].next);
#endif
        if (x == xHigh) return(1);      /* just one variable */

        if (!zddGroupSiftingDown(table,x,xHigh,&moves))
            goto zddGroupSiftingAuxOutOfMem;
        /* at this point x == xHigh, unless early term */

        /* move backward and stop at best position */
        result = zddGroupSiftingBackward(table,moves,initialSize);
#ifdef DD_DEBUG
        assert(table->keysZ <= (unsigned) initialSize);
#endif
        if (!result) goto zddGroupSiftingAuxOutOfMem;

    } else if (cuddZddNextHigh(table,x) > xHigh) { /* Sift up */
#ifdef DD_DEBUG
        /* x is bottom of group */
        assert((unsigned) x >= table->subtableZ[x].next);
#endif
        /* Find top of x's group */
        x = table->subtableZ[x].next;

        if (!zddGroupSiftingUp(table,x,xLow,&moves))
            goto zddGroupSiftingAuxOutOfMem;
        /* at this point x == xLow, unless early term */

        /* move backward and stop at best position */
        result = zddGroupSiftingBackward(table,moves,initialSize);
#ifdef DD_DEBUG
        assert(table->keysZ <= (unsigned) initialSize);
#endif
        if (!result) goto zddGroupSiftingAuxOutOfMem;

    } else if (x - xLow > xHigh - x) { /* must go down first: shorter */
        if (!zddGroupSiftingDown(table,x,xHigh,&moves))
            goto zddGroupSiftingAuxOutOfMem;
        /* at this point x == xHigh, unless early term */

        /* Find top of group */
        if (moves) {
            x = moves->y;
        }
        while ((unsigned) x < table->subtableZ[x].next)
            x = table->subtableZ[x].next;
        x = table->subtableZ[x].next;
#ifdef DD_DEBUG
        /* x should be the top of a group */
        assert((unsigned) x <= table->subtableZ[x].next);
#endif

        if (!zddGroupSiftingUp(table,x,xLow,&moves))
            goto zddGroupSiftingAuxOutOfMem;

        /* move backward and stop at best position */
        result = zddGroupSiftingBackward(table,moves,initialSize);
#ifdef DD_DEBUG
        assert(table->keysZ <= (unsigned) initialSize);
#endif
        if (!result) goto zddGroupSiftingAuxOutOfMem;

    } else { /* moving up first: shorter */
        /* Find top of x's group */
        x = table->subtableZ[x].next;

        if (!zddGroupSiftingUp(table,x,xLow,&moves))
            goto zddGroupSiftingAuxOutOfMem;
        /* at this point x == xHigh, unless early term */

        if (moves) {
            x = moves->x;
        }
        while ((unsigned) x < table->subtableZ[x].next)
            x = table->subtableZ[x].next;
#ifdef DD_DEBUG
        /* x is bottom of a group */
        assert((unsigned) x >= table->subtableZ[x].next);
#endif

        if (!zddGroupSiftingDown(table,x,xHigh,&moves))
            goto zddGroupSiftingAuxOutOfMem;

        /* move backward and stop at best position */
        result = zddGroupSiftingBackward(table,moves,initialSize);
#ifdef DD_DEBUG
        assert(table->keysZ <= (unsigned) initialSize);
#endif
        if (!result) goto zddGroupSiftingAuxOutOfMem;
    }

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

    return(1);

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

    return(0);

} /* end of zddGroupSiftingAux */

static int zddGroupSiftingBackward	(	DdManager *	table,
		Move *	moves,
		int	size
	)			[static]

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

Synopsis [Determines the best position for a variables and returns it there.]

Description [Determines the best position for a variables and returns it there. Returns 1 in case of success; 0 otherwise.]

SideEffects [None]

Definition at line 1234 of file cuddZddGroup.c.

{
    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 ((table->subtableZ[move->x].next == move->x) &&
        (table->subtableZ[move->y].next == move->y)) {
            res = cuddZddSwapInPlace(table,(int)move->x,(int)move->y);
            if (!res) return(0);
#ifdef DD_DEBUG
            if (pr > 0) (void) fprintf(table->out,"zddGroupSiftingBackward:\n");
            assert(table->subtableZ[move->x].next == move->x);
            assert(table->subtableZ[move->y].next == move->y);
#endif
        } else { /* Group move necessary */
            res = zddGroupMoveBackward(table,(int)move->x,(int)move->y);
            if (!res) return(0);
        }
    }

    return(1);

} /* end of zddGroupSiftingBackward */

static int zddGroupSiftingDown	(	DdManager *	table,
		int	x,
		int	xHigh,
		Move **	moves
	)			[static]

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

Synopsis [Sifts down a variable until it reaches position xHigh.]

Description [Sifts down a variable until it reaches position xHigh. Assumes that x is the bottom of a group (or a singleton). Records all the moves. Returns 1 in case of success; 0 otherwise.]

SideEffects [None]

Definition at line 965 of file cuddZddGroup.c.

{
    Move *move;
    int  y;
    int  size;
    int  limitSize;
    int  gxtop,gybot;
    int  xindex;


    /* Initialize R */
    xindex = table->invpermZ[x];
    gxtop = table->subtableZ[x].next;
    limitSize = size = table->keysZ;
    y = cuddZddNextHigh(table,x);
    while (y <= xHigh) {
        /* Find bottom of y group. */
        gybot = table->subtableZ[y].next;
        while (table->subtableZ[gybot].next != (unsigned) y)
            gybot = table->subtableZ[gybot].next;

        if (table->subtableZ[x].next == (unsigned) x &&
            table->subtableZ[y].next == (unsigned) y) {
            /* x and y are self groups */
            size = cuddZddSwapInPlace(table,x,y);
#ifdef DD_DEBUG
            assert(table->subtableZ[x].next == (unsigned) x);
            assert(table->subtableZ[y].next == (unsigned) y);
#endif
            if (size == 0) goto zddGroupSiftingDownOutOfMem;

            /* Record move. */
            move = (Move *) cuddDynamicAllocNode(table);
            if (move == NULL) goto zddGroupSiftingDownOutOfMem;
            move->x = x;
            move->y = y;
            move->flags = MTR_DEFAULT;
            move->size = size;
            move->next = *moves;
            *moves = move;

#ifdef DD_DEBUG
            if (pr > 0) (void) fprintf(table->out,"zddGroupSiftingDown (2 single groups):\n");
#endif
            if ((double) size > (double) limitSize * table->maxGrowth)
                return(1);
            if (size < limitSize) limitSize = size;
            x = y;
            y = cuddZddNextHigh(table,x);
        } else { /* Group move */
            size = zddGroupMove(table,x,y,moves);
            if (size == 0) goto zddGroupSiftingDownOutOfMem;
            if ((double) size > (double) limitSize * table->maxGrowth)
                return(1);
            if (size < limitSize) limitSize = size;
        }
        x = gybot;
        y = cuddZddNextHigh(table,x);
    }

    return(1);

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

    return(0);

} /* end of zddGroupSiftingDown */

static int zddGroupSiftingUp	(	DdManager *	table,
		int	y,
		int	xLow,
		Move **	moves
	)			[static]

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

Synopsis [Sifts up a variable until either it reaches position xLow or the size of the DD heap increases too much.]

Description [Sifts up a variable until either it reaches position xLow or the size of the DD heap increases too much. Assumes that y is the top of a group (or a singleton). Checks y for aggregation to the adjacent variables. Records all the moves that are appended to the list of moves received as input and returned as a side effect. Returns 1 in case of success; 0 otherwise.]

SideEffects [None]

Definition at line 884 of file cuddZddGroup.c.

{
    Move *move;
    int  x;
    int  size;
    int  gxtop;
    int  limitSize;
    int  xindex, yindex;

    yindex = table->invpermZ[y];

    limitSize = table->keysZ;

    x = cuddZddNextLow(table,y);
    while (x >= xLow) {
        gxtop = table->subtableZ[x].next;
        if (table->subtableZ[x].next == (unsigned) x &&
            table->subtableZ[y].next == (unsigned) y) {
            /* x and y are self groups */
            xindex = table->invpermZ[x];
            size = cuddZddSwapInPlace(table,x,y);
#ifdef DD_DEBUG
            assert(table->subtableZ[x].next == (unsigned) x);
            assert(table->subtableZ[y].next == (unsigned) y);
#endif
            if (size == 0) goto zddGroupSiftingUpOutOfMem;
            move = (Move *)cuddDynamicAllocNode(table);
            if (move == NULL) goto zddGroupSiftingUpOutOfMem;
            move->x = x;
            move->y = y;
            move->flags = MTR_DEFAULT;
            move->size = size;
            move->next = *moves;
            *moves = move;

#ifdef DD_DEBUG
            if (pr > 0) (void) fprintf(table->out,"zddGroupSiftingUp (2 single groups):\n");
#endif
            if ((double) size > (double) limitSize * table->maxGrowth)
                return(1);
            if (size < limitSize) limitSize = size;
        } else { /* group move */
            size = zddGroupMove(table,x,y,moves);
            if (size == 0) goto zddGroupSiftingUpOutOfMem;
            if ((double) size > (double) limitSize * table->maxGrowth)
                return(1);
            if (size < limitSize) limitSize = size;
        }
        y = gxtop;
        x = cuddZddNextLow(table,y);
    }

    return(1);

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

} /* end of zddGroupSiftingUp */

static void zddMergeGroups	(	DdManager *	table,
		MtrNode *	treenode,
		int	low,
		int	high
	)			[static]

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

Synopsis [Merges groups in the DD table.]

Description [Creates a single group from low to high and adjusts the idex field of the tree node.]

SideEffects [None]

Definition at line 1282 of file cuddZddGroup.c.

{
    int i;
    MtrNode *auxnode;
    int saveindex;
    int newindex;

    /* Merge all variables from low to high in one group, unless
    ** this is the topmost group. In such a case we do not merge lest
    ** we lose the symmetry information. */
    if (treenode != table->treeZ) {
        for (i = low; i < high; i++)
            table->subtableZ[i].next = i+1;
        table->subtableZ[high].next = low;
    }

    /* Adjust the index fields of the tree nodes. If a node is the
    ** first child of its parent, then the parent may also need adjustment. */
    saveindex = treenode->index;
    newindex = table->invpermZ[low];
    auxnode = treenode;
    do {
        auxnode->index = newindex;
        if (auxnode->parent == NULL ||
                (int) auxnode->parent->index != saveindex)
            break;
        auxnode = auxnode->parent;
    } while (1);
    return;

} /* end of zddMergeGroups */

static int zddReorderChildren	(	DdManager *	table,
		MtrNode *	treenode,
		Cudd_ReorderingType	method
	)			[static]

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

Synopsis [Reorders the children of a group tree node according to the options.]

Description [Reorders the children of a group tree node according to the options. After reordering puts all the variables in the group and/or its descendents in a single group. This allows hierarchical reordering. If the variables in the group do not exist yet, simply does nothing. Returns 1 if successful; 0 otherwise.]

SideEffects [None]

Definition at line 402 of file cuddZddGroup.c.

{
    int lower;
    int upper;
    int result;
    unsigned int initialSize;

    zddFindNodeHiLo(table,treenode,&lower,&upper);
    /* If upper == -1 these variables do not exist yet. */
    if (upper == -1)
        return(1);

    if (treenode->flags == MTR_FIXED) {
        result = 1;
    } else {
#ifdef DD_STATS
        (void) fprintf(table->out," ");
#endif
        switch (method) {
        case CUDD_REORDER_RANDOM:
        case CUDD_REORDER_RANDOM_PIVOT:
            result = cuddZddSwapping(table,lower,upper,method);
            break;
        case CUDD_REORDER_SIFT:
            result = cuddZddSifting(table,lower,upper);
            break;
        case CUDD_REORDER_SIFT_CONVERGE:
            do {
                initialSize = table->keysZ;
                result = cuddZddSifting(table,lower,upper);
                if (initialSize <= table->keysZ)
                    break;
#ifdef DD_STATS
                else
                    (void) fprintf(table->out,"\n");
#endif
            } while (result != 0);
            break;
        case CUDD_REORDER_SYMM_SIFT:
            result = cuddZddSymmSifting(table,lower,upper);
            break;
        case CUDD_REORDER_SYMM_SIFT_CONV:
            result = cuddZddSymmSiftingConv(table,lower,upper);
            break;
        case CUDD_REORDER_GROUP_SIFT:
            result = zddGroupSifting(table,lower,upper);
            break;
        case CUDD_REORDER_LINEAR:
            result = cuddZddLinearSifting(table,lower,upper);
            break;
        case CUDD_REORDER_LINEAR_CONVERGE:
            do {
                initialSize = table->keysZ;
                result = cuddZddLinearSifting(table,lower,upper);
                if (initialSize <= table->keysZ)
                    break;
#ifdef DD_STATS
                else
                    (void) fprintf(table->out,"\n");
#endif
            } while (result != 0);
            break;
        default:
            return(0);
        }
    }

    /* Create a single group for all the variables that were sifted,
    ** so that they will be treated as a single block by successive
    ** invocations of zddGroupSifting.
    */
    zddMergeGroups(table,treenode,lower,upper);

#ifdef DD_DEBUG
    if (pr > 0) (void) fprintf(table->out,"zddReorderChildren:");
#endif

    return(result);

} /* end of zddReorderChildren */

static int zddTreeSiftingAux	(	DdManager *	table,
		MtrNode *	treenode,
		Cudd_ReorderingType	method
	)			[static]

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

Synopsis [Visits the group tree and reorders each group.]

Description [Recursively visits the group tree and reorders each group in postorder fashion. Returns 1 if successful; 0 otherwise.]

SideEffects [None]

Definition at line 318 of file cuddZddGroup.c.

{
    MtrNode  *auxnode;
    int res;

#ifdef DD_DEBUG
    Mtr_PrintGroups(treenode,1);
#endif

    auxnode = treenode;
    while (auxnode != NULL) {
        if (auxnode->child != NULL) {
            if (!zddTreeSiftingAux(table, auxnode->child, method))
                return(0);
            res = zddReorderChildren(table, auxnode, CUDD_REORDER_GROUP_SIFT);
            if (res == 0)
                return(0);
        } else if (auxnode->size > 1) {
            if (!zddReorderChildren(table, auxnode, method))
                return(0);
        }
        auxnode = auxnode->younger;
    }

    return(1);

} /* end of zddTreeSiftingAux */

static int zddUniqueCompareGroup	(	int *	ptrX,
		int *	ptrY
	)			[static]

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]

Definition at line 578 of file cuddZddGroup.c.

{
#if 0
    if (entry[*ptrY] == entry[*ptrX]) {
        return((*ptrX) - (*ptrY));
    }
#endif
    return(entry[*ptrY] - entry[*ptrX]);

} /* end of zddUniqueCompareGroup */

---

Variable Documentation

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

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

FileName [cuddZddGroup.c]

PackageName [cudd]

Synopsis [Functions for ZDD group sifting.]

Description [External procedures included in this file:

• Cudd_MakeZddTreeNode()

Internal procedures included in this file:

• cuddZddTreeSifting()

Static procedures included in this module:

• zddTreeSiftingAux()
• zddCountInternalMtrNodes()
• zddReorderChildren()
• zddFindNodeHiLo()
• zddUniqueCompareGroup()
• zddGroupSifting()
• zddGroupSiftingAux()
• zddGroupSiftingUp()
• zddGroupSiftingDown()
• zddGroupMove()
• zddGroupMoveBackward()
• zddGroupSiftingBackward()
• zddMergeGroups()

]

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 63 of file cuddZddGroup.c.

int* entry [static]

Definition at line 66 of file cuddZddGroup.c.

int zddTotalNumberSwapping

Definition at line 79 of file cuddZddReord.c.