diff options
Diffstat (limited to 'src/bdd/cudd/cuddLevelQ.c')
-rw-r--r-- | src/bdd/cudd/cuddLevelQ.c | 533 |
1 files changed, 533 insertions, 0 deletions
diff --git a/src/bdd/cudd/cuddLevelQ.c b/src/bdd/cudd/cuddLevelQ.c new file mode 100644 index 00000000..3cc8e8d8 --- /dev/null +++ b/src/bdd/cudd/cuddLevelQ.c @@ -0,0 +1,533 @@ +/**CFile*********************************************************************** + + FileName [cuddLevelQ.c] + + PackageName [cudd] + + Synopsis [Procedure to manage level queues.] + + Description [The functions in this file allow an application to + easily manipulate a queue where nodes are prioritized by level. The + emphasis is on efficiency. Therefore, the queue items can have + variable size. If the application does not need to attach + information to the nodes, it can declare the queue items to be of + type DdQueueItem. Otherwise, it can declare them to be of a + structure type such that the first three fields are data + pointers. The third pointer points to the node. The first two + pointers are used by the level queue functions. The remaining fields + are initialized to 0 when a new item is created, and are then left + to the exclusive use of the application. On the DEC Alphas the three + pointers must be 32-bit pointers when CUDD is compiled with 32-bit + pointers. The level queue functions make sure that each node + appears at most once in the queue. They do so by keeping a hash + table where the node is used as key. Queue items are recycled via a + free list for efficiency. + + Internal procedures provided by this module: + <ul> + <li> cuddLevelQueueInit() + <li> cuddLevelQueueQuit() + <li> cuddLevelQueueEnqueue() + <li> cuddLevelQueueDequeue() + </ul> + Static procedures included in this module: + <ul> + <li> hashLookup() + <li> hashInsert() + <li> hashDelete() + <li> hashResize() + </ul> + ] + + SeeAlso [] + + Author [Fabio Somenzi] + + Copyright [This file was created at the University of Colorado at + Boulder. The University of Colorado at Boulder makes no + warranty about the suitability of this software for any + purpose. It is presented on an AS IS basis.] + +******************************************************************************/ + +#include "util_hack.h" +#include "cuddInt.h" + +/*---------------------------------------------------------------------------*/ +/* Constant declarations */ +/*---------------------------------------------------------------------------*/ + + +/*---------------------------------------------------------------------------*/ +/* Stucture declarations */ +/*---------------------------------------------------------------------------*/ + +/*---------------------------------------------------------------------------*/ +/* Type declarations */ +/*---------------------------------------------------------------------------*/ + +/*---------------------------------------------------------------------------*/ +/* Variable declarations */ +/*---------------------------------------------------------------------------*/ + +#ifndef lint +static char rcsid[] DD_UNUSED = "$Id: cuddLevelQ.c,v 1.1.1.1 2003/02/24 22:23:52 wjiang Exp $"; +#endif + +/*---------------------------------------------------------------------------*/ +/* Macro declarations */ +/*---------------------------------------------------------------------------*/ + + +/**Macro*********************************************************************** + + Synopsis [Hash function for the table of a level queue.] + + Description [Hash function for the table of a level queue.] + + SideEffects [None] + + SeeAlso [hashInsert hashLookup hashDelete] + +******************************************************************************/ +#if SIZEOF_VOID_P == 8 && SIZEOF_INT == 4 +#define lqHash(key,shift) \ +(((unsigned)(unsigned long)(key) * DD_P1) >> (shift)) +#else +#define lqHash(key,shift) \ +(((unsigned)(key) * DD_P1) >> (shift)) +#endif + + +/**AutomaticStart*************************************************************/ + +/*---------------------------------------------------------------------------*/ +/* Static function prototypes */ +/*---------------------------------------------------------------------------*/ + +static DdQueueItem * hashLookup ARGS((DdLevelQueue *queue, void *key)); +static int hashInsert ARGS((DdLevelQueue *queue, DdQueueItem *item)); +static void hashDelete ARGS((DdLevelQueue *queue, DdQueueItem *item)); +static int hashResize ARGS((DdLevelQueue *queue)); + +/**AutomaticEnd***************************************************************/ + + +/*---------------------------------------------------------------------------*/ +/* Definition of internal functions */ +/*---------------------------------------------------------------------------*/ + + +/**Function******************************************************************** + + Synopsis [Initializes a level queue.] + + Description [Initializes a level queue. A level queue is a queue + where inserts are based on the levels of the nodes. Within each + level the policy is FIFO. Level queues are useful in traversing a + BDD top-down. Queue items are kept in a free list when dequeued for + efficiency. Returns a pointer to the new queue if successful; NULL + otherwise.] + + SideEffects [None] + + SeeAlso [cuddLevelQueueQuit cuddLevelQueueEnqueue cuddLevelQueueDequeue] + +******************************************************************************/ +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 */ + + +/**Function******************************************************************** + + Synopsis [Shuts down a level queue.] + + Description [Shuts down a level queue and releases all the + associated memory.] + + SideEffects [None] + + SeeAlso [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 */ + + +/**Function******************************************************************** + + Synopsis [Inserts a new key in a level queue.] + + Description [Inserts a new key in a level queue. A new entry is + created in the queue only if the node is not already + enqueued. Returns a pointer to the queue item if successful; NULL + otherwise.] + + SideEffects [None] + + SeeAlso [cuddLevelQueueInit cuddLevelQueueDequeue] + +******************************************************************************/ +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 */ + + +/**Function******************************************************************** + + Synopsis [Remove an item from the front of a level queue.] + + Description [Remove an item from the front of a level queue.] + + SideEffects [None] + + SeeAlso [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 */ +/*---------------------------------------------------------------------------*/ + + +/**Function******************************************************************** + + Synopsis [Looks up a key in the hash table of a level queue.] + + Description [Looks up a key in the hash table of a level queue. Returns + a pointer to the item with the given key if the key is found; NULL + otherwise.] + + SideEffects [None] + + SeeAlso [cuddLevelQueueEnqueue hashInsert] + +******************************************************************************/ +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 */ + + +/**Function******************************************************************** + + Synopsis [Inserts an item in the hash table of a level queue.] + + Description [Inserts an item in the hash table of a level queue. Returns + 1 if successful; 0 otherwise. No check is performed to see if an item with + the same key is already in the hash table.] + + SideEffects [None] + + SeeAlso [cuddLevelQueueEnqueue] + +******************************************************************************/ +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 */ + + +/**Function******************************************************************** + + Synopsis [Removes an item from the hash table of a level queue.] + + Description [Removes an item from the hash table of a level queue. + Nothing is done if the item is not in the table.] + + SideEffects [None] + + SeeAlso [cuddLevelQueueDequeue 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 */ + + +/**Function******************************************************************** + + Synopsis [Resizes the hash table of a level queue.] + + Description [Resizes the hash table of a level queue. Returns 1 if + successful; 0 otherwise.] + + SideEffects [None] + + SeeAlso [hashInsert] + +******************************************************************************/ +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 void (*MMoutOfMemory)(long); + void (*saveHandler)(long); + + /* 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); + 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 */ |