src/bdd/cudd/cuddGroup.c

Go to the documentation of this file.

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

/*---------------------------------------------------------------------------*/
/* Constant declarations                                                     */
/*---------------------------------------------------------------------------*/

/* Constants for lazy sifting */
#define DD_NORMAL_SIFT  0
#define DD_LAZY_SIFT    1

/* Constants for sifting up and down */
#define DD_SIFT_DOWN    0
#define DD_SIFT_UP      1

/*---------------------------------------------------------------------------*/
/* Stucture declarations                                                     */
/*---------------------------------------------------------------------------*/

/*---------------------------------------------------------------------------*/
/* Type declarations                                                         */
/*---------------------------------------------------------------------------*/

/*---------------------------------------------------------------------------*/
/* Variable declarations                                                     */
/*---------------------------------------------------------------------------*/

#ifndef lint
static char rcsid[] DD_UNUSED = "$Id: cuddGroup.c,v 1.1.1.1 2003/02/24 22:23:52 wjiang Exp $";
#endif

static  int     *entry;
extern  int     ddTotalNumberSwapping;
#ifdef DD_STATS
extern  int     ddTotalNISwaps;
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
static int originalSize;
static int originalLevel;

/*---------------------------------------------------------------------------*/
/* Macro declarations                                                        */
/*---------------------------------------------------------------------------*/

/*---------------------------------------------------------------------------*/
/* Static function prototypes                                                */
/*---------------------------------------------------------------------------*/

static int ddTreeSiftingAux ARGS((DdManager *table, MtrNode *treenode, Cudd_ReorderingType method));
#ifdef DD_STATS
static int ddCountInternalMtrNodes ARGS((DdManager *table, MtrNode *treenode));
#endif
static int ddReorderChildren ARGS((DdManager *table, MtrNode *treenode, Cudd_ReorderingType method));
static void ddFindNodeHiLo ARGS((DdManager *table, MtrNode *treenode, int *lower, int *upper));
static int ddUniqueCompareGroup ARGS((int *ptrX, int *ptrY));
static int ddGroupSifting ARGS((DdManager *table, int lower, int upper, int (*checkFunction)(DdManager *, int, int), int lazyFlag));
static void ddCreateGroup ARGS((DdManager *table, int x, int y));
static int ddGroupSiftingAux ARGS((DdManager *table, int x, int xLow, int xHigh, int (*checkFunction)(DdManager *, int, int), int lazyFlag));
static int ddGroupSiftingUp ARGS((DdManager *table, int y, int xLow, int (*checkFunction)(DdManager *, int, int), Move **moves));
static int ddGroupSiftingDown ARGS((DdManager *table, int x, int xHigh, int (*checkFunction)(DdManager *, int, int), Move **moves));
static int ddGroupMove ARGS((DdManager *table, int x, int y, Move **moves));
static int ddGroupMoveBackward ARGS((DdManager *table, int x, int y));
static int ddGroupSiftingBackward ARGS((DdManager *table, Move *moves, int size, int upFlag, int lazyFlag));
static void ddMergeGroups ARGS((DdManager *table, MtrNode *treenode, int low, int high));
static void ddDissolveGroup ARGS((DdManager *table, int x, int y));
static int ddNoCheck ARGS((DdManager *table, int x, int y));
static int ddSecDiffCheck ARGS((DdManager *table, int x, int y));
static int ddExtSymmCheck ARGS((DdManager *table, int x, int y));
static int ddVarGroupCheck ARGS((DdManager * table, int x, int y)); 
static int ddSetVarHandled ARGS((DdManager *dd, int index));
static int ddResetVarHandled ARGS((DdManager *dd, int index));
static int ddIsVarHandled ARGS((DdManager *dd, int index));

/*---------------------------------------------------------------------------*/
/* Definition of exported functions                                          */
/*---------------------------------------------------------------------------*/


MtrNode *
Cudd_MakeTreeNode(
  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->size) ? dd->perm[low] : low;

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

    /* If the tree does not exist yet, create it. */
    tree = dd->tree;
    if (tree == NULL) {
        dd->tree = tree = Mtr_InitGroupTree(0, dd->size);
        if (tree == NULL)
            return(NULL);
        tree->index = dd->invperm[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, ddMax(level + size, (unsigned) dd->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_MakeTreeNode */


/*---------------------------------------------------------------------------*/
/* Definition of internal functions                                          */
/*---------------------------------------------------------------------------*/


int
cuddTreeSifting(
  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->tree == NULL;
    if (tempTree) {
        table->tree = Mtr_InitGroupTree(0,table->size);
        table->tree->index = table->invperm[0];
    }
    nvars = table->size;

#ifdef DD_DEBUG
    if (pr > 0 && !tempTree) (void) fprintf(table->out,"cuddTreeSifting:");
    Mtr_PrintGroups(table->tree,pr <= 0);
#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",
                       ddCountInternalMtrNodes(table,table->tree));
#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->subtables[i].next = i;


    /* Reorder. */
    result = ddTreeSiftingAux(table, table->tree, 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_FreeTree(table);
    return(result);

} /* end of cuddTreeSifting */


/*---------------------------------------------------------------------------*/
/* Definition of static functions                                            */
/*---------------------------------------------------------------------------*/


static int
ddTreeSiftingAux(
  DdManager * table,
  MtrNode * treenode,
  Cudd_ReorderingType method)
{
    MtrNode  *auxnode;
    int res;
    Cudd_AggregationType saveCheck;

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

    auxnode = treenode;
    while (auxnode != NULL) {
        if (auxnode->child != NULL) {
            if (!ddTreeSiftingAux(table, auxnode->child, method))
                return(0);
            saveCheck = table->groupcheck;
            table->groupcheck = CUDD_NO_CHECK;
            if (method != CUDD_REORDER_LAZY_SIFT)
              res = ddReorderChildren(table, auxnode, CUDD_REORDER_GROUP_SIFT);
            else
              res = ddReorderChildren(table, auxnode, CUDD_REORDER_LAZY_SIFT);
            table->groupcheck = saveCheck;

            if (res == 0)
                return(0);
        } else if (auxnode->size > 1) {
            if (!ddReorderChildren(table, auxnode, method))
                return(0);
        }
        auxnode = auxnode->younger;
    }

    return(1);

} /* end of ddTreeSiftingAux */


#ifdef DD_STATS

static int
ddCountInternalMtrNodes(
  DdManager * table,
  MtrNode * treenode)
{
    MtrNode *auxnode;
    int     count,nodeCount;


    nodeCount = 0;
    auxnode = treenode;
    while (auxnode != NULL) {
        if (!(MTR_TEST(auxnode,MTR_TERMINAL))) {
            nodeCount++;
            count = ddCountInternalMtrNodes(table,auxnode->child);
            nodeCount += count;
        }
        auxnode = auxnode->younger;
    }

    return(nodeCount);

} /* end of ddCountInternalMtrNodes */
#endif


static int
ddReorderChildren(
  DdManager * table,
  MtrNode * treenode,
  Cudd_ReorderingType method)
{
    int lower;
    int upper;
    int result;
    unsigned int initialSize;

    ddFindNodeHiLo(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 = cuddSwapping(table,lower,upper,method);
            break;
        case CUDD_REORDER_SIFT:
            result = cuddSifting(table,lower,upper);
            break;
        case CUDD_REORDER_SIFT_CONVERGE:
            do {
                initialSize = table->keys - table->isolated;
                result = cuddSifting(table,lower,upper);
                if (initialSize <= table->keys - table->isolated)
                    break;
#ifdef DD_STATS
                else
                    (void) fprintf(table->out,"\n");
#endif
            } while (result != 0);
            break;
        case CUDD_REORDER_SYMM_SIFT:
            result = cuddSymmSifting(table,lower,upper);
            break;
        case CUDD_REORDER_SYMM_SIFT_CONV:
            result = cuddSymmSiftingConv(table,lower,upper);
            break;
        case CUDD_REORDER_GROUP_SIFT:
            if (table->groupcheck == CUDD_NO_CHECK) {
                result = ddGroupSifting(table,lower,upper,ddNoCheck,
                                        DD_NORMAL_SIFT);
            } else if (table->groupcheck == CUDD_GROUP_CHECK5) {
                result = ddGroupSifting(table,lower,upper,ddExtSymmCheck,
                                        DD_NORMAL_SIFT);
            } else if (table->groupcheck == CUDD_GROUP_CHECK7) {
                result = ddGroupSifting(table,lower,upper,ddExtSymmCheck,
                                        DD_NORMAL_SIFT);
            } else {
                (void) fprintf(table->err,
                               "Unknown group ckecking method\n");
                result = 0;
            }
            break;
        case CUDD_REORDER_GROUP_SIFT_CONV:
            do {
                initialSize = table->keys - table->isolated;
                if (table->groupcheck == CUDD_NO_CHECK) {
                    result = ddGroupSifting(table,lower,upper,ddNoCheck,
                                            DD_NORMAL_SIFT);
                } else if (table->groupcheck == CUDD_GROUP_CHECK5) {
                    result = ddGroupSifting(table,lower,upper,ddExtSymmCheck,
                                            DD_NORMAL_SIFT);
                } else if (table->groupcheck == CUDD_GROUP_CHECK7) {
                    result = ddGroupSifting(table,lower,upper,ddExtSymmCheck,
                                            DD_NORMAL_SIFT);
                } else {
                    (void) fprintf(table->err,
                                   "Unknown group ckecking method\n");
                    result = 0;
                }
#ifdef DD_STATS
                (void) fprintf(table->out,"\n");
#endif
                result = cuddWindowReorder(table,lower,upper,
                                           CUDD_REORDER_WINDOW4);
                if (initialSize <= table->keys - table->isolated)
                    break;
#ifdef DD_STATS
                else
                    (void) fprintf(table->out,"\n");
#endif
            } while (result != 0);
            break;
        case CUDD_REORDER_WINDOW2:
        case CUDD_REORDER_WINDOW3:
        case CUDD_REORDER_WINDOW4:
        case CUDD_REORDER_WINDOW2_CONV:
        case CUDD_REORDER_WINDOW3_CONV:
        case CUDD_REORDER_WINDOW4_CONV:
            result = cuddWindowReorder(table,lower,upper,method);
            break;
        case CUDD_REORDER_ANNEALING:
            result = cuddAnnealing(table,lower,upper);
            break;
        case CUDD_REORDER_GENETIC:
            result = cuddGa(table,lower,upper);
            break;
        case CUDD_REORDER_LINEAR:
            result = cuddLinearAndSifting(table,lower,upper);
            break;
        case CUDD_REORDER_LINEAR_CONVERGE:
            do {
                initialSize = table->keys - table->isolated;
                result = cuddLinearAndSifting(table,lower,upper);
                if (initialSize <= table->keys - table->isolated)
                    break;
#ifdef DD_STATS
                else
                    (void) fprintf(table->out,"\n");
#endif
            } while (result != 0);
            break;
        case CUDD_REORDER_EXACT:
            result = cuddExact(table,lower,upper);
            break;
        case CUDD_REORDER_LAZY_SIFT:
            result = ddGroupSifting(table,lower,upper,ddVarGroupCheck,
                                    DD_LAZY_SIFT);
            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 ddGroupSifting.
    */
    ddMergeGroups(table,treenode,lower,upper);

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

    return(result);

} /* end of ddReorderChildren */


static void
ddFindNodeHiLo(
  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->size) {
        *lower = table->size;
        *upper = -1;
        return;
    }

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

    if (high >= table->size) {
        /* 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->size - 1;
        } else {
            /* Search the subgroup that strands the table->size line.
            ** If the first group starts at 0 and goes past table->size
            ** upper will get -1, thus correctly signaling that no reordering
            ** should take place.
            */
            while (auxnode != NULL) {
                int thisLower = table->perm[auxnode->low];
                int thisUpper = thisLower + auxnode->size - 1;
                if (thisUpper >= table->size && thisLower < table->size)
                    *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 ddFindNodeHiLo */


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

} /* end of ddUniqueCompareGroup */


static int
ddGroupSifting(
  DdManager * table,
  int  lower,
  int  upper,
  int (*checkFunction)(DdManager *, int, int),
  int lazyFlag)
{
    int         *var;
    int         i,j,x,xInit;
    int         nvars;
    int         classes;
    int         result;
    int         *sifted;
    int         merged;
    int         dissolve;
#ifdef DD_STATS
    unsigned    previousSize;
#endif
    int         xindex;

    nvars = table->size;

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

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

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

    if (lazyFlag) {
        for (i = 0; i < nvars; i ++) {
            ddResetVarHandled(table, i);
        }
    }

    /* Now sift. */
    for (i = 0; i < ddMin(table->siftMaxVar,classes); i++) {
        if (ddTotalNumberSwapping >= table->siftMaxSwap)
            break;
        xindex = var[i];
        if (sifted[xindex] == 1) /* variable already sifted as part of group */
            continue;
        x = table->perm[xindex]; /* find current level of this variable */

        if (x < lower || x > upper || table->subtables[x].bindVar == 1)
            continue;
#ifdef DD_STATS
        previousSize = table->keys - table->isolated;
#endif
#ifdef DD_DEBUG
        /* x is bottom of group */
        assert((unsigned) x >= table->subtables[x].next);
#endif
        if ((unsigned) x == table->subtables[x].next) {
            dissolve = 1;
            result = ddGroupSiftingAux(table,x,lower,upper,checkFunction,
                                        lazyFlag);
        } else {
            dissolve = 0;
            result = ddGroupSiftingAux(table,x,lower,upper,ddNoCheck,lazyFlag);
        }
        if (!result) goto ddGroupSiftingOutOfMem;

        /* check for aggregation */
        merged = 0;
        if (lazyFlag == 0 && table->groupcheck == CUDD_GROUP_CHECK7) {
            x = table->perm[xindex]; /* find current level */
            if ((unsigned) x == table->subtables[x].next) { /* not part of a group */
                if (x != upper && sifted[table->invperm[x+1]] == 0 &&
                (unsigned) x+1 == table->subtables[x+1].next) {
                    if (ddSecDiffCheck(table,x,x+1)) {
                        merged =1;
                        ddCreateGroup(table,x,x+1);
                    }
                }
                if (x != lower && sifted[table->invperm[x-1]] == 0 &&
                (unsigned) x-1 == table->subtables[x-1].next) {
                    if (ddSecDiffCheck(table,x-1,x)) {
                        merged =1;
                        ddCreateGroup(table,x-1,x);
                    }
                }
            }
        }

        if (merged) { /* a group was created */
            /* move x to bottom of group */
            while ((unsigned) x < table->subtables[x].next)
                x = table->subtables[x].next;
            /* sift */
            result = ddGroupSiftingAux(table,x,lower,upper,ddNoCheck,lazyFlag);
            if (!result) goto ddGroupSiftingOutOfMem;
#ifdef DD_STATS
            if (table->keys < previousSize + table->isolated) {
                (void) fprintf(table->out,"_");
            } else if (table->keys > previousSize + table->isolated) {
                (void) fprintf(table->out,"^");
            } else {
                (void) fprintf(table->out,"*");
            }
            fflush(table->out);
        } else {
            if (table->keys < previousSize + table->isolated) {
                (void) fprintf(table->out,"-");
            } else if (table->keys > previousSize + table->isolated) {
                (void) fprintf(table->out,"+");
            } else {
                (void) fprintf(table->out,"=");
            }
            fflush(table->out);
#endif
        }

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

            /* Dissolve the group if it was created. */
            if (lazyFlag == 0 && dissolve) {
                do {
                    j = table->subtables[x].next;
                    table->subtables[x].next = x;
                    x = j;
                } while (x != xInit);
            }
        }

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

      if (lazyFlag) ddSetVarHandled(table, xindex);
    } /* for */

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

    return(1);

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

    return(0);

} /* end of ddGroupSifting */


static void
ddCreateGroup(
  DdManager * table,
  int  x,
  int  y)
{
    int  gybot;

#ifdef DD_DEBUG
    assert(y == x+1);
#endif

    /* Find bottom of second group. */
    gybot = y;
    while ((unsigned) gybot < table->subtables[gybot].next)
        gybot = table->subtables[gybot].next;

    /* Link groups. */
    table->subtables[x].next = y;
    table->subtables[gybot].next = x;

    return;

} /* ddCreateGroup */


static int
ddGroupSiftingAux(
  DdManager * table,
  int  x,
  int  xLow,
  int  xHigh,
  int (*checkFunction)(DdManager *, int, int),
  int lazyFlag)
{
    Move *move;
    Move *moves;        /* list of moves */
    int  initialSize;
    int  result;
    int  y;
    int  topbot;

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

    initialSize = table->keys - table->isolated;
    moves = NULL;

    originalSize = initialSize;         /* for lazy sifting */

    /* If we have a singleton, we check for aggregation in both
    ** directions before we sift.
    */
    if ((unsigned) x == table->subtables[x].next) {
        /* Will go down first, unless x == xHigh:
        ** Look for aggregation above x.
        */
        for (y = x; y > xLow; y--) {
            if (!checkFunction(table,y-1,y))
                break;
            topbot = table->subtables[y-1].next; /* find top of y-1's group */
            table->subtables[y-1].next = y;
            table->subtables[x].next = topbot; /* x is bottom of group so its */
                                               /* next is top of y-1's group */
            y = topbot + 1; /* add 1 for y--; new y is top of group */
        }
        /* Will go up first unless x == xlow:
        ** Look for aggregation below x.
        */
        for (y = x; y < xHigh; y++) {
            if (!checkFunction(table,y,y+1))
                break;
            /* find bottom of y+1's group */
            topbot = y + 1;
            while ((unsigned) topbot < table->subtables[topbot].next) {
                topbot = table->subtables[topbot].next;
            }
            table->subtables[topbot].next = table->subtables[y].next;
            table->subtables[y].next = y + 1;
            y = topbot - 1; /* subtract 1 for y++; new y is bottom of group */
        }
    }

    /* Now x may be in the middle of a group.
    ** Find bottom of x's group.
    */
    while ((unsigned) x < table->subtables[x].next)
        x = table->subtables[x].next;

    originalLevel = x;                  /* for lazy sifting */

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

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

        /* move backward and stop at best position */
        result = ddGroupSiftingBackward(table,moves,initialSize,
                                        DD_SIFT_DOWN,lazyFlag);
#ifdef DD_DEBUG
        assert(table->keys - table->isolated <= (unsigned) initialSize);
#endif
        if (!result) goto ddGroupSiftingAuxOutOfMem;

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

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

        /* move backward and stop at best position */
        result = ddGroupSiftingBackward(table,moves,initialSize,
                                        DD_SIFT_UP,lazyFlag);
#ifdef DD_DEBUG
        assert(table->keys - table->isolated <= (unsigned) initialSize);
#endif
        if (!result) goto ddGroupSiftingAuxOutOfMem;

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

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

        if (!ddGroupSiftingUp(table,x,xLow,checkFunction,&moves))
            goto ddGroupSiftingAuxOutOfMem;

        /* move backward and stop at best position */
        result = ddGroupSiftingBackward(table,moves,initialSize,
                                        DD_SIFT_UP,lazyFlag);
#ifdef DD_DEBUG
        assert(table->keys - table->isolated <= (unsigned) initialSize);
#endif
        if (!result) goto ddGroupSiftingAuxOutOfMem;

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

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

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

        if (!ddGroupSiftingDown(table,x,xHigh,checkFunction,&moves))
            goto ddGroupSiftingAuxOutOfMem;

        /* move backward and stop at best position */
        result = ddGroupSiftingBackward(table,moves,initialSize,
                                        DD_SIFT_DOWN,lazyFlag);
#ifdef DD_DEBUG
        assert(table->keys - table->isolated <= (unsigned) initialSize);
#endif
        if (!result) goto ddGroupSiftingAuxOutOfMem;
    }

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

    return(1);

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

    return(0);

} /* end of ddGroupSiftingAux */


static int
ddGroupSiftingUp(
  DdManager * table,
  int  y,
  int  xLow,
  int (*checkFunction)(DdManager *, int, int),
  Move ** moves)
{
    Move *move;
    int  x;
    int  size;
    int  i;
    int  gxtop,gybot;
    int  limitSize;
    int  xindex, yindex;
    int  zindex;
    int  z;
    int  isolated;
    int  L;     /* lower bound on DD size */
#ifdef DD_DEBUG
    int  checkL;
#endif

    yindex = table->invperm[y];

    /* Initialize the lower bound.
    ** The part of the DD below the bottom of y's group will not change.
    ** The part of the DD above y that does not interact with any
    ** variable of y's group will not change.
    ** The rest may vanish in the best case, except for
    ** the nodes at level xLow, which will not vanish, regardless.
    ** What we use here is not really a lower bound, because we ignore
    ** the interactions with all variables except y.
    */
    limitSize = L = table->keys - table->isolated;
    gybot = y;
    while ((unsigned) gybot < table->subtables[gybot].next)
        gybot = table->subtables[gybot].next;
    for (z = xLow + 1; z <= gybot; z++) {
        zindex = table->invperm[z];
        if (zindex == yindex || cuddTestInteract(table,zindex,yindex)) {
            isolated = table->vars[zindex]->ref == 1;
            L -= table->subtables[z].keys - isolated;
        }
    }

    originalLevel = y;                  /* for lazy sifting */

    x = cuddNextLow(table,y);
    while (x >= xLow && L <= limitSize) {
#ifdef DD_DEBUG
        gybot = y;
        while ((unsigned) gybot < table->subtables[gybot].next)
            gybot = table->subtables[gybot].next;
        checkL = table->keys - table->isolated;
        for (z = xLow + 1; z <= gybot; z++) {
            zindex = table->invperm[z];
            if (zindex == yindex || cuddTestInteract(table,zindex,yindex)) {
                isolated = table->vars[zindex]->ref == 1;
                checkL -= table->subtables[z].keys - isolated;
            }
        }
        if (pr > 0 && L != checkL) {
            (void) fprintf(table->out,
                           "Inaccurate lower bound: L = %d checkL = %d\n",
                           L, checkL);
        }
#endif
        gxtop = table->subtables[x].next;
        if (checkFunction(table,x,y)) {
            /* Group found, attach groups */
            table->subtables[x].next = y;
            i = table->subtables[y].next;
            while (table->subtables[i].next != (unsigned) y)
                i = table->subtables[i].next;
            table->subtables[i].next = gxtop;
            move = (Move *)cuddDynamicAllocNode(table);
            if (move == NULL) goto ddGroupSiftingUpOutOfMem;
            move->x = x;
            move->y = y;
            move->flags = MTR_NEWNODE;
            move->size = table->keys - table->isolated;
            move->next = *moves;
            *moves = move;
        } else if (table->subtables[x].next == (unsigned) x &&
                   table->subtables[y].next == (unsigned) y) {
            /* x and y are self groups */
            xindex = table->invperm[x];
            size = cuddSwapInPlace(table,x,y);
#ifdef DD_DEBUG
            assert(table->subtables[x].next == (unsigned) x);
            assert(table->subtables[y].next == (unsigned) y);
#endif
            if (size == 0) goto ddGroupSiftingUpOutOfMem;
            /* Update the lower bound. */
            if (cuddTestInteract(table,xindex,yindex)) {
                isolated = table->vars[xindex]->ref == 1;
                L += table->subtables[y].keys - isolated;
            }
            move = (Move *)cuddDynamicAllocNode(table);
            if (move == NULL) goto ddGroupSiftingUpOutOfMem;
            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,
                                       "ddGroupSiftingUp (2 single groups):\n");
#endif
            if ((double) size > (double) limitSize * table->maxGrowth)
                return(1);
            if (size < limitSize) limitSize = size;
        } else { /* Group move */
            size = ddGroupMove(table,x,y,moves);
            if (size == 0) goto ddGroupSiftingUpOutOfMem;
            /* Update the lower bound. */
            z = (*moves)->y;
            do {
                zindex = table->invperm[z];
                if (cuddTestInteract(table,zindex,yindex)) {
                    isolated = table->vars[zindex]->ref == 1;
                    L += table->subtables[z].keys - isolated;
                }
                z = table->subtables[z].next;
            } while (z != (int) (*moves)->y);
            if ((double) size > (double) limitSize * table->maxGrowth)
                return(1);
            if (size < limitSize) limitSize = size;
        }
        y = gxtop;
        x = cuddNextLow(table,y);
    }

    return(1);

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

} /* end of ddGroupSiftingUp */


static int
ddGroupSiftingDown(
  DdManager * table,
  int  x,
  int  xHigh,
  int (*checkFunction)(DdManager *, int, int),
  Move ** moves)
{
    Move *move;
    int  y;
    int  size;
    int  limitSize;
    int  gxtop,gybot;
    int  R;     /* upper bound on node decrease */
    int  xindex, yindex;
    int  isolated, allVars;
    int  z;
    int  zindex;
#ifdef DD_DEBUG
    int  checkR;
#endif

    /* If the group consists of simple variables, there is no point in
    ** sifting it down. This check is redundant if the projection functions
    ** do not have external references, because the computation of the
    ** lower bound takes care of the problem.  It is necessary otherwise to
    ** prevent the sifting down of simple variables. */
    y = x;
    allVars = 1;
    do {
        if (table->subtables[y].keys != 1) {
            allVars = 0;
            break;
        }
        y = table->subtables[y].next;
    } while (table->subtables[y].next != (unsigned) x);
    if (allVars)
        return(1);
    
    /* Initialize R. */
    xindex = table->invperm[x];
    gxtop = table->subtables[x].next;
    limitSize = size = table->keys - table->isolated;
    R = 0;
    for (z = xHigh; z > gxtop; z--) {
        zindex = table->invperm[z];
        if (zindex == xindex || cuddTestInteract(table,xindex,zindex)) {
            isolated = table->vars[zindex]->ref == 1;
            R += table->subtables[z].keys - isolated;
        }
    }

    originalLevel = x;                  /* for lazy sifting */

    y = cuddNextHigh(table,x);
    while (y <= xHigh && size - R < limitSize) {
#ifdef DD_DEBUG
        gxtop = table->subtables[x].next;
        checkR = 0;
        for (z = xHigh; z > gxtop; z--) {
            zindex = table->invperm[z];
            if (zindex == xindex || cuddTestInteract(table,xindex,zindex)) {
                isolated = table->vars[zindex]->ref == 1;
                checkR += table->subtables[z].keys - isolated;
            }
        }
        assert(R >= checkR);
#endif
        /* Find bottom of y group. */
        gybot = table->subtables[y].next;
        while (table->subtables[gybot].next != (unsigned) y)
            gybot = table->subtables[gybot].next;

        if (checkFunction(table,x,y)) {
            /* Group found: attach groups and record move. */
            gxtop = table->subtables[x].next;
            table->subtables[x].next = y;
            table->subtables[gybot].next = gxtop;
            move = (Move *)cuddDynamicAllocNode(table);
            if (move == NULL) goto ddGroupSiftingDownOutOfMem;
            move->x = x;
            move->y = y;
            move->flags = MTR_NEWNODE;
            move->size = table->keys - table->isolated;
            move->next = *moves;
            *moves = move;
        } else if (table->subtables[x].next == (unsigned) x &&
                   table->subtables[y].next == (unsigned) y) {
            /* x and y are self groups */
            /* Update upper bound on node decrease. */
            yindex = table->invperm[y];
            if (cuddTestInteract(table,xindex,yindex)) {
                isolated = table->vars[yindex]->ref == 1;
                R -= table->subtables[y].keys - isolated;
            }
            size = cuddSwapInPlace(table,x,y);
#ifdef DD_DEBUG
            assert(table->subtables[x].next == (unsigned) x);
            assert(table->subtables[y].next == (unsigned) y);
#endif
            if (size == 0) goto ddGroupSiftingDownOutOfMem;

            /* Record move. */
            move = (Move *) cuddDynamicAllocNode(table);
            if (move == NULL) goto ddGroupSiftingDownOutOfMem;
            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,
                                       "ddGroupSiftingDown (2 single groups):\n");
#endif
            if ((double) size > (double) limitSize * table->maxGrowth)
                return(1);
            if (size < limitSize) limitSize = size;

            x = y;
            y = cuddNextHigh(table,x);
        } else { /* Group move */
            /* Update upper bound on node decrease: first phase. */
            gxtop = table->subtables[x].next;
            z = gxtop + 1;
            do {
                zindex = table->invperm[z];
                if (zindex == xindex || cuddTestInteract(table,xindex,zindex)) {
                    isolated = table->vars[zindex]->ref == 1;
                    R -= table->subtables[z].keys - isolated;
                }
                z++;
            } while (z <= gybot);
            size = ddGroupMove(table,x,y,moves);
            if (size == 0) goto ddGroupSiftingDownOutOfMem;
            if ((double) size > (double) limitSize * table->maxGrowth)
                return(1);
            if (size < limitSize) limitSize = size;

            /* Update upper bound on node decrease: second phase. */
            gxtop = table->subtables[gybot].next;
            for (z = gxtop + 1; z <= gybot; z++) {
                zindex = table->invperm[z];
                if (zindex == xindex || cuddTestInteract(table,xindex,zindex)) {
                    isolated = table->vars[zindex]->ref == 1;
                    R += table->subtables[z].keys - isolated;
                }
            }
        }
        x = gybot;
        y = cuddNextHigh(table,x);
    }

    return(1);

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

    return(0);

} /* end of ddGroupSiftingDown */


static int
ddGroupMove(
  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->subtables[x].next;
    xsize = xbot - xtop + 1;
    ybot = y;
    while ((unsigned) ybot < table->subtables[ybot].next)
        ybot = table->subtables[ybot].next;
    ytop = y;
    ysize = ybot - ytop + 1;

#if defined(DD_DEBUG) && defined(DD_VERBOSE)
    initialSize = bestSize = table->keys - table->isolated;
#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 = cuddSwapInPlace(table,x,y);
            if (size == 0) goto ddGroupMoveOutOfMem;
#if defined(DD_DEBUG) && defined(DD_VERBOSE)
            if (size < bestSize)
                bestSize = size;
#endif
            swapx = x; swapy = y;
            y = x;
            x = cuddNextLow(table,y);
        }
        y = ytop + i;
        x = cuddNextLow(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->subtables[y].next = cuddNextHigh(table,y);
        y = cuddNextHigh(table,y);
    }
    table->subtables[y].next = xtop; /* y is bottom of its group, join */
                                    /* it to top of its group */
    x = cuddNextHigh(table,y);
    newxtop = x;
    for (i = 0; i < xsize - 1; i++) {
        table->subtables[x].next = cuddNextHigh(table,x);
        x = cuddNextHigh(table,x);
    }
    table->subtables[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,"ddGroupMove:\n");
#endif

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

    return(table->keys - table->isolated);

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

} /* end of ddGroupMove */


static int
ddGroupMoveBackward(
  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->subtables[x].next;
    xsize = xbot - xtop + 1;
    ybot = y;
    while ((unsigned) ybot < table->subtables[ybot].next)
        ybot = table->subtables[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 = cuddSwapInPlace(table,x,y);
            if (size == 0)
                return(0);
            y = x;
            x = cuddNextLow(table,y);
        }
        y = ytop + i;
        x = cuddNextLow(table,y);
    }

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

    return(1);

} /* end of ddGroupMoveBackward */


static int
ddGroupSiftingBackward(
  DdManager * table,
  Move * moves,
  int  size,
  int  upFlag, 
  int  lazyFlag)
{
    Move *move;
    int  res;
    Move *end_move;
    int diff, tmp_diff;
    int index, pairlev;

    if (lazyFlag) {
        end_move = NULL;

        /* Find the minimum size, and the earliest position at which it
        ** was achieved. */
        for (move = moves; move != NULL; move = move->next) {
            if (move->size < size) {
                size = move->size;
                end_move = move;
            } else if (move->size == size) {
                if (end_move == NULL) end_move = move;
            } 
        }

        /* Find among the moves that give minimum size the one that
        ** minimizes the distance from the corresponding variable. */
        if (moves != NULL) {
            diff = Cudd_ReadSize(table) + 1;
            index = (upFlag == 1) ? 
                    table->invperm[moves->x] : table->invperm[moves->y];
            pairlev = table->perm[Cudd_bddReadPairIndex(table, index)];

            for (move = moves; move != NULL; move = move->next) {
                if (move->size == size) {
                    if (upFlag == 1) {
                        tmp_diff = (move->x > pairlev) ? 
                                    move->x - pairlev : pairlev - move->x;
                    } else {
                        tmp_diff = (move->y > pairlev) ?
                                    move->y - pairlev : pairlev - move->y;
                    }
                    if (tmp_diff < diff) {
                        diff = tmp_diff;
                        end_move = move;
                    } 
                }
            }
        }
    } else {
        /* Find the minimum size. */
        for (move = moves; move != NULL; move = move->next) {
            if (move->size < size) {
                size = move->size;
            } 
        }
    }

    /* In case of lazy sifting, end_move identifies the position at
    ** which we want to stop.  Otherwise, we stop as soon as we meet
    ** the minimum size. */
    for (move = moves; move != NULL; move = move->next) {
        if (lazyFlag) {
            if (move == end_move) return(1);
        } else {
            if (move->size == size) return(1);
        }
        if ((table->subtables[move->x].next == move->x) &&
        (table->subtables[move->y].next == move->y)) {
            res = cuddSwapInPlace(table,(int)move->x,(int)move->y);
            if (!res) return(0);
#ifdef DD_DEBUG
            if (pr > 0) (void) fprintf(table->out,"ddGroupSiftingBackward:\n");
            assert(table->subtables[move->x].next == move->x);
            assert(table->subtables[move->y].next == move->y);
#endif
        } else { /* Group move necessary */
            if (move->flags == MTR_NEWNODE) {
                ddDissolveGroup(table,(int)move->x,(int)move->y);
            } else {
                res = ddGroupMoveBackward(table,(int)move->x,(int)move->y);
                if (!res) return(0);
            }
        }

    }

    return(1);

} /* end of ddGroupSiftingBackward */


static void
ddMergeGroups(
  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->tree) {
        for (i = low; i < high; i++)
            table->subtables[i].next = i+1;
        table->subtables[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->invperm[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 ddMergeGroups */


static void
ddDissolveGroup(
  DdManager * table,
  int  x,
  int  y)
{
    int topx;
    int boty;

    /* find top and bottom of the two groups */
    boty = y;
    while ((unsigned) boty < table->subtables[boty].next)
        boty = table->subtables[boty].next;
    
    topx = table->subtables[boty].next;

    table->subtables[boty].next = y;
    table->subtables[x].next = topx;

    return;

} /* end of ddDissolveGroup */


static int
ddNoCheck(
  DdManager * table,
  int  x,
  int  y)
{
    return(0);

} /* end of ddNoCheck */


static int
ddSecDiffCheck(
  DdManager * table,
  int  x,
  int  y)
{
    double Nx,Nx_1;
    double Sx;
    double threshold;
    int    xindex,yindex;

    if (x==0) return(0);

#ifdef DD_STATS
    secdiffcalls++;
#endif
    Nx = (double) table->subtables[x].keys;
    Nx_1 = (double) table->subtables[x-1].keys;
    Sx = (table->subtables[y].keys/Nx) - (Nx/Nx_1);

    threshold = table->recomb / 100.0;
    if (Sx < threshold) {
        xindex = table->invperm[x];
        yindex = table->invperm[y];
        if (cuddTestInteract(table,xindex,yindex)) {
#if defined(DD_DEBUG) && defined(DD_VERBOSE)
            (void) fprintf(table->out,
                           "Second difference for %d = %g Pos(%d)\n",
                           table->invperm[x],Sx,x);
#endif
#ifdef DD_STATS
            secdiff++;
#endif
            return(1);
        } else {
#ifdef DD_STATS
            secdiffmisfire++;
#endif
            return(0);
        }

    }
    return(0);

} /* end of ddSecDiffCheck */


static int
ddExtSymmCheck(
  DdManager * table,
  int  x,
  int  y)
{
    DdNode *f,*f0,*f1,*f01,*f00,*f11,*f10;
    DdNode *one;
    int comple;         /* f0 is complemented */
    int notproj;        /* f is not a projection function */
    int arccount;       /* number of arcs from layer x to layer y */
    int TotalRefCount;  /* total reference count of layer y minus 1 */
    int counter;        /* number of nodes of layer x that are allowed */
                        /* to violate extended symmetry conditions */
    int arccounter;     /* number of arcs into layer y that are allowed */
                        /* to come from layers other than x */
    int i;
    int xindex;
    int yindex;
    int res;
    int slots;
    DdNodePtr *list;
    DdNode *sentinel = &(table->sentinel);

    xindex = table->invperm[x];
    yindex = table->invperm[y];

    /* If the two variables do not interact, we do not want to merge them. */
    if (!cuddTestInteract(table,xindex,yindex))
        return(0);

#ifdef DD_DEBUG
    /* Checks that x and y do not contain just the projection functions.
    ** With the test on interaction, these test become redundant,
    ** because an isolated projection function does not interact with
    ** any other variable.
    */
    if (table->subtables[x].keys == 1) {
        assert(table->vars[xindex]->ref != 1);
    }
    if (table->subtables[y].keys == 1) {
        assert(table->vars[yindex]->ref != 1);
    }
#endif

#ifdef DD_STATS
    extsymmcalls++;
#endif

    arccount = 0;
    counter = (int) (table->subtables[x].keys *
              (table->symmviolation/100.0) + 0.5);
    one = DD_ONE(table);

    slots = table->subtables[x].slots;
    list = table->subtables[x].nodelist;
    for (i = 0; i < slots; i++) {
        f = list[i];
        while (f != sentinel) {
            /* Find f1, f0, f11, f10, f01, f00. */
            f1 = cuddT(f);
            f0 = Cudd_Regular(cuddE(f));
            comple = Cudd_IsComplement(cuddE(f));
            notproj = f1 != one || f0 != one || f->ref != (DdHalfWord) 1;
            if (f1->index == yindex) {
                arccount++;
                f11 = cuddT(f1); f10 = cuddE(f1);
            } else {
                if ((int) f0->index != yindex) {
                    /* If f is an isolated projection function it is
                    ** allowed to bypass layer y.
                    */
                    if (notproj) {
                        if (counter == 0)
                            return(0);
                        counter--; /* f bypasses layer y */
                    }
                }
                f11 = f10 = f1;
            }
            if ((int) f0->index == yindex) {
                arccount++;
                f01 = cuddT(f0); f00 = cuddE(f0);
            } else {
                f01 = f00 = f0;
            }
            if (comple) {
                f01 = Cudd_Not(f01);
                f00 = Cudd_Not(f00);
            }

            /* Unless we are looking at a projection function
            ** without external references except the one from the
            ** table, we insist that f01 == f10 or f11 == f00
            */
            if (notproj) {
                if (f01 != f10 && f11 != f00) {
                    if (counter == 0)
                        return(0);
                    counter--;
                }
            }

            f = f->next;
        } /* while */
    } /* for */

    /* Calculate the total reference counts of y */
    TotalRefCount = -1; /* -1 for projection function */
    slots = table->subtables[y].slots;
    list = table->subtables[y].nodelist;
    for (i = 0; i < slots; i++) {
        f = list[i];
        while (f != sentinel) {
            TotalRefCount += f->ref;
            f = f->next;
        }
    }

    arccounter = (int) (table->subtables[y].keys *
                 (table->arcviolation/100.0) + 0.5);
    res = arccount >= TotalRefCount - arccounter;

#if defined(DD_DEBUG) && defined(DD_VERBOSE)
    if (res) {
        (void) fprintf(table->out,
                       "Found extended symmetry! x = %d\ty = %d\tPos(%d,%d)\n",
                       xindex,yindex,x,y);
    }
#endif

#ifdef DD_STATS
    if (res)
        extsymm++;
#endif
    return(res);

} /* end ddExtSymmCheck */


static int
ddVarGroupCheck(
  DdManager * table,
  int x,
  int y)
{
    int xindex = table->invperm[x];
    int yindex = table->invperm[y];

    if (Cudd_bddIsVarToBeUngrouped(table, xindex)) return(0);

    if (Cudd_bddReadPairIndex(table, xindex) == yindex) {
        if (ddIsVarHandled(table, xindex) ||
            ddIsVarHandled(table, yindex)) {
            if (Cudd_bddIsVarToBeGrouped(table, xindex) ||
                Cudd_bddIsVarToBeGrouped(table, yindex) ) {
                if (table->keys - table->isolated <= originalSize) {
                    return(1);
                }
            }
        }
    }

    return(0);

} /* end of ddVarGroupCheck */


static int
ddSetVarHandled(
  DdManager *dd,
  int index)
{
    if (index >= dd->size || index < 0) return(0);
    dd->subtables[dd->perm[index]].varHandled = 1;
    return(1);

} /* end of ddSetVarHandled */


static int
ddResetVarHandled(
  DdManager *dd,
  int index)
{
    if (index >= dd->size || index < 0) return(0);
    dd->subtables[dd->perm[index]].varHandled = 0;
    return(1);

} /* end of ddResetVarHandled */


static int
ddIsVarHandled(
  DdManager *dd,
  int index)
{
    if (index >= dd->size || index < 0) return(-1);
    return dd->subtables[dd->perm[index]].varHandled;

} /* end of ddIsVarHandled */

---