cuddSymmetry.c

Go to the documentation of this file.

#include "CUDD/util.h"
#include "CUDD/cuddInt.h"

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

#define MV_OOM (Move *)1

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

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

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

#ifndef lint
static char rcsid[] DD_UNUSED = "$Id: cuddSymmetry.c,v 1.28 2012/02/05 01:07:19 fabio Exp $";
#endif

static  int *entry;

extern  int ddTotalNumberSwapping;
#ifdef DD_STATS
extern  int ddTotalNISwaps;
#endif

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

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

static int ddSymmUniqueCompare (int *ptrX, int *ptrY);
static int ddSymmSiftingAux (DdManager *table, int x, int xLow, int xHigh);
static int ddSymmSiftingConvAux (DdManager *table, int x, int xLow, int xHigh);
static Move * ddSymmSiftingUp (DdManager *table, int y, int xLow);
static Move * ddSymmSiftingDown (DdManager *table, int x, int xHigh);
static int ddSymmGroupMove (DdManager *table, int x, int y, Move **moves);
static int ddSymmGroupMoveBackward (DdManager *table, int x, int y);
static int ddSymmSiftingBackward (DdManager *table, Move *moves, int size);
static void ddSymmSummary (DdManager *table, int lower, int upper, int *symvars, int *symgroups);

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


void
Cudd_SymmProfile(
  DdManager * table,
  int  lower,
  int  upper)
{
    int i,x,gbot;
    int TotalSymm = 0;
    int TotalSymmGroups = 0;

    for (i = lower; i <= upper; i++) {
    if (table->subtables[i].next != (unsigned) i) {
        x = i;
        (void) fprintf(table->out,"Group:");
        do {
        (void) fprintf(table->out,"  %d",table->invperm[x]);
        TotalSymm++;
        gbot = x;
        x = table->subtables[x].next;
        } while (x != i);
        TotalSymmGroups++;
#ifdef DD_DEBUG
        assert(table->subtables[gbot].next == (unsigned) i);
#endif
        i = gbot;
        (void) fprintf(table->out,"\n");
    }
    }
    (void) fprintf(table->out,"Total Symmetric = %d\n",TotalSymm);
    (void) fprintf(table->out,"Total Groups = %d\n",TotalSymmGroups);

} /* end of Cudd_SymmProfile */


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


int
cuddSymmCheck(
  DdManager * table,
  int  x,
  int  y)
{
    DdNode *f,*f0,*f1,*f01,*f00,*f11,*f10;
    int comple;     /* f0 is complemented */
    int xsymmy;     /* x and y may be positively symmetric */
    int xsymmyp;    /* x and y may be negatively symmetric */
    int arccount;   /* number of arcs from layer x to layer y */
    int TotalRefCount;  /* total reference count of layer y minus 1 */
    int yindex;
    int i;
    DdNodePtr *list;
    int slots;
    DdNode *sentinel = &(table->sentinel);
#ifdef DD_DEBUG
    int xindex;
#endif

    /* Checks that x and y are not the projection functions.
    ** For x it is sufficient to check whether there is only one
    ** node; indeed, if there is one node, it is the projection function
    ** and it cannot point to y. Hence, if y isn't just the projection
    ** function, it has one arc coming from a layer different from x.
    */
    if (table->subtables[x].keys == 1) {
    return(0);
    }
    yindex = table->invperm[y];
    if (table->subtables[y].keys == 1) {
    if (table->vars[yindex]->ref == 1)
        return(0);
    }

    xsymmy = xsymmyp = 1;
    arccount = 0;
    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));
        if ((int) 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 (f1 != DD_ONE(table) || f0 != DD_ONE(table) || f->ref != 1)
            return(0); /* 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);
        }

        if (f1 != DD_ONE(table) || f0 != DD_ONE(table) || f->ref != 1) {
        xsymmy &= f01 == f10;
        xsymmyp &= f11 == f00;
        if ((xsymmy == 0) && (xsymmyp == 0))
            return(0);
        }

        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;
    }
    }

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

    return(arccount == TotalRefCount);

} /* end of cuddSymmCheck */


int
cuddSymmSifting(
  DdManager * table,
  int  lower,
  int  upper)
{
    int     i;
    int     *var;
    int     size;
    int     x;
    int     result;
    int     symvars;
    int     symgroups;
#ifdef DD_STATS
    int     previousSize;
#endif

    size = table->size;

    /* Find order in which to sift variables. */
    var = NULL;
    entry = ALLOC(int,size);
    if (entry == NULL) {
    table->errorCode = CUDD_MEMORY_OUT;
    goto ddSymmSiftingOutOfMem;
    }
    var = ALLOC(int,size);
    if (var == NULL) {
    table->errorCode = CUDD_MEMORY_OUT;
    goto ddSymmSiftingOutOfMem;
    }

    for (i = 0; i < size; i++) {
    x = table->perm[i];
    entry[i] = table->subtables[x].keys;
    var[i] = i;
    }

    qsort((void *)var,size,sizeof(int),(DD_QSFP)ddSymmUniqueCompare);

    /* Initialize the symmetry of each subtable to itself. */
    for (i = lower; i <= upper; i++) {
    table->subtables[i].next = i;
    }

    for (i = 0; i < ddMin(table->siftMaxVar,size); i++) {
    if (ddTotalNumberSwapping >= table->siftMaxSwap)
        break;
        if (util_cpu_time() - table->startTime > table->timeLimit) {
            table->autoDyn = 0; /* prevent further reordering */
            break;
        }
    x = table->perm[var[i]];
#ifdef DD_STATS
    previousSize = table->keys - table->isolated;
#endif
    if (x < lower || x > upper) continue;
    if (table->subtables[x].next == (unsigned) x) {
        result = ddSymmSiftingAux(table,x,lower,upper);
        if (!result) goto ddSymmSiftingOutOfMem;
#ifdef DD_STATS
        if (table->keys < (unsigned) previousSize + table->isolated) {
        (void) fprintf(table->out,"-");
        } else if (table->keys > (unsigned) previousSize +
               table->isolated) {
        (void) fprintf(table->out,"+"); /* should never happen */
        } else {
        (void) fprintf(table->out,"=");
        }
        fflush(table->out);
#endif
    }
    }

    FREE(var);
    FREE(entry);

    ddSymmSummary(table, lower, upper, &symvars, &symgroups);

#ifdef DD_STATS
    (void) fprintf(table->out, "\n#:S_SIFTING %8d: symmetric variables\n",
           symvars);
    (void) fprintf(table->out, "#:G_SIFTING %8d: symmetric groups",
           symgroups);
#endif

    return(1+symvars);

ddSymmSiftingOutOfMem:

    if (entry != NULL) FREE(entry);
    if (var != NULL) FREE(var);

    return(0);

} /* end of cuddSymmSifting */


int
cuddSymmSiftingConv(
  DdManager * table,
  int  lower,
  int  upper)
{
    int     i;
    int     *var;
    int     size;
    int     x;
    int     result;
    int     symvars;
    int     symgroups;
    int     classes;
    int     initialSize;
#ifdef DD_STATS
    int     previousSize;
#endif

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

    size = table->size;

    /* Find order in which to sift variables. */
    var = NULL;
    entry = ALLOC(int,size);
    if (entry == NULL) {
    table->errorCode = CUDD_MEMORY_OUT;
    goto ddSymmSiftingConvOutOfMem;
    }
    var = ALLOC(int,size);
    if (var == NULL) {
    table->errorCode = CUDD_MEMORY_OUT;
    goto ddSymmSiftingConvOutOfMem;
    }

    for (i = 0; i < size; i++) {
    x = table->perm[i];
    entry[i] = table->subtables[x].keys;
    var[i] = i;
    }

    qsort((void *)var,size,sizeof(int),(DD_QSFP)ddSymmUniqueCompare);

    /* Initialize the symmetry of each subtable to itself
    ** for first pass of converging symmetric sifting.
    */
    for (i = lower; i <= upper; i++) {
    table->subtables[i].next = i;
    }

    for (i = 0; i < ddMin(table->siftMaxVar, table->size); i++) {
    if (ddTotalNumberSwapping >= table->siftMaxSwap)
        break;
        if (util_cpu_time() - table->startTime > table->timeLimit) {
            table->autoDyn = 0; /* prevent further reordering */
            break;
        }
    x = table->perm[var[i]];
    if (x < lower || x > upper) continue;
    /* Only sift if not in symmetry group already. */
    if (table->subtables[x].next == (unsigned) x) {
#ifdef DD_STATS
        previousSize = table->keys - table->isolated;
#endif
        result = ddSymmSiftingAux(table,x,lower,upper);
        if (!result) goto ddSymmSiftingConvOutOfMem;
#ifdef DD_STATS
        if (table->keys < (unsigned) previousSize + table->isolated) {
        (void) fprintf(table->out,"-");
        } else if (table->keys > (unsigned) previousSize +
               table->isolated) {
        (void) fprintf(table->out,"+");
        } else {
        (void) fprintf(table->out,"=");
        }
        fflush(table->out);
#endif
    }
    }

    /* Sifting now until convergence. */
    while ((unsigned) initialSize > table->keys - table->isolated) {
    initialSize = table->keys - table->isolated;
#ifdef DD_STATS
    (void) fprintf(table->out,"\n");
#endif
    /* Here we consider only one representative for each symmetry class. */
    for (x = lower, classes = 0; x <= upper; x++, classes++) {
        while ((unsigned) x < table->subtables[x].next) {
        x = table->subtables[x].next;
        }
        /* Here x is the largest index in a group.
        ** Groups consist of adjacent variables.
        ** Hence, the next increment of x will move it to a new group.
        */
        i = table->invperm[x];
        entry[i] = table->subtables[x].keys;
        var[classes] = i;
    }

    qsort((void *)var,classes,sizeof(int),(DD_QSFP)ddSymmUniqueCompare);

    /* Now sift. */
    for (i = 0; i < ddMin(table->siftMaxVar,classes); i++) {
        if (ddTotalNumberSwapping >= table->siftMaxSwap)
        break;
            if (util_cpu_time() - table->startTime > table->timeLimit) {
              table->autoDyn = 0; /* prevent further reordering */
              break;
            }
        x = table->perm[var[i]];
        if ((unsigned) x >= table->subtables[x].next) {
#ifdef DD_STATS
        previousSize = table->keys - table->isolated;
#endif
        result = ddSymmSiftingConvAux(table,x,lower,upper);
        if (!result ) goto ddSymmSiftingConvOutOfMem;
#ifdef DD_STATS
        if (table->keys < (unsigned) previousSize + table->isolated) {
            (void) fprintf(table->out,"-");
        } else if (table->keys > (unsigned) previousSize +
               table->isolated) {
            (void) fprintf(table->out,"+");
        } else {
            (void) fprintf(table->out,"=");
        }
        fflush(table->out);
#endif
        }
    } /* for */
    }

    ddSymmSummary(table, lower, upper, &symvars, &symgroups);

#ifdef DD_STATS
    (void) fprintf(table->out, "\n#:S_SIFTING %8d: symmetric variables\n",
           symvars);
    (void) fprintf(table->out, "#:G_SIFTING %8d: symmetric groups",
           symgroups);
#endif

    FREE(var);
    FREE(entry);

    return(1+symvars);

ddSymmSiftingConvOutOfMem:

    if (entry != NULL) FREE(entry);
    if (var != NULL) FREE(var);

    return(0);

} /* end of cuddSymmSiftingConv */


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


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

} /* end of ddSymmUniqueCompare */


static int
ddSymmSiftingAux(
  DdManager * table,
  int  x,
  int  xLow,
  int  xHigh)
{
    Move *move;
    Move *moveUp;   /* list of up moves */
    Move *moveDown; /* list of down moves */
    int  initialSize;
    int  result;
    int  i;
    int  topbot;    /* index to either top or bottom of symmetry group */
    int  initGroupSize, finalGroupSize;


#ifdef DD_DEBUG
    /* check for previously detected symmetry */
    assert(table->subtables[x].next == (unsigned) x);
#endif

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

    moveDown = NULL;
    moveUp = NULL;

    if ((x - xLow) > (xHigh - x)) {
    /* Will go down first, unless x == xHigh:
    ** Look for consecutive symmetries above x.
    */
    for (i = x; i > xLow; i--) {
        if (!cuddSymmCheck(table,i-1,i))
        break;
        topbot = table->subtables[i-1].next; /* find top of i-1's group */
        table->subtables[i-1].next = i;
        table->subtables[x].next = topbot; /* x is bottom of group so its */
                           /* next is top of i-1's group */
        i = topbot + 1; /* add 1 for i--; new i is top of symm group */
    }
    } else {
    /* Will go up first unless x == xlow:
    ** Look for consecutive symmetries below x.
    */
    for (i = x; i < xHigh; i++) {
        if (!cuddSymmCheck(table,i,i+1))
        break;
        /* find bottom of i+1's symm group */
        topbot = i + 1;
        while ((unsigned) topbot < table->subtables[topbot].next) {
        topbot = table->subtables[topbot].next;
        }
        table->subtables[topbot].next = table->subtables[i].next;
        table->subtables[i].next = i + 1;
        i = topbot - 1; /* subtract 1 for i++; new i is bottom of group */
    }
    }

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

    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 */

    initGroupSize = 1;

    moveDown = ddSymmSiftingDown(table,x,xHigh);
        /* after this point x --> xHigh, unless early term */
    if (moveDown == MV_OOM) goto ddSymmSiftingAuxOutOfMem;
    if (moveDown == NULL) return(1);

    x = moveDown->y;
    /* Find bottom of x's group */
    i = x;
    while ((unsigned) i < table->subtables[i].next) {
        i = table->subtables[i].next;
    }
#ifdef DD_DEBUG
    /* x should be the top of the symmetry group and i the bottom */
    assert((unsigned) i >= table->subtables[i].next);
    assert((unsigned) x == table->subtables[i].next);
#endif
    finalGroupSize = i - x + 1;

    if (initGroupSize == finalGroupSize) {
        /* No new symmetry groups detected, return to best position */
        result = ddSymmSiftingBackward(table,moveDown,initialSize);
    } else {
        initialSize = table->keys - table->isolated;
        moveUp = ddSymmSiftingUp(table,x,xLow);
        result = ddSymmSiftingBackward(table,moveUp,initialSize);
    }
    if (!result) goto ddSymmSiftingAuxOutOfMem;

    } else if (cuddNextHigh(table,x) > xHigh) { /* Sift up */
    /* Find top of x's symm group */
    i = x;              /* bottom */
    x = table->subtables[x].next;   /* top */

    if (x == xLow) return(1); /* just one big group */

    initGroupSize = i - x + 1;

    moveUp = ddSymmSiftingUp(table,x,xLow);
        /* after this point x --> xLow, unless early term */
    if (moveUp == MV_OOM) goto ddSymmSiftingAuxOutOfMem;
    if (moveUp == NULL) return(1);

    x = moveUp->x;
    /* Find top of x's group */
    i = table->subtables[x].next;
#ifdef DD_DEBUG
    /* x should be the bottom of the symmetry group and i the top */
    assert((unsigned) x >= table->subtables[x].next);
    assert((unsigned) i == table->subtables[x].next);
#endif
    finalGroupSize = x - i + 1;

    if (initGroupSize == finalGroupSize) {
        /* No new symmetry groups detected, return to best position */
        result = ddSymmSiftingBackward(table,moveUp,initialSize);
    } else {
        initialSize = table->keys - table->isolated;
        moveDown = ddSymmSiftingDown(table,x,xHigh);
        result = ddSymmSiftingBackward(table,moveDown,initialSize);
    }
    if (!result) goto ddSymmSiftingAuxOutOfMem;

    } else if ((x - xLow) > (xHigh - x)) { /* must go down first: shorter */

    moveDown = ddSymmSiftingDown(table,x,xHigh);
    /* at this point x == xHigh, unless early term */
    if (moveDown == MV_OOM) goto ddSymmSiftingAuxOutOfMem;

    if (moveDown != NULL) {
        x = moveDown->y;    /* x is top here */
        i = x;
        while ((unsigned) i < table->subtables[i].next) {
        i = table->subtables[i].next;
        }
    } else {
        i = x;
        while ((unsigned) i < table->subtables[i].next) {
        i = table->subtables[i].next;
        }
        x = table->subtables[i].next;
    }
#ifdef DD_DEBUG
    /* x should be the top of the symmetry group and i the bottom */
    assert((unsigned) i >= table->subtables[i].next);
    assert((unsigned) x == table->subtables[i].next);
#endif
    initGroupSize = i - x + 1;

    moveUp = ddSymmSiftingUp(table,x,xLow);
    if (moveUp == MV_OOM) goto ddSymmSiftingAuxOutOfMem;

    if (moveUp != NULL) {
        x = moveUp->x;
        i = table->subtables[x].next;
    } else {
        i = x;
        while ((unsigned) x < table->subtables[x].next)
        x = table->subtables[x].next;
    }
#ifdef DD_DEBUG
    /* x should be the bottom of the symmetry group and i the top */
    assert((unsigned) x >= table->subtables[x].next);
    assert((unsigned) i == table->subtables[x].next);
#endif
    finalGroupSize = x - i + 1;

    if (initGroupSize == finalGroupSize) {
        /* No new symmetry groups detected, return to best position */
        result = ddSymmSiftingBackward(table,moveUp,initialSize);
    } else {
        while (moveDown != NULL) {
        move = moveDown->next;
        cuddDeallocMove(table, moveDown);
        moveDown = move;
        }
        initialSize = table->keys - table->isolated;
        moveDown = ddSymmSiftingDown(table,x,xHigh);
        result = ddSymmSiftingBackward(table,moveDown,initialSize);
    }
    if (!result) goto ddSymmSiftingAuxOutOfMem;

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

    moveUp = ddSymmSiftingUp(table,x,xLow);
    /* at this point x == xHigh, unless early term */
    if (moveUp == MV_OOM) goto ddSymmSiftingAuxOutOfMem;

    if (moveUp != NULL) {
        x = moveUp->x;
        i = table->subtables[x].next;
    } else {
        while ((unsigned) x < table->subtables[x].next)
        x = table->subtables[x].next;
        i = table->subtables[x].next;
    }
#ifdef DD_DEBUG
    /* x is bottom of the symmetry group and i is top */
    assert((unsigned) x >= table->subtables[x].next);
    assert((unsigned) i == table->subtables[x].next);
#endif
    initGroupSize = x - i + 1;

    moveDown = ddSymmSiftingDown(table,x,xHigh);
    if (moveDown == MV_OOM) goto ddSymmSiftingAuxOutOfMem;

    if (moveDown != NULL) {
        x = moveDown->y;
        i = x;
        while ((unsigned) i < table->subtables[i].next) {
        i = table->subtables[i].next;
        }
    } else {
        i = x;
        x = table->subtables[x].next;
    }
#ifdef DD_DEBUG
    /* x should be the top of the symmetry group and i the bottom */
    assert((unsigned) i >= table->subtables[i].next);
    assert((unsigned) x == table->subtables[i].next);
#endif
    finalGroupSize = i - x + 1;

    if (initGroupSize == finalGroupSize) {
        /* No new symmetries detected, go back to best position */
        result = ddSymmSiftingBackward(table,moveDown,initialSize);
    } else {
        while (moveUp != NULL) {
        move = moveUp->next;
        cuddDeallocMove(table, moveUp);
        moveUp = move;
        }
        initialSize = table->keys - table->isolated;
        moveUp = ddSymmSiftingUp(table,x,xLow);
        result = ddSymmSiftingBackward(table,moveUp,initialSize);
    }
    if (!result) goto ddSymmSiftingAuxOutOfMem;
    }

    while (moveDown != NULL) {
    move = moveDown->next;
    cuddDeallocMove(table, moveDown);
    moveDown = move;
    }
    while (moveUp != NULL) {
    move = moveUp->next;
    cuddDeallocMove(table, moveUp);
    moveUp = move;
    }

    return(1);

ddSymmSiftingAuxOutOfMem:
    if (moveDown != MV_OOM) {
    while (moveDown != NULL) {
        move = moveDown->next;
        cuddDeallocMove(table, moveDown);
        moveDown = move;
    }
    }
    if (moveUp != MV_OOM) {
    while (moveUp != NULL) {
        move = moveUp->next;
        cuddDeallocMove(table, moveUp);
        moveUp = move;
    }
    }

    return(0);

} /* end of ddSymmSiftingAux */


static int
ddSymmSiftingConvAux(
  DdManager * table,
  int  x,
  int  xLow,
  int  xHigh)
{
    Move *move;
    Move *moveUp;   /* list of up moves */
    Move *moveDown; /* list of down moves */
    int  initialSize;
    int  result;
    int  i;
    int  initGroupSize, finalGroupSize;


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

    moveDown = NULL;
    moveUp = NULL;

    if (x == xLow) { /* Sift down */
#ifdef DD_DEBUG
    /* x is bottom of symmetry group */
    assert((unsigned) x >= table->subtables[x].next);
#endif
    i = table->subtables[x].next;
    initGroupSize = x - i + 1;

    moveDown = ddSymmSiftingDown(table,x,xHigh);
    /* at this point x == xHigh, unless early term */
    if (moveDown == MV_OOM) goto ddSymmSiftingConvAuxOutOfMem;
    if (moveDown == NULL) return(1);

    x = moveDown->y;
    i = x;
    while ((unsigned) i < table->subtables[i].next) {
        i = table->subtables[i].next;
    }
#ifdef DD_DEBUG
    /* x should be the top of the symmetric group and i the bottom */
    assert((unsigned) i >= table->subtables[i].next);
    assert((unsigned) x == table->subtables[i].next);
#endif
    finalGroupSize = i - x + 1;

    if (initGroupSize == finalGroupSize) {
        /* No new symmetries detected, go back to best position */
        result = ddSymmSiftingBackward(table,moveDown,initialSize);
    } else {
        initialSize = table->keys - table->isolated;
        moveUp = ddSymmSiftingUp(table,x,xLow);
        result = ddSymmSiftingBackward(table,moveUp,initialSize);
    }
    if (!result) goto ddSymmSiftingConvAuxOutOfMem;

    } else if (cuddNextHigh(table,x) > xHigh) { /* Sift up */
    /* Find top of x's symm group */
    while ((unsigned) x < table->subtables[x].next)
        x = table->subtables[x].next;
    i = x;              /* bottom */
    x = table->subtables[x].next;   /* top */

    if (x == xLow) return(1);

    initGroupSize = i - x + 1;

    moveUp = ddSymmSiftingUp(table,x,xLow);
        /* at this point x == xLow, unless early term */
    if (moveUp == MV_OOM) goto ddSymmSiftingConvAuxOutOfMem;
    if (moveUp == NULL) return(1);

    x = moveUp->x;
    i = table->subtables[x].next;
#ifdef DD_DEBUG
    /* x should be the bottom of the symmetry group and i the top */
    assert((unsigned) x >= table->subtables[x].next);
    assert((unsigned) i == table->subtables[x].next);
#endif
    finalGroupSize = x - i + 1;

    if (initGroupSize == finalGroupSize) {
        /* No new symmetry groups detected, return to best position */
        result = ddSymmSiftingBackward(table,moveUp,initialSize);
    } else {
        initialSize = table->keys - table->isolated;
        moveDown = ddSymmSiftingDown(table,x,xHigh);
        result = ddSymmSiftingBackward(table,moveDown,initialSize);
    }
    if (!result)
        goto ddSymmSiftingConvAuxOutOfMem;

    } else if ((x - xLow) > (xHigh - x)) { /* must go down first: shorter */
    moveDown = ddSymmSiftingDown(table,x,xHigh);
        /* at this point x == xHigh, unless early term */
    if (moveDown == MV_OOM) goto ddSymmSiftingConvAuxOutOfMem;

    if (moveDown != NULL) {
        x = moveDown->y;
        i = x;
        while ((unsigned) i < table->subtables[i].next) {
        i = table->subtables[i].next;
        }
    } else {
        while ((unsigned) x < table->subtables[x].next)
        x = table->subtables[x].next;
        i = x;
        x = table->subtables[x].next;
    }
#ifdef DD_DEBUG
    /* x should be the top of the symmetry group and i the bottom */
    assert((unsigned) i >= table->subtables[i].next);
    assert((unsigned) x == table->subtables[i].next);
#endif
    initGroupSize = i - x + 1;

    moveUp = ddSymmSiftingUp(table,x,xLow);
    if (moveUp == MV_OOM) goto ddSymmSiftingConvAuxOutOfMem;

    if (moveUp != NULL) {
        x = moveUp->x;
        i = table->subtables[x].next;
    } else {
        i = x;
        while ((unsigned) x < table->subtables[x].next)
        x = table->subtables[x].next;
    }
#ifdef DD_DEBUG
    /* x should be the bottom of the symmetry group and i the top */
    assert((unsigned) x >= table->subtables[x].next);
    assert((unsigned) i == table->subtables[x].next);
#endif
    finalGroupSize = x - i + 1;

    if (initGroupSize == finalGroupSize) {
        /* No new symmetry groups detected, return to best position */
        result = ddSymmSiftingBackward(table,moveUp,initialSize);
    } else {
        while (moveDown != NULL) {
        move = moveDown->next;
        cuddDeallocMove(table, moveDown);
        moveDown = move;
        }
        initialSize = table->keys - table->isolated;
        moveDown = ddSymmSiftingDown(table,x,xHigh);
        result = ddSymmSiftingBackward(table,moveDown,initialSize);
    }
    if (!result) goto ddSymmSiftingConvAuxOutOfMem;

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

    moveUp = ddSymmSiftingUp(table,x,xLow);
    /* at this point x == xHigh, unless early term */
    if (moveUp == MV_OOM) goto ddSymmSiftingConvAuxOutOfMem;

    if (moveUp != NULL) {
        x = moveUp->x;
        i = table->subtables[x].next;
    } else {
        i = x;
        while ((unsigned) x < table->subtables[x].next)
        x = table->subtables[x].next;
    }
#ifdef DD_DEBUG
    /* x is bottom of the symmetry group and i is top */
    assert((unsigned) x >= table->subtables[x].next);
    assert((unsigned) i == table->subtables[x].next);
#endif
    initGroupSize = x - i + 1;

    moveDown = ddSymmSiftingDown(table,x,xHigh);
    if (moveDown == MV_OOM) goto ddSymmSiftingConvAuxOutOfMem;

    if (moveDown != NULL) {
        x = moveDown->y;
        i = x;
        while ((unsigned) i < table->subtables[i].next) {
        i = table->subtables[i].next;
        }
    } else {
        i = x;
        x = table->subtables[x].next;
    }
#ifdef DD_DEBUG
    /* x should be the top of the symmetry group and i the bottom */
    assert((unsigned) i >= table->subtables[i].next);
    assert((unsigned) x == table->subtables[i].next);
#endif
    finalGroupSize = i - x + 1;

    if (initGroupSize == finalGroupSize) {
        /* No new symmetries detected, go back to best position */
        result = ddSymmSiftingBackward(table,moveDown,initialSize);
    } else {
        while (moveUp != NULL) {
        move = moveUp->next;
        cuddDeallocMove(table, moveUp);
        moveUp = move;
        }
        initialSize = table->keys - table->isolated;
        moveUp = ddSymmSiftingUp(table,x,xLow);
        result = ddSymmSiftingBackward(table,moveUp,initialSize);
    }
    if (!result) goto ddSymmSiftingConvAuxOutOfMem;
    }

    while (moveDown != NULL) {
    move = moveDown->next;
    cuddDeallocMove(table, moveDown);
    moveDown = move;
    }
    while (moveUp != NULL) {
    move = moveUp->next;
    cuddDeallocMove(table, moveUp);
    moveUp = move;
    }

    return(1);

ddSymmSiftingConvAuxOutOfMem:
    if (moveDown != MV_OOM) {
    while (moveDown != NULL) {
        move = moveDown->next;
        cuddDeallocMove(table, moveDown);
        moveDown = move;
    }
    }
    if (moveUp != MV_OOM) {
    while (moveUp != NULL) {
        move = moveUp->next;
        cuddDeallocMove(table, moveUp);
        moveUp = move;
    }
    }

    return(0);

} /* end of ddSymmSiftingConvAux */


static Move *
ddSymmSiftingUp(
  DdManager * table,
  int  y,
  int  xLow)
{
    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


    moves = NULL;
    yindex = table->invperm[y];

    /* Initialize the lower bound.
    ** The part of the DD below the bottom of y' group will not change.
    ** The part of the DD above y that does not interact with y will not
    ** change. The rest may vanish in the best case, except for
    ** the nodes at level xLow, which will not vanish, regardless.
    */
    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;
    }
    }

    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;
        }
    }
    assert(L == checkL);
#endif
    gxtop = table->subtables[x].next;
    if (cuddSymmCheck(table,x,y)) {
        /* Symmetry found, attach symm 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;
    } else if (table->subtables[x].next == (unsigned) x &&
           table->subtables[y].next == (unsigned) y) {
        /* x and y have self symmetry */
        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 ddSymmSiftingUpOutOfMem;
        /* 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 ddSymmSiftingUpOutOfMem;
        move->x = x;
        move->y = y;
        move->size = size;
        move->next = moves;
        moves = move;
        if ((double) size > (double) limitSize * table->maxGrowth)
        return(moves);
        if (size < limitSize) limitSize = size;
    } else { /* Group move */
        size = ddSymmGroupMove(table,x,y,&moves);
        if (size == 0) goto ddSymmSiftingUpOutOfMem;
        /* 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(moves);
        if (size < limitSize) limitSize = size;
    }
    y = gxtop;
    x = cuddNextLow(table,y);
    }

    return(moves);

ddSymmSiftingUpOutOfMem:
    while (moves != NULL) {
    move = moves->next;
    cuddDeallocMove(table, moves);
    moves = move;
    }
    return(MV_OOM);

} /* end of ddSymmSiftingUp */


static Move *
ddSymmSiftingDown(
  DdManager * table,
  int  x,
  int  xHigh)
{
    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;
    int  z;
    int  zindex;
#ifdef DD_DEBUG
    int  checkR;
#endif

    moves = NULL;
    /* 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;
    }
    }

    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
    gybot = table->subtables[y].next;
    while (table->subtables[gybot].next != (unsigned) y)
        gybot = table->subtables[gybot].next;
    if (cuddSymmCheck(table,x,y)) {
        /* Symmetry found, attach symm groups */
        gxtop = table->subtables[x].next;
        table->subtables[x].next = y;
        table->subtables[gybot].next = gxtop;
    } else if (table->subtables[x].next == (unsigned) x &&
           table->subtables[y].next == (unsigned) y) {
        /* x and y have self symmetry */
        /* 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 ddSymmSiftingDownOutOfMem;
        move = (Move *) cuddDynamicAllocNode(table);
        if (move == NULL) goto ddSymmSiftingDownOutOfMem;
        move->x = x;
        move->y = y;
        move->size = size;
        move->next = moves;
        moves = move;
        if ((double) size > (double) limitSize * table->maxGrowth)
        return(moves);
        if (size < limitSize) limitSize = size;
    } 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 = ddSymmGroupMove(table,x,y,&moves);
        if (size == 0) goto ddSymmSiftingDownOutOfMem;
        if ((double) size > (double) limitSize * table->maxGrowth)
        return(moves);
        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(moves);

ddSymmSiftingDownOutOfMem:
    while (moves != NULL) {
    move = moves->next;
    cuddDeallocMove(table, moves);
    moves = move;
    }
    return(MV_OOM);

} /* end of ddSymmSiftingDown */


static int
ddSymmGroupMove(
  DdManager * table,
  int  x,
  int  y,
  Move ** moves)
{
    Move *move;
    int  size;
    int  i,j;
    int  xtop,xbot,xsize,ytop,ybot,ysize,newxtop;
    int  swapx,swapy;

#ifdef DD_DEBUG
    assert(x < y);  /* we assume that 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);
        swapx = x; swapy = y;
        y = x;
        x = y - 1;
    }
    y = ytop + i;
    x = y - 1;
    }

    /* fix symmetries */
    y = xtop; /* ytop is now where xtop used to be */
    for (i = 0; i < ysize-1 ; i++) {
    table->subtables[y].next = y + 1;
    y = y + 1;
    }
    table->subtables[y].next = xtop; /* y is bottom of its group, join */
                     /* its symmetry to top of its group */
    x = y + 1;
    newxtop = x;
    for (i = 0; i < xsize - 1 ; i++) {
    table->subtables[x].next = x + 1;
    x = x + 1;
    }
    table->subtables[x].next = newxtop; /* x is bottom of its group, join */
                    /* its symmetry to top of its group */
    /* Store group move */
    move = (Move *) cuddDynamicAllocNode(table);
    if (move == NULL) return(0);
    move->x = swapx;
    move->y = swapy;
    move->size = size;
    move->next = *moves;
    *moves = move;

    return(size);

} /* end of ddSymmGroupMove */


static int
ddSymmGroupMoveBackward(
  DdManager * table,
  int  x,
  int  y)
{
    int size;
    int i,j;
    int xtop,xbot,xsize,ytop,ybot,ysize,newxtop;

#ifdef DD_DEBUG
    assert(x < y); /* We assume that 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 = y - 1;
    }

    /* Fix symmetries. */
    y = xtop;
    for (i = 0; i < ysize-1 ; i++) {
    table->subtables[y].next = y + 1;
    y = y + 1;
    }
    table->subtables[y].next = xtop; /* y is bottom of its group, join */
                     /* its symmetry to top of its group */
    x = y + 1;
    newxtop = x;
    for (i = 0; i < xsize-1 ; i++) {
    table->subtables[x].next = x + 1;
    x = x + 1;
    }
    table->subtables[x].next = newxtop; /* x is bottom of its group, join */
                    /* its symmetry to top of its group */

    return(size);

} /* end of ddSymmGroupMoveBackward */


static int
ddSymmSiftingBackward(
  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->subtables[move->x].next == move->x && table->subtables[move->y].next == move->y) {
        res = cuddSwapInPlace(table,(int)move->x,(int)move->y);
#ifdef DD_DEBUG
        assert(table->subtables[move->x].next == move->x);
        assert(table->subtables[move->y].next == move->y);
#endif
    } else { /* Group move necessary */
        res = ddSymmGroupMoveBackward(table,(int)move->x,(int)move->y);
    }
    if (!res) return(0);
    }

    return(1);

} /* end of ddSymmSiftingBackward */


static void
ddSymmSummary(
  DdManager * table,
  int  lower,
  int  upper,
  int * symvars,
  int * symgroups)
{
    int i,x,gbot;
    int TotalSymm = 0;
    int TotalSymmGroups = 0;

    for (i = lower; i <= upper; i++) {
    if (table->subtables[i].next != (unsigned) i) {
        TotalSymmGroups++;
        x = i;
        do {
        TotalSymm++;
        gbot = x;
        x = table->subtables[x].next;
        } while (x != i);
#ifdef DD_DEBUG
        assert(table->subtables[gbot].next == (unsigned) i);
#endif
        i = gbot;
    }
    }
    *symvars = TotalSymm;
    *symgroups = TotalSymmGroups;

    return;

} /* end of ddSymmSummary */