/**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   [Copyright (c) 1995-2004, Regents of the University of Colorado

  All rights reserved.

  Redistribution and use in source and binary forms, with or without
  modification, are permitted provided that the following conditions
  are met:

  Redistributions of source code must retain the above copyright
  notice, this list of conditions and the following disclaimer.

  Redistributions in binary form must reproduce the above copyright
  notice, this list of conditions and the following disclaimer in the
  documentation and/or other materials provided with the distribution.

  Neither the name of the University of Colorado nor the names of its
  contributors may be used to endorse or promote products derived from
  this software without specific prior written permission.

  THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS
  "AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT
  LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS
  FOR A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE
  COPYRIGHT OWNER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT,
  INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING,
  BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES;
  LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER
  CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT
  LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN
  ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE
  POSSIBILITY OF SUCH DAMAGE.]

******************************************************************************/

#include "misc/util/util_hack.h"
#include "cuddInt.h"

ABC_NAMESPACE_IMPL_START


/*---------------------------------------------------------------------------*/
/* 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.24 2009/03/08 02:49:02 fabio 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)(ptruint)(f) * DD_P1 + \
   (unsigned)(ptruint)(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 (DdLocalCache *cache);
DD_INLINE static unsigned int ddLCHash (DdNodePtr *key, unsigned int keysize, int shift);
static void cuddLocalCacheAddToList (DdLocalCache *cache);
static void cuddLocalCacheRemoveFromList (DdLocalCache *cache);
static int cuddHashTableResize (DdHashTable *hash);
DD_INLINE static DdHashItem * cuddHashTableAlloc (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 = ABC_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 *)
        ABC_ALLOC(char, cacheSize * cache->itemsize);
    if (cache->item == NULL) {
        manager->errorCode = CUDD_MEMORY_OUT;
        ABC_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);
    ABC_FREE(cache->item);
    ABC_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) {
                if (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 = ABC_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);
    }

    ABC_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 = ABC_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 = ABC_ALLOC(DdHashItem *, hash->numBuckets);
    if (hash->bucket == NULL) {
        manager->errorCode = CUDD_MEMORY_OUT;
        ABC_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];
        ABC_FREE(memlist);
        memlist = nextmem;
    }

    ABC_FREE(hash->bucket);
    ABC_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(cuddF2L(f),cuddF2L(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(cuddF2L(f),cuddF2L(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(cuddF2L(f),cuddF2L(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(cuddF2L(f),cuddF2L(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(cuddF2L(f),cuddF2L(g),cuddF2L(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(cuddF2L(f),cuddF2L(g),cuddF2L(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 DD_OOMFP MMoutOfMemory;
    DD_OOMFP saveHandler;

    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 *) ABC_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,shift);
            entry = (DdLocalCacheItem *) ((char *) item +
                                          posn * cache->itemsize);
            memcpy(entry->key,old->key,cache->keysize*sizeof(DdNode *));
            entry->value = old->value;
        }
    }

    ABC_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] * DD_P2;
    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 DD_OOMFP MMoutOfMemory;
    DD_OOMFP saveHandler;

    /* 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 = ABC_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(cuddF2L(key[0]), cuddF2L(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(cuddF2L(key[0]), cuddF2L(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(cuddF2L(key[0]), cuddF2L(key[1]), cuddF2L(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;
            }
        }
    }
    ABC_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 DD_OOMFP MMoutOfMemory;
    DD_OOMFP saveHandler;
#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 **) ABC_ALLOC(char,(DD_MEM_CHUNK+1) * itemsize);
        MMoutOfMemory = saveHandler;
#ifdef __osf__
#pragma pointer_size restore
#endif
        if (mem == NULL) {
            if (hash->manager->stash != NULL) {
                ABC_FREE(hash->manager->stash);
                hash->manager->stash = NULL;
                /* Inhibit resizing of tables. */
                hash->manager->maxCacheHard = hash->manager->cacheSlots - 1;
                hash->manager->cacheSlack = - (int) (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 **) ABC_ALLOC(char,(DD_MEM_CHUNK+1) * itemsize);
#ifdef __osf__
#pragma pointer_size restore
#endif
            }
            if (mem == NULL) {
                (*MMoutOfMemory)((long)((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 */


ABC_NAMESPACE_IMPL_END