src/cuBdd/cuddLevelQ.c

Go to the documentation of this file.

#include "util.h"
#include "cuddInt.h"

/*---------------------------------------------------------------------------*/
/* Constant declarations                                                     */
/*---------------------------------------------------------------------------*/


/*---------------------------------------------------------------------------*/
/* Stucture declarations                                                     */
/*---------------------------------------------------------------------------*/

/*---------------------------------------------------------------------------*/
/* Type declarations                                                         */
/*---------------------------------------------------------------------------*/

/*---------------------------------------------------------------------------*/
/* Variable declarations                                                     */
/*---------------------------------------------------------------------------*/

#ifndef lint
static char rcsid[] DD_UNUSED = "$Id: cuddLevelQ.c,v 1.13 2009/03/08 02:49:02 fabio Exp $";
#endif

/*---------------------------------------------------------------------------*/
/* Macro declarations                                                        */
/*---------------------------------------------------------------------------*/


#if SIZEOF_VOID_P == 8 && SIZEOF_INT == 4
#define lqHash(key,shift) \
(((unsigned)(ptruint)(key) * DD_P1) >> (shift))
#else
#define lqHash(key,shift) \
(((unsigned)(key) * DD_P1) >> (shift))
#endif


/*---------------------------------------------------------------------------*/
/* Static function prototypes                                                */
/*---------------------------------------------------------------------------*/

static DdQueueItem * hashLookup (DdLevelQueue *queue, void *key);
static int hashInsert (DdLevelQueue *queue, DdQueueItem *item);
static void hashDelete (DdLevelQueue *queue, DdQueueItem *item);
static int hashResize (DdLevelQueue *queue);

/*---------------------------------------------------------------------------*/
/* Definition of internal functions                                          */
/*---------------------------------------------------------------------------*/


DdLevelQueue *
cuddLevelQueueInit(
  int  levels /* number of levels */,
  int  itemSize /* size of the item */,
  int  numBuckets /* initial number of hash buckets */)
{
    DdLevelQueue *queue;
    int logSize;

    queue = ALLOC(DdLevelQueue,1);
    if (queue == NULL)
        return(NULL);
#ifdef __osf__
#pragma pointer_size save
#pragma pointer_size short
#endif
    /* Keep pointers to the insertion points for all levels. */
    queue->last = ALLOC(DdQueueItem *, levels);
#ifdef __osf__
#pragma pointer_size restore
#endif
    if (queue->last == NULL) {
        FREE(queue);
        return(NULL);
    }
    /* Use a hash table to test for uniqueness. */
    if (numBuckets < 2) numBuckets = 2;
    logSize = cuddComputeFloorLog2(numBuckets);
    queue->numBuckets = 1 << logSize;
    queue->shift = sizeof(int) * 8 - logSize;
#ifdef __osf__
#pragma pointer_size save
#pragma pointer_size short
#endif
    queue->buckets = ALLOC(DdQueueItem *, queue->numBuckets);
#ifdef __osf__
#pragma pointer_size restore
#endif
    if (queue->buckets == NULL) {
        FREE(queue->last);
        FREE(queue);
        return(NULL);
    }
#ifdef __osf__
#pragma pointer_size save
#pragma pointer_size short
#endif
    memset(queue->last, 0, levels * sizeof(DdQueueItem *));
    memset(queue->buckets, 0, queue->numBuckets * sizeof(DdQueueItem *));
#ifdef __osf__
#pragma pointer_size restore
#endif
    queue->first = NULL;
    queue->freelist = NULL;
    queue->levels = levels;
    queue->itemsize = itemSize;
    queue->size = 0;
    queue->maxsize = queue->numBuckets * DD_MAX_SUBTABLE_DENSITY;
    return(queue);

} /* end of cuddLevelQueueInit */


void
cuddLevelQueueQuit(
  DdLevelQueue * queue)
{
    DdQueueItem *item;

    while (queue->freelist != NULL) {
        item = queue->freelist;
        queue->freelist = item->next;
        FREE(item);
    }
    while (queue->first != NULL) {
        item = (DdQueueItem *) queue->first;
        queue->first = item->next;
        FREE(item);
    }
    FREE(queue->buckets);
    FREE(queue->last);
    FREE(queue);
    return;

} /* end of cuddLevelQueueQuit */


void *
cuddLevelQueueEnqueue(
  DdLevelQueue * queue /* level queue */,
  void * key /* key to be enqueued */,
  int  level /* level at which to insert */)
{
    int plevel;
    DdQueueItem *item;

#ifdef DD_DEBUG
    assert(level < queue->levels);
#endif
    /* Check whether entry for this node exists. */
    item = hashLookup(queue,key);
    if (item != NULL) return(item);

    /* Get a free item from either the free list or the memory manager. */
    if (queue->freelist == NULL) {
        item = (DdQueueItem *) ALLOC(char, queue->itemsize);
        if (item == NULL)
            return(NULL);
    } else {
        item = queue->freelist;
        queue->freelist = item->next;
    }
    /* Initialize. */
    memset(item, 0, queue->itemsize);
    item->key = key;
    /* Update stats. */
    queue->size++;

    if (queue->last[level]) {
        /* There are already items for this level in the queue. */
        item->next = queue->last[level]->next;
        queue->last[level]->next = item;
    } else {
        /* There are no items at the current level.  Look for the first
        ** non-empty level preceeding this one. */
        plevel = level;
        while (plevel != 0 && queue->last[plevel] == NULL)
            plevel--;
        if (queue->last[plevel] == NULL) {
            /* No element precedes this one in the queue. */
            item->next = (DdQueueItem *) queue->first;
            queue->first = item;
        } else {
            item->next = queue->last[plevel]->next;
            queue->last[plevel]->next = item;
        }
    }
    queue->last[level] = item;

    /* Insert entry for the key in the hash table. */
    if (hashInsert(queue,item) == 0) {
        return(NULL);
    }
    return(item);

} /* end of cuddLevelQueueEnqueue */


void
cuddLevelQueueDequeue(
  DdLevelQueue * queue,
  int  level)
{
    DdQueueItem *item = (DdQueueItem *) queue->first;

    /* Delete from the hash table. */
    hashDelete(queue,item);

    /* Since we delete from the front, if this is the last item for
    ** its level, there are no other items for the same level. */
    if (queue->last[level] == item)
        queue->last[level] = NULL;

    queue->first = item->next;
    /* Put item on the free list. */
    item->next = queue->freelist;
    queue->freelist = item;
    /* Update stats. */
    queue->size--;
    return;

} /* end of cuddLevelQueueDequeue */


/*---------------------------------------------------------------------------*/
/* Definition of static functions                                            */
/*---------------------------------------------------------------------------*/


static DdQueueItem *
hashLookup(
  DdLevelQueue * queue,
  void * key)
{
    int posn;
    DdQueueItem *item;

    posn = lqHash(key,queue->shift);
    item = queue->buckets[posn];

    while (item != NULL) {
        if (item->key == key) {
            return(item);
        }
        item = item->cnext;
    }
    return(NULL);

} /* end of hashLookup */


static int
hashInsert(
  DdLevelQueue * queue,
  DdQueueItem * item)
{
    int result;
    int posn;

    if (queue->size > queue->maxsize) {
        result = hashResize(queue);
        if (result == 0) return(0);
    }

    posn = lqHash(item->key,queue->shift);
    item->cnext = queue->buckets[posn];
    queue->buckets[posn] = item;

    return(1);
    
} /* end of hashInsert */


static void
hashDelete(
  DdLevelQueue * queue,
  DdQueueItem * item)
{
    int posn;
    DdQueueItem *prevItem;

    posn = lqHash(item->key,queue->shift);
    prevItem = queue->buckets[posn];

    if (prevItem == NULL) return;
    if (prevItem == item) {
        queue->buckets[posn] = prevItem->cnext;
        return;
    }

    while (prevItem->cnext != NULL) {
        if (prevItem->cnext == item) {
            prevItem->cnext = item->cnext;
            return;
        }
        prevItem = prevItem->cnext;
    }
    return;

} /* end of hashDelete */


static int
hashResize(
  DdLevelQueue * queue)
{
    int j;
    int posn;
    DdQueueItem *item;
    DdQueueItem *next;
    int numBuckets;
#ifdef __osf__
#pragma pointer_size save
#pragma pointer_size short
#endif
    DdQueueItem **buckets;
    DdQueueItem **oldBuckets = queue->buckets;
#ifdef __osf__
#pragma pointer_size restore
#endif
    int shift;
    int oldNumBuckets = queue->numBuckets;
    extern DD_OOMFP MMoutOfMemory;
    DD_OOMFP saveHandler;

    /* Compute the new size of the subtable. */
    numBuckets = oldNumBuckets << 1;
    saveHandler = MMoutOfMemory;
    MMoutOfMemory = Cudd_OutOfMem;
#ifdef __osf__
#pragma pointer_size save
#pragma pointer_size short
#endif
    buckets = queue->buckets = ALLOC(DdQueueItem *, numBuckets);
    MMoutOfMemory = saveHandler;
    if (buckets == NULL) {
        queue->maxsize <<= 1;
        return(1);
    }

    queue->numBuckets = numBuckets;
    shift = --(queue->shift);
    queue->maxsize <<= 1;
    memset(buckets, 0, numBuckets * sizeof(DdQueueItem *));
#ifdef __osf__
#pragma pointer_size restore
#endif
    for (j = 0; j < oldNumBuckets; j++) {
        item = oldBuckets[j];
        while (item != NULL) {
            next = item->cnext;
            posn = lqHash(item->key, shift);
            item->cnext = buckets[posn];
            buckets[posn] = item;
            item = next;
        }
    }
    FREE(oldBuckets);
    return(1);

} /* end of hashResize */

---