src/cuBdd/cuddZddSymm.c

Go to the documentation of this file.

#include "util.h"
#include "cuddInt.h"

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

#define ZDD_MV_OOM (Move *)1

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

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

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

#ifndef lint
static char rcsid[] DD_UNUSED = "$Id: cuddZddSymm.c,v 1.29 2004/08/13 18:04:54 fabio Exp $";
#endif

extern int      *zdd_entry;

extern int      zddTotalNumberSwapping;

static DdNode   *empty;

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


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

static int cuddZddSymmSiftingAux (DdManager *table, int x, int x_low, int x_high);
static int cuddZddSymmSiftingConvAux (DdManager *table, int x, int x_low, int x_high);
static Move * cuddZddSymmSifting_up (DdManager *table, int x, int x_low, int initial_size);
static Move * cuddZddSymmSifting_down (DdManager *table, int x, int x_high, int initial_size);
static int cuddZddSymmSiftingBackward (DdManager *table, Move *moves, int size);
static int zdd_group_move (DdManager *table, int x, int y, Move **moves);
static int zdd_group_move_backward (DdManager *table, int x, int y);
static void cuddZddSymmSummary (DdManager *table, int lower, int upper, int *symvars, int *symgroups);

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


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

    for (i = lower; i < upper; i++) {
        if (table->subtableZ[i].next != (unsigned) i) {
            x = i;
            (void) fprintf(table->out,"Group:");
            do {
                (void) fprintf(table->out,"  %d", table->invpermZ[x]);
                TotalSymm++;
                gbot = x;
                x = table->subtableZ[x].next;
            } while (x != i);
            TotalSymmGroups++;
#ifdef DD_DEBUG
            assert(table->subtableZ[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_zddSymmProfile */


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


int
cuddZddSymmCheck(
  DdManager * table,
  int  x,
  int  y)
{
    int         i;
    DdNode      *f, *f0, *f1, *f01, *f00, *f11, *f10;
    int         yindex;
    int         xsymmy = 1;
    int         xsymmyp = 1;
    int         arccount = 0;
    int         TotalRefCount = 0;
    int         symm_found;

    empty = table->zero;

    yindex = table->invpermZ[y];
    for (i = table->subtableZ[x].slots - 1; i >= 0; i--) {
        f = table->subtableZ[x].nodelist[i];
        while (f != NULL) {
            /* Find f1, f0, f11, f10, f01, f00 */
            f1 = cuddT(f);
            f0 = cuddE(f);
            if ((int) f1->index == yindex) {
                f11 = cuddT(f1);
                f10 = cuddE(f1);
                if (f10 != empty)
                    arccount++;
            } else {
                if ((int) f0->index != yindex) {
                    return(0); /* f bypasses layer y */
                }
                f11 = empty;
                f10 = f1;
            }
            if ((int) f0->index == yindex) {
                f01 = cuddT(f0);
                f00 = cuddE(f0);
                if (f00 != empty)
                    arccount++;
            } else {
                f01 = empty;
                f00 = f0;
            }
            if (f01 != f10)
                xsymmy = 0;
            if (f11 != f00)
                xsymmyp = 0;
            if ((xsymmy == 0) && (xsymmyp == 0))
                return(0);

            f = f->next;
        } /* for each element of the collision list */
    } /* for each slot of the subtable */

    /* Calculate the total reference counts of y
    ** whose else arc is not empty.
    */
    for (i = table->subtableZ[y].slots - 1; i >= 0; i--) {
        f = table->subtableZ[y].nodelist[i];
        while (f != NIL(DdNode)) {
            if (cuddE(f) != empty)
                TotalRefCount += f->ref;
            f = f->next;
        }
    }

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

    return(symm_found);

} /* end cuddZddSymmCheck */


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

    nvars = table->sizeZ;

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

    for (i = 0; i < nvars; i++) {
        x = table->permZ[i];
        zdd_entry[i] = table->subtableZ[x].keys;
        var[i] = i;
    }

    qsort((void *)var, nvars, sizeof(int), (DD_QSFP)cuddZddUniqueCompare);

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

    iteration = ddMin(table->siftMaxVar, nvars);
    for (i = 0; i < iteration; i++) {
        if (zddTotalNumberSwapping >= table->siftMaxSwap)
            break;
        x = table->permZ[var[i]];
#ifdef DD_STATS
        previousSize = table->keysZ;
#endif
        if (x < lower || x > upper) continue;
        if (table->subtableZ[x].next == (unsigned) x) {
            result = cuddZddSymmSiftingAux(table, x, lower, upper);
            if (!result)
                goto cuddZddSymmSiftingOutOfMem;
#ifdef DD_STATS
            if (table->keysZ < (unsigned) previousSize) {
                (void) fprintf(table->out,"-");
            } else if (table->keysZ > (unsigned) previousSize) {
                (void) fprintf(table->out,"+");
#ifdef DD_VERBOSE
                (void) fprintf(table->out,"\nSize increased from %d to %d while sifting variable %d\n", previousSize, table->keysZ, var[i]);
#endif
            } else {
                (void) fprintf(table->out,"=");
            }
            fflush(table->out);
#endif
        }
    }

    FREE(var);
    FREE(zdd_entry);

    cuddZddSymmSummary(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\n",symgroups);
#endif

    return(1+symvars);

cuddZddSymmSiftingOutOfMem:

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

    return(0);

} /* end of cuddZddSymmSifting */


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

    initialSize = table->keysZ;

    nvars = table->sizeZ;

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

    for (i = 0; i < nvars; i++) {
        x = table->permZ[i];
        zdd_entry[i] = table->subtableZ[x].keys;
        var[i] = i;
    }

    qsort((void *)var, nvars, sizeof(int), (DD_QSFP)cuddZddUniqueCompare);

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

    iteration = ddMin(table->siftMaxVar, table->sizeZ);
    for (i = 0; i < iteration; i++) {
        if (zddTotalNumberSwapping >= table->siftMaxSwap)
            break;
        x = table->permZ[var[i]];
        if (x < lower || x > upper) continue;
        /* Only sift if not in symmetry group already. */
        if (table->subtableZ[x].next == (unsigned) x) {
#ifdef DD_STATS
            previousSize = table->keysZ;
#endif
            result = cuddZddSymmSiftingAux(table, x, lower, upper);
            if (!result)
                goto cuddZddSymmSiftingConvOutOfMem;
#ifdef DD_STATS
            if (table->keysZ < (unsigned) previousSize) {
                (void) fprintf(table->out,"-");
            } else if (table->keysZ > (unsigned) previousSize) {
                (void) fprintf(table->out,"+");
#ifdef DD_VERBOSE
                (void) fprintf(table->out,"\nSize increased from %d to %d while sifting variable %d\n", previousSize, table->keysZ, var[i]);
#endif
            } else {
                (void) fprintf(table->out,"=");
            }
            fflush(table->out);
#endif
        }
    }

    /* Sifting now until convergence. */
    while ((unsigned) initialSize > table->keysZ) {
        initialSize = table->keysZ;
#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->subtableZ[x].next)
                x = table->subtableZ[x].next;
            /* Here x is the largest index in a group.
            ** Groups consists of adjacent variables.
            ** Hence, the next increment of x will move it to a new group.
            */
            i = table->invpermZ[x];
            zdd_entry[i] = table->subtableZ[x].keys;
            var[classes] = i;
        }

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

        /* Now sift. */
        iteration = ddMin(table->siftMaxVar, nvars);
        for (i = 0; i < iteration; i++) {
            if (zddTotalNumberSwapping >= table->siftMaxSwap)
                break;
            x = table->permZ[var[i]];
            if ((unsigned) x >= table->subtableZ[x].next) {
#ifdef DD_STATS
                previousSize = table->keysZ;
#endif
                result = cuddZddSymmSiftingConvAux(table, x, lower, upper);
                if (!result)
                    goto cuddZddSymmSiftingConvOutOfMem;
#ifdef DD_STATS
                if (table->keysZ < (unsigned) previousSize) {
                    (void) fprintf(table->out,"-");
                } else if (table->keysZ > (unsigned) previousSize) {
                    (void) fprintf(table->out,"+");
#ifdef DD_VERBOSE
                (void) fprintf(table->out,"\nSize increased from %d to %d while sifting variable %d\n", previousSize, table->keysZ, var[i]);
#endif
                } else {
                    (void) fprintf(table->out,"=");
                }
                fflush(table->out);
#endif
            }
        } /* for */
    }

    cuddZddSymmSummary(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\n",
                   symgroups);
#endif

    FREE(var);
    FREE(zdd_entry);

    return(1+symvars);

cuddZddSymmSiftingConvOutOfMem:

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

    return(0);

} /* end of cuddZddSymmSiftingConv */


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


static int
cuddZddSymmSiftingAux(
  DdManager * table,
  int  x,
  int  x_low,
  int  x_high)
{
    Move *move;
    Move *move_up;      /* list of up move */
    Move *move_down;    /* list of down move */
    int  initial_size;
    int  result;
    int  i;
    int  topbot;        /* index to either top or bottom of symmetry group */
    int  init_group_size, final_group_size;

    initial_size = table->keysZ;

    move_down = NULL;
    move_up = NULL;

    /* Look for consecutive symmetries above x. */
    for (i = x; i > x_low; i--) {
        if (!cuddZddSymmCheck(table, i - 1, i))
            break;
        /* find top of i-1's symmetry */
        topbot = table->subtableZ[i - 1].next;
        table->subtableZ[i - 1].next = i;
        table->subtableZ[x].next = topbot;
        /* x is bottom of group so its symmetry is top of i-1's
           group */
        i = topbot + 1; /* add 1 for i--, new i is top of symm group */
    }
    /* Look for consecutive symmetries below x. */
    for (i = x; i < x_high; i++) {
        if (!cuddZddSymmCheck(table, i, i + 1))
            break;
        /* find bottom of i+1's symm group */
        topbot = i + 1;
        while ((unsigned) topbot < table->subtableZ[topbot].next)
            topbot = table->subtableZ[topbot].next;

        table->subtableZ[topbot].next = table->subtableZ[i].next;
        table->subtableZ[i].next = i + 1;
        i = topbot - 1; /* add 1 for i++,
                           new i is bottom of symm group */
    }

    /* Now x maybe in the middle of a symmetry group. */
    if (x == x_low) { /* Sift down */
        /* Find bottom of x's symm group */
        while ((unsigned) x < table->subtableZ[x].next)
            x = table->subtableZ[x].next;

        i = table->subtableZ[x].next;
        init_group_size = x - i + 1;

        move_down = cuddZddSymmSifting_down(table, x, x_high,
            initial_size);
        /* after that point x --> x_high, unless early term */
        if (move_down == ZDD_MV_OOM)
            goto cuddZddSymmSiftingAuxOutOfMem;

        if (move_down == NULL ||
            table->subtableZ[move_down->y].next != move_down->y) {
            /* symmetry detected may have to make another complete
               pass */
            if (move_down != NULL)
                x = move_down->y;
            else
                x = table->subtableZ[x].next;
            i = x;
            while ((unsigned) i < table->subtableZ[i].next) {
                i = table->subtableZ[i].next;
            }
            final_group_size = i - x + 1;

            if (init_group_size == final_group_size) {
                /* No new symmetry groups detected,
                   return to best position */
                result = cuddZddSymmSiftingBackward(table,
                    move_down, initial_size);
            }
            else {
                initial_size = table->keysZ;
                move_up = cuddZddSymmSifting_up(table, x, x_low,
                    initial_size);
                result = cuddZddSymmSiftingBackward(table, move_up,
                    initial_size);
            }
        }
        else {
            result = cuddZddSymmSiftingBackward(table, move_down,
                initial_size);
            /* move backward and stop at best position */
        }
        if (!result)
            goto cuddZddSymmSiftingAuxOutOfMem;
    }
    else if (x == x_high) { /* Sift up */
        /* Find top of x's symm group */
        while ((unsigned) x < table->subtableZ[x].next)
            x = table->subtableZ[x].next;
        x = table->subtableZ[x].next;

        i = x;
        while ((unsigned) i < table->subtableZ[i].next) {
            i = table->subtableZ[i].next;
        }
        init_group_size = i - x + 1;

        move_up = cuddZddSymmSifting_up(table, x, x_low, initial_size);
        /* after that point x --> x_low, unless early term */
        if (move_up == ZDD_MV_OOM)
            goto cuddZddSymmSiftingAuxOutOfMem;

        if (move_up == NULL ||
            table->subtableZ[move_up->x].next != move_up->x) {
            /* symmetry detected may have to make another complete
                pass */
            if (move_up != NULL)
                x = move_up->x;
            else {
                while ((unsigned) x < table->subtableZ[x].next)
                    x = table->subtableZ[x].next;
            }
            i = table->subtableZ[x].next;
            final_group_size = x - i + 1;

            if (init_group_size == final_group_size) {
                /* No new symmetry groups detected,
                   return to best position */
                result = cuddZddSymmSiftingBackward(table, move_up,
                    initial_size);
            }
            else {
                initial_size = table->keysZ;
                move_down = cuddZddSymmSifting_down(table, x, x_high,
                    initial_size);
                result = cuddZddSymmSiftingBackward(table, move_down,
                    initial_size);
            }
        }
        else {
            result = cuddZddSymmSiftingBackward(table, move_up,
                initial_size);
            /* move backward and stop at best position */
        }
        if (!result)
            goto cuddZddSymmSiftingAuxOutOfMem;
    }
    else if ((x - x_low) > (x_high - x)) { /* must go down first:
                                                shorter */
        /* Find bottom of x's symm group */
        while ((unsigned) x < table->subtableZ[x].next)
            x = table->subtableZ[x].next;

        move_down = cuddZddSymmSifting_down(table, x, x_high,
            initial_size);
        /* after that point x --> x_high, unless early term */
        if (move_down == ZDD_MV_OOM)
            goto cuddZddSymmSiftingAuxOutOfMem;

        if (move_down != NULL) {
            x = move_down->y;
        }
        else {
            x = table->subtableZ[x].next;
        }
        i = x;
        while ((unsigned) i < table->subtableZ[i].next) {
            i = table->subtableZ[i].next;
        }
        init_group_size = i - x + 1;

        move_up = cuddZddSymmSifting_up(table, x, x_low, initial_size);
        if (move_up == ZDD_MV_OOM)
            goto cuddZddSymmSiftingAuxOutOfMem;

        if (move_up == NULL ||
            table->subtableZ[move_up->x].next != move_up->x) {
            /* symmetry detected may have to make another complete
               pass */
            if (move_up != NULL) {
                x = move_up->x;
            }
            else {
                while ((unsigned) x < table->subtableZ[x].next)
                    x = table->subtableZ[x].next;
            }
            i = table->subtableZ[x].next;
            final_group_size = x - i + 1;

            if (init_group_size == final_group_size) {
                /* No new symmetry groups detected,
                   return to best position */
                result = cuddZddSymmSiftingBackward(table, move_up,
                    initial_size);
            }
            else {
                while (move_down != NULL) {
                    move = move_down->next;
                    cuddDeallocMove(table, move_down);
                    move_down = move;
                }
                initial_size = table->keysZ;
                move_down = cuddZddSymmSifting_down(table, x, x_high,
                    initial_size);
                result = cuddZddSymmSiftingBackward(table, move_down,
                    initial_size);
            }
        }
        else {
            result = cuddZddSymmSiftingBackward(table, move_up,
                initial_size);
            /* move backward and stop at best position */
        }
        if (!result)
            goto cuddZddSymmSiftingAuxOutOfMem;
    }
    else { /* moving up first:shorter */
        /* Find top of x's symmetry group */
        while ((unsigned) x < table->subtableZ[x].next)
            x = table->subtableZ[x].next;
        x = table->subtableZ[x].next;

        move_up = cuddZddSymmSifting_up(table, x, x_low, initial_size);
        /* after that point x --> x_high, unless early term */
        if (move_up == ZDD_MV_OOM)
            goto cuddZddSymmSiftingAuxOutOfMem;

        if (move_up != NULL) {
            x = move_up->x;
        }
        else {
            while ((unsigned) x < table->subtableZ[x].next)
                x = table->subtableZ[x].next;
        }
        i = table->subtableZ[x].next;
        init_group_size = x - i + 1;

        move_down = cuddZddSymmSifting_down(table, x, x_high,
            initial_size);
        if (move_down == ZDD_MV_OOM)
            goto cuddZddSymmSiftingAuxOutOfMem;

        if (move_down == NULL ||
            table->subtableZ[move_down->y].next != move_down->y) {
            /* symmetry detected may have to make another complete
               pass */
            if (move_down != NULL) {
                x = move_down->y;
            }
            else {
                x = table->subtableZ[x].next;
            }
            i = x;
            while ((unsigned) i < table->subtableZ[i].next) {
                i = table->subtableZ[i].next;
            }
            final_group_size = i - x + 1;

            if (init_group_size == final_group_size) {
                /* No new symmetries detected,
                   go back to best position */
                result = cuddZddSymmSiftingBackward(table, move_down,
                    initial_size);
            }
            else {
                while (move_up != NULL) {
                    move = move_up->next;
                    cuddDeallocMove(table, move_up);
                    move_up = move;
                }
                initial_size = table->keysZ;
                move_up = cuddZddSymmSifting_up(table, x, x_low,
                    initial_size);
                result = cuddZddSymmSiftingBackward(table, move_up,
                    initial_size);
            }
        }
        else {
            result = cuddZddSymmSiftingBackward(table, move_down,
                initial_size);
            /* move backward and stop at best position */
        }
        if (!result)
            goto cuddZddSymmSiftingAuxOutOfMem;
    }

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

    return(1);

cuddZddSymmSiftingAuxOutOfMem:
    if (move_down != ZDD_MV_OOM) {
        while (move_down != NULL) {
            move = move_down->next;
            cuddDeallocMove(table, move_down);
            move_down = move;
        }
    }
    if (move_up != ZDD_MV_OOM) {
        while (move_up != NULL) {
            move = move_up->next;
            cuddDeallocMove(table, move_up);
            move_up = move;
        }
    }

    return(0);

} /* end of cuddZddSymmSiftingAux */


static int
cuddZddSymmSiftingConvAux(
  DdManager * table,
  int  x,
  int  x_low,
  int  x_high)
{
    Move        *move;
    Move        *move_up;       /* list of up move */
    Move        *move_down;     /* list of down move */
    int         initial_size;
    int         result;
    int         i;
    int         init_group_size, final_group_size;

    initial_size = table->keysZ;

    move_down = NULL;
    move_up = NULL;

    if (x == x_low) { /* Sift down */
        i = table->subtableZ[x].next;
        init_group_size = x - i + 1;

        move_down = cuddZddSymmSifting_down(table, x, x_high,
            initial_size);
        /* after that point x --> x_high, unless early term */
        if (move_down == ZDD_MV_OOM)
            goto cuddZddSymmSiftingConvAuxOutOfMem;

        if (move_down == NULL ||
            table->subtableZ[move_down->y].next != move_down->y) {
            /* symmetry detected may have to make another complete
                pass */
            if (move_down != NULL)
                x = move_down->y;
            else {
                while ((unsigned) x < table->subtableZ[x].next)
                    x = table->subtableZ[x].next;
                x = table->subtableZ[x].next;
            }
            i = x;
            while ((unsigned) i < table->subtableZ[i].next) {
                i = table->subtableZ[i].next;
            }
            final_group_size = i - x + 1;

            if (init_group_size == final_group_size) {
                /* No new symmetries detected,
                   go back to best position */
                result = cuddZddSymmSiftingBackward(table, move_down,
                    initial_size);
            }
            else {
                initial_size = table->keysZ;
                move_up = cuddZddSymmSifting_up(table, x, x_low,
                    initial_size);
                result = cuddZddSymmSiftingBackward(table, move_up,
                    initial_size);
            }
        }
        else {
            result = cuddZddSymmSiftingBackward(table, move_down,
                initial_size);
            /* move backward and stop at best position */
        }
        if (!result)
            goto cuddZddSymmSiftingConvAuxOutOfMem;
    }
    else if (x == x_high) { /* Sift up */
        /* Find top of x's symm group */
        while ((unsigned) x < table->subtableZ[x].next)
            x = table->subtableZ[x].next;
        x = table->subtableZ[x].next;

        i = x;
        while ((unsigned) i < table->subtableZ[i].next) {
            i = table->subtableZ[i].next;
        }
        init_group_size = i - x + 1;

        move_up = cuddZddSymmSifting_up(table, x, x_low, initial_size);
        /* after that point x --> x_low, unless early term */
        if (move_up == ZDD_MV_OOM)
            goto cuddZddSymmSiftingConvAuxOutOfMem;

        if (move_up == NULL ||
            table->subtableZ[move_up->x].next != move_up->x) {
            /* symmetry detected may have to make another complete
               pass */
            if (move_up != NULL)
                x = move_up->x;
            else {
                while ((unsigned) x < table->subtableZ[x].next)
                    x = table->subtableZ[x].next;
            }
            i = table->subtableZ[x].next;
            final_group_size = x - i + 1;

            if (init_group_size == final_group_size) {
                /* No new symmetry groups detected,
                   return to best position */
                result = cuddZddSymmSiftingBackward(table, move_up,
                    initial_size);
            }
            else {
                initial_size = table->keysZ;
                move_down = cuddZddSymmSifting_down(table, x, x_high,
                    initial_size);
                result = cuddZddSymmSiftingBackward(table, move_down,
                    initial_size);
            }
        }
        else {
            result = cuddZddSymmSiftingBackward(table, move_up,
                initial_size);
            /* move backward and stop at best position */
        }
        if (!result)
            goto cuddZddSymmSiftingConvAuxOutOfMem;
    }
    else if ((x - x_low) > (x_high - x)) { /* must go down first:
                                                shorter */
        move_down = cuddZddSymmSifting_down(table, x, x_high,
            initial_size);
        /* after that point x --> x_high */
        if (move_down == ZDD_MV_OOM)
            goto cuddZddSymmSiftingConvAuxOutOfMem;

        if (move_down != NULL) {
            x = move_down->y;
        }
        else {
            while ((unsigned) x < table->subtableZ[x].next)
                x = table->subtableZ[x].next;
            x = table->subtableZ[x].next;
        }
        i = x;
        while ((unsigned) i < table->subtableZ[i].next) {
            i = table->subtableZ[i].next;
        }
        init_group_size = i - x + 1;

        move_up = cuddZddSymmSifting_up(table, x, x_low, initial_size);
        if (move_up == ZDD_MV_OOM)
            goto cuddZddSymmSiftingConvAuxOutOfMem;

        if (move_up == NULL ||
            table->subtableZ[move_up->x].next != move_up->x) {
            /* symmetry detected may have to make another complete
               pass */
            if (move_up != NULL) {
                x = move_up->x;
            }
            else {
                while ((unsigned) x < table->subtableZ[x].next)
                    x = table->subtableZ[x].next;
            }
            i = table->subtableZ[x].next;
            final_group_size = x - i + 1;

            if (init_group_size == final_group_size) {
                /* No new symmetry groups detected,
                   return to best position */
                result = cuddZddSymmSiftingBackward(table, move_up,
                    initial_size);
            }
            else {
                while (move_down != NULL) {
                    move = move_down->next;
                    cuddDeallocMove(table, move_down);
                    move_down = move;
                }
                initial_size = table->keysZ;
                move_down = cuddZddSymmSifting_down(table, x, x_high,
                    initial_size);
                result = cuddZddSymmSiftingBackward(table, move_down,
                    initial_size);
            }
        }
        else {
            result = cuddZddSymmSiftingBackward(table, move_up,
                initial_size);
            /* move backward and stop at best position */
        }
        if (!result)
            goto cuddZddSymmSiftingConvAuxOutOfMem;
    }
    else { /* moving up first:shorter */
        /* Find top of x's symmetry group */
        x = table->subtableZ[x].next;

        move_up = cuddZddSymmSifting_up(table, x, x_low, initial_size);
        /* after that point x --> x_high, unless early term */
        if (move_up == ZDD_MV_OOM)
            goto cuddZddSymmSiftingConvAuxOutOfMem;

        if (move_up != NULL) {
            x = move_up->x;
        }
        else {
            while ((unsigned) x < table->subtableZ[x].next)
                x = table->subtableZ[x].next;
        }
        i = table->subtableZ[x].next;
        init_group_size = x - i + 1;

        move_down = cuddZddSymmSifting_down(table, x, x_high,
            initial_size);
        if (move_down == ZDD_MV_OOM)
            goto cuddZddSymmSiftingConvAuxOutOfMem;

        if (move_down == NULL ||
            table->subtableZ[move_down->y].next != move_down->y) {
            /* symmetry detected may have to make another complete
               pass */
            if (move_down != NULL) {
                x = move_down->y;
            }
            else {
                while ((unsigned) x < table->subtableZ[x].next)
                    x = table->subtableZ[x].next;
                x = table->subtableZ[x].next;
            }
            i = x;
            while ((unsigned) i < table->subtableZ[i].next) {
                i = table->subtableZ[i].next;
            }
            final_group_size = i - x + 1;

            if (init_group_size == final_group_size) {
                /* No new symmetries detected,
                   go back to best position */
                result = cuddZddSymmSiftingBackward(table, move_down,
                    initial_size);
            }
            else {
                while (move_up != NULL) {
                    move = move_up->next;
                    cuddDeallocMove(table, move_up);
                    move_up = move;
                }
                initial_size = table->keysZ;
                move_up = cuddZddSymmSifting_up(table, x, x_low,
                    initial_size);
                result = cuddZddSymmSiftingBackward(table, move_up,
                    initial_size);
            }
        }
        else {
            result = cuddZddSymmSiftingBackward(table, move_down,
                initial_size);
            /* move backward and stop at best position */
        }
        if (!result)
            goto cuddZddSymmSiftingConvAuxOutOfMem;
    }

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

    return(1);

cuddZddSymmSiftingConvAuxOutOfMem:
    if (move_down != ZDD_MV_OOM) {
        while (move_down != NULL) {
            move = move_down->next;
            cuddDeallocMove(table, move_down);
            move_down = move;
        }
    }
    if (move_up != ZDD_MV_OOM) {
        while (move_up != NULL) {
            move = move_up->next;
            cuddDeallocMove(table, move_up);
            move_up = move;
        }
    }

    return(0);

} /* end of cuddZddSymmSiftingConvAux */


static Move *
cuddZddSymmSifting_up(
  DdManager * table,
  int  x,
  int  x_low,
  int  initial_size)
{
    Move        *moves;
    Move        *move;
    int         y;
    int         size;
    int         limit_size = initial_size;
    int         i, gytop;

    moves = NULL;
    y = cuddZddNextLow(table, x);
    while (y >= x_low) {
        gytop = table->subtableZ[y].next;
        if (cuddZddSymmCheck(table, y, x)) {
            /* Symmetry found, attach symm groups */
            table->subtableZ[y].next = x;
            i = table->subtableZ[x].next;
            while (table->subtableZ[i].next != (unsigned) x)
                i = table->subtableZ[i].next;
            table->subtableZ[i].next = gytop;
        }
        else if ((table->subtableZ[x].next == (unsigned) x) &&
            (table->subtableZ[y].next == (unsigned) y)) {
            /* x and y have self symmetry */
            size = cuddZddSwapInPlace(table, y, x);
            if (size == 0)
                goto cuddZddSymmSifting_upOutOfMem;
            move = (Move *)cuddDynamicAllocNode(table);
            if (move == NULL)
                goto cuddZddSymmSifting_upOutOfMem;
            move->x = y;
            move->y = x;
            move->size = size;
            move->next = moves;
            moves = move;
            if ((double)size >
                (double)limit_size * table->maxGrowth)
                return(moves);
            if (size < limit_size)
                limit_size = size;
        }
        else { /* Group move */
            size = zdd_group_move(table, y, x, &moves);
            if ((double)size >
                (double)limit_size * table->maxGrowth)
                return(moves);
            if (size < limit_size)
                limit_size = size;
        }
        x = gytop;
        y = cuddZddNextLow(table, x);
    }

    return(moves);

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

} /* end of cuddZddSymmSifting_up */


static Move *
cuddZddSymmSifting_down(
  DdManager * table,
  int  x,
  int  x_high,
  int  initial_size)
{
    Move        *moves;
    Move        *move;
    int         y;
    int         size;
    int         limit_size = initial_size;
    int         i, gxtop, gybot;

    moves = NULL;
    y = cuddZddNextHigh(table, x);
    while (y <= x_high) {
        gybot = table->subtableZ[y].next;
        while (table->subtableZ[gybot].next != (unsigned) y)
            gybot = table->subtableZ[gybot].next;
        if (cuddZddSymmCheck(table, x, y)) {
            /* Symmetry found, attach symm groups */
            gxtop = table->subtableZ[x].next;
            table->subtableZ[x].next = y;
            i = table->subtableZ[y].next;
            while (table->subtableZ[i].next != (unsigned) y)
                i = table->subtableZ[i].next;
            table->subtableZ[i].next = gxtop;
        }
        else if ((table->subtableZ[x].next == (unsigned) x) &&
            (table->subtableZ[y].next == (unsigned) y)) {
            /* x and y have self symmetry */
            size = cuddZddSwapInPlace(table, x, y);
            if (size == 0)
                goto cuddZddSymmSifting_downOutOfMem;
            move = (Move *)cuddDynamicAllocNode(table);
            if (move == NULL)
                goto cuddZddSymmSifting_downOutOfMem;
            move->x = x;
            move->y = y;
            move->size = size;
            move->next = moves;
            moves = move;
            if ((double)size >
                (double)limit_size * table->maxGrowth)
                return(moves);
            if (size < limit_size)
                limit_size = size;
            x = y;
            y = cuddZddNextHigh(table, x);
        }
        else { /* Group move */
            size = zdd_group_move(table, x, y, &moves);
            if ((double)size >
                (double)limit_size * table->maxGrowth)
                return(moves);
            if (size < limit_size)
                limit_size = size;
        }
        x = gybot;
        y = cuddZddNextHigh(table, x);
    }

    return(moves);

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

} /* end of cuddZddSymmSifting_down */


static int
cuddZddSymmSiftingBackward(
  DdManager * table,
  Move * moves,
  int  size)
{
    int         i;
    int         i_best;
    Move        *move;
    int         res;

    i_best = -1;
    for (move = moves, i = 0; move != NULL; move = move->next, i++) {
        if (move->size < size) {
            i_best = i;
            size = move->size;
        }
    }

    for (move = moves, i = 0; move != NULL; move = move->next, i++) {
        if (i == i_best) break;
        if ((table->subtableZ[move->x].next == move->x) &&
            (table->subtableZ[move->y].next == move->y)) {
            res = cuddZddSwapInPlace(table, move->x, move->y);
            if (!res) return(0);
        }
        else { /* Group move necessary */
            res = zdd_group_move_backward(table, move->x, move->y);
        }
        if (i_best == -1 && res == size)
            break;
    }

    return(1);

} /* end of cuddZddSymmSiftingBackward */


static int
zdd_group_move(
  DdManager * table,
  int  x,
  int  y,
  Move ** moves)
{
    Move        *move;
    int         size;
    int         i, temp, gxtop, gxbot, gybot, yprev;
    int         swapx, swapy;

#ifdef DD_DEBUG
    assert(x < y);      /* we assume that x < y */
#endif
    /* Find top and bottom for the two groups. */
    gxtop = table->subtableZ[x].next;
    gxbot = x;
    gybot = table->subtableZ[y].next;
    while (table->subtableZ[gybot].next != (unsigned) y)
        gybot = table->subtableZ[gybot].next;
    yprev = gybot;

    while (x <= y) {
        while (y > gxtop) {
            /* Set correct symmetries. */
            temp = table->subtableZ[x].next;
            if (temp == x)
                temp = y;
            i = gxtop;
            for (;;) {
                if (table->subtableZ[i].next == (unsigned) x) {
                    table->subtableZ[i].next = y;
                    break;
                } else {
                    i = table->subtableZ[i].next;
                }
            }
            if (table->subtableZ[y].next != (unsigned) y) {
                table->subtableZ[x].next = table->subtableZ[y].next;
            } else {
                table->subtableZ[x].next = x;
            }

            if (yprev != y) {
                table->subtableZ[yprev].next = x;
            } else {
                yprev = x;
            }
            table->subtableZ[y].next = temp;

            size = cuddZddSwapInPlace(table, x, y);
            if (size == 0)
                goto zdd_group_moveOutOfMem;
            swapx = x;
            swapy = y;
            y = x;
            x--;
        } /* while y > gxtop */

        /* Trying to find the next y. */
        if (table->subtableZ[y].next <= (unsigned) y) {
            gybot = y;
        } else {
            y = table->subtableZ[y].next;
        }

        yprev = gxtop;
        gxtop++;
        gxbot++;
        x = gxbot;
    } /* while x <= y, end of group movement */
    move = (Move *)cuddDynamicAllocNode(table);
    if (move == NULL)
        goto zdd_group_moveOutOfMem;
    move->x = swapx;
    move->y = swapy;
    move->size = table->keysZ;
    move->next = *moves;
    *moves = move;

    return(table->keysZ);

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

} /* end of zdd_group_move */


static int
zdd_group_move_backward(
  DdManager * table,
  int  x,
  int  y)
{
    int        size;
    int        i, temp, gxtop, gxbot, gybot, yprev;

#ifdef DD_DEBUG
    assert(x < y);      /* we assume that x < y */
#endif
    /* Find top and bottom of the two groups. */
    gxtop = table->subtableZ[x].next;
    gxbot = x;
    gybot = table->subtableZ[y].next;
    while (table->subtableZ[gybot].next != (unsigned) y)
        gybot = table->subtableZ[gybot].next;
    yprev = gybot;

    while (x <= y) {
        while (y > gxtop) {
            /* Set correct symmetries. */
            temp = table->subtableZ[x].next;
            if (temp == x)
                temp = y;
            i = gxtop;
            for (;;) {
                if (table->subtableZ[i].next == (unsigned) x) {
                    table->subtableZ[i].next = y;
                    break;
                } else {
                    i = table->subtableZ[i].next;
                }
            }
            if (table->subtableZ[y].next != (unsigned) y) {
                table->subtableZ[x].next = table->subtableZ[y].next;
            } else {
                table->subtableZ[x].next = x;
            }

            if (yprev != y) {
                table->subtableZ[yprev].next = x;
            } else {
                yprev = x;
            }
            table->subtableZ[y].next = temp;

            size = cuddZddSwapInPlace(table, x, y);
            if (size == 0)
                return(0);
            y = x;
            x--;
        } /* while y > gxtop */

        /* Trying to find the next y. */
        if (table->subtableZ[y].next <= (unsigned) y) {
            gybot = y;
        } else {
            y = table->subtableZ[y].next;
        }

        yprev = gxtop;
        gxtop++;
        gxbot++;
        x = gxbot;
    } /* while x <= y, end of group movement backward */

    return(size);

} /* end of zdd_group_move_backward */


static void
cuddZddSymmSummary(
  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->subtableZ[i].next != (unsigned) i) {
            TotalSymmGroups++;
            x = i;
            do {
                TotalSymm++;
                gbot = x;
                x = table->subtableZ[x].next;
            } while (x != i);
#ifdef DD_DEBUG
            assert(table->subtableZ[gbot].next == (unsigned) i);
#endif
            i = gbot;
        }
    }
    *symvars = TotalSymm;
    *symgroups = TotalSymmGroups;

    return;

} /* end of cuddZddSymmSummary */

---