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
21 */
22
23 /*
24 * This used to be part of arith_vartable. Moved it to a separate
25 * file to share the code with other modules.
26 */
27
28 #include "utils/index_vectors.h"
29
30
31 /*
32 * Add index k at the end of vector *v
33 * - if *v is NULL, allocate a fresh vector of default size
34 */
add_index_to_vector(int32_t ** v,int32_t k)35 void add_index_to_vector(int32_t **v, int32_t k) {
36 index_vector_t *u;
37 int32_t *d;
38 uint32_t i, n;
39
40 d = *v;
41 if (d == NULL) {
42 // initial allocation
43 i = 0;
44 n = DEF_IDX_VECTOR_SIZE;
45 assert(n <= MAX_IDX_VECTOR_SIZE);
46 u = (index_vector_t *) safe_malloc(sizeof(index_vector_t) + n * sizeof(int32_t));
47 u->capacity = n;
48 d = u->data;
49 *v = d;
50 } else {
51 u = iv_header(d);
52 i = u->size;
53 n = u->capacity;
54 if (i == n) {
55 // make the vector 50% larger
56 n ++;
57 n += n>>1; // new capacity
58 if (n > MAX_IDX_VECTOR_SIZE) {
59 out_of_memory();
60 }
61 u = (index_vector_t *) safe_realloc(u, sizeof(index_vector_t) + n * sizeof(int32_t));
62 u->capacity = n;
63 d = u->data;
64 *v = d;
65 }
66 }
67
68 assert(i < u->capacity && d == u->data);
69 d[i] = k;
70 u->size = i+1;
71 }
72
73
74
75 /*
76 * Make v large enough for n elements
77 * - if *v is NULL, a fresh vector of size = max(n, default size) is allocated
78 * - if *v is large enough, do nothing.
79 */
resize_index_vector(int32_t ** v,uint32_t n)80 void resize_index_vector(int32_t **v, uint32_t n) {
81 index_vector_t *u;
82 int32_t *d;
83 uint32_t new_cap;
84
85 d = *v;
86 if (d == NULL) {
87 new_cap = DEF_IDX_VECTOR_SIZE;
88 if (new_cap < n) {
89 new_cap = n;
90 if (new_cap > MAX_IDX_VECTOR_SIZE) {
91 out_of_memory();
92 }
93 }
94 u = (index_vector_t *) safe_malloc(sizeof(index_vector_t) + new_cap * sizeof(int32_t));
95 u->capacity = new_cap;
96 u->size = 0;
97 *v = u->data;
98 } else {
99 u = iv_header(d);
100 if (u->capacity < n) {
101 if (n > MAX_IDX_VECTOR_SIZE) {
102 out_of_memory();
103 }
104 u = (index_vector_t *) safe_realloc(u, sizeof(index_vector_t) + n * sizeof(int32_t));
105 u->capacity = n;
106 *v = u->data;
107 }
108 }
109 }
110
111
112 /*
113 * Create a vector that contains a[0 ... n-1]
114 */
make_index_vector(int32_t * a,uint32_t n)115 int32_t *make_index_vector(int32_t *a, uint32_t n) {
116 index_vector_t *v;
117 uint32_t i;
118
119 if (n == 0) return NULL;
120 if (n > MAX_IDX_VECTOR_SIZE) {
121 out_of_memory();
122 }
123 v = (index_vector_t *) safe_malloc(sizeof(index_vector_t) + n * sizeof(int32_t));
124 v->capacity = n;
125 v->size = n;
126 for (i=0; i<n; i++) {
127 v->data[i] = a[i];
128 }
129
130 return v->data;
131 }
132
133
134 /*
135 * Remove element k from vector v
136 * - no change if v is NULL or if k is not in v
137 */
remove_index_from_vector(int32_t * v,int32_t k)138 void remove_index_from_vector(int32_t *v, int32_t k) {
139 uint32_t i, n;
140
141 if (v != NULL) {
142 n = iv_size(v);
143 /*
144 * The common case should be when k is the last element of v
145 */
146 if (n > 0) {
147 n --;
148 if (v[n] != k) {
149 i = n;
150 do {
151 if (i == 0) return; // k is not in v
152 i --;
153 } while (v[i] != k);
154 // shift elements v[i+1... n] into v[i .. n-1]
155 while (i < n) {
156 v[i] = v[i+1];
157 i ++;
158 }
159 }
160 iv_header(v)->size = n;
161 }
162 }
163 }
164
165
166 /*
167 * Remove v[i] from vector v
168 */
clear_index_elem(int32_t * v,uint32_t i)169 void clear_index_elem(int32_t *v, uint32_t i) {
170 uint32_t n;
171
172 assert(v != NULL && i < iv_size(v));
173 n = iv_size(v) - 1;
174 // move last element into v[i] (no effect if i == n)
175 v[i] = v[n];
176 iv_header(v)->size = n;
177 }
178
179
180 /*
181 * Check whether k is present in v
182 */
index_in_vector(int32_t * v,int32_t k)183 bool index_in_vector(int32_t *v, int32_t k) {
184 uint32_t i, n;
185
186 if (v != NULL) {
187 n = iv_size(v);
188 for (i=0; i<n; i++) {
189 if (v[i] == k) return true;
190 }
191 }
192 return false;
193 }
194
195