diff options
Diffstat (limited to 'src/bdd/cudd/cuddTable.c')
| -rw-r--r-- | src/bdd/cudd/cuddTable.c | 2890 |
1 files changed, 1455 insertions, 1435 deletions
diff --git a/src/bdd/cudd/cuddTable.c b/src/bdd/cudd/cuddTable.c index 6ec6f6e7..040e4670 100644 --- a/src/bdd/cudd/cuddTable.c +++ b/src/bdd/cudd/cuddTable.c @@ -7,72 +7,99 @@ 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>] + <ul> + <li> Cudd_Prime() + </ul> + Internal procedures included in this module: + <ul> + <li> cuddAllocNode() + <li> cuddInitTable() + <li> cuddFreeTable() + <li> cuddGarbageCollect() + <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.] + Copyright [Copyright (c) 1995-2004, Regents of the University of Colorado + + All rights reserved. + + Redistribution and use in source and binary forms, with or without + modification, are permitted provided that the following conditions + are met: + + Redistributions of source code must retain the above copyright + notice, this list of conditions and the following disclaimer. + + Redistributions in binary form must reproduce the above copyright + notice, this list of conditions and the following disclaimer in the + documentation and/or other materials provided with the distribution. + + Neither the name of the University of Colorado nor the names of its + contributors may be used to endorse or promote products derived from + this software without specific prior written permission. + + THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS + "AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT + LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS + FOR A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE + COPYRIGHT OWNER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, + INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, + BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; + LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER + CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT + LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN + ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE + POSSIBILITY OF SUCH DAMAGE.] ******************************************************************************/ -#include "util_hack.h" -#include "cuddInt.h" +#include "util_hack.h" +#include "cuddInt.h" ABC_NAMESPACE_IMPL_START + /*---------------------------------------------------------------------------*/ /* Constant declarations */ /*---------------------------------------------------------------------------*/ #ifndef DD_UNSORTED_FREE_LIST +#ifdef DD_RED_BLACK_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 #endif /*---------------------------------------------------------------------------*/ @@ -94,7 +121,7 @@ typedef union hack { /*---------------------------------------------------------------------------*/ #ifndef lint -static char rcsid[] DD_UNUSED = "$Id: cuddTable.c,v 1.1.1.1 2003/02/24 22:23:53 wjiang Exp $"; +static char rcsid[] DD_UNUSED = "$Id: cuddTable.c,v 1.122 2009/02/19 16:24:28 fabio Exp $"; #endif /*---------------------------------------------------------------------------*/ @@ -103,7 +130,10 @@ static char rcsid[] DD_UNUSED = "$Id: cuddTable.c,v 1.1.1.1 2003/02/24 22:23:53 #ifndef DD_UNSORTED_FREE_LIST +#ifdef DD_RED_BLACK_FREE_LIST /* Macros for red/black trees. */ +#define DD_INSERT_COMPARE(x,y) \ + (((ptruint) (x) & DD_PAGE_MASK) - ((ptruint) (y) & DD_PAGE_MASK)) #define DD_COLOR(p) ((p)->index) #define DD_IS_BLACK(p) ((p)->index == DD_BLACK) #define DD_IS_RED(p) ((p)->index == DD_RED) @@ -111,6 +141,7 @@ static char rcsid[] DD_UNUSED = "$Id: cuddTable.c,v 1.1.1.1 2003/02/24 22:23:53 #define DD_RIGHT(p) cuddE(p) #define DD_NEXT(p) ((p)->next) #endif +#endif /**AutomaticStart*************************************************************/ @@ -119,20 +150,22 @@ static char rcsid[] DD_UNUSED = "$Id: cuddTable.c,v 1.1.1.1 2003/02/24 22:23:53 /* 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)); +static void ddRehashZdd (DdManager *unique, int i); +static int ddResizeTable (DdManager *unique, int index); +static int cuddFindParent (DdManager *table, DdNode *node); +DD_INLINE static void ddFixLimits (DdManager *unique); +#ifdef DD_RED_BLACK_FREE_LIST +static void cuddOrderedInsert (DdNodePtr *root, DdNodePtr node); +static DdNode * cuddOrderedThread (DdNode *root, DdNode *list); +static void cuddRotateLeft (DdNodePtr *nodeP); +static void cuddRotateRight (DdNodePtr *nodeP); +static void cuddDoRebalance (DdNodePtr **stack, int stackN); +#endif +static void ddPatchTree (DdManager *dd, MtrNode *treenode); #ifdef DD_DEBUG -static int cuddCheckCollisionOrdering ARGS((DdManager *unique, int i, int j)); +static int cuddCheckCollisionOrdering (DdManager *unique, int i, int j); #endif -static void ddReportRefMess ARGS((DdManager *unique, int i, char *caller)); +static void ddReportRefMess (DdManager *unique, int i, const char *caller); /**AutomaticEnd***************************************************************/ @@ -161,18 +194,18 @@ Cudd_Prime( do { p++; if (p&1) { - pn = 1; - i = 3; - while ((unsigned) (i * i) <= p) { - if (p % i == 0) { + pn = 1; + i = 3; + while ((unsigned) (i * i) <= p) { + if (p % i == 0) { + pn = 0; + break; + } + i += 2; + } + } else { pn = 0; - break; - } - i += 2; } - } else { - pn = 0; - } } while (!pn); return(p); @@ -205,87 +238,89 @@ cuddAllocNode( 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); + extern DD_OOMFP MMoutOfMemory; + DD_OOMFP saveHandler; + + 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); } - /* Try to allocate a new block. */ - saveHandler = MMoutOfMemory; - MMoutOfMemory = Cudd_OutOfMem; - mem = (DdNodePtr *) ABC_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) { - ABC_FREE(unique->stash); - unique->stash = NULL; - /* Inhibit resizing of tables. */ - cuddSlowTableGrowth(unique); - /* Now try again. */ - mem = (DdNodePtr *) ABC_ALLOC(DdNode,DD_MEM_CHUNK + 1); + 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 *) ABC_ALLOC(DdNode,DD_MEM_CHUNK + 1); + MMoutOfMemory = saveHandler; 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; + /* 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) { + ABC_FREE(unique->stash); + unique->stash = NULL; + /* Inhibit resizing of tables. */ + cuddSlowTableGrowth(unique); + /* Now try again. */ + mem = (DdNodePtr *) ABC_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); + (void) fprintf(unique->err, + "cuddAllocNode: out of memory"); + (void) fprintf(unique->err, "Memory in use = %lu\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].ref = 0; + list[i - 1].next = &list[i]; + } while (++i < DD_MEM_CHUNK); + + list[DD_MEM_CHUNK-1].ref = 0; + list[DD_MEM_CHUNK-1].next = NULL; + + unique->nextFree = &list[0]; } - } - } - 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; @@ -313,15 +348,15 @@ cuddInitTable( unsigned int numSlots /* Initial size of the BDD subtables */, unsigned int looseUpTo /* Limit for fast table growth */) { - DdManager *unique = ABC_ALLOC(DdManager,1); - int i, j; - DdNodePtr *nodelist; - DdNode *sentinel; + DdManager *unique = ABC_ALLOC(DdManager,1); + int i, j; + DdNodePtr *nodelist; + DdNode *sentinel; unsigned int slots; int shift; if (unique == NULL) { - return(NULL); + return(NULL); } sentinel = &(unique->sentinel); sentinel->ref = 0; @@ -332,7 +367,7 @@ cuddInitTable( 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->reordCycle = 0; /* do not use alternate threshold */ unique->size = numVars; unique->sizeZ = numVarsZ; unique->maxSize = ddMax(DD_DEFAULT_RESIZE, numVars); @@ -341,14 +376,14 @@ cuddInitTable( /* Adjust the requested number of slots to a power of 2. */ slots = 8; while (slots < numSlots) { - slots <<= 1; + 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->maxLive = ~0; /* very large number */ unique->keysZ = 0; unique->dead = 0; unique->deadZ = 0; @@ -360,39 +395,60 @@ cuddInitTable( unique->reclaimed = 0; unique->subtables = ABC_ALLOC(DdSubtable,unique->maxSize); if (unique->subtables == NULL) { - unique->errorCode = CUDD_MEMORY_OUT; - return(0); + ABC_FREE(unique); + return(NULL); } unique->subtableZ = ABC_ALLOC(DdSubtable,unique->maxSizeZ); if (unique->subtableZ == NULL) { - unique->errorCode = CUDD_MEMORY_OUT; - return(0); + ABC_FREE(unique->subtables); + ABC_FREE(unique); + return(NULL); } unique->perm = ABC_ALLOC(int,unique->maxSize); if (unique->perm == NULL) { - unique->errorCode = CUDD_MEMORY_OUT; - return(0); + ABC_FREE(unique->subtables); + ABC_FREE(unique->subtableZ); + ABC_FREE(unique); + return(NULL); } unique->invperm = ABC_ALLOC(int,unique->maxSize); if (unique->invperm == NULL) { - unique->errorCode = CUDD_MEMORY_OUT; - return(0); + ABC_FREE(unique->subtables); + ABC_FREE(unique->subtableZ); + ABC_FREE(unique->perm); + ABC_FREE(unique); + return(NULL); } unique->permZ = ABC_ALLOC(int,unique->maxSizeZ); if (unique->permZ == NULL) { - unique->errorCode = CUDD_MEMORY_OUT; - return(0); + ABC_FREE(unique->subtables); + ABC_FREE(unique->subtableZ); + ABC_FREE(unique->perm); + ABC_FREE(unique->invperm); + ABC_FREE(unique); + return(NULL); } unique->invpermZ = ABC_ALLOC(int,unique->maxSizeZ); if (unique->invpermZ == NULL) { - unique->errorCode = CUDD_MEMORY_OUT; - return(0); + ABC_FREE(unique->subtables); + ABC_FREE(unique->subtableZ); + ABC_FREE(unique->perm); + ABC_FREE(unique->invperm); + ABC_FREE(unique->permZ); + ABC_FREE(unique); + return(NULL); } unique->map = NULL; unique->stack = ABC_ALLOC(DdNodePtr,ddMax(unique->maxSize,unique->maxSizeZ)+1); if (unique->stack == NULL) { - unique->errorCode = CUDD_MEMORY_OUT; - return(0); + ABC_FREE(unique->subtables); + ABC_FREE(unique->subtableZ); + ABC_FREE(unique->perm); + ABC_FREE(unique->invperm); + ABC_FREE(unique->permZ); + ABC_FREE(unique->invpermZ); + ABC_FREE(unique); + return(NULL); } unique->stack[0] = NULL; /* to suppress harmless UMR */ @@ -400,55 +456,85 @@ cuddInitTable( unique->deathRowDepth = 1 << cuddComputeFloorLog2(unique->looseUpTo >> 2); unique->deathRow = ABC_ALLOC(DdNodePtr,unique->deathRowDepth); if (unique->deathRow == NULL) { - unique->errorCode = CUDD_MEMORY_OUT; - return(0); + ABC_FREE(unique->subtables); + ABC_FREE(unique->subtableZ); + ABC_FREE(unique->perm); + ABC_FREE(unique->invperm); + ABC_FREE(unique->permZ); + ABC_FREE(unique->invpermZ); + ABC_FREE(unique->stack); + ABC_FREE(unique); + return(NULL); } for (i = 0; i < unique->deathRowDepth; i++) { - unique->deathRow[i] = NULL; + 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; + 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 = ABC_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; + nodelist = unique->subtables[i].nodelist = ABC_ALLOC(DdNodePtr,slots); + if (nodelist == NULL) { + for (j = 0; j < i; j++) { + ABC_FREE(unique->subtables[j].nodelist); + } + ABC_FREE(unique->subtables); + ABC_FREE(unique->subtableZ); + ABC_FREE(unique->perm); + ABC_FREE(unique->invperm); + ABC_FREE(unique->permZ); + ABC_FREE(unique->invpermZ); + ABC_FREE(unique->stack); + ABC_FREE(unique); + 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 = ABC_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->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 = ABC_ALLOC(DdNodePtr,slots); + if (nodelist == NULL) { + for (j = 0; (unsigned) j < numVars; j++) { + ABC_FREE(unique->subtables[j].nodelist); + } + ABC_FREE(unique->subtables); + for (j = 0; j < i; j++) { + ABC_FREE(unique->subtableZ[j].nodelist); + } + ABC_FREE(unique->subtableZ); + ABC_FREE(unique->perm); + ABC_FREE(unique->invperm); + ABC_FREE(unique->permZ); + ABC_FREE(unique->invpermZ); + ABC_FREE(unique->stack); + ABC_FREE(unique); + 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; @@ -457,30 +543,43 @@ cuddInitTable( unique->constants.maxKeys = slots * DD_MAX_SUBTABLE_DENSITY; nodelist = unique->constants.nodelist = ABC_ALLOC(DdNodePtr,slots); if (nodelist == NULL) { - unique->errorCode = CUDD_MEMORY_OUT; - return(NULL); + for (j = 0; (unsigned) j < numVars; j++) { + ABC_FREE(unique->subtables[j].nodelist); + } + ABC_FREE(unique->subtables); + for (j = 0; (unsigned) j < numVarsZ; j++) { + ABC_FREE(unique->subtableZ[j].nodelist); + } + ABC_FREE(unique->subtableZ); + ABC_FREE(unique->perm); + ABC_FREE(unique->invperm); + ABC_FREE(unique->permZ); + ABC_FREE(unique->invpermZ); + ABC_FREE(unique->stack); + ABC_FREE(unique); + return(NULL); } for (j = 0; (unsigned) j < slots; j++) { - nodelist[j] = NULL; + 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); + * (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->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; @@ -513,7 +612,7 @@ cuddInitTable( unique->errorCode = CUDD_NO_ERROR; /* Initialize statistical counters. */ - unique->maxmemhard = (long) ((~ (unsigned long) 0) >> 1); + unique->maxmemhard = ~ 0UL; unique->garbageCollections = 0; unique->GCTime = 0; unique->reordTime = 0; @@ -560,18 +659,18 @@ cuddFreeTable( if (unique->univ != NULL) cuddZddFreeUniv(unique); while (memlist != NULL) { - next = (DdNodePtr *) memlist[0]; /* link to next block */ - ABC_FREE(memlist); - memlist = next; + next = (DdNodePtr *) memlist[0]; /* link to next block */ + ABC_FREE(memlist); + memlist = next; } unique->nextFree = NULL; unique->memoryList = NULL; for (i = 0; i < unique->size; i++) { - ABC_FREE(unique->subtables[i].nodelist); + ABC_FREE(unique->subtables[i].nodelist); } for (i = 0; i < unique->sizeZ; i++) { - ABC_FREE(unique->subtableZ[i].nodelist); + ABC_FREE(unique->subtableZ[i].nodelist); } ABC_FREE(unique->constants.nodelist); ABC_FREE(unique->subtables); @@ -591,15 +690,15 @@ cuddFreeTable( if (unique->treeZ != NULL) Mtr_FreeTree(unique->treeZ); if (unique->linear != NULL) ABC_FREE(unique->linear); while (unique->preGCHook != NULL) - Cudd_RemoveHook(unique,unique->preGCHook->f,CUDD_PRE_GC_HOOK); + Cudd_RemoveHook(unique,unique->preGCHook->f,CUDD_PRE_GC_HOOK); while (unique->postGCHook != NULL) - Cudd_RemoveHook(unique,unique->postGCHook->f,CUDD_POST_GC_HOOK); + Cudd_RemoveHook(unique,unique->postGCHook->f,CUDD_POST_GC_HOOK); while (unique->preReorderingHook != NULL) - Cudd_RemoveHook(unique,unique->preReorderingHook->f, - CUDD_PRE_REORDERING_HOOK); + Cudd_RemoveHook(unique,unique->preReorderingHook->f, + CUDD_PRE_REORDERING_HOOK); while (unique->postReorderingHook != NULL) - Cudd_RemoveHook(unique,unique->postReorderingHook->f, - CUDD_POST_REORDERING_HOOK); + Cudd_RemoveHook(unique,unique->postReorderingHook->f, + CUDD_POST_REORDERING_HOOK); ABC_FREE(unique); } /* end of cuddFreeTable */ @@ -607,9 +706,9 @@ cuddFreeTable( /**Function******************************************************************** - Synopsis [Performs garbage collection on a unique table.] + Synopsis [Performs garbage collection on the unique tables.] - Description [Performs garbage collection on a unique table. + Description [Performs garbage collection on the BDD and ZDD unique tables. 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.) @@ -617,7 +716,7 @@ cuddFreeTable( SideEffects [None] - SeeAlso [cuddGarbageCollectZdd] + SeeAlso [] ******************************************************************************/ int @@ -625,18 +724,24 @@ 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; + DdHook *hook; + DdCache *cache = unique->cache; + DdNode *sentinel = &(unique->sentinel); + DdNodePtr *nodelist; + int i, j, deleted, totalDeleted, totalDeletedZ; + DdCache *c; + DdNode *node,*next; + DdNodePtr *lastP; + int slots; + long localTime; #ifndef DD_UNSORTED_FREE_LIST - DdNodePtr tree; +#ifdef DD_RED_BLACK_FREE_LIST + DdNodePtr tree; +#else + DdNodePtr *memListTrav, *nxtNode; + DdNode *downTrav, *sentry; + int k; +#endif #endif #ifndef DD_NO_DEATH_ROW @@ -645,18 +750,18 @@ cuddGarbageCollect( 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); + int res = (hook->f)(unique,"DD",NULL); if (res == 0) return(0); hook = hook->next; } + + if (unique->dead + unique->deadZ == 0) { + hook = unique->postGCHook; + while (hook != NULL) { + int res = (hook->f)(unique,"DD",NULL); + if (res == 0) return(0); + hook = hook->next; + } return(0); } @@ -664,14 +769,14 @@ cuddGarbageCollect( ** 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); + 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); + (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); + unique->gcFrac = DD_GC_FRAC_HI; + return(0); } localTime = util_cpu_time(); @@ -679,115 +784,124 @@ cuddGarbageCollect( unique->garbageCollections++; #ifdef DD_VERBOSE (void) fprintf(unique->err, - "garbage collecting (%d dead out of %d, min %d)...", - unique->dead, unique->keys, unique->minDead); + "garbage collecting (%d dead BDD nodes out of %d, min %d)...", + unique->dead, unique->keys, unique->minDead); + (void) fprintf(unique->err, + " (%d dead ZDD nodes 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++; - } + 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); + cuddLocalCacheClearDead(unique); } /* Now return dead nodes to free list. Count them for sanity check. */ totalDeleted = 0; #ifndef DD_UNSORTED_FREE_LIST +#ifdef DD_RED_BLACK_FREE_LIST tree = NULL; #endif +#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++; + 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 DD_RED_BLACK_FREE_LIST #ifdef __osf__ #pragma pointer_size save #pragma pointer_size short #endif - cuddOrderedInsert(&tree,node); + cuddOrderedInsert(&tree,node); #ifdef __osf__ #pragma pointer_size restore #endif +#endif #else - cuddDeallocNode(unique,node); + cuddDeallocNode(unique,node); #endif - } else { - *lastP = node; - lastP = &(node->next); + } else { + *lastP = node; + lastP = &(node->next); + } + node = next; + } + *lastP = sentinel; } - node = next; + if ((unsigned) deleted != unique->subtables[i].dead) { + ddReportRefMess(unique, i, "cuddGarbageCollect"); } - *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; + 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++; + 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 DD_RED_BLACK_FREE_LIST #ifdef __osf__ #pragma pointer_size save #pragma pointer_size short #endif - cuddOrderedInsert(&tree,node); + cuddOrderedInsert(&tree,node); #ifdef __osf__ #pragma pointer_size restore #endif +#endif #else - cuddDeallocNode(unique,node); + cuddDeallocNode(unique,node); #endif - } else { - *lastP = node; - lastP = &(node->next); - } - node = next; + } else { + *lastP = node; + lastP = &(node->next); + } + node = next; + } + *lastP = NULL; } - *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) 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"); + ddReportRefMess(unique, -1, "cuddGarbageCollect"); } unique->keys -= totalDeleted; unique->dead = 0; @@ -795,198 +909,110 @@ cuddGarbageCollect( 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 + totalDeletedZ = 0; 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++; + 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 DD_RED_BLACK_FREE_LIST #ifdef __osf__ #pragma pointer_size save #pragma pointer_size short #endif - cuddOrderedInsert(&tree,node); + cuddOrderedInsert(&tree,node); #ifdef __osf__ #pragma pointer_size restore #endif +#endif #else - cuddDeallocNode(unique,node); + cuddDeallocNode(unique,node); #endif - } else { - *lastP = node; - lastP = &(node->next); - } - node = next; + } else { + *lastP = node; + lastP = &(node->next); + } + node = next; + } + *lastP = NULL; } - *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; + if ((unsigned) deleted != unique->subtableZ[i].dead) { + ddReportRefMess(unique, i, "cuddGarbageCollect"); + } + totalDeletedZ += 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"); + if ((unsigned) totalDeletedZ != unique->deadZ) { + ddReportRefMess(unique, -1, "cuddGarbageCollect"); } - unique->keysZ -= totalDeleted; + unique->keysZ -= totalDeletedZ; unique->deadZ = 0; #ifdef DD_STATS - unique->nodesFreed += (double) totalDeleted; + unique->nodesFreed += (double) totalDeletedZ; #endif + #ifndef DD_UNSORTED_FREE_LIST +#ifdef DD_RED_BLACK_FREE_LIST unique->nextFree = cuddOrderedThread(tree,unique->nextFree); +#else + memListTrav = unique->memoryList; + sentry = NULL; + while (memListTrav != NULL) { + ptruint offset; + nxtNode = (DdNodePtr *)memListTrav[0]; + offset = (ptruint) memListTrav & (sizeof(DdNode) - 1); + memListTrav += (sizeof(DdNode) - offset) / sizeof(DdNodePtr); + downTrav = (DdNode *)memListTrav; + k = 0; + do { + if (downTrav[k].ref == 0) { + if (sentry == NULL) { + unique->nextFree = sentry = &downTrav[k]; + } else { + /* First hook sentry->next to the dead node and then + ** reassign sentry to the dead node. */ + sentry = (sentry->next = &downTrav[k]); + } + } + } while (++k < DD_MEM_CHUNK); + memListTrav = nxtNode; + } + sentry->next = NULL; +#endif #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; + int res = (hook->f)(unique,"DD",NULL); + if (res == 0) return(0); + hook = hook->next; } #ifdef DD_VERBOSE (void) fprintf(unique->err," done\n"); #endif - return(totalDeleted); + return(totalDeleted+totalDeletedZ); -} /* end of cuddGarbageCollectZdd */ +} /* end of cuddGarbageCollect */ /**Function******************************************************************** @@ -1009,10 +1035,10 @@ cuddZddGetNode( DdNode * T, DdNode * E) { - DdNode *node; + DdNode *node; if (T == DD_ZERO(zdd)) - return(E); + return(E); node = cuddUniqueInterZdd(zdd, id, T, E); return(node); @@ -1042,26 +1068,26 @@ cuddZddGetNodeIVO( DdNode * g, DdNode * h) { - DdNode *f, *r, *t; - DdNode *zdd_one = DD_ONE(dd); - DdNode *zdd_zero = DD_ZERO(dd); + 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); + return(NULL); } cuddRef(f); t = cuddZddProduct(dd, f, g); if (t == NULL) { - Cudd_RecursiveDerefZdd(dd, f); - return(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); + Cudd_RecursiveDerefZdd(dd, t); + return(NULL); } cuddRef(r); Cudd_RecursiveDerefZdd(dd, t); @@ -1110,7 +1136,7 @@ cuddUniqueInter( #endif if (index >= unique->size) { - if (!ddResizeTable(unique,index)) return(NULL); + if (!ddResizeTable(unique,index)) return(NULL); } level = unique->perm[index]; @@ -1127,116 +1153,115 @@ cuddUniqueInter( looking = *previousP; while (T < cuddT(looking)) { - previousP = &(looking->next); - looking = *previousP; + previousP = &(looking->next); + looking = *previousP; #ifdef DD_UNIQUE_PROFILE - unique->uniqueLinks++; + unique->uniqueLinks++; #endif } while (T == cuddT(looking) && E < cuddE(looking)) { - previousP = &(looking->next); - looking = *previousP; + previousP = &(looking->next); + looking = *previousP; #ifdef DD_UNIQUE_PROFILE - unique->uniqueLinks++; + unique->uniqueLinks++; #endif } if (T == cuddT(looking) && E == cuddE(looking)) { - if (looking->ref == 0) { - cuddReclaim(unique,looking); - } - return(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); + 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; + 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; + retval = Cudd_DebugCheck(unique); + if (retval != 0) unique->reordered = 2; + retval = Cudd_CheckKeys(unique); + if (retval != 0) unique->reordered = 2; #endif - return(NULL); + 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); + ((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++; + unique->uniqueLinks++; #endif - } - while (T == cuddT(looking) && E < cuddE(looking)) { - previousP = &(looking->next); - looking = *previousP; + } + while (T == cuddT(looking) && E < cuddE(looking)) { + previousP = &(looking->next); + looking = *previousP; #ifdef DD_UNIQUE_PROFILE - unique->uniqueLinks++; + unique->uniqueLinks++; #endif - } + } } gcNumber = unique->garbageCollections; looking = cuddAllocNode(unique); if (looking == NULL) { - return(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); + 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++; + unique->uniqueLinks++; #endif - } - while (T == cuddT(looking2) && E < cuddE(looking2)) { - previousP = &(looking2->next); - looking2 = *previousP; + } + while (T == cuddT(looking2) && E < cuddE(looking2)) { + previousP = &(looking2->next); + looking2 = *previousP; #ifdef DD_UNIQUE_PROFILE - unique->uniqueLinks++; + 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 */ + cuddSatInc(T->ref); /* we know T is a regular pointer */ cuddRef(E); #ifdef DD_DEBUG @@ -1275,9 +1300,9 @@ cuddUniqueInterIVO( DdNode *v; v = cuddUniqueInter(unique, index, DD_ONE(unique), - Cudd_Not(DD_ONE(unique))); + Cudd_Not(DD_ONE(unique))); if (v == NULL) - return(NULL); + return(NULL); cuddRef(v); result = cuddBddIteRecur(unique, v, T, E); Cudd_RecursiveDeref(unique, v); @@ -1322,7 +1347,7 @@ cuddUniqueInterZdd( #endif if (index >= unique->sizeZ) { - if (!cuddResizeTableZdd(unique,index)) return(NULL); + if (!cuddResizeTableZdd(unique,index)) return(NULL); } level = unique->permZ[index]; @@ -1335,11 +1360,11 @@ cuddUniqueInterZdd( 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); - } + (10 * subtable->dead > 9 * subtable->keys))) { /* too many dead */ + (void) cuddGarbageCollect(unique,1); + } else { + ddRehashZdd(unique,(int)level); + } } pos = ddHash(T, E, subtable->shift); @@ -1348,14 +1373,14 @@ cuddUniqueInterZdd( while (looking != NULL) { if (cuddT(looking) == T && cuddE(looking) == E) { - if (looking->ref == 0) { - cuddReclaimZdd(unique,looking); + if (looking->ref == 0) { + cuddReclaimZdd(unique,looking); + } + return(looking); } - return(looking); - } - looking = looking->next; + looking = looking->next; #ifdef DD_UNIQUE_PROFILE - unique->uniqueLinks++; + unique->uniqueLinks++; #endif } @@ -1363,20 +1388,20 @@ cuddUniqueInterZdd( 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); + 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; + 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; + retval = Cudd_DebugCheck(unique); + if (retval != 0) unique->reordered = 2; + retval = Cudd_CheckKeys(unique); + if (retval != 0) unique->reordered = 2; #endif - return(NULL); + return(NULL); } unique->keysZ++; @@ -1384,7 +1409,6 @@ cuddUniqueInterZdd( looking = cuddAllocNode(unique); if (looking == NULL) return(NULL); - looking->ref = 0; looking->index = index; cuddT(looking) = T; cuddE(looking) = E; @@ -1427,17 +1451,17 @@ cuddUniqueConst( 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); - } + (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; + value = 0.0; } split.value = value; @@ -1452,15 +1476,15 @@ cuddUniqueConst( */ while (looking != NULL) { if (looking->type.value == value || - ddEqualVal(looking->type.value,value,unique->epsilon)) { - if (looking->ref == 0) { - cuddReclaim(unique,looking); + ddEqualVal(looking->type.value,value,unique->epsilon)) { + if (looking->ref == 0) { + cuddReclaim(unique,looking); + } + return(looking); } - return(looking); - } - looking = looking->next; + looking = looking->next; #ifdef DD_UNIQUE_PROFILE - unique->uniqueLinks++; + unique->uniqueLinks++; #endif } @@ -1469,7 +1493,6 @@ cuddUniqueConst( looking = cuddAllocNode(unique); if (looking == NULL) return(NULL); - looking->ref = 0; looking->index = CUDD_CONST_INDEX; looking->type.value = value; looking->next = nodelist[pos]; @@ -1504,144 +1527,143 @@ cuddRehash( DdNode *node, *next; DdNode *sentinel = &(unique->sentinel); hack split; -// extern void (*MMoutOfMemory)(long); - void (*saveHandler)(long); + extern DD_OOMFP MMoutOfMemory; + DD_OOMFP saveHandler; 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); + 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); + (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); + 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); + (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; + 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; + oldslots = unique->subtables[i].slots; + oldshift = unique->subtables[i].shift; + oldnodelist = unique->subtables[i].nodelist; - saveHandler = MMoutOfMemory; - MMoutOfMemory = Cudd_OutOfMem; - nodelist = ABC_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) { - ABC_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; + /* Compute the new size of the subtable. */ + slots = oldslots << 1; + shift = oldshift - 1; - /* 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); + saveHandler = MMoutOfMemory; + MMoutOfMemory = Cudd_OutOfMem; + nodelist = ABC_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) { + ABC_FREE(unique->stash); + unique->stash = NULL; + /* Inhibit resizing of tables. */ + cuddSlowTableGrowth(unique); + } + return; } - node = next; + 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; } - *evenP = *oddP = sentinel; - } - ABC_FREE(oldnodelist); + ABC_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); + (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 = ABC_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; + 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 = ABC_ALLOC(DdNodePtr, slots); + MMoutOfMemory = saveHandler; + if (nodelist == NULL) { + (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.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; + 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; } - } - ABC_FREE(oldnodelist); + 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; + } + } + ABC_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); + (void) fprintf(unique->err, + "rehashing constants: keys %d dead %d new size %d\n", + unique->constants.keys,unique->constants.dead,slots); #endif } @@ -1676,8 +1698,8 @@ cuddShrinkSubtable( DdNode *node, *next; DdNode *sentinel = &(unique->sentinel); unsigned int slots, oldslots; -// extern void (*MMoutOfMemory)(long); - void (*saveHandler)(long); + extern DD_OOMFP MMoutOfMemory; + DD_OOMFP saveHandler; oldnodelist = unique->subtables[i].nodelist; oldslots = unique->subtables[i].slots; @@ -1687,7 +1709,7 @@ cuddShrinkSubtable( nodelist = ABC_ALLOC(DdNodePtr, slots); MMoutOfMemory = saveHandler; if (nodelist == NULL) { - return; + return; } unique->subtables[i].nodelist = nodelist; unique->subtables[i].slots = slots; @@ -1695,43 +1717,43 @@ cuddShrinkSubtable( 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); + "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; + 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; + 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++; + unique->uniqueLinks++; #endif - } - while (T == cuddT(looking) && E < cuddE(looking)) { - previousP = &(looking->next); - looking = *previousP; + } + while (T == cuddT(looking) && E < cuddE(looking)) { + previousP = &(looking->next); + looking = *previousP; #ifdef DD_UNIQUE_PROFILE - unique->uniqueLinks++; + unique->uniqueLinks++; #endif + } + node->next = *previousP; + *previousP = node; + node = next; } - node->next = *previousP; - *previousP = node; - node = next; - } } ABC_FREE(oldnodelist); @@ -1739,8 +1761,8 @@ cuddShrinkSubtable( 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; + ddMin(unique->maxCacheHard,DD_MAX_CACHE_TO_SLOTS_RATIO * unique->slots) + - 2 * (int) unique->cacheSlots; } /* end of cuddShrinkSubtable */ @@ -1771,8 +1793,7 @@ cuddInsertSubtables( int oldsize,newsize; int i,j,index,reorderSave; unsigned int numSlots = unique->initSlots; - int *newperm, *newinvperm; - int *newmap = NULL; // Suppress "might be used uninitialized" + int *newperm, *newinvperm, *newmap; DdNode *one, *zero; #ifdef DD_DEBUG @@ -1782,210 +1803,210 @@ cuddInsertSubtables( 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 = - ABC_ALLOC(DdNodePtr, numSlots); - if (newnodelist == NULL) { - unique->errorCode = CUDD_MEMORY_OUT; - return(0); + /* 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; } - for (j = 0; j < (int)numSlots; j++) { - newnodelist[j] = sentinel; - } - } - if (unique->map != NULL) { + /* Create new subtables. */ for (i = 0; i < n; i++) { - unique->map[oldsize+i] = oldsize + 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 = + ABC_ALLOC(DdNodePtr, numSlots); + if (newnodelist == NULL) { + unique->errorCode = CUDD_MEMORY_OUT; + return(0); + } + for (j = 0; (unsigned) 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; + /* 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); + (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 = ABC_ALLOC(DdSubtable,newsize); - if (newsubtables == NULL) { - unique->errorCode = CUDD_MEMORY_OUT; - return(0); - } - newvars = ABC_ALLOC(DdNodePtr,newsize); - if (newvars == NULL) { - unique->errorCode = CUDD_MEMORY_OUT; - ABC_FREE(newsubtables); - return(0); - } - newperm = ABC_ALLOC(int,newsize); - if (newperm == NULL) { - unique->errorCode = CUDD_MEMORY_OUT; - ABC_FREE(newsubtables); - ABC_FREE(newvars); - return(0); - } - newinvperm = ABC_ALLOC(int,newsize); - if (newinvperm == NULL) { - unique->errorCode = CUDD_MEMORY_OUT; - ABC_FREE(newsubtables); - ABC_FREE(newvars); - ABC_FREE(newperm); - return(0); - } - if (unique->map != NULL) { - newmap = ABC_ALLOC(int,newsize); - if (newmap == NULL) { - unique->errorCode = CUDD_MEMORY_OUT; - ABC_FREE(newsubtables); - ABC_FREE(newvars); - ABC_FREE(newperm); - ABC_FREE(newinvperm); - return(0); + /* Allocate memory for new arrays (except nodelists). */ + newsubtables = ABC_ALLOC(DdSubtable,newsize); + if (newsubtables == NULL) { + 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)); - /* 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 = ABC_ALLOC(DdNodePtr, numSlots); - if (newnodelist == NULL) { - /* We are going to leak some memory. We should clean up. */ - unique->errorCode = CUDD_MEMORY_OUT; - return(0); + newvars = ABC_ALLOC(DdNodePtr,newsize); + if (newvars == NULL) { + unique->errorCode = CUDD_MEMORY_OUT; + ABC_FREE(newsubtables); + return(0); } - for (j = 0; j < (int)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]; + newperm = ABC_ALLOC(int,newsize); + if (newperm == NULL) { + unique->errorCode = CUDD_MEMORY_OUT; + ABC_FREE(newsubtables); + ABC_FREE(newvars); + return(0); } - for (i = oldsize; i < oldsize + n; i++) { - newmap[i] = i; + newinvperm = ABC_ALLOC(int,newsize); + if (newinvperm == NULL) { + unique->errorCode = CUDD_MEMORY_OUT; + ABC_FREE(newsubtables); + ABC_FREE(newvars); + ABC_FREE(newperm); + return(0); } - ABC_FREE(unique->map); - unique->map = newmap; - } - /* Install the new tables and free the old ones. */ - ABC_FREE(unique->subtables); - unique->subtables = newsubtables; - unique->maxSize = newsize; - ABC_FREE(unique->vars); - unique->vars = newvars; - ABC_FREE(unique->perm); - unique->perm = newperm; - ABC_FREE(unique->invperm); - unique->invperm = newinvperm; - /* Update the stack for iterative procedures. */ - if (newsize > unique->maxSizeZ) { - ABC_FREE(unique->stack); - unique->stack = ABC_ALLOC(DdNodePtr,newsize + 1); - if (unique->stack == NULL) { - unique->errorCode = CUDD_MEMORY_OUT; - return(0); + if (unique->map != NULL) { + newmap = ABC_ALLOC(int,newsize); + if (newmap == NULL) { + unique->errorCode = CUDD_MEMORY_OUT; + ABC_FREE(newsubtables); + ABC_FREE(newvars); + ABC_FREE(newperm); + ABC_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 = ABC_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; (unsigned) 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; + } + ABC_FREE(unique->map); + unique->map = newmap; + } + /* Install the new tables and free the old ones. */ + ABC_FREE(unique->subtables); + unique->subtables = newsubtables; + unique->maxSize = newsize; + ABC_FREE(unique->vars); + unique->vars = newvars; + ABC_FREE(unique->perm); + unique->perm = newperm; + ABC_FREE(unique->invperm); + unique->invperm = newinvperm; + /* Update the stack for iterative procedures. */ + if (newsize > unique->maxSizeZ) { + ABC_FREE(unique->stack); + unique->stack = ABC_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 *); } - 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; @@ -2002,53 +2023,53 @@ cuddInsertSubtables( 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; - ABC_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]); + 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; + ABC_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->tree->size += n; + unique->tree->index = unique->invperm[0]; + ddPatchTree(unique,unique->tree); } unique->autoDyn = reorderSave; @@ -2103,26 +2124,26 @@ cuddDestroySubtables( */ 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; + 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]); + Cudd_RecursiveDeref(unique,vars[index]); } /* Collect garbage, because we cannot afford having dead nodes pointing @@ -2132,15 +2153,15 @@ cuddDestroySubtables( /* Here we know we can destroy our subtables. */ for (index = firstIndex; index < lastIndex; index++) { - level = unique->perm[index]; - nodelist = subtables[level].nodelist; + level = unique->perm[index]; + nodelist = subtables[level].nodelist; #ifdef DD_DEBUG - assert(subtables[level].keys == 0); + assert(subtables[level].keys == 0); #endif - ABC_FREE(nodelist); - unique->memused -= sizeof(DdNodePtr) * subtables[level].slots; - unique->slots -= subtables[level].slots; - unique->dead -= subtables[level].dead; + ABC_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 @@ -2152,33 +2173,33 @@ cuddDestroySubtables( */ 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; + 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); - ABC_FREE(unique->map); - unique->map = NULL; + cuddCacheFlush(unique); + ABC_FREE(unique->map); + unique->map = NULL; } unique->minDead = (unsigned) (unique->gcFrac * (double) unique->slots); @@ -2216,105 +2237,104 @@ cuddResizeTableZdd( 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 = - ABC_ALLOC(DdNodePtr, numSlots); - if (newnodelist == NULL) { - unique->errorCode = CUDD_MEMORY_OUT; - return(0); - } - for (j = 0; j < (int)numSlots; j++) { - newnodelist[j] = NULL; + 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 = + ABC_ALLOC(DdNodePtr, numSlots); + if (newnodelist == NULL) { + unique->errorCode = CUDD_MEMORY_OUT; + return(0); + } + for (j = 0; (unsigned) 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; + /* 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); + (void) fprintf(unique->err, + "Increasing the ZDD table size from %d to %d\n", + unique->maxSizeZ, newsize); #endif - newsubtables = ABC_ALLOC(DdSubtable,newsize); - if (newsubtables == NULL) { - unique->errorCode = CUDD_MEMORY_OUT; - return(0); - } - newperm = ABC_ALLOC(int,newsize); - if (newperm == NULL) { - unique->errorCode = CUDD_MEMORY_OUT; - return(0); - } - newinvperm = ABC_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) { - ABC_FREE(unique->stack); - unique->stack = ABC_ALLOC(DdNodePtr,newsize + 1); - if (unique->stack == NULL) { - unique->errorCode = CUDD_MEMORY_OUT; - return(0); + newsubtables = ABC_ALLOC(DdSubtable,newsize); + if (newsubtables == 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 = ABC_ALLOC(DdNodePtr, numSlots); - if (newnodelist == NULL) { - unique->errorCode = CUDD_MEMORY_OUT; - return(0); + newperm = ABC_ALLOC(int,newsize); + if (newperm == NULL) { + unique->errorCode = CUDD_MEMORY_OUT; + return(0); } - for (j = 0; j < (int)numSlots; j++) { - newnodelist[j] = NULL; + newinvperm = ABC_ALLOC(int,newsize); + if (newinvperm == NULL) { + unique->errorCode = CUDD_MEMORY_OUT; + return(0); } - } - ABC_FREE(unique->subtableZ); - unique->subtableZ = newsubtables; - unique->maxSizeZ = newsize; - ABC_FREE(unique->permZ); - unique->permZ = newperm; - ABC_FREE(unique->invpermZ); - unique->invpermZ = newinvperm; + unique->memused += (newsize - unique->maxSizeZ) * ((numSlots+1) * + sizeof(DdNode *) + 2 * sizeof(int) + sizeof(DdSubtable)); + if (newsize > unique->maxSize) { + ABC_FREE(unique->stack); + unique->stack = ABC_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 = ABC_ALLOC(DdNodePtr, numSlots); + if (newnodelist == NULL) { + unique->errorCode = CUDD_MEMORY_OUT; + return(0); + } + for (j = 0; (unsigned) j < numSlots; j++) { + newnodelist[j] = NULL; + } + } + ABC_FREE(unique->subtableZ); + unique->subtableZ = newsubtables; + unique->maxSizeZ = newsize; + ABC_FREE(unique->permZ); + unique->permZ = newperm; + ABC_FREE(unique->invpermZ); + unique->invpermZ = newinvperm; } unique->slots += (index + 1 - unique->sizeZ) * numSlots; ddFixLimits(unique); @@ -2324,15 +2344,13 @@ cuddResizeTableZdd( ** 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(0); } unique->autoDynZ = reorderSave; @@ -2359,16 +2377,16 @@ cuddSlowTableGrowth( int i; unique->maxCacheHard = unique->cacheSlots - 1; - unique->cacheSlack = -(int)(unique->cacheSlots + 1); + unique->cacheSlack = - (int) (unique->cacheSlots + 1); for (i = 0; i < unique->size; i++) { - unique->subtables[i].maxKeys <<= 2; + 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); + (void) fprintf(unique->err,"minDead = %u\n", unique->minDead); } /* end of cuddSlowTableGrowth */ @@ -2399,19 +2417,19 @@ ddRehashZdd( int j, pos; DdNodePtr *nodelist, *oldnodelist; DdNode *node, *next; -// extern void (*MMoutOfMemory)(long); - void (*saveHandler)(long); + extern DD_OOMFP MMoutOfMemory; + DD_OOMFP saveHandler; if (unique->slots > unique->looseUpTo) { - unique->minDead = (unsigned) (DD_GC_FRAC_LO * (double) unique->slots); + 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); - } + 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; + unique->gcFrac = DD_GC_FRAC_LO; } assert(i != CUDD_MAXINDEX); @@ -2425,8 +2443,8 @@ ddRehashZdd( slots = oldslots; shift = oldshift; do { - slots <<= 1; - shift--; + slots <<= 1; + shift--; } while (slots * DD_MAX_SUBTABLE_DENSITY < unique->subtableZ[i].keys); saveHandler = MMoutOfMemory; @@ -2434,40 +2452,39 @@ ddRehashZdd( nodelist = ABC_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; + (void) fprintf(unique->err, + "Unable to resize ZDD subtable %d for lack of memory.\n", + i); + (void) cuddGarbageCollect(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; + 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; - } + 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; + } } ABC_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); + "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. */ @@ -2503,176 +2520,175 @@ ddResizeTable( int oldsize,newsize; int i,j,reorderSave; int numSlots = unique->initSlots; - int *newperm, *newinvperm; - int *newmap = NULL; // Suppress "might be used uninitialized" + 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 = - ABC_ALLOC(DdNodePtr, numSlots); - if (newnodelist == NULL) { - for (j = oldsize; j < i; j++) { - ABC_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; + 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 = + ABC_ALLOC(DdNodePtr, numSlots); + if (newnodelist == NULL) { + for (j = oldsize; j < i; j++) { + ABC_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; + /* 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); + (void) fprintf(unique->err, + "Increasing the table size from %d to %d\n", + unique->maxSize, newsize); #endif - newsubtables = ABC_ALLOC(DdSubtable,newsize); - if (newsubtables == NULL) { - unique->errorCode = CUDD_MEMORY_OUT; - return(0); - } - newvars = ABC_ALLOC(DdNodePtr,newsize); - if (newvars == NULL) { - ABC_FREE(newsubtables); - unique->errorCode = CUDD_MEMORY_OUT; - return(0); - } - newperm = ABC_ALLOC(int,newsize); - if (newperm == NULL) { - ABC_FREE(newsubtables); - ABC_FREE(newvars); - unique->errorCode = CUDD_MEMORY_OUT; - return(0); - } - newinvperm = ABC_ALLOC(int,newsize); - if (newinvperm == NULL) { - ABC_FREE(newsubtables); - ABC_FREE(newvars); - ABC_FREE(newperm); - unique->errorCode = CUDD_MEMORY_OUT; - return(0); - } - if (unique->map != NULL) { - newmap = ABC_ALLOC(int,newsize); - if (newmap == NULL) { - ABC_FREE(newsubtables); - ABC_FREE(newvars); - ABC_FREE(newperm); - ABC_FREE(newinvperm); - unique->errorCode = CUDD_MEMORY_OUT; - return(0); + newsubtables = ABC_ALLOC(DdSubtable,newsize); + if (newsubtables == NULL) { + 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) { - ABC_FREE(unique->stack); - unique->stack = ABC_ALLOC(DdNodePtr,newsize + 1); - if (unique->stack == NULL) { - ABC_FREE(newsubtables); - ABC_FREE(newvars); - ABC_FREE(newperm); - ABC_FREE(newinvperm); - if (unique->map != NULL) { - ABC_FREE(newmap); + newvars = ABC_ALLOC(DdNodePtr,newsize); + if (newvars == NULL) { + ABC_FREE(newsubtables); + unique->errorCode = CUDD_MEMORY_OUT; + return(0); } - unique->errorCode = CUDD_MEMORY_OUT; - return(0); + newperm = ABC_ALLOC(int,newsize); + if (newperm == NULL) { + ABC_FREE(newsubtables); + ABC_FREE(newvars); + 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 = ABC_ALLOC(DdNodePtr, numSlots); - if (newnodelist == NULL) { - unique->errorCode = CUDD_MEMORY_OUT; - return(0); + newinvperm = ABC_ALLOC(int,newsize); + if (newinvperm == NULL) { + ABC_FREE(newsubtables); + ABC_FREE(newvars); + ABC_FREE(newperm); + unique->errorCode = CUDD_MEMORY_OUT; + return(0); } - for (j = 0; j < numSlots; j++) { - newnodelist[j] = sentinel; + if (unique->map != NULL) { + newmap = ABC_ALLOC(int,newsize); + if (newmap == NULL) { + ABC_FREE(newsubtables); + ABC_FREE(newvars); + ABC_FREE(newperm); + ABC_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) { + ABC_FREE(unique->stack); + unique->stack = ABC_ALLOC(DdNodePtr,newsize + 1); + if (unique->stack == NULL) { + ABC_FREE(newsubtables); + ABC_FREE(newvars); + ABC_FREE(newperm); + ABC_FREE(newinvperm); + if (unique->map != NULL) { + ABC_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 *); } - } - if (unique->map != NULL) { for (i = 0; i < oldsize; i++) { - newmap[i] = unique->map[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++) { - newmap[i] = 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 = ABC_ALLOC(DdNodePtr, numSlots); + if (newnodelist == NULL) { + unique->errorCode = CUDD_MEMORY_OUT; + return(0); + } + for (j = 0; j < numSlots; j++) { + newnodelist[j] = sentinel; + } } - ABC_FREE(unique->map); - unique->map = newmap; - } - ABC_FREE(unique->subtables); - unique->subtables = newsubtables; - unique->maxSize = newsize; - ABC_FREE(unique->vars); - unique->vars = newvars; - ABC_FREE(unique->perm); - unique->perm = newperm; - ABC_FREE(unique->invperm); - unique->invperm = newinvperm; + if (unique->map != NULL) { + for (i = 0; i < oldsize; i++) { + newmap[i] = unique->map[i]; + } + for (i = oldsize; i <= index; i++) { + newmap[i] = i; + } + ABC_FREE(unique->map); + unique->map = newmap; + } + ABC_FREE(unique->subtables); + unique->subtables = newsubtables; + unique->maxSize = newsize; + ABC_FREE(unique->vars); + unique->vars = newvars; + ABC_FREE(unique->perm); + unique->perm = newperm; + ABC_FREE(unique->invperm); + unique->invperm = newinvperm; } /* Now that the table is in a coherent state, create the new @@ -2689,24 +2705,24 @@ ddResizeTable( 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++) { - ABC_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->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++) { + ABC_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; @@ -2733,27 +2749,27 @@ cuddFindParent( DdNode * node) { int i,j; - int slots; - DdNodePtr *nodelist; - DdNode *f; + 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; + 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); + 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); @@ -2780,16 +2796,17 @@ ddFixLimits( { 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; + DD_MAX_CACHE_TO_SLOTS_RATIO * unique->slots) - + 2 * (int) unique->cacheSlots; if (unique->cacheSlots < unique->slots/2 && unique->cacheSlack >= 0) - cuddCacheResize(unique); + cuddCacheResize(unique); return; } /* end of ddFixLimits */ #ifndef DD_UNSORTED_FREE_LIST +#ifdef DD_RED_BLACK_FREE_LIST /**Function******************************************************************** Synopsis [Inserts a DdNode in a red/black search tree.] @@ -2814,13 +2831,13 @@ cuddOrderedInsert( 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); + 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; @@ -2866,42 +2883,42 @@ cuddOrderedThread( *((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; + 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 { - current = prev; + /* 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); @@ -2983,55 +3000,56 @@ cuddDoRebalance( 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; + 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 { - DD_COLOR(parent) = DD_BLACK; - } - DD_COLOR(grandpa) = DD_RED; - cuddRotateLeft(grandpaP); + 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 +#endif /**Function******************************************************************** @@ -3055,11 +3073,11 @@ ddPatchTree( MtrNode *auxnode = treenode; while (auxnode != NULL) { - auxnode->low = dd->perm[auxnode->index]; - if (auxnode->child != NULL) { - ddPatchTree(dd, auxnode->child); - } - auxnode = auxnode->younger; + auxnode->low = dd->perm[auxnode->index]; + if (auxnode->child != NULL) { + ddPatchTree(dd, auxnode->child); + } + auxnode = auxnode->younger; } return; @@ -3096,14 +3114,14 @@ cuddCheckCollisionOrdering( 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; + 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); @@ -3128,14 +3146,14 @@ static void ddReportRefMess( DdManager *unique /* manager */, int i /* table in which the problem occurred */, - char *caller /* procedure that detected the problem */) + const char *caller /* procedure that detected the problem */) { if (i == CUDD_CONST_INDEX) { - (void) fprintf(unique->err, - "%s: problem in constants\n", caller); + (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, + "%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 \ @@ -3144,5 +3162,7 @@ See the CUDD Programmer's Guide for additional details."); abort(); } /* end of ddReportRefMess */ + + ABC_NAMESPACE_IMPL_END |