Version abc70930

1 files changed, 0 insertions, 1004 deletions

diff --git a/src/bdd/cudd/cuddExact.c b/src/bdd/cudd/cuddExact.c
deleted file mode 100644
index 6852be68..00000000
--- a/src/bdd/cudd/cuddExact.c
+++ /dev/null
@@ -1,1004 +0,0 @@
-/**CFile***********************************************************************
-
-  FileName    [cuddExact.c]
-
-  PackageName [cudd]
-
-  Synopsis    [Functions for exact variable reordering.]
-
-  Description [External procedures included in this file:
-        <ul>
-        </ul>
-    Internal procedures included in this module:
-        <ul>
-        <li> cuddExact()
-        </ul>
-    Static procedures included in this module:
-        <ul> 
-                <li> getMaxBinomial()
-        <li> gcd()
-                <li> getMatrix()
-        <li> freeMatrix()
-                <li> getLevelKeys()
-                <li> ddShuffle()
-                <li> ddSiftUp()
-        <li> updateUB()
-        <li> ddCountRoots()
-        <li> ddClearGlobal()
-        <li> computeLB()
-        <li> updateEntry()
-        <li> pushDown()
-        <li> initSymmInfo()
-                </ul>]
-
-  Author      [Cheng Hua, 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                                                     */
-/*---------------------------------------------------------------------------*/
-
-
-/*---------------------------------------------------------------------------*/
-/* Stucture declarations                                                     */
-/*---------------------------------------------------------------------------*/
-
-/*---------------------------------------------------------------------------*/
-/* Type declarations                                                         */
-/*---------------------------------------------------------------------------*/
-
-/*---------------------------------------------------------------------------*/
-/* Variable declarations                                                     */
-/*---------------------------------------------------------------------------*/
-
-#ifndef lint
-static char rcsid[] DD_UNUSED = "$Id: cuddExact.c,v 1.1.1.1 2003/02/24 22:23:52 wjiang Exp $";
-#endif
-
-#ifdef DD_STATS
-static int ddTotalShuffles;
-#endif
-
-/*---------------------------------------------------------------------------*/
-/* Macro declarations                                                        */
-/*---------------------------------------------------------------------------*/
-
-/**AutomaticStart*************************************************************/
-
-/*---------------------------------------------------------------------------*/
-/* Static function prototypes                                                */
-/*---------------------------------------------------------------------------*/
-
-static int getMaxBinomial ARGS((int n));
-static int gcd ARGS((int x, int y));
-static DdHalfWord ** getMatrix ARGS((int rows, int cols));
-static void freeMatrix ARGS((DdHalfWord **matrix));
-static int getLevelKeys ARGS((DdManager *table, int l));
-static int ddShuffle ARGS((DdManager *table, DdHalfWord *permutation, int lower, int upper));
-static int ddSiftUp ARGS((DdManager *table, int x, int xLow));
-static int updateUB ARGS((DdManager *table, int oldBound, DdHalfWord *bestOrder, int lower, int upper));
-static int ddCountRoots ARGS((DdManager *table, int lower, int upper));
-static void ddClearGlobal ARGS((DdManager *table, int lower, int maxlevel));
-static int computeLB ARGS((DdManager *table, DdHalfWord *order, int roots, int cost, int lower, int upper, int level));
-static int updateEntry ARGS((DdManager *table, DdHalfWord *order, int level, int cost, DdHalfWord **orders, int *costs, int subsets, char *mask, int lower, int upper));
-static void pushDown ARGS((DdHalfWord *order, int j, int level));
-static DdHalfWord * initSymmInfo ARGS((DdManager *table, int lower, int upper));
-static int checkSymmInfo ARGS((DdManager *table, DdHalfWord *symmInfo, int index, int level));
-
-/**AutomaticEnd***************************************************************/
-
-
-/*---------------------------------------------------------------------------*/
-/* Definition of exported functions                                          */
-/*---------------------------------------------------------------------------*/
-
-/*---------------------------------------------------------------------------*/
-/* Definition of internal functions                                          */
-/*---------------------------------------------------------------------------*/
-
-
-/**Function********************************************************************
-
-  Synopsis    [Exact variable ordering algorithm.]
-
-  Description [Exact variable ordering algorithm. Finds an optimum
-  order for the variables between lower and upper.  Returns 1 if
-  successful; 0 otherwise.]
-
-  SideEffects [None]
-
-  SeeAlso     []
-
-******************************************************************************/
-int
-cuddExact(
-  DdManager * table,
-  int  lower,
-  int  upper)
-{
-    int k, i, j;
-    int maxBinomial, oldSubsets, newSubsets;
-    int subsetCost;
-    int size;            /* number of variables to be reordered */
-    int unused, nvars, level, result;
-    int upperBound, lowerBound, cost;
-    int roots;
-    char *mask = NULL;
-    DdHalfWord  *symmInfo = NULL;
-    DdHalfWord **newOrder = NULL;
-    DdHalfWord **oldOrder = NULL;
-    int *newCost = NULL;
-    int *oldCost = NULL;
-    DdHalfWord **tmpOrder;
-    int *tmpCost;
-    DdHalfWord *bestOrder = NULL;
-    DdHalfWord *order;
-#ifdef DD_STATS
-    int  ddTotalSubsets;
-#endif
-
-    /* Restrict the range to be reordered by excluding unused variables
-    ** at the two ends. */
-    while (table->subtables[lower].keys == 1 &&
-       table->vars[table->invperm[lower]]->ref == 1 &&
-       lower < upper)
-    lower++;
-    while (table->subtables[upper].keys == 1 &&
-       table->vars[table->invperm[upper]]->ref == 1 &&
-       lower < upper)
-    upper--;
-    if (lower == upper) return(1); /* trivial problem */
-
-    /* Apply symmetric sifting to get a good upper bound and to extract
-    ** symmetry information. */
-    result = cuddSymmSiftingConv(table,lower,upper);
-    if (result == 0) goto cuddExactOutOfMem;
-
-#ifdef DD_STATS
-    (void) fprintf(table->out,"\n");
-    ddTotalShuffles = 0;
-    ddTotalSubsets = 0;
-#endif
-
-    /* Initialization. */
-    nvars = table->size;
-    size = upper - lower + 1;
-    /* Count unused variable among those to be reordered.  This is only
-    ** used to compute maxBinomial. */
-    unused = 0;
-    for (i = lower + 1; i < upper; i++) {
-    if (table->subtables[i].keys == 1 &&
-        table->vars[table->invperm[i]]->ref == 1)
-        unused++;
-    }
-
-    /* Find the maximum number of subsets we may have to store. */
-    maxBinomial = getMaxBinomial(size - unused);
-    if (maxBinomial == -1) goto cuddExactOutOfMem;
-
-    newOrder = getMatrix(maxBinomial, size);
-    if (newOrder == NULL) goto cuddExactOutOfMem;
-
-    newCost = ALLOC(int, maxBinomial);
-    if (newCost == NULL) goto cuddExactOutOfMem;
-
-    oldOrder = getMatrix(maxBinomial, size);
-    if (oldOrder == NULL) goto cuddExactOutOfMem;
-
-    oldCost = ALLOC(int, maxBinomial);
-    if (oldCost == NULL) goto cuddExactOutOfMem;
-
-    bestOrder = ALLOC(DdHalfWord, size);
-    if (bestOrder == NULL) goto cuddExactOutOfMem;
-
-    mask = ALLOC(char, nvars);
-    if (mask == NULL) goto cuddExactOutOfMem;
-
-    symmInfo = initSymmInfo(table, lower, upper);
-    if (symmInfo == NULL) goto cuddExactOutOfMem;
-
-    roots = ddCountRoots(table, lower, upper);
-
-    /* Initialize the old order matrix for the empty subset and the best
-    ** order to the current order. The cost for the empty subset includes
-    ** the cost of the levels between upper and the constants. These levels
-    ** are not going to change. Hence, we count them only once.
-    */
-    oldSubsets = 1;
-    for (i = 0; i < size; i++) {
-    oldOrder[0][i] = bestOrder[i] = (DdHalfWord) table->invperm[i+lower];
-    }
-    subsetCost = table->constants.keys;
-    for (i = upper + 1; i < nvars; i++)
-    subsetCost += getLevelKeys(table,i);
-    oldCost[0] = subsetCost;
-    /* The upper bound is initialized to the current size of the BDDs. */
-    upperBound = table->keys - table->isolated;
-
-    /* Now consider subsets of increasing size. */
-    for (k = 1; k <= size; k++) {
-#if DD_STATS
-    (void) fprintf(table->out,"Processing subsets of size %d\n", k);
-    fflush(table->out);
-#endif
-    newSubsets = 0;
-    level = size - k;        /* offset of first bottom variable */
-
-    for (i = 0; i < oldSubsets; i++) { /* for each subset of size k-1 */
-        order = oldOrder[i];
-        cost = oldCost[i];
-        lowerBound = computeLB(table, order, roots, cost, lower, upper,
-                   level);
-        if (lowerBound >= upperBound)
-        continue;
-        /* Impose new order. */
-        result = ddShuffle(table, order, lower, upper);
-        if (result == 0) goto cuddExactOutOfMem;
-        upperBound = updateUB(table,upperBound,bestOrder,lower,upper);
-        /* For each top bottom variable. */
-        for (j = level; j >= 0; j--) {
-        /* Skip unused variables. */
-        if (table->subtables[j+lower-1].keys == 1 &&
-            table->vars[table->invperm[j+lower-1]]->ref == 1) continue;
-        /* Find cost under this order. */
-        subsetCost = cost + getLevelKeys(table, lower + level);
-        newSubsets = updateEntry(table, order, level, subsetCost,
-                     newOrder, newCost, newSubsets, mask,
-                     lower, upper);
-        if (j == 0)
-            break;
-        if (checkSymmInfo(table, symmInfo, order[j-1], level) == 0)
-            continue;
-        pushDown(order,j-1,level);
-        /* Impose new order. */
-        result = ddShuffle(table, order, lower, upper);
-        if (result == 0) goto cuddExactOutOfMem;
-        upperBound = updateUB(table,upperBound,bestOrder,lower,upper);
-        } /* for each bottom variable */
-    } /* for each subset of size k */
-
-    /* New orders become old orders in preparation for next iteration. */
-    tmpOrder = oldOrder; tmpCost = oldCost;
-    oldOrder = newOrder; oldCost = newCost;
-    newOrder = tmpOrder; newCost = tmpCost;
-#ifdef DD_STATS
-    ddTotalSubsets += newSubsets;
-#endif
-    oldSubsets = newSubsets;
-    }
-    result = ddShuffle(table, bestOrder, lower, upper);
-    if (result == 0) goto cuddExactOutOfMem;
-#ifdef DD_STATS
-#ifdef DD_VERBOSE
-    (void) fprintf(table->out,"\n");
-#endif
-    (void) fprintf(table->out,"#:S_EXACT   %8d: total subsets\n",
-           ddTotalSubsets);
-    (void) fprintf(table->out,"#:H_EXACT   %8d: total shuffles",
-           ddTotalShuffles);
-#endif
-
-    freeMatrix(newOrder);
-    freeMatrix(oldOrder);
-    FREE(bestOrder);
-    FREE(oldCost);
-    FREE(newCost);
-    FREE(symmInfo);
-    FREE(mask);
-    return(1);
-
-cuddExactOutOfMem:
-
-    if (newOrder != NULL) freeMatrix(newOrder);
-    if (oldOrder != NULL) freeMatrix(oldOrder);
-    if (bestOrder != NULL) FREE(bestOrder);
-    if (oldCost != NULL) FREE(oldCost);
-    if (newCost != NULL) FREE(newCost);
-    if (symmInfo != NULL) FREE(symmInfo);
-    if (mask != NULL) FREE(mask);
-    table->errorCode = CUDD_MEMORY_OUT;
-    return(0);
-
-} /* end of cuddExact */
-
-
-/**Function********************************************************************
-
-  Synopsis    [Returns the maximum value of (n choose k) for a given n.]
-
-  Description [Computes the maximum value of (n choose k) for a given
-  n.  The maximum value occurs for k = n/2 when n is even, or k =
-  (n-1)/2 when n is odd.  The algorithm used in this procedure is
-  quite inefficient, but it avoids intermediate overflow problems.
-  Returns the computed value if successful; -1 otherwise.]
-
-  SideEffects [None]
-
-  SeeAlso     []
-
-******************************************************************************/
-static int
-getMaxBinomial(
-  int  n)
-{
-    int *numerator;
-    int i, j, k, y, g, result;
-
-    k = (n & ~1) >> 1;
-
-    numerator = ALLOC(int,k);
-    if (numerator == NULL) return(-1);
-    
-    for (i = 0; i < k; i++)
-    numerator[i] = n - i;
-    
-    for (i = k; i > 1; i--) {
-    y = i;
-    for (j = 0; j < k; j++) {
-        if (numerator[j] == 1) continue;
-        g = gcd(numerator[j], y);
-        if (g != 1) {
-        numerator[j] /= g;
-        if (y == g) break;
-        y /= g;
-        }
-    }
-    }
-
-    result = 1;
-    for (i = 0; i < k; i++)
-    result *= numerator[i];
-
-    FREE(numerator);
-    return(result);
-
-}  /* end of getMaxBinomial */
-
-
-/**Function********************************************************************
-
-  Synopsis    [Returns the gcd of two integers.]
-
-  Description [Returns the gcd of two integers. Uses the binary GCD
-  algorithm described in Cormen, Leiserson, and Rivest.]
-
-  SideEffects [None]
-
-  SeeAlso     []
-
-******************************************************************************/
-static int
-gcd(
-  int  x,
-  int  y)
-{
-    int a;
-    int b;
-    int lsbMask;
-
-    /* GCD(n,0) = n. */
-    if (x == 0) return(y);
-    if (y == 0) return(x);
-
-    a = x; b = y; lsbMask = 1;
-    
-    /* Here both a and b are != 0. The iteration maintains this invariant.
-    ** Hence, we only need to check for when they become equal.
-    */
-    while (a != b) {
-    if (a & lsbMask) {
-        if (b & lsbMask) {    /* both odd */
-        if (a < b) {
-            b = (b - a) >> 1;
-        } else {
-            a = (a - b) >> 1;
-        }
-        } else {        /* a odd, b even */
-        b >>= 1;
-        }
-    } else {
-        if (b & lsbMask) {    /* a even, b odd */
-        a >>= 1;
-        } else {        /* both even */
-        lsbMask <<= 1;
-        }
-    }
-    }
-
-    return(a);
-
-} /* end of gcd */
-
-
-/**Function********************************************************************
-
-  Synopsis    [Allocates a two-dimensional matrix of ints.]
-
-  Description [Allocates a two-dimensional matrix of ints.
-  Returns the pointer to the matrix if successful; NULL otherwise.]
-
-  SideEffects [None]
-
-  SeeAlso     [freeMatrix]
-
-******************************************************************************/
-static DdHalfWord **
-getMatrix(
-  int  rows /* number of rows */,
-  int  cols /* number of columns */)
-{
-    DdHalfWord **matrix;
-    int i;
-
-    if (cols*rows == 0) return(NULL);
-    matrix = ALLOC(DdHalfWord *, rows);
-    if (matrix == NULL) return(NULL);
-    matrix[0] = ALLOC(DdHalfWord, cols*rows);
-    if (matrix[0] == NULL) return(NULL);
-    for (i = 1; i < rows; i++) {
-    matrix[i] = matrix[i-1] + cols;
-    }
-    return(matrix);
-
-} /* end of getMatrix */
-
-
-/**Function********************************************************************
-
-  Synopsis    [Frees a two-dimensional matrix allocated by getMatrix.]
-
-  Description []
-
-  SideEffects [None]
-
-  SeeAlso     [getMatrix]
-
-******************************************************************************/
-static void
-freeMatrix(
-  DdHalfWord ** matrix)
-{
-    FREE(matrix[0]);
-    FREE(matrix);
-    return;
-
-} /* end of freeMatrix */
-
-
-/**Function********************************************************************
-
-  Synopsis    [Returns the number of nodes at one level of a unique table.]
-
-  Description [Returns the number of nodes at one level of a unique table.
-  The projection function, if isolated, is not counted.]
-
-  SideEffects [None]
-
-  SeeAlso []
-
-******************************************************************************/
-static int
-getLevelKeys(
-  DdManager * table,
-  int  l)
-{
-    int isolated;
-    int x;        /* x is an index */
-
-    x = table->invperm[l];
-    isolated = table->vars[x]->ref == 1;
-
-    return(table->subtables[l].keys - isolated);
-
-} /* end of getLevelKeys */
-
-
-/**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,
-  DdHalfWord * permutation,
-  int  lower,
-  int  upper)
-{
-    DdHalfWord    index;
-    int        level;
-    int        position;
-    int        numvars;
-    int        result;
-#ifdef DD_STATS
-    long    localTime;
-    int        initialSize;
-#ifdef DD_VERBOSE
-    int        finalSize;
-#endif
-    int        previousSize;
-#endif
-
-#ifdef DD_STATS
-    localTime = util_cpu_time();
-    initialSize = table->keys - table->isolated;
-#endif
-
-    numvars = table->size;
-
-#if 0
-    (void) fprintf(table->out,"%d:", ddTotalShuffles);
-    for (level = 0; level < numvars; level++) {
-    (void) fprintf(table->out," %d", table->invperm[level]);
-    }
-    (void) fprintf(table->out,"\n");
-#endif
-
-    for (level = 0; level <= upper - lower; level++) {
-    index = permutation[level];
-    position = table->perm[index];
-#ifdef DD_STATS
-    previousSize = table->keys - table->isolated;
-#endif
-    result = ddSiftUp(table,position,level+lower);
-    if (!result) return(0);
-    }
-
-#ifdef DD_STATS
-    ddTotalShuffles++;
-#ifdef DD_VERBOSE
-    finalSize = table->keys - table->isolated;
-    if (finalSize < initialSize) {
-    (void) fprintf(table->out,"-");
-    } else if (finalSize > initialSize) {
-    (void) fprintf(table->out,"+");
-    } else {
-    (void) fprintf(table->out,"=");
-    }
-    if ((ddTotalShuffles & 63) == 0) (void) fprintf(table->out,"\n");
-    fflush(table->out);
-#endif
-#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    [Updates the upper bound and saves the best order seen so far.]
-
-  Description [Updates the upper bound and saves the best order seen so far.
-  Returns the current value of the upper bound.]
-
-  SideEffects [None]
-
-  SeeAlso     []
-
-******************************************************************************/
-static int
-updateUB(
-  DdManager * table,
-  int  oldBound,
-  DdHalfWord * bestOrder,
-  int  lower,
-  int  upper)
-{
-    int i;
-    int newBound = table->keys - table->isolated;
-
-    if (newBound < oldBound) {
-#ifdef DD_STATS
-    (void) fprintf(table->out,"New upper bound = %d\n", newBound);
-    fflush(table->out);
-#endif
-    for (i = lower; i <= upper; i++)
-        bestOrder[i-lower] = (DdHalfWord) table->invperm[i];
-    return(newBound);
-    } else {
-    return(oldBound);
-    }
-
-} /* end of updateUB */
-
-
-/**Function********************************************************************
-
-  Synopsis    [Counts the number of roots.]
-
-  Description [Counts the number of roots at the levels between lower and
-  upper.  The computation is based on breadth-first search.
-  A node is a root if it is not reachable from any previously visited node.
-  (All the nodes at level lower are therefore considered roots.)
-  The visited flag uses the LSB of the next pointer.  Returns the root
-  count. The roots that are constant nodes are always ignored.]
-
-  SideEffects [None]
-
-  SeeAlso     [ddClearGlobal]
-
-******************************************************************************/
-static int
-ddCountRoots(
-  DdManager * table,
-  int  lower,
-  int  upper)
-{
-    int i,j;
-    DdNode *f;
-    DdNodePtr *nodelist;
-    DdNode *sentinel = &(table->sentinel);
-    int slots;
-    int roots = 0;
-    int maxlevel = lower;
-
-    for (i = lower; i <= upper; i++) {
-    nodelist = table->subtables[i].nodelist;
-    slots = table->subtables[i].slots;
-    for (j = 0; j < slots; j++) {
-        f = nodelist[j];
-        while (f != sentinel) {
-        /* A node is a root of the DAG if it cannot be
-        ** reached by nodes above it. If a node was never
-        ** reached during the previous depth-first searches,
-        ** then it is a root, and we start a new depth-first
-        ** search from it.
-        */
-        if (!Cudd_IsComplement(f->next)) {
-            if (f != table->vars[f->index]) {
-            roots++;
-            }
-        }
-        if (!Cudd_IsConstant(cuddT(f))) {
-            cuddT(f)->next = Cudd_Complement(cuddT(f)->next);
-            if (table->perm[cuddT(f)->index] > maxlevel)
-            maxlevel = table->perm[cuddT(f)->index];
-        }
-        if (!Cudd_IsConstant(cuddE(f))) {
-            Cudd_Regular(cuddE(f))->next =
-            Cudd_Complement(Cudd_Regular(cuddE(f))->next);
-            if (table->perm[Cudd_Regular(cuddE(f))->index] > maxlevel)
-            maxlevel = table->perm[Cudd_Regular(cuddE(f))->index];
-        }
-        f = Cudd_Regular(f->next);
-        }
-    }
-    }
-    ddClearGlobal(table, lower, maxlevel);
-
-    return(roots);
-
-} /* end of ddCountRoots */
-
-
-/**Function********************************************************************
-
-  Synopsis    [Scans the DD and clears the LSB of the next pointers.]
-
-  Description [Scans the DD and clears the LSB of the next pointers.
-  The LSB of the next pointers are used as markers to tell whether a
-  node was reached. Once the roots are counted, these flags are
-  reset.]
-
-  SideEffects [None]
-
-  SeeAlso     [ddCountRoots]
-
-******************************************************************************/
-static void
-ddClearGlobal(
-  DdManager * table,
-  int  lower,
-  int  maxlevel)
-{
-    int i,j;
-    DdNode *f;
-    DdNodePtr *nodelist;
-    DdNode *sentinel = &(table->sentinel);
-    int slots;
-
-    for (i = lower; i <= maxlevel; i++) {
-    nodelist = table->subtables[i].nodelist;
-    slots = table->subtables[i].slots;
-    for (j = 0; j < slots; j++) {
-        f = nodelist[j];
-        while (f != sentinel) {
-        f->next = Cudd_Regular(f->next);
-        f = f->next;
-        }
-    }
-    }
-
-} /* end of ddClearGlobal */
-
-
-/**Function********************************************************************
-
-  Synopsis    [Computes a lower bound on the size of a BDD.]
-
-  Description [Computes a lower bound on the size of a BDD from the
-  following factors:
-  <ul>
-  <li> size of the lower part of it;
-  <li> size of the part of the upper part not subjected to reordering;
-  <li> number of roots in the part of the BDD subjected to reordering;
-  <li> variable in the support of the roots in the upper part of the
-       BDD subjected to reordering.
-  <ul/>]
-
-  SideEffects [None]
-
-  SeeAlso     []
-
-******************************************************************************/
-static int
-computeLB(
-  DdManager * table        /* manager */,
-  DdHalfWord * order        /* optimal order for the subset */,
-  int  roots            /* roots between lower and upper */,
-  int  cost            /* minimum cost for the subset */,
-  int  lower            /* lower level to be reordered */,
-  int  upper            /* upper level to be reordered */,
-  int  level            /* offset for the current top bottom var */
-  )
-{
-    int i;
-    int lb = cost;
-    int lb1 = 0;
-    int lb2;
-    int support;
-    DdHalfWord ref;
-
-    /* The levels not involved in reordering are not going to change.
-    ** Add their sizes to the lower bound.
-    */
-    for (i = 0; i < lower; i++) {
-    lb += getLevelKeys(table,i);
-    }
-    /* If a variable is in the support, then there is going
-    ** to be at least one node labeled by that variable.
-    */
-    for (i = lower; i <= lower+level; i++) {
-    support = table->subtables[i].keys > 1 ||
-        table->vars[order[i-lower]]->ref > 1;
-    lb1 += support;
-    }
-
-    /* Estimate the number of nodes required to connect the roots to
-    ** the nodes in the bottom part. */
-    if (lower+level+1 < table->size) {
-    if (lower+level < upper)
-        ref = table->vars[order[level+1]]->ref;
-    else
-        ref = table->vars[table->invperm[upper+1]]->ref;
-    lb2 = table->subtables[lower+level+1].keys -
-        (ref > (DdHalfWord) 1) - roots;
-    } else {
-    lb2 = 0;
-    }
-
-    lb += lb1 > lb2 ? lb1 : lb2;
-
-    return(lb);
-
-} /* end of computeLB */
-
-
-/**Function********************************************************************
-
-  Synopsis    [Updates entry for a subset.]
-
-  Description [Updates entry for a subset. Finds the subset, if it exists.
-  If the new order for the subset has lower cost, or if the subset did not
-  exist, it stores the new order and cost. Returns the number of subsets
-  currently in the table.]
-
-  SideEffects [None]
-
-  SeeAlso     []
-
-******************************************************************************/
-static int
-updateEntry(
-  DdManager * table,
-  DdHalfWord * order,
-  int  level,
-  int  cost,
-  DdHalfWord ** orders,
-  int * costs,
-  int  subsets,
-  char * mask,
-  int  lower,
-  int  upper)
-{
-    int i, j;
-    int size = upper - lower + 1;
-
-    /* Build a mask that says what variables are in this subset. */
-    for (i = lower; i <= upper; i++)
-    mask[table->invperm[i]] = 0;
-    for (i = level; i < size; i++)
-    mask[order[i]] = 1;
-
-    /* Check each subset until a match is found or all subsets are examined. */
-    for (i = 0; i < subsets; i++) {
-    DdHalfWord *subset = orders[i];
-    for (j = level; j < size; j++) {
-        if (mask[subset[j]] == 0)
-        break;
-    }
-    if (j == size)        /* no mismatches: success */
-        break;
-    }
-    if (i == subsets || cost < costs[i]) {        /* add or replace */
-    for (j = 0; j < size; j++)
-        orders[i][j] = order[j];
-    costs[i] = cost;
-    subsets += (i == subsets);
-    }
-    return(subsets);
-
-} /* end of updateEntry */
-
-
-/**Function********************************************************************
-
-  Synopsis    [Pushes a variable in the order down to position "level."]
-
-  Description []
-
-  SideEffects [None]
-
-  SeeAlso     []
-
-******************************************************************************/
-static void
-pushDown(
-  DdHalfWord * order,
-  int  j,
-  int  level)
-{
-    int i;
-    DdHalfWord tmp;
-
-    tmp = order[j];
-    for (i = j; i < level; i++) {
-    order[i] = order[i+1];
-    }
-    order[level] = tmp;
-    return;
-
-} /* end of pushDown */
-
-
-/**Function********************************************************************
-
-  Synopsis    [Gathers symmetry information.]
-
-  Description [Translates the symmetry information stored in the next
-  field of each subtable from level to indices. This procedure is called
-  immediately after symmetric sifting, so that the next fields are correct.
-  By translating this informaton in terms of indices, we make it independent
-  of subsequent reorderings. The format used is that of the next fields:
-  a circular list where each variable points to the next variable in the
-  same symmetry group. Only the entries between lower and upper are
-  considered.  The procedure returns a pointer to an array
-  holding the symmetry information if successful; NULL otherwise.]
-
-  SideEffects [None]
-
-  SeeAlso     [checkSymmInfo]
-
-******************************************************************************/
-static DdHalfWord *
-initSymmInfo(
-  DdManager * table,
-  int  lower,
-  int  upper)
-{
-    int level, index, next, nextindex;
-    DdHalfWord *symmInfo;
-
-    symmInfo =  ALLOC(DdHalfWord, table->size);
-    if (symmInfo == NULL) return(NULL);
-
-    for (level = lower; level <= upper; level++) {
-    index = table->invperm[level];
-    next =  table->subtables[level].next;
-    nextindex = table->invperm[next];
-    symmInfo[index] = nextindex;
-    }
-    return(symmInfo);
-
-} /* end of initSymmInfo */
-
-
-/**Function********************************************************************
-
-  Synopsis    [Check symmetry condition.]
-
-  Description [Returns 1 if a variable is the one with the highest index
-  among those belonging to a symmetry group that are in the top part of
-  the BDD.  The top part is given by level.]
-
-  SideEffects [None]
-
-  SeeAlso     [initSymmInfo]
-
-******************************************************************************/
-static int
-checkSymmInfo(
-  DdManager * table,
-  DdHalfWord * symmInfo,
-  int  index,
-  int  level)
-{
-    int i;
-
-    i = symmInfo[index];
-    while (i != index) {
-    if (index < i && table->perm[i] <= level)
-        return(0);
-    i = symmInfo[i];
-    }
-    return(1);
-
-} /* end of checkSymmInfo */
-