******************************************************************************/static intzddGroupSiftingUp(  DdManager * table,  int  y,  int  xLow,  Move ** moves){    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 *//**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]******************************************************************************/static intzddGroupSiftingDown(  DdManager * table,  int  x,  int  xHigh,  Move ** moves){    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 *//**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]******************************************************************************/static intzddGroupMove(  DdManager * table,  int  x,  int  y,  Move ** moves){    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 *//**Function********************************************************************  Synopsis    [Undoes the swap two groups.]  Description [Undoes the swap two groups.  Returns 1 in case of  success; 0 otherwise.]  SideEffects [None]******************************************************************************/static intzddGroupMoveBackward(  DdManager * table,  int  x,  int  y){    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 *//**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]******************************************************************************/static intzddGroupSiftingBackward(  DdManager * table,  Move * moves,  int  size){    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 *//**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]******************************************************************************/static voidzddMergeGroups(  DdManager * table,  MtrNode * treenode,  int  low,  int  high){    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 */