cuddZddReord.c

Go to the documentation of this file.

#include "CUDD/util.h"
#include "CUDD/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: cuddZddReord.c,v 1.49 2012/02/05 01:07:19 fabio Exp $";
#endif

int *zdd_entry;

int zddTotalNumberSwapping;

static  DdNode  *empty;


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


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

static Move * zddSwapAny (DdManager *table, int x, int y);
static int cuddZddSiftingAux (DdManager *table, int x, int x_low, int x_high);
static Move * cuddZddSiftingUp (DdManager *table, int x, int x_low, int initial_size);
static Move * cuddZddSiftingDown (DdManager *table, int x, int x_high, int initial_size);
static int cuddZddSiftingBackward (DdManager *table, Move *moves, int size);
static void zddReorderPreprocess (DdManager *table);
static int zddReorderPostprocess (DdManager *table);
static int zddShuffle (DdManager *table, int *permutation);
static int zddSiftUp (DdManager *table, int x, int xLow);
static void zddFixTree (DdManager *table, MtrNode *treenode);

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


int
Cudd_zddReduceHeap(
  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
    unsigned long localTime;

    /* Don't reorder if there are too many dead nodes. */
    if (table->keysZ - table->deadZ < (unsigned) minsize)
    return(1);

    if (heuristic == CUDD_REORDER_SAME) {
    heuristic = table->autoMethodZ;
    }
    if (heuristic == CUDD_REORDER_NONE) {
    return(1);
    }

    /* This call to Cudd_zddReduceHeap does initiate reordering. Therefore
    ** we count it.
    */
    table->reorderings++;
    empty = table->zero;

    localTime = util_cpu_time();

    /* Run the hook functions. */
    hook = table->preReorderingHook;
    while (hook != NULL) {
    int res = (hook->f)(table, "ZDD", (void *)heuristic);
    if (res == 0) return(0);
    hook = hook->next;
    }

    /* Clear the cache and collect garbage. */
    zddReorderPreprocess(table);
    zddTotalNumberSwapping = 0;

#ifdef DD_STATS
    initialSize = table->keysZ;

    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:
    (void) fprintf(table->out,"#:I_SIFTING ");
    break;
    case CUDD_REORDER_LINEAR:
    case CUDD_REORDER_LINEAR_CONVERGE:
    (void) fprintf(table->out,"#:I_LINSIFT ");
    break;
    default:
    (void) fprintf(table->err,"Unsupported ZDD reordering method\n");
    return(0);
    }
    (void) fprintf(table->out,"%8d: initial size",initialSize); 
#endif

    result = cuddZddTreeSifting(table,heuristic);

#ifdef DD_STATS
    (void) fprintf(table->out,"\n");
    finalSize = table->keysZ;
    (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",
           zddTotalNumberSwapping);
#endif

    if (result == 0)
    return(0);

    if (!zddReorderPostprocess(table))
    return(0);

    if (table->realignZ) {
    if (!cuddBddAlignToZdd(table))
        return(0);
    }

    nextDyn = table->keysZ * DD_DYN_RATIO;
    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, "ZDD", (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_zddReduceHeap */


int
Cudd_zddShuffleHeap(
  DdManager * table /* DD manager */,
  int * permutation /* required variable permutation */)
{

    int result;

    empty = table->zero;
    zddReorderPreprocess(table);

    result = zddShuffle(table,permutation);

    if (!zddReorderPostprocess(table)) return(0);

    return(result);

} /* end of Cudd_zddShuffleHeap */


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


int
cuddZddAlignToBdd(
  DdManager * table /* DD manager */)
{
    int *invpermZ;      /* permutation array */
    int M;          /* ratio of ZDD variables to BDD variables */
    int i,j;            /* loop indices */
    int result;         /* return value */

    /* We assume that a ratio of 0 is OK. */
    if (table->sizeZ == 0)
    return(1);

    empty = table->zero;
    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. */
    invpermZ = ALLOC(int,table->sizeZ);
    if (invpermZ == NULL) {
    table->errorCode = CUDD_MEMORY_OUT;
    return(0);
    }
    for (i = 0; i < table->size; i++) {
    int index = table->invperm[i];
    int indexZ = index * M;
    int levelZ = table->permZ[indexZ];
    levelZ = (levelZ / M) * M;
    for (j = 0; j < M; j++) {
        invpermZ[M * i + j] = table->invpermZ[levelZ + j];
    }
    }
    /* Eliminate dead nodes. Do not scan the cache again, because we
    ** assume that Cudd_ReduceHeap has already cleared it.
    */
    cuddGarbageCollect(table,0);

    result = zddShuffle(table, invpermZ);
    FREE(invpermZ);
    /* Fix the ZDD variable group tree. */
    zddFixTree(table,table->treeZ);
    return(result);
    
} /* end of cuddZddAlignToBdd */


int
cuddZddNextHigh(
  DdManager * table,
  int  x)
{
    return(x + 1);

} /* end of cuddZddNextHigh */


int
cuddZddNextLow(
  DdManager * table,
  int  x)
{
    return(x - 1);

} /* end of cuddZddNextLow */


int
cuddZddUniqueCompare(
  int * ptr_x,
  int * ptr_y)
{
    return(zdd_entry[*ptr_y] - zdd_entry[*ptr_x]);

} /* end of cuddZddUniqueCompare */


int
cuddZddSwapInPlace(
  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     i;
    int     posn;
    DdNode  *f, *f1, *f0, *f11, *f10, *f01, *f00;
    DdNode  *newf1, *newf0, *next;
    DdNodePtr   g, *lastP, *previousP;

#ifdef DD_DEBUG
    assert(x < y);
    assert(cuddZddNextHigh(table,x) == y);
    assert(table->subtableZ[x].keys != 0);
    assert(table->subtableZ[y].keys != 0);
    assert(table->subtableZ[x].dead == 0);
    assert(table->subtableZ[y].dead == 0);
#endif

    zddTotalNumberSwapping++;

    /* Get parameters of x subtable. */
    xindex   = table->invpermZ[x];
    xlist    = table->subtableZ[x].nodelist;
    oldxkeys = table->subtableZ[x].keys;
    xslots   = table->subtableZ[x].slots;
    xshift   = table->subtableZ[x].shift;
    newxkeys = 0;

    yindex   = table->invpermZ[y];
    ylist    = table->subtableZ[y].nodelist;
    oldykeys = table->subtableZ[y].keys;
    yslots   = table->subtableZ[y].slots;
    yshift   = table->subtableZ[y].shift;
    newykeys = oldykeys;

    /* The nodes in the x layer that don't depend on y directly
    ** will stay there; the others are put in a chain.
    ** The chain is handled as a FIFO; g points to the beginning and
    ** last points to the end.
    */

    g = NULL;
    lastP = &g;
    for (i = 0; i < xslots; i++) {
    previousP = &(xlist[i]);
    f = *previousP;
    while (f != NULL) {
        next = f->next;
        f1 = cuddT(f); f0 = cuddE(f);
        if ((f1->index != (DdHalfWord) yindex) &&
        (f0->index != (DdHalfWord) yindex)) { /* stays */
            newxkeys++;
        *previousP = f;
        previousP = &(f->next);
        } else {
        f->index = yindex;
        *lastP = f;
        lastP = &(f->next);
        }
        f = next;
    } /* while there are elements in the collision chain */
    *previousP = NULL;
    } /* for each slot of the x subtable */
    *lastP = NULL;


#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
    ** changed to yindex already.
    */
    f = g;
    while (f != NULL) {
    next = f->next;
    /* Find f1, f0, f11, f10, f01, f00. */
    f1 = cuddT(f);
    if ((int) f1->index == yindex) {
        f11 = cuddT(f1); f10 = cuddE(f1);
    } else {
        f11 = empty; f10 = f1;
    }
    f0 = cuddE(f);
    if ((int) f0->index == yindex) {
        f01 = cuddT(f0); f00 = cuddE(f0);
    } else {
        f01 = empty; f00 = f0;
    }

    /* Decrease ref count of f1. */
    cuddSatDec(f1->ref);
    /* Create the new T child. */
    if (f11 == empty) {
        if (f01 != empty) {
        newf1 = f01;
        cuddSatInc(newf1->ref);
        }
        /* else case was already handled when finding nodes
        ** with both children below level y
        */
    } else {
        /* Check xlist for triple (xindex, f11, f01). */
        posn = ddHash(f11, f01, xshift);
        /* For each element newf1 in collision list xlist[posn]. */
        newf1 = xlist[posn];
        while (newf1 != NULL) {
        if (cuddT(newf1) == f11 && cuddE(newf1) == f01) {
            cuddSatInc(newf1->ref);
            break; /* match */
        }
        newf1 = newf1->next;
        } /* while newf1 */
        if (newf1 == NULL) {    /* no match */
        newf1 = cuddDynamicAllocNode(table);
        if (newf1 == NULL)
            goto zddSwapOutOfMem;
        newf1->index = xindex; newf1->ref = 1;
        cuddT(newf1) = f11;
        cuddE(newf1) = f01;
        /* Insert newf1 in the collision list xlist[pos];
        ** increase the ref counts of f11 and f01
        */
        newxkeys++;
        newf1->next = xlist[posn];
        xlist[posn] = newf1;
        cuddSatInc(f11->ref);
        cuddSatInc(f01->ref);
        }
    }
    cuddT(f) = newf1;

    /* Do the same for f0. */
    /* Decrease ref count of f0. */
    cuddSatDec(f0->ref);
    /* Create the new E child. */
    if (f10 == empty) {
        newf0 = f00;
        cuddSatInc(newf0->ref);
    } else {
        /* Check xlist for triple (xindex, f10, f00). */
        posn = ddHash(f10, f00, xshift);
        /* For each element newf0 in collision list xlist[posn]. */
        newf0 = xlist[posn];
        while (newf0 != NULL) {
        if (cuddT(newf0) == f10 && cuddE(newf0) == f00) {
            cuddSatInc(newf0->ref);
            break; /* match */
        }
        newf0 = newf0->next;
        } /* while newf0 */
        if (newf0 == NULL) {    /* no match */
        newf0 = cuddDynamicAllocNode(table);
        if (newf0 == NULL)
            goto zddSwapOutOfMem;
        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 = xlist[posn];
        xlist[posn] = newf0;
        cuddSatInc(f10->ref);
        cuddSatInc(f00->ref);
        }
    }
    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++;
    f->next = ylist[posn];
    ylist[posn] = 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 != NULL) {
        next = f->next;
        if (f->ref == 0) {
        cuddSatDec(cuddT(f)->ref);
        cuddSatDec(cuddE(f)->ref);
        cuddDeallocNode(table, f);
        newykeys--;
        } else {
        *previousP = f;
        previousP = &(f->next);
        }
        f = next;
    } /* while f */
    *previousP = NULL;
    } /* for i */

    /* Set the appropriate fields in table. */
    table->subtableZ[x].nodelist = ylist;
    table->subtableZ[x].slots    = yslots;
    table->subtableZ[x].shift    = yshift;
    table->subtableZ[x].keys     = newykeys;
    table->subtableZ[x].maxKeys  = yslots * DD_MAX_SUBTABLE_DENSITY;

    table->subtableZ[y].nodelist = xlist;
    table->subtableZ[y].slots    = xslots;
    table->subtableZ[y].shift    = xshift;
    table->subtableZ[y].keys     = newxkeys;
    table->subtableZ[y].maxKeys  = xslots * DD_MAX_SUBTABLE_DENSITY;

    table->permZ[xindex] = y; table->permZ[yindex] = x;
    table->invpermZ[x] = yindex; table->invpermZ[y] = xindex;

    table->keysZ += newxkeys + newykeys - oldxkeys - oldykeys;

    /* Update univ section; univ[x] remains the same. */
    table->univ[y] = cuddT(table->univ[x]);

    return (table->keysZ);

zddSwapOutOfMem:
    (void) fprintf(table->err, "Error: cuddZddSwapInPlace out of memory\n");

    return (0);

} /* end of cuddZddSwapInPlace */


int
cuddZddSwapping(
  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->sizeZ && lower <= upper);
#endif

    nvars = upper - lower + 1;
    iterate = nvars;

    for (i = 0; i < iterate; i++) {
    if (heuristic == CUDD_REORDER_RANDOM_PIVOT) {
        /* Find pivot <= id with maximum keys. */
        for (max = -1, j = lower; j <= upper; j++) {
        if ((keys = table->subtableZ[j].keys) > max) {
            max = keys;
            pivot = j;
        }
        }

        modulo = upper - pivot;
        if (modulo == 0) {
        y = pivot;  /* y = nvars-1 */
        } else {
        /* y = random # from {pivot+1 .. nvars-1} */
        y = pivot + 1 + (int) (Cudd_Random() % modulo);
        }

        modulo = pivot - lower - 1;
        if (modulo < 1) {   /* if pivot = 1 or 0 */
        x = lower;
        } else {
        do { /* x = random # from {0 .. pivot-2} */
            x = (int) Cudd_Random() % modulo;
        } while (x == y);
          /* Is this condition really needed, since x and y
             are in regions separated by pivot? */
        }
    } else {
        x = (int) (Cudd_Random() % nvars) + lower;
        do {
        y = (int) (Cudd_Random() % nvars) + lower;
        } while (x == y);
    }

    previousSize = table->keysZ;
    moves = zddSwapAny(table, x, y);
    if (moves == NULL)
        goto cuddZddSwappingOutOfMem;

    result = cuddZddSiftingBackward(table, moves, previousSize);
    if (!result)
        goto cuddZddSwappingOutOfMem;

    while (moves != NULL) {
        move = moves->next;
        cuddDeallocMove(table, moves);
        moves = move;
    }
#ifdef DD_STATS
    if (table->keysZ < (unsigned) previousSize) {
        (void) fprintf(table->out,"-");
    } else if (table->keysZ > (unsigned) previousSize) {
        (void) fprintf(table->out,"+"); /* should never happen */
    } else {
        (void) fprintf(table->out,"=");
    }
    fflush(table->out);
#endif
    }

    return(1);

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

} /* end of cuddZddSwapping */


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

    size = table->sizeZ;

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

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

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

    /* Now sift. */
    for (i = 0; i < ddMin(table->siftMaxVar, size); i++) {
    if (zddTotalNumberSwapping >= table->siftMaxSwap)
        break;
        if (util_cpu_time() - table->startTime > table->timeLimit) {
            table->autoDynZ = 0; /* prevent further reordering */
            break;
        }
    x = table->permZ[var[i]];
    if (x < lower || x > upper) continue;
#ifdef DD_STATS
    previousSize = table->keysZ;
#endif
    result = cuddZddSiftingAux(table, x, lower, upper);
    if (!result)
        goto cuddZddSiftingOutOfMem;
#ifdef DD_STATS
    if (table->keysZ < (unsigned) previousSize) {
        (void) fprintf(table->out,"-");
    } else if (table->keysZ > (unsigned) previousSize) {
        (void) fprintf(table->out,"+"); /* should never happen */
        (void) fprintf(table->out,"\nSize increased from %d to %d while sifting variable %d\n", previousSize, table->keysZ , var[i]);
    } else {
        (void) fprintf(table->out,"=");
    }
    fflush(table->out);
#endif
    }

    FREE(var);
    FREE(zdd_entry);

    return(1);

cuddZddSiftingOutOfMem:

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

    return(0);

} /* end of cuddZddSifting */


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


static Move *
zddSwapAny(
  DdManager * table,
  int  x,
  int  y)
{
    Move    *move, *moves;
    int     tmp, size;
    int     x_ref, y_ref;
    int     x_next, y_next;
    int     limit_size;

    if (x > y) {    /* make x precede y */
    tmp = x; x = y; y = tmp;
    }

    x_ref = x; y_ref = y;

    x_next = cuddZddNextHigh(table, x);
    y_next = cuddZddNextLow(table, y);
    moves = NULL;
    limit_size = table->keysZ;

    for (;;) {
    if (x_next == y_next) { /* x < x_next = y_next < y */
        size = cuddZddSwapInPlace(table, x, x_next);
        if (size == 0)
        goto zddSwapAnyOutOfMem;
        move = (Move *) cuddDynamicAllocNode(table);
        if (move == NULL)
        goto zddSwapAnyOutOfMem;
        move->x = x;
        move->y = x_next;
        move->size = size;
        move->next = moves;
        moves = move;

        size = cuddZddSwapInPlace(table, y_next, y);
        if (size == 0)
        goto zddSwapAnyOutOfMem;
        move = (Move *)cuddDynamicAllocNode(table);
        if (move == NULL)
        goto zddSwapAnyOutOfMem;
        move->x = y_next;
        move->y = y;
        move->size = size;
        move->next = moves;
        moves = move;

        size = cuddZddSwapInPlace(table, x, x_next);
        if (size == 0)
        goto zddSwapAnyOutOfMem;
        move = (Move *)cuddDynamicAllocNode(table);
        if (move == NULL)
        goto zddSwapAnyOutOfMem;
        move->x = x;
        move->y = x_next;
        move->size = size;
        move->next = moves;
        moves = move;

        tmp = x; x = y; y = tmp;

    } else if (x == y_next) { /* x = y_next < y = x_next */
        size = cuddZddSwapInPlace(table, x, x_next);
        if (size == 0)
        goto zddSwapAnyOutOfMem;
        move = (Move *)cuddDynamicAllocNode(table);
        if (move == NULL)
        goto zddSwapAnyOutOfMem;
        move->x = x;
        move->y = x_next;
        move->size = size;
        move->next = moves;
        moves = move;

        tmp = x; x = y;  y = tmp;
    } else {
        size = cuddZddSwapInPlace(table, x, x_next);
        if (size == 0)
        goto zddSwapAnyOutOfMem;
        move = (Move *)cuddDynamicAllocNode(table);
        if (move == NULL)
        goto zddSwapAnyOutOfMem;
        move->x = x;
        move->y = x_next;
        move->size = size;
        move->next = moves;
        moves = move;

        size = cuddZddSwapInPlace(table, y_next, y);
        if (size == 0)
        goto zddSwapAnyOutOfMem;
        move = (Move *)cuddDynamicAllocNode(table);
        if (move == NULL)
        goto zddSwapAnyOutOfMem;
        move->x = y_next;
        move->y = y;
        move->size = size;
        move->next = moves;
        moves = move;

        x = x_next; y = y_next;
    }

    x_next = cuddZddNextHigh(table, x);
    y_next = cuddZddNextLow(table, y);
    if (x_next > y_ref)
        break;  /* if x == y_ref */

    if ((double) size > table->maxGrowth * (double) limit_size)
        break;
    if (size < limit_size)
        limit_size = size;
    }
    if (y_next >= x_ref) {
    size = cuddZddSwapInPlace(table, y_next, y);
    if (size == 0)
        goto zddSwapAnyOutOfMem;
    move = (Move *)cuddDynamicAllocNode(table);
    if (move == NULL)
        goto zddSwapAnyOutOfMem;
    move->x = y_next;
    move->y = y;
    move->size = size;
    move->next = moves;
    moves = move;
    }

    return(moves);

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

} /* end of zddSwapAny */


static int
cuddZddSiftingAux(
  DdManager * table,
  int  x,
  int  x_low,
  int  x_high)
{
    Move    *move;
    Move    *moveUp;    /* list of up move */
    Move    *moveDown;  /* list of down move */

    int     initial_size;
    int     result;

    initial_size = table->keysZ;

#ifdef DD_DEBUG
    assert(table->subtableZ[x].keys > 0);
#endif

    moveDown = NULL;
    moveUp = NULL;

    if (x == x_low) {
    moveDown = cuddZddSiftingDown(table, x, x_high, initial_size);
    /* after that point x --> x_high */
    if (moveDown == NULL)
        goto cuddZddSiftingAuxOutOfMem;
    result = cuddZddSiftingBackward(table, moveDown,
        initial_size);
    /* move backward and stop at best position */
    if (!result)
        goto cuddZddSiftingAuxOutOfMem;

    }
    else if (x == x_high) {
    moveUp = cuddZddSiftingUp(table, x, x_low, initial_size);
    /* after that point x --> x_low */
    if (moveUp == NULL)
        goto cuddZddSiftingAuxOutOfMem;
    result = cuddZddSiftingBackward(table, moveUp, initial_size);
    /* move backward and stop at best position */
    if (!result)
        goto cuddZddSiftingAuxOutOfMem;
    }
    else if ((x - x_low) > (x_high - x)) {
    /* must go down first:shorter */
    moveDown = cuddZddSiftingDown(table, x, x_high, initial_size);
    /* after that point x --> x_high */
    if (moveDown == NULL)
        goto cuddZddSiftingAuxOutOfMem;
    moveUp = cuddZddSiftingUp(table, moveDown->y, x_low,
        initial_size);
    if (moveUp == NULL)
        goto cuddZddSiftingAuxOutOfMem;
    result = cuddZddSiftingBackward(table, moveUp, initial_size);
    /* move backward and stop at best position */
    if (!result)
        goto cuddZddSiftingAuxOutOfMem;
    }
    else {
    moveUp = cuddZddSiftingUp(table, x, x_low, initial_size);
    /* after that point x --> x_high */
    if (moveUp == NULL)
        goto cuddZddSiftingAuxOutOfMem;
    moveDown = cuddZddSiftingDown(table, moveUp->x, x_high,
        initial_size);
    /* then move up */
    if (moveDown == NULL)
        goto cuddZddSiftingAuxOutOfMem;
    result = cuddZddSiftingBackward(table, moveDown,
        initial_size);
    /* move backward and stop at best position */
    if (!result)
        goto cuddZddSiftingAuxOutOfMem;
    }

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

    return(1);

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

    return(0);

} /* end of cuddZddSiftingAux */


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

    moves = NULL;
    y = cuddZddNextLow(table, x);
    while (y >= x_low) {
    size = cuddZddSwapInPlace(table, y, x);
    if (size == 0)
        goto cuddZddSiftingUpOutOfMem;
    move = (Move *)cuddDynamicAllocNode(table);
    if (move == NULL)
        goto cuddZddSiftingUpOutOfMem;
    move->x = y;
    move->y = x;
    move->size = size;
    move->next = moves;
    moves = move;

    if ((double)size > (double)limit_size * table->maxGrowth)
        break;
        if (size < limit_size)
        limit_size = size;

    x = y;
    y = cuddZddNextLow(table, x);
    }
    return(moves);

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

} /* end of cuddZddSiftingUp */


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

    moves = NULL;
    y = cuddZddNextHigh(table, x);
    while (y <= x_high) {
    size = cuddZddSwapInPlace(table, x, y);
    if (size == 0)
        goto cuddZddSiftingDownOutOfMem;
    move = (Move *)cuddDynamicAllocNode(table);
    if (move == NULL)
        goto cuddZddSiftingDownOutOfMem;
    move->x = x;
    move->y = y;
    move->size = size;
    move->next = moves;
    moves = move;

    if ((double)size > (double)limit_size * table->maxGrowth)
        break;
        if (size < limit_size)
        limit_size = size;

    x = y;
    y = cuddZddNextHigh(table, x);
    }
    return(moves);

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

} /* end of cuddZddSiftingDown */


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

    /* Find the minimum size among moves. */
    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;
    res = cuddZddSwapInPlace(table, move->x, move->y);
    if (!res)
        return(0);
    if (i_best == -1 && res == size)
        break;
    }

    return(1);

} /* end of cuddZddSiftingBackward */


static void
zddReorderPreprocess(
  DdManager * table)
{

    /* Clear the cache. */
    cuddCacheFlush(table);

    /* Eliminate dead nodes. Do not scan the cache again. */
    cuddGarbageCollect(table,0);

    return;

} /* end of ddReorderPreprocess */


static int
zddReorderPostprocess(
  DdManager * table)
{
    int i, j, posn;
    DdNodePtr *nodelist, *oldnodelist;
    DdNode *node, *next;
    unsigned int slots, oldslots;
    extern DD_OOMFP MMoutOfMemory;
    DD_OOMFP saveHandler;

#ifdef DD_VERBOSE
    (void) fflush(table->out);
#endif

    /* If we have very many reclaimed nodes, we do not want to shrink
    ** the subtables, because this will lead to more garbage
    ** collections. More garbage collections mean shorter mean life for
    ** nodes with zero reference count; hence lower probability of finding
    ** a result in the cache.
    */
    if (table->reclaimed > table->allocated * 0.5) return(1);

    /* Resize subtables. */
    for (i = 0; i < table->sizeZ; i++) {
    int shift;
    oldslots = table->subtableZ[i].slots;
    if (oldslots < table->subtableZ[i].keys * DD_MAX_SUBTABLE_SPARSITY ||
        oldslots <= table->initSlots) continue;
    oldnodelist = table->subtableZ[i].nodelist;
    slots = oldslots >> 1;
    saveHandler = MMoutOfMemory;
    MMoutOfMemory = Cudd_OutOfMem;
    nodelist = ALLOC(DdNodePtr, slots);
    MMoutOfMemory = saveHandler;
    if (nodelist == NULL) {
        return(1);
    }
    table->subtableZ[i].nodelist = nodelist;
    table->subtableZ[i].slots = slots;
    table->subtableZ[i].shift++;
    table->subtableZ[i].maxKeys = slots * DD_MAX_SUBTABLE_DENSITY;
#ifdef DD_VERBOSE
    (void) fprintf(table->err,
               "shrunk layer %d (%d keys) from %d to %d slots\n",
               i, table->subtableZ[i].keys, oldslots, slots);
#endif

    for (j = 0; (unsigned) j < slots; j++) {
        nodelist[j] = NULL;
    }
    shift = table->subtableZ[i].shift;
    for (j = 0; (unsigned) j < oldslots; j++) {
        node = oldnodelist[j];
        while (node != NULL) {
        next = node->next;
        posn = ddHash(cuddT(node), cuddE(node), shift);
        node->next = nodelist[posn];
        nodelist[posn] = node;
        node = next;
        }
    }
    FREE(oldnodelist);

    table->memused += (slots - oldslots) * sizeof(DdNode *);
    table->slots += slots - oldslots;
    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;
    }
    /* We don't look at the constant subtable, because it is not
    ** affected by reordering.
    */

    return(1);

} /* end of zddReorderPostprocess */


static int
zddShuffle(
  DdManager * table,
  int * permutation)
{
    int     index;
    int     level;
    int     position;
    int     numvars;
    int     result;
#ifdef DD_STATS
    unsigned long localTime;
    int     initialSize;
    int     finalSize;
    int     previousSize;
#endif

    zddTotalNumberSwapping = 0;
#ifdef DD_STATS
    localTime = util_cpu_time();
    initialSize = table->keysZ;
    (void) fprintf(table->out,"#:I_SHUFFLE %8d: initial size\n",
           initialSize); 
#endif

    numvars = table->sizeZ;

    for (level = 0; level < numvars; level++) {
    index = permutation[level];
    position = table->permZ[index];
#ifdef DD_STATS
    previousSize = table->keysZ;
#endif
    result = zddSiftUp(table,position,level);
    if (!result) return(0);
#ifdef DD_STATS
    if (table->keysZ < (unsigned) previousSize) {
        (void) fprintf(table->out,"-");
    } else if (table->keysZ > (unsigned) previousSize) {
        (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->keysZ;
    (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",
           zddTotalNumberSwapping);
#endif

    return(1);

} /* end of zddShuffle */


static int
zddSiftUp(
  DdManager * table,
  int  x,
  int  xLow)
{
    int        y;
    int        size;

    y = cuddZddNextLow(table,x);
    while (y >= xLow) {
    size = cuddZddSwapInPlace(table,y,x);
    if (size == 0) {
        return(0);
    }
    x = y;
    y = cuddZddNextLow(table,x);
    }
    return(1);

} /* end of zddSiftUp */


static void
zddFixTree(
  DdManager * table,
  MtrNode * treenode)
{
    if (treenode == NULL) return;
    treenode->low = ((int) treenode->index < table->sizeZ) ?
    table->permZ[treenode->index] : treenode->index;
    if (treenode->child != NULL) {
    zddFixTree(table, treenode->child);
    }
    if (treenode->younger != NULL)
    zddFixTree(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 zddFixTree */