cuddLCache.c File Reference

#include "CUDD/util.h"
#include "CUDD/cuddInt.h"

Go to the source code of this file.

Macros
#define	DD_MAX_HASHTABLE_DENSITY   2 /* tells when to resize a table */
#define	ddLCHash1(f, shift)   (((unsigned)(f) * DD_P1) >> (shift))
#define	ddLCHash2(f, g, shift)   ((((unsigned)(f) * DD_P1 + (unsigned)(g)) * DD_P2) >> (shift))
#define	ddLCHash3(f, g, h, shift)   ddCHash2(f,g,h,shift)

Functions
static void	cuddLocalCacheResize (DdLocalCache *cache)
static DD_INLINE 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)
static DD_INLINE DdHashItem *	cuddHashTableAlloc (DdHashTable *hash)
DdLocalCache *	cuddLocalCacheInit (DdManager *manager, unsigned int keySize, unsigned int cacheSize, unsigned int maxCacheSize)
void	cuddLocalCacheQuit (DdLocalCache *cache)
void	cuddLocalCacheInsert (DdLocalCache *cache, DdNodePtr *key, DdNode *value)
DdNode *	cuddLocalCacheLookup (DdLocalCache *cache, DdNodePtr *key)
void	cuddLocalCacheClearDead (DdManager *manager)
void	cuddLocalCacheClearAll (DdManager *manager)
DdHashTable *	cuddHashTableInit (DdManager *manager, unsigned int keySize, unsigned int initSize)
void	cuddHashTableQuit (DdHashTable *hash)
void	cuddHashTableGenericQuit (DdHashTable *hash)
int	cuddHashTableInsert (DdHashTable *hash, DdNodePtr *key, DdNode *value, ptrint count)
DdNode *	cuddHashTableLookup (DdHashTable *hash, DdNodePtr *key)
int	cuddHashTableInsert1 (DdHashTable *hash, DdNode *f, DdNode *value, ptrint count)
DdNode *	cuddHashTableLookup1 (DdHashTable *hash, DdNode *f)
int	cuddHashTableGenericInsert (DdHashTable *hash, DdNode *f, void *value)
void *	cuddHashTableGenericLookup (DdHashTable *hash, DdNode *f)
int	cuddHashTableInsert2 (DdHashTable *hash, DdNode *f, DdNode *g, DdNode *value, ptrint count)
DdNode *	cuddHashTableLookup2 (DdHashTable *hash, DdNode *f, DdNode *g)
int	cuddHashTableInsert3 (DdHashTable *hash, DdNode *f, DdNode *g, DdNode *h, DdNode *value, ptrint count)
DdNode *	cuddHashTableLookup3 (DdHashTable *hash, DdNode *f, DdNode *g, DdNode *h)

Variables
static char rcsid []	DD_UNUSED = "$Id: cuddLCache.c,v 1.27 2012/02/05 01:07:19 fabio Exp $"

Macro Definition Documentation

DD_MAX_HASHTABLE_DENSITY

#define DD_MAX_HASHTABLE_DENSITY   2 /* tells when to resize a table */

CFile***********************************************************************

FileName [cuddLCache.c]

PackageName [cudd]

Synopsis [Functions for local caches.]

Description [Internal procedures included in this module:

• cuddLocalCacheInit()
• cuddLocalCacheQuit()
• cuddLocalCacheInsert()
• cuddLocalCacheLookup()
• cuddLocalCacheClearDead()
• cuddLocalCacheClearAll()
• cuddLocalCacheProfile()
• cuddHashTableInit()
• cuddHashTableQuit()
• cuddHashTableGenericQuit()
• cuddHashTableInsert()
• cuddHashTableLookup()
• cuddHashTableGenericInsert()
• cuddHashTableGenericLookup()
• cuddHashTableInsert2()
• cuddHashTableLookup2()
• cuddHashTableInsert3()
• cuddHashTableLookup3()

Static procedures included in this module:

• cuddLocalCacheResize()
• ddLCHash()
• cuddLocalCacheAddToList()
• cuddLocalCacheRemoveFromList()
• cuddHashTableResize()
• cuddHashTableAlloc()

]

SeeAlso []

Author [Fabio Somenzi]

Copyright [Copyright (c) 1995-2012, 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.]

Definition at line 85 of file cuddLCache.c.

ddLCHash1

#define ddLCHash1	(		f,
			shift
	)		(((unsigned)(f) * DD_P1) >> (shift))

Macro***********************************************************************

Synopsis [Computes hash function for keys of one operand.]

Description []

SideEffects [None]

SeeAlso [ddLCHash3 ddLCHash]

Definition at line 124 of file cuddLCache.c.

ddLCHash2

#define ddLCHash2	(		f,
			g,
			shift
	)		((((unsigned)(f) * DD_P1 + (unsigned)(g)) * DD_P2) >> (shift))

Macro***********************************************************************

Synopsis [Computes hash function for keys of two operands.]

Description []

SideEffects [None]

SeeAlso [ddLCHash3 ddLCHash]

Definition at line 145 of file cuddLCache.c.

ddLCHash3

#define ddLCHash3	(		f,
			g,
			h,
			shift
	)		ddCHash2(f,g,h,shift)

Macro***********************************************************************

Synopsis [Computes hash function for keys of three operands.]

Description []

SideEffects [None]

SeeAlso [ddLCHash2 ddLCHash]

Definition at line 161 of file cuddLCache.c.

Function Documentation

cuddHashTableAlloc()

static DD_INLINE DdHashItem * cuddHashTableAlloc ( DdHashTable *  hash )

static

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]

Definition at line 1503 of file cuddLCache.c.

{
    int i;
    unsigned int itemsize = hash->itemsize;
    extern DD_OOMFP MMoutOfMemory;
    DD_OOMFP saveHandler;
    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;
    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 = - (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);
        mem = (DdHashItem **) ALLOC(char,(DD_MEM_CHUNK+1) * itemsize);
        }
        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 */

cuddHashTableGenericInsert()

int cuddHashTableGenericInsert	(	DdHashTable *	hash,
		DdNode *	f,
		void *	value
	)

Function********************************************************************

Synopsis [Inserts an item in a hash table.]

Description [Inserts an item in a hash table when the key is one pointer and the value is not a DdNode pointer. Returns 1 if successful; 0 otherwise.]

SideEffects [None]

SeeAlso [cuddHashTableInsert1 cuddHashTableGenericLookup]

Definition at line 919 of file cuddLCache.c.

{
    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 = (DdNode *) value;
    item->count = 0;
    item->key[0] = f;
    posn = ddLCHash1(f,hash->shift);
    item->next = hash->bucket[posn];
    hash->bucket[posn] = item;

    return(1);

} /* end of cuddHashTableGenericInsert */

cuddHashTableGenericLookup()

void* cuddHashTableGenericLookup	(	DdHashTable *	hash,
		DdNode *	f
	)

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 when the value is not a DdNode pointer. Returns the value associated to the key if there is an entry for the given key in the table; NULL otherwise.]

SideEffects [None]

SeeAlso [cuddHashTableLookup1 cuddHashTableGenericInsert]

Definition at line 966 of file cuddLCache.c.

{
    unsigned int posn;
    DdHashItem *item;

#ifdef DD_DEBUG
    assert(hash->keysize == 1);
#endif

    posn = ddLCHash1(f,hash->shift);
    item = hash->bucket[posn];

    while (item != NULL) {
    if (f == item->key[0]) {
            return ((void *) item->value);
    }
    item = item->next;
    }
    return(NULL);

} /* end of cuddHashTableGenericLookup */

cuddHashTableGenericQuit()

void cuddHashTableGenericQuit

(

DdHashTable *

hash

)

Function********************************************************************

Synopsis [Shuts down a hash table.]

Description [Shuts down a hash table, when the values are not DdNode pointers.]

SideEffects [None]

SeeAlso [cuddHashTableInit]

Definition at line 652 of file cuddLCache.c.

{
#ifdef __osf__
#pragma pointer_size save
#pragma pointer_size short
#endif
    DdHashItem **memlist, **nextmem;

    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 cuddHashTableGenericQuit */

cuddHashTableInit()

DdHashTable* cuddHashTableInit	(	DdManager *	manager,
		unsigned int	keySize,
		unsigned int	initSize
	)

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]

Definition at line 557 of file cuddLCache.c.

{
    DdHashTable *hash;
    int logSize;

    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;
    return(hash);

} /* end of cuddHashTableInit */

cuddHashTableInsert()

int cuddHashTableInsert	(	DdHashTable *	hash,
		DdNodePtr *	key,
		DdNode *	value,
		ptrint	count
	)

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]

Definition at line 693 of file cuddLCache.c.

{
    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 */

cuddHashTableInsert1()

int cuddHashTableInsert1	(	DdHashTable *	hash,
		DdNode *	f,
		DdNode *	value,
		ptrint	count
	)

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]

Definition at line 812 of file cuddLCache.c.

{
    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 = ddLCHash1(f,hash->shift);
    item->next = hash->bucket[posn];
    hash->bucket[posn] = item;

    return(1);

} /* end of cuddHashTableInsert1 */

cuddHashTableInsert2()

int cuddHashTableInsert2	(	DdHashTable *	hash,
		DdNode *	f,
		DdNode *	g,
		DdNode *	value,
		ptrint	count
	)

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]

Definition at line 1005 of file cuddLCache.c.

{
    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 */

cuddHashTableInsert3()

int cuddHashTableInsert3	(	DdHashTable *	hash,
		DdNode *	f,
		DdNode *	g,
		DdNode *	h,
		DdNode *	value,
		ptrint	count
	)

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]

Definition at line 1115 of file cuddLCache.c.

{
    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 */

cuddHashTableLookup()

DdNode* cuddHashTableLookup	(	DdHashTable *	hash,
		DdNodePtr *	key
	)

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]

Definition at line 748 of file cuddLCache.c.

{
    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 */

cuddHashTableLookup1()

DdNode* cuddHashTableLookup1	(	DdHashTable *	hash,
		DdNode *	f
	)

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]

Definition at line 864 of file cuddLCache.c.

{
    unsigned int posn;
    DdHashItem *item, *prev;

#ifdef DD_DEBUG
    assert(hash->keysize == 1);
#endif

    posn = ddLCHash1(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 */

cuddHashTableLookup2()

DdNode* cuddHashTableLookup2	(	DdHashTable *	hash,
		DdNode *	f,
		DdNode *	g
	)

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]

Definition at line 1059 of file cuddLCache.c.

{
    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 */

cuddHashTableLookup3()

DdNode* cuddHashTableLookup3	(	DdHashTable *	hash,
		DdNode *	f,
		DdNode *	g,
		DdNode *	h
	)

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]

Definition at line 1171 of file cuddLCache.c.

{
    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 */

cuddHashTableQuit()

void cuddHashTableQuit

(

DdHashTable *

hash

)

Function********************************************************************

Synopsis [Shuts down a hash table.]

Description [Shuts down a hash table, dereferencing all the values.]

SideEffects [None]

SeeAlso [cuddHashTableInit]

Definition at line 607 of file cuddLCache.c.

{
    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);

    return;

} /* end of cuddHashTableQuit */

cuddHashTableResize()

static int cuddHashTableResize ( DdHashTable *  hash )

static

Function********************************************************************

Synopsis [Resizes a hash table.]

Description [Resizes a hash table. Returns 1 if successful; 0 otherwise.]

SideEffects [None]

SeeAlso [cuddHashTableInsert]

Definition at line 1401 of file cuddLCache.c.

{
    int j;
    unsigned int posn;
    DdHashItem *item;
    DdHashItem *next;
    DdNode **key;
    int numBuckets;
    DdHashItem **buckets;
    DdHashItem **oldBuckets = hash->bucket;
    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;
    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 *));
    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 */

cuddLocalCacheAddToList()

static void cuddLocalCacheAddToList ( DdLocalCache *  cache )

static

Function********************************************************************

Synopsis [Inserts a local cache in the manager list.]

Description []

SideEffects [None]

SeeAlso []

Definition at line 1342 of file cuddLCache.c.

{
    DdManager *manager = cache->manager;

    cache->next = manager->localCaches;
    manager->localCaches = cache;
    return;

} /* end of cuddLocalCacheAddToList */

cuddLocalCacheClearAll()

void cuddLocalCacheClearAll

(

DdManager *

manager

)

Function********************************************************************

Synopsis [Clears the local caches of a manager.]

Description [Clears the local caches of a manager. Used before reordering.]

SideEffects [None]

SeeAlso []

Definition at line 423 of file cuddLCache.c.

{
    DdLocalCache *cache = manager->localCaches;

    while (cache != NULL) {
    memset(cache->item, 0, cache->slots * cache->itemsize);
    cache = cache->next;
    }
    return;

} /* end of cuddLocalCacheClearAll */

cuddLocalCacheClearDead()

void cuddLocalCacheClearDead

(

DdManager *

manager

)

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 []

Definition at line 371 of file cuddLCache.c.

{
    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 */

cuddLocalCacheInit()

DdLocalCache* cuddLocalCacheInit	(	DdManager *	manager,
		unsigned int	keySize,
		unsigned int	cacheSize,
		unsigned int	maxCacheSize
	)

AutomaticEnd 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]

Definition at line 202 of file cuddLCache.c.

{
    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 */

cuddLocalCacheInsert()

void cuddLocalCacheInsert	(	DdLocalCache *	cache,
		DdNodePtr *	key,
		DdNode *	value
	)

Function********************************************************************

Synopsis [Inserts a result in a local cache.]

Description []

SideEffects [None]

SeeAlso []

Definition at line 291 of file cuddLCache.c.

{
    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 */

cuddLocalCacheLookup()

DdNode* cuddLocalCacheLookup	(	DdLocalCache *	cache,
		DdNodePtr *	key
	)

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 []

Definition at line 324 of file cuddLCache.c.

{
    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 */

cuddLocalCacheQuit()

void cuddLocalCacheQuit

(

DdLocalCache *

cache

)

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]

Definition at line 265 of file cuddLCache.c.

{
    cache->manager->memused -=
    cache->slots * cache->itemsize + sizeof(DdLocalCache);
    cuddLocalCacheRemoveFromList(cache);
    FREE(cache->item);
    FREE(cache);

    return;

} /* end of cuddLocalCacheQuit */

cuddLocalCacheRemoveFromList()

static void cuddLocalCacheRemoveFromList ( DdLocalCache *  cache )

static

Function********************************************************************

Synopsis [Removes a local cache from the manager list.]

Description []

SideEffects [None]

SeeAlso []

Definition at line 1366 of file cuddLCache.c.

{
    DdManager *manager = cache->manager;
    DdLocalCache **prevCache, *nextCache;

    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 */

cuddLocalCacheResize()

static void cuddLocalCacheResize ( DdLocalCache *  cache )

static

AutomaticStart

Function********************************************************************

Synopsis [Resizes a local cache.]

Description []

SideEffects [None]

SeeAlso []

Definition at line 1231 of file cuddLCache.c.

{
    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 *) 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;
    }
    }

    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 */

ddLCHash()

static DD_INLINE unsigned int ddLCHash ( DdNodePtr *  key, unsigned int  keysize, int  shift  )

static

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 []

Definition at line 1313 of file cuddLCache.c.

{
    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 */

Variable Documentation

DD_UNUSED

char rcsid [] DD_UNUSED = "$Id: cuddLCache.c,v 1.27 2012/02/05 01:07:19 fabio Exp $"

static

Definition at line 102 of file cuddLCache.c.