1 /*-----------------------------------------------------------------------
2
3 File : clb_pqueue.h
4
5 Author: Stephan Schulz
6
7 Contents
8
9 Functions for LIFO-lists.
10
11 Copyright 1998, 1999 by the author.
12 This code is released under the GNU General Public Licence and
13 the GNU Lesser General Public License.
14 See the file COPYING in the main E directory for details..
15 Run "eprover -h" for contact information.
16
17 Changes
18
19 <1> Tue Jun 30 17:14:42 MET DST 1998
20 New
21
22 -----------------------------------------------------------------------*/
23
24 #ifndef CLB_PQUEUE
25
26 #define CLB_PQUEUE
27
28
29 #include <clb_memory.h>
30
31 /*---------------------------------------------------------------------*/
32 /* Data type declarations */
33 /*---------------------------------------------------------------------*/
34
35 #define PQUEUE_DEFAULT_SIZE 128 /* Queues grow exponentially (and never
36 shrink unless explicitly freed) -
37 take care */
38
39 typedef struct pqueuecell
40 {
41 long size; /* Of allocateted memory */
42 long head; /* Where the next element will be put */
43 long tail; /* Where the next element will come from */
44 IntOrP *queue; /* Memory */
45 }PQueueCell, *PQueue_p;
46
47
48 /*---------------------------------------------------------------------*/
49 /* Exported Functions and Variables */
50 /*---------------------------------------------------------------------*/
51
52 #define PQueueCellAlloc() (PQueueCell*)SizeMalloc(sizeof(PQueueCell))
53 #define PQueueCellFree(junk) SizeFree(junk, sizeof(PQueueCell))
54
55 static __inline__ PQueue_p PQueueAlloc(void);
56 static __inline__ void PQueueFree(PQueue_p junk);
57 void PQueueGrow(PQueue_p queue);
58 #define PQueueEmpty(queue) ((queue)->head == (queue)->tail)
59 static __inline__ void PQueueReset(PQueue_p queue);
60
61 static __inline__ void PQueueStoreInt(PQueue_p queue, long val);
62 static __inline__ void PQueueStoreP(PQueue_p queue, void* val);
63
64 static __inline__ void PQueueBuryInt(PQueue_p queue, long val);
65 static __inline__ void PQueueBuryP(PQueue_p queue, void* val);
66
67 static __inline__ IntOrP PQueueGetNext(PQueue_p queue);
68 #define PQueueGetNextInt(Queue) (PQueueGetNext(Queue).i_val)
69 #define PQueueGetNextP(Queue) (PQueueGetNext(Queue).p_val)
70
71 static __inline__ IntOrP PQueueGetLast(PQueue_p queue);
72 #define PQueueGetLastInt(Queue) (PQueueGetLast(Queue).i_val)
73 #define PQueueGetLastP(Queue) (PQueueGetLast(Queue).p_val)
74
75 static __inline__ IntOrP PQueueLook(PQueue_p queue);
76 #define PQueueLookInt(Queue) (PQueueLook(Queue).i_val)
77 #define PQueueLookP(Queue) (PQueueLook(Queue).p_val)
78 static __inline__ IntOrP PQueueLookLast(PQueue_p queue);
79 #define PQueueLookLastInt(Queue) (PQueueLookLast(Queue).i_val)
80 #define PQueueLookLastP(Queue) (PQueueLookLast(Queue).p_val)
81 long PQueueCardinality(PQueue_p queue);
82
83 IntOrP PQueueElement(PQueue_p queue, long index);
84 #define PQueueElementInt(Queue, index) (PQueueElement(Queue,index).i_val)
85 #define PQueueElementP(Queue, index) (PQueueElement(Queue,index).p_val)
86
87 long PQueueTailIndex(PQueue_p queue);
88 long PQueueIncIndex(PQueue_p queue, long index);
89
90 /*---------------------------------------------------------------------*/
91 /* Inline-Functions */
92 /*---------------------------------------------------------------------*/
93
94
95 /*-----------------------------------------------------------------------
96 //
97 // Function: pqueue_store()
98 //
99 // Put an element in the queue.
100 //
101 // Global Variables: -
102 //
103 // Side Effects : memory operations, changes queue
104 //
105 /----------------------------------------------------------------------*/
106
pqueue_store(PQueue_p queue,IntOrP val)107 static __inline__ void pqueue_store(PQueue_p queue, IntOrP val)
108 {
109 queue->queue[queue->head] = val;
110 queue->head++;
111 if(queue->head == queue->size)
112 {
113 queue->head = 0;
114 }
115
116 if(queue->head == queue->tail)
117 {
118 PQueueGrow(queue);
119 }
120 }
121
122
123 /*-----------------------------------------------------------------------
124 //
125 // Function: pqueue_bury()
126 //
127 // Put an element at the front of the queue (i.e. "bury" it under
128 // all the other elements in a stack-view of the queue).
129 //
130 // Global Variables: -
131 //
132 // Side Effects : memory operations, changes queue
133 //
134 /----------------------------------------------------------------------*/
135
pqueue_bury(PQueue_p queue,IntOrP val)136 static __inline__ void pqueue_bury(PQueue_p queue, IntOrP val)
137 {
138 queue->tail = queue->tail? (queue->tail-1):queue->size-1;
139 queue->queue[queue->tail] = val;
140
141 if(queue->head == queue->tail)
142 {
143 PQueueGrow(queue);
144 }
145 }
146
147
148 /*-----------------------------------------------------------------------
149 //
150 // Function: PQueueAlloc()
151 //
152 // Allocate an empty, initialized Queue.
153 //
154 // Global Variables: -
155 //
156 // Side Effects : Memory operations
157 //
158 /----------------------------------------------------------------------*/
159
PQueueAlloc(void)160 static __inline__ PQueue_p PQueueAlloc(void)
161 {
162 PQueue_p handle = PQueueCellAlloc();
163
164 handle->size = PQUEUE_DEFAULT_SIZE;
165 handle->head = 0;
166 handle->tail = 0;
167 handle->queue = SizeMalloc(PQUEUE_DEFAULT_SIZE*sizeof(IntOrP));
168
169 return handle;
170 }
171
172
173 /*-----------------------------------------------------------------------
174 //
175 // Function: PQueueFree()
176 //
177 // Free a Queue.
178 //
179 // Global Variables: -
180 //
181 // Side Effects : Memory operations
182 //
183 /----------------------------------------------------------------------*/
184
PQueueFree(PQueue_p junk)185 static __inline__ void PQueueFree(PQueue_p junk)
186 {
187 SizeFree(junk->queue, junk->size*sizeof(IntOrP));
188 PQueueCellFree(junk);
189 }
190
191 /*-----------------------------------------------------------------------
192 //
193 // Function: PQueueReset()
194 //
195 // Reset a queue to empty state.
196 //
197 // Global Variables: -
198 //
199 // Side Effects : -
200 //
201 /----------------------------------------------------------------------*/
202
PQueueReset(PQueue_p queue)203 static __inline__ void PQueueReset(PQueue_p queue)
204 {
205 queue->head = 0;
206 queue->tail = 0;
207 }
208
209
210 /*-----------------------------------------------------------------------
211 //
212 // Function: PQueueStoreInt()
213 //
214 // Store an integer in the queue.
215 //
216 // Global Variables: -
217 //
218 // Side Effects : -
219 //
220 /----------------------------------------------------------------------*/
221
PQueueStoreInt(PQueue_p queue,long val)222 static __inline__ void PQueueStoreInt(PQueue_p queue, long val)
223 {
224 IntOrP handle;
225
226 handle.i_val = val;
227 pqueue_store(queue, handle);
228 }
229
230 /*-----------------------------------------------------------------------
231 //
232 // Function: PQueueStoreP()
233 //
234 // Store a pointer in the queue.
235 //
236 // Global Variables: -
237 //
238 // Side Effects : -
239 //
240 /----------------------------------------------------------------------*/
241
PQueueStoreP(PQueue_p queue,void * val)242 static __inline__ void PQueueStoreP(PQueue_p queue, void* val)
243 {
244 IntOrP handle;
245
246 handle.p_val = val;
247 pqueue_store(queue, handle);
248 }
249
250 /*-----------------------------------------------------------------------
251 //
252 // Function: PQueueBuryInt()
253 //
254 // Store an integer at the front of the the queue.
255 //
256 // Global Variables: -
257 //
258 // Side Effects : -
259 //
260 /----------------------------------------------------------------------*/
261
PQueueBuryInt(PQueue_p queue,long val)262 static __inline__ void PQueueBuryInt(PQueue_p queue, long val)
263 {
264 IntOrP handle;
265
266 handle.i_val = val;
267 pqueue_bury(queue, handle);
268 }
269
270 /*-----------------------------------------------------------------------
271 //
272 // Function: PQueueBuryP()
273 //
274 // Store a pointer at the front of the queue.
275 //
276 // Global Variables: -
277 //
278 // Side Effects : -
279 //
280 /----------------------------------------------------------------------*/
281
PQueueBuryP(PQueue_p queue,void * val)282 static __inline__ void PQueueBuryP(PQueue_p queue, void* val)
283 {
284 IntOrP handle;
285
286 handle.p_val = val;
287 pqueue_bury(queue, handle);
288 }
289
290
291 /*-----------------------------------------------------------------------
292 //
293 // Function: PQueueGetNext()
294 //
295 // Extract the next value from the queue and return it.
296 //
297 // Global Variables: -
298 //
299 // Side Effects : Changes queue.
300 //
301 /----------------------------------------------------------------------*/
302
PQueueGetNext(PQueue_p queue)303 static __inline__ IntOrP PQueueGetNext(PQueue_p queue)
304 {
305 IntOrP res;
306
307 assert(!PQueueEmpty(queue));
308
309 res = queue->queue[queue->tail];
310 queue->tail++;
311 if(queue->tail == queue->size)
312 {
313 queue->tail = 0;
314 }
315
316 return res;
317 }
318
319
320 /*-----------------------------------------------------------------------
321 //
322 // Function: PQueueGetLast()
323 //
324 // Extract the last value from the queue (i.e. pop from the queue
325 // viewed as a stack) and return it.
326 //
327 // Global Variables: -
328 //
329 // Side Effects : Changes queue.
330 //
331 /----------------------------------------------------------------------*/
332
PQueueGetLast(PQueue_p queue)333 static __inline__ IntOrP PQueueGetLast(PQueue_p queue)
334 {
335 IntOrP res;
336
337 assert(!PQueueEmpty(queue));
338
339 queue->head = queue->head? (queue->head-1):queue->size-1;
340 res = queue->queue[queue->head];
341
342 return res;
343 }
344
345
346 /*-----------------------------------------------------------------------
347 //
348 // Function: PQueueLook()
349 //
350 // Return the next element from the queue without changing the
351 // queue.
352 //
353 // Global Variables: -
354 //
355 // Side Effects : -
356 //
357 /----------------------------------------------------------------------*/
358
PQueueLook(PQueue_p queue)359 static __inline__ IntOrP PQueueLook(PQueue_p queue)
360 {
361 assert(!PQueueEmpty(queue));
362
363 return queue->queue[queue->tail];
364 }
365
366
367
368 /*-----------------------------------------------------------------------
369 //
370 // Function: PQueueLookLast()
371 //
372 // Return the last (youngest) value from the queue without modifyin
373 // the queue.
374 //
375 // Global Variables: -
376 //
377 // Side Effects : Changes queue.
378 //
379 /----------------------------------------------------------------------*/
380
PQueueLookLast(PQueue_p queue)381 static __inline__ IntOrP PQueueLookLast(PQueue_p queue)
382 {
383 IntOrP res;
384 long index;
385
386 assert(!PQueueEmpty(queue));
387
388 index = queue->head? (queue->head-1):queue->size-1;
389 res = queue->queue[index];
390
391 return res;
392 }
393
394
395 #endif
396
397 /*---------------------------------------------------------------------*/
398 /* End of File */
399 /*---------------------------------------------------------------------*/
400
401
402
403
404
405