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.c527
1 files changed, 273 insertions, 254 deletions
diff --git a/src/bdd/cudd/cuddExact.c b/src/bdd/cudd/cuddExact.c
index b9ed4676..19fcbcd4 100644
--- a/src/bdd/cudd/cuddExact.c
+++ b/src/bdd/cudd/cuddExact.c
@@ -7,36 +7,63 @@
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>
+ <ul>
+ </ul>
+ Internal procedures included in this module:
+ <ul>
+ <li> cuddExact()
+ </ul>
+ Static procedures included in this module:
+ <ul>
<li> getMaxBinomial()
- <li> gcd()
+ <li> gcd()
<li> getMatrix()
- <li> freeMatrix()
+ <li> freeMatrix()
<li> getLevelKeys()
<li> ddShuffle()
<li> ddSiftUp()
- <li> updateUB()
- <li> ddCountRoots()
- <li> ddClearGlobal()
- <li> computeLB()
- <li> updateEntry()
- <li> pushDown()
- <li> initSymmInfo()
+ <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.]
+ Copyright [Copyright (c) 1995-2004, Regents of the University of Colorado
+
+ All rights reserved.
+
+ Redistribution and use in source and binary forms, with or without
+ modification, are permitted provided that the following conditions
+ are met:
+
+ Redistributions of source code must retain the above copyright
+ notice, this list of conditions and the following disclaimer.
+
+ Redistributions in binary form must reproduce the above copyright
+ notice, this list of conditions and the following disclaimer in the
+ documentation and/or other materials provided with the distribution.
+
+ Neither the name of the University of Colorado nor the names of its
+ contributors may be used to endorse or promote products derived from
+ this software without specific prior written permission.
+
+ THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS
+ "AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT
+ LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS
+ FOR A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE
+ COPYRIGHT OWNER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT,
+ INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING,
+ BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES;
+ LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER
+ CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT
+ LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN
+ ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE
+ POSSIBILITY OF SUCH DAMAGE.]
******************************************************************************/
@@ -46,6 +73,7 @@
ABC_NAMESPACE_IMPL_START
+
/*---------------------------------------------------------------------------*/
/* Constant declarations */
/*---------------------------------------------------------------------------*/
@@ -64,7 +92,7 @@ ABC_NAMESPACE_IMPL_START
/*---------------------------------------------------------------------------*/
#ifndef lint
-static char rcsid[] DD_UNUSED = "$Id: cuddExact.c,v 1.1.1.1 2003/02/24 22:23:52 wjiang Exp $";
+static char rcsid[] DD_UNUSED = "$Id: cuddExact.c,v 1.28 2009/02/19 16:19:19 fabio Exp $";
#endif
#ifdef DD_STATS
@@ -81,21 +109,20 @@ static int ddTotalShuffles;
/* 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));
+static int getMaxBinomial (int n);
+static DdHalfWord ** getMatrix (int rows, int cols);
+static void freeMatrix (DdHalfWord **matrix);
+static int getLevelKeys (DdManager *table, int l);
+static int ddShuffle (DdManager *table, DdHalfWord *permutation, int lower, int upper);
+static int ddSiftUp (DdManager *table, int x, int xLow);
+static int updateUB (DdManager *table, int oldBound, DdHalfWord *bestOrder, int lower, int upper);
+static int ddCountRoots (DdManager *table, int lower, int upper);
+static void ddClearGlobal (DdManager *table, int lower, int maxlevel);
+static int computeLB (DdManager *table, DdHalfWord *order, int roots, int cost, int lower, int upper, int level);
+static int updateEntry (DdManager *table, DdHalfWord *order, int level, int cost, DdHalfWord **orders, int *costs, int subsets, char *mask, int lower, int upper);
+static void pushDown (DdHalfWord *order, int j, int level);
+static DdHalfWord * initSymmInfo (DdManager *table, int lower, int upper);
+static int checkSymmInfo (DdManager *table, DdHalfWord *symmInfo, int index, int level);
/**AutomaticEnd***************************************************************/
@@ -131,7 +158,7 @@ cuddExact(
int k, i, j;
int maxBinomial, oldSubsets, newSubsets;
int subsetCost;
- int size; /* number of variables to be reordered */
+ int size; /* number of variables to be reordered */
int unused, nvars, level, result;
int upperBound, lowerBound, cost;
int roots;
@@ -152,13 +179,13 @@ cuddExact(
/* 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++;
+ 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--;
+ 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
@@ -179,9 +206,9 @@ cuddExact(
** 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++;
+ 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. */
@@ -218,65 +245,65 @@ cuddExact(
*/
oldSubsets = 1;
for (i = 0; i < size; i++) {
- oldOrder[0][i] = bestOrder[i] = (DdHalfWord) table->invperm[i+lower];
+ 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);
+ 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);
+#ifdef 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;
+ 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;
+ ddTotalSubsets += newSubsets;
#endif
- oldSubsets = newSubsets;
+ oldSubsets = newSubsets;
}
result = ddShuffle(table, bestOrder, lower, upper);
if (result == 0) goto cuddExactOutOfMem;
@@ -285,9 +312,9 @@ cuddExact(
(void) fprintf(table->out,"\n");
#endif
(void) fprintf(table->out,"#:S_EXACT %8d: total subsets\n",
- ddTotalSubsets);
+ ddTotalSubsets);
(void) fprintf(table->out,"#:H_EXACT %8d: total shuffles",
- ddTotalShuffles);
+ ddTotalShuffles);
#endif
freeMatrix(newOrder);
@@ -320,9 +347,12 @@ cuddExactOutOfMem:
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.]
+ (n-1)/2 when n is odd. The algorithm used in this procedure avoids
+ intermediate overflow problems. It is based on the identity
+ <pre>
+ binomial(n,k) = n/k * binomial(n-1,k-1).
+ </pre>
+ Returns the computed value if successful; -1 if out of range.]
SideEffects [None]
@@ -331,42 +361,24 @@ cuddExactOutOfMem:
******************************************************************************/
static int
getMaxBinomial(
- int n)
+ int n)
{
- int *numerator;
- int i, j, k, y, g, result;
-
- k = (n & ~1) >> 1;
-
- numerator = ABC_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;
- }
- }
- }
+ double i, j, result;
+
+ if (n < 0 || n > 33) return(-1); /* error */
+ if (n < 2) return(1);
- result = 1;
- for (i = 0; i < k; i++)
- result *= numerator[i];
+ for (result = (double)((n+3)/2), i = result+1, j=2; i <= n; i++, j++) {
+ result *= i;
+ result /= j;
+ }
- ABC_FREE(numerator);
- return(result);
+ return((int)result);
-} /* end of getMaxBinomial */
+} /* end of getMaxBinomial */
+#if 0
/**Function********************************************************************
Synopsis [Returns the gcd of two integers.]
@@ -393,33 +405,34 @@ gcd(
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;
+ 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 {
- 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;
+ if (b & lsbMask) { /* a even, b odd */
+ a >>= 1;
+ } else { /* both even */
+ lsbMask <<= 1;
+ }
}
}
- }
return(a);
} /* end of gcd */
+#endif
/**Function********************************************************************
@@ -446,9 +459,12 @@ getMatrix(
matrix = ABC_ALLOC(DdHalfWord *, rows);
if (matrix == NULL) return(NULL);
matrix[0] = ABC_ALLOC(DdHalfWord, cols*rows);
- if (matrix[0] == NULL) return(NULL);
+ if (matrix[0] == NULL) {
+ ABC_FREE(matrix);
+ return(NULL);
+ }
for (i = 1; i < rows; i++) {
- matrix[i] = matrix[i-1] + cols;
+ matrix[i] = matrix[i-1] + cols;
}
return(matrix);
@@ -528,18 +544,20 @@ ddShuffle(
int lower,
int upper)
{
- DdHalfWord index;
- int level;
- int position;
- int numvars;
- int result;
+ DdHalfWord index;
+ int level;
+ int position;
+#if 0
+ int numvars;
+#endif
+ int result;
#ifdef DD_STATS
- long localTime;
- int initialSize;
+ long localTime;
+ int initialSize;
#ifdef DD_VERBOSE
- int finalSize;
+ int finalSize;
#endif
- int previousSize;
+ int previousSize;
#endif
#ifdef DD_STATS
@@ -547,24 +565,24 @@ ddShuffle(
initialSize = table->keys - table->isolated;
#endif
+#if 0
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," %d", table->invperm[level]);
}
(void) fprintf(table->out,"\n");
#endif
for (level = 0; level <= upper - lower; level++) {
- index = permutation[level];
- position = table->perm[index];
+ index = permutation[level];
+ position = table->perm[index];
#ifdef DD_STATS
- previousSize = table->keys - table->isolated;
+ previousSize = table->keys - table->isolated;
#endif
- result = ddSiftUp(table,position,level+lower);
- if (!result) return(0);
+ result = ddSiftUp(table,position,level+lower);
+ if (!result) return(0);
}
#ifdef DD_STATS
@@ -572,11 +590,11 @@ ddShuffle(
#ifdef DD_VERBOSE
finalSize = table->keys - table->isolated;
if (finalSize < initialSize) {
- (void) fprintf(table->out,"-");
+ (void) fprintf(table->out,"-");
} else if (finalSize > initialSize) {
- (void) fprintf(table->out,"+");
+ (void) fprintf(table->out,"+");
} else {
- (void) fprintf(table->out,"=");
+ (void) fprintf(table->out,"=");
}
if ((ddTotalShuffles & 63) == 0) (void) fprintf(table->out,"\n");
fflush(table->out);
@@ -612,12 +630,12 @@ ddSiftUp(
y = cuddNextLow(table,x);
while (y >= xLow) {
- size = cuddSwapInPlace(table,y,x);
- if (size == 0) {
- return(0);
- }
- x = y;
- y = cuddNextLow(table,x);
+ size = cuddSwapInPlace(table,y,x);
+ if (size == 0) {
+ return(0);
+ }
+ x = y;
+ y = cuddNextLow(table,x);
}
return(1);
@@ -649,14 +667,14 @@ updateUB(
if (newBound < oldBound) {
#ifdef DD_STATS
- (void) fprintf(table->out,"New upper bound = %d\n", newBound);
- fflush(table->out);
+ (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);
+ for (i = lower; i <= upper; i++)
+ bestOrder[i-lower] = (DdHalfWord) table->invperm[i];
+ return(newBound);
} else {
- return(oldBound);
+ return(oldBound);
}
} /* end of updateUB */
@@ -693,36 +711,36 @@ ddCountRoots(
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++;
+ 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);
}
}
- 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);
@@ -758,16 +776,16 @@ ddClearGlobal(
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;
+ 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 */
@@ -793,13 +811,13 @@ ddClearGlobal(
******************************************************************************/
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 */
+ 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;
@@ -813,28 +831,28 @@ computeLB(
** Add their sizes to the lower bound.
*/
for (i = 0; i < lower; i++) {
- lb += getLevelKeys(table,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;
+ 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;
+ 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;
+ lb2 = 0;
}
lb += lb1 > lb2 ? lb1 : lb2;
@@ -876,25 +894,25 @@ updateEntry(
/* Build a mask that says what variables are in this subset. */
for (i = lower; i <= upper; i++)
- mask[table->invperm[i]] = 0;
+ mask[table->invperm[i]] = 0;
for (i = level; i < size; i++)
- mask[order[i]] = 1;
+ 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;
+ 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);
+ 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);
@@ -923,7 +941,7 @@ pushDown(
tmp = order[j];
for (i = j; i < level; i++) {
- order[i] = order[i+1];
+ order[i] = order[i+1];
}
order[level] = tmp;
return;
@@ -963,10 +981,10 @@ initSymmInfo(
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;
+ index = table->invperm[level];
+ next = table->subtables[level].next;
+ nextindex = table->invperm[next];
+ symmInfo[index] = nextindex;
}
return(symmInfo);
@@ -997,13 +1015,14 @@ checkSymmInfo(
i = symmInfo[index];
while (i != index) {
- if (index < i && table->perm[i] <= level)
- return(0);
- i = symmInfo[i];
+ if (index < i && table->perm[i] <= level)
+ return(0);
+ i = symmInfo[i];
}
return(1);
} /* end of checkSymmInfo */
+
ABC_NAMESPACE_IMPL_END
generated by cgit v1.2.3 (git 2.25.1) at 2024-07-15 21:03:35 +0000