From 888e5bed5d7f56a5d86d91a6e8e88f3e5a3454dc Mon Sep 17 00:00:00 2001 From: Alan Mishchenko Date: Fri, 29 Jul 2005 08:01:00 -0700 Subject: Version abc50729 --- src/bdd/cudd/cuddLCache.c | 1428 +++++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 1428 insertions(+) create mode 100644 src/bdd/cudd/cuddLCache.c (limited to 'src/bdd/cudd/cuddLCache.c') diff --git a/src/bdd/cudd/cuddLCache.c b/src/bdd/cudd/cuddLCache.c new file mode 100644 index 00000000..72fbd48a --- /dev/null +++ b/src/bdd/cudd/cuddLCache.c @@ -0,0 +1,1428 @@ +/**CFile*********************************************************************** + + FileName [cuddLCache.c] + + PackageName [cudd] + + Synopsis [Functions for local caches.] + + Description [Internal procedures included in this module: + + Static procedures included in this module: + ] + + SeeAlso [] + + Author [Fabio Somenzi] + + Copyright [ This file was created at the University of Colorado at + Boulder. The University of Colorado at Boulder makes no warranty + about the suitability of this software for any purpose. It is + presented on an AS IS basis.] + +******************************************************************************/ + +#include "util.h" +#include "cuddInt.h" + +/*---------------------------------------------------------------------------*/ +/* Constant declarations */ +/*---------------------------------------------------------------------------*/ + +#define DD_MAX_HASHTABLE_DENSITY 2 /* tells when to resize a table */ + +/*---------------------------------------------------------------------------*/ +/* Stucture declarations */ +/*---------------------------------------------------------------------------*/ + + +/*---------------------------------------------------------------------------*/ +/* Type declarations */ +/*---------------------------------------------------------------------------*/ + + +/*---------------------------------------------------------------------------*/ +/* Variable declarations */ +/*---------------------------------------------------------------------------*/ + +#ifndef lint +static char rcsid[] DD_UNUSED = "$Id: cuddLCache.c,v 1.1.1.1 2003/02/24 22:23:52 wjiang Exp $"; +#endif + +/*---------------------------------------------------------------------------*/ +/* Macro declarations */ +/*---------------------------------------------------------------------------*/ + +/**Macro*********************************************************************** + + Synopsis [Computes hash function for keys of two operands.] + + Description [] + + SideEffects [None] + + SeeAlso [ddLCHash3 ddLCHash] + +******************************************************************************/ +#if SIZEOF_VOID_P == 8 && SIZEOF_INT == 4 +#define ddLCHash2(f,g,shift) \ +((((unsigned)(unsigned long)(f) * DD_P1 + \ + (unsigned)(unsigned long)(g)) * DD_P2) >> (shift)) +#else +#define ddLCHash2(f,g,shift) \ +((((unsigned)(f) * DD_P1 + (unsigned)(g)) * DD_P2) >> (shift)) +#endif + + +/**Macro*********************************************************************** + + Synopsis [Computes hash function for keys of three operands.] + + Description [] + + SideEffects [None] + + SeeAlso [ddLCHash2 ddLCHash] + +******************************************************************************/ +#define ddLCHash3(f,g,h,shift) ddCHash2(f,g,h,shift) + + +/**AutomaticStart*************************************************************/ + +/*---------------------------------------------------------------------------*/ +/* Static function prototypes */ +/*---------------------------------------------------------------------------*/ + +static void cuddLocalCacheResize ARGS((DdLocalCache *cache)); +DD_INLINE static unsigned int ddLCHash ARGS((DdNodePtr *key, unsigned int keysize, int shift)); +static void cuddLocalCacheAddToList ARGS((DdLocalCache *cache)); +static void cuddLocalCacheRemoveFromList ARGS((DdLocalCache *cache)); +static int cuddHashTableResize ARGS((DdHashTable *hash)); +DD_INLINE static DdHashItem * cuddHashTableAlloc ARGS((DdHashTable *hash)); + +/**AutomaticEnd***************************************************************/ + + +/*---------------------------------------------------------------------------*/ +/* Definition of exported functions */ +/*---------------------------------------------------------------------------*/ + +/*---------------------------------------------------------------------------*/ +/* Definition of internal functions */ +/*---------------------------------------------------------------------------*/ + + +/**Function******************************************************************** + + Synopsis [Initializes a local computed table.] + + Description [Initializes a computed table. Returns a pointer the + the new local cache in case of success; NULL otherwise.] + + SideEffects [None] + + SeeAlso [cuddInitCache] + +******************************************************************************/ +DdLocalCache * +cuddLocalCacheInit( + DdManager * manager /* manager */, + unsigned int keySize /* size of the key (number of operands) */, + unsigned int cacheSize /* Initial size of the cache */, + unsigned int maxCacheSize /* Size of the cache beyond which no resizing occurs */) +{ + DdLocalCache *cache; + int logSize; + + cache = ALLOC(DdLocalCache,1); + if (cache == NULL) { + manager->errorCode = CUDD_MEMORY_OUT; + return(NULL); + } + cache->manager = manager; + cache->keysize = keySize; + cache->itemsize = (keySize + 1) * sizeof(DdNode *); +#ifdef DD_CACHE_PROFILE + cache->itemsize += sizeof(ptrint); +#endif + logSize = cuddComputeFloorLog2(ddMax(cacheSize,manager->slots/2)); + cacheSize = 1 << logSize; + cache->item = (DdLocalCacheItem *) + ALLOC(char, cacheSize * cache->itemsize); + if (cache->item == NULL) { + manager->errorCode = CUDD_MEMORY_OUT; + FREE(cache); + return(NULL); + } + cache->slots = cacheSize; + cache->shift = sizeof(int) * 8 - logSize; + cache->maxslots = ddMin(maxCacheSize,manager->slots); + cache->minHit = manager->minHit; + /* Initialize to avoid division by 0 and immediate resizing. */ + cache->lookUps = (double) (int) (cacheSize * cache->minHit + 1); + cache->hits = 0; + manager->memused += cacheSize * cache->itemsize + sizeof(DdLocalCache); + + /* Initialize the cache. */ + memset(cache->item, 0, cacheSize * cache->itemsize); + + /* Add to manager's list of local caches for GC. */ + cuddLocalCacheAddToList(cache); + + return(cache); + +} /* end of cuddLocalCacheInit */ + + +/**Function******************************************************************** + + Synopsis [Shuts down a local computed table.] + + Description [Initializes the computed table. It is called by + Cudd_Init. Returns a pointer the the new local cache in case of + success; NULL otherwise.] + + SideEffects [None] + + SeeAlso [cuddLocalCacheInit] + +******************************************************************************/ +void +cuddLocalCacheQuit( + DdLocalCache * cache /* cache to be shut down */) +{ + cache->manager->memused -= + cache->slots * cache->itemsize + sizeof(DdLocalCache); + cuddLocalCacheRemoveFromList(cache); + FREE(cache->item); + FREE(cache); + + return; + +} /* end of cuddLocalCacheQuit */ + + +/**Function******************************************************************** + + Synopsis [Inserts a result in a local cache.] + + Description [] + + SideEffects [None] + + SeeAlso [] + +******************************************************************************/ +void +cuddLocalCacheInsert( + DdLocalCache * cache, + DdNodePtr * key, + DdNode * value) +{ + unsigned int posn; + DdLocalCacheItem *entry; + + posn = ddLCHash(key,cache->keysize,cache->shift); + entry = (DdLocalCacheItem *) ((char *) cache->item + + posn * cache->itemsize); + memcpy(entry->key,key,cache->keysize * sizeof(DdNode *)); + entry->value = value; +#ifdef DD_CACHE_PROFILE + entry->count++; +#endif + +} /* end of cuddLocalCacheInsert */ + + +/**Function******************************************************************** + + Synopsis [Looks up in a local cache.] + + Description [Looks up in a local cache. Returns the result if found; + it returns NULL if no result is found.] + + SideEffects [None] + + SeeAlso [] + +******************************************************************************/ +DdNode * +cuddLocalCacheLookup( + DdLocalCache * cache, + DdNodePtr * key) +{ + unsigned int posn; + DdLocalCacheItem *entry; + DdNode *value; + + cache->lookUps++; + posn = ddLCHash(key,cache->keysize,cache->shift); + entry = (DdLocalCacheItem *) ((char *) cache->item + + posn * cache->itemsize); + if (entry->value != NULL && + memcmp(key,entry->key,cache->keysize*sizeof(DdNode *)) == 0) { + cache->hits++; + value = Cudd_Regular(entry->value); + if (value->ref == 0) { + cuddReclaim(cache->manager,value); + } + return(entry->value); + } + + /* Cache miss: decide whether to resize */ + + if (cache->slots < cache->maxslots && + cache->hits > cache->lookUps * cache->minHit) { + cuddLocalCacheResize(cache); + } + + return(NULL); + +} /* end of cuddLocalCacheLookup */ + + +/**Function******************************************************************** + + Synopsis [Clears the dead entries of the local caches of a manager.] + + Description [Clears the dead entries of the local caches of a manager. + Used during garbage collection.] + + SideEffects [None] + + SeeAlso [] + +******************************************************************************/ +void +cuddLocalCacheClearDead( + DdManager * manager) +{ + DdLocalCache *cache = manager->localCaches; + unsigned int keysize; + unsigned int itemsize; + unsigned int slots; + DdLocalCacheItem *item; + DdNodePtr *key; + unsigned int i, j; + + while (cache != NULL) { + keysize = cache->keysize; + itemsize = cache->itemsize; + slots = cache->slots; + item = cache->item; + for (i = 0; i < slots; i++) { + if (item->value != NULL && Cudd_Regular(item->value)->ref == 0) { + item->value = NULL; + } else { + key = item->key; + for (j = 0; j < keysize; j++) { + if (Cudd_Regular(key[j])->ref == 0) { + item->value = NULL; + break; + } + } + } + item = (DdLocalCacheItem *) ((char *) item + itemsize); + } + cache = cache->next; + } + return; + +} /* end of cuddLocalCacheClearDead */ + + +/**Function******************************************************************** + + Synopsis [Clears the local caches of a manager.] + + Description [Clears the local caches of a manager. + Used before reordering.] + + SideEffects [None] + + SeeAlso [] + +******************************************************************************/ +void +cuddLocalCacheClearAll( + DdManager * manager) +{ + DdLocalCache *cache = manager->localCaches; + + while (cache != NULL) { + memset(cache->item, 0, cache->slots * cache->itemsize); + cache = cache->next; + } + return; + +} /* end of cuddLocalCacheClearAll */ + + +#ifdef DD_CACHE_PROFILE + +#define DD_HYSTO_BINS 8 + +/**Function******************************************************************** + + Synopsis [Computes and prints a profile of a local cache usage.] + + Description [Computes and prints a profile of a local cache usage. + Returns 1 if successful; 0 otherwise.] + + SideEffects [None] + + SeeAlso [] + +******************************************************************************/ +int +cuddLocalCacheProfile( + DdLocalCache * cache) +{ + double count, mean, meansq, stddev, expected; + long max, min; + int imax, imin; + int i, retval, slots; + long *hystogram; + int nbins = DD_HYSTO_BINS; + int bin; + long thiscount; + double totalcount; + int nzeroes; + DdLocalCacheItem *entry; + FILE *fp = cache->manager->out; + + slots = cache->slots; + + meansq = mean = expected = 0.0; + max = min = (long) cache->item[0].count; + imax = imin = nzeroes = 0; + totalcount = 0.0; + + hystogram = ALLOC(long, nbins); + if (hystogram == NULL) { + return(0); + } + for (i = 0; i < nbins; i++) { + hystogram[i] = 0; + } + + for (i = 0; i < slots; i++) { + entry = (DdLocalCacheItem *) ((char *) cache->item + + i * cache->itemsize); + thiscount = (long) entry->count; + if (thiscount > max) { + max = thiscount; + imax = i; + } + if (thiscount < min) { + min = thiscount; + imin = i; + } + if (thiscount == 0) { + nzeroes++; + } + count = (double) thiscount; + mean += count; + meansq += count * count; + totalcount += count; + expected += count * (double) i; + bin = (i * nbins) / slots; + hystogram[bin] += thiscount; + } + mean /= (double) slots; + meansq /= (double) slots; + stddev = sqrt(meansq - mean*mean); + + retval = fprintf(fp,"Cache stats: slots = %d average = %g ", slots, mean); + if (retval == EOF) return(0); + retval = fprintf(fp,"standard deviation = %g\n", stddev); + if (retval == EOF) return(0); + retval = fprintf(fp,"Cache max accesses = %ld for slot %d\n", max, imax); + if (retval == EOF) return(0); + retval = fprintf(fp,"Cache min accesses = %ld for slot %d\n", min, imin); + if (retval == EOF) return(0); + retval = fprintf(fp,"Cache unused slots = %d\n", nzeroes); + if (retval == EOF) return(0); + + if (totalcount) { + expected /= totalcount; + retval = fprintf(fp,"Cache access hystogram for %d bins", nbins); + if (retval == EOF) return(0); + retval = fprintf(fp," (expected bin value = %g)\n# ", expected); + if (retval == EOF) return(0); + for (i = nbins - 1; i>=0; i--) { + retval = fprintf(fp,"%ld ", hystogram[i]); + if (retval == EOF) return(0); + } + retval = fprintf(fp,"\n"); + if (retval == EOF) return(0); + } + + FREE(hystogram); + return(1); + +} /* end of cuddLocalCacheProfile */ +#endif + + +/**Function******************************************************************** + + Synopsis [Initializes a hash table.] + + Description [Initializes a hash table. Returns a pointer to the new + table if successful; NULL otherwise.] + + SideEffects [None] + + SeeAlso [cuddHashTableQuit] + +******************************************************************************/ +DdHashTable * +cuddHashTableInit( + DdManager * manager, + unsigned int keySize, + unsigned int initSize) +{ + DdHashTable *hash; + int logSize; + +#ifdef __osf__ +#pragma pointer_size save +#pragma pointer_size short +#endif + hash = ALLOC(DdHashTable, 1); + if (hash == NULL) { + manager->errorCode = CUDD_MEMORY_OUT; + return(NULL); + } + hash->keysize = keySize; + hash->manager = manager; + hash->memoryList = NULL; + hash->nextFree = NULL; + hash->itemsize = (keySize + 1) * sizeof(DdNode *) + + sizeof(ptrint) + sizeof(DdHashItem *); + /* We have to guarantee that the shift be < 32. */ + if (initSize < 2) initSize = 2; + logSize = cuddComputeFloorLog2(initSize); + hash->numBuckets = 1 << logSize; + hash->shift = sizeof(int) * 8 - logSize; + hash->bucket = ALLOC(DdHashItem *, hash->numBuckets); + if (hash->bucket == NULL) { + manager->errorCode = CUDD_MEMORY_OUT; + FREE(hash); + return(NULL); + } + memset(hash->bucket, 0, hash->numBuckets * sizeof(DdHashItem *)); + hash->size = 0; + hash->maxsize = hash->numBuckets * DD_MAX_HASHTABLE_DENSITY; +#ifdef __osf__ +#pragma pointer_size restore +#endif + return(hash); + +} /* end of cuddHashTableInit */ + + +/**Function******************************************************************** + + Synopsis [Shuts down a hash table.] + + Description [Shuts down a hash table, dereferencing all the values.] + + SideEffects [None] + + SeeAlso [cuddHashTableInit] + +******************************************************************************/ +void +cuddHashTableQuit( + DdHashTable * hash) +{ +#ifdef __osf__ +#pragma pointer_size save +#pragma pointer_size short +#endif + unsigned int i; + DdManager *dd = hash->manager; + DdHashItem *bucket; + DdHashItem **memlist, **nextmem; + unsigned int numBuckets = hash->numBuckets; + + for (i = 0; i < numBuckets; i++) { + bucket = hash->bucket[i]; + while (bucket != NULL) { + Cudd_RecursiveDeref(dd, bucket->value); + bucket = bucket->next; + } + } + + memlist = hash->memoryList; + while (memlist != NULL) { + nextmem = (DdHashItem **) memlist[0]; + FREE(memlist); + memlist = nextmem; + } + + FREE(hash->bucket); + FREE(hash); +#ifdef __osf__ +#pragma pointer_size restore +#endif + + return; + +} /* end of cuddHashTableQuit */ + + +/**Function******************************************************************** + + Synopsis [Inserts an item in a hash table.] + + Description [Inserts an item in a hash table when the key has more than + three pointers. Returns 1 if successful; 0 otherwise.] + + SideEffects [None] + + SeeAlso [[cuddHashTableInsert1 cuddHashTableInsert2 cuddHashTableInsert3 + cuddHashTableLookup] + +******************************************************************************/ +int +cuddHashTableInsert( + DdHashTable * hash, + DdNodePtr * key, + DdNode * value, + ptrint count) +{ + int result; + unsigned int posn; + DdHashItem *item; + unsigned int i; + +#ifdef DD_DEBUG + assert(hash->keysize > 3); +#endif + + if (hash->size > hash->maxsize) { + result = cuddHashTableResize(hash); + if (result == 0) return(0); + } + item = cuddHashTableAlloc(hash); + if (item == NULL) return(0); + hash->size++; + item->value = value; + cuddRef(value); + item->count = count; + for (i = 0; i < hash->keysize; i++) { + item->key[i] = key[i]; + } + posn = ddLCHash(key,hash->keysize,hash->shift); + item->next = hash->bucket[posn]; + hash->bucket[posn] = item; + + return(1); + +} /* end of cuddHashTableInsert */ + + +/**Function******************************************************************** + + Synopsis [Looks up a key in a hash table.] + + Description [Looks up a key consisting of more than three pointers + in a hash table. Returns the value associated to the key if there + is an entry for the given key in the table; NULL otherwise. If the + entry is present, its reference counter is decremented if not + saturated. If the counter reaches 0, the value of the entry is + dereferenced, and the entry is returned to the free list.] + + SideEffects [None] + + SeeAlso [cuddHashTableLookup1 cuddHashTableLookup2 cuddHashTableLookup3 + cuddHashTableInsert] + +******************************************************************************/ +DdNode * +cuddHashTableLookup( + DdHashTable * hash, + DdNodePtr * key) +{ + unsigned int posn; + DdHashItem *item, *prev; + unsigned int i, keysize; + +#ifdef DD_DEBUG + assert(hash->keysize > 3); +#endif + + posn = ddLCHash(key,hash->keysize,hash->shift); + item = hash->bucket[posn]; + prev = NULL; + + keysize = hash->keysize; + while (item != NULL) { + DdNodePtr *key2 = item->key; + int equal = 1; + for (i = 0; i < keysize; i++) { + if (key[i] != key2[i]) { + equal = 0; + break; + } + } + if (equal) { + DdNode *value = item->value; + cuddSatDec(item->count); + if (item->count == 0) { + cuddDeref(value); + if (prev == NULL) { + hash->bucket[posn] = item->next; + } else { + prev->next = item->next; + } + item->next = hash->nextFree; + hash->nextFree = item; + hash->size--; + } + return(value); + } + prev = item; + item = item->next; + } + return(NULL); + +} /* end of cuddHashTableLookup */ + + +/**Function******************************************************************** + + Synopsis [Inserts an item in a hash table.] + + Description [Inserts an item in a hash table when the key is one pointer. + Returns 1 if successful; 0 otherwise.] + + SideEffects [None] + + SeeAlso [cuddHashTableInsert cuddHashTableInsert2 cuddHashTableInsert3 + cuddHashTableLookup1] + +******************************************************************************/ +int +cuddHashTableInsert1( + DdHashTable * hash, + DdNode * f, + DdNode * value, + ptrint count) +{ + int result; + unsigned int posn; + DdHashItem *item; + +#ifdef DD_DEBUG + assert(hash->keysize == 1); +#endif + + if (hash->size > hash->maxsize) { + result = cuddHashTableResize(hash); + if (result == 0) return(0); + } + item = cuddHashTableAlloc(hash); + if (item == NULL) return(0); + hash->size++; + item->value = value; + cuddRef(value); + item->count = count; + item->key[0] = f; + posn = ddLCHash2(f,f,hash->shift); + item->next = hash->bucket[posn]; + hash->bucket[posn] = item; + + return(1); + +} /* end of cuddHashTableInsert1 */ + + +/**Function******************************************************************** + + Synopsis [Looks up a key consisting of one pointer in a hash table.] + + Description [Looks up a key consisting of one pointer in a hash table. + Returns the value associated to the key if there is an entry for the given + key in the table; NULL otherwise. If the entry is present, its reference + counter is decremented if not saturated. If the counter reaches 0, the + value of the entry is dereferenced, and the entry is returned to the free + list.] + + SideEffects [None] + + SeeAlso [cuddHashTableLookup cuddHashTableLookup2 cuddHashTableLookup3 + cuddHashTableInsert1] + +******************************************************************************/ +DdNode * +cuddHashTableLookup1( + DdHashTable * hash, + DdNode * f) +{ + unsigned int posn; + DdHashItem *item, *prev; + +#ifdef DD_DEBUG + assert(hash->keysize == 1); +#endif + + posn = ddLCHash2(f,f,hash->shift); + item = hash->bucket[posn]; + prev = NULL; + + while (item != NULL) { + DdNodePtr *key = item->key; + if (f == key[0]) { + DdNode *value = item->value; + cuddSatDec(item->count); + if (item->count == 0) { + cuddDeref(value); + if (prev == NULL) { + hash->bucket[posn] = item->next; + } else { + prev->next = item->next; + } + item->next = hash->nextFree; + hash->nextFree = item; + hash->size--; + } + return(value); + } + prev = item; + item = item->next; + } + return(NULL); + +} /* end of cuddHashTableLookup1 */ + + +/**Function******************************************************************** + + Synopsis [Inserts an item in a hash table.] + + Description [Inserts an item in a hash table when the key is + composed of two pointers. Returns 1 if successful; 0 otherwise.] + + SideEffects [None] + + SeeAlso [cuddHashTableInsert cuddHashTableInsert1 cuddHashTableInsert3 + cuddHashTableLookup2] + +******************************************************************************/ +int +cuddHashTableInsert2( + DdHashTable * hash, + DdNode * f, + DdNode * g, + DdNode * value, + ptrint count) +{ + int result; + unsigned int posn; + DdHashItem *item; + +#ifdef DD_DEBUG + assert(hash->keysize == 2); +#endif + + if (hash->size > hash->maxsize) { + result = cuddHashTableResize(hash); + if (result == 0) return(0); + } + item = cuddHashTableAlloc(hash); + if (item == NULL) return(0); + hash->size++; + item->value = value; + cuddRef(value); + item->count = count; + item->key[0] = f; + item->key[1] = g; + posn = ddLCHash2(f,g,hash->shift); + item->next = hash->bucket[posn]; + hash->bucket[posn] = item; + + return(1); + +} /* end of cuddHashTableInsert2 */ + + +/**Function******************************************************************** + + Synopsis [Looks up a key consisting of two pointers in a hash table.] + + Description [Looks up a key consisting of two pointer in a hash table. + Returns the value associated to the key if there is an entry for the given + key in the table; NULL otherwise. If the entry is present, its reference + counter is decremented if not saturated. If the counter reaches 0, the + value of the entry is dereferenced, and the entry is returned to the free + list.] + + SideEffects [None] + + SeeAlso [cuddHashTableLookup cuddHashTableLookup1 cuddHashTableLookup3 + cuddHashTableInsert2] + +******************************************************************************/ +DdNode * +cuddHashTableLookup2( + DdHashTable * hash, + DdNode * f, + DdNode * g) +{ + unsigned int posn; + DdHashItem *item, *prev; + +#ifdef DD_DEBUG + assert(hash->keysize == 2); +#endif + + posn = ddLCHash2(f,g,hash->shift); + item = hash->bucket[posn]; + prev = NULL; + + while (item != NULL) { + DdNodePtr *key = item->key; + if ((f == key[0]) && (g == key[1])) { + DdNode *value = item->value; + cuddSatDec(item->count); + if (item->count == 0) { + cuddDeref(value); + if (prev == NULL) { + hash->bucket[posn] = item->next; + } else { + prev->next = item->next; + } + item->next = hash->nextFree; + hash->nextFree = item; + hash->size--; + } + return(value); + } + prev = item; + item = item->next; + } + return(NULL); + +} /* end of cuddHashTableLookup2 */ + + +/**Function******************************************************************** + + Synopsis [Inserts an item in a hash table.] + + Description [Inserts an item in a hash table when the key is + composed of three pointers. Returns 1 if successful; 0 otherwise.] + + SideEffects [None] + + SeeAlso [cuddHashTableInsert cuddHashTableInsert1 cuddHashTableInsert2 + cuddHashTableLookup3] + +******************************************************************************/ +int +cuddHashTableInsert3( + DdHashTable * hash, + DdNode * f, + DdNode * g, + DdNode * h, + DdNode * value, + ptrint count) +{ + int result; + unsigned int posn; + DdHashItem *item; + +#ifdef DD_DEBUG + assert(hash->keysize == 3); +#endif + + if (hash->size > hash->maxsize) { + result = cuddHashTableResize(hash); + if (result == 0) return(0); + } + item = cuddHashTableAlloc(hash); + if (item == NULL) return(0); + hash->size++; + item->value = value; + cuddRef(value); + item->count = count; + item->key[0] = f; + item->key[1] = g; + item->key[2] = h; + posn = ddLCHash3(f,g,h,hash->shift); + item->next = hash->bucket[posn]; + hash->bucket[posn] = item; + + return(1); + +} /* end of cuddHashTableInsert3 */ + + +/**Function******************************************************************** + + Synopsis [Looks up a key consisting of three pointers in a hash table.] + + Description [Looks up a key consisting of three pointers in a hash table. + Returns the value associated to the key if there is an entry for the given + key in the table; NULL otherwise. If the entry is present, its reference + counter is decremented if not saturated. If the counter reaches 0, the + value of the entry is dereferenced, and the entry is returned to the free + list.] + + SideEffects [None] + + SeeAlso [cuddHashTableLookup cuddHashTableLookup1 cuddHashTableLookup2 + cuddHashTableInsert3] + +******************************************************************************/ +DdNode * +cuddHashTableLookup3( + DdHashTable * hash, + DdNode * f, + DdNode * g, + DdNode * h) +{ + unsigned int posn; + DdHashItem *item, *prev; + +#ifdef DD_DEBUG + assert(hash->keysize == 3); +#endif + + posn = ddLCHash3(f,g,h,hash->shift); + item = hash->bucket[posn]; + prev = NULL; + + while (item != NULL) { + DdNodePtr *key = item->key; + if ((f == key[0]) && (g == key[1]) && (h == key[2])) { + DdNode *value = item->value; + cuddSatDec(item->count); + if (item->count == 0) { + cuddDeref(value); + if (prev == NULL) { + hash->bucket[posn] = item->next; + } else { + prev->next = item->next; + } + item->next = hash->nextFree; + hash->nextFree = item; + hash->size--; + } + return(value); + } + prev = item; + item = item->next; + } + return(NULL); + +} /* end of cuddHashTableLookup3 */ + + +/*---------------------------------------------------------------------------*/ +/* Definition of static functions */ +/*---------------------------------------------------------------------------*/ + + +/**Function******************************************************************** + + Synopsis [Resizes a local cache.] + + Description [] + + SideEffects [None] + + SeeAlso [] + +******************************************************************************/ +static void +cuddLocalCacheResize( + DdLocalCache * cache) +{ + DdLocalCacheItem *item, *olditem, *entry, *old; + int i, shift; + unsigned int posn; + unsigned int slots, oldslots; + extern void (*MMoutOfMemory)(long); + void (*saveHandler)(long); + + olditem = cache->item; + oldslots = cache->slots; + slots = cache->slots = oldslots << 1; + +#ifdef DD_VERBOSE + (void) fprintf(cache->manager->err, + "Resizing local cache from %d to %d entries\n", + oldslots, slots); + (void) fprintf(cache->manager->err, + "\thits = %.0f\tlookups = %.0f\thit ratio = %5.3f\n", + cache->hits, cache->lookUps, cache->hits / cache->lookUps); +#endif + + saveHandler = MMoutOfMemory; + MMoutOfMemory = Cudd_OutOfMem; + cache->item = item = + (DdLocalCacheItem *) ALLOC(char, slots * cache->itemsize); + MMoutOfMemory = saveHandler; + /* If we fail to allocate the new table we just give up. */ + if (item == NULL) { +#ifdef DD_VERBOSE + (void) fprintf(cache->manager->err,"Resizing failed. Giving up.\n"); +#endif + cache->slots = oldslots; + cache->item = olditem; + /* Do not try to resize again. */ + cache->maxslots = oldslots - 1; + return; + } + shift = --(cache->shift); + cache->manager->memused += (slots - oldslots) * cache->itemsize; + + /* Clear new cache. */ + memset(item, 0, slots * cache->itemsize); + + /* Copy from old cache to new one. */ + for (i = 0; (unsigned) i < oldslots; i++) { + old = (DdLocalCacheItem *) ((char *) olditem + i * cache->itemsize); + if (old->value != NULL) { + posn = ddLCHash(old->key,cache->keysize,slots); + entry = (DdLocalCacheItem *) ((char *) item + + posn * cache->itemsize); + memcpy(entry->key,old->key,cache->keysize*sizeof(DdNode *)); + entry->value = old->value; + } + } + + FREE(olditem); + + /* Reinitialize measurements so as to avoid division by 0 and + ** immediate resizing. + */ + cache->lookUps = (double) (int) (slots * cache->minHit + 1); + cache->hits = 0; + +} /* end of cuddLocalCacheResize */ + + +/**Function******************************************************************** + + Synopsis [Computes the hash value for a local cache.] + + Description [Computes the hash value for a local cache. Returns the + bucket index.] + + SideEffects [None] + + SeeAlso [] + +******************************************************************************/ +DD_INLINE +static unsigned int +ddLCHash( + DdNodePtr * key, + unsigned int keysize, + int shift) +{ + unsigned int val = (unsigned int) (ptrint) key[0]; + unsigned int i; + + for (i = 1; i < keysize; i++) { + val = val * DD_P1 + (int) (ptrint) key[i]; + } + + return(val >> shift); + +} /* end of ddLCHash */ + + +/**Function******************************************************************** + + Synopsis [Inserts a local cache in the manager list.] + + Description [] + + SideEffects [None] + + SeeAlso [] + +******************************************************************************/ +static void +cuddLocalCacheAddToList( + DdLocalCache * cache) +{ + DdManager *manager = cache->manager; + + cache->next = manager->localCaches; + manager->localCaches = cache; + return; + +} /* end of cuddLocalCacheAddToList */ + + +/**Function******************************************************************** + + Synopsis [Removes a local cache from the manager list.] + + Description [] + + SideEffects [None] + + SeeAlso [] + +******************************************************************************/ +static void +cuddLocalCacheRemoveFromList( + DdLocalCache * cache) +{ + DdManager *manager = cache->manager; +#ifdef __osf__ +#pragma pointer_size save +#pragma pointer_size short +#endif + DdLocalCache **prevCache, *nextCache; +#ifdef __osf__ +#pragma pointer_size restore +#endif + + prevCache = &(manager->localCaches); + nextCache = manager->localCaches; + + while (nextCache != NULL) { + if (nextCache == cache) { + *prevCache = nextCache->next; + return; + } + prevCache = &(nextCache->next); + nextCache = nextCache->next; + } + return; /* should never get here */ + +} /* end of cuddLocalCacheRemoveFromList */ + + +/**Function******************************************************************** + + Synopsis [Resizes a hash table.] + + Description [Resizes a hash table. Returns 1 if successful; 0 + otherwise.] + + SideEffects [None] + + SeeAlso [cuddHashTableInsert] + +******************************************************************************/ +static int +cuddHashTableResize( + DdHashTable * hash) +{ + int j; + unsigned int posn; + DdHashItem *item; + DdHashItem *next; +#ifdef __osf__ +#pragma pointer_size save +#pragma pointer_size short +#endif + DdNode **key; + int numBuckets; + DdHashItem **buckets; + DdHashItem **oldBuckets = hash->bucket; +#ifdef __osf__ +#pragma pointer_size restore +#endif + int shift; + int oldNumBuckets = hash->numBuckets; + extern void (*MMoutOfMemory)(long); + void (*saveHandler)(long); + + /* Compute the new size of the table. */ + numBuckets = oldNumBuckets << 1; + saveHandler = MMoutOfMemory; + MMoutOfMemory = Cudd_OutOfMem; +#ifdef __osf__ +#pragma pointer_size save +#pragma pointer_size short +#endif + buckets = ALLOC(DdHashItem *, numBuckets); + MMoutOfMemory = saveHandler; + if (buckets == NULL) { + hash->maxsize <<= 1; + return(1); + } + + hash->bucket = buckets; + hash->numBuckets = numBuckets; + shift = --(hash->shift); + hash->maxsize <<= 1; + memset(buckets, 0, numBuckets * sizeof(DdHashItem *)); +#ifdef __osf__ +#pragma pointer_size restore +#endif + if (hash->keysize == 1) { + for (j = 0; j < oldNumBuckets; j++) { + item = oldBuckets[j]; + while (item != NULL) { + next = item->next; + key = item->key; + posn = ddLCHash2(key[0], key[0], shift); + item->next = buckets[posn]; + buckets[posn] = item; + item = next; + } + } + } else if (hash->keysize == 2) { + for (j = 0; j < oldNumBuckets; j++) { + item = oldBuckets[j]; + while (item != NULL) { + next = item->next; + key = item->key; + posn = ddLCHash2(key[0], key[1], shift); + item->next = buckets[posn]; + buckets[posn] = item; + item = next; + } + } + } else if (hash->keysize == 3) { + for (j = 0; j < oldNumBuckets; j++) { + item = oldBuckets[j]; + while (item != NULL) { + next = item->next; + key = item->key; + posn = ddLCHash3(key[0], key[1], key[2], shift); + item->next = buckets[posn]; + buckets[posn] = item; + item = next; + } + } + } else { + for (j = 0; j < oldNumBuckets; j++) { + item = oldBuckets[j]; + while (item != NULL) { + next = item->next; + posn = ddLCHash(item->key, hash->keysize, shift); + item->next = buckets[posn]; + buckets[posn] = item; + item = next; + } + } + } + FREE(oldBuckets); + return(1); + +} /* end of cuddHashTableResize */ + + +/**Function******************************************************************** + + Synopsis [Fast storage allocation for items in a hash table.] + + Description [Fast storage allocation for items in a hash table. The + first 4 bytes of a chunk contain a pointer to the next block; the + rest contains DD_MEM_CHUNK spaces for hash items. Returns a pointer to + a new item if successful; NULL is memory is full.] + + SideEffects [None] + + SeeAlso [cuddAllocNode cuddDynamicAllocNode] + +******************************************************************************/ +DD_INLINE +static DdHashItem * +cuddHashTableAlloc( + DdHashTable * hash) +{ + int i; + unsigned int itemsize = hash->itemsize; + extern void (*MMoutOfMemory)(long); + void (*saveHandler)(long); +#ifdef __osf__ +#pragma pointer_size save +#pragma pointer_size short +#endif + DdHashItem **mem, *thisOne, *next, *item; + + if (hash->nextFree == NULL) { + saveHandler = MMoutOfMemory; + MMoutOfMemory = Cudd_OutOfMem; + mem = (DdHashItem **) ALLOC(char,(DD_MEM_CHUNK+1) * itemsize); + MMoutOfMemory = saveHandler; +#ifdef __osf__ +#pragma pointer_size restore +#endif + if (mem == NULL) { + if (hash->manager->stash != NULL) { + FREE(hash->manager->stash); + hash->manager->stash = NULL; + /* Inhibit resizing of tables. */ + hash->manager->maxCacheHard = hash->manager->cacheSlots - 1; + hash->manager->cacheSlack = -(hash->manager->cacheSlots + 1); + for (i = 0; i < hash->manager->size; i++) { + hash->manager->subtables[i].maxKeys <<= 2; + } + hash->manager->gcFrac = 0.2; + hash->manager->minDead = + (unsigned) (0.2 * (double) hash->manager->slots); +#ifdef __osf__ +#pragma pointer_size save +#pragma pointer_size short +#endif + mem = (DdHashItem **) ALLOC(char,(DD_MEM_CHUNK+1) * itemsize); +#ifdef __osf__ +#pragma pointer_size restore +#endif + } + if (mem == NULL) { + (*MMoutOfMemory)((DD_MEM_CHUNK + 1) * itemsize); + hash->manager->errorCode = CUDD_MEMORY_OUT; + return(NULL); + } + } + + mem[0] = (DdHashItem *) hash->memoryList; + hash->memoryList = mem; + + thisOne = (DdHashItem *) ((char *) mem + itemsize); + hash->nextFree = thisOne; + for (i = 1; i < DD_MEM_CHUNK; i++) { + next = (DdHashItem *) ((char *) thisOne + itemsize); + thisOne->next = next; + thisOne = next; + } + + thisOne->next = NULL; + + } + item = hash->nextFree; + hash->nextFree = item->next; + return(item); + +} /* end of cuddHashTableAlloc */ -- cgit v1.2.3