Version abc50729

1 files changed, 1428 insertions, 0 deletions

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:
+        <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.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 */