diff options
Diffstat (limited to 'src/bdd/cudd/cuddExact.c')
-rw-r--r-- | src/bdd/cudd/cuddExact.c | 1004 |
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 */ - |