Version abc71001

1 files changed, 2090 insertions, 0 deletions

diff --git a/src/bdd/cudd/cuddReorder.c b/src/bdd/cudd/cuddReorder.c
new file mode 100644
index 00000000..1387196f
--- /dev/null
+++ b/src/bdd/cudd/cuddReorder.c
@@ -0,0 +1,2090 @@
+/**CFile***********************************************************************
+
+  FileName    [cuddReorder.c]
+
+  PackageName [cudd]
+
+  Synopsis    [Functions for dynamic variable reordering.]
+
+  Description [External procedures included in this file:
+        <ul>
+        <li> Cudd_ReduceHeap()
+        <li> Cudd_ShuffleHeap()
+        </ul>
+    Internal procedures included in this module:
+        <ul>
+        <li> cuddDynamicAllocNode()
+        <li> cuddSifting()
+        <li> cuddSwapping()
+        <li> cuddNextHigh()
+        <li> cuddNextLow()
+        <li> cuddSwapInPlace()
+        <li> cuddBddAlignToZdd()
+        </ul>
+    Static procedures included in this module:
+        <ul>
+        <li> ddUniqueCompare()
+        <li> ddSwapAny()
+        <li> ddSiftingAux()
+        <li> ddSiftingUp()
+        <li> ddSiftingDown()
+        <li> ddSiftingBackward()
+        <li> ddReorderPreprocess()
+        <li> ddReorderPostprocess()
+        <li> ddShuffle()
+        <li> ddSiftUp()
+        <li> bddFixTree()
+        </ul>]
+
+  Author      [Shipra Panda, Bernard Plessier, Fabio Somenzi]
+
+  Copyright   [This file was created at the University of Colorado at
+  Boulder.  The University of Colorado at Boulder makes no warranty
+  about the suitability of this software for any purpose.  It is
+  presented on an AS IS basis.]
+
+******************************************************************************/
+
+#include "util_hack.h"
+#include "cuddInt.h"
+
+/*---------------------------------------------------------------------------*/
+/* Constant declarations                                                     */
+/*---------------------------------------------------------------------------*/
+
+#define DD_MAX_SUBTABLE_SPARSITY 8
+#define DD_SHRINK_FACTOR 2
+
+/*---------------------------------------------------------------------------*/
+/* Stucture declarations                                                     */
+/*---------------------------------------------------------------------------*/
+
+/*---------------------------------------------------------------------------*/
+/* Type declarations                                                         */
+/*---------------------------------------------------------------------------*/
+
+/*---------------------------------------------------------------------------*/
+/* Variable declarations                                                     */
+/*---------------------------------------------------------------------------*/
+
+#ifndef lint
+static char rcsid[] DD_UNUSED = "$Id: cuddReorder.c,v 1.1.1.1 2003/02/24 22:23:53 wjiang Exp $";
+#endif
+
+static    int    *entry;
+
+int    ddTotalNumberSwapping;
+#ifdef DD_STATS
+int    ddTotalNISwaps;
+#endif
+
+/*---------------------------------------------------------------------------*/
+/* Macro declarations                                                        */
+/*---------------------------------------------------------------------------*/
+
+/**AutomaticStart*************************************************************/
+
+/*---------------------------------------------------------------------------*/
+/* Static function prototypes                                                */
+/*---------------------------------------------------------------------------*/
+
+static int ddUniqueCompare ARGS((int *ptrX, int *ptrY));
+static Move * ddSwapAny ARGS((DdManager *table, int x, int y));
+static int ddSiftingAux ARGS((DdManager *table, int x, int xLow, int xHigh));
+static Move * ddSiftingUp ARGS((DdManager *table, int y, int xLow));
+static Move * ddSiftingDown ARGS((DdManager *table, int x, int xHigh));
+static int ddSiftingBackward ARGS((DdManager *table, int size, Move *moves));
+static int ddReorderPreprocess ARGS((DdManager *table));
+static int ddReorderPostprocess ARGS((DdManager *table));
+static int ddShuffle ARGS((DdManager *table, int *permutation));
+static int ddSiftUp ARGS((DdManager *table, int x, int xLow));
+static void bddFixTree ARGS((DdManager *table, MtrNode *treenode));
+static int ddUpdateMtrTree ARGS((DdManager *table, MtrNode *treenode, int *perm, int *invperm));
+static int ddCheckPermuation ARGS((DdManager *table, MtrNode *treenode, int *perm, int *invperm));
+
+/**AutomaticEnd***************************************************************/
+
+
+/*---------------------------------------------------------------------------*/
+/* Definition of exported functions                                          */
+/*---------------------------------------------------------------------------*/
+
+
+/**Function********************************************************************
+
+  Synopsis    [Main dynamic reordering routine.]
+
+  Description [Main dynamic reordering routine.
+  Calls one of the possible reordering procedures:
+  <ul>
+  <li>Swapping
+  <li>Sifting
+  <li>Symmetric Sifting
+  <li>Group Sifting
+  <li>Window Permutation
+  <li>Simulated Annealing
+  <li>Genetic Algorithm
+  <li>Dynamic Programming (exact)
+  </ul>
+
+  For sifting, symmetric sifting, group sifting, and window
+  permutation it is possible to request reordering to convergence.<p>
+
+  The core of all methods is the reordering procedure
+  cuddSwapInPlace() which swaps two adjacent variables and is based
+  on Rudell's paper.
+  Returns 1 in case of success; 0 otherwise. In the case of symmetric
+  sifting (with and without convergence) returns 1 plus the number of
+  symmetric variables, in case of success.]
+
+  SideEffects [Changes the variable order for all diagrams and clears
+  the cache.]
+
+******************************************************************************/
+int
+Cudd_ReduceHeap(
+  DdManager * table /* DD manager */,
+  Cudd_ReorderingType heuristic /* method used for reordering */,
+  int  minsize /* bound below which no reordering occurs */)
+{
+    DdHook *hook;
+    int    result;
+    unsigned int nextDyn;
+#ifdef DD_STATS
+    unsigned int initialSize;
+    unsigned int finalSize;
+#endif
+    long localTime;
+
+    /* Don't reorder if there are too many dead nodes. */
+    if (table->keys - table->dead < (unsigned) minsize)
+    return(1);
+
+    if (heuristic == CUDD_REORDER_SAME) {
+    heuristic = table->autoMethod;
+    }
+    if (heuristic == CUDD_REORDER_NONE) {
+    return(1);
+    }
+
+    /* This call to Cudd_ReduceHeap does initiate reordering. Therefore
+    ** we count it.
+    */
+    table->reorderings++;
+
+    localTime = util_cpu_time();
+
+    /* Run the hook functions. */
+    hook = table->preReorderingHook;
+    while (hook != NULL) {
+    int res = (hook->f)(table, "BDD", (void *)heuristic);
+    if (res == 0) return(0);
+    hook = hook->next;
+    }
+
+    if (!ddReorderPreprocess(table)) return(0);
+    ddTotalNumberSwapping = 0;
+    
+    if (table->keys > table->peakLiveNodes) {
+    table->peakLiveNodes = table->keys;
+    }
+#ifdef DD_STATS
+    initialSize = table->keys - table->isolated;
+    ddTotalNISwaps = 0;
+
+    switch(heuristic) {
+    case CUDD_REORDER_RANDOM:
+    case CUDD_REORDER_RANDOM_PIVOT:
+    (void) fprintf(table->out,"#:I_RANDOM  ");
+    break;
+    case CUDD_REORDER_SIFT:
+    case CUDD_REORDER_SIFT_CONVERGE:
+    case CUDD_REORDER_SYMM_SIFT:
+    case CUDD_REORDER_SYMM_SIFT_CONV:
+    case CUDD_REORDER_GROUP_SIFT:
+    case CUDD_REORDER_GROUP_SIFT_CONV:
+    (void) fprintf(table->out,"#:I_SIFTING ");
+    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:
+    (void) fprintf(table->out,"#:I_WINDOW  ");
+    break;
+    case CUDD_REORDER_ANNEALING:
+    (void) fprintf(table->out,"#:I_ANNEAL  ");
+    break;
+    case CUDD_REORDER_GENETIC:
+    (void) fprintf(table->out,"#:I_GENETIC ");
+    break;
+    case CUDD_REORDER_LINEAR:
+    case CUDD_REORDER_LINEAR_CONVERGE:
+    (void) fprintf(table->out,"#:I_LINSIFT ");
+    break;
+    case CUDD_REORDER_EXACT:
+    (void) fprintf(table->out,"#:I_EXACT   ");
+    break;
+    default:
+    return(0);
+    }
+    (void) fprintf(table->out,"%8d: initial size",initialSize); 
+#endif
+
+    /* See if we should use alternate threshold for maximum growth. */
+    if (table->reordCycle && table->reorderings % table->reordCycle == 0) {
+    double saveGrowth = table->maxGrowth;
+    table->maxGrowth = table->maxGrowthAlt;
+    result = cuddTreeSifting(table,heuristic);
+    table->maxGrowth = saveGrowth;
+    } else {
+    result = cuddTreeSifting(table,heuristic);
+    }
+
+#ifdef DD_STATS
+    (void) fprintf(table->out,"\n");
+    finalSize = table->keys - table->isolated;
+    (void) fprintf(table->out,"#:F_REORDER %8d: final size\n",finalSize); 
+    (void) fprintf(table->out,"#:T_REORDER %8g: total time (sec)\n",
+           ((double)(util_cpu_time() - localTime)/1000.0)); 
+    (void) fprintf(table->out,"#:N_REORDER %8d: total swaps\n",
+           ddTotalNumberSwapping);
+    (void) fprintf(table->out,"#:M_REORDER %8d: NI swaps\n",ddTotalNISwaps);
+#endif
+
+    if (result == 0)
+    return(0);
+
+    if (!ddReorderPostprocess(table))
+    return(0);
+
+    if (table->realign) {
+    if (!cuddZddAlignToBdd(table))
+        return(0);
+    }
+
+    nextDyn = (table->keys - table->constants.keys + 1) *
+          DD_DYN_RATIO + table->constants.keys;
+    if (table->reorderings < 20 || nextDyn > table->nextDyn)
+    table->nextDyn = nextDyn;
+    else
+    table->nextDyn += 20;
+    table->reordered = 1;
+
+    /* Run hook functions. */
+    hook = table->postReorderingHook;
+    while (hook != NULL) {
+    int res = (hook->f)(table, "BDD", (void *)localTime);
+    if (res == 0) return(0);
+    hook = hook->next;
+    }
+    /* Update cumulative reordering time. */
+    table->reordTime += util_cpu_time() - localTime;
+
+    return(result);
+
+} /* end of Cudd_ReduceHeap */
+
+
+/**Function********************************************************************
+
+  Synopsis    [Reorders variables according to given permutation.]
+
+  Description [Reorders variables according to given permutation.
+  The i-th entry of the permutation array contains the index of the variable
+  that should be brought to the i-th level.  The size of the array should be
+  equal or greater to the number of variables currently in use.
+  Returns 1 in case of success; 0 otherwise.]
+
+  SideEffects [Changes the variable order for all diagrams and clears
+  the cache.]
+
+  SeeAlso [Cudd_ReduceHeap]
+
+******************************************************************************/
+int
+Cudd_ShuffleHeap(
+  DdManager * table /* DD manager */,
+  int * permutation /* required variable permutation */)
+{
+
+    int    result;
+    int i;
+    int identity = 1;
+    int *perm;
+
+    /* Don't waste time in case of identity permutation. */
+    for (i = 0; i < table->size; i++) {
+    if (permutation[i] != table->invperm[i]) {
+        identity = 0;
+        break;
+    }
+    }
+    if (identity == 1) {
+    return(1);
+    }
+    if (!ddReorderPreprocess(table)) return(0);
+    if (table->keys > table->peakLiveNodes) {
+    table->peakLiveNodes = table->keys;
+    }
+
+    perm = ALLOC(int, table->size);
+    for (i = 0; i < table->size; i++)
+    perm[permutation[i]] = i;
+    if (!ddCheckPermuation(table,table->tree,perm,permutation)) {
+    FREE(perm);
+    return(0);
+    }
+    if (!ddUpdateMtrTree(table,table->tree,perm,permutation)) {
+    FREE(perm);
+    return(0);
+    }
+    FREE(perm);
+
+    result = ddShuffle(table,permutation);
+
+    if (!ddReorderPostprocess(table)) return(0);
+
+    return(result);
+
+} /* end of Cudd_ShuffleHeap */
+
+
+/*---------------------------------------------------------------------------*/
+/* Definition of internal functions                                          */
+/*---------------------------------------------------------------------------*/
+
+
+/**Function********************************************************************
+
+  Synopsis    [Dynamically allocates a Node.]
+
+  Description [Dynamically allocates a Node. This procedure is similar
+  to cuddAllocNode in Cudd_Table.c, but it does not attempt garbage
+  collection, because during reordering there are no dead nodes.
+  Returns a pointer to a new node if successful; NULL is memory is
+  full.]
+
+  SideEffects [None]
+
+  SeeAlso     [cuddAllocNode]
+
+******************************************************************************/
+DdNode *
+cuddDynamicAllocNode(
+  DdManager * table)
+{
+    int     i;
+    DdNodePtr *mem;
+    DdNode *list, *node;
+    extern void (*MMoutOfMemory)(long);
+    void (*saveHandler)(long);
+
+    if (table->nextFree == NULL) {        /* free list is empty */
+    /* Try to allocate a new block. */
+    saveHandler = MMoutOfMemory;
+    MMoutOfMemory = Cudd_OutOfMem;
+    mem = (DdNodePtr *) ALLOC(DdNode, DD_MEM_CHUNK + 1);
+    MMoutOfMemory = saveHandler;
+    if (mem == NULL && table->stash != NULL) {
+        FREE(table->stash);
+        table->stash = NULL;
+        /* Inhibit resizing of tables. */
+        table->maxCacheHard = table->cacheSlots - 1;
+        table->cacheSlack = -(table->cacheSlots + 1);
+        for (i = 0; i < table->size; i++) {
+        table->subtables[i].maxKeys <<= 2;
+        }
+        mem = (DdNodePtr *) ALLOC(DdNode,DD_MEM_CHUNK + 1);
+    }
+    if (mem == NULL) {
+        /* Out of luck. Call the default handler to do
+        ** whatever it specifies for a failed malloc.  If this
+        ** handler returns, then set error code, print
+        ** warning, and return. */
+        (*MMoutOfMemory)(sizeof(DdNode)*(DD_MEM_CHUNK + 1));
+        table->errorCode = CUDD_MEMORY_OUT;
+#ifdef DD_VERBOSE
+        (void) fprintf(table->err,
+               "cuddDynamicAllocNode: out of memory");
+        (void) fprintf(table->err,"Memory in use = %ld\n",
+               table->memused);
+#endif
+        return(NULL);
+    } else {    /* successful allocation; slice memory */
+        unsigned long offset;
+        table->memused += (DD_MEM_CHUNK + 1) * sizeof(DdNode);
+        mem[0] = (DdNode *) table->memoryList;
+        table->memoryList = mem;
+
+        /* Here we rely on the fact that the size of a DdNode is a
+        ** power of 2 and a multiple of the size of a pointer.
+        ** If we align one node, all the others will be aligned
+        ** as well. */
+        offset = (unsigned long) mem & (sizeof(DdNode) - 1);
+        mem += (sizeof(DdNode) - offset) / sizeof(DdNodePtr);
+#ifdef DD_DEBUG
+        assert(((unsigned long) mem & (sizeof(DdNode) - 1)) == 0);
+#endif
+        list = (DdNode *) mem;
+
+        i = 1;
+        do {
+        list[i - 1].next = &list[i];
+        } while (++i < DD_MEM_CHUNK);
+
+        list[DD_MEM_CHUNK - 1].next = NULL;
+
+        table->nextFree = &list[0];
+    }
+    } /* if free list empty */
+
+    node = table->nextFree;
+    table->nextFree = node->next;
+    return (node);
+
+} /* end of cuddDynamicAllocNode */
+
+
+/**Function********************************************************************
+
+  Synopsis    [Implementation of Rudell's sifting algorithm.]
+
+  Description [Implementation of Rudell's sifting algorithm.
+  Assumes that no dead nodes are present.
+    <ol>
+    <li> Order all the variables according to the number of entries
+    in each unique table.
+    <li> Sift the variable up and down, remembering each time the
+    total size of the DD heap.
+    <li> Select the best permutation.
+    <li> Repeat 3 and 4 for all variables.
+    </ol>
+  Returns 1 if successful; 0 otherwise.]
+
+  SideEffects [None]
+
+******************************************************************************/
+int
+cuddSifting(
+  DdManager * table,
+  int  lower,
+  int  upper)
+{
+    int    i;
+    int    *var;
+    int    size;
+    int    x;
+    int    result;
+#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 cuddSiftingOutOfMem;
+    }
+    var = ALLOC(int,size);
+    if (var == NULL) {
+    table->errorCode = CUDD_MEMORY_OUT;
+    goto cuddSiftingOutOfMem;
+    }
+
+    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),(int (*)(const void *, const void *))ddUniqueCompare);
+
+    /* Now sift. */
+    for (i = 0; i < ddMin(table->siftMaxVar,size); i++) {
+    if (ddTotalNumberSwapping >= table->siftMaxSwap)
+        break;
+    x = table->perm[var[i]];
+    
+    if (x < lower || x > upper || table->subtables[x].bindVar == 1) 
+        continue;
+#ifdef DD_STATS
+    previousSize = table->keys - table->isolated;
+#endif
+    result = ddSiftingAux(table, x, lower, upper);
+    if (!result) goto cuddSiftingOutOfMem;
+#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 */
+        (void) fprintf(table->err,"\nSize increased from %d to %d while sifting variable %d\n", previousSize, table->keys - table->isolated, var[i]);
+    } else {
+        (void) fprintf(table->out,"=");
+    }
+    fflush(table->out);
+#endif
+    }
+
+    FREE(var);
+    FREE(entry);
+
+    return(1);
+
+cuddSiftingOutOfMem:
+
+    if (entry != NULL) FREE(entry);
+    if (var != NULL) FREE(var);
+
+    return(0); 
+
+} /* end of cuddSifting */
+
+
+/**Function********************************************************************
+
+  Synopsis    [Reorders variables by a sequence of (non-adjacent) swaps.]
+
+  Description [Implementation of Plessier's algorithm that reorders
+  variables by a sequence of (non-adjacent) swaps.
+    <ol>
+    <li> Select two variables (RANDOM or HEURISTIC).
+    <li> Permute these variables.
+    <li> If the nodes have decreased accept the permutation.
+    <li> Otherwise reconstruct the original heap.
+    <li> Loop.
+    </ol>
+  Returns 1 in case of success; 0 otherwise.]
+
+  SideEffects [None]
+
+******************************************************************************/
+int
+cuddSwapping(
+  DdManager * table,
+  int lower,
+  int upper,
+  Cudd_ReorderingType heuristic)
+{
+    int    i, j;
+    int    max, keys;
+    int    nvars;
+    int    x, y;
+    int    iterate;
+    int previousSize;
+    Move *moves, *move;
+    int    pivot;
+    int    modulo;
+    int result;
+
+#ifdef DD_DEBUG
+    /* Sanity check */
+    assert(lower >= 0 && upper < table->size && lower <= upper);
+#endif
+
+    nvars = upper - lower + 1;
+    iterate = nvars;
+
+    for (i = 0; i < iterate; i++) {
+    if (ddTotalNumberSwapping >= table->siftMaxSwap)
+        break;
+    if (heuristic == CUDD_REORDER_RANDOM_PIVOT) {
+        max = -1;
+        for (j = lower; j <= upper; j++) {
+        if ((keys = table->subtables[j].keys) > max) {
+            max = keys;
+            pivot = j;
+        }
+        }
+
+        modulo = upper - pivot;
+        if (modulo == 0) {
+        y = pivot;
+        } else{
+        y = pivot + 1 + ((int) Cudd_Random() % modulo);
+        }
+
+        modulo = pivot - lower - 1;
+        if (modulo < 1) {
+        x = lower;
+        } else{
+        do {
+            x = (int) Cudd_Random() % modulo;
+        } while (x == y);
+        }
+    } else {
+        x = ((int) Cudd_Random() % nvars) + lower;
+        do {
+        y = ((int) Cudd_Random() % nvars) + lower;
+        } while (x == y);
+    }
+    previousSize = table->keys - table->isolated;
+    moves = ddSwapAny(table,x,y);
+    if (moves == NULL) goto cuddSwappingOutOfMem;
+    result = ddSiftingBackward(table,previousSize,moves);
+    if (!result) goto cuddSwappingOutOfMem;
+    while (moves != NULL) {
+        move = moves->next;
+        cuddDeallocNode(table, (DdNode *) moves);
+        moves = move;
+    }
+#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
+#if 0
+    (void) fprintf(table->out,"#:t_SWAPPING %8d: tmp size\n",
+               table->keys - table->isolated); 
+#endif
+    }
+
+    return(1);
+
+cuddSwappingOutOfMem:
+    while (moves != NULL) {
+    move = moves->next;
+    cuddDeallocNode(table, (DdNode *) moves);
+    moves = move;
+    }
+
+    return(0);
+
+} /* end of cuddSwapping */
+
+
+/**Function********************************************************************
+
+  Synopsis    [Finds the next subtable with a larger index.]
+
+  Description [Finds the next subtable with a larger index. Returns the
+  index.]
+
+  SideEffects [None]
+
+  SeeAlso     [cuddNextLow]
+
+******************************************************************************/
+int
+cuddNextHigh(
+  DdManager * table,
+  int  x)
+{
+    return(x+1);
+
+} /* end of cuddNextHigh */
+    
+
+/**Function********************************************************************
+
+  Synopsis    [Finds the next subtable with a smaller index.]
+
+  Description [Finds the next subtable with a smaller index. Returns the
+  index.]
+
+  SideEffects [None]
+
+  SeeAlso     [cuddNextHigh]
+
+******************************************************************************/
+int
+cuddNextLow(
+  DdManager * table,
+  int  x)
+{
+    return(x-1);
+
+} /* end of cuddNextLow */
+
+
+/**Function********************************************************************
+
+  Synopsis    [Swaps two adjacent variables.]
+
+  Description [Swaps two adjacent variables. It assumes that no dead
+  nodes are present on entry to this procedure.  The procedure then
+  guarantees that no dead nodes will be present when it terminates.
+  cuddSwapInPlace assumes that x &lt; y.  Returns the number of keys in
+  the table if successful; 0 otherwise.]
+
+  SideEffects [None]
+
+******************************************************************************/
+int
+cuddSwapInPlace(
+  DdManager * table,
+  int  x,
+  int  y)
+{
+    DdNodePtr *xlist, *ylist;
+    int    xindex, yindex;
+    int    xslots, yslots;
+    int    xshift, yshift;
+    int    oldxkeys, oldykeys;
+    int    newxkeys, newykeys;
+    int    comple, newcomplement;
+    int    i;
+    Cudd_VariableType varType;
+    Cudd_LazyGroupType groupType;
+    int    posn;
+    int    isolated;
+    DdNode *f,*f0,*f1,*f01,*f00,*f11,*f10,*newf1,*newf0;
+    DdNode *g,*next;
+    DdNodePtr *previousP;
+    DdNode *tmp;
+    DdNode *sentinel = &(table->sentinel);
+    extern void (*MMoutOfMemory)(long);
+    void (*saveHandler)(long);
+
+#if DD_DEBUG
+    int    count,idcheck;
+#endif
+
+#ifdef DD_DEBUG
+    assert(x < y);
+    assert(cuddNextHigh(table,x) == y);
+    assert(table->subtables[x].keys != 0);
+    assert(table->subtables[y].keys != 0);
+    assert(table->subtables[x].dead == 0);
+    assert(table->subtables[y].dead == 0);
+#endif
+
+    ddTotalNumberSwapping++;
+
+    /* Get parameters of x subtable. */
+    xindex = table->invperm[x];
+    xlist = table->subtables[x].nodelist; 
+    oldxkeys = table->subtables[x].keys;
+    xslots = table->subtables[x].slots;
+    xshift = table->subtables[x].shift;
+
+    /* Get parameters of y subtable. */
+    yindex = table->invperm[y];
+    ylist = table->subtables[y].nodelist;
+    oldykeys = table->subtables[y].keys;
+    yslots = table->subtables[y].slots;
+    yshift = table->subtables[y].shift;
+
+    if (!cuddTestInteract(table,xindex,yindex)) {
+#ifdef DD_STATS
+    ddTotalNISwaps++;
+#endif
+    newxkeys = oldxkeys;
+    newykeys = oldykeys;
+    } else {
+    newxkeys = 0;
+    newykeys = oldykeys;
+
+    /* Check whether the two projection functions involved in this
+    ** swap are isolated. At the end, we'll be able to tell how many
+    ** isolated projection functions are there by checking only these
+    ** two functions again. This is done to eliminate the isolated
+    ** projection functions from the node count.
+    */
+    isolated = - ((table->vars[xindex]->ref == 1) +
+             (table->vars[yindex]->ref == 1));
+
+    /* The nodes in the x layer that do not depend on
+    ** y will stay there; the others are put in a chain.
+    ** The chain is handled as a LIFO; g points to the beginning.
+    */
+    g = NULL;
+    if ((oldxkeys >= xslots || (unsigned) xslots == table->initSlots) &&
+        oldxkeys <= DD_MAX_SUBTABLE_DENSITY * xslots) {
+        for (i = 0; i < xslots; i++) {
+        previousP = &(xlist[i]);
+        f = *previousP;
+        while (f != sentinel) {
+            next = f->next;
+            f1 = cuddT(f); f0 = cuddE(f);
+            if (f1->index != (DdHalfWord) yindex &&
+            Cudd_Regular(f0)->index != (DdHalfWord) yindex) {
+            /* stays */
+            newxkeys++;
+            *previousP = f;
+            previousP = &(f->next);
+            } else {
+            f->index = yindex;
+            f->next = g;
+            g = f;
+            }
+            f = next;
+        } /* while there are elements in the collision chain */
+        *previousP = sentinel;
+        } /* for each slot of the x subtable */
+    } else {        /* resize xlist */
+        DdNode *h = NULL;
+        DdNodePtr *newxlist;
+        unsigned int newxslots;
+        int newxshift;
+        /* Empty current xlist. Nodes that stay go to list h;
+        ** nodes that move go to list g. */
+        for (i = 0; i < xslots; i++) {
+        f = xlist[i];
+        while (f != sentinel) {
+            next = f->next;
+            f1 = cuddT(f); f0 = cuddE(f);
+            if (f1->index != (DdHalfWord) yindex &&
+            Cudd_Regular(f0)->index != (DdHalfWord) yindex) {
+            /* stays */
+            f->next = h;
+            h = f;
+            newxkeys++;
+            } else {
+            f->index = yindex;
+            f->next = g;
+            g = f;
+            }
+            f = next;
+        } /* while there are elements in the collision chain */
+        } /* for each slot of the x subtable */
+        /* Decide size of new subtable. */
+        if (oldxkeys > DD_MAX_SUBTABLE_DENSITY * xslots) {
+        newxshift = xshift - 1;
+        newxslots = xslots << 1;
+        } else {
+        newxshift = xshift + 1;
+        newxslots = xslots >> 1;
+        }
+        /* Try to allocate new table. Be ready to back off. */
+        saveHandler = MMoutOfMemory;
+        MMoutOfMemory = Cudd_OutOfMem;
+        newxlist = ALLOC(DdNodePtr, newxslots);
+        MMoutOfMemory = saveHandler;
+        if (newxlist == NULL) {
+        (void) fprintf(table->err, "Unable to resize subtable %d for lack of memory\n", i);
+        newxlist = xlist;
+        newxslots = xslots;
+        newxshift = xshift;
+        } else {
+        table->slots += (newxslots - xslots);
+        table->minDead = (unsigned)
+            (table->gcFrac * (double) table->slots);
+        table->cacheSlack = (int)
+            ddMin(table->maxCacheHard, DD_MAX_CACHE_TO_SLOTS_RATIO
+              * table->slots) - 2 * (int) table->cacheSlots;
+        table->memused += (newxslots - xslots) * sizeof(DdNodePtr);
+        FREE(xlist);
+        xslots =  newxslots;
+        xshift = newxshift;
+        xlist = newxlist;
+        }
+        /* Initialize new subtable. */
+        for (i = 0; i < xslots; i++) {
+        xlist[i] = sentinel;
+        }
+        /* Move nodes that were parked in list h to their new home. */
+        f = h;
+        while (f != NULL) {
+        next = f->next;
+        f1 = cuddT(f);
+        f0 = cuddE(f);
+        /* Check xlist for pair (f11,f01). */
+        posn = ddHash(f1, f0, xshift);
+        /* For each element tmp in collision list xlist[posn]. */
+        previousP = &(xlist[posn]);
+        tmp = *previousP;
+        while (f1 < cuddT(tmp)) {
+            previousP = &(tmp->next);
+            tmp = *previousP;
+        }
+        while (f1 == cuddT(tmp) && f0 < cuddE(tmp)) {
+            previousP = &(tmp->next);
+            tmp = *previousP;
+        }
+        f->next = *previousP;
+        *previousP = f;
+        f = next;
+        }
+    }
+
+#ifdef DD_COUNT
+    table->swapSteps += oldxkeys - newxkeys;
+#endif
+    /* Take care of the x nodes that must be re-expressed.
+    ** They form a linked list pointed by g. Their index has been
+    ** already changed to yindex.
+    */
+    f = g;
+    while (f != NULL) {
+        next = f->next;
+        /* Find f1, f0, f11, f10, f01, f00. */
+        f1 = cuddT(f);
+#ifdef DD_DEBUG
+        assert(!(Cudd_IsComplement(f1)));
+#endif
+        if ((int) f1->index == yindex) {
+        f11 = cuddT(f1); f10 = cuddE(f1);
+        } else {
+        f11 = f10 = f1;
+        }
+#ifdef DD_DEBUG
+        assert(!(Cudd_IsComplement(f11)));
+#endif
+        f0 = cuddE(f);
+        comple = Cudd_IsComplement(f0);
+        f0 = Cudd_Regular(f0);
+        if ((int) f0->index == yindex) {
+        f01 = cuddT(f0); f00 = cuddE(f0);
+        } else {
+        f01 = f00 = f0;
+        }
+        if (comple) {
+        f01 = Cudd_Not(f01);
+        f00 = Cudd_Not(f00);
+        }
+        /* Decrease ref count of f1. */
+        cuddSatDec(f1->ref);
+        /* Create the new T child. */
+        if (f11 == f01) {
+        newf1 = f11;
+        cuddSatInc(newf1->ref);
+        } else {
+        /* Check xlist for triple (xindex,f11,f01). */
+        posn = ddHash(f11, f01, xshift);
+        /* For each element newf1 in collision list xlist[posn]. */
+        previousP = &(xlist[posn]);
+        newf1 = *previousP;
+        while (f11 < cuddT(newf1)) {
+            previousP = &(newf1->next);
+            newf1 = *previousP;
+        }
+        while (f11 == cuddT(newf1) && f01 < cuddE(newf1)) {
+            previousP = &(newf1->next);
+            newf1 = *previousP;
+        }
+        if (cuddT(newf1) == f11 && cuddE(newf1) == f01) {
+            cuddSatInc(newf1->ref);
+        } else { /* no match */
+            newf1 = cuddDynamicAllocNode(table);
+            if (newf1 == NULL)
+            goto cuddSwapOutOfMem;
+            newf1->index = xindex; newf1->ref = 1;
+            cuddT(newf1) = f11;
+            cuddE(newf1) = f01;
+            /* Insert newf1 in the collision list xlist[posn];
+            ** increase the ref counts of f11 and f01.
+            */
+            newxkeys++;
+            newf1->next = *previousP;
+            *previousP = newf1;
+            cuddSatInc(f11->ref);
+            tmp = Cudd_Regular(f01);
+            cuddSatInc(tmp->ref);
+        }
+        }
+        cuddT(f) = newf1;
+#ifdef DD_DEBUG
+        assert(!(Cudd_IsComplement(newf1)));
+#endif
+
+        /* Do the same for f0, keeping complement dots into account. */
+        /* Decrease ref count of f0. */
+        tmp = Cudd_Regular(f0);
+        cuddSatDec(tmp->ref);
+        /* Create the new E child. */
+        if (f10 == f00) {
+        newf0 = f00;
+        tmp = Cudd_Regular(newf0);
+        cuddSatInc(tmp->ref); 
+        } else {
+        /* make sure f10 is regular */
+        newcomplement = Cudd_IsComplement(f10);
+        if (newcomplement) {
+            f10 = Cudd_Not(f10);
+            f00 = Cudd_Not(f00);
+        }
+        /* Check xlist for triple (xindex,f10,f00). */
+        posn = ddHash(f10, f00, xshift);
+        /* For each element newf0 in collision list xlist[posn]. */
+        previousP = &(xlist[posn]);
+        newf0 = *previousP;
+        while (f10 < cuddT(newf0)) {
+            previousP = &(newf0->next);
+            newf0 = *previousP;
+        }
+        while (f10 == cuddT(newf0) && f00 < cuddE(newf0)) {
+            previousP = &(newf0->next);
+            newf0 = *previousP;
+        }
+        if (cuddT(newf0) == f10 && cuddE(newf0) == f00) {
+            cuddSatInc(newf0->ref); 
+        } else { /* no match */
+            newf0 = cuddDynamicAllocNode(table);
+            if (newf0 == NULL)
+            goto cuddSwapOutOfMem;
+            newf0->index = xindex; newf0->ref = 1;
+            cuddT(newf0) = f10;
+            cuddE(newf0) = f00;
+            /* Insert newf0 in the collision list xlist[posn];
+            ** increase the ref counts of f10 and f00.
+            */
+            newxkeys++;
+            newf0->next = *previousP;
+            *previousP = newf0;
+            cuddSatInc(f10->ref);
+            tmp = Cudd_Regular(f00);
+            cuddSatInc(tmp->ref);
+        }
+        if (newcomplement) {
+            newf0 = Cudd_Not(newf0);
+        }
+        }
+        cuddE(f) = newf0;
+
+        /* Insert the modified f in ylist.
+        ** The modified f does not already exists in ylist.
+        ** (Because of the uniqueness of the cofactors.)
+        */
+        posn = ddHash(newf1, newf0, yshift);
+        newykeys++;
+        previousP = &(ylist[posn]);
+        tmp = *previousP;
+        while (newf1 < cuddT(tmp)) {
+        previousP = &(tmp->next);
+        tmp = *previousP;
+        }
+        while (newf1 == cuddT(tmp) && newf0 < cuddE(tmp)) {
+        previousP = &(tmp->next);
+        tmp = *previousP;
+        }
+        f->next = *previousP;
+        *previousP = f;
+        f = next;
+    } /* while f != NULL */
+
+    /* GC the y layer. */
+
+    /* For each node f in ylist. */
+    for (i = 0; i < yslots; i++) {
+        previousP = &(ylist[i]);
+        f = *previousP;
+        while (f != sentinel) {
+        next = f->next;
+        if (f->ref == 0) {
+            tmp = cuddT(f);
+            cuddSatDec(tmp->ref);
+            tmp = Cudd_Regular(cuddE(f));
+            cuddSatDec(tmp->ref);
+            cuddDeallocNode(table,f);
+            newykeys--;
+        } else {
+            *previousP = f;
+            previousP = &(f->next);
+        }
+        f = next;
+        } /* while f */
+        *previousP = sentinel;
+    } /* for i */
+
+#if DD_DEBUG
+#if 0
+    (void) fprintf(table->out,"Swapping %d and %d\n",x,y);
+#endif
+    count = 0;
+    idcheck = 0;
+    for (i = 0; i < yslots; i++) {
+        f = ylist[i];
+        while (f != sentinel) {
+        count++;
+        if (f->index != (DdHalfWord) yindex)
+            idcheck++;
+        f = f->next;
+        }
+    }
+    if (count != newykeys) {
+        (void) fprintf(table->out,
+               "Error in finding newykeys\toldykeys = %d\tnewykeys = %d\tactual = %d\n",
+               oldykeys,newykeys,count);
+    }
+    if (idcheck != 0)
+        (void) fprintf(table->out,
+               "Error in id's of ylist\twrong id's = %d\n",
+               idcheck);
+    count = 0;
+    idcheck = 0;
+    for (i = 0; i < xslots; i++) {
+        f = xlist[i];
+        while (f != sentinel) {
+        count++;
+        if (f->index != (DdHalfWord) xindex)
+            idcheck++;
+        f = f->next;
+        }
+    }
+    if (count != newxkeys) {
+        (void) fprintf(table->out,
+               "Error in finding newxkeys\toldxkeys = %d \tnewxkeys = %d \tactual = %d\n",
+               oldxkeys,newxkeys,count);
+    }
+    if (idcheck != 0)
+        (void) fprintf(table->out,
+               "Error in id's of xlist\twrong id's = %d\n",
+               idcheck);
+#endif
+
+    isolated += (table->vars[xindex]->ref == 1) +
+            (table->vars[yindex]->ref == 1);
+    table->isolated += isolated;
+    }
+
+    /* Set the appropriate fields in table. */
+    table->subtables[x].nodelist = ylist;
+    table->subtables[x].slots = yslots;
+    table->subtables[x].shift = yshift;
+    table->subtables[x].keys = newykeys;
+    table->subtables[x].maxKeys = yslots * DD_MAX_SUBTABLE_DENSITY;
+    i = table->subtables[x].bindVar;
+    table->subtables[x].bindVar = table->subtables[y].bindVar;
+    table->subtables[y].bindVar = i;
+    /* Adjust filds for lazy sifting. */
+    varType = table->subtables[x].varType;
+    table->subtables[x].varType = table->subtables[y].varType;
+    table->subtables[y].varType = varType;
+    i = table->subtables[x].pairIndex;
+    table->subtables[x].pairIndex = table->subtables[y].pairIndex;
+    table->subtables[y].pairIndex = i;
+    i = table->subtables[x].varHandled;
+    table->subtables[x].varHandled = table->subtables[y].varHandled;
+    table->subtables[y].varHandled = i;
+    groupType = table->subtables[x].varToBeGrouped;
+    table->subtables[x].varToBeGrouped = table->subtables[y].varToBeGrouped;
+    table->subtables[y].varToBeGrouped = groupType;
+
+    table->subtables[y].nodelist = xlist;
+    table->subtables[y].slots = xslots;
+    table->subtables[y].shift = xshift;
+    table->subtables[y].keys = newxkeys;
+    table->subtables[y].maxKeys = xslots * DD_MAX_SUBTABLE_DENSITY;
+
+    table->perm[xindex] = y; table->perm[yindex] = x;
+    table->invperm[x] = yindex; table->invperm[y] = xindex;
+
+    table->keys += newxkeys + newykeys - oldxkeys - oldykeys;
+
+    return(table->keys - table->isolated);
+
+cuddSwapOutOfMem:
+    (void) fprintf(table->err,"Error: cuddSwapInPlace out of memory\n");
+
+    return (0);
+
+} /* end of cuddSwapInPlace */
+
+
+/**Function********************************************************************
+
+  Synopsis    [Reorders BDD variables according to the order of the ZDD
+  variables.]
+
+  Description [Reorders BDD variables according to the order of the
+  ZDD variables. This function can be called at the end of ZDD
+  reordering to insure that the order of the BDD variables is
+  consistent with the order of the ZDD variables. The number of ZDD
+  variables must be a multiple of the number of BDD variables. Let
+  <code>M</code> be the ratio of the two numbers. cuddBddAlignToZdd
+  then considers the ZDD variables from <code>M*i</code> to
+  <code>(M+1)*i-1</code> as corresponding to BDD variable
+  <code>i</code>.  This function should be normally called from
+  Cudd_zddReduceHeap, which clears the cache.  Returns 1 in case of
+  success; 0 otherwise.]
+
+  SideEffects [Changes the BDD variable order for all diagrams and performs
+  garbage collection of the BDD unique table.]
+
+  SeeAlso [Cudd_ShuffleHeap Cudd_zddReduceHeap]
+
+******************************************************************************/
+int
+cuddBddAlignToZdd(
+  DdManager * table /* DD manager */)
+{
+    int *invperm;        /* permutation array */
+    int M;            /* ratio of ZDD variables to BDD variables */
+    int i;            /* loop index */
+    int result;            /* return value */
+
+    /* We assume that a ratio of 0 is OK. */
+    if (table->size == 0)
+    return(1);
+
+    M = table->sizeZ / table->size;
+    /* Check whether the number of ZDD variables is a multiple of the
+    ** number of BDD variables.
+    */
+    if (M * table->size != table->sizeZ)
+    return(0);
+    /* Create and initialize the inverse permutation array. */
+    invperm = ALLOC(int,table->size);
+    if (invperm == NULL) {
+    table->errorCode = CUDD_MEMORY_OUT;
+    return(0);
+    }
+    for (i = 0; i < table->sizeZ; i += M) {
+    int indexZ = table->invpermZ[i];
+    int index  = indexZ / M;
+    invperm[i / M] = index;
+    }
+    /* Eliminate dead nodes. Do not scan the cache again, because we
+    ** assume that Cudd_zddReduceHeap has already cleared it.
+    */
+    cuddGarbageCollect(table,0);
+
+    /* Initialize number of isolated projection functions. */
+    table->isolated = 0;
+    for (i = 0; i < table->size; i++) {
+    if (table->vars[i]->ref == 1) table->isolated++;
+    }
+
+    /* Initialize the interaction matrix. */
+    result = cuddInitInteract(table);
+    if (result == 0) return(0);
+
+    result = ddShuffle(table, invperm);
+    FREE(invperm);
+    /* Free interaction matrix. */
+    FREE(table->interact);
+    /* Fix the BDD variable group tree. */
+    bddFixTree(table,table->tree);
+    return(result);
+
+} /* end of cuddBddAlignToZdd */
+
+/*---------------------------------------------------------------------------*/
+/* Definition of static functions                                            */
+/*---------------------------------------------------------------------------*/
+
+
+/**Function********************************************************************
+
+  Synopsis    [Comparison function used by qsort.]
+
+  Description [Comparison function used by qsort to order the
+  variables according to the number of keys in the subtables.
+  Returns the difference in number of keys between the two
+  variables being compared.]
+
+  SideEffects [None]
+
+******************************************************************************/
+static int
+ddUniqueCompare(
+  int * ptrX,
+  int * ptrY)
+{
+#if 0
+    if (entry[*ptrY] == entry[*ptrX]) {
+    return((*ptrX) - (*ptrY));
+    }
+#endif
+    return(entry[*ptrY] - entry[*ptrX]);
+
+} /* end of ddUniqueCompare */
+
+
+/**Function********************************************************************
+
+  Synopsis    [Swaps any two variables.]
+
+  Description [Swaps any two variables. Returns the set of moves.]
+
+  SideEffects [None]
+
+******************************************************************************/
+static Move *
+ddSwapAny(
+  DdManager * table,
+  int  x,
+  int  y)
+{
+    Move    *move, *moves;
+    int        xRef,yRef;
+    int        xNext,yNext;
+    int        size;
+    int        limitSize;
+    int        tmp;
+
+    if (x >y) {
+    tmp = x; x = y; y = tmp;
+    }
+
+    xRef = x; yRef = y;
+
+    xNext = cuddNextHigh(table,x);
+    yNext = cuddNextLow(table,y);
+    moves = NULL;
+    limitSize = table->keys - table->isolated;
+
+    for (;;) {
+    if ( xNext == yNext) {
+        size = cuddSwapInPlace(table,x,xNext);
+        if (size == 0) goto ddSwapAnyOutOfMem;
+        move = (Move *) cuddDynamicAllocNode(table);            
+        if (move == NULL) goto ddSwapAnyOutOfMem;
+        move->x = x;
+        move->y = xNext;
+        move->size = size; 
+        move->next = moves;
+        moves = move;
+
+        size = cuddSwapInPlace(table,yNext,y);
+        if (size == 0) goto ddSwapAnyOutOfMem;
+        move = (Move *) cuddDynamicAllocNode(table);
+        if (move == NULL) goto ddSwapAnyOutOfMem;
+        move->x = yNext;
+        move->y = y;
+        move->size = size; 
+        move->next = moves;
+        moves = move;
+
+        size = cuddSwapInPlace(table,x,xNext);
+        if (size == 0) goto ddSwapAnyOutOfMem;
+        move = (Move *) cuddDynamicAllocNode(table);
+        if (move == NULL) goto ddSwapAnyOutOfMem;
+        move->x = x;
+        move->y = xNext;
+        move->size = size;
+        move->next = moves;
+        moves = move;
+
+        tmp = x; x = y; y = tmp;
+
+    } else if (x == yNext) {
+        
+        size = cuddSwapInPlace(table,x,xNext);
+        if (size == 0) goto ddSwapAnyOutOfMem;
+        move = (Move *) cuddDynamicAllocNode(table);
+        if (move == NULL) goto ddSwapAnyOutOfMem;
+        move->x = x;
+        move->y = xNext;
+        move->size = size;
+        move->next = moves;
+        moves = move;
+
+        tmp = x; x = y; y = tmp;
+
+    } else {
+        size = cuddSwapInPlace(table,x,xNext);
+        if (size == 0) goto ddSwapAnyOutOfMem;
+        move = (Move *) cuddDynamicAllocNode(table);
+        if (move == NULL) goto ddSwapAnyOutOfMem;
+        move->x = x;
+        move->y = xNext;
+        move->size = size; 
+        move->next = moves;
+        moves = move;
+
+        size = cuddSwapInPlace(table,yNext,y);
+        if (size == 0) goto ddSwapAnyOutOfMem;
+        move = (Move *) cuddDynamicAllocNode(table);
+        if (move == NULL) goto ddSwapAnyOutOfMem;
+        move->x = yNext;
+        move->y = y;
+        move->size = size;
+        move->next = moves;
+        moves = move;
+
+        x = xNext;
+        y = yNext;
+    }
+
+    xNext = cuddNextHigh(table,x);
+    yNext = cuddNextLow(table,y);
+    if (xNext > yRef) break;
+
+    if ((double) size > table->maxGrowth * (double) limitSize) break;
+    if (size < limitSize) limitSize = size;
+    }
+    if (yNext>=xRef) {
+    size = cuddSwapInPlace(table,yNext,y);
+    if (size == 0) goto ddSwapAnyOutOfMem;
+    move = (Move *) cuddDynamicAllocNode(table);
+    if (move == NULL) goto ddSwapAnyOutOfMem;
+    move->x = yNext;
+    move->y = y;
+    move->size = size; 
+    move->next = moves;
+    moves = move;
+    }
+
+    return(moves);
+    
+ddSwapAnyOutOfMem:
+    while (moves != NULL) {
+    move = moves->next;
+    cuddDeallocNode(table, (DdNode *) moves);
+    moves = move;
+    }
+    return(NULL);
+
+} /* end of ddSwapAny */
+
+
+/**Function********************************************************************
+
+  Synopsis    [Given xLow <= x <= xHigh moves x up and down between the
+  boundaries.]
+
+  Description [Given xLow <= x <= xHigh moves x up and down between the
+  boundaries. Finds the best position and does the required changes.
+  Returns 1 if successful; 0 otherwise.]
+
+  SideEffects [None]
+
+******************************************************************************/
+static int
+ddSiftingAux(
+  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;
+
+    initialSize = table->keys - table->isolated;
+
+    moveDown = NULL;
+    moveUp = NULL;
+
+    if (x == xLow) {
+    moveDown = ddSiftingDown(table,x,xHigh);
+    /* At this point x --> xHigh unless bounding occurred. */
+    if (moveDown == (Move *) CUDD_OUT_OF_MEM) goto ddSiftingAuxOutOfMem;
+    /* Move backward and stop at best position. */    
+    result = ddSiftingBackward(table,initialSize,moveDown);
+    if (!result) goto ddSiftingAuxOutOfMem;
+
+    } else if (x == xHigh) {
+    moveUp = ddSiftingUp(table,x,xLow);
+    /* At this point x --> xLow unless bounding occurred. */
+    if (moveUp == (Move *) CUDD_OUT_OF_MEM) goto ddSiftingAuxOutOfMem;
+    /* Move backward and stop at best position. */
+    result = ddSiftingBackward(table,initialSize,moveUp);
+    if (!result) goto ddSiftingAuxOutOfMem;
+
+    } else if ((x - xLow) > (xHigh - x)) { /* must go down first: shorter */
+    moveDown = ddSiftingDown(table,x,xHigh);
+    /* At this point x --> xHigh unless bounding occurred. */
+    if (moveDown == (Move *) CUDD_OUT_OF_MEM) goto ddSiftingAuxOutOfMem;
+    if (moveDown != NULL) {
+        x = moveDown->y;
+    }
+    moveUp = ddSiftingUp(table,x,xLow);
+    if (moveUp == (Move *) CUDD_OUT_OF_MEM) goto ddSiftingAuxOutOfMem;
+    /* Move backward and stop at best position */    
+    result = ddSiftingBackward(table,initialSize,moveUp);
+    if (!result) goto ddSiftingAuxOutOfMem;
+
+    } else { /* must go up first: shorter */
+    moveUp = ddSiftingUp(table,x,xLow);
+    /* At this point x --> xLow unless bounding occurred. */
+    if (moveUp == (Move *) CUDD_OUT_OF_MEM) goto ddSiftingAuxOutOfMem;
+    if (moveUp != NULL) {
+        x = moveUp->x;
+    }
+    moveDown = ddSiftingDown(table,x,xHigh);
+    if (moveDown == (Move *) CUDD_OUT_OF_MEM) goto ddSiftingAuxOutOfMem;
+    /* Move backward and stop at best position. */    
+    result = ddSiftingBackward(table,initialSize,moveDown);
+    if (!result) goto ddSiftingAuxOutOfMem;
+    }
+
+    while (moveDown != NULL) {
+    move = moveDown->next;
+    cuddDeallocNode(table, (DdNode *) moveDown);
+    moveDown = move;
+    }
+    while (moveUp != NULL) {
+    move = moveUp->next;
+    cuddDeallocNode(table, (DdNode *) moveUp);
+    moveUp = move;
+    }
+
+    return(1);
+
+ddSiftingAuxOutOfMem:
+    if (moveDown != (Move *) CUDD_OUT_OF_MEM) {
+    while (moveDown != NULL) {
+        move = moveDown->next;
+        cuddDeallocNode(table, (DdNode *) moveDown);
+        moveDown = move;
+    }
+    }
+    if (moveUp != (Move *) CUDD_OUT_OF_MEM) {
+    while (moveUp != NULL) {
+        move = moveUp->next;
+        cuddDeallocNode(table, (DdNode *) moveUp);
+        moveUp = move;
+    }
+    }
+
+    return(0);
+
+} /* end of ddSiftingAux */
+
+
+/**Function********************************************************************
+
+  Synopsis    [Sifts a variable up.]
+
+  Description [Sifts a variable up. Moves y up until either it reaches
+  the bound (xLow) or the size of the DD heap increases too much.
+  Returns the set of moves in case of success; NULL if memory is full.]
+
+  SideEffects [None]
+
+******************************************************************************/
+static Move *
+ddSiftingUp(
+  DdManager * table,
+  int  y,
+  int  xLow)
+{
+    Move    *moves;
+    Move    *move;
+    int        x;
+    int        size;
+    int        limitSize;
+    int        xindex, yindex;
+    int        isolated;
+    int        L;    /* lower bound on DD size */
+#ifdef DD_DEBUG
+    int checkL;
+    int z;
+    int zindex;
+#endif
+
+    moves = NULL;
+    yindex = table->invperm[y];
+
+    /* Initialize the lower bound.
+    ** The part of the DD below y 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;
+    for (x = xLow + 1; x < y; x++) {
+    xindex = table->invperm[x];
+    if (cuddTestInteract(table,xindex,yindex)) {
+        isolated = table->vars[xindex]->ref == 1;
+        L -= table->subtables[x].keys - isolated;
+    }
+    }
+    isolated = table->vars[yindex]->ref == 1;
+    L -= table->subtables[y].keys - isolated;
+
+    x = cuddNextLow(table,y);
+    while (x >= xLow && L <= limitSize) {
+    xindex = table->invperm[x];
+#ifdef DD_DEBUG
+    checkL = table->keys - table->isolated;
+    for (z = xLow + 1; z < y; z++) {
+        zindex = table->invperm[z];
+        if (cuddTestInteract(table,zindex,yindex)) {
+        isolated = table->vars[zindex]->ref == 1;
+        checkL -= table->subtables[z].keys - isolated;
+        }
+    }
+    isolated = table->vars[yindex]->ref == 1;
+    checkL -= table->subtables[y].keys - isolated;
+    assert(L == checkL);
+#endif
+    size = cuddSwapInPlace(table,x,y);
+    if (size == 0) goto ddSiftingUpOutOfMem;
+    /* 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 ddSiftingUpOutOfMem;
+    move->x = x;
+    move->y = y;
+    move->size = size;
+    move->next = moves;
+    moves = move;
+    if ((double) size > (double) limitSize * table->maxGrowth) break;
+    if (size < limitSize) limitSize = size;
+    y = x;
+    x = cuddNextLow(table,y);
+    }
+    return(moves);
+
+ddSiftingUpOutOfMem:
+    while (moves != NULL) {
+    move = moves->next;
+    cuddDeallocNode(table, (DdNode *) moves);
+    moves = move;
+    }
+    return((Move *) CUDD_OUT_OF_MEM);
+
+} /* end of ddSiftingUp */
+    
+
+/**Function********************************************************************
+
+  Synopsis    [Sifts a variable down.]
+
+  Description [Sifts a variable down. Moves x down until either it
+  reaches the bound (xHigh) or the size of the DD heap increases too
+  much. Returns the set of moves in case of success; NULL if memory is
+  full.]
+
+  SideEffects [None]
+
+******************************************************************************/
+static Move *
+ddSiftingDown(
+  DdManager * table,
+  int  x,
+  int  xHigh)
+{
+    Move    *moves;
+    Move    *move;
+    int        y;
+    int        size;
+    int        R;    /* upper bound on node decrease */
+    int        limitSize;
+    int        xindex, yindex;
+    int        isolated;
+#ifdef DD_DEBUG
+    int        checkR;
+    int        z;
+    int        zindex;
+#endif
+
+    moves = NULL;
+    /* Initialize R */
+    xindex = table->invperm[x];
+    limitSize = size = table->keys - table->isolated;
+    R = 0;
+    for (y = xHigh; y > x; y--) {
+    yindex = table->invperm[y];
+    if (cuddTestInteract(table,xindex,yindex)) {
+        isolated = table->vars[yindex]->ref == 1;
+        R += table->subtables[y].keys - isolated;
+    }
+    }
+
+    y = cuddNextHigh(table,x);
+    while (y <= xHigh && size - R < limitSize) {
+#ifdef DD_DEBUG
+    checkR = 0;
+    for (z = xHigh; z > x; z--) {
+        zindex = table->invperm[z];
+        if (cuddTestInteract(table,xindex,zindex)) {
+        isolated = table->vars[zindex]->ref == 1;
+        checkR += table->subtables[z].keys - isolated;
+        }
+    }
+    assert(R == checkR);
+#endif
+    /* 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);
+    if (size == 0) goto ddSiftingDownOutOfMem; 
+    move = (Move *) cuddDynamicAllocNode(table);
+    if (move == NULL) goto ddSiftingDownOutOfMem;
+    move->x = x;
+    move->y = y;
+    move->size = size;
+    move->next = moves;
+    moves = move;
+    if ((double) size > (double) limitSize * table->maxGrowth) break;
+    if (size < limitSize) limitSize = size;
+    x = y;
+    y = cuddNextHigh(table,x);
+    }
+    return(moves);
+
+ddSiftingDownOutOfMem:
+    while (moves != NULL) {
+    move = moves->next;
+    cuddDeallocNode(table, (DdNode *) moves);
+    moves = move;
+    }
+    return((Move *) CUDD_OUT_OF_MEM);
+
+} /* end of ddSiftingDown */
+
+
+/**Function********************************************************************
+
+  Synopsis    [Given a set of moves, returns the DD heap to the position
+  giving the minimum size.]
+
+  Description [Given a set of moves, returns the DD heap to the
+  position giving the minimum size. In case of ties, returns to the
+  closest position giving the minimum size. Returns 1 in case of
+  success; 0 otherwise.]
+
+  SideEffects [None]
+
+******************************************************************************/
+static int
+ddSiftingBackward(
+  DdManager * table,
+  int  size,
+  Move * moves)
+{
+    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);
+    res = cuddSwapInPlace(table,(int)move->x,(int)move->y);
+    if (!res) return(0);    
+    }
+
+    return(1);
+
+} /* end of ddSiftingBackward */
+
+
+/**Function********************************************************************
+
+  Synopsis    [Prepares the DD heap for dynamic reordering.]
+
+  Description [Prepares the DD heap for dynamic reordering. Does
+  garbage collection, to guarantee that there are no dead nodes;
+  clears the cache, which is invalidated by dynamic reordering; initializes
+  the number of isolated projection functions; and initializes the
+  interaction matrix.  Returns 1 in case of success; 0 otherwise.]
+
+  SideEffects [None]
+
+******************************************************************************/
+static int
+ddReorderPreprocess(
+  DdManager * table)
+{
+    int i;
+    int res;
+
+    /* Clear the cache. */
+    cuddCacheFlush(table);
+    cuddLocalCacheClearAll(table);
+
+    /* Eliminate dead nodes. Do not scan the cache again. */
+    cuddGarbageCollect(table,0);
+
+    /* Initialize number of isolated projection functions. */
+    table->isolated = 0;
+    for (i = 0; i < table->size; i++) {
+    if (table->vars[i]->ref == 1) table->isolated++;
+    }
+
+    /* Initialize the interaction matrix. */
+    res = cuddInitInteract(table);
+    if (res == 0) return(0);
+
+    return(1);
+
+} /* end of ddReorderPreprocess */
+
+
+/**Function********************************************************************
+
+  Synopsis    [Cleans up at the end of reordering.]
+
+  Description []
+
+  SideEffects [None]
+
+******************************************************************************/
+static int
+ddReorderPostprocess(
+  DdManager * table)
+{
+
+#ifdef DD_VERBOSE
+    (void) fflush(table->out);
+#endif
+
+    /* Free interaction matrix. */
+    FREE(table->interact);
+
+    return(1);
+
+} /* end of ddReorderPostprocess */
+
+
+/**Function********************************************************************
+
+  Synopsis    [Reorders variables according to a given permutation.]
+
+  Description [Reorders variables according to a given permutation.
+  The i-th permutation array contains the index of the variable that
+  should be brought to the i-th level. ddShuffle assumes that no
+  dead nodes are present and that the interaction matrix is properly
+  initialized.  The reordering is achieved by a series of upward sifts.
+  Returns 1 if successful; 0 otherwise.]
+
+  SideEffects [None]
+
+  SeeAlso []
+
+******************************************************************************/
+static int
+ddShuffle(
+  DdManager * table,
+  int * permutation)
+{
+    int        index;
+    int        level;
+    int        position;
+    int        numvars;
+    int        result;
+#ifdef DD_STATS
+    long    localTime;
+    int        initialSize;
+    int        finalSize;
+    int        previousSize;
+#endif
+
+    ddTotalNumberSwapping = 0;
+#ifdef DD_STATS
+    localTime = util_cpu_time();
+    initialSize = table->keys - table->isolated;
+    (void) fprintf(table->out,"#:I_SHUFFLE %8d: initial size\n",
+           initialSize); 
+    ddTotalNISwaps = 0;
+#endif
+
+    numvars = table->size;
+
+    for (level = 0; level < numvars; level++) {
+    index = permutation[level];
+    position = table->perm[index];
+#ifdef DD_STATS
+    previousSize = table->keys - table->isolated;
+#endif
+    result = ddSiftUp(table,position,level);
+    if (!result) return(0);
+#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
+    }
+
+#ifdef DD_STATS
+    (void) fprintf(table->out,"\n");
+    finalSize = table->keys - table->isolated;
+    (void) fprintf(table->out,"#:F_SHUFFLE %8d: final size\n",finalSize); 
+    (void) fprintf(table->out,"#:T_SHUFFLE %8g: total time (sec)\n",
+    ((double)(util_cpu_time() - localTime)/1000.0)); 
+    (void) fprintf(table->out,"#:N_SHUFFLE %8d: total swaps\n",
+           ddTotalNumberSwapping);
+    (void) fprintf(table->out,"#:M_SHUFFLE %8d: NI swaps\n",ddTotalNISwaps);
+#endif
+
+    return(1);
+
+} /* end of ddShuffle */
+
+
+/**Function********************************************************************
+
+  Synopsis    [Moves one variable up.]
+
+  Description [Takes a variable from position x and sifts it up to
+  position xLow;  xLow should be less than or equal to x.
+  Returns 1 if successful; 0 otherwise]
+
+  SideEffects [None]
+
+  SeeAlso     []
+
+******************************************************************************/
+static int
+ddSiftUp(
+  DdManager * table,
+  int  x,
+  int  xLow)
+{
+    int        y;
+    int        size;
+
+    y = cuddNextLow(table,x);
+    while (y >= xLow) {
+    size = cuddSwapInPlace(table,y,x);
+    if (size == 0) {
+        return(0);
+    }
+    x = y;
+    y = cuddNextLow(table,x);
+    }
+    return(1);
+
+} /* end of ddSiftUp */
+
+
+/**Function********************************************************************
+
+  Synopsis    [Fixes the BDD variable group tree after a shuffle.]
+
+  Description [Fixes the BDD variable group tree after a
+  shuffle. Assumes that the order of the variables in a terminal node
+  has not been changed.]
+
+  SideEffects [Changes the BDD variable group tree.]
+
+  SeeAlso     []
+
+******************************************************************************/
+static void
+bddFixTree(
+  DdManager * table,
+  MtrNode * treenode)
+{
+    if (treenode == NULL) return;
+    treenode->low = ((int) treenode->index < table->size) ?
+    table->perm[treenode->index] : treenode->index;
+    if (treenode->child != NULL) {
+    bddFixTree(table, treenode->child);
+    }
+    if (treenode->younger != NULL)
+    bddFixTree(table, treenode->younger);
+    if (treenode->parent != NULL && treenode->low < treenode->parent->low) {
+    treenode->parent->low = treenode->low;
+    treenode->parent->index = treenode->index;
+    }
+    return;
+
+} /* end of bddFixTree */
+
+
+/**Function********************************************************************
+
+  Synopsis    [Updates the BDD variable group tree before a shuffle.]
+
+  Description [Updates the BDD variable group tree before a shuffle.
+  Returns 1 if successful; 0 otherwise.]
+
+  SideEffects [Changes the BDD variable group tree.]
+
+  SeeAlso     []
+
+******************************************************************************/
+static int
+ddUpdateMtrTree(
+  DdManager * table,
+  MtrNode * treenode,
+  int * perm,
+  int * invperm)
+{
+    int    i, size, index, level;
+    int    minLevel, maxLevel, minIndex;
+
+    if (treenode == NULL) return(1);
+
+    /* i : level */
+    for (i = treenode->low; i < treenode->low + treenode->size; i++) {
+    index = table->invperm[i];
+    level = perm[index];
+    if (level < minLevel) {
+        minLevel = level;
+        minIndex = index;
+    }
+    if (level > maxLevel)
+        maxLevel = level;
+    }
+    size = maxLevel - minLevel + 1;
+    if (size == treenode->size) {
+    treenode->low = minLevel;
+    treenode->index = minIndex;
+    } else
+    return(0);
+
+    if (treenode->child != NULL) {
+    if (!ddUpdateMtrTree(table, treenode->child, perm, invperm))
+        return(0);
+    }
+    if (treenode->younger != NULL) {
+    if (!ddUpdateMtrTree(table, treenode->younger, perm, invperm))
+        return(0);
+    }
+    return(1);
+}
+
+
+/**Function********************************************************************
+
+  Synopsis    [Checks the BDD variable group tree before a shuffle.]
+
+  Description [Checks the BDD variable group tree before a shuffle.
+  Returns 1 if successful; 0 otherwise.]
+
+  SideEffects [Changes the BDD variable group tree.]
+
+  SeeAlso     []
+
+******************************************************************************/
+static int
+ddCheckPermuation(
+  DdManager * table,
+  MtrNode * treenode,
+  int * perm,
+  int * invperm)
+{
+    int    i, size, index, level;
+    int    minLevel, maxLevel;
+
+    if (treenode == NULL) return(1);
+
+    minLevel = table->size;
+    maxLevel = 0;
+    /* i : level */
+    for (i = treenode->low; i < treenode->low + treenode->size; i++) {
+    index = table->invperm[i];
+    level = perm[index];
+    if (level < minLevel)
+        minLevel = level;
+    if (level > maxLevel)
+        maxLevel = level;
+    }
+    size = maxLevel - minLevel + 1;
+    if (size != treenode->size)
+    return(0);
+
+    if (treenode->child != NULL) {
+    if (!ddCheckPermuation(table, treenode->child, perm, invperm))
+        return(0);
+    }
+    if (treenode->younger != NULL) {
+    if (!ddCheckPermuation(table, treenode->younger, perm, invperm))
+        return(0);
+    }
+    return(1);
+}