summaryrefslogtreecommitdiffstats
path: root/src/bdd/cudd/cuddLevelQ.c
diff options
context:
space:
mode:
Diffstat (limited to 'src/bdd/cudd/cuddLevelQ.c')
-rw-r--r--src/bdd/cudd/cuddLevelQ.c533
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..c4c621e7
--- /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.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 */
generated by cgit v1.2.3 (git 2.25.1) at 2024-07-02 19:34:22 +0000