diff options
Diffstat (limited to 'src/bdd/cudd/cuddTable.c')
| -rw-r--r-- | src/bdd/cudd/cuddTable.c | 3141 |
1 files changed, 3141 insertions, 0 deletions
diff --git a/src/bdd/cudd/cuddTable.c b/src/bdd/cudd/cuddTable.c new file mode 100644 index 00000000..7f14aed1 --- /dev/null +++ b/src/bdd/cudd/cuddTable.c @@ -0,0 +1,3141 @@ +/**CFile*********************************************************************** + + FileName [cuddTable.c] + + PackageName [cudd] + + Synopsis [Unique table management functions.] + + Description [External procedures included in this module: + <ul> + <li> Cudd_Prime() + </ul> + Internal procedures included in this module: + <ul> + <li> cuddAllocNode() + <li> cuddInitTable() + <li> cuddFreeTable() + <li> cuddGarbageCollect() + <li> cuddGarbageCollectZdd() + <li> cuddZddGetNode() + <li> cuddZddGetNodeIVO() + <li> cuddUniqueInter() + <li> cuddUniqueInterIVO() + <li> cuddUniqueInterZdd() + <li> cuddUniqueConst() + <li> cuddRehash() + <li> cuddShrinkSubtable() + <li> cuddInsertSubtables() + <li> cuddDestroySubtables() + <li> cuddResizeTableZdd() + <li> cuddSlowTableGrowth() + </ul> + Static procedures included in this module: + <ul> + <li> ddRehashZdd() + <li> ddResizeTable() + <li> cuddFindParent() + <li> cuddOrderedInsert() + <li> cuddOrderedThread() + <li> cuddRotateLeft() + <li> cuddRotateRight() + <li> cuddDoRebalance() + <li> cuddCheckCollisionOrdering() + </ul>] + + SeeAlso [] + + Author [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 */ +/*---------------------------------------------------------------------------*/ + +#ifndef DD_UNSORTED_FREE_LIST +/* Constants for red/black trees. */ +#define DD_STACK_SIZE 128 +#define DD_RED 0 +#define DD_BLACK 1 +#define DD_PAGE_SIZE 8192 +#define DD_PAGE_MASK ~(DD_PAGE_SIZE - 1) +#define DD_INSERT_COMPARE(x,y) \ + (((ptruint) (x) & DD_PAGE_MASK) - ((ptruint) (y) & DD_PAGE_MASK)) +#endif + +/*---------------------------------------------------------------------------*/ +/* Stucture declarations */ +/*---------------------------------------------------------------------------*/ + +/* This is a hack for when CUDD_VALUE_TYPE is double */ +typedef union hack { + CUDD_VALUE_TYPE value; + unsigned int bits[2]; +} hack; + +/*---------------------------------------------------------------------------*/ +/* Type declarations */ +/*---------------------------------------------------------------------------*/ + +/*---------------------------------------------------------------------------*/ +/* Variable declarations */ +/*---------------------------------------------------------------------------*/ + +#ifndef lint +static char rcsid[] DD_UNUSED = "$Id: cuddTable.c,v 1.1.1.1 2003/02/24 22:23:53 wjiang Exp $"; +#endif + +/*---------------------------------------------------------------------------*/ +/* Macro declarations */ +/*---------------------------------------------------------------------------*/ + + +#ifndef DD_UNSORTED_FREE_LIST +/* Macros for red/black trees. */ +#define DD_COLOR(p) ((p)->index) +#define DD_IS_BLACK(p) ((p)->index == DD_BLACK) +#define DD_IS_RED(p) ((p)->index == DD_RED) +#define DD_LEFT(p) cuddT(p) +#define DD_RIGHT(p) cuddE(p) +#define DD_NEXT(p) ((p)->next) +#endif + + +/**AutomaticStart*************************************************************/ + +/*---------------------------------------------------------------------------*/ +/* Static function prototypes */ +/*---------------------------------------------------------------------------*/ + +static void ddRehashZdd ARGS((DdManager *unique, int i)); +static int ddResizeTable ARGS((DdManager *unique, int index)); +static int cuddFindParent ARGS((DdManager *table, DdNode *node)); +DD_INLINE static void ddFixLimits ARGS((DdManager *unique)); +static void cuddOrderedInsert ARGS((DdNodePtr *root, DdNodePtr node)); +static DdNode * cuddOrderedThread ARGS((DdNode *root, DdNode *list)); +static void cuddRotateLeft ARGS((DdNodePtr *nodeP)); +static void cuddRotateRight ARGS((DdNodePtr *nodeP)); +static void cuddDoRebalance ARGS((DdNodePtr **stack, int stackN)); +static void ddPatchTree ARGS((DdManager *dd, MtrNode *treenode)); +#ifdef DD_DEBUG +static int cuddCheckCollisionOrdering ARGS((DdManager *unique, int i, int j)); +#endif +static void ddReportRefMess ARGS((DdManager *unique, int i, char *caller)); + +/**AutomaticEnd***************************************************************/ + + +/*---------------------------------------------------------------------------*/ +/* Definition of exported functions */ +/*---------------------------------------------------------------------------*/ + + +/**Function******************************************************************** + + Synopsis [Returns the next prime >= p.] + + Description [] + + SideEffects [None] + +******************************************************************************/ +unsigned int +Cudd_Prime( + unsigned int p) +{ + int i,pn; + + p--; + do { + p++; + if (p&1) { + pn = 1; + i = 3; + while ((unsigned) (i * i) <= p) { + if (p % i == 0) { + pn = 0; + break; + } + i += 2; + } + } else { + pn = 0; + } + } while (!pn); + return(p); + +} /* end of Cudd_Prime */ + + +/*---------------------------------------------------------------------------*/ +/* Definition of internal functions */ +/*---------------------------------------------------------------------------*/ + + +/**Function******************************************************************** + + Synopsis [Fast storage allocation for DdNodes in the table.] + + Description [Fast storage allocation for DdNodes in the table. The + first 4 bytes of a chunk contain a pointer to the next block; the + rest contains DD_MEM_CHUNK spaces for DdNodes. Returns a pointer to + a new node if successful; NULL is memory is full.] + + SideEffects [None] + + SeeAlso [cuddDynamicAllocNode] + +******************************************************************************/ +DdNode * +cuddAllocNode( + DdManager * unique) +{ + int i; + DdNodePtr *mem; + DdNode *list, *node; + extern void (*MMoutOfMemory)(long); + void (*saveHandler)(long); + + if (unique->nextFree == NULL) { /* free list is empty */ + /* Check for exceeded limits. */ + if ((unique->keys - unique->dead) + (unique->keysZ - unique->deadZ) > + unique->maxLive) { + unique->errorCode = CUDD_TOO_MANY_NODES; + return(NULL); + } + if (unique->stash == NULL || unique->memused > unique->maxmemhard) { + (void) cuddGarbageCollect(unique,1); + mem = NULL; + } + if (unique->nextFree == NULL) { + if (unique->memused > unique->maxmemhard) { + unique->errorCode = CUDD_MAX_MEM_EXCEEDED; + return(NULL); + } + /* Try to allocate a new block. */ + saveHandler = MMoutOfMemory; + MMoutOfMemory = Cudd_OutOfMem; + mem = (DdNodePtr *) ALLOC(DdNode,DD_MEM_CHUNK + 1); + MMoutOfMemory = saveHandler; + if (mem == NULL) { + /* No more memory: Try collecting garbage. If this succeeds, + ** we end up with mem still NULL, but unique->nextFree != + ** NULL. */ + if (cuddGarbageCollect(unique,1) == 0) { + /* Last resort: Free the memory stashed away, if there + ** any. If this succeeeds, mem != NULL and + ** unique->nextFree still NULL. */ + if (unique->stash != NULL) { + FREE(unique->stash); + unique->stash = NULL; + /* Inhibit resizing of tables. */ + cuddSlowTableGrowth(unique); + /* Now try again. */ + 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)); + unique->errorCode = CUDD_MEMORY_OUT; +#ifdef DD_VERBOSE + (void) fprintf(unique->err, + "cuddAllocNode: out of memory"); + (void) fprintf(unique->err, "Memory in use = %ld\n", + unique->memused); +#endif + return(NULL); + } + } + } + if (mem != NULL) { /* successful allocation; slice memory */ + ptruint offset; + unique->memused += (DD_MEM_CHUNK + 1) * sizeof(DdNode); + mem[0] = (DdNodePtr) unique->memoryList; + unique->memoryList = mem; + + /* Here we rely on the fact that a DdNode is as large + ** as 4 pointers. */ + offset = (ptruint) mem & (sizeof(DdNode) - 1); + mem += (sizeof(DdNode) - offset) / sizeof(DdNodePtr); + assert(((ptruint) mem & (sizeof(DdNode) - 1)) == 0); + list = (DdNode *) mem; + + i = 1; + do { + list[i - 1].next = &list[i]; + } while (++i < DD_MEM_CHUNK); + + list[DD_MEM_CHUNK-1].next = NULL; + + unique->nextFree = &list[0]; + } + } + } + unique->allocated++; + node = unique->nextFree; + unique->nextFree = node->next; + return(node); + +} /* end of cuddAllocNode */ + + +/**Function******************************************************************** + + Synopsis [Creates and initializes the unique table.] + + Description [Creates and initializes the unique table. Returns a pointer + to the table if successful; NULL otherwise.] + + SideEffects [None] + + SeeAlso [Cudd_Init cuddFreeTable] + +******************************************************************************/ +DdManager * +cuddInitTable( + unsigned int numVars /* Initial number of BDD variables (and subtables) */, + unsigned int numVarsZ /* Initial number of ZDD variables (and subtables) */, + unsigned int numSlots /* Initial size of the BDD subtables */, + unsigned int looseUpTo /* Limit for fast table growth */) +{ + DdManager *unique = ALLOC(DdManager,1); + int i, j; + DdNodePtr *nodelist; + DdNode *sentinel; + unsigned int slots; + int shift; + + if (unique == NULL) { + return(NULL); + } + sentinel = &(unique->sentinel); + sentinel->ref = 0; + sentinel->index = 0; + cuddT(sentinel) = NULL; + cuddE(sentinel) = NULL; + sentinel->next = NULL; + unique->epsilon = DD_EPSILON; + unique->maxGrowth = DD_MAX_REORDER_GROWTH; + unique->maxGrowthAlt = 2.0 * DD_MAX_REORDER_GROWTH; + unique->reordCycle = 0; /* do not use alternate threshold */ + unique->size = numVars; + unique->sizeZ = numVarsZ; + unique->maxSize = ddMax(DD_DEFAULT_RESIZE, numVars); + unique->maxSizeZ = ddMax(DD_DEFAULT_RESIZE, numVarsZ); + + /* Adjust the requested number of slots to a power of 2. */ + slots = 8; + while (slots < numSlots) { + slots <<= 1; + } + unique->initSlots = slots; + shift = sizeof(int) * 8 - cuddComputeFloorLog2(slots); + + unique->slots = (numVars + numVarsZ + 1) * slots; + unique->keys = 0; + unique->maxLive = ~0; /* very large number */ + unique->keysZ = 0; + unique->dead = 0; + unique->deadZ = 0; + unique->gcFrac = DD_GC_FRAC_HI; + unique->minDead = (unsigned) (DD_GC_FRAC_HI * (double) unique->slots); + unique->looseUpTo = looseUpTo; + unique->gcEnabled = 1; + unique->allocated = 0; + unique->reclaimed = 0; + unique->subtables = ALLOC(DdSubtable,unique->maxSize); + if (unique->subtables == NULL) { + unique->errorCode = CUDD_MEMORY_OUT; + return(0); + } + unique->subtableZ = ALLOC(DdSubtable,unique->maxSizeZ); + if (unique->subtableZ == NULL) { + unique->errorCode = CUDD_MEMORY_OUT; + return(0); + } + unique->perm = ALLOC(int,unique->maxSize); + if (unique->perm == NULL) { + unique->errorCode = CUDD_MEMORY_OUT; + return(0); + } + unique->invperm = ALLOC(int,unique->maxSize); + if (unique->invperm == NULL) { + unique->errorCode = CUDD_MEMORY_OUT; + return(0); + } + unique->permZ = ALLOC(int,unique->maxSizeZ); + if (unique->permZ == NULL) { + unique->errorCode = CUDD_MEMORY_OUT; + return(0); + } + unique->invpermZ = ALLOC(int,unique->maxSizeZ); + if (unique->invpermZ == NULL) { + unique->errorCode = CUDD_MEMORY_OUT; + return(0); + } + unique->map = NULL; + unique->stack = ALLOC(DdNodePtr,ddMax(unique->maxSize,unique->maxSizeZ)+1); + if (unique->stack == NULL) { + unique->errorCode = CUDD_MEMORY_OUT; + return(0); + } + unique->stack[0] = NULL; /* to suppress harmless UMR */ + +#ifndef DD_NO_DEATH_ROW + unique->deathRowDepth = 1 << cuddComputeFloorLog2(unique->looseUpTo >> 2); + unique->deathRow = ALLOC(DdNodePtr,unique->deathRowDepth); + if (unique->deathRow == NULL) { + unique->errorCode = CUDD_MEMORY_OUT; + return(0); + } + for (i = 0; i < unique->deathRowDepth; i++) { + unique->deathRow[i] = NULL; + } + unique->nextDead = 0; + unique->deadMask = unique->deathRowDepth - 1; +#endif + + for (i = 0; (unsigned) i < numVars; i++) { + unique->subtables[i].slots = slots; + unique->subtables[i].shift = shift; + unique->subtables[i].keys = 0; + unique->subtables[i].dead = 0; + unique->subtables[i].maxKeys = slots * DD_MAX_SUBTABLE_DENSITY; + unique->subtables[i].bindVar = 0; + unique->subtables[i].varType = CUDD_VAR_PRIMARY_INPUT; + unique->subtables[i].pairIndex = 0; + unique->subtables[i].varHandled = 0; + unique->subtables[i].varToBeGrouped = CUDD_LAZY_NONE; + + nodelist = unique->subtables[i].nodelist = ALLOC(DdNodePtr,slots); + if (nodelist == NULL) { + unique->errorCode = CUDD_MEMORY_OUT; + return(NULL); + } + for (j = 0; (unsigned) j < slots; j++) { + nodelist[j] = sentinel; + } + unique->perm[i] = i; + unique->invperm[i] = i; + } + for (i = 0; (unsigned) i < numVarsZ; i++) { + unique->subtableZ[i].slots = slots; + unique->subtableZ[i].shift = shift; + unique->subtableZ[i].keys = 0; + unique->subtableZ[i].dead = 0; + unique->subtableZ[i].maxKeys = slots * DD_MAX_SUBTABLE_DENSITY; + nodelist = unique->subtableZ[i].nodelist = ALLOC(DdNodePtr,slots); + if (nodelist == NULL) { + unique->errorCode = CUDD_MEMORY_OUT; + return(NULL); + } + for (j = 0; (unsigned) j < slots; j++) { + nodelist[j] = NULL; + } + unique->permZ[i] = i; + unique->invpermZ[i] = i; + } + unique->constants.slots = slots; + unique->constants.shift = shift; + unique->constants.keys = 0; + unique->constants.dead = 0; + unique->constants.maxKeys = slots * DD_MAX_SUBTABLE_DENSITY; + nodelist = unique->constants.nodelist = ALLOC(DdNodePtr,slots); + if (nodelist == NULL) { + unique->errorCode = CUDD_MEMORY_OUT; + return(NULL); + } + for (j = 0; (unsigned) j < slots; j++) { + nodelist[j] = NULL; + } + + unique->memoryList = NULL; + unique->nextFree = NULL; + + unique->memused = sizeof(DdManager) + (unique->maxSize + unique->maxSizeZ) + * (sizeof(DdSubtable) + 2 * sizeof(int)) + (numVars + 1) * + slots * sizeof(DdNodePtr) + + (ddMax(unique->maxSize,unique->maxSizeZ) + 1) * sizeof(DdNodePtr); +#ifndef DD_NO_DEATH_ROW + unique->memused += unique->deathRowDepth * sizeof(DdNodePtr); +#endif + + /* Initialize fields concerned with automatic dynamic reordering */ + unique->reorderings = 0; + unique->autoDyn = 0; /* initially disabled */ + unique->autoDynZ = 0; /* initially disabled */ + unique->realign = 0; /* initially disabled */ + unique->realignZ = 0; /* initially disabled */ + unique->reordered = 0; + unique->autoMethod = CUDD_REORDER_SIFT; + unique->autoMethodZ = CUDD_REORDER_SIFT; + unique->nextDyn = DD_FIRST_REORDER; + unique->countDead = ~0; + unique->siftMaxVar = DD_SIFT_MAX_VAR; + unique->siftMaxSwap = DD_SIFT_MAX_SWAPS; + unique->tree = NULL; + unique->treeZ = NULL; + unique->groupcheck = CUDD_GROUP_CHECK7; + unique->recomb = DD_DEFAULT_RECOMB; + unique->symmviolation = 0; + unique->arcviolation = 0; + unique->populationSize = 0; + unique->numberXovers = 0; + unique->linear = NULL; + unique->linearSize = 0; + + /* Initialize ZDD universe. */ + unique->univ = (DdNodePtr *)NULL; + + /* Initialize auxiliary fields. */ + unique->localCaches = NULL; + unique->preGCHook = NULL; + unique->postGCHook = NULL; + unique->preReorderingHook = NULL; + unique->postReorderingHook = NULL; + unique->out = stdout; + unique->err = stderr; + unique->errorCode = CUDD_NO_ERROR; + + /* Initialize statistical counters. */ + unique->maxmemhard = (long) ((~ (unsigned long) 0) >> 1); + unique->garbageCollections = 0; + unique->GCTime = 0; + unique->reordTime = 0; +#ifdef DD_STATS + unique->nodesDropped = 0; + unique->nodesFreed = 0; +#endif + unique->peakLiveNodes = 0; +#ifdef DD_UNIQUE_PROFILE + unique->uniqueLookUps = 0; + unique->uniqueLinks = 0; +#endif +#ifdef DD_COUNT + unique->recursiveCalls = 0; + unique->swapSteps = 0; +#ifdef DD_STATS + unique->nextSample = 250000; +#endif +#endif + + return(unique); + +} /* end of cuddInitTable */ + + +/**Function******************************************************************** + + Synopsis [Frees the resources associated to a unique table.] + + Description [] + + SideEffects [None] + + SeeAlso [cuddInitTable] + +******************************************************************************/ +void +cuddFreeTable( + DdManager * unique) +{ + DdNodePtr *next; + DdNodePtr *memlist = unique->memoryList; + int i; + + if (unique->univ != NULL) cuddZddFreeUniv(unique); + while (memlist != NULL) { + next = (DdNodePtr *) memlist[0]; /* link to next block */ + FREE(memlist); + memlist = next; + } + unique->nextFree = NULL; + unique->memoryList = NULL; + + for (i = 0; i < unique->size; i++) { + FREE(unique->subtables[i].nodelist); + } + for (i = 0; i < unique->sizeZ; i++) { + FREE(unique->subtableZ[i].nodelist); + } + FREE(unique->constants.nodelist); + FREE(unique->subtables); + FREE(unique->subtableZ); + FREE(unique->acache); + FREE(unique->perm); + FREE(unique->permZ); + FREE(unique->invperm); + FREE(unique->invpermZ); + FREE(unique->vars); + if (unique->map != NULL) FREE(unique->map); + FREE(unique->stack); +#ifndef DD_NO_DEATH_ROW + FREE(unique->deathRow); +#endif + if (unique->tree != NULL) Mtr_FreeTree(unique->tree); + if (unique->treeZ != NULL) Mtr_FreeTree(unique->treeZ); + if (unique->linear != NULL) FREE(unique->linear); + while (unique->preGCHook != NULL) + Cudd_RemoveHook(unique,unique->preGCHook->f,CUDD_PRE_GC_HOOK); + while (unique->postGCHook != NULL) + Cudd_RemoveHook(unique,unique->postGCHook->f,CUDD_POST_GC_HOOK); + while (unique->preReorderingHook != NULL) + Cudd_RemoveHook(unique,unique->preReorderingHook->f, + CUDD_PRE_REORDERING_HOOK); + while (unique->postReorderingHook != NULL) + Cudd_RemoveHook(unique,unique->postReorderingHook->f, + CUDD_POST_REORDERING_HOOK); + FREE(unique); + +} /* end of cuddFreeTable */ + + +/**Function******************************************************************** + + Synopsis [Performs garbage collection on a unique table.] + + Description [Performs garbage collection on a unique table. + If clearCache is 0, the cache is not cleared. This should only be + specified if the cache has been cleared right before calling + cuddGarbageCollect. (As in the case of dynamic reordering.) + Returns the total number of deleted nodes.] + + SideEffects [None] + + SeeAlso [cuddGarbageCollectZdd] + +******************************************************************************/ +int +cuddGarbageCollect( + DdManager * unique, + int clearCache) +{ + DdHook *hook; + DdCache *cache = unique->cache; + DdNode *sentinel = &(unique->sentinel); + DdNodePtr *nodelist; + int i, j, deleted, totalDeleted; + DdCache *c; + DdNode *node,*next; + DdNodePtr *lastP; + int slots; + long localTime; +#ifndef DD_UNSORTED_FREE_LIST + DdNodePtr tree; +#endif + +#ifndef DD_NO_DEATH_ROW + cuddClearDeathRow(unique); +#endif + + hook = unique->preGCHook; + while (hook != NULL) { + int res = (hook->f)(unique,"BDD",NULL); + if (res == 0) return(0); + hook = hook->next; + } + + if (unique->dead == 0) { + hook = unique->postGCHook; + while (hook != NULL) { + int res = (hook->f)(unique,"BDD",NULL); + if (res == 0) return(0); + hook = hook->next; + } + return(0); + } + + /* If many nodes are being reclaimed, we want to resize the tables + ** more aggressively, to reduce the frequency of garbage collection. + */ + if (clearCache && unique->gcFrac == DD_GC_FRAC_LO && + unique->slots <= unique->looseUpTo && unique->stash != NULL) { + unique->minDead = (unsigned) (DD_GC_FRAC_HI * (double) unique->slots); +#ifdef DD_VERBOSE + (void) fprintf(unique->err,"GC fraction = %.2f\t", DD_GC_FRAC_HI); + (void) fprintf(unique->err,"minDead = %d\n", unique->minDead); +#endif + unique->gcFrac = DD_GC_FRAC_HI; + return(0); + } + + localTime = util_cpu_time(); + + unique->garbageCollections++; +#ifdef DD_VERBOSE + (void) fprintf(unique->err, + "garbage collecting (%d dead out of %d, min %d)...", + unique->dead, unique->keys, unique->minDead); +#endif + + /* Remove references to garbage collected nodes from the cache. */ + if (clearCache) { + slots = unique->cacheSlots; + for (i = 0; i < slots; i++) { + c = &cache[i]; + if (c->data != NULL) { + if (cuddClean(c->f)->ref == 0 || + cuddClean(c->g)->ref == 0 || + (((ptruint)c->f & 0x2) && Cudd_Regular(c->h)->ref == 0) || + (c->data != DD_NON_CONSTANT && + Cudd_Regular(c->data)->ref == 0)) { + c->data = NULL; + unique->cachedeletions++; + } + } + } + cuddLocalCacheClearDead(unique); + } + + /* Now return dead nodes to free list. Count them for sanity check. */ + totalDeleted = 0; +#ifndef DD_UNSORTED_FREE_LIST + tree = NULL; +#endif + + for (i = 0; i < unique->size; i++) { + if (unique->subtables[i].dead == 0) continue; + nodelist = unique->subtables[i].nodelist; + + deleted = 0; + slots = unique->subtables[i].slots; + for (j = 0; j < slots; j++) { + lastP = &(nodelist[j]); + node = *lastP; + while (node != sentinel) { + next = node->next; + if (node->ref == 0) { + deleted++; +#ifndef DD_UNSORTED_FREE_LIST +#ifdef __osf__ +#pragma pointer_size save +#pragma pointer_size short +#endif + cuddOrderedInsert(&tree,node); +#ifdef __osf__ +#pragma pointer_size restore +#endif +#else + cuddDeallocNode(unique,node); +#endif + } else { + *lastP = node; + lastP = &(node->next); + } + node = next; + } + *lastP = sentinel; + } + if ((unsigned) deleted != unique->subtables[i].dead) { + ddReportRefMess(unique, i, "cuddGarbageCollect"); + } + totalDeleted += deleted; + unique->subtables[i].keys -= deleted; + unique->subtables[i].dead = 0; + } + if (unique->constants.dead != 0) { + nodelist = unique->constants.nodelist; + deleted = 0; + slots = unique->constants.slots; + for (j = 0; j < slots; j++) { + lastP = &(nodelist[j]); + node = *lastP; + while (node != NULL) { + next = node->next; + if (node->ref == 0) { + deleted++; +#ifndef DD_UNSORTED_FREE_LIST +#ifdef __osf__ +#pragma pointer_size save +#pragma pointer_size short +#endif + cuddOrderedInsert(&tree,node); +#ifdef __osf__ +#pragma pointer_size restore +#endif +#else + cuddDeallocNode(unique,node); +#endif + } else { + *lastP = node; + lastP = &(node->next); + } + node = next; + } + *lastP = NULL; + } + if ((unsigned) deleted != unique->constants.dead) { + ddReportRefMess(unique, CUDD_CONST_INDEX, "cuddGarbageCollect"); + } + totalDeleted += deleted; + unique->constants.keys -= deleted; + unique->constants.dead = 0; + } + if ((unsigned) totalDeleted != unique->dead) { + ddReportRefMess(unique, -1, "cuddGarbageCollect"); + } + unique->keys -= totalDeleted; + unique->dead = 0; +#ifdef DD_STATS + unique->nodesFreed += (double) totalDeleted; +#endif + +#ifndef DD_UNSORTED_FREE_LIST + unique->nextFree = cuddOrderedThread(tree,unique->nextFree); +#endif + + unique->GCTime += util_cpu_time() - localTime; + + hook = unique->postGCHook; + while (hook != NULL) { + int res = (hook->f)(unique,"BDD",NULL); + if (res == 0) return(0); + hook = hook->next; + } + +#ifdef DD_VERBOSE + (void) fprintf(unique->err," done\n"); +#endif + + return(totalDeleted); + +} /* end of cuddGarbageCollect */ + + +/**Function******************************************************************** + + Synopsis [Performs garbage collection on a ZDD unique table.] + + Description [Performs garbage collection on a ZDD unique table. + If clearCache is 0, the cache is not cleared. This should only be + specified if the cache has been cleared right before calling + cuddGarbageCollectZdd. (As in the case of dynamic reordering.) + Returns the total number of deleted nodes.] + + SideEffects [None] + + SeeAlso [cuddGarbageCollect] + +******************************************************************************/ +int +cuddGarbageCollectZdd( + DdManager * unique, + int clearCache) +{ + DdHook *hook; + DdCache *cache = unique->cache; + DdNodePtr *nodelist; + int i, j, deleted, totalDeleted; + DdCache *c; + DdNode *node,*next; + DdNodePtr *lastP; + int slots; + long localTime; +#ifndef DD_UNSORTED_FREE_LIST + DdNodePtr tree; +#endif + + hook = unique->preGCHook; + while (hook != NULL) { + int res = (hook->f)(unique,"ZDD",NULL); + if (res == 0) return(0); + hook = hook->next; + } + + if (unique->deadZ == 0) { + hook = unique->postGCHook; + while (hook != NULL) { + int res = (hook->f)(unique,"ZDD",NULL); + if (res == 0) return(0); + hook = hook->next; + } + return(0); + } + + /* If many nodes are being reclaimed, we want to resize the tables + ** more aggressively, to reduce the frequency of garbage collection. + */ + if (clearCache && unique->slots <= unique->looseUpTo) { + unique->minDead = (unsigned) (DD_GC_FRAC_HI * (double) unique->slots); +#ifdef DD_VERBOSE + if (unique->gcFrac == DD_GC_FRAC_LO) { + (void) fprintf(unique->err,"GC fraction = %.2f\t", + DD_GC_FRAC_HI); + (void) fprintf(unique->err,"minDead = %d\n", unique->minDead); + } +#endif + unique->gcFrac = DD_GC_FRAC_HI; + } + + localTime = util_cpu_time(); + + unique->garbageCollections++; +#ifdef DD_VERBOSE + (void) fprintf(unique->err,"garbage collecting (%d dead out of %d)...", + unique->deadZ,unique->keysZ); +#endif + + /* Remove references to garbage collected nodes from the cache. */ + if (clearCache) { + slots = unique->cacheSlots; + for (i = 0; i < slots; i++) { + c = &cache[i]; + if (c->data != NULL) { + if (cuddClean(c->f)->ref == 0 || + cuddClean(c->g)->ref == 0 || + (((ptruint)c->f & 0x2) && Cudd_Regular(c->h)->ref == 0) || + (c->data != DD_NON_CONSTANT && + Cudd_Regular(c->data)->ref == 0)) { + c->data = NULL; + unique->cachedeletions++; + } + } + } + } + + /* Now return dead nodes to free list. Count them for sanity check. */ + totalDeleted = 0; +#ifndef DD_UNSORTED_FREE_LIST + tree = NULL; +#endif + + for (i = 0; i < unique->sizeZ; i++) { + if (unique->subtableZ[i].dead == 0) continue; + nodelist = unique->subtableZ[i].nodelist; + + deleted = 0; + slots = unique->subtableZ[i].slots; + for (j = 0; j < slots; j++) { + lastP = &(nodelist[j]); + node = *lastP; + while (node != NULL) { + next = node->next; + if (node->ref == 0) { + deleted++; +#ifndef DD_UNSORTED_FREE_LIST +#ifdef __osf__ +#pragma pointer_size save +#pragma pointer_size short +#endif + cuddOrderedInsert(&tree,node); +#ifdef __osf__ +#pragma pointer_size restore +#endif +#else + cuddDeallocNode(unique,node); +#endif + } else { + *lastP = node; + lastP = &(node->next); + } + node = next; + } + *lastP = NULL; + } + if ((unsigned) deleted != unique->subtableZ[i].dead) { + ddReportRefMess(unique, i, "cuddGarbageCollectZdd"); + } + totalDeleted += deleted; + unique->subtableZ[i].keys -= deleted; + unique->subtableZ[i].dead = 0; + } + + /* No need to examine the constant table for ZDDs. + ** If we did we should be careful not to count whatever dead + ** nodes we found there among the dead ZDD nodes. */ + if ((unsigned) totalDeleted != unique->deadZ) { + ddReportRefMess(unique, -1, "cuddGarbageCollectZdd"); + } + unique->keysZ -= totalDeleted; + unique->deadZ = 0; +#ifdef DD_STATS + unique->nodesFreed += (double) totalDeleted; +#endif + +#ifndef DD_UNSORTED_FREE_LIST + unique->nextFree = cuddOrderedThread(tree,unique->nextFree); +#endif + + unique->GCTime += util_cpu_time() - localTime; + + hook = unique->postGCHook; + while (hook != NULL) { + int res = (hook->f)(unique,"ZDD",NULL); + if (res == 0) return(0); + hook = hook->next; + } + +#ifdef DD_VERBOSE + (void) fprintf(unique->err," done\n"); +#endif + + return(totalDeleted); + +} /* end of cuddGarbageCollectZdd */ + + +/**Function******************************************************************** + + Synopsis [Wrapper for cuddUniqueInterZdd.] + + Description [Wrapper for cuddUniqueInterZdd, which applies the ZDD + reduction rule. Returns a pointer to the result node under normal + conditions; NULL if reordering occurred or memory was exhausted.] + + SideEffects [None] + + SeeAlso [cuddUniqueInterZdd] + +******************************************************************************/ +DdNode * +cuddZddGetNode( + DdManager * zdd, + int id, + DdNode * T, + DdNode * E) +{ + DdNode *node; + + if (T == DD_ZERO(zdd)) + return(E); + node = cuddUniqueInterZdd(zdd, id, T, E); + return(node); + +} /* end of cuddZddGetNode */ + + +/**Function******************************************************************** + + Synopsis [Wrapper for cuddUniqueInterZdd that is independent of variable + ordering.] + + Description [Wrapper for cuddUniqueInterZdd that is independent of + variable ordering (IVO). This function does not require parameter + index to precede the indices of the top nodes of g and h in the + variable order. Returns a pointer to the result node under normal + conditions; NULL if reordering occurred or memory was exhausted.] + + SideEffects [None] + + SeeAlso [cuddZddGetNode cuddZddIsop] + +******************************************************************************/ +DdNode * +cuddZddGetNodeIVO( + DdManager * dd, + int index, + DdNode * g, + DdNode * h) +{ + DdNode *f, *r, *t; + DdNode *zdd_one = DD_ONE(dd); + DdNode *zdd_zero = DD_ZERO(dd); + + f = cuddUniqueInterZdd(dd, index, zdd_one, zdd_zero); + if (f == NULL) { + return(NULL); + } + cuddRef(f); + t = cuddZddProduct(dd, f, g); + if (t == NULL) { + Cudd_RecursiveDerefZdd(dd, f); + return(NULL); + } + cuddRef(t); + Cudd_RecursiveDerefZdd(dd, f); + r = cuddZddUnion(dd, t, h); + if (r == NULL) { + Cudd_RecursiveDerefZdd(dd, t); + return(NULL); + } + cuddRef(r); + Cudd_RecursiveDerefZdd(dd, t); + + cuddDeref(r); + return(r); + +} /* end of cuddZddGetNodeIVO */ + + +/**Function******************************************************************** + + Synopsis [Checks the unique table for the existence of an internal node.] + + Description [Checks the unique table for the existence of an internal + node. If it does not exist, it creates a new one. Does not + modify the reference count of whatever is returned. A newly created + internal node comes back with a reference count 0. For a newly + created node, increments the reference counts of what T and E point + to. Returns a pointer to the new node if successful; NULL if memory + is exhausted or if reordering took place.] + + SideEffects [None] + + SeeAlso [cuddUniqueInterZdd] + +******************************************************************************/ +DdNode * +cuddUniqueInter( + DdManager * unique, + int index, + DdNode * T, + DdNode * E) +{ + int pos; + unsigned int level; + int retval; + DdNodePtr *nodelist; + DdNode *looking; + DdNodePtr *previousP; + DdSubtable *subtable; + int gcNumber; + +#ifdef DD_UNIQUE_PROFILE + unique->uniqueLookUps++; +#endif + + if (index >= unique->size) { + if (!ddResizeTable(unique,index)) return(NULL); + } + + level = unique->perm[index]; + subtable = &(unique->subtables[level]); + +#ifdef DD_DEBUG + assert(level < (unsigned) cuddI(unique,T->index)); + assert(level < (unsigned) cuddI(unique,Cudd_Regular(E)->index)); +#endif + + pos = ddHash(T, E, subtable->shift); + nodelist = subtable->nodelist; + previousP = &(nodelist[pos]); + looking = *previousP; + + while (T < cuddT(looking)) { + previousP = &(looking->next); + looking = *previousP; +#ifdef DD_UNIQUE_PROFILE + unique->uniqueLinks++; +#endif + } + while (T == cuddT(looking) && E < cuddE(looking)) { + previousP = &(looking->next); + looking = *previousP; +#ifdef DD_UNIQUE_PROFILE + unique->uniqueLinks++; +#endif + } + if (T == cuddT(looking) && E == cuddE(looking)) { + if (looking->ref == 0) { + cuddReclaim(unique,looking); + } + return(looking); + } + + /* countDead is 0 if deads should be counted and ~0 if they should not. */ + if (unique->autoDyn && + unique->keys - (unique->dead & unique->countDead) >= unique->nextDyn) { +#ifdef DD_DEBUG + retval = Cudd_DebugCheck(unique); + if (retval != 0) return(NULL); + retval = Cudd_CheckKeys(unique); + if (retval != 0) return(NULL); +#endif + retval = Cudd_ReduceHeap(unique,unique->autoMethod,10); /* 10 = whatever */ + if (retval == 0) unique->reordered = 2; +#ifdef DD_DEBUG + retval = Cudd_DebugCheck(unique); + if (retval != 0) unique->reordered = 2; + retval = Cudd_CheckKeys(unique); + if (retval != 0) unique->reordered = 2; +#endif + return(NULL); + } + + if (subtable->keys > subtable->maxKeys) { + if (unique->gcEnabled && + ((unique->dead > unique->minDead) || + ((unique->dead > unique->minDead / 2) && + (subtable->dead > subtable->keys * 0.95)))) { /* too many dead */ + (void) cuddGarbageCollect(unique,1); + } else { + cuddRehash(unique,(int)level); + } + /* Update pointer to insertion point. In the case of rehashing, + ** the slot may have changed. In the case of garbage collection, + ** the predecessor may have been dead. */ + pos = ddHash(T, E, subtable->shift); + nodelist = subtable->nodelist; + previousP = &(nodelist[pos]); + looking = *previousP; + + while (T < cuddT(looking)) { + previousP = &(looking->next); + looking = *previousP; +#ifdef DD_UNIQUE_PROFILE + unique->uniqueLinks++; +#endif + } + while (T == cuddT(looking) && E < cuddE(looking)) { + previousP = &(looking->next); + looking = *previousP; +#ifdef DD_UNIQUE_PROFILE + unique->uniqueLinks++; +#endif + } + } + + gcNumber = unique->garbageCollections; + looking = cuddAllocNode(unique); + if (looking == NULL) { + return(NULL); + } + unique->keys++; + subtable->keys++; + + if (gcNumber != unique->garbageCollections) { + DdNode *looking2; + pos = ddHash(T, E, subtable->shift); + nodelist = subtable->nodelist; + previousP = &(nodelist[pos]); + looking2 = *previousP; + + while (T < cuddT(looking2)) { + previousP = &(looking2->next); + looking2 = *previousP; +#ifdef DD_UNIQUE_PROFILE + unique->uniqueLinks++; +#endif + } + while (T == cuddT(looking2) && E < cuddE(looking2)) { + previousP = &(looking2->next); + looking2 = *previousP; +#ifdef DD_UNIQUE_PROFILE + unique->uniqueLinks++; +#endif + } + } + looking->ref = 0; + looking->index = index; + cuddT(looking) = T; + cuddE(looking) = E; + looking->next = *previousP; + *previousP = looking; + cuddSatInc(T->ref); /* we know T is a regular pointer */ + cuddRef(E); + +#ifdef DD_DEBUG + cuddCheckCollisionOrdering(unique,level,pos); +#endif + + return(looking); + +} /* end of cuddUniqueInter */ + + +/**Function******************************************************************** + + Synopsis [Wrapper for cuddUniqueInter that is independent of variable + ordering.] + + Description [Wrapper for cuddUniqueInter that is independent of + variable ordering (IVO). This function does not require parameter + index to precede the indices of the top nodes of T and E in the + variable order. Returns a pointer to the result node under normal + conditions; NULL if reordering occurred or memory was exhausted.] + + SideEffects [None] + + SeeAlso [cuddUniqueInter Cudd_MakeBddFromZddCover] + +******************************************************************************/ +DdNode * +cuddUniqueInterIVO( + DdManager * unique, + int index, + DdNode * T, + DdNode * E) +{ + DdNode *result; + DdNode *v; + + v = cuddUniqueInter(unique, index, DD_ONE(unique), + Cudd_Not(DD_ONE(unique))); + if (v == NULL) + return(NULL); + cuddRef(v); + result = cuddBddIteRecur(unique, v, T, E); + Cudd_RecursiveDeref(unique, v); + return(result); +} + + +/**Function******************************************************************** + + Synopsis [Checks the unique table for the existence of an internal + ZDD node.] + + Description [Checks the unique table for the existence of an internal + ZDD node. If it does not exist, it creates a new one. Does not + modify the reference count of whatever is returned. A newly created + internal node comes back with a reference count 0. For a newly + created node, increments the reference counts of what T and E point + to. Returns a pointer to the new node if successful; NULL if memory + is exhausted or if reordering took place.] + + SideEffects [None] + + SeeAlso [cuddUniqueInter] + +******************************************************************************/ +DdNode * +cuddUniqueInterZdd( + DdManager * unique, + int index, + DdNode * T, + DdNode * E) +{ + int pos; + unsigned int level; + int retval; + DdNodePtr *nodelist; + DdNode *looking; + DdSubtable *subtable; + +#ifdef DD_UNIQUE_PROFILE + unique->uniqueLookUps++; +#endif + + if (index >= unique->sizeZ) { + if (!cuddResizeTableZdd(unique,index)) return(NULL); + } + + level = unique->permZ[index]; + subtable = &(unique->subtableZ[level]); + +#ifdef DD_DEBUG + assert(level < (unsigned) cuddIZ(unique,T->index)); + assert(level < (unsigned) cuddIZ(unique,Cudd_Regular(E)->index)); +#endif + + if (subtable->keys > subtable->maxKeys) { + if (unique->gcEnabled && ((unique->deadZ > unique->minDead) || + (10 * subtable->dead > 9 * subtable->keys))) { /* too many dead */ + (void) cuddGarbageCollectZdd(unique,1); + } else { + ddRehashZdd(unique,(int)level); + } + } + + pos = ddHash(T, E, subtable->shift); + nodelist = subtable->nodelist; + looking = nodelist[pos]; + + while (looking != NULL) { + if (cuddT(looking) == T && cuddE(looking) == E) { + if (looking->ref == 0) { + cuddReclaimZdd(unique,looking); + } + return(looking); + } + looking = looking->next; +#ifdef DD_UNIQUE_PROFILE + unique->uniqueLinks++; +#endif + } + + /* countDead is 0 if deads should be counted and ~0 if they should not. */ + if (unique->autoDynZ && + unique->keysZ - (unique->deadZ & unique->countDead) >= unique->nextDyn) { +#ifdef DD_DEBUG + retval = Cudd_DebugCheck(unique); + if (retval != 0) return(NULL); + retval = Cudd_CheckKeys(unique); + if (retval != 0) return(NULL); +#endif + retval = Cudd_zddReduceHeap(unique,unique->autoMethodZ,10); /* 10 = whatever */ + if (retval == 0) unique->reordered = 2; +#ifdef DD_DEBUG + retval = Cudd_DebugCheck(unique); + if (retval != 0) unique->reordered = 2; + retval = Cudd_CheckKeys(unique); + if (retval != 0) unique->reordered = 2; +#endif + return(NULL); + } + + unique->keysZ++; + subtable->keys++; + + looking = cuddAllocNode(unique); + if (looking == NULL) return(NULL); + looking->ref = 0; + looking->index = index; + cuddT(looking) = T; + cuddE(looking) = E; + looking->next = nodelist[pos]; + nodelist[pos] = looking; + cuddRef(T); + cuddRef(E); + + return(looking); + +} /* end of cuddUniqueInterZdd */ + + +/**Function******************************************************************** + + Synopsis [Checks the unique table for the existence of a constant node.] + + Description [Checks the unique table for the existence of a constant node. + If it does not exist, it creates a new one. Does not + modify the reference count of whatever is returned. A newly created + internal node comes back with a reference count 0. Returns a + pointer to the new node.] + + SideEffects [None] + +******************************************************************************/ +DdNode * +cuddUniqueConst( + DdManager * unique, + CUDD_VALUE_TYPE value) +{ + int pos; + DdNodePtr *nodelist; + DdNode *looking; + hack split; + +#ifdef DD_UNIQUE_PROFILE + unique->uniqueLookUps++; +#endif + + if (unique->constants.keys > unique->constants.maxKeys) { + if (unique->gcEnabled && ((unique->dead > unique->minDead) || + (10 * unique->constants.dead > 9 * unique->constants.keys))) { /* too many dead */ + (void) cuddGarbageCollect(unique,1); + } else { + cuddRehash(unique,CUDD_CONST_INDEX); + } + } + + cuddAdjust(value); /* for the case of crippled infinities */ + + if (ddAbs(value) < unique->epsilon) { + value = 0.0; + } + split.value = value; + + pos = ddHash(split.bits[0], split.bits[1], unique->constants.shift); + nodelist = unique->constants.nodelist; + looking = nodelist[pos]; + + /* Here we compare values both for equality and for difference less + * than epsilon. The first comparison is required when values are + * infinite, since Infinity - Infinity is NaN and NaN < X is 0 for + * every X. + */ + while (looking != NULL) { + if (looking->type.value == value || + ddEqualVal(looking->type.value,value,unique->epsilon)) { + if (looking->ref == 0) { + cuddReclaim(unique,looking); + } + return(looking); + } + looking = looking->next; +#ifdef DD_UNIQUE_PROFILE + unique->uniqueLinks++; +#endif + } + + unique->keys++; + unique->constants.keys++; + + looking = cuddAllocNode(unique); + if (looking == NULL) return(NULL); + looking->ref = 0; + looking->index = CUDD_CONST_INDEX; + looking->type.value = value; + looking->next = nodelist[pos]; + nodelist[pos] = looking; + + return(looking); + +} /* end of cuddUniqueConst */ + + +/**Function******************************************************************** + + Synopsis [Rehashes a unique subtable.] + + Description [Doubles the size of a unique subtable and rehashes its + contents.] + + SideEffects [None] + + SeeAlso [] + +******************************************************************************/ +void +cuddRehash( + DdManager * unique, + int i) +{ + unsigned int slots, oldslots; + int shift, oldshift; + int j, pos; + DdNodePtr *nodelist, *oldnodelist; + DdNode *node, *next; + DdNode *sentinel = &(unique->sentinel); + hack split; + extern void (*MMoutOfMemory)(long); + void (*saveHandler)(long); + + if (unique->gcFrac == DD_GC_FRAC_HI && unique->slots > unique->looseUpTo) { + unique->gcFrac = DD_GC_FRAC_LO; + unique->minDead = (unsigned) (DD_GC_FRAC_LO * (double) unique->slots); +#ifdef DD_VERBOSE + (void) fprintf(unique->err,"GC fraction = %.2f\t", DD_GC_FRAC_LO); + (void) fprintf(unique->err,"minDead = %d\n", unique->minDead); +#endif + } + + if (unique->gcFrac != DD_GC_FRAC_MIN && unique->memused > unique->maxmem) { + unique->gcFrac = DD_GC_FRAC_MIN; + unique->minDead = (unsigned) (DD_GC_FRAC_MIN * (double) unique->slots); +#ifdef DD_VERBOSE + (void) fprintf(unique->err,"GC fraction = %.2f\t", DD_GC_FRAC_MIN); + (void) fprintf(unique->err,"minDead = %d\n", unique->minDead); +#endif + cuddShrinkDeathRow(unique); + if (cuddGarbageCollect(unique,1) > 0) return; + } + + if (i != CUDD_CONST_INDEX) { + oldslots = unique->subtables[i].slots; + oldshift = unique->subtables[i].shift; + oldnodelist = unique->subtables[i].nodelist; + + /* Compute the new size of the subtable. */ + slots = oldslots << 1; + shift = oldshift - 1; + + saveHandler = MMoutOfMemory; + MMoutOfMemory = Cudd_OutOfMem; + nodelist = ALLOC(DdNodePtr, slots); + MMoutOfMemory = saveHandler; + if (nodelist == NULL) { + (void) fprintf(unique->err, + "Unable to resize subtable %d for lack of memory\n", + i); + /* Prevent frequent resizing attempts. */ + (void) cuddGarbageCollect(unique,1); + if (unique->stash != NULL) { + FREE(unique->stash); + unique->stash = NULL; + /* Inhibit resizing of tables. */ + cuddSlowTableGrowth(unique); + } + return; + } + unique->subtables[i].nodelist = nodelist; + unique->subtables[i].slots = slots; + unique->subtables[i].shift = shift; + unique->subtables[i].maxKeys = slots * DD_MAX_SUBTABLE_DENSITY; + + /* Move the nodes from the old table to the new table. + ** This code depends on the type of hash function. + ** It assumes that the effect of doubling the size of the table + ** is to retain one more bit of the 32-bit hash value. + ** The additional bit is the LSB. */ + for (j = 0; (unsigned) j < oldslots; j++) { + DdNodePtr *evenP, *oddP; + node = oldnodelist[j]; + evenP = &(nodelist[j<<1]); + oddP = &(nodelist[(j<<1)+1]); + while (node != sentinel) { + next = node->next; + pos = ddHash(cuddT(node), cuddE(node), shift); + if (pos & 1) { + *oddP = node; + oddP = &(node->next); + } else { + *evenP = node; + evenP = &(node->next); + } + node = next; + } + *evenP = *oddP = sentinel; + } + FREE(oldnodelist); + +#ifdef DD_VERBOSE + (void) fprintf(unique->err, + "rehashing layer %d: keys %d dead %d new size %d\n", + i, unique->subtables[i].keys, + unique->subtables[i].dead, slots); +#endif + } else { + oldslots = unique->constants.slots; + oldshift = unique->constants.shift; + oldnodelist = unique->constants.nodelist; + + /* The constant subtable is never subjected to reordering. + ** Therefore, when it is resized, it is because it has just + ** reached the maximum load. We can safely just double the size, + ** with no need for the loop we use for the other tables. + */ + slots = oldslots << 1; + shift = oldshift - 1; + saveHandler = MMoutOfMemory; + MMoutOfMemory = Cudd_OutOfMem; + nodelist = ALLOC(DdNodePtr, slots); + MMoutOfMemory = saveHandler; + if (nodelist == NULL) { + int j; + (void) fprintf(unique->err, + "Unable to resize constant subtable for lack of memory\n"); + (void) cuddGarbageCollect(unique,1); + for (j = 0; j < unique->size; j++) { + unique->subtables[j].maxKeys <<= 1; + } + unique->constants.maxKeys <<= 1; + return; + } + unique->constants.slots = slots; + unique->constants.shift = shift; + unique->constants.maxKeys = slots * DD_MAX_SUBTABLE_DENSITY; + unique->constants.nodelist = nodelist; + for (j = 0; (unsigned) j < slots; j++) { + nodelist[j] = NULL; + } + for (j = 0; (unsigned) j < oldslots; j++) { + node = oldnodelist[j]; + while (node != NULL) { + next = node->next; + split.value = cuddV(node); + pos = ddHash(split.bits[0], split.bits[1], shift); + node->next = nodelist[pos]; + nodelist[pos] = node; + node = next; + } + } + FREE(oldnodelist); + +#ifdef DD_VERBOSE + (void) fprintf(unique->err, + "rehashing constants: keys %d dead %d new size %d\n", + unique->constants.keys,unique->constants.dead,slots); +#endif + } + + /* Update global data */ + + unique->memused += (slots - oldslots) * sizeof(DdNodePtr); + unique->slots += (slots - oldslots); + ddFixLimits(unique); + +} /* end of cuddRehash */ + + +/**Function******************************************************************** + + Synopsis [Shrinks a subtable.] + + Description [Shrinks a subtable.] + + SideEffects [None] + + SeeAlso [cuddRehash] + +******************************************************************************/ +void +cuddShrinkSubtable( + DdManager *unique, + int i) +{ + int j; + int shift, posn; + DdNodePtr *nodelist, *oldnodelist; + DdNode *node, *next; + DdNode *sentinel = &(unique->sentinel); + unsigned int slots, oldslots; + extern void (*MMoutOfMemory)(long); + void (*saveHandler)(long); + + oldnodelist = unique->subtables[i].nodelist; + oldslots = unique->subtables[i].slots; + slots = oldslots >> 1; + saveHandler = MMoutOfMemory; + MMoutOfMemory = Cudd_OutOfMem; + nodelist = ALLOC(DdNodePtr, slots); + MMoutOfMemory = saveHandler; + if (nodelist == NULL) { + return; + } + unique->subtables[i].nodelist = nodelist; + unique->subtables[i].slots = slots; + unique->subtables[i].shift++; + unique->subtables[i].maxKeys = slots * DD_MAX_SUBTABLE_DENSITY; +#ifdef DD_VERBOSE + (void) fprintf(unique->err, + "shrunk layer %d (%d keys) from %d to %d slots\n", + i, unique->subtables[i].keys, oldslots, slots); +#endif + + for (j = 0; (unsigned) j < slots; j++) { + nodelist[j] = sentinel; + } + shift = unique->subtables[i].shift; + for (j = 0; (unsigned) j < oldslots; j++) { + node = oldnodelist[j]; + while (node != sentinel) { + DdNode *looking, *T, *E; + DdNodePtr *previousP; + next = node->next; + posn = ddHash(cuddT(node), cuddE(node), shift); + previousP = &(nodelist[posn]); + looking = *previousP; + T = cuddT(node); + E = cuddE(node); + while (T < cuddT(looking)) { + previousP = &(looking->next); + looking = *previousP; +#ifdef DD_UNIQUE_PROFILE + unique->uniqueLinks++; +#endif + } + while (T == cuddT(looking) && E < cuddE(looking)) { + previousP = &(looking->next); + looking = *previousP; +#ifdef DD_UNIQUE_PROFILE + unique->uniqueLinks++; +#endif + } + node->next = *previousP; + *previousP = node; + node = next; + } + } + FREE(oldnodelist); + + unique->memused += ((long) slots - (long) oldslots) * sizeof(DdNode *); + unique->slots += slots - oldslots; + unique->minDead = (unsigned) (unique->gcFrac * (double) unique->slots); + unique->cacheSlack = (int) + ddMin(unique->maxCacheHard,DD_MAX_CACHE_TO_SLOTS_RATIO * unique->slots) + - 2 * (int) unique->cacheSlots; + +} /* end of cuddShrinkSubtable */ + + +/**Function******************************************************************** + + Synopsis [Inserts n new subtables in a unique table at level.] + + Description [Inserts n new subtables in a unique table at level. + The number n should be positive, and level should be an existing level. + Returns 1 if successful; 0 otherwise.] + + SideEffects [None] + + SeeAlso [cuddDestroySubtables] + +******************************************************************************/ +int +cuddInsertSubtables( + DdManager * unique, + int n, + int level) +{ + DdSubtable *newsubtables; + DdNodePtr *newnodelist; + DdNodePtr *newvars; + DdNode *sentinel = &(unique->sentinel); + int oldsize,newsize; + int i,j,index,reorderSave; + unsigned int numSlots = unique->initSlots; + int *newperm, *newinvperm, *newmap; + DdNode *one, *zero; + +#ifdef DD_DEBUG + assert(n > 0 && level < unique->size); +#endif + + oldsize = unique->size; + /* Easy case: there is still room in the current table. */ + if (oldsize + n <= unique->maxSize) { + /* Shift the tables at and below level. */ + for (i = oldsize - 1; i >= level; i--) { + unique->subtables[i+n].slots = unique->subtables[i].slots; + unique->subtables[i+n].shift = unique->subtables[i].shift; + unique->subtables[i+n].keys = unique->subtables[i].keys; + unique->subtables[i+n].maxKeys = unique->subtables[i].maxKeys; + unique->subtables[i+n].dead = unique->subtables[i].dead; + unique->subtables[i+n].nodelist = unique->subtables[i].nodelist; + unique->subtables[i+n].bindVar = unique->subtables[i].bindVar; + unique->subtables[i+n].varType = unique->subtables[i].varType; + unique->subtables[i+n].pairIndex = unique->subtables[i].pairIndex; + unique->subtables[i+n].varHandled = unique->subtables[i].varHandled; + unique->subtables[i+n].varToBeGrouped = + unique->subtables[i].varToBeGrouped; + + index = unique->invperm[i]; + unique->invperm[i+n] = index; + unique->perm[index] += n; + } + /* Create new subtables. */ + for (i = 0; i < n; i++) { + unique->subtables[level+i].slots = numSlots; + unique->subtables[level+i].shift = sizeof(int) * 8 - + cuddComputeFloorLog2(numSlots); + unique->subtables[level+i].keys = 0; + unique->subtables[level+i].maxKeys = numSlots * DD_MAX_SUBTABLE_DENSITY; + unique->subtables[level+i].dead = 0; + unique->subtables[level+i].bindVar = 0; + unique->subtables[level+i].varType = CUDD_VAR_PRIMARY_INPUT; + unique->subtables[level+i].pairIndex = 0; + unique->subtables[level+i].varHandled = 0; + unique->subtables[level+i].varToBeGrouped = CUDD_LAZY_NONE; + + unique->perm[oldsize+i] = level + i; + unique->invperm[level+i] = oldsize + i; + newnodelist = unique->subtables[level+i].nodelist = + ALLOC(DdNodePtr, numSlots); + if (newnodelist == NULL) { + unique->errorCode = CUDD_MEMORY_OUT; + return(0); + } + for (j = 0; j < numSlots; j++) { + newnodelist[j] = sentinel; + } + } + if (unique->map != NULL) { + for (i = 0; i < n; i++) { + unique->map[oldsize+i] = oldsize + i; + } + } + } else { + /* The current table is too small: we need to allocate a new, + ** larger one; move all old subtables, and initialize the new + ** subtables. + */ + newsize = oldsize + n + DD_DEFAULT_RESIZE; +#ifdef DD_VERBOSE + (void) fprintf(unique->err, + "Increasing the table size from %d to %d\n", + unique->maxSize, newsize); +#endif + /* Allocate memory for new arrays (except nodelists). */ + newsubtables = ALLOC(DdSubtable,newsize); + if (newsubtables == NULL) { + unique->errorCode = CUDD_MEMORY_OUT; + return(0); + } + newvars = ALLOC(DdNodePtr,newsize); + if (newvars == NULL) { + unique->errorCode = CUDD_MEMORY_OUT; + FREE(newsubtables); + return(0); + } + newperm = ALLOC(int,newsize); + if (newperm == NULL) { + unique->errorCode = CUDD_MEMORY_OUT; + FREE(newsubtables); + FREE(newvars); + return(0); + } + newinvperm = ALLOC(int,newsize); + if (newinvperm == NULL) { + unique->errorCode = CUDD_MEMORY_OUT; + FREE(newsubtables); + FREE(newvars); + FREE(newperm); + return(0); + } + if (unique->map != NULL) { + newmap = ALLOC(int,newsize); + if (newmap == NULL) { + unique->errorCode = CUDD_MEMORY_OUT; + FREE(newsubtables); + FREE(newvars); + FREE(newperm); + FREE(newinvperm); + return(0); + } + unique->memused += (newsize - unique->maxSize) * sizeof(int); + } + unique->memused += (newsize - unique->maxSize) * ((numSlots+1) * + sizeof(DdNode *) + 2 * sizeof(int) + sizeof(DdSubtable)); + /* Copy levels before insertion points from old tables. */ + for (i = 0; i < level; i++) { + newsubtables[i].slots = unique->subtables[i].slots; + newsubtables[i].shift = unique->subtables[i].shift; + newsubtables[i].keys = unique->subtables[i].keys; + newsubtables[i].maxKeys = unique->subtables[i].maxKeys; + newsubtables[i].dead = unique->subtables[i].dead; + newsubtables[i].nodelist = unique->subtables[i].nodelist; + newsubtables[i].bindVar = unique->subtables[i].bindVar; + newsubtables[i].varType = unique->subtables[i].varType; + newsubtables[i].pairIndex = unique->subtables[i].pairIndex; + newsubtables[i].varHandled = unique->subtables[i].varHandled; + newsubtables[i].varToBeGrouped = unique->subtables[i].varToBeGrouped; + + newvars[i] = unique->vars[i]; + newperm[i] = unique->perm[i]; + newinvperm[i] = unique->invperm[i]; + } + /* Finish initializing permutation for new table to old one. */ + for (i = level; i < oldsize; i++) { + newperm[i] = unique->perm[i]; + } + /* Initialize new levels. */ + for (i = level; i < level + n; i++) { + newsubtables[i].slots = numSlots; + newsubtables[i].shift = sizeof(int) * 8 - + cuddComputeFloorLog2(numSlots); + newsubtables[i].keys = 0; + newsubtables[i].maxKeys = numSlots * DD_MAX_SUBTABLE_DENSITY; + newsubtables[i].dead = 0; + newsubtables[i].bindVar = 0; + newsubtables[i].varType = CUDD_VAR_PRIMARY_INPUT; + newsubtables[i].pairIndex = 0; + newsubtables[i].varHandled = 0; + newsubtables[i].varToBeGrouped = CUDD_LAZY_NONE; + + newperm[oldsize + i - level] = i; + newinvperm[i] = oldsize + i - level; + newnodelist = newsubtables[i].nodelist = ALLOC(DdNodePtr, numSlots); + if (newnodelist == NULL) { + /* We are going to leak some memory. We should clean up. */ + unique->errorCode = CUDD_MEMORY_OUT; + return(0); + } + for (j = 0; j < numSlots; j++) { + newnodelist[j] = sentinel; + } + } + /* Copy the old tables for levels past the insertion point. */ + for (i = level; i < oldsize; i++) { + newsubtables[i+n].slots = unique->subtables[i].slots; + newsubtables[i+n].shift = unique->subtables[i].shift; + newsubtables[i+n].keys = unique->subtables[i].keys; + newsubtables[i+n].maxKeys = unique->subtables[i].maxKeys; + newsubtables[i+n].dead = unique->subtables[i].dead; + newsubtables[i+n].nodelist = unique->subtables[i].nodelist; + newsubtables[i+n].bindVar = unique->subtables[i].bindVar; + newsubtables[i+n].varType = unique->subtables[i].varType; + newsubtables[i+n].pairIndex = unique->subtables[i].pairIndex; + newsubtables[i+n].varHandled = unique->subtables[i].varHandled; + newsubtables[i+n].varToBeGrouped = + unique->subtables[i].varToBeGrouped; + + newvars[i] = unique->vars[i]; + index = unique->invperm[i]; + newinvperm[i+n] = index; + newperm[index] += n; + } + /* Update the map. */ + if (unique->map != NULL) { + for (i = 0; i < oldsize; i++) { + newmap[i] = unique->map[i]; + } + for (i = oldsize; i < oldsize + n; i++) { + newmap[i] = i; + } + FREE(unique->map); + unique->map = newmap; + } + /* Install the new tables and free the old ones. */ + FREE(unique->subtables); + unique->subtables = newsubtables; + unique->maxSize = newsize; + FREE(unique->vars); + unique->vars = newvars; + FREE(unique->perm); + unique->perm = newperm; + FREE(unique->invperm); + unique->invperm = newinvperm; + /* Update the stack for iterative procedures. */ + if (newsize > unique->maxSizeZ) { + FREE(unique->stack); + unique->stack = ALLOC(DdNodePtr,newsize + 1); + if (unique->stack == NULL) { + unique->errorCode = CUDD_MEMORY_OUT; + return(0); + } + unique->stack[0] = NULL; /* to suppress harmless UMR */ + unique->memused += + (newsize - ddMax(unique->maxSize,unique->maxSizeZ)) + * sizeof(DdNode *); + } + } + /* Update manager parameters to account for the new subtables. */ + unique->slots += n * numSlots; + ddFixLimits(unique); + unique->size += n; + + /* Now that the table is in a coherent state, create the new + ** projection functions. We need to temporarily disable reordering, + ** because we cannot reorder without projection functions in place. + **/ + one = unique->one; + zero = Cudd_Not(one); + + reorderSave = unique->autoDyn; + unique->autoDyn = 0; + for (i = oldsize; i < oldsize + n; i++) { + unique->vars[i] = cuddUniqueInter(unique,i,one,zero); + if (unique->vars[i] == NULL) { + unique->autoDyn = reorderSave; + /* Shift everything back so table remains coherent. */ + for (j = oldsize; j < i; j++) { + Cudd_IterDerefBdd(unique,unique->vars[j]); + cuddDeallocNode(unique,unique->vars[j]); + unique->vars[j] = NULL; + } + for (j = level; j < oldsize; j++) { + unique->subtables[j].slots = unique->subtables[j+n].slots; + unique->subtables[j].slots = unique->subtables[j+n].slots; + unique->subtables[j].shift = unique->subtables[j+n].shift; + unique->subtables[j].keys = unique->subtables[j+n].keys; + unique->subtables[j].maxKeys = + unique->subtables[j+n].maxKeys; + unique->subtables[j].dead = unique->subtables[j+n].dead; + FREE(unique->subtables[j].nodelist); + unique->subtables[j].nodelist = + unique->subtables[j+n].nodelist; + unique->subtables[j+n].nodelist = NULL; + unique->subtables[j].bindVar = + unique->subtables[j+n].bindVar; + unique->subtables[j].varType = + unique->subtables[j+n].varType; + unique->subtables[j].pairIndex = + unique->subtables[j+n].pairIndex; + unique->subtables[j].varHandled = + unique->subtables[j+n].varHandled; + unique->subtables[j].varToBeGrouped = + unique->subtables[j+n].varToBeGrouped; + index = unique->invperm[j+n]; + unique->invperm[j] = index; + unique->perm[index] -= n; + } + unique->size = oldsize; + unique->slots -= n * numSlots; + ddFixLimits(unique); + (void) Cudd_DebugCheck(unique); + return(0); + } + cuddRef(unique->vars[i]); + } + if (unique->tree != NULL) { + unique->tree->size += n; + unique->tree->index = unique->invperm[0]; + ddPatchTree(unique,unique->tree); + } + unique->autoDyn = reorderSave; + + return(1); + +} /* end of cuddInsertSubtables */ + + +/**Function******************************************************************** + + Synopsis [Destroys the n most recently created subtables in a unique table.] + + Description [Destroys the n most recently created subtables in a unique + table. n should be positive. The subtables should not contain any live + nodes, except the (isolated) projection function. The projection + functions are freed. Returns 1 if successful; 0 otherwise.] + + SideEffects [The variable map used for fast variable substitution is + destroyed if it exists. In this case the cache is also cleared.] + + SeeAlso [cuddInsertSubtables Cudd_SetVarMap] + +******************************************************************************/ +int +cuddDestroySubtables( + DdManager * unique, + int n) +{ + DdSubtable *subtables; + DdNodePtr *nodelist; + DdNodePtr *vars; + int firstIndex, lastIndex; + int index, level, newlevel; + int lowestLevel; + int shift; + int found; + + /* Sanity check and set up. */ + if (n <= 0) return(0); + if (n > unique->size) n = unique->size; + + subtables = unique->subtables; + vars = unique->vars; + firstIndex = unique->size - n; + lastIndex = unique->size; + + /* Check for nodes labeled by the variables being destroyed + ** that may still be in use. It is allowed to destroy a variable + ** only if there are no such nodes. Also, find the lowest level + ** among the variables being destroyed. This will make further + ** processing more efficient. + */ + lowestLevel = unique->size; + for (index = firstIndex; index < lastIndex; index++) { + level = unique->perm[index]; + if (level < lowestLevel) lowestLevel = level; + nodelist = subtables[level].nodelist; + if (subtables[level].keys - subtables[level].dead != 1) return(0); + /* The projection function should be isolated. If the ref count + ** is 1, everything is OK. If the ref count is saturated, then + ** we need to make sure that there are no nodes pointing to it. + ** As for the external references, we assume the application is + ** responsible for them. + */ + if (vars[index]->ref != 1) { + if (vars[index]->ref != DD_MAXREF) return(0); + found = cuddFindParent(unique,vars[index]); + if (found) { + return(0); + } else { + vars[index]->ref = 1; + } + } + Cudd_RecursiveDeref(unique,vars[index]); + } + + /* Collect garbage, because we cannot afford having dead nodes pointing + ** to the dead nodes in the subtables being destroyed. + */ + (void) cuddGarbageCollect(unique,1); + + /* Here we know we can destroy our subtables. */ + for (index = firstIndex; index < lastIndex; index++) { + level = unique->perm[index]; + nodelist = subtables[level].nodelist; +#ifdef DD_DEBUG + assert(subtables[level].keys == 0); +#endif + FREE(nodelist); + unique->memused -= sizeof(DdNodePtr) * subtables[level].slots; + unique->slots -= subtables[level].slots; + unique->dead -= subtables[level].dead; + } + + /* Here all subtables to be destroyed have their keys field == 0 and + ** their hash tables have been freed. + ** We now scan the subtables from level lowestLevel + 1 to level size - 1, + ** shifting the subtables as required. We keep a running count of + ** how many subtables have been moved, so that we know by how many + ** positions each subtable should be shifted. + */ + shift = 1; + for (level = lowestLevel + 1; level < unique->size; level++) { + if (subtables[level].keys == 0) { + shift++; + continue; + } + newlevel = level - shift; + subtables[newlevel].slots = subtables[level].slots; + subtables[newlevel].shift = subtables[level].shift; + subtables[newlevel].keys = subtables[level].keys; + subtables[newlevel].maxKeys = subtables[level].maxKeys; + subtables[newlevel].dead = subtables[level].dead; + subtables[newlevel].nodelist = subtables[level].nodelist; + index = unique->invperm[level]; + unique->perm[index] = newlevel; + unique->invperm[newlevel] = index; + subtables[newlevel].bindVar = subtables[level].bindVar; + subtables[newlevel].varType = subtables[level].varType; + subtables[newlevel].pairIndex = subtables[level].pairIndex; + subtables[newlevel].varHandled = subtables[level].varHandled; + subtables[newlevel].varToBeGrouped = subtables[level].varToBeGrouped; + } + /* Destroy the map. If a surviving variable is + ** mapped to a dying variable, and the map were used again, + ** an out-of-bounds access to unique->vars would result. */ + if (unique->map != NULL) { + cuddCacheFlush(unique); + FREE(unique->map); + unique->map = NULL; + } + + unique->minDead = (unsigned) (unique->gcFrac * (double) unique->slots); + unique->size -= n; + + return(1); + +} /* end of cuddDestroySubtables */ + + +/**Function******************************************************************** + + Synopsis [Increases the number of ZDD subtables in a unique table so + that it meets or exceeds index.] + + Description [Increases the number of ZDD subtables in a unique table so + that it meets or exceeds index. When new ZDD variables are created, it + is possible to preserve the functions unchanged, or it is possible to + preserve the covers unchanged, but not both. cuddResizeTableZdd preserves + the covers. Returns 1 if successful; 0 otherwise.] + + SideEffects [None] + + SeeAlso [ddResizeTable] + +******************************************************************************/ +int +cuddResizeTableZdd( + DdManager * unique, + int index) +{ + DdSubtable *newsubtables; + DdNodePtr *newnodelist; + int oldsize,newsize; + int i,j,reorderSave; + unsigned int numSlots = unique->initSlots; + int *newperm, *newinvperm; + DdNode *one, *zero; + + oldsize = unique->sizeZ; + /* Easy case: there is still room in the current table. */ + if (index < unique->maxSizeZ) { + for (i = oldsize; i <= index; i++) { + unique->subtableZ[i].slots = numSlots; + unique->subtableZ[i].shift = sizeof(int) * 8 - + cuddComputeFloorLog2(numSlots); + unique->subtableZ[i].keys = 0; + unique->subtableZ[i].maxKeys = numSlots * DD_MAX_SUBTABLE_DENSITY; + unique->subtableZ[i].dead = 0; + unique->permZ[i] = i; + unique->invpermZ[i] = i; + newnodelist = unique->subtableZ[i].nodelist = + ALLOC(DdNodePtr, numSlots); + if (newnodelist == NULL) { + unique->errorCode = CUDD_MEMORY_OUT; + return(0); + } + for (j = 0; j < numSlots; j++) { + newnodelist[j] = NULL; + } + } + } else { + /* The current table is too small: we need to allocate a new, + ** larger one; move all old subtables, and initialize the new + ** subtables up to index included. + */ + newsize = index + DD_DEFAULT_RESIZE; +#ifdef DD_VERBOSE + (void) fprintf(unique->err, + "Increasing the ZDD table size from %d to %d\n", + unique->maxSizeZ, newsize); +#endif + newsubtables = ALLOC(DdSubtable,newsize); + if (newsubtables == NULL) { + unique->errorCode = CUDD_MEMORY_OUT; + return(0); + } + newperm = ALLOC(int,newsize); + if (newperm == NULL) { + unique->errorCode = CUDD_MEMORY_OUT; + return(0); + } + newinvperm = ALLOC(int,newsize); + if (newinvperm == NULL) { + unique->errorCode = CUDD_MEMORY_OUT; + return(0); + } + unique->memused += (newsize - unique->maxSizeZ) * ((numSlots+1) * + sizeof(DdNode *) + 2 * sizeof(int) + sizeof(DdSubtable)); + if (newsize > unique->maxSize) { + FREE(unique->stack); + unique->stack = ALLOC(DdNodePtr,newsize + 1); + if (unique->stack == NULL) { + unique->errorCode = CUDD_MEMORY_OUT; + return(0); + } + unique->stack[0] = NULL; /* to suppress harmless UMR */ + unique->memused += + (newsize - ddMax(unique->maxSize,unique->maxSizeZ)) + * sizeof(DdNode *); + } + for (i = 0; i < oldsize; i++) { + newsubtables[i].slots = unique->subtableZ[i].slots; + newsubtables[i].shift = unique->subtableZ[i].shift; + newsubtables[i].keys = unique->subtableZ[i].keys; + newsubtables[i].maxKeys = unique->subtableZ[i].maxKeys; + newsubtables[i].dead = unique->subtableZ[i].dead; + newsubtables[i].nodelist = unique->subtableZ[i].nodelist; + newperm[i] = unique->permZ[i]; + newinvperm[i] = unique->invpermZ[i]; + } + for (i = oldsize; i <= index; i++) { + newsubtables[i].slots = numSlots; + newsubtables[i].shift = sizeof(int) * 8 - + cuddComputeFloorLog2(numSlots); + newsubtables[i].keys = 0; + newsubtables[i].maxKeys = numSlots * DD_MAX_SUBTABLE_DENSITY; + newsubtables[i].dead = 0; + newperm[i] = i; + newinvperm[i] = i; + newnodelist = newsubtables[i].nodelist = ALLOC(DdNodePtr, numSlots); + if (newnodelist == NULL) { + unique->errorCode = CUDD_MEMORY_OUT; + return(0); + } + for (j = 0; j < numSlots; j++) { + newnodelist[j] = NULL; + } + } + FREE(unique->subtableZ); + unique->subtableZ = newsubtables; + unique->maxSizeZ = newsize; + FREE(unique->permZ); + unique->permZ = newperm; + FREE(unique->invpermZ); + unique->invpermZ = newinvperm; + } + unique->slots += (index + 1 - unique->sizeZ) * numSlots; + ddFixLimits(unique); + unique->sizeZ = index + 1; + + /* Now that the table is in a coherent state, update the ZDD + ** universe. We need to temporarily disable reordering, + ** because we cannot reorder without universe in place. + */ + one = unique->one; + zero = unique->zero; + + reorderSave = unique->autoDynZ; + unique->autoDynZ = 0; + cuddZddFreeUniv(unique); + if (!cuddZddInitUniv(unique)) { + unique->autoDynZ = reorderSave; + return(0); + } + unique->autoDynZ = reorderSave; + + return(1); + +} /* end of cuddResizeTableZdd */ + + +/**Function******************************************************************** + + Synopsis [Adjusts parameters of a table to slow down its growth.] + + Description [] + + SideEffects [None] + + SeeAlso [] + +******************************************************************************/ +void +cuddSlowTableGrowth( + DdManager *unique) +{ + int i; + + unique->maxCacheHard = unique->cacheSlots - 1; + unique->cacheSlack = -(unique->cacheSlots + 1); + for (i = 0; i < unique->size; i++) { + unique->subtables[i].maxKeys <<= 2; + } + unique->gcFrac = DD_GC_FRAC_MIN; + unique->minDead = (unsigned) (DD_GC_FRAC_MIN * (double) unique->slots); + cuddShrinkDeathRow(unique); + (void) fprintf(unique->err,"Slowing down table growth: "); + (void) fprintf(unique->err,"GC fraction = %.2f\t", unique->gcFrac); + (void) fprintf(unique->err,"minDead = %d\n", unique->minDead); + +} /* end of cuddSlowTableGrowth */ + + +/*---------------------------------------------------------------------------*/ +/* Definition of static functions */ +/*---------------------------------------------------------------------------*/ + + +/**Function******************************************************************** + + Synopsis [Rehashes a ZDD unique subtable.] + + Description [] + + SideEffects [None] + + SeeAlso [cuddRehash] + +******************************************************************************/ +static void +ddRehashZdd( + DdManager * unique, + int i) +{ + unsigned int slots, oldslots; + int shift, oldshift; + int j, pos; + DdNodePtr *nodelist, *oldnodelist; + DdNode *node, *next; + extern void (*MMoutOfMemory)(long); + void (*saveHandler)(long); + + if (unique->slots > unique->looseUpTo) { + unique->minDead = (unsigned) (DD_GC_FRAC_LO * (double) unique->slots); +#ifdef DD_VERBOSE + if (unique->gcFrac == DD_GC_FRAC_HI) { + (void) fprintf(unique->err,"GC fraction = %.2f\t", + DD_GC_FRAC_LO); + (void) fprintf(unique->err,"minDead = %d\n", unique->minDead); + } +#endif + unique->gcFrac = DD_GC_FRAC_LO; + } + + assert(i != CUDD_MAXINDEX); + oldslots = unique->subtableZ[i].slots; + oldshift = unique->subtableZ[i].shift; + oldnodelist = unique->subtableZ[i].nodelist; + + /* Compute the new size of the subtable. Normally, we just + ** double. However, after reordering, a table may be severely + ** overloaded. Therefore, we iterate. */ + slots = oldslots; + shift = oldshift; + do { + slots <<= 1; + shift--; + } while (slots * DD_MAX_SUBTABLE_DENSITY < unique->subtableZ[i].keys); + + saveHandler = MMoutOfMemory; + MMoutOfMemory = Cudd_OutOfMem; + nodelist = ALLOC(DdNodePtr, slots); + MMoutOfMemory = saveHandler; + if (nodelist == NULL) { + int j; + (void) fprintf(unique->err, + "Unable to resize ZDD subtable %d for lack of memory.\n", + i); + (void) cuddGarbageCollectZdd(unique,1); + for (j = 0; j < unique->sizeZ; j++) { + unique->subtableZ[j].maxKeys <<= 1; + } + return; + } + unique->subtableZ[i].nodelist = nodelist; + unique->subtableZ[i].slots = slots; + unique->subtableZ[i].shift = shift; + unique->subtableZ[i].maxKeys = slots * DD_MAX_SUBTABLE_DENSITY; + for (j = 0; (unsigned) j < slots; j++) { + nodelist[j] = NULL; + } + for (j = 0; (unsigned) j < oldslots; j++) { + node = oldnodelist[j]; + while (node != NULL) { + next = node->next; + pos = ddHash(cuddT(node), cuddE(node), shift); + node->next = nodelist[pos]; + nodelist[pos] = node; + node = next; + } + } + FREE(oldnodelist); + +#ifdef DD_VERBOSE + (void) fprintf(unique->err, + "rehashing layer %d: keys %d dead %d new size %d\n", + i, unique->subtableZ[i].keys, + unique->subtableZ[i].dead, slots); +#endif + + /* Update global data. */ + unique->memused += (slots - oldslots) * sizeof(DdNode *); + unique->slots += (slots - oldslots); + ddFixLimits(unique); + +} /* end of ddRehashZdd */ + + +/**Function******************************************************************** + + Synopsis [Increases the number of subtables in a unique table so + that it meets or exceeds index.] + + Description [Increases the number of subtables in a unique table so + that it meets or exceeds index. Returns 1 if successful; 0 otherwise.] + + SideEffects [None] + + SeeAlso [cuddResizeTableZdd] + +******************************************************************************/ +static int +ddResizeTable( + DdManager * unique, + int index) +{ + DdSubtable *newsubtables; + DdNodePtr *newnodelist; + DdNodePtr *newvars; + DdNode *sentinel = &(unique->sentinel); + int oldsize,newsize; + int i,j,reorderSave; + int numSlots = unique->initSlots; + int *newperm, *newinvperm, *newmap; + DdNode *one, *zero; + + oldsize = unique->size; + /* Easy case: there is still room in the current table. */ + if (index < unique->maxSize) { + for (i = oldsize; i <= index; i++) { + unique->subtables[i].slots = numSlots; + unique->subtables[i].shift = sizeof(int) * 8 - + cuddComputeFloorLog2(numSlots); + unique->subtables[i].keys = 0; + unique->subtables[i].maxKeys = numSlots * DD_MAX_SUBTABLE_DENSITY; + unique->subtables[i].dead = 0; + unique->subtables[i].bindVar = 0; + unique->subtables[i].varType = CUDD_VAR_PRIMARY_INPUT; + unique->subtables[i].pairIndex = 0; + unique->subtables[i].varHandled = 0; + unique->subtables[i].varToBeGrouped = CUDD_LAZY_NONE; + + unique->perm[i] = i; + unique->invperm[i] = i; + newnodelist = unique->subtables[i].nodelist = + ALLOC(DdNodePtr, numSlots); + if (newnodelist == NULL) { + for (j = oldsize; j < i; j++) { + FREE(unique->subtables[j].nodelist); + } + unique->errorCode = CUDD_MEMORY_OUT; + return(0); + } + for (j = 0; j < numSlots; j++) { + newnodelist[j] = sentinel; + } + } + if (unique->map != NULL) { + for (i = oldsize; i <= index; i++) { + unique->map[i] = i; + } + } + } else { + /* The current table is too small: we need to allocate a new, + ** larger one; move all old subtables, and initialize the new + ** subtables up to index included. + */ + newsize = index + DD_DEFAULT_RESIZE; +#ifdef DD_VERBOSE + (void) fprintf(unique->err, + "Increasing the table size from %d to %d\n", + unique->maxSize, newsize); +#endif + newsubtables = ALLOC(DdSubtable,newsize); + if (newsubtables == NULL) { + unique->errorCode = CUDD_MEMORY_OUT; + return(0); + } + newvars = ALLOC(DdNodePtr,newsize); + if (newvars == NULL) { + FREE(newsubtables); + unique->errorCode = CUDD_MEMORY_OUT; + return(0); + } + newperm = ALLOC(int,newsize); + if (newperm == NULL) { + FREE(newsubtables); + FREE(newvars); + unique->errorCode = CUDD_MEMORY_OUT; + return(0); + } + newinvperm = ALLOC(int,newsize); + if (newinvperm == NULL) { + FREE(newsubtables); + FREE(newvars); + FREE(newperm); + unique->errorCode = CUDD_MEMORY_OUT; + return(0); + } + if (unique->map != NULL) { + newmap = ALLOC(int,newsize); + if (newmap == NULL) { + FREE(newsubtables); + FREE(newvars); + FREE(newperm); + FREE(newinvperm); + unique->errorCode = CUDD_MEMORY_OUT; + return(0); + } + unique->memused += (newsize - unique->maxSize) * sizeof(int); + } + unique->memused += (newsize - unique->maxSize) * ((numSlots+1) * + sizeof(DdNode *) + 2 * sizeof(int) + sizeof(DdSubtable)); + if (newsize > unique->maxSizeZ) { + FREE(unique->stack); + unique->stack = ALLOC(DdNodePtr,newsize + 1); + if (unique->stack == NULL) { + FREE(newsubtables); + FREE(newvars); + FREE(newperm); + FREE(newinvperm); + if (unique->map != NULL) { + FREE(newmap); + } + unique->errorCode = CUDD_MEMORY_OUT; + return(0); + } + unique->stack[0] = NULL; /* to suppress harmless UMR */ + unique->memused += + (newsize - ddMax(unique->maxSize,unique->maxSizeZ)) + * sizeof(DdNode *); + } + for (i = 0; i < oldsize; i++) { + newsubtables[i].slots = unique->subtables[i].slots; + newsubtables[i].shift = unique->subtables[i].shift; + newsubtables[i].keys = unique->subtables[i].keys; + newsubtables[i].maxKeys = unique->subtables[i].maxKeys; + newsubtables[i].dead = unique->subtables[i].dead; + newsubtables[i].nodelist = unique->subtables[i].nodelist; + newsubtables[i].bindVar = unique->subtables[i].bindVar; + newsubtables[i].varType = unique->subtables[i].varType; + newsubtables[i].pairIndex = unique->subtables[i].pairIndex; + newsubtables[i].varHandled = unique->subtables[i].varHandled; + newsubtables[i].varToBeGrouped = unique->subtables[i].varToBeGrouped; + + newvars[i] = unique->vars[i]; + newperm[i] = unique->perm[i]; + newinvperm[i] = unique->invperm[i]; + } + for (i = oldsize; i <= index; i++) { + newsubtables[i].slots = numSlots; + newsubtables[i].shift = sizeof(int) * 8 - + cuddComputeFloorLog2(numSlots); + newsubtables[i].keys = 0; + newsubtables[i].maxKeys = numSlots * DD_MAX_SUBTABLE_DENSITY; + newsubtables[i].dead = 0; + newsubtables[i].bindVar = 0; + newsubtables[i].varType = CUDD_VAR_PRIMARY_INPUT; + newsubtables[i].pairIndex = 0; + newsubtables[i].varHandled = 0; + newsubtables[i].varToBeGrouped = CUDD_LAZY_NONE; + + newperm[i] = i; + newinvperm[i] = i; + newnodelist = newsubtables[i].nodelist = ALLOC(DdNodePtr, numSlots); + if (newnodelist == NULL) { + unique->errorCode = CUDD_MEMORY_OUT; + return(0); + } + for (j = 0; j < numSlots; j++) { + newnodelist[j] = sentinel; + } + } + if (unique->map != NULL) { + for (i = 0; i < oldsize; i++) { + newmap[i] = unique->map[i]; + } + for (i = oldsize; i <= index; i++) { + newmap[i] = i; + } + FREE(unique->map); + unique->map = newmap; + } + FREE(unique->subtables); + unique->subtables = newsubtables; + unique->maxSize = newsize; + FREE(unique->vars); + unique->vars = newvars; + FREE(unique->perm); + unique->perm = newperm; + FREE(unique->invperm); + unique->invperm = newinvperm; + } + + /* Now that the table is in a coherent state, create the new + ** projection functions. We need to temporarily disable reordering, + ** because we cannot reorder without projection functions in place. + **/ + one = unique->one; + zero = Cudd_Not(one); + + unique->size = index + 1; + unique->slots += (index + 1 - oldsize) * numSlots; + ddFixLimits(unique); + + reorderSave = unique->autoDyn; + unique->autoDyn = 0; + for (i = oldsize; i <= index; i++) { + unique->vars[i] = cuddUniqueInter(unique,i,one,zero); + if (unique->vars[i] == NULL) { + unique->autoDyn = reorderSave; + for (j = oldsize; j < i; j++) { + Cudd_IterDerefBdd(unique,unique->vars[j]); + cuddDeallocNode(unique,unique->vars[j]); + unique->vars[j] = NULL; + } + for (j = oldsize; j <= index; j++) { + FREE(unique->subtables[j].nodelist); + unique->subtables[j].nodelist = NULL; + } + unique->size = oldsize; + unique->slots -= (index + 1 - oldsize) * numSlots; + ddFixLimits(unique); + return(0); + } + cuddRef(unique->vars[i]); + } + unique->autoDyn = reorderSave; + + return(1); + +} /* end of ddResizeTable */ + + +/**Function******************************************************************** + + Synopsis [Searches the subtables above node for a parent.] + + Description [Searches the subtables above node for a parent. Returns 1 + as soon as one parent is found. Returns 0 is the search is fruitless.] + + SideEffects [None] + + SeeAlso [] + +******************************************************************************/ +static int +cuddFindParent( + DdManager * table, + DdNode * node) +{ + int i,j; + int slots; + DdNodePtr *nodelist; + DdNode *f; + + for (i = cuddI(table,node->index) - 1; i >= 0; i--) { + nodelist = table->subtables[i].nodelist; + slots = table->subtables[i].slots; + + for (j = 0; j < slots; j++) { + f = nodelist[j]; + while (cuddT(f) > node) { + f = f->next; + } + while (cuddT(f) == node && Cudd_Regular(cuddE(f)) > node) { + f = f->next; + } + if (cuddT(f) == node && Cudd_Regular(cuddE(f)) == node) { + return(1); + } + } + } + + return(0); + +} /* end of cuddFindParent */ + + +/**Function******************************************************************** + + Synopsis [Adjusts the values of table limits.] + + Description [Adjusts the values of table fields controlling the. + sizes of subtables and computed table. If the computed table is too small + according to the new values, it is resized.] + + SideEffects [Modifies manager fields. May resize computed table.] + + SeeAlso [] + +******************************************************************************/ +DD_INLINE +static void +ddFixLimits( + DdManager *unique) +{ + unique->minDead = (unsigned) (unique->gcFrac * (double) unique->slots); + unique->cacheSlack = (int) ddMin(unique->maxCacheHard, + DD_MAX_CACHE_TO_SLOTS_RATIO * unique->slots) - + 2 * (int) unique->cacheSlots; + if (unique->cacheSlots < unique->slots/2 && unique->cacheSlack >= 0) + cuddCacheResize(unique); + return; + +} /* end of ddFixLimits */ + + +#ifndef DD_UNSORTED_FREE_LIST +/**Function******************************************************************** + + Synopsis [Inserts a DdNode in a red/black search tree.] + + Description [Inserts a DdNode in a red/black search tree. Nodes from + the same "page" (defined by DD_PAGE_MASK) are linked in a LIFO list.] + + SideEffects [None] + + SeeAlso [cuddOrderedThread] + +******************************************************************************/ +static void +cuddOrderedInsert( + DdNodePtr * root, + DdNodePtr node) +{ + DdNode *scan; + DdNodePtr *scanP; + DdNodePtr *stack[DD_STACK_SIZE]; + int stackN = 0; + + scanP = root; + while ((scan = *scanP) != NULL) { + stack[stackN++] = scanP; + if (DD_INSERT_COMPARE(node, scan) == 0) { /* add to page list */ + DD_NEXT(node) = DD_NEXT(scan); + DD_NEXT(scan) = node; + return; + } + scanP = (node < scan) ? &DD_LEFT(scan) : &DD_RIGHT(scan); + } + DD_RIGHT(node) = DD_LEFT(node) = DD_NEXT(node) = NULL; + DD_COLOR(node) = DD_RED; + *scanP = node; + stack[stackN] = &node; + cuddDoRebalance(stack,stackN); + +} /* end of cuddOrderedInsert */ + + +/**Function******************************************************************** + + Synopsis [Threads all the nodes of a search tree into a linear list.] + + Description [Threads all the nodes of a search tree into a linear + list. For each node of the search tree, the "left" child, if non-null, has + a lower address than its parent, and the "right" child, if non-null, has a + higher address than its parent. + The list is sorted in order of increasing addresses. The search + tree is destroyed as a result of this operation. The last element of + the linear list is made to point to the address passed in list. Each + node if the search tree is a linearly-linked list of nodes from the + same memory page (as defined in DD_PAGE_MASK). When a node is added to + the linear list, all the elements of the linked list are added.] + + SideEffects [The search tree is destroyed as a result of this operation.] + + SeeAlso [cuddOrderedInsert] + +******************************************************************************/ +static DdNode * +cuddOrderedThread( + DdNode * root, + DdNode * list) +{ + DdNode *current, *next, *prev, *end; + + current = root; + /* The first word in the node is used to implement a stack that holds + ** the nodes from the root of the tree to the current node. Here we + ** put the root of the tree at the bottom of the stack. + */ + *((DdNodePtr *) current) = NULL; + + while (current != NULL) { + if (DD_RIGHT(current) != NULL) { + /* If possible, we follow the "right" link. Eventually we'll + ** find the node with the largest address in the current tree. + ** In this phase we use the first word of a node to implemen + ** a stack of the nodes on the path from the root to "current". + ** Also, we disconnect the "right" pointers to indicate that + ** we have already followed them. + */ + next = DD_RIGHT(current); + DD_RIGHT(current) = NULL; + *((DdNodePtr *)next) = current; + current = next; + } else { + /* We can't proceed along the "right" links any further. + ** Hence "current" is the largest element in the current tree. + ** We make this node the new head of "list". (Repeating this + ** operation until the tree is empty yields the desired linear + ** threading of all nodes.) + */ + prev = *((DdNodePtr *) current); /* save prev node on stack in prev */ + /* Traverse the linked list of current until the end. */ + for (end = current; DD_NEXT(end) != NULL; end = DD_NEXT(end)); + DD_NEXT(end) = list; /* attach "list" at end and make */ + list = current; /* "current" the new head of "list" */ + /* Now, if current has a "left" child, we push it on the stack. + ** Otherwise, we just continue with the parent of "current". + */ + if (DD_LEFT(current) != NULL) { + next = DD_LEFT(current); + *((DdNodePtr *) next) = prev; + current = next; + } else { + current = prev; + } + } + } + + return(list); + +} /* end of cuddOrderedThread */ + + +/**Function******************************************************************** + + Synopsis [Performs the left rotation for red/black trees.] + + Description [] + + SideEffects [None] + + SeeAlso [cuddRotateRight] + +******************************************************************************/ +DD_INLINE +static void +cuddRotateLeft( + DdNodePtr * nodeP) +{ + DdNode *newRoot; + DdNode *oldRoot = *nodeP; + + *nodeP = newRoot = DD_RIGHT(oldRoot); + DD_RIGHT(oldRoot) = DD_LEFT(newRoot); + DD_LEFT(newRoot) = oldRoot; + +} /* end of cuddRotateLeft */ + + +/**Function******************************************************************** + + Synopsis [Performs the right rotation for red/black trees.] + + Description [] + + SideEffects [None] + + SeeAlso [cuddRotateLeft] + +******************************************************************************/ +DD_INLINE +static void +cuddRotateRight( + DdNodePtr * nodeP) +{ + DdNode *newRoot; + DdNode *oldRoot = *nodeP; + + *nodeP = newRoot = DD_LEFT(oldRoot); + DD_LEFT(oldRoot) = DD_RIGHT(newRoot); + DD_RIGHT(newRoot) = oldRoot; + +} /* end of cuddRotateRight */ + + +/**Function******************************************************************** + + Synopsis [Rebalances a red/black tree.] + + Description [] + + SideEffects [None] + + SeeAlso [] + +******************************************************************************/ +static void +cuddDoRebalance( + DdNodePtr ** stack, + int stackN) +{ + DdNodePtr *xP, *parentP, *grandpaP; + DdNode *x, *y, *parent, *grandpa; + + xP = stack[stackN]; + x = *xP; + /* Work our way back up, re-balancing the tree. */ + while (--stackN >= 0) { + parentP = stack[stackN]; + parent = *parentP; + if (DD_IS_BLACK(parent)) break; + /* Since the root is black, here a non-null grandparent exists. */ + grandpaP = stack[stackN-1]; + grandpa = *grandpaP; + if (parent == DD_LEFT(grandpa)) { + y = DD_RIGHT(grandpa); + if (y != NULL && DD_IS_RED(y)) { + DD_COLOR(parent) = DD_BLACK; + DD_COLOR(y) = DD_BLACK; + DD_COLOR(grandpa) = DD_RED; + x = grandpa; + stackN--; + } else { + if (x == DD_RIGHT(parent)) { + cuddRotateLeft(parentP); + DD_COLOR(x) = DD_BLACK; + } else { + DD_COLOR(parent) = DD_BLACK; + } + DD_COLOR(grandpa) = DD_RED; + cuddRotateRight(grandpaP); + break; + } + } else { + y = DD_LEFT(grandpa); + if (y != NULL && DD_IS_RED(y)) { + DD_COLOR(parent) = DD_BLACK; + DD_COLOR(y) = DD_BLACK; + DD_COLOR(grandpa) = DD_RED; + x = grandpa; + stackN--; + } else { + if (x == DD_LEFT(parent)) { + cuddRotateRight(parentP); + DD_COLOR(x) = DD_BLACK; + } else { + DD_COLOR(parent) = DD_BLACK; + } + DD_COLOR(grandpa) = DD_RED; + cuddRotateLeft(grandpaP); + } + } + } + DD_COLOR(*(stack[0])) = DD_BLACK; + +} /* end of cuddDoRebalance */ +#endif + + +/**Function******************************************************************** + + Synopsis [Fixes a variable tree after the insertion of new subtables.] + + Description [Fixes a variable tree after the insertion of new subtables. + After such an insertion, the low fields of the tree below the insertion + point are inconsistent.] + + SideEffects [None] + + SeeAlso [] + +******************************************************************************/ +static void +ddPatchTree( + DdManager *dd, + MtrNode *treenode) +{ + MtrNode *auxnode = treenode; + + while (auxnode != NULL) { + auxnode->low = dd->perm[auxnode->index]; + if (auxnode->child != NULL) { + ddPatchTree(dd, auxnode->child); + } + auxnode = auxnode->younger; + } + + return; + +} /* end of ddPatchTree */ + + +#ifdef DD_DEBUG +/**Function******************************************************************** + + Synopsis [Checks whether a collision list is ordered.] + + Description [] + + SideEffects [None] + + SeeAlso [] + +******************************************************************************/ +static int +cuddCheckCollisionOrdering( + DdManager *unique, + int i, + int j) +{ + int slots; + DdNode *node, *next; + DdNodePtr *nodelist; + DdNode *sentinel = &(unique->sentinel); + + nodelist = unique->subtables[i].nodelist; + slots = unique->subtables[i].slots; + node = nodelist[j]; + if (node == sentinel) return(1); + next = node->next; + while (next != sentinel) { + if (cuddT(node) < cuddT(next) || + (cuddT(node) == cuddT(next) && cuddE(node) < cuddE(next))) { + (void) fprintf(unique->err, + "Unordered list: index %u, position %d\n", i, j); + return(0); + } + node = next; + next = node->next; + } + return(1); + +} /* end of cuddCheckCollisionOrdering */ +#endif + + + + +/**Function******************************************************************** + + Synopsis [Reports problem in garbage collection.] + + Description [] + + SideEffects [None] + + SeeAlso [cuddGarbageCollect cuddGarbageCollectZdd] + +******************************************************************************/ +static void +ddReportRefMess( + DdManager *unique /* manager */, + int i /* table in which the problem occurred */, + char *caller /* procedure that detected the problem */) +{ + if (i == CUDD_CONST_INDEX) { + (void) fprintf(unique->err, + "%s: problem in constants\n", caller); + } else if (i != -1) { + (void) fprintf(unique->err, + "%s: problem in table %d\n", caller, i); + } + (void) fprintf(unique->err, " dead count != deleted\n"); + (void) fprintf(unique->err, " This problem is often due to a missing \ +call to Cudd_Ref\n or to an extra call to Cudd_RecursiveDeref.\n \ +See the CUDD Programmer's Guide for additional details."); + abort(); + +} /* end of ddReportRefMess */ |