summaryrefslogtreecommitdiffstats
path: root/src/bdd/cudd/cuddLCache.c
diff options
context:
space:
mode:
Diffstat (limited to 'src/bdd/cudd/cuddLCache.c')
-rw-r--r--src/bdd/cudd/cuddLCache.c1428
1 files changed, 0 insertions, 1428 deletions
diff --git a/src/bdd/cudd/cuddLCache.c b/src/bdd/cudd/cuddLCache.c
deleted file mode 100644
index 8bd37ba0..00000000
--- a/src/bdd/cudd/cuddLCache.c
+++ /dev/null
@@ -1,1428 +0,0 @@
-/**CFile***********************************************************************
-
- FileName [cuddLCache.c]
-
- PackageName [cudd]
-
- Synopsis [Functions for local caches.]
-
- Description [Internal procedures included in this module:
- <ul>
- <li> cuddLocalCacheInit()
- <li> cuddLocalCacheQuit()
- <li> cuddLocalCacheInsert()
- <li> cuddLocalCacheLookup()
- <li> cuddLocalCacheClearDead()
- <li> cuddLocalCacheClearAll()
- <li> cuddLocalCacheProfile()
- <li> cuddHashTableInit()
- <li> cuddHashTableQuit()
- <li> cuddHashTableInsert()
- <li> cuddHashTableLookup()
- <li> cuddHashTableInsert2()
- <li> cuddHashTableLookup2()
- <li> cuddHashTableInsert3()
- <li> cuddHashTableLookup3()
- </ul>
- Static procedures included in this module:
- <ul>
- <li> cuddLocalCacheResize()
- <li> ddLCHash()
- <li> cuddLocalCacheAddToList()
- <li> cuddLocalCacheRemoveFromList()
- <li> cuddHashTableResize()
- <li> cuddHashTableAlloc()
- </ul> ]
-
- SeeAlso []
-
- Author [Fabio Somenzi]
-
- Copyright [ This file was created at the University of Colorado at
- Boulder. The University of Colorado at Boulder makes no warranty
- about the suitability of this software for any purpose. It is
- presented on an AS IS basis.]
-
-******************************************************************************/
-
-#include "util_hack.h"
-#include "cuddInt.h"
-
-/*---------------------------------------------------------------------------*/
-/* Constant declarations */
-/*---------------------------------------------------------------------------*/
-
-#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 */
generated by cgit v1.2.3 (git 2.25.1) at 2024-08-27 05:43:59 +0000