From e54d9691616b9a0326e2fdb3156bb4eeb8abfcd7 Mon Sep 17 00:00:00 2001 From: Alan Mishchenko Date: Sun, 30 Sep 2007 08:01:00 -0700 Subject: Version abc70930 --- src/bdd/cudd/cuddReorder.c | 2090 -------------------------------------------- 1 file changed, 2090 deletions(-) delete mode 100644 src/bdd/cudd/cuddReorder.c (limited to 'src/bdd/cudd/cuddReorder.c') diff --git a/src/bdd/cudd/cuddReorder.c b/src/bdd/cudd/cuddReorder.c deleted file mode 100644 index 1387196f..00000000 --- a/src/bdd/cudd/cuddReorder.c +++ /dev/null @@ -1,2090 +0,0 @@ -/**CFile*********************************************************************** - - FileName [cuddReorder.c] - - PackageName [cudd] - - Synopsis [Functions for dynamic variable reordering.] - - Description [External procedures included in this file: - - Internal procedures included in this module: - - Static procedures included in this module: - ] - - Author [Shipra Panda, Bernard Plessier, 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 */ -/*---------------------------------------------------------------------------*/ - -#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: cuddReorder.c,v 1.1.1.1 2003/02/24 22:23:53 wjiang Exp $"; -#endif - -static int *entry; - -int ddTotalNumberSwapping; -#ifdef DD_STATS -int ddTotalNISwaps; -#endif - -/*---------------------------------------------------------------------------*/ -/* Macro declarations */ -/*---------------------------------------------------------------------------*/ - -/**AutomaticStart*************************************************************/ - -/*---------------------------------------------------------------------------*/ -/* Static function prototypes */ -/*---------------------------------------------------------------------------*/ - -static int ddUniqueCompare ARGS((int *ptrX, int *ptrY)); -static Move * ddSwapAny ARGS((DdManager *table, int x, int y)); -static int ddSiftingAux ARGS((DdManager *table, int x, int xLow, int xHigh)); -static Move * ddSiftingUp ARGS((DdManager *table, int y, int xLow)); -static Move * ddSiftingDown ARGS((DdManager *table, int x, int xHigh)); -static int ddSiftingBackward ARGS((DdManager *table, int size, Move *moves)); -static int ddReorderPreprocess ARGS((DdManager *table)); -static int ddReorderPostprocess ARGS((DdManager *table)); -static int ddShuffle ARGS((DdManager *table, int *permutation)); -static int ddSiftUp ARGS((DdManager *table, int x, int xLow)); -static void bddFixTree ARGS((DdManager *table, MtrNode *treenode)); -static int ddUpdateMtrTree ARGS((DdManager *table, MtrNode *treenode, int *perm, int *invperm)); -static int ddCheckPermuation ARGS((DdManager *table, MtrNode *treenode, int *perm, int *invperm)); - -/**AutomaticEnd***************************************************************/ - - -/*---------------------------------------------------------------------------*/ -/* Definition of exported functions */ -/*---------------------------------------------------------------------------*/ - - -/**Function******************************************************************** - - Synopsis [Main dynamic reordering routine.] - - Description [Main dynamic reordering routine. - Calls one of the possible reordering procedures: - - - For sifting, symmetric sifting, group sifting, and window - permutation it is possible to request reordering to convergence.

- - The core of all methods is the reordering procedure - cuddSwapInPlace() which swaps two adjacent variables and is based - on Rudell's paper. - 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 diagrams and clears - the cache.] - -******************************************************************************/ -int -Cudd_ReduceHeap( - 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->keys - table->dead < (unsigned) minsize) - return(1); - - if (heuristic == CUDD_REORDER_SAME) { - heuristic = table->autoMethod; - } - if (heuristic == CUDD_REORDER_NONE) { - return(1); - } - - /* This call to Cudd_ReduceHeap does initiate reordering. Therefore - ** we count it. - */ - table->reorderings++; - - localTime = util_cpu_time(); - - /* Run the hook functions. */ - hook = table->preReorderingHook; - while (hook != NULL) { - int res = (hook->f)(table, "BDD", (void *)heuristic); - if (res == 0) return(0); - hook = hook->next; - } - - if (!ddReorderPreprocess(table)) return(0); - ddTotalNumberSwapping = 0; - - if (table->keys > table->peakLiveNodes) { - table->peakLiveNodes = table->keys; - } -#ifdef DD_STATS - initialSize = table->keys - table->isolated; - ddTotalNISwaps = 0; - - 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: - case CUDD_REORDER_GROUP_SIFT: - case CUDD_REORDER_GROUP_SIFT_CONV: - (void) fprintf(table->out,"#:I_SIFTING "); - break; - case CUDD_REORDER_WINDOW2: - case CUDD_REORDER_WINDOW3: - case CUDD_REORDER_WINDOW4: - case CUDD_REORDER_WINDOW2_CONV: - case CUDD_REORDER_WINDOW3_CONV: - case CUDD_REORDER_WINDOW4_CONV: - (void) fprintf(table->out,"#:I_WINDOW "); - break; - case CUDD_REORDER_ANNEALING: - (void) fprintf(table->out,"#:I_ANNEAL "); - break; - case CUDD_REORDER_GENETIC: - (void) fprintf(table->out,"#:I_GENETIC "); - break; - case CUDD_REORDER_LINEAR: - case CUDD_REORDER_LINEAR_CONVERGE: - (void) fprintf(table->out,"#:I_LINSIFT "); - break; - case CUDD_REORDER_EXACT: - (void) fprintf(table->out,"#:I_EXACT "); - break; - default: - return(0); - } - (void) fprintf(table->out,"%8d: initial size",initialSize); -#endif - - /* See if we should use alternate threshold for maximum growth. */ - if (table->reordCycle && table->reorderings % table->reordCycle == 0) { - double saveGrowth = table->maxGrowth; - table->maxGrowth = table->maxGrowthAlt; - result = cuddTreeSifting(table,heuristic); - table->maxGrowth = saveGrowth; - } else { - result = cuddTreeSifting(table,heuristic); - } - -#ifdef DD_STATS - (void) fprintf(table->out,"\n"); - finalSize = table->keys - table->isolated; - (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", - ddTotalNumberSwapping); - (void) fprintf(table->out,"#:M_REORDER %8d: NI swaps\n",ddTotalNISwaps); -#endif - - if (result == 0) - return(0); - - if (!ddReorderPostprocess(table)) - return(0); - - if (table->realign) { - if (!cuddZddAlignToBdd(table)) - return(0); - } - - nextDyn = (table->keys - table->constants.keys + 1) * - DD_DYN_RATIO + table->constants.keys; - 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, "BDD", (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_ReduceHeap */ - - -/**Function******************************************************************** - - Synopsis [Reorders variables according to given permutation.] - - Description [Reorders 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 variable order for all diagrams and clears - the cache.] - - SeeAlso [Cudd_ReduceHeap] - -******************************************************************************/ -int -Cudd_ShuffleHeap( - DdManager * table /* DD manager */, - int * permutation /* required variable permutation */) -{ - - int result; - int i; - int identity = 1; - int *perm; - - /* Don't waste time in case of identity permutation. */ - for (i = 0; i < table->size; i++) { - if (permutation[i] != table->invperm[i]) { - identity = 0; - break; - } - } - if (identity == 1) { - return(1); - } - if (!ddReorderPreprocess(table)) return(0); - if (table->keys > table->peakLiveNodes) { - table->peakLiveNodes = table->keys; - } - - perm = ALLOC(int, table->size); - for (i = 0; i < table->size; i++) - perm[permutation[i]] = i; - if (!ddCheckPermuation(table,table->tree,perm,permutation)) { - FREE(perm); - return(0); - } - if (!ddUpdateMtrTree(table,table->tree,perm,permutation)) { - FREE(perm); - return(0); - } - FREE(perm); - - result = ddShuffle(table,permutation); - - if (!ddReorderPostprocess(table)) return(0); - - return(result); - -} /* end of Cudd_ShuffleHeap */ - - -/*---------------------------------------------------------------------------*/ -/* Definition of internal functions */ -/*---------------------------------------------------------------------------*/ - - -/**Function******************************************************************** - - Synopsis [Dynamically allocates a Node.] - - Description [Dynamically allocates a Node. This procedure is similar - to cuddAllocNode in Cudd_Table.c, but it does not attempt garbage - collection, because during reordering there are no dead nodes. - Returns a pointer to a new node if successful; NULL is memory is - full.] - - SideEffects [None] - - SeeAlso [cuddAllocNode] - -******************************************************************************/ -DdNode * -cuddDynamicAllocNode( - DdManager * table) -{ - int i; - DdNodePtr *mem; - DdNode *list, *node; - extern void (*MMoutOfMemory)(long); - void (*saveHandler)(long); - - if (table->nextFree == NULL) { /* free list is empty */ - /* Try to allocate a new block. */ - saveHandler = MMoutOfMemory; - MMoutOfMemory = Cudd_OutOfMem; - mem = (DdNodePtr *) ALLOC(DdNode, DD_MEM_CHUNK + 1); - MMoutOfMemory = saveHandler; - if (mem == NULL && table->stash != NULL) { - FREE(table->stash); - table->stash = NULL; - /* Inhibit resizing of tables. */ - table->maxCacheHard = table->cacheSlots - 1; - table->cacheSlack = -(table->cacheSlots + 1); - for (i = 0; i < table->size; i++) { - table->subtables[i].maxKeys <<= 2; - } - mem = (DdNodePtr *) ALLOC(DdNode,DD_MEM_CHUNK + 1); - } - if (mem == NULL) { - /* Out of luck. Call the default handler to do - ** whatever it specifies for a failed malloc. If this - ** handler returns, then set error code, print - ** warning, and return. */ - (*MMoutOfMemory)(sizeof(DdNode)*(DD_MEM_CHUNK + 1)); - table->errorCode = CUDD_MEMORY_OUT; -#ifdef DD_VERBOSE - (void) fprintf(table->err, - "cuddDynamicAllocNode: out of memory"); - (void) fprintf(table->err,"Memory in use = %ld\n", - table->memused); -#endif - return(NULL); - } else { /* successful allocation; slice memory */ - unsigned long offset; - table->memused += (DD_MEM_CHUNK + 1) * sizeof(DdNode); - mem[0] = (DdNode *) table->memoryList; - table->memoryList = mem; - - /* Here we rely on the fact that the size of a DdNode is a - ** power of 2 and a multiple of the size of a pointer. - ** If we align one node, all the others will be aligned - ** as well. */ - offset = (unsigned long) mem & (sizeof(DdNode) - 1); - mem += (sizeof(DdNode) - offset) / sizeof(DdNodePtr); -#ifdef DD_DEBUG - assert(((unsigned long) mem & (sizeof(DdNode) - 1)) == 0); -#endif - list = (DdNode *) mem; - - i = 1; - do { - list[i - 1].next = &list[i]; - } while (++i < DD_MEM_CHUNK); - - list[DD_MEM_CHUNK - 1].next = NULL; - - table->nextFree = &list[0]; - } - } /* if free list empty */ - - node = table->nextFree; - table->nextFree = node->next; - return (node); - -} /* end of cuddDynamicAllocNode */ - - -/**Function******************************************************************** - - Synopsis [Implementation of Rudell's sifting algorithm.] - - Description [Implementation of Rudell's sifting algorithm. - Assumes that no dead nodes are present. -

    -
  1. Order all the variables according to the number of entries - in each unique table. -
  2. Sift the variable up and down, remembering each time the - total size of the DD heap. -
  3. Select the best permutation. -
  4. Repeat 3 and 4 for all variables. -
- Returns 1 if successful; 0 otherwise.] - - SideEffects [None] - -******************************************************************************/ -int -cuddSifting( - DdManager * table, - int lower, - int upper) -{ - int i; - int *var; - int size; - int x; - int result; -#ifdef DD_STATS - int previousSize; -#endif - - size = table->size; - - /* Find order in which to sift variables. */ - var = NULL; - entry = ALLOC(int,size); - if (entry == NULL) { - table->errorCode = CUDD_MEMORY_OUT; - goto cuddSiftingOutOfMem; - } - var = ALLOC(int,size); - if (var == NULL) { - table->errorCode = CUDD_MEMORY_OUT; - goto cuddSiftingOutOfMem; - } - - for (i = 0; i < size; i++) { - x = table->perm[i]; - entry[i] = table->subtables[x].keys; - var[i] = i; - } - - qsort((void *)var,size,sizeof(int),(int (*)(const void *, const void *))ddUniqueCompare); - - /* Now sift. */ - for (i = 0; i < ddMin(table->siftMaxVar,size); i++) { - if (ddTotalNumberSwapping >= table->siftMaxSwap) - break; - x = table->perm[var[i]]; - - if (x < lower || x > upper || table->subtables[x].bindVar == 1) - continue; -#ifdef DD_STATS - previousSize = table->keys - table->isolated; -#endif - result = ddSiftingAux(table, x, lower, upper); - if (!result) goto cuddSiftingOutOfMem; -#ifdef DD_STATS - if (table->keys < (unsigned) previousSize + table->isolated) { - (void) fprintf(table->out,"-"); - } else if (table->keys > (unsigned) previousSize + table->isolated) { - (void) fprintf(table->out,"+"); /* should never happen */ - (void) fprintf(table->err,"\nSize increased from %d to %d while sifting variable %d\n", previousSize, table->keys - table->isolated, var[i]); - } else { - (void) fprintf(table->out,"="); - } - fflush(table->out); -#endif - } - - FREE(var); - FREE(entry); - - return(1); - -cuddSiftingOutOfMem: - - if (entry != NULL) FREE(entry); - if (var != NULL) FREE(var); - - return(0); - -} /* end of cuddSifting */ - - -/**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. -
    -
  1. Select two variables (RANDOM or HEURISTIC). -
  2. Permute these variables. -
  3. If the nodes have decreased accept the permutation. -
  4. Otherwise reconstruct the original heap. -
  5. Loop. -
- Returns 1 in case of success; 0 otherwise.] - - SideEffects [None] - -******************************************************************************/ -int -cuddSwapping( - 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->size && lower <= upper); -#endif - - nvars = upper - lower + 1; - iterate = nvars; - - for (i = 0; i < iterate; i++) { - if (ddTotalNumberSwapping >= table->siftMaxSwap) - break; - if (heuristic == CUDD_REORDER_RANDOM_PIVOT) { - max = -1; - for (j = lower; j <= upper; j++) { - if ((keys = table->subtables[j].keys) > max) { - max = keys; - pivot = j; - } - } - - modulo = upper - pivot; - if (modulo == 0) { - y = pivot; - } else{ - y = pivot + 1 + ((int) Cudd_Random() % modulo); - } - - modulo = pivot - lower - 1; - if (modulo < 1) { - x = lower; - } else{ - do { - x = (int) Cudd_Random() % modulo; - } while (x == y); - } - } else { - x = ((int) Cudd_Random() % nvars) + lower; - do { - y = ((int) Cudd_Random() % nvars) + lower; - } while (x == y); - } - previousSize = table->keys - table->isolated; - moves = ddSwapAny(table,x,y); - if (moves == NULL) goto cuddSwappingOutOfMem; - result = ddSiftingBackward(table,previousSize,moves); - if (!result) goto cuddSwappingOutOfMem; - while (moves != NULL) { - move = moves->next; - cuddDeallocNode(table, (DdNode *) moves); - moves = move; - } -#ifdef DD_STATS - if (table->keys < (unsigned) previousSize + table->isolated) { - (void) fprintf(table->out,"-"); - } else if (table->keys > (unsigned) previousSize + table->isolated) { - (void) fprintf(table->out,"+"); /* should never happen */ - } else { - (void) fprintf(table->out,"="); - } - fflush(table->out); -#endif -#if 0 - (void) fprintf(table->out,"#:t_SWAPPING %8d: tmp size\n", - table->keys - table->isolated); -#endif - } - - return(1); - -cuddSwappingOutOfMem: - while (moves != NULL) { - move = moves->next; - cuddDeallocNode(table, (DdNode *) moves); - moves = move; - } - - return(0); - -} /* end of cuddSwapping */ - - -/**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 [cuddNextLow] - -******************************************************************************/ -int -cuddNextHigh( - DdManager * table, - int x) -{ - return(x+1); - -} /* end of cuddNextHigh */ - - -/**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 [cuddNextHigh] - -******************************************************************************/ -int -cuddNextLow( - DdManager * table, - int x) -{ - return(x-1); - -} /* end of cuddNextLow */ - - -/**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. - cuddSwapInPlace assumes that x < y. Returns the number of keys in - the table if successful; 0 otherwise.] - - SideEffects [None] - -******************************************************************************/ -int -cuddSwapInPlace( - 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 comple, newcomplement; - int i; - Cudd_VariableType varType; - Cudd_LazyGroupType groupType; - int posn; - int isolated; - DdNode *f,*f0,*f1,*f01,*f00,*f11,*f10,*newf1,*newf0; - DdNode *g,*next; - DdNodePtr *previousP; - DdNode *tmp; - DdNode *sentinel = &(table->sentinel); - extern void (*MMoutOfMemory)(long); - void (*saveHandler)(long); - -#if DD_DEBUG - int count,idcheck; -#endif - -#ifdef DD_DEBUG - assert(x < y); - assert(cuddNextHigh(table,x) == y); - assert(table->subtables[x].keys != 0); - assert(table->subtables[y].keys != 0); - assert(table->subtables[x].dead == 0); - assert(table->subtables[y].dead == 0); -#endif - - ddTotalNumberSwapping++; - - /* Get parameters of x subtable. */ - xindex = table->invperm[x]; - xlist = table->subtables[x].nodelist; - oldxkeys = table->subtables[x].keys; - xslots = table->subtables[x].slots; - xshift = table->subtables[x].shift; - - /* Get parameters of y subtable. */ - yindex = table->invperm[y]; - ylist = table->subtables[y].nodelist; - oldykeys = table->subtables[y].keys; - yslots = table->subtables[y].slots; - yshift = table->subtables[y].shift; - - if (!cuddTestInteract(table,xindex,yindex)) { -#ifdef DD_STATS - ddTotalNISwaps++; -#endif - newxkeys = oldxkeys; - newykeys = oldykeys; - } else { - newxkeys = 0; - newykeys = oldykeys; - - /* Check whether the two projection functions involved in this - ** swap are isolated. At the end, we'll be able to tell how many - ** isolated projection functions are there by checking only these - ** two functions again. This is done to eliminate the isolated - ** projection functions from the node count. - */ - isolated = - ((table->vars[xindex]->ref == 1) + - (table->vars[yindex]->ref == 1)); - - /* The nodes in the x layer that do not depend on - ** y will stay there; the others are put in a chain. - ** The chain is handled as a LIFO; g points to the beginning. - */ - g = NULL; - if ((oldxkeys >= xslots || (unsigned) xslots == table->initSlots) && - oldxkeys <= DD_MAX_SUBTABLE_DENSITY * xslots) { - for (i = 0; i < xslots; i++) { - previousP = &(xlist[i]); - f = *previousP; - while (f != sentinel) { - next = f->next; - f1 = cuddT(f); f0 = cuddE(f); - if (f1->index != (DdHalfWord) yindex && - Cudd_Regular(f0)->index != (DdHalfWord) yindex) { - /* stays */ - newxkeys++; - *previousP = f; - previousP = &(f->next); - } else { - f->index = yindex; - f->next = g; - g = f; - } - f = next; - } /* while there are elements in the collision chain */ - *previousP = sentinel; - } /* for each slot of the x subtable */ - } else { /* resize xlist */ - DdNode *h = NULL; - DdNodePtr *newxlist; - unsigned int newxslots; - int newxshift; - /* Empty current xlist. Nodes that stay go to list h; - ** nodes that move go to list g. */ - for (i = 0; i < xslots; i++) { - f = xlist[i]; - while (f != sentinel) { - next = f->next; - f1 = cuddT(f); f0 = cuddE(f); - if (f1->index != (DdHalfWord) yindex && - Cudd_Regular(f0)->index != (DdHalfWord) yindex) { - /* stays */ - f->next = h; - h = f; - newxkeys++; - } else { - f->index = yindex; - f->next = g; - g = f; - } - f = next; - } /* while there are elements in the collision chain */ - } /* for each slot of the x subtable */ - /* Decide size of new subtable. */ - if (oldxkeys > DD_MAX_SUBTABLE_DENSITY * xslots) { - newxshift = xshift - 1; - newxslots = xslots << 1; - } else { - newxshift = xshift + 1; - newxslots = xslots >> 1; - } - /* Try to allocate new table. Be ready to back off. */ - saveHandler = MMoutOfMemory; - MMoutOfMemory = Cudd_OutOfMem; - newxlist = ALLOC(DdNodePtr, newxslots); - MMoutOfMemory = saveHandler; - if (newxlist == NULL) { - (void) fprintf(table->err, "Unable to resize subtable %d for lack of memory\n", i); - newxlist = xlist; - newxslots = xslots; - newxshift = xshift; - } else { - table->slots += (newxslots - xslots); - 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; - table->memused += (newxslots - xslots) * sizeof(DdNodePtr); - FREE(xlist); - xslots = newxslots; - xshift = newxshift; - xlist = newxlist; - } - /* Initialize new subtable. */ - for (i = 0; i < xslots; i++) { - xlist[i] = sentinel; - } - /* Move nodes that were parked in list h to their new home. */ - f = h; - while (f != NULL) { - next = f->next; - f1 = cuddT(f); - f0 = cuddE(f); - /* Check xlist for pair (f11,f01). */ - posn = ddHash(f1, f0, xshift); - /* For each element tmp in collision list xlist[posn]. */ - previousP = &(xlist[posn]); - tmp = *previousP; - while (f1 < cuddT(tmp)) { - previousP = &(tmp->next); - tmp = *previousP; - } - while (f1 == cuddT(tmp) && f0 < cuddE(tmp)) { - previousP = &(tmp->next); - tmp = *previousP; - } - f->next = *previousP; - *previousP = f; - f = next; - } - } - -#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 - ** already changed to yindex. - */ - f = g; - while (f != NULL) { - next = f->next; - /* Find f1, f0, f11, f10, f01, f00. */ - f1 = cuddT(f); -#ifdef DD_DEBUG - assert(!(Cudd_IsComplement(f1))); -#endif - if ((int) f1->index == yindex) { - f11 = cuddT(f1); f10 = cuddE(f1); - } else { - f11 = f10 = f1; - } -#ifdef DD_DEBUG - assert(!(Cudd_IsComplement(f11))); -#endif - f0 = cuddE(f); - comple = Cudd_IsComplement(f0); - f0 = Cudd_Regular(f0); - if ((int) f0->index == yindex) { - f01 = cuddT(f0); f00 = cuddE(f0); - } else { - f01 = f00 = f0; - } - if (comple) { - f01 = Cudd_Not(f01); - f00 = Cudd_Not(f00); - } - /* Decrease ref count of f1. */ - cuddSatDec(f1->ref); - /* Create the new T child. */ - if (f11 == f01) { - newf1 = f11; - cuddSatInc(newf1->ref); - } else { - /* Check xlist for triple (xindex,f11,f01). */ - posn = ddHash(f11, f01, xshift); - /* For each element newf1 in collision list xlist[posn]. */ - previousP = &(xlist[posn]); - newf1 = *previousP; - while (f11 < cuddT(newf1)) { - previousP = &(newf1->next); - newf1 = *previousP; - } - while (f11 == cuddT(newf1) && f01 < cuddE(newf1)) { - previousP = &(newf1->next); - newf1 = *previousP; - } - if (cuddT(newf1) == f11 && cuddE(newf1) == f01) { - cuddSatInc(newf1->ref); - } else { /* no match */ - newf1 = cuddDynamicAllocNode(table); - if (newf1 == NULL) - goto cuddSwapOutOfMem; - newf1->index = xindex; newf1->ref = 1; - cuddT(newf1) = f11; - cuddE(newf1) = f01; - /* Insert newf1 in the collision list xlist[posn]; - ** increase the ref counts of f11 and f01. - */ - newxkeys++; - newf1->next = *previousP; - *previousP = newf1; - cuddSatInc(f11->ref); - tmp = Cudd_Regular(f01); - cuddSatInc(tmp->ref); - } - } - cuddT(f) = newf1; -#ifdef DD_DEBUG - assert(!(Cudd_IsComplement(newf1))); -#endif - - /* Do the same for f0, keeping complement dots into account. */ - /* Decrease ref count of f0. */ - tmp = Cudd_Regular(f0); - cuddSatDec(tmp->ref); - /* Create the new E child. */ - if (f10 == f00) { - newf0 = f00; - tmp = Cudd_Regular(newf0); - cuddSatInc(tmp->ref); - } else { - /* make sure f10 is regular */ - newcomplement = Cudd_IsComplement(f10); - if (newcomplement) { - f10 = Cudd_Not(f10); - f00 = Cudd_Not(f00); - } - /* Check xlist for triple (xindex,f10,f00). */ - posn = ddHash(f10, f00, xshift); - /* For each element newf0 in collision list xlist[posn]. */ - previousP = &(xlist[posn]); - newf0 = *previousP; - while (f10 < cuddT(newf0)) { - previousP = &(newf0->next); - newf0 = *previousP; - } - while (f10 == cuddT(newf0) && f00 < cuddE(newf0)) { - previousP = &(newf0->next); - newf0 = *previousP; - } - if (cuddT(newf0) == f10 && cuddE(newf0) == f00) { - cuddSatInc(newf0->ref); - } else { /* no match */ - newf0 = cuddDynamicAllocNode(table); - if (newf0 == NULL) - goto cuddSwapOutOfMem; - 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 = *previousP; - *previousP = newf0; - cuddSatInc(f10->ref); - tmp = Cudd_Regular(f00); - cuddSatInc(tmp->ref); - } - if (newcomplement) { - newf0 = Cudd_Not(newf0); - } - } - 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++; - previousP = &(ylist[posn]); - tmp = *previousP; - while (newf1 < cuddT(tmp)) { - previousP = &(tmp->next); - tmp = *previousP; - } - while (newf1 == cuddT(tmp) && newf0 < cuddE(tmp)) { - previousP = &(tmp->next); - tmp = *previousP; - } - f->next = *previousP; - *previousP = 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 != sentinel) { - next = f->next; - if (f->ref == 0) { - tmp = cuddT(f); - cuddSatDec(tmp->ref); - tmp = Cudd_Regular(cuddE(f)); - cuddSatDec(tmp->ref); - cuddDeallocNode(table,f); - newykeys--; - } else { - *previousP = f; - previousP = &(f->next); - } - f = next; - } /* while f */ - *previousP = sentinel; - } /* for i */ - -#if DD_DEBUG -#if 0 - (void) fprintf(table->out,"Swapping %d and %d\n",x,y); -#endif - count = 0; - idcheck = 0; - for (i = 0; i < yslots; i++) { - f = ylist[i]; - while (f != sentinel) { - count++; - if (f->index != (DdHalfWord) yindex) - idcheck++; - f = f->next; - } - } - if (count != newykeys) { - (void) fprintf(table->out, - "Error in finding newykeys\toldykeys = %d\tnewykeys = %d\tactual = %d\n", - oldykeys,newykeys,count); - } - if (idcheck != 0) - (void) fprintf(table->out, - "Error in id's of ylist\twrong id's = %d\n", - idcheck); - count = 0; - idcheck = 0; - for (i = 0; i < xslots; i++) { - f = xlist[i]; - while (f != sentinel) { - count++; - if (f->index != (DdHalfWord) xindex) - idcheck++; - f = f->next; - } - } - if (count != newxkeys) { - (void) fprintf(table->out, - "Error in finding newxkeys\toldxkeys = %d \tnewxkeys = %d \tactual = %d\n", - oldxkeys,newxkeys,count); - } - if (idcheck != 0) - (void) fprintf(table->out, - "Error in id's of xlist\twrong id's = %d\n", - idcheck); -#endif - - isolated += (table->vars[xindex]->ref == 1) + - (table->vars[yindex]->ref == 1); - table->isolated += isolated; - } - - /* Set the appropriate fields in table. */ - table->subtables[x].nodelist = ylist; - table->subtables[x].slots = yslots; - table->subtables[x].shift = yshift; - table->subtables[x].keys = newykeys; - table->subtables[x].maxKeys = yslots * DD_MAX_SUBTABLE_DENSITY; - i = table->subtables[x].bindVar; - table->subtables[x].bindVar = table->subtables[y].bindVar; - table->subtables[y].bindVar = i; - /* Adjust filds for lazy sifting. */ - varType = table->subtables[x].varType; - table->subtables[x].varType = table->subtables[y].varType; - table->subtables[y].varType = varType; - i = table->subtables[x].pairIndex; - table->subtables[x].pairIndex = table->subtables[y].pairIndex; - table->subtables[y].pairIndex = i; - i = table->subtables[x].varHandled; - table->subtables[x].varHandled = table->subtables[y].varHandled; - table->subtables[y].varHandled = i; - groupType = table->subtables[x].varToBeGrouped; - table->subtables[x].varToBeGrouped = table->subtables[y].varToBeGrouped; - table->subtables[y].varToBeGrouped = groupType; - - table->subtables[y].nodelist = xlist; - table->subtables[y].slots = xslots; - table->subtables[y].shift = xshift; - table->subtables[y].keys = newxkeys; - table->subtables[y].maxKeys = xslots * DD_MAX_SUBTABLE_DENSITY; - - table->perm[xindex] = y; table->perm[yindex] = x; - table->invperm[x] = yindex; table->invperm[y] = xindex; - - table->keys += newxkeys + newykeys - oldxkeys - oldykeys; - - return(table->keys - table->isolated); - -cuddSwapOutOfMem: - (void) fprintf(table->err,"Error: cuddSwapInPlace out of memory\n"); - - return (0); - -} /* end of cuddSwapInPlace */ - - -/**Function******************************************************************** - - Synopsis [Reorders BDD variables according to the order of the ZDD - variables.] - - Description [Reorders BDD variables according to the order of the - ZDD variables. This function can be called at the end of ZDD - reordering to insure that the order of the BDD variables is - consistent with the order of the ZDD variables. The number of ZDD - variables must be a multiple of the number of BDD variables. Let - M be the ratio of the two numbers. cuddBddAlignToZdd - then considers the ZDD variables from M*i to - (M+1)*i-1 as corresponding to BDD variable - i. This function should be normally called from - Cudd_zddReduceHeap, which clears the cache. Returns 1 in case of - success; 0 otherwise.] - - SideEffects [Changes the BDD variable order for all diagrams and performs - garbage collection of the BDD unique table.] - - SeeAlso [Cudd_ShuffleHeap Cudd_zddReduceHeap] - -******************************************************************************/ -int -cuddBddAlignToZdd( - DdManager * table /* DD manager */) -{ - int *invperm; /* permutation array */ - int M; /* ratio of ZDD variables to BDD variables */ - int i; /* loop index */ - int result; /* return value */ - - /* We assume that a ratio of 0 is OK. */ - if (table->size == 0) - return(1); - - 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. */ - invperm = ALLOC(int,table->size); - if (invperm == NULL) { - table->errorCode = CUDD_MEMORY_OUT; - return(0); - } - for (i = 0; i < table->sizeZ; i += M) { - int indexZ = table->invpermZ[i]; - int index = indexZ / M; - invperm[i / M] = index; - } - /* Eliminate dead nodes. Do not scan the cache again, because we - ** assume that Cudd_zddReduceHeap has already cleared it. - */ - cuddGarbageCollect(table,0); - - /* Initialize number of isolated projection functions. */ - table->isolated = 0; - for (i = 0; i < table->size; i++) { - if (table->vars[i]->ref == 1) table->isolated++; - } - - /* Initialize the interaction matrix. */ - result = cuddInitInteract(table); - if (result == 0) return(0); - - result = ddShuffle(table, invperm); - FREE(invperm); - /* Free interaction matrix. */ - FREE(table->interact); - /* Fix the BDD variable group tree. */ - bddFixTree(table,table->tree); - return(result); - -} /* end of cuddBddAlignToZdd */ - -/*---------------------------------------------------------------------------*/ -/* Definition of static functions */ -/*---------------------------------------------------------------------------*/ - - -/**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] - -******************************************************************************/ -static int -ddUniqueCompare( - int * ptrX, - int * ptrY) -{ -#if 0 - if (entry[*ptrY] == entry[*ptrX]) { - return((*ptrX) - (*ptrY)); - } -#endif - return(entry[*ptrY] - entry[*ptrX]); - -} /* end of ddUniqueCompare */ - - -/**Function******************************************************************** - - Synopsis [Swaps any two variables.] - - Description [Swaps any two variables. Returns the set of moves.] - - SideEffects [None] - -******************************************************************************/ -static Move * -ddSwapAny( - DdManager * table, - int x, - int y) -{ - Move *move, *moves; - int xRef,yRef; - int xNext,yNext; - int size; - int limitSize; - int tmp; - - if (x >y) { - tmp = x; x = y; y = tmp; - } - - xRef = x; yRef = y; - - xNext = cuddNextHigh(table,x); - yNext = cuddNextLow(table,y); - moves = NULL; - limitSize = table->keys - table->isolated; - - for (;;) { - if ( xNext == yNext) { - size = cuddSwapInPlace(table,x,xNext); - if (size == 0) goto ddSwapAnyOutOfMem; - move = (Move *) cuddDynamicAllocNode(table); - if (move == NULL) goto ddSwapAnyOutOfMem; - move->x = x; - move->y = xNext; - move->size = size; - move->next = moves; - moves = move; - - size = cuddSwapInPlace(table,yNext,y); - if (size == 0) goto ddSwapAnyOutOfMem; - move = (Move *) cuddDynamicAllocNode(table); - if (move == NULL) goto ddSwapAnyOutOfMem; - move->x = yNext; - move->y = y; - move->size = size; - move->next = moves; - moves = move; - - size = cuddSwapInPlace(table,x,xNext); - if (size == 0) goto ddSwapAnyOutOfMem; - move = (Move *) cuddDynamicAllocNode(table); - if (move == NULL) goto ddSwapAnyOutOfMem; - move->x = x; - move->y = xNext; - move->size = size; - move->next = moves; - moves = move; - - tmp = x; x = y; y = tmp; - - } else if (x == yNext) { - - size = cuddSwapInPlace(table,x,xNext); - if (size == 0) goto ddSwapAnyOutOfMem; - move = (Move *) cuddDynamicAllocNode(table); - if (move == NULL) goto ddSwapAnyOutOfMem; - move->x = x; - move->y = xNext; - move->size = size; - move->next = moves; - moves = move; - - tmp = x; x = y; y = tmp; - - } else { - size = cuddSwapInPlace(table,x,xNext); - if (size == 0) goto ddSwapAnyOutOfMem; - move = (Move *) cuddDynamicAllocNode(table); - if (move == NULL) goto ddSwapAnyOutOfMem; - move->x = x; - move->y = xNext; - move->size = size; - move->next = moves; - moves = move; - - size = cuddSwapInPlace(table,yNext,y); - if (size == 0) goto ddSwapAnyOutOfMem; - move = (Move *) cuddDynamicAllocNode(table); - if (move == NULL) goto ddSwapAnyOutOfMem; - move->x = yNext; - move->y = y; - move->size = size; - move->next = moves; - moves = move; - - x = xNext; - y = yNext; - } - - xNext = cuddNextHigh(table,x); - yNext = cuddNextLow(table,y); - if (xNext > yRef) break; - - if ((double) size > table->maxGrowth * (double) limitSize) break; - if (size < limitSize) limitSize = size; - } - if (yNext>=xRef) { - size = cuddSwapInPlace(table,yNext,y); - if (size == 0) goto ddSwapAnyOutOfMem; - move = (Move *) cuddDynamicAllocNode(table); - if (move == NULL) goto ddSwapAnyOutOfMem; - move->x = yNext; - move->y = y; - move->size = size; - move->next = moves; - moves = move; - } - - return(moves); - -ddSwapAnyOutOfMem: - while (moves != NULL) { - move = moves->next; - cuddDeallocNode(table, (DdNode *) moves); - moves = move; - } - return(NULL); - -} /* end of ddSwapAny */ - - -/**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] - -******************************************************************************/ -static int -ddSiftingAux( - DdManager * table, - int x, - int xLow, - int xHigh) -{ - - Move *move; - Move *moveUp; /* list of up moves */ - Move *moveDown; /* list of down moves */ - int initialSize; - int result; - - initialSize = table->keys - table->isolated; - - moveDown = NULL; - moveUp = NULL; - - if (x == xLow) { - moveDown = ddSiftingDown(table,x,xHigh); - /* At this point x --> xHigh unless bounding occurred. */ - if (moveDown == (Move *) CUDD_OUT_OF_MEM) goto ddSiftingAuxOutOfMem; - /* Move backward and stop at best position. */ - result = ddSiftingBackward(table,initialSize,moveDown); - if (!result) goto ddSiftingAuxOutOfMem; - - } else if (x == xHigh) { - moveUp = ddSiftingUp(table,x,xLow); - /* At this point x --> xLow unless bounding occurred. */ - if (moveUp == (Move *) CUDD_OUT_OF_MEM) goto ddSiftingAuxOutOfMem; - /* Move backward and stop at best position. */ - result = ddSiftingBackward(table,initialSize,moveUp); - if (!result) goto ddSiftingAuxOutOfMem; - - } else if ((x - xLow) > (xHigh - x)) { /* must go down first: shorter */ - moveDown = ddSiftingDown(table,x,xHigh); - /* At this point x --> xHigh unless bounding occurred. */ - if (moveDown == (Move *) CUDD_OUT_OF_MEM) goto ddSiftingAuxOutOfMem; - if (moveDown != NULL) { - x = moveDown->y; - } - moveUp = ddSiftingUp(table,x,xLow); - if (moveUp == (Move *) CUDD_OUT_OF_MEM) goto ddSiftingAuxOutOfMem; - /* Move backward and stop at best position */ - result = ddSiftingBackward(table,initialSize,moveUp); - if (!result) goto ddSiftingAuxOutOfMem; - - } else { /* must go up first: shorter */ - moveUp = ddSiftingUp(table,x,xLow); - /* At this point x --> xLow unless bounding occurred. */ - if (moveUp == (Move *) CUDD_OUT_OF_MEM) goto ddSiftingAuxOutOfMem; - if (moveUp != NULL) { - x = moveUp->x; - } - moveDown = ddSiftingDown(table,x,xHigh); - if (moveDown == (Move *) CUDD_OUT_OF_MEM) goto ddSiftingAuxOutOfMem; - /* Move backward and stop at best position. */ - result = ddSiftingBackward(table,initialSize,moveDown); - if (!result) goto ddSiftingAuxOutOfMem; - } - - 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); - -ddSiftingAuxOutOfMem: - if (moveDown != (Move *) CUDD_OUT_OF_MEM) { - while (moveDown != NULL) { - move = moveDown->next; - cuddDeallocNode(table, (DdNode *) moveDown); - moveDown = move; - } - } - if (moveUp != (Move *) CUDD_OUT_OF_MEM) { - while (moveUp != NULL) { - move = moveUp->next; - cuddDeallocNode(table, (DdNode *) moveUp); - moveUp = move; - } - } - - return(0); - -} /* end of ddSiftingAux */ - - -/**Function******************************************************************** - - Synopsis [Sifts a variable up.] - - Description [Sifts a variable up. Moves y up until either it reaches - the bound (xLow) or the size of the DD heap increases too much. - Returns the set of moves in case of success; NULL if memory is full.] - - SideEffects [None] - -******************************************************************************/ -static Move * -ddSiftingUp( - DdManager * table, - int y, - int xLow) -{ - Move *moves; - Move *move; - int x; - int size; - int limitSize; - int xindex, yindex; - int isolated; - int L; /* lower bound on DD size */ -#ifdef DD_DEBUG - int checkL; - int z; - int zindex; -#endif - - moves = NULL; - yindex = table->invperm[y]; - - /* Initialize the lower bound. - ** The part of the DD below y will not change. - ** The part of the DD above y that does not interact with y will not - ** change. The rest may vanish in the best case, except for - ** the nodes at level xLow, which will not vanish, regardless. - */ - limitSize = L = table->keys - table->isolated; - for (x = xLow + 1; x < y; x++) { - xindex = table->invperm[x]; - if (cuddTestInteract(table,xindex,yindex)) { - isolated = table->vars[xindex]->ref == 1; - L -= table->subtables[x].keys - isolated; - } - } - isolated = table->vars[yindex]->ref == 1; - L -= table->subtables[y].keys - isolated; - - x = cuddNextLow(table,y); - while (x >= xLow && L <= limitSize) { - xindex = table->invperm[x]; -#ifdef DD_DEBUG - checkL = table->keys - table->isolated; - for (z = xLow + 1; z < y; z++) { - zindex = table->invperm[z]; - if (cuddTestInteract(table,zindex,yindex)) { - isolated = table->vars[zindex]->ref == 1; - checkL -= table->subtables[z].keys - isolated; - } - } - isolated = table->vars[yindex]->ref == 1; - checkL -= table->subtables[y].keys - isolated; - assert(L == checkL); -#endif - size = cuddSwapInPlace(table,x,y); - if (size == 0) goto ddSiftingUpOutOfMem; - /* Update the lower bound. */ - if (cuddTestInteract(table,xindex,yindex)) { - isolated = table->vars[xindex]->ref == 1; - L += table->subtables[y].keys - isolated; - } - move = (Move *) cuddDynamicAllocNode(table); - if (move == NULL) goto ddSiftingUpOutOfMem; - move->x = x; - move->y = y; - move->size = size; - move->next = moves; - moves = move; - if ((double) size > (double) limitSize * table->maxGrowth) break; - if (size < limitSize) limitSize = size; - y = x; - x = cuddNextLow(table,y); - } - return(moves); - -ddSiftingUpOutOfMem: - while (moves != NULL) { - move = moves->next; - cuddDeallocNode(table, (DdNode *) moves); - moves = move; - } - return((Move *) CUDD_OUT_OF_MEM); - -} /* end of ddSiftingUp */ - - -/**Function******************************************************************** - - Synopsis [Sifts a variable down.] - - Description [Sifts a variable down. Moves x down until either it - reaches the bound (xHigh) or the size of the DD heap increases too - much. Returns the set of moves in case of success; NULL if memory is - full.] - - SideEffects [None] - -******************************************************************************/ -static Move * -ddSiftingDown( - DdManager * table, - int x, - int xHigh) -{ - Move *moves; - Move *move; - int y; - int size; - int R; /* upper bound on node decrease */ - int limitSize; - int xindex, yindex; - int isolated; -#ifdef DD_DEBUG - int checkR; - int z; - int zindex; -#endif - - moves = NULL; - /* Initialize R */ - xindex = table->invperm[x]; - limitSize = size = table->keys - table->isolated; - R = 0; - for (y = xHigh; y > x; y--) { - yindex = table->invperm[y]; - if (cuddTestInteract(table,xindex,yindex)) { - isolated = table->vars[yindex]->ref == 1; - R += table->subtables[y].keys - isolated; - } - } - - y = cuddNextHigh(table,x); - while (y <= xHigh && size - R < limitSize) { -#ifdef DD_DEBUG - checkR = 0; - for (z = xHigh; z > x; z--) { - zindex = table->invperm[z]; - if (cuddTestInteract(table,xindex,zindex)) { - isolated = table->vars[zindex]->ref == 1; - checkR += table->subtables[z].keys - isolated; - } - } - assert(R == checkR); -#endif - /* Update upper bound on node decrease. */ - yindex = table->invperm[y]; - if (cuddTestInteract(table,xindex,yindex)) { - isolated = table->vars[yindex]->ref == 1; - R -= table->subtables[y].keys - isolated; - } - size = cuddSwapInPlace(table,x,y); - if (size == 0) goto ddSiftingDownOutOfMem; - move = (Move *) cuddDynamicAllocNode(table); - if (move == NULL) goto ddSiftingDownOutOfMem; - move->x = x; - move->y = y; - move->size = size; - move->next = moves; - moves = move; - if ((double) size > (double) limitSize * table->maxGrowth) break; - if (size < limitSize) limitSize = size; - x = y; - y = cuddNextHigh(table,x); - } - return(moves); - -ddSiftingDownOutOfMem: - while (moves != NULL) { - move = moves->next; - cuddDeallocNode(table, (DdNode *) moves); - moves = move; - } - return((Move *) CUDD_OUT_OF_MEM); - -} /* end of ddSiftingDown */ - - -/**Function******************************************************************** - - Synopsis [Given a set of moves, returns the DD heap to the position - giving the minimum size.] - - Description [Given a set of moves, returns the DD 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] - -******************************************************************************/ -static int -ddSiftingBackward( - DdManager * table, - int size, - Move * moves) -{ - Move *move; - int res; - - for (move = moves; move != NULL; move = move->next) { - if (move->size < size) { - size = move->size; - } - } - - for (move = moves; move != NULL; move = move->next) { - if (move->size == size) return(1); - res = cuddSwapInPlace(table,(int)move->x,(int)move->y); - if (!res) return(0); - } - - return(1); - -} /* end of ddSiftingBackward */ - - -/**Function******************************************************************** - - Synopsis [Prepares the DD heap for dynamic reordering.] - - Description [Prepares the DD heap for dynamic reordering. Does - garbage collection, to guarantee that there are no dead nodes; - clears the cache, which is invalidated by dynamic reordering; initializes - the number of isolated projection functions; and initializes the - interaction matrix. Returns 1 in case of success; 0 otherwise.] - - SideEffects [None] - -******************************************************************************/ -static int -ddReorderPreprocess( - DdManager * table) -{ - int i; - int res; - - /* Clear the cache. */ - cuddCacheFlush(table); - cuddLocalCacheClearAll(table); - - /* Eliminate dead nodes. Do not scan the cache again. */ - cuddGarbageCollect(table,0); - - /* Initialize number of isolated projection functions. */ - table->isolated = 0; - for (i = 0; i < table->size; i++) { - if (table->vars[i]->ref == 1) table->isolated++; - } - - /* Initialize the interaction matrix. */ - res = cuddInitInteract(table); - if (res == 0) return(0); - - return(1); - -} /* end of ddReorderPreprocess */ - - -/**Function******************************************************************** - - Synopsis [Cleans up at the end of reordering.] - - Description [] - - SideEffects [None] - -******************************************************************************/ -static int -ddReorderPostprocess( - DdManager * table) -{ - -#ifdef DD_VERBOSE - (void) fflush(table->out); -#endif - - /* Free interaction matrix. */ - FREE(table->interact); - - return(1); - -} /* end of ddReorderPostprocess */ - - -/**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, - int * permutation) -{ - int index; - int level; - int position; - int numvars; - int result; -#ifdef DD_STATS - long localTime; - int initialSize; - int finalSize; - int previousSize; -#endif - - ddTotalNumberSwapping = 0; -#ifdef DD_STATS - localTime = util_cpu_time(); - initialSize = table->keys - table->isolated; - (void) fprintf(table->out,"#:I_SHUFFLE %8d: initial size\n", - initialSize); - ddTotalNISwaps = 0; -#endif - - numvars = table->size; - - for (level = 0; level < numvars; level++) { - index = permutation[level]; - position = table->perm[index]; -#ifdef DD_STATS - previousSize = table->keys - table->isolated; -#endif - result = ddSiftUp(table,position,level); - if (!result) return(0); -#ifdef DD_STATS - if (table->keys < (unsigned) previousSize + table->isolated) { - (void) fprintf(table->out,"-"); - } else if (table->keys > (unsigned) previousSize + table->isolated) { - (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->keys - table->isolated; - (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", - ddTotalNumberSwapping); - (void) fprintf(table->out,"#:M_SHUFFLE %8d: NI swaps\n",ddTotalNISwaps); -#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 [Fixes the BDD variable group tree after a shuffle.] - - Description [Fixes the BDD variable group tree after a - shuffle. Assumes that the order of the variables in a terminal node - has not been changed.] - - SideEffects [Changes the BDD variable group tree.] - - SeeAlso [] - -******************************************************************************/ -static void -bddFixTree( - DdManager * table, - MtrNode * treenode) -{ - if (treenode == NULL) return; - treenode->low = ((int) treenode->index < table->size) ? - table->perm[treenode->index] : treenode->index; - if (treenode->child != NULL) { - bddFixTree(table, treenode->child); - } - if (treenode->younger != NULL) - bddFixTree(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 bddFixTree */ - - -/**Function******************************************************************** - - Synopsis [Updates the BDD variable group tree before a shuffle.] - - Description [Updates the BDD variable group tree before a shuffle. - Returns 1 if successful; 0 otherwise.] - - SideEffects [Changes the BDD variable group tree.] - - SeeAlso [] - -******************************************************************************/ -static int -ddUpdateMtrTree( - DdManager * table, - MtrNode * treenode, - int * perm, - int * invperm) -{ - int i, size, index, level; - int minLevel, maxLevel, minIndex; - - if (treenode == NULL) return(1); - - /* i : level */ - for (i = treenode->low; i < treenode->low + treenode->size; i++) { - index = table->invperm[i]; - level = perm[index]; - if (level < minLevel) { - minLevel = level; - minIndex = index; - } - if (level > maxLevel) - maxLevel = level; - } - size = maxLevel - minLevel + 1; - if (size == treenode->size) { - treenode->low = minLevel; - treenode->index = minIndex; - } else - return(0); - - if (treenode->child != NULL) { - if (!ddUpdateMtrTree(table, treenode->child, perm, invperm)) - return(0); - } - if (treenode->younger != NULL) { - if (!ddUpdateMtrTree(table, treenode->younger, perm, invperm)) - return(0); - } - return(1); -} - - -/**Function******************************************************************** - - Synopsis [Checks the BDD variable group tree before a shuffle.] - - Description [Checks the BDD variable group tree before a shuffle. - Returns 1 if successful; 0 otherwise.] - - SideEffects [Changes the BDD variable group tree.] - - SeeAlso [] - -******************************************************************************/ -static int -ddCheckPermuation( - DdManager * table, - MtrNode * treenode, - int * perm, - int * invperm) -{ - int i, size, index, level; - int minLevel, maxLevel; - - if (treenode == NULL) return(1); - - minLevel = table->size; - maxLevel = 0; - /* i : level */ - for (i = treenode->low; i < treenode->low + treenode->size; i++) { - index = table->invperm[i]; - level = perm[index]; - if (level < minLevel) - minLevel = level; - if (level > maxLevel) - maxLevel = level; - } - size = maxLevel - minLevel + 1; - if (size != treenode->size) - return(0); - - if (treenode->child != NULL) { - if (!ddCheckPermuation(table, treenode->child, perm, invperm)) - return(0); - } - if (treenode->younger != NULL) { - if (!ddCheckPermuation(table, treenode->younger, perm, invperm)) - return(0); - } - return(1); -} -- cgit v1.2.3