Version abc71001

1 files changed, 1317 insertions, 0 deletions

diff --git a/src/bdd/cudd/cuddZddGroup.c b/src/bdd/cudd/cuddZddGroup.c
new file mode 100644
index 00000000..621fa43f
--- /dev/null
+++ b/src/bdd/cudd/cuddZddGroup.c
@@ -0,0 +1,1317 @@
+/**CFile***********************************************************************
+
+  FileName    [cuddZddGroup.c]
+
+  PackageName [cudd]
+
+  Synopsis    [Functions for ZDD group sifting.]
+
+  Description [External procedures included in this file:
+        <ul>
+        <li> Cudd_MakeZddTreeNode()
+        </ul>
+    Internal procedures included in this file:
+        <ul>
+        <li> cuddZddTreeSifting()
+        </ul>
+    Static procedures included in this module:
+        <ul>
+        <li> zddTreeSiftingAux()
+        <li> zddCountInternalMtrNodes()
+        <li> zddReorderChildren()
+        <li> zddFindNodeHiLo()
+        <li> zddUniqueCompareGroup()
+        <li> zddGroupSifting()
+        <li> zddGroupSiftingAux()
+        <li> zddGroupSiftingUp()
+        <li> zddGroupSiftingDown()
+        <li> zddGroupMove()
+        <li> zddGroupMoveBackward()
+        <li> zddGroupSiftingBackward()
+        <li> zddMergeGroups()
+        </ul>]
+
+  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.]
+
+******************************************************************************/
+
+#include "util_hack.h"
+#include "cuddInt.h"
+
+/*---------------------------------------------------------------------------*/
+/* Constant declarations                                                     */
+/*---------------------------------------------------------------------------*/
+
+/*---------------------------------------------------------------------------*/
+/* Stucture declarations                                                     */
+/*---------------------------------------------------------------------------*/
+
+/*---------------------------------------------------------------------------*/
+/* Type declarations                                                         */
+/*---------------------------------------------------------------------------*/
+
+/*---------------------------------------------------------------------------*/
+/* Variable declarations                                                     */
+/*---------------------------------------------------------------------------*/
+
+#ifndef lint
+static char rcsid[] DD_UNUSED = "$Id: cuddZddGroup.c,v 1.1.1.1 2003/02/24 22:23:54 wjiang Exp $";
+#endif
+
+static    int    *entry;
+extern    int    zddTotalNumberSwapping;
+#ifdef DD_STATS
+static  int     extsymmcalls;
+static  int     extsymm;
+static  int     secdiffcalls;
+static  int     secdiff;
+static  int     secdiffmisfire;
+#endif
+#ifdef DD_DEBUG
+static    int    pr = 0;    /* flag to enable printing while debugging */
+            /* by depositing a 1 into it */
+#endif
+
+/*---------------------------------------------------------------------------*/
+/* Macro declarations                                                        */
+/*---------------------------------------------------------------------------*/
+
+/**AutomaticStart*************************************************************/
+
+/*---------------------------------------------------------------------------*/
+/* Static function prototypes                                                */
+/*---------------------------------------------------------------------------*/
+
+static int zddTreeSiftingAux ARGS((DdManager *table, MtrNode *treenode, Cudd_ReorderingType method));
+#ifdef DD_STATS
+static int zddCountInternalMtrNodes ARGS((DdManager *table, MtrNode *treenode));
+#endif
+static int zddReorderChildren 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));
+
+/**AutomaticEnd***************************************************************/
+
+
+/*---------------------------------------------------------------------------*/
+/* Definition of exported functions                                          */
+/*---------------------------------------------------------------------------*/
+
+
+/**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]
+
+******************************************************************************/
+MtrNode *
+Cudd_MakeZddTreeNode(
+  DdManager * dd /* manager */,
+  unsigned int  low /* index of the first group variable */,
+  unsigned int  size /* number of variables in the group */,
+  unsigned int  type /* MTR_DEFAULT or MTR_FIXED */)
+{
+    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 */
+
+
+/*---------------------------------------------------------------------------*/
+/* Definition of internal functions                                          */
+/*---------------------------------------------------------------------------*/
+
+
+/**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]
+
+******************************************************************************/
+int
+cuddZddTreeSifting(
+  DdManager * table /* DD table */,
+  Cudd_ReorderingType method /* reordering method for the groups of leaves */)
+{
+    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 */
+
+
+/*---------------------------------------------------------------------------*/
+/* Definition of static functions                                            */
+/*---------------------------------------------------------------------------*/
+
+
+/**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]
+
+******************************************************************************/
+static int
+zddTreeSiftingAux(
+  DdManager * table,
+  MtrNode * treenode,
+  Cudd_ReorderingType method)
+{
+    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 */
+
+
+#ifdef DD_STATS
+/**Function********************************************************************
+
+  Synopsis    [Counts the number of internal nodes of the group tree.]
+
+  Description [Counts the number of internal nodes of the group tree.
+  Returns the count.]
+
+  SideEffects [None]
+
+******************************************************************************/
+static int
+zddCountInternalMtrNodes(
+  DdManager * table,
+  MtrNode * treenode)
+{
+    MtrNode *auxnode;
+    int     count,nodeCount;
+
+
+    nodeCount = 0;
+    auxnode = treenode;
+    while (auxnode != NULL) {
+    if (!(MTR_TEST(auxnode,MTR_TERMINAL))) {
+        nodeCount++;
+        count = zddCountInternalMtrNodes(table,auxnode->child);
+        nodeCount += count;
+    }
+    auxnode = auxnode->younger;
+    }
+
+    return(nodeCount);
+
+} /* end of zddCountInternalMtrNodes */
+#endif
+
+
+/**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]
+
+******************************************************************************/
+static int
+zddReorderChildren(
+  DdManager * table,
+  MtrNode * treenode,
+  Cudd_ReorderingType method)
+{
+    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 */
+
+
+/**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     []
+
+******************************************************************************/
+static void
+zddFindNodeHiLo(
+  DdManager * table,
+  MtrNode * treenode,
+  int * lower,
+  int * upper)
+{
+    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 */
+
+
+/**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]
+
+******************************************************************************/
+static int
+zddUniqueCompareGroup(
+  int * ptrX,
+  int * ptrY)
+{
+#if 0
+    if (entry[*ptrY] == entry[*ptrX]) {
+    return((*ptrX) - (*ptrY));
+    }
+#endif
+    return(entry[*ptrY] - entry[*ptrX]);
+
+} /* end of zddUniqueCompareGroup */
+
+
+/**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]
+
+******************************************************************************/
+static int
+zddGroupSifting(
+  DdManager * table,
+  int  lower,
+  int  upper)
+{
+    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 */
+
+
+/**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]
+
+******************************************************************************/
+static int
+zddGroupSiftingAux(
+  DdManager * table,
+  int  x,
+  int  xLow,
+  int  xHigh)
+{
+    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 */
+
+
+/**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]
+
+******************************************************************************/
+static int
+zddGroupSiftingUp(
+  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 int
+zddGroupSiftingDown(
+  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 int
+zddGroupMove(
+  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 int
+zddGroupMoveBackward(
+  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 int
+zddGroupSiftingBackward(
+  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 void
+zddMergeGroups(
+  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 */
+