summaryrefslogtreecommitdiffstats
path: root/src/bdd/cudd/cuddExact.c
diff options
context:
space:
mode:
Diffstat (limited to 'src/bdd/cudd/cuddExact.c')
-rw-r--r--src/bdd/cudd/cuddExact.c1004
1 files changed, 1004 insertions, 0 deletions
diff --git a/src/bdd/cudd/cuddExact.c b/src/bdd/cudd/cuddExact.c
new file mode 100644
index 00000000..6a81406b
--- /dev/null
+++ b/src/bdd/cudd/cuddExact.c
@@ -0,0 +1,1004 @@
+/**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.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 */
+
generated by cgit v1.2.3 (git 2.25.1) at 2024-06-30 22:14:42 +0000