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 * VECTORS OF INTEGERS (RESIZABLE ARRAYS)
21 */
22
23 #ifndef __INT_VECTORS_H
24 #define __INT_VECTORS_H
25
26 #include <stdint.h>
27 #include <stdbool.h>
28 #include <assert.h>
29
30
31 /*
32 * Vector of signed 32bit integers
33 * - capacity = size of the data array
34 * - size = number of elements stored in data
35 * (i.e., the vector's content is data[0 ... size-1])
36 */
37 typedef struct ivector_s {
38 uint32_t capacity;
39 uint32_t size;
40 int32_t *data;
41 } ivector_t;
42
43
44 /*
45 * Default initial size and max size
46 */
47 #define DEF_IVECTOR_SIZE 10
48 #define MAX_IVECTOR_SIZE (UINT32_MAX/sizeof(int32_t))
49
50
51
52 /*
53 * Initialize v with initial capacity = n
54 * - v is empty
55 */
56 extern void init_ivector(ivector_t *v, uint32_t n);
57
58 /*
59 * Free the memory used by v
60 */
61 extern void delete_ivector(ivector_t *v);
62
63 /*
64 * Increase v's capacity by 50% (approximately)
65 * Keep the content and size unchanged.
66 */
67 extern void extend_ivector(ivector_t *v);
68
69 /*
70 * Make v large enough for at least n elements
71 * - increase the capacity if needed
72 * - keep the content and size unchanged.
73 */
74 extern void resize_ivector(ivector_t *v, uint32_t n);
75
76 /*
77 * copy array a[0 .. n-1] into v
78 */
79 extern void ivector_copy(ivector_t *v, const int32_t *a, uint32_t n);
80
81 /*
82 * append a[0 .. n-1] to v
83 */
84 extern void ivector_add(ivector_t *v, const int32_t *a, uint32_t n);
85
86
87 /*
88 * Swap the content of v1 and v2
89 */
90 extern void ivector_swap(ivector_t *v1, ivector_t *v2);
91
92
93 /*
94 * add x at the end of v
95 */
ivector_push(ivector_t * v,int32_t x)96 static inline void ivector_push(ivector_t *v, int32_t x) {
97 uint32_t i;
98
99 i = v->size;
100 if (i >= v->capacity) {
101 extend_ivector(v);
102 }
103 v->data[i] = x;
104 v->size = i+1;
105 }
106
107 /*
108 * get the last element
109 */
ivector_last(ivector_t * v)110 static inline int32_t ivector_last(ivector_t *v) {
111 assert(v->size > 0);
112 return v->data[v->size - 1];
113 }
114
115 /*
116 * remove the last element
117 */
ivector_pop(ivector_t * v)118 static inline void ivector_pop(ivector_t *v) {
119 assert(v->size > 0);
120 v->size --;
121 }
122
123 /*
124 * combine pop and last: remove and return the last element
125 */
ivector_pop2(ivector_t * v)126 static inline int32_t ivector_pop2(ivector_t *v) {
127 assert(v->size > 0);
128 v->size --;
129 return v->data[v->size];
130 }
131
132 /*
133 * Empty v
134 */
ivector_reset(ivector_t * v)135 static inline void ivector_reset(ivector_t *v) {
136 v->size = 0;
137 }
138
139
140 /*
141 * Keep the n first elements of v
142 * - n must be less than or equal to v's current size.
143 */
ivector_shrink(ivector_t * v,uint32_t n)144 static inline void ivector_shrink(ivector_t *v, uint32_t n) {
145 assert(n <= v->size);
146 v->size = n;
147 }
148
149
150 /*
151 * Remove duplicates in an integer vector
152 * Side effect: sort v in increasing order
153 */
154 extern void ivector_remove_duplicates(ivector_t *v);
155
156 #endif /* _INT__VECTORS_H */
157