diff options
Diffstat (limited to 'src/bdd/cudd/cuddZddReord.c')
| -rw-r--r-- | src/bdd/cudd/cuddZddReord.c | 1633 |
1 files changed, 0 insertions, 1633 deletions
diff --git a/src/bdd/cudd/cuddZddReord.c b/src/bdd/cudd/cuddZddReord.c deleted file mode 100644 index e2da37f2..00000000 --- a/src/bdd/cudd/cuddZddReord.c +++ /dev/null @@ -1,1633 +0,0 @@ -/**CFile*********************************************************************** - - FileName [cuddZddReord.c] - - PackageName [cudd] - - Synopsis [Procedures for dynamic variable ordering of ZDDs.] - - Description [External procedures included in this module: - <ul> - <li> Cudd_zddReduceHeap() - <li> Cudd_zddShuffleHeap() - </ul> - Internal procedures included in this module: - <ul> - <li> cuddZddAlignToBdd() - <li> cuddZddNextHigh() - <li> cuddZddNextLow() - <li> cuddZddUniqueCompare() - <li> cuddZddSwapInPlace() - <li> cuddZddSwapping() - <li> cuddZddSifting() - </ul> - Static procedures included in this module: - <ul> - <li> zddSwapAny() - <li> cuddZddSiftingAux() - <li> cuddZddSiftingUp() - <li> cuddZddSiftingDown() - <li> cuddZddSiftingBackward() - <li> zddReorderPreprocess() - <li> zddReorderPostprocess() - <li> zddShuffle() - <li> zddSiftUp() - </ul> - ] - - SeeAlso [] - - Author [Hyong-Kyoon Shin, In-Ho Moon] - - 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 */ -/*---------------------------------------------------------------------------*/ - -#define DD_MAX_SUBTABLE_SPARSITY 8 -#define DD_SHRINK_FACTOR 2 - -/*---------------------------------------------------------------------------*/ -/* Stucture declarations */ -/*---------------------------------------------------------------------------*/ - - -/*---------------------------------------------------------------------------*/ -/* Type declarations */ -/*---------------------------------------------------------------------------*/ - - -/*---------------------------------------------------------------------------*/ -/* Variable declarations */ -/*---------------------------------------------------------------------------*/ - -#ifndef lint -static char rcsid[] DD_UNUSED = "$Id: cuddZddReord.c,v 1.1.1.1 2003/02/24 22:23:54 wjiang Exp $"; -#endif - -int *zdd_entry; - -int zddTotalNumberSwapping; - -static DdNode *empty; - - -/*---------------------------------------------------------------------------*/ -/* Macro declarations */ -/*---------------------------------------------------------------------------*/ - - -/**AutomaticStart*************************************************************/ - -/*---------------------------------------------------------------------------*/ -/* Static function prototypes */ -/*---------------------------------------------------------------------------*/ - -static Move * zddSwapAny ARGS((DdManager *table, int x, int y)); -static int cuddZddSiftingAux ARGS((DdManager *table, int x, int x_low, int x_high)); -static Move * cuddZddSiftingUp ARGS((DdManager *table, int x, int x_low, int initial_size)); -static Move * cuddZddSiftingDown ARGS((DdManager *table, int x, int x_high, int initial_size)); -static int cuddZddSiftingBackward ARGS((DdManager *table, Move *moves, int size)); -static void zddReorderPreprocess ARGS((DdManager *table)); -static int zddReorderPostprocess ARGS((DdManager *table)); -static int zddShuffle ARGS((DdManager *table, int *permutation)); -static int zddSiftUp ARGS((DdManager *table, int x, int xLow)); -static void zddFixTree ARGS((DdManager *table, MtrNode *treenode)); - -/**AutomaticEnd***************************************************************/ - - -/*---------------------------------------------------------------------------*/ -/* Definition of exported functions */ -/*---------------------------------------------------------------------------*/ - - -/**Function******************************************************************** - - Synopsis [Main dynamic reordering routine for ZDDs.] - - Description [Main dynamic reordering routine for ZDDs. - Calls one of the possible reordering procedures: - <ul> - <li>Swapping - <li>Sifting - <li>Symmetric Sifting - </ul> - - For sifting and symmetric sifting it is possible to request reordering - to convergence.<p> - - The core of all methods is the reordering procedure - cuddZddSwapInPlace() which swaps two adjacent variables. - Returns 1 in case of success; 0 otherwise. In the case of symmetric - sifting (with and without convergence) returns 1 plus the number of - symmetric variables, in case of success.] - - SideEffects [Changes the variable order for all ZDDs and clears - the cache.] - -******************************************************************************/ -int -Cudd_zddReduceHeap( - DdManager * table /* DD manager */, - Cudd_ReorderingType heuristic /* method used for reordering */, - int minsize /* bound below which no reordering occurs */) -{ - DdHook *hook; - int result; - unsigned int nextDyn; -#ifdef DD_STATS - unsigned int initialSize; - unsigned int finalSize; -#endif - long localTime; - - /* Don't reorder if there are too many dead nodes. */ - if (table->keysZ - table->deadZ < (unsigned) minsize) - return(1); - - if (heuristic == CUDD_REORDER_SAME) { - heuristic = table->autoMethodZ; - } - if (heuristic == CUDD_REORDER_NONE) { - return(1); - } - - /* This call to Cudd_zddReduceHeap does initiate reordering. Therefore - ** we count it. - */ - table->reorderings++; - empty = table->zero; - - localTime = util_cpu_time(); - - /* Run the hook functions. */ - hook = table->preReorderingHook; - while (hook != NULL) { - int res = (hook->f)(table, "ZDD", (void *)heuristic); - if (res == 0) return(0); - hook = hook->next; - } - - /* Clear the cache and collect garbage. */ - zddReorderPreprocess(table); - zddTotalNumberSwapping = 0; - -#ifdef DD_STATS - initialSize = table->keysZ; - - switch(heuristic) { - case CUDD_REORDER_RANDOM: - case CUDD_REORDER_RANDOM_PIVOT: - (void) fprintf(table->out,"#:I_RANDOM "); - break; - case CUDD_REORDER_SIFT: - case CUDD_REORDER_SIFT_CONVERGE: - case CUDD_REORDER_SYMM_SIFT: - case CUDD_REORDER_SYMM_SIFT_CONV: - (void) fprintf(table->out,"#:I_SIFTING "); - break; - case CUDD_REORDER_LINEAR: - case CUDD_REORDER_LINEAR_CONVERGE: - (void) fprintf(table->out,"#:I_LINSIFT "); - break; - default: - (void) fprintf(table->err,"Unsupported ZDD reordering method\n"); - return(0); - } - (void) fprintf(table->out,"%8d: initial size",initialSize); -#endif - - result = cuddZddTreeSifting(table,heuristic); - -#ifdef DD_STATS - (void) fprintf(table->out,"\n"); - finalSize = table->keysZ; - (void) fprintf(table->out,"#:F_REORDER %8d: final size\n",finalSize); - (void) fprintf(table->out,"#:T_REORDER %8g: total time (sec)\n", - ((double)(util_cpu_time() - localTime)/1000.0)); - (void) fprintf(table->out,"#:N_REORDER %8d: total swaps\n", - zddTotalNumberSwapping); -#endif - - if (result == 0) - return(0); - - if (!zddReorderPostprocess(table)) - return(0); - - if (table->realignZ) { - if (!cuddBddAlignToZdd(table)) - return(0); - } - - nextDyn = table->keysZ * DD_DYN_RATIO; - if (table->reorderings < 20 || nextDyn > table->nextDyn) - table->nextDyn = nextDyn; - else - table->nextDyn += 20; - - table->reordered = 1; - - /* Run hook functions. */ - hook = table->postReorderingHook; - while (hook != NULL) { - int res = (hook->f)(table, "ZDD", (void *)localTime); - if (res == 0) return(0); - hook = hook->next; - } - /* Update cumulative reordering time. */ - table->reordTime += util_cpu_time() - localTime; - - return(result); - -} /* end of Cudd_zddReduceHeap */ - - -/**Function******************************************************************** - - Synopsis [Reorders ZDD variables according to given permutation.] - - Description [Reorders ZDD variables according to given permutation. - The i-th entry of the permutation array contains the index of the variable - that should be brought to the i-th level. The size of the array should be - equal or greater to the number of variables currently in use. - Returns 1 in case of success; 0 otherwise.] - - SideEffects [Changes the ZDD variable order for all diagrams and clears - the cache.] - - SeeAlso [Cudd_zddReduceHeap] - -******************************************************************************/ -int -Cudd_zddShuffleHeap( - DdManager * table /* DD manager */, - int * permutation /* required variable permutation */) -{ - - int result; - - empty = table->zero; - zddReorderPreprocess(table); - - result = zddShuffle(table,permutation); - - if (!zddReorderPostprocess(table)) return(0); - - return(result); - -} /* end of Cudd_zddShuffleHeap */ - - -/*---------------------------------------------------------------------------*/ -/* Definition of internal functions */ -/*---------------------------------------------------------------------------*/ - - -/**Function******************************************************************** - - Synopsis [Reorders ZDD variables according to the order of the BDD - variables.] - - Description [Reorders ZDD variables according to the order of the - BDD variables. This function can be called at the end of BDD - reordering to insure that the order of the ZDD variables is - consistent with the order of the BDD variables. The number of ZDD - variables must be a multiple of the number of BDD variables. Let - <code>M</code> be the ratio of the two numbers. cuddZddAlignToBdd - then considers the ZDD variables from <code>M*i</code> to - <code>(M+1)*i-1</code> as corresponding to BDD variable - <code>i</code>. This function should be normally called from - Cudd_ReduceHeap, which clears the cache. Returns 1 in case of - success; 0 otherwise.] - - SideEffects [Changes the ZDD variable order for all diagrams and performs - garbage collection of the ZDD unique table.] - - SeeAlso [Cudd_zddShuffleHeap Cudd_ReduceHeap] - -******************************************************************************/ -int -cuddZddAlignToBdd( - DdManager * table /* DD manager */) -{ - int *invpermZ; /* permutation array */ - int M; /* ratio of ZDD variables to BDD variables */ - int i,j; /* loop indices */ - int result; /* return value */ - - /* We assume that a ratio of 0 is OK. */ - if (table->sizeZ == 0) - return(1); - - empty = table->zero; - M = table->sizeZ / table->size; - /* Check whether the number of ZDD variables is a multiple of the - ** number of BDD variables. - */ - if (M * table->size != table->sizeZ) - return(0); - /* Create and initialize the inverse permutation array. */ - invpermZ = ALLOC(int,table->sizeZ); - if (invpermZ == NULL) { - table->errorCode = CUDD_MEMORY_OUT; - return(0); - } - for (i = 0; i < table->size; i++) { - int index = table->invperm[i]; - int indexZ = index * M; - int levelZ = table->permZ[indexZ]; - levelZ = (levelZ / M) * M; - for (j = 0; j < M; j++) { - invpermZ[M * i + j] = table->invpermZ[levelZ + j]; - } - } - /* Eliminate dead nodes. Do not scan the cache again, because we - ** assume that Cudd_ReduceHeap has already cleared it. - */ - cuddGarbageCollectZdd(table,0); - - result = zddShuffle(table, invpermZ); - FREE(invpermZ); - /* Fix the ZDD variable group tree. */ - zddFixTree(table,table->treeZ); - return(result); - -} /* end of cuddZddAlignToBdd */ - - -/**Function******************************************************************** - - Synopsis [Finds the next subtable with a larger index.] - - Description [Finds the next subtable with a larger index. Returns the - index.] - - SideEffects [None] - - SeeAlso [] - -******************************************************************************/ -int -cuddZddNextHigh( - DdManager * table, - int x) -{ - return(x + 1); - -} /* end of cuddZddNextHigh */ - - -/**Function******************************************************************** - - Synopsis [Finds the next subtable with a smaller index.] - - Description [Finds the next subtable with a smaller index. Returns the - index.] - - SideEffects [None] - - SeeAlso [] - -******************************************************************************/ -int -cuddZddNextLow( - DdManager * table, - int x) -{ - return(x - 1); - -} /* end of cuddZddNextLow */ - - -/**Function******************************************************************** - - Synopsis [Comparison function used by qsort.] - - Description [Comparison function used by qsort to order the - variables according to the number of keys in the subtables. - Returns the difference in number of keys between the two - variables being compared.] - - SideEffects [None] - - SeeAlso [] - -******************************************************************************/ -int -cuddZddUniqueCompare( - int * ptr_x, - int * ptr_y) -{ - return(zdd_entry[*ptr_y] - zdd_entry[*ptr_x]); - -} /* end of cuddZddUniqueCompare */ - - -/**Function******************************************************************** - - Synopsis [Swaps two adjacent variables.] - - Description [Swaps two adjacent variables. It assumes that no dead - nodes are present on entry to this procedure. The procedure then - guarantees that no dead nodes will be present when it terminates. - cuddZddSwapInPlace assumes that x < y. Returns the number of keys in - the table if successful; 0 otherwise.] - - SideEffects [None] - - SeeAlso [] - -******************************************************************************/ -int -cuddZddSwapInPlace( - DdManager * table, - int x, - int y) -{ - DdNodePtr *xlist, *ylist; - int xindex, yindex; - int xslots, yslots; - int xshift, yshift; - int oldxkeys, oldykeys; - int newxkeys, newykeys; - int i; - int posn; - DdNode *f, *f1, *f0, *f11, *f10, *f01, *f00; - DdNode *newf1, *newf0, *next; - DdNodePtr g, *lastP, *previousP; - -#ifdef DD_DEBUG - assert(x < y); - assert(cuddZddNextHigh(table,x) == y); - assert(table->subtableZ[x].keys != 0); - assert(table->subtableZ[y].keys != 0); - assert(table->subtableZ[x].dead == 0); - assert(table->subtableZ[y].dead == 0); -#endif - - zddTotalNumberSwapping++; - - /* Get parameters of x subtable. */ - xindex = table->invpermZ[x]; - xlist = table->subtableZ[x].nodelist; - oldxkeys = table->subtableZ[x].keys; - xslots = table->subtableZ[x].slots; - xshift = table->subtableZ[x].shift; - newxkeys = 0; - - yindex = table->invpermZ[y]; - ylist = table->subtableZ[y].nodelist; - oldykeys = table->subtableZ[y].keys; - yslots = table->subtableZ[y].slots; - yshift = table->subtableZ[y].shift; - newykeys = oldykeys; - - /* The nodes in the x layer that don't depend on y directly - ** will stay there; the others are put in a chain. - ** The chain is handled as a FIFO; g points to the beginning and - ** last points to the end. - */ - - g = NULL; - lastP = &g; - for (i = 0; i < xslots; i++) { - previousP = &(xlist[i]); - f = *previousP; - while (f != NULL) { - next = f->next; - f1 = cuddT(f); f0 = cuddE(f); - if ((f1->index != (DdHalfWord) yindex) && - (f0->index != (DdHalfWord) yindex)) { /* stays */ - newxkeys++; - *previousP = f; - previousP = &(f->next); - } else { - f->index = yindex; - *lastP = f; - lastP = &(f->next); - } - f = next; - } /* while there are elements in the collision chain */ - *previousP = NULL; - } /* for each slot of the x subtable */ - *lastP = NULL; - - -#ifdef DD_COUNT - table->swapSteps += oldxkeys - newxkeys; -#endif - /* Take care of the x nodes that must be re-expressed. - ** They form a linked list pointed by g. Their index has been - ** changed to yindex already. - */ - f = g; - while (f != NULL) { - next = f->next; - /* Find f1, f0, f11, f10, f01, f00. */ - f1 = cuddT(f); - if ((int) f1->index == yindex) { - f11 = cuddT(f1); f10 = cuddE(f1); - } else { - f11 = empty; f10 = f1; - } - f0 = cuddE(f); - if ((int) f0->index == yindex) { - f01 = cuddT(f0); f00 = cuddE(f0); - } else { - f01 = empty; f00 = f0; - } - - /* Decrease ref count of f1. */ - cuddSatDec(f1->ref); - /* Create the new T child. */ - if (f11 == empty) { - if (f01 != empty) { - newf1 = f01; - cuddSatInc(newf1->ref); - } - /* else case was already handled when finding nodes - ** with both children below level y - */ - } else { - /* Check xlist for triple (xindex, f11, f01). */ - posn = ddHash(f11, f01, xshift); - /* For each element newf1 in collision list xlist[posn]. */ - newf1 = xlist[posn]; - while (newf1 != NULL) { - if (cuddT(newf1) == f11 && cuddE(newf1) == f01) { - cuddSatInc(newf1->ref); - break; /* match */ - } - newf1 = newf1->next; - } /* while newf1 */ - if (newf1 == NULL) { /* no match */ - newf1 = cuddDynamicAllocNode(table); - if (newf1 == NULL) - goto zddSwapOutOfMem; - newf1->index = xindex; newf1->ref = 1; - cuddT(newf1) = f11; - cuddE(newf1) = f01; - /* Insert newf1 in the collision list xlist[pos]; - ** increase the ref counts of f11 and f01 - */ - newxkeys++; - newf1->next = xlist[posn]; - xlist[posn] = newf1; - cuddSatInc(f11->ref); - cuddSatInc(f01->ref); - } - } - cuddT(f) = newf1; - - /* Do the same for f0. */ - /* Decrease ref count of f0. */ - cuddSatDec(f0->ref); - /* Create the new E child. */ - if (f10 == empty) { - newf0 = f00; - cuddSatInc(newf0->ref); - } else { - /* Check xlist for triple (xindex, f10, f00). */ - posn = ddHash(f10, f00, xshift); - /* For each element newf0 in collision list xlist[posn]. */ - newf0 = xlist[posn]; - while (newf0 != NULL) { - if (cuddT(newf0) == f10 && cuddE(newf0) == f00) { - cuddSatInc(newf0->ref); - break; /* match */ - } - newf0 = newf0->next; - } /* while newf0 */ - if (newf0 == NULL) { /* no match */ - newf0 = cuddDynamicAllocNode(table); - if (newf0 == NULL) - goto zddSwapOutOfMem; - newf0->index = xindex; newf0->ref = 1; - cuddT(newf0) = f10; cuddE(newf0) = f00; - /* Insert newf0 in the collision list xlist[posn]; - ** increase the ref counts of f10 and f00. - */ - newxkeys++; - newf0->next = xlist[posn]; - xlist[posn] = newf0; - cuddSatInc(f10->ref); - cuddSatInc(f00->ref); - } - } - cuddE(f) = newf0; - - /* Insert the modified f in ylist. - ** The modified f does not already exists in ylist. - ** (Because of the uniqueness of the cofactors.) - */ - posn = ddHash(newf1, newf0, yshift); - newykeys++; - f->next = ylist[posn]; - ylist[posn] = f; - f = next; - } /* while f != NULL */ - - /* GC the y layer. */ - - /* For each node f in ylist. */ - for (i = 0; i < yslots; i++) { - previousP = &(ylist[i]); - f = *previousP; - while (f != NULL) { - next = f->next; - if (f->ref == 0) { - cuddSatDec(cuddT(f)->ref); - cuddSatDec(cuddE(f)->ref); - cuddDeallocNode(table, f); - newykeys--; - } else { - *previousP = f; - previousP = &(f->next); - } - f = next; - } /* while f */ - *previousP = NULL; - } /* for i */ - - /* Set the appropriate fields in table. */ - table->subtableZ[x].nodelist = ylist; - table->subtableZ[x].slots = yslots; - table->subtableZ[x].shift = yshift; - table->subtableZ[x].keys = newykeys; - table->subtableZ[x].maxKeys = yslots * DD_MAX_SUBTABLE_DENSITY; - - table->subtableZ[y].nodelist = xlist; - table->subtableZ[y].slots = xslots; - table->subtableZ[y].shift = xshift; - table->subtableZ[y].keys = newxkeys; - table->subtableZ[y].maxKeys = xslots * DD_MAX_SUBTABLE_DENSITY; - - table->permZ[xindex] = y; table->permZ[yindex] = x; - table->invpermZ[x] = yindex; table->invpermZ[y] = xindex; - - table->keysZ += newxkeys + newykeys - oldxkeys - oldykeys; - - /* Update univ section; univ[x] remains the same. */ - table->univ[y] = cuddT(table->univ[x]); - - return (table->keysZ); - -zddSwapOutOfMem: - (void) fprintf(table->err, "Error: cuddZddSwapInPlace out of memory\n"); - - return (0); - -} /* end of cuddZddSwapInPlace */ - - -/**Function******************************************************************** - - Synopsis [Reorders variables by a sequence of (non-adjacent) swaps.] - - Description [Implementation of Plessier's algorithm that reorders - variables by a sequence of (non-adjacent) swaps. - <ol> - <li> Select two variables (RANDOM or HEURISTIC). - <li> Permute these variables. - <li> If the nodes have decreased accept the permutation. - <li> Otherwise reconstruct the original heap. - <li> Loop. - </ol> - Returns 1 in case of success; 0 otherwise.] - - SideEffects [None] - - SeeAlso [] - -******************************************************************************/ -int -cuddZddSwapping( - DdManager * table, - int lower, - int upper, - Cudd_ReorderingType heuristic) -{ - int i, j; - int max, keys; - int nvars; - int x, y; - int iterate; - int previousSize; - Move *moves, *move; - int pivot; - int modulo; - int result; - -#ifdef DD_DEBUG - /* Sanity check */ - assert(lower >= 0 && upper < table->sizeZ && lower <= upper); -#endif - - nvars = upper - lower + 1; - iterate = nvars; - - for (i = 0; i < iterate; i++) { - if (heuristic == CUDD_REORDER_RANDOM_PIVOT) { - /* Find pivot <= id with maximum keys. */ - for (max = -1, j = lower; j <= upper; j++) { - if ((keys = table->subtableZ[j].keys) > max) { - max = keys; - pivot = j; - } - } - - modulo = upper - pivot; - if (modulo == 0) { - y = pivot; /* y = nvars-1 */ - } else { - /* y = random # from {pivot+1 .. nvars-1} */ - y = pivot + 1 + (int) (Cudd_Random() % modulo); - } - - modulo = pivot - lower - 1; - if (modulo < 1) { /* if pivot = 1 or 0 */ - x = lower; - } else { - do { /* x = random # from {0 .. pivot-2} */ - x = (int) Cudd_Random() % modulo; - } while (x == y); - /* Is this condition really needed, since x and y - are in regions separated by pivot? */ - } - } else { - x = (int) (Cudd_Random() % nvars) + lower; - do { - y = (int) (Cudd_Random() % nvars) + lower; - } while (x == y); - } - - previousSize = table->keysZ; - moves = zddSwapAny(table, x, y); - if (moves == NULL) - goto cuddZddSwappingOutOfMem; - - result = cuddZddSiftingBackward(table, moves, previousSize); - if (!result) - goto cuddZddSwappingOutOfMem; - - while (moves != NULL) { - move = moves->next; - cuddDeallocNode(table, (DdNode *) moves); - moves = move; - } -#ifdef DD_STATS - if (table->keysZ < (unsigned) previousSize) { - (void) fprintf(table->out,"-"); - } else if (table->keysZ > (unsigned) previousSize) { - (void) fprintf(table->out,"+"); /* should never happen */ - } else { - (void) fprintf(table->out,"="); - } - fflush(table->out); -#endif - } - - return(1); - -cuddZddSwappingOutOfMem: - while (moves != NULL) { - move = moves->next; - cuddDeallocNode(table, (DdNode *) moves); - moves = move; - } - return(0); - -} /* end of cuddZddSwapping */ - - -/**Function******************************************************************** - - Synopsis [Implementation of Rudell's sifting algorithm.] - - Description [Implementation of Rudell's sifting algorithm. - Assumes that no dead nodes are present. - <ol> - <li> Order all the variables according to the number of entries - in each unique table. - <li> Sift the variable up and down, remembering each time the - total size of the DD heap. - <li> Select the best permutation. - <li> Repeat 3 and 4 for all variables. - </ol> - Returns 1 if successful; 0 otherwise.] - - SideEffects [None] - - SeeAlso [] - -******************************************************************************/ -int -cuddZddSifting( - DdManager * table, - int lower, - int upper) -{ - int i; - int *var; - int size; - int x; - int result; -#ifdef DD_STATS - int previousSize; -#endif - - size = table->sizeZ; - - /* Find order in which to sift variables. */ - var = NULL; - zdd_entry = ALLOC(int, size); - if (zdd_entry == NULL) { - table->errorCode = CUDD_MEMORY_OUT; - goto cuddZddSiftingOutOfMem; - } - var = ALLOC(int, size); - if (var == NULL) { - table->errorCode = CUDD_MEMORY_OUT; - goto cuddZddSiftingOutOfMem; - } - - for (i = 0; i < size; i++) { - x = table->permZ[i]; - zdd_entry[i] = table->subtableZ[x].keys; - var[i] = i; - } - - qsort((void *)var, size, sizeof(int), (int (*)(const void *, const void *))cuddZddUniqueCompare); - - /* Now sift. */ - for (i = 0; i < ddMin(table->siftMaxVar, size); i++) { - if (zddTotalNumberSwapping >= table->siftMaxSwap) - break; - x = table->permZ[var[i]]; - if (x < lower || x > upper) continue; -#ifdef DD_STATS - previousSize = table->keysZ; -#endif - result = cuddZddSiftingAux(table, x, lower, upper); - if (!result) - goto cuddZddSiftingOutOfMem; -#ifdef DD_STATS - if (table->keysZ < (unsigned) previousSize) { - (void) fprintf(table->out,"-"); - } else if (table->keysZ > (unsigned) previousSize) { - (void) fprintf(table->out,"+"); /* should never happen */ - (void) fprintf(table->out,"\nSize increased from %d to %d while sifting variable %d\n", previousSize, table->keysZ , var[i]); - } else { - (void) fprintf(table->out,"="); - } - fflush(table->out); -#endif - } - - FREE(var); - FREE(zdd_entry); - - return(1); - -cuddZddSiftingOutOfMem: - - if (zdd_entry != NULL) FREE(zdd_entry); - if (var != NULL) FREE(var); - - return(0); - -} /* end of cuddZddSifting */ - - -/*---------------------------------------------------------------------------*/ -/* Definition of static functions */ -/*---------------------------------------------------------------------------*/ - - -/**Function******************************************************************** - - Synopsis [Swaps any two variables.] - - Description [Swaps any two variables. Returns the set of moves.] - - SideEffects [None] - - SeeAlso [] - -******************************************************************************/ -static Move * -zddSwapAny( - DdManager * table, - int x, - int y) -{ - Move *move, *moves; - int tmp, size; - int x_ref, y_ref; - int x_next, y_next; - int limit_size; - - if (x > y) { /* make x precede y */ - tmp = x; x = y; y = tmp; - } - - x_ref = x; y_ref = y; - - x_next = cuddZddNextHigh(table, x); - y_next = cuddZddNextLow(table, y); - moves = NULL; - limit_size = table->keysZ; - - for (;;) { - if (x_next == y_next) { /* x < x_next = y_next < y */ - size = cuddZddSwapInPlace(table, x, x_next); - if (size == 0) - goto zddSwapAnyOutOfMem; - move = (Move *) cuddDynamicAllocNode(table); - if (move == NULL) - goto zddSwapAnyOutOfMem; - move->x = x; - move->y = x_next; - move->size = size; - move->next = moves; - moves = move; - - size = cuddZddSwapInPlace(table, y_next, y); - if (size == 0) - goto zddSwapAnyOutOfMem; - move = (Move *)cuddDynamicAllocNode(table); - if (move == NULL) - goto zddSwapAnyOutOfMem; - move->x = y_next; - move->y = y; - move->size = size; - move->next = moves; - moves = move; - - size = cuddZddSwapInPlace(table, x, x_next); - if (size == 0) - goto zddSwapAnyOutOfMem; - move = (Move *)cuddDynamicAllocNode(table); - if (move == NULL) - goto zddSwapAnyOutOfMem; - move->x = x; - move->y = x_next; - move->size = size; - move->next = moves; - moves = move; - - tmp = x; x = y; y = tmp; - - } else if (x == y_next) { /* x = y_next < y = x_next */ - size = cuddZddSwapInPlace(table, x, x_next); - if (size == 0) - goto zddSwapAnyOutOfMem; - move = (Move *)cuddDynamicAllocNode(table); - if (move == NULL) - goto zddSwapAnyOutOfMem; - move->x = x; - move->y = x_next; - move->size = size; - move->next = moves; - moves = move; - - tmp = x; x = y; y = tmp; - } else { - size = cuddZddSwapInPlace(table, x, x_next); - if (size == 0) - goto zddSwapAnyOutOfMem; - move = (Move *)cuddDynamicAllocNode(table); - if (move == NULL) - goto zddSwapAnyOutOfMem; - move->x = x; - move->y = x_next; - move->size = size; - move->next = moves; - moves = move; - - size = cuddZddSwapInPlace(table, y_next, y); - if (size == 0) - goto zddSwapAnyOutOfMem; - move = (Move *)cuddDynamicAllocNode(table); - if (move == NULL) - goto zddSwapAnyOutOfMem; - move->x = y_next; - move->y = y; - move->size = size; - move->next = moves; - moves = move; - - x = x_next; y = y_next; - } - - x_next = cuddZddNextHigh(table, x); - y_next = cuddZddNextLow(table, y); - if (x_next > y_ref) - break; /* if x == y_ref */ - - if ((double) size > table->maxGrowth * (double) limit_size) - break; - if (size < limit_size) - limit_size = size; - } - if (y_next >= x_ref) { - size = cuddZddSwapInPlace(table, y_next, y); - if (size == 0) - goto zddSwapAnyOutOfMem; - move = (Move *)cuddDynamicAllocNode(table); - if (move == NULL) - goto zddSwapAnyOutOfMem; - move->x = y_next; - move->y = y; - move->size = size; - move->next = moves; - moves = move; - } - - return(moves); - -zddSwapAnyOutOfMem: - while (moves != NULL) { - move = moves->next; - cuddDeallocNode(table, (DdNode *)moves); - moves = move; - } - return(NULL); - -} /* end of zddSwapAny */ - - -/**Function******************************************************************** - - Synopsis [Given xLow <= x <= xHigh moves x up and down between the - boundaries.] - - Description [Given xLow <= x <= xHigh moves x up and down between the - boundaries. Finds the best position and does the required changes. - Returns 1 if successful; 0 otherwise.] - - SideEffects [None] - - SeeAlso [] - -******************************************************************************/ -static int -cuddZddSiftingAux( - DdManager * table, - int x, - int x_low, - int x_high) -{ - Move *move; - Move *moveUp; /* list of up move */ - Move *moveDown; /* list of down move */ - - int initial_size; - int result; - - initial_size = table->keysZ; - -#ifdef DD_DEBUG - assert(table->subtableZ[x].keys > 0); -#endif - - moveDown = NULL; - moveUp = NULL; - - if (x == x_low) { - moveDown = cuddZddSiftingDown(table, x, x_high, initial_size); - /* after that point x --> x_high */ - if (moveDown == NULL) - goto cuddZddSiftingAuxOutOfMem; - result = cuddZddSiftingBackward(table, moveDown, - initial_size); - /* move backward and stop at best position */ - if (!result) - goto cuddZddSiftingAuxOutOfMem; - - } - else if (x == x_high) { - moveUp = cuddZddSiftingUp(table, x, x_low, initial_size); - /* after that point x --> x_low */ - if (moveUp == NULL) - goto cuddZddSiftingAuxOutOfMem; - result = cuddZddSiftingBackward(table, moveUp, initial_size); - /* move backward and stop at best position */ - if (!result) - goto cuddZddSiftingAuxOutOfMem; - } - else if ((x - x_low) > (x_high - x)) { - /* must go down first:shorter */ - moveDown = cuddZddSiftingDown(table, x, x_high, initial_size); - /* after that point x --> x_high */ - if (moveDown == NULL) - goto cuddZddSiftingAuxOutOfMem; - moveUp = cuddZddSiftingUp(table, moveDown->y, x_low, - initial_size); - if (moveUp == NULL) - goto cuddZddSiftingAuxOutOfMem; - result = cuddZddSiftingBackward(table, moveUp, initial_size); - /* move backward and stop at best position */ - if (!result) - goto cuddZddSiftingAuxOutOfMem; - } - else { - moveUp = cuddZddSiftingUp(table, x, x_low, initial_size); - /* after that point x --> x_high */ - if (moveUp == NULL) - goto cuddZddSiftingAuxOutOfMem; - moveDown = cuddZddSiftingDown(table, moveUp->x, x_high, - initial_size); - /* then move up */ - if (moveDown == NULL) - goto cuddZddSiftingAuxOutOfMem; - result = cuddZddSiftingBackward(table, moveDown, - initial_size); - /* move backward and stop at best position */ - if (!result) - goto cuddZddSiftingAuxOutOfMem; - } - - while (moveDown != NULL) { - move = moveDown->next; - cuddDeallocNode(table, (DdNode *)moveDown); - moveDown = move; - } - while (moveUp != NULL) { - move = moveUp->next; - cuddDeallocNode(table, (DdNode *)moveUp); - moveUp = move; - } - - return(1); - -cuddZddSiftingAuxOutOfMem: - while (moveDown != NULL) { - move = moveDown->next; - cuddDeallocNode(table, (DdNode *)moveDown); - moveDown = move; - } - while (moveUp != NULL) { - move = moveUp->next; - cuddDeallocNode(table, (DdNode *)moveUp); - moveUp = move; - } - - return(0); - -} /* end of cuddZddSiftingAux */ - - -/**Function******************************************************************** - - Synopsis [Sifts a variable up.] - - Description [Sifts a variable up. Moves y up until either it reaches - the bound (x_low) or the size of the ZDD heap increases too much. - Returns the set of moves in case of success; NULL if memory is full.] - - SideEffects [None] - - SeeAlso [] - -******************************************************************************/ -static Move * -cuddZddSiftingUp( - DdManager * table, - int x, - int x_low, - int initial_size) -{ - Move *moves; - Move *move; - int y; - int size; - int limit_size = initial_size; - - moves = NULL; - y = cuddZddNextLow(table, x); - while (y >= x_low) { - size = cuddZddSwapInPlace(table, y, x); - if (size == 0) - goto cuddZddSiftingUpOutOfMem; - move = (Move *)cuddDynamicAllocNode(table); - if (move == NULL) - goto cuddZddSiftingUpOutOfMem; - move->x = y; - move->y = x; - move->size = size; - move->next = moves; - moves = move; - - if ((double)size > (double)limit_size * table->maxGrowth) - break; - if (size < limit_size) - limit_size = size; - - x = y; - y = cuddZddNextLow(table, x); - } - return(moves); - -cuddZddSiftingUpOutOfMem: - while (moves != NULL) { - move = moves->next; - cuddDeallocNode(table, (DdNode *)moves); - moves = move; - } - return(NULL); - -} /* end of cuddZddSiftingUp */ - - -/**Function******************************************************************** - - Synopsis [Sifts a variable down.] - - Description [Sifts a variable down. Moves x down until either it - reaches the bound (x_high) or the size of the ZDD heap increases too - much. Returns the set of moves in case of success; NULL if memory is - full.] - - SideEffects [None] - - SeeAlso [] - -******************************************************************************/ -static Move * -cuddZddSiftingDown( - DdManager * table, - int x, - int x_high, - int initial_size) -{ - Move *moves; - Move *move; - int y; - int size; - int limit_size = initial_size; - - moves = NULL; - y = cuddZddNextHigh(table, x); - while (y <= x_high) { - size = cuddZddSwapInPlace(table, x, y); - if (size == 0) - goto cuddZddSiftingDownOutOfMem; - move = (Move *)cuddDynamicAllocNode(table); - if (move == NULL) - goto cuddZddSiftingDownOutOfMem; - move->x = x; - move->y = y; - move->size = size; - move->next = moves; - moves = move; - - if ((double)size > (double)limit_size * table->maxGrowth) - break; - if (size < limit_size) - limit_size = size; - - x = y; - y = cuddZddNextHigh(table, x); - } - return(moves); - -cuddZddSiftingDownOutOfMem: - while (moves != NULL) { - move = moves->next; - cuddDeallocNode(table, (DdNode *)moves); - moves = move; - } - return(NULL); - -} /* end of cuddZddSiftingDown */ - - -/**Function******************************************************************** - - Synopsis [Given a set of moves, returns the ZDD heap to the position - giving the minimum size.] - - Description [Given a set of moves, returns the ZDD heap to the - position giving the minimum size. In case of ties, returns to the - closest position giving the minimum size. Returns 1 in case of - success; 0 otherwise.] - - SideEffects [None] - - SeeAlso [] - -******************************************************************************/ -static int -cuddZddSiftingBackward( - DdManager * table, - Move * moves, - int size) -{ - int i; - int i_best; - Move *move; - int res; - - /* Find the minimum size among moves. */ - i_best = -1; - for (move = moves, i = 0; move != NULL; move = move->next, i++) { - if (move->size < size) { - i_best = i; - size = move->size; - } - } - - for (move = moves, i = 0; move != NULL; move = move->next, i++) { - if (i == i_best) - break; - res = cuddZddSwapInPlace(table, move->x, move->y); - if (!res) - return(0); - if (i_best == -1 && res == size) - break; - } - - return(1); - -} /* end of cuddZddSiftingBackward */ - - -/**Function******************************************************************** - - Synopsis [Prepares the ZDD heap for dynamic reordering.] - - Description [Prepares the ZDD heap for dynamic reordering. Does - garbage collection, to guarantee that there are no dead nodes; - and clears the cache, which is invalidated by dynamic reordering.] - - SideEffects [None] - -******************************************************************************/ -static void -zddReorderPreprocess( - DdManager * table) -{ - - /* Clear the cache. */ - cuddCacheFlush(table); - - /* Eliminate dead nodes. Do not scan the cache again. */ - cuddGarbageCollectZdd(table,0); - - return; - -} /* end of ddReorderPreprocess */ - - -/**Function******************************************************************** - - Synopsis [Shrinks almost empty ZDD subtables at the end of reordering - to guarantee that they have a reasonable load factor.] - - Description [Shrinks almost empty subtables at the end of reordering to - guarantee that they have a reasonable load factor. However, if there many - nodes are being reclaimed, then no resizing occurs. Returns 1 in case of - success; 0 otherwise.] - - SideEffects [None] - -******************************************************************************/ -static int -zddReorderPostprocess( - DdManager * table) -{ - int i, j, posn; - DdNodePtr *nodelist, *oldnodelist; - DdNode *node, *next; - unsigned int slots, oldslots; - extern void (*MMoutOfMemory)(long); - void (*saveHandler)(long); - -#ifdef DD_VERBOSE - (void) fflush(table->out); -#endif - - /* If we have very many reclaimed nodes, we do not want to shrink - ** the subtables, because this will lead to more garbage - ** collections. More garbage collections mean shorter mean life for - ** nodes with zero reference count; hence lower probability of finding - ** a result in the cache. - */ - if (table->reclaimed > table->allocated * 0.5) return(1); - - /* Resize subtables. */ - for (i = 0; i < table->sizeZ; i++) { - int shift; - oldslots = table->subtableZ[i].slots; - if (oldslots < table->subtableZ[i].keys * DD_MAX_SUBTABLE_SPARSITY || - oldslots <= table->initSlots) continue; - oldnodelist = table->subtableZ[i].nodelist; - slots = oldslots >> 1; - saveHandler = MMoutOfMemory; - MMoutOfMemory = Cudd_OutOfMem; - nodelist = ALLOC(DdNodePtr, slots); - MMoutOfMemory = saveHandler; - if (nodelist == NULL) { - return(1); - } - table->subtableZ[i].nodelist = nodelist; - table->subtableZ[i].slots = slots; - table->subtableZ[i].shift++; - table->subtableZ[i].maxKeys = slots * DD_MAX_SUBTABLE_DENSITY; -#ifdef DD_VERBOSE - (void) fprintf(table->err, - "shrunk layer %d (%d keys) from %d to %d slots\n", - i, table->subtableZ[i].keys, oldslots, slots); -#endif - - for (j = 0; (unsigned) j < slots; j++) { - nodelist[j] = NULL; - } - shift = table->subtableZ[i].shift; - for (j = 0; (unsigned) j < oldslots; j++) { - node = oldnodelist[j]; - while (node != NULL) { - next = node->next; - posn = ddHash(cuddT(node), cuddE(node), shift); - node->next = nodelist[posn]; - nodelist[posn] = node; - node = next; - } - } - FREE(oldnodelist); - - table->memused += (slots - oldslots) * sizeof(DdNode *); - table->slots += slots - oldslots; - table->minDead = (unsigned) (table->gcFrac * (double) table->slots); - table->cacheSlack = (int) ddMin(table->maxCacheHard, - DD_MAX_CACHE_TO_SLOTS_RATIO*table->slots) - - 2 * (int) table->cacheSlots; - } - /* We don't look at the constant subtable, because it is not - ** affected by reordering. - */ - - return(1); - -} /* end of zddReorderPostprocess */ - - -/**Function******************************************************************** - - Synopsis [Reorders ZDD variables according to a given permutation.] - - Description [Reorders ZDD 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. zddShuffle assumes that no - dead nodes are present. The reordering is achieved by a series of - upward sifts. Returns 1 if successful; 0 otherwise.] - - SideEffects [None] - - SeeAlso [] - -******************************************************************************/ -static int -zddShuffle( - DdManager * table, - int * permutation) -{ - int index; - int level; - int position; - int numvars; - int result; -#ifdef DD_STATS - long localTime; - int initialSize; - int finalSize; - int previousSize; -#endif - - zddTotalNumberSwapping = 0; -#ifdef DD_STATS - localTime = util_cpu_time(); - initialSize = table->keysZ; - (void) fprintf(table->out,"#:I_SHUFFLE %8d: initial size\n", - initialSize); -#endif - - numvars = table->sizeZ; - - for (level = 0; level < numvars; level++) { - index = permutation[level]; - position = table->permZ[index]; -#ifdef DD_STATS - previousSize = table->keysZ; -#endif - result = zddSiftUp(table,position,level); - if (!result) return(0); -#ifdef DD_STATS - if (table->keysZ < (unsigned) previousSize) { - (void) fprintf(table->out,"-"); - } else if (table->keysZ > (unsigned) previousSize) { - (void) fprintf(table->out,"+"); /* should never happen */ - } else { - (void) fprintf(table->out,"="); - } - fflush(table->out); -#endif - } - -#ifdef DD_STATS - (void) fprintf(table->out,"\n"); - finalSize = table->keysZ; - (void) fprintf(table->out,"#:F_SHUFFLE %8d: final size\n",finalSize); - (void) fprintf(table->out,"#:T_SHUFFLE %8g: total time (sec)\n", - ((double)(util_cpu_time() - localTime)/1000.0)); - (void) fprintf(table->out,"#:N_SHUFFLE %8d: total swaps\n", - zddTotalNumberSwapping); -#endif - - return(1); - -} /* end of zddShuffle */ - - -/**Function******************************************************************** - - Synopsis [Moves one ZDD variable up.] - - Description [Takes a ZDD 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 -zddSiftUp( - DdManager * table, - int x, - int xLow) -{ - int y; - int size; - - y = cuddZddNextLow(table,x); - while (y >= xLow) { - size = cuddZddSwapInPlace(table,y,x); - if (size == 0) { - return(0); - } - x = y; - y = cuddZddNextLow(table,x); - } - return(1); - -} /* end of zddSiftUp */ - - -/**Function******************************************************************** - - Synopsis [Fixes the ZDD variable group tree after a shuffle.] - - Description [Fixes the ZDD variable group tree after a - shuffle. Assumes that the order of the variables in a terminal node - has not been changed.] - - SideEffects [Changes the ZDD variable group tree.] - - SeeAlso [] - -******************************************************************************/ -static void -zddFixTree( - DdManager * table, - MtrNode * treenode) -{ - if (treenode == NULL) return; - treenode->low = ((int) treenode->index < table->sizeZ) ? - table->permZ[treenode->index] : treenode->index; - if (treenode->child != NULL) { - zddFixTree(table, treenode->child); - } - if (treenode->younger != NULL) - zddFixTree(table, treenode->younger); - if (treenode->parent != NULL && treenode->low < treenode->parent->low) { - treenode->parent->low = treenode->low; - treenode->parent->index = treenode->index; - } - return; - -} /* end of zddFixTree */ - |