source: vis_dev/glu-2.3/src/cuBdd/cuddLevelQ.c @ 100

Last change on this file since 100 was 13, checked in by cecile, 13 years ago

library glu 2.3

File size: 16.4 KB
Line 
1/**CFile***********************************************************************
2
3  FileName    [cuddLevelQ.c]
4
5  PackageName [cudd]
6
7  Synopsis    [Procedure to manage level queues.]
8
9  Description [The functions in this file allow an application to
10  easily manipulate a queue where nodes are prioritized by level. The
11  emphasis is on efficiency. Therefore, the queue items can have
12  variable size.  If the application does not need to attach
13  information to the nodes, it can declare the queue items to be of
14  type DdQueueItem. Otherwise, it can declare them to be of a
15  structure type such that the first three fields are data
16  pointers. The third pointer points to the node.  The first two
17  pointers are used by the level queue functions. The remaining fields
18  are initialized to 0 when a new item is created, and are then left
19  to the exclusive use of the application. On the DEC Alphas the three
20  pointers must be 32-bit pointers when CUDD is compiled with 32-bit
21  pointers.  The level queue functions make sure that each node
22  appears at most once in the queue. They do so by keeping a hash
23  table where the node is used as key.  Queue items are recycled via a
24  free list for efficiency.
25 
26  Internal procedures provided by this module:
27                <ul>
28                <li> cuddLevelQueueInit()
29                <li> cuddLevelQueueQuit()
30                <li> cuddLevelQueueEnqueue()
31                <li> cuddLevelQueueDequeue()
32                </ul>
33  Static procedures included in this module:
34                <ul>
35                <li> hashLookup()
36                <li> hashInsert()
37                <li> hashDelete()
38                <li> hashResize()
39                </ul>
40                ]
41
42  SeeAlso     []
43
44  Author      [Fabio Somenzi]
45
46  Copyright   [Copyright (c) 1995-2004, Regents of the University of Colorado
47
48  All rights reserved.
49
50  Redistribution and use in source and binary forms, with or without
51  modification, are permitted provided that the following conditions
52  are met:
53
54  Redistributions of source code must retain the above copyright
55  notice, this list of conditions and the following disclaimer.
56
57  Redistributions in binary form must reproduce the above copyright
58  notice, this list of conditions and the following disclaimer in the
59  documentation and/or other materials provided with the distribution.
60
61  Neither the name of the University of Colorado nor the names of its
62  contributors may be used to endorse or promote products derived from
63  this software without specific prior written permission.
64
65  THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS
66  "AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT
67  LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS
68  FOR A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE
69  COPYRIGHT OWNER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT,
70  INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING,
71  BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES;
72  LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER
73  CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT
74  LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN
75  ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE
76  POSSIBILITY OF SUCH DAMAGE.]
77
78******************************************************************************/
79
80#include "util.h"
81#include "cuddInt.h"
82
83/*---------------------------------------------------------------------------*/
84/* Constant declarations                                                     */
85/*---------------------------------------------------------------------------*/
86
87
88/*---------------------------------------------------------------------------*/
89/* Stucture declarations                                                     */
90/*---------------------------------------------------------------------------*/
91
92/*---------------------------------------------------------------------------*/
93/* Type declarations                                                         */
94/*---------------------------------------------------------------------------*/
95
96/*---------------------------------------------------------------------------*/
97/* Variable declarations                                                     */
98/*---------------------------------------------------------------------------*/
99
100#ifndef lint
101static char rcsid[] DD_UNUSED = "$Id: cuddLevelQ.c,v 1.13 2009/03/08 02:49:02 fabio Exp $";
102#endif
103
104/*---------------------------------------------------------------------------*/
105/* Macro declarations                                                        */
106/*---------------------------------------------------------------------------*/
107
108
109/**Macro***********************************************************************
110
111  Synopsis    [Hash function for the table of a level queue.]
112
113  Description [Hash function for the table of a level queue.]
114
115  SideEffects [None]
116
117  SeeAlso     [hashInsert hashLookup hashDelete]
118
119******************************************************************************/
120#if SIZEOF_VOID_P == 8 && SIZEOF_INT == 4
121#define lqHash(key,shift) \
122(((unsigned)(ptruint)(key) * DD_P1) >> (shift))
123#else
124#define lqHash(key,shift) \
125(((unsigned)(key) * DD_P1) >> (shift))
126#endif
127
128
129/**AutomaticStart*************************************************************/
130
131/*---------------------------------------------------------------------------*/
132/* Static function prototypes                                                */
133/*---------------------------------------------------------------------------*/
134
135static DdQueueItem * hashLookup (DdLevelQueue *queue, void *key);
136static int hashInsert (DdLevelQueue *queue, DdQueueItem *item);
137static void hashDelete (DdLevelQueue *queue, DdQueueItem *item);
138static int hashResize (DdLevelQueue *queue);
139
140/**AutomaticEnd***************************************************************/
141
142
143/*---------------------------------------------------------------------------*/
144/* Definition of internal functions                                          */
145/*---------------------------------------------------------------------------*/
146
147
148/**Function********************************************************************
149
150  Synopsis    [Initializes a level queue.]
151
152  Description [Initializes a level queue. A level queue is a queue
153  where inserts are based on the levels of the nodes. Within each
154  level the policy is FIFO. Level queues are useful in traversing a
155  BDD top-down. Queue items are kept in a free list when dequeued for
156  efficiency. Returns a pointer to the new queue if successful; NULL
157  otherwise.]
158
159  SideEffects [None]
160
161  SeeAlso     [cuddLevelQueueQuit cuddLevelQueueEnqueue cuddLevelQueueDequeue]
162
163******************************************************************************/
164DdLevelQueue *
165cuddLevelQueueInit(
166  int  levels /* number of levels */,
167  int  itemSize /* size of the item */,
168  int  numBuckets /* initial number of hash buckets */)
169{
170    DdLevelQueue *queue;
171    int logSize;
172
173    queue = ALLOC(DdLevelQueue,1);
174    if (queue == NULL)
175        return(NULL);
176#ifdef __osf__
177#pragma pointer_size save
178#pragma pointer_size short
179#endif
180    /* Keep pointers to the insertion points for all levels. */
181    queue->last = ALLOC(DdQueueItem *, levels);
182#ifdef __osf__
183#pragma pointer_size restore
184#endif
185    if (queue->last == NULL) {
186        FREE(queue);
187        return(NULL);
188    }
189    /* Use a hash table to test for uniqueness. */
190    if (numBuckets < 2) numBuckets = 2;
191    logSize = cuddComputeFloorLog2(numBuckets);
192    queue->numBuckets = 1 << logSize;
193    queue->shift = sizeof(int) * 8 - logSize;
194#ifdef __osf__
195#pragma pointer_size save
196#pragma pointer_size short
197#endif
198    queue->buckets = ALLOC(DdQueueItem *, queue->numBuckets);
199#ifdef __osf__
200#pragma pointer_size restore
201#endif
202    if (queue->buckets == NULL) {
203        FREE(queue->last);
204        FREE(queue);
205        return(NULL);
206    }
207#ifdef __osf__
208#pragma pointer_size save
209#pragma pointer_size short
210#endif
211    memset(queue->last, 0, levels * sizeof(DdQueueItem *));
212    memset(queue->buckets, 0, queue->numBuckets * sizeof(DdQueueItem *));
213#ifdef __osf__
214#pragma pointer_size restore
215#endif
216    queue->first = NULL;
217    queue->freelist = NULL;
218    queue->levels = levels;
219    queue->itemsize = itemSize;
220    queue->size = 0;
221    queue->maxsize = queue->numBuckets * DD_MAX_SUBTABLE_DENSITY;
222    return(queue);
223
224} /* end of cuddLevelQueueInit */
225
226
227/**Function********************************************************************
228
229  Synopsis    [Shuts down a level queue.]
230
231  Description [Shuts down a level queue and releases all the
232  associated memory.]
233
234  SideEffects [None]
235
236  SeeAlso     [cuddLevelQueueInit]
237
238******************************************************************************/
239void
240cuddLevelQueueQuit(
241  DdLevelQueue * queue)
242{
243    DdQueueItem *item;
244
245    while (queue->freelist != NULL) {
246        item = queue->freelist;
247        queue->freelist = item->next;
248        FREE(item);
249    }
250    while (queue->first != NULL) {
251        item = (DdQueueItem *) queue->first;
252        queue->first = item->next;
253        FREE(item);
254    }
255    FREE(queue->buckets);
256    FREE(queue->last);
257    FREE(queue);
258    return;
259
260} /* end of cuddLevelQueueQuit */
261
262
263/**Function********************************************************************
264
265  Synopsis    [Inserts a new key in a level queue.]
266
267  Description [Inserts a new key in a level queue. A new entry is
268  created in the queue only if the node is not already
269  enqueued. Returns a pointer to the queue item if successful; NULL
270  otherwise.]
271
272  SideEffects [None]
273
274  SeeAlso     [cuddLevelQueueInit cuddLevelQueueDequeue]
275
276******************************************************************************/
277void *
278cuddLevelQueueEnqueue(
279  DdLevelQueue * queue /* level queue */,
280  void * key /* key to be enqueued */,
281  int  level /* level at which to insert */)
282{
283    int plevel;
284    DdQueueItem *item;
285
286#ifdef DD_DEBUG
287    assert(level < queue->levels);
288#endif
289    /* Check whether entry for this node exists. */
290    item = hashLookup(queue,key);
291    if (item != NULL) return(item);
292
293    /* Get a free item from either the free list or the memory manager. */
294    if (queue->freelist == NULL) {
295        item = (DdQueueItem *) ALLOC(char, queue->itemsize);
296        if (item == NULL)
297            return(NULL);
298    } else {
299        item = queue->freelist;
300        queue->freelist = item->next;
301    }
302    /* Initialize. */
303    memset(item, 0, queue->itemsize);
304    item->key = key;
305    /* Update stats. */
306    queue->size++;
307
308    if (queue->last[level]) {
309        /* There are already items for this level in the queue. */
310        item->next = queue->last[level]->next;
311        queue->last[level]->next = item;
312    } else {
313        /* There are no items at the current level.  Look for the first
314        ** non-empty level preceeding this one. */
315        plevel = level;
316        while (plevel != 0 && queue->last[plevel] == NULL)
317            plevel--;
318        if (queue->last[plevel] == NULL) {
319            /* No element precedes this one in the queue. */
320            item->next = (DdQueueItem *) queue->first;
321            queue->first = item;
322        } else {
323            item->next = queue->last[plevel]->next;
324            queue->last[plevel]->next = item;
325        }
326    }
327    queue->last[level] = item;
328
329    /* Insert entry for the key in the hash table. */
330    if (hashInsert(queue,item) == 0) {
331        return(NULL);
332    }
333    return(item);
334
335} /* end of cuddLevelQueueEnqueue */
336
337
338/**Function********************************************************************
339
340  Synopsis    [Remove an item from the front of a level queue.]
341
342  Description [Remove an item from the front of a level queue.]
343
344  SideEffects [None]
345
346  SeeAlso     [cuddLevelQueueEnqueue]
347
348******************************************************************************/
349void
350cuddLevelQueueDequeue(
351  DdLevelQueue * queue,
352  int  level)
353{
354    DdQueueItem *item = (DdQueueItem *) queue->first;
355
356    /* Delete from the hash table. */
357    hashDelete(queue,item);
358
359    /* Since we delete from the front, if this is the last item for
360    ** its level, there are no other items for the same level. */
361    if (queue->last[level] == item)
362        queue->last[level] = NULL;
363
364    queue->first = item->next;
365    /* Put item on the free list. */
366    item->next = queue->freelist;
367    queue->freelist = item;
368    /* Update stats. */
369    queue->size--;
370    return;
371
372} /* end of cuddLevelQueueDequeue */
373
374
375/*---------------------------------------------------------------------------*/
376/* Definition of static functions                                            */
377/*---------------------------------------------------------------------------*/
378
379
380/**Function********************************************************************
381
382  Synopsis    [Looks up a key in the hash table of a level queue.]
383
384  Description [Looks up a key in the hash table of a level queue. Returns
385  a pointer to the item with the given key if the key is found; NULL
386  otherwise.]
387
388  SideEffects [None]
389
390  SeeAlso     [cuddLevelQueueEnqueue hashInsert]
391
392******************************************************************************/
393static DdQueueItem *
394hashLookup(
395  DdLevelQueue * queue,
396  void * key)
397{
398    int posn;
399    DdQueueItem *item;
400
401    posn = lqHash(key,queue->shift);
402    item = queue->buckets[posn];
403
404    while (item != NULL) {
405        if (item->key == key) {
406            return(item);
407        }
408        item = item->cnext;
409    }
410    return(NULL);
411
412} /* end of hashLookup */
413
414
415/**Function********************************************************************
416
417  Synopsis    [Inserts an item in the hash table of a level queue.]
418
419  Description [Inserts an item in the hash table of a level queue. Returns
420  1 if successful; 0 otherwise. No check is performed to see if an item with
421  the same key is already in the hash table.]
422
423  SideEffects [None]
424
425  SeeAlso     [cuddLevelQueueEnqueue]
426
427******************************************************************************/
428static int
429hashInsert(
430  DdLevelQueue * queue,
431  DdQueueItem * item)
432{
433    int result;
434    int posn;
435
436    if (queue->size > queue->maxsize) {
437        result = hashResize(queue);
438        if (result == 0) return(0);
439    }
440
441    posn = lqHash(item->key,queue->shift);
442    item->cnext = queue->buckets[posn];
443    queue->buckets[posn] = item;
444
445    return(1);
446   
447} /* end of hashInsert */
448
449
450/**Function********************************************************************
451
452  Synopsis    [Removes an item from the hash table of a level queue.]
453
454  Description [Removes an item from the hash table of a level queue.
455  Nothing is done if the item is not in the table.]
456
457  SideEffects [None]
458
459  SeeAlso     [cuddLevelQueueDequeue hashInsert]
460
461******************************************************************************/
462static void
463hashDelete(
464  DdLevelQueue * queue,
465  DdQueueItem * item)
466{
467    int posn;
468    DdQueueItem *prevItem;
469
470    posn = lqHash(item->key,queue->shift);
471    prevItem = queue->buckets[posn];
472
473    if (prevItem == NULL) return;
474    if (prevItem == item) {
475        queue->buckets[posn] = prevItem->cnext;
476        return;
477    }
478
479    while (prevItem->cnext != NULL) {
480        if (prevItem->cnext == item) {
481            prevItem->cnext = item->cnext;
482            return;
483        }
484        prevItem = prevItem->cnext;
485    }
486    return;
487
488} /* end of hashDelete */
489
490
491/**Function********************************************************************
492
493  Synopsis    [Resizes the hash table of a level queue.]
494
495  Description [Resizes the hash table of a level queue. Returns 1 if
496  successful; 0 otherwise.]
497
498  SideEffects [None]
499
500  SeeAlso     [hashInsert]
501
502******************************************************************************/
503static int
504hashResize(
505  DdLevelQueue * queue)
506{
507    int j;
508    int posn;
509    DdQueueItem *item;
510    DdQueueItem *next;
511    int numBuckets;
512#ifdef __osf__
513#pragma pointer_size save
514#pragma pointer_size short
515#endif
516    DdQueueItem **buckets;
517    DdQueueItem **oldBuckets = queue->buckets;
518#ifdef __osf__
519#pragma pointer_size restore
520#endif
521    int shift;
522    int oldNumBuckets = queue->numBuckets;
523    extern DD_OOMFP MMoutOfMemory;
524    DD_OOMFP saveHandler;
525
526    /* Compute the new size of the subtable. */
527    numBuckets = oldNumBuckets << 1;
528    saveHandler = MMoutOfMemory;
529    MMoutOfMemory = Cudd_OutOfMem;
530#ifdef __osf__
531#pragma pointer_size save
532#pragma pointer_size short
533#endif
534    buckets = queue->buckets = ALLOC(DdQueueItem *, numBuckets);
535    MMoutOfMemory = saveHandler;
536    if (buckets == NULL) {
537        queue->maxsize <<= 1;
538        return(1);
539    }
540
541    queue->numBuckets = numBuckets;
542    shift = --(queue->shift);
543    queue->maxsize <<= 1;
544    memset(buckets, 0, numBuckets * sizeof(DdQueueItem *));
545#ifdef __osf__
546#pragma pointer_size restore
547#endif
548    for (j = 0; j < oldNumBuckets; j++) {
549        item = oldBuckets[j];
550        while (item != NULL) {
551            next = item->cnext;
552            posn = lqHash(item->key, shift);
553            item->cnext = buckets[posn];
554            buckets[posn] = item;
555            item = next;
556        }
557    }
558    FREE(oldBuckets);
559    return(1);
560
561} /* end of hashResize */
Note: See TracBrowser for help on using the repository browser.