1 /*
2 * This file is part of the Yices SMT Solver.
3 * Copyright (C) 2017 SRI International.
4 *
5 * Yices is free software: you can redistribute it and/or modify
6 * it under the terms of the GNU General Public License as published by
7 * the Free Software Foundation, either version 3 of the License, or
8 * (at your option) any later version.
9 *
10 * Yices is distributed in the hope that it will be useful,
11 * but WITHOUT ANY WARRANTY; without even the implied warranty of
12 * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
13 * GNU General Public License for more details.
14 *
15 * You should have received a copy of the GNU General Public License
16 * along with Yices. If not, see <http://www.gnu.org/licenses/>.
17 */
18
19 /*
20 * QUEUES OF 32BIT SIGNED INTEGERS
21 */
22
23 #ifndef __INT_QUEUES_H
24 #define __INT_QUEUES_H
25
26 #include <stdint.h>
27 #include <stdbool.h>
28
29
30 /*
31 * Components:
32 * - data = integer array to store the elements
33 * - size = size of that array
34 * - head, tail = indices between 0 and size - 1.
35 * The queue is managed as a circular array:
36 * - if head = tail, the queue is empty
37 * - if head < tail, the queue content is data[head ... tail-1]
38 * - if head > tail, the queue content is
39 * data[head...size-1] + data[0 ... tail-1]
40 */
41 typedef struct int_queue_s {
42 int32_t *data;
43 uint32_t size;
44 uint32_t head;
45 uint32_t tail;
46 } int_queue_t;
47
48
49 /*
50 * Maximal size: make sure n * sizeof(int32_t) does not overflow
51 */
52 #define MAX_INT_QUEUE_SIZE (UINT32_MAX/sizeof(int32_t))
53
54
55 /*
56 * Default size
57 */
58 #define DEFAULT_INT_QUEUE_INITIAL_SIZE 16
59
60
61 /*
62 * Initialize a queue of size n.
63 * If n = 0 then DEFAULT_QUEUE_INITIAL_SIZE is used.
64 */
65 extern void init_int_queue(int_queue_t *q, uint32_t n);
66
67
68 /*
69 * Delete q
70 */
71 extern void delete_int_queue(int_queue_t *q);
72
73
74 /*
75 * Push element x in the queue (at the end)
76 */
77 extern void int_queue_push(int_queue_t *q, int32_t x);
78
79
80 /*
81 * Push a[0 ... n-1] in the queue (in this order)
82 */
83 extern void int_queue_push_array(int_queue_t *q, int32_t *a, uint32_t n);
84
85
86 /*
87 * Check whether the queue is empty
88 */
int_queue_is_empty(int_queue_t * q)89 static inline bool int_queue_is_empty(int_queue_t *q) {
90 return q->head == q->tail;
91 }
92
93 /*
94 * Return the first element and remove it from q.
95 * - q must be non-empty.
96 */
97 extern int32_t int_queue_pop(int_queue_t *q);
98
99
100 /*
101 * Get the first element of q but don't remove it.
102 * - q must be non-empty
103 */
104 extern int32_t int_queue_first(int_queue_t *q);
105
106
107 /*
108 * Get the last element of q (don't remove it)
109 * - q must be non-empty
110 */
111 extern int32_t int_queue_last(int_queue_t *q);
112
113
114 /*
115 * Empty the queue
116 */
int_queue_reset(int_queue_t * q)117 static inline void int_queue_reset(int_queue_t *q) {
118 q->head = 0;
119 q->tail = 0;
120 }
121
122
123 #endif /* __INT_QUEUES_H */
124