#include "misc/util/util_hack.h"
#include "cuddInt.h"

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

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

int	cuddZddTreeSifting (DdManager *table, Cudd_ReorderingType method)

Variables
static ABC_NAMESPACE_IMPL_START char rcsid[]	DD_UNUSED = "$Id: cuddZddGroup.c,v 1.20 2009/02/19 16:25:36 fabio Exp $"

static int *	entry

int	zddTotalNumberSwapping

Function Documentation

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 163 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 232 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 534 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 1078 of file cuddZddGroup.c.

 {
     Move *move;
     int  size;
     int  i,j,xtop,xbot,xsize,ytop,ybot,ysize,newxtop;
     int  swapx=-1,swapy=-1;
 #if defined(DD_DEBUG) && defined(DD_VERBOSE)
     int  initialSize,bestSize;
 #endif
 
 #ifdef 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;
         cuddDeallocMove(table, *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 1184 of file cuddZddGroup.c.

 {
     int size;
     int i,j,xtop,xbot,xsize,ytop,ybot,ysize,newxtop;
 
 
 #ifdef 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 637 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 = ABC_ALLOC(int,nvars);
     if (var == NULL) {
         table->errorCode = CUDD_MEMORY_OUT;
         goto zddGroupSiftingOutOfMem;
     }
     entry = ABC_ALLOC(int,nvars);
     if (entry == NULL) {
         table->errorCode = CUDD_MEMORY_OUT;
         goto zddGroupSiftingOutOfMem;
     }
     sifted = ABC_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),(DD_QSFP)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 */
 
     ABC_FREE(sifted);
     ABC_FREE(var);
     ABC_FREE(entry);
 
     return(1);
 
 zddGroupSiftingOutOfMem:
     if (entry != NULL)  ABC_FREE(entry);
     if (var != NULL)    ABC_FREE(var);
     if (sifted != NULL) ABC_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 766 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;
         cuddDeallocMove(table, moves);
         moves = move;
     }
 
     return(1);
 
 zddGroupSiftingAuxOutOfMem:
     while (moves != NULL) {
         move = moves->next;
         cuddDeallocMove(table, 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 1258 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 992 of file cuddZddGroup.c.

 {
     Move *move;
     int  y;
     int  size;
     int  limitSize;
     int  gybot;
 
 
     /* Initialize R */
     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;
         cuddDeallocMove(table, *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 915 of file cuddZddGroup.c.

 {
     Move *move;
     int  x;
     int  size;
     int  gxtop;
     int  limitSize;
 
     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 */
             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;
         cuddDeallocMove(table, *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 1306 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 433 of file cuddZddGroup.c.

 {
     int lower;
     int upper = -1;
     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

AutomaticStart

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 349 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 609 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

ABC_NAMESPACE_IMPL_START char rcsid [] DD_UNUSED = "$Id: cuddZddGroup.c,v 1.20 2009/02/19 16:25:36 fabio 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:

]

Author [Fabio Somenzi]

Redistribution and use in source and binary forms, with or without modification, are permitted provided that the following conditions are met:

Redistributions of source code must retain the above copyright notice, this list of conditions and the following disclaimer.

Redistributions in binary form must reproduce the above copyright notice, this list of conditions and the following disclaimer in the documentation and/or other materials provided with the distribution.

Neither the name of the University of Colorado nor the names of its contributors may be used to endorse or promote products derived from this software without specific prior written permission.

THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT OWNER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.]

Definition at line 94 of file cuddZddGroup.c.

int* entry

static

Definition at line 97 of file cuddZddGroup.c.

int zddTotalNumberSwapping

Definition at line 110 of file cuddZddReord.c.

Functions

Variables

Function Documentation

Variable Documentation