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 * MAPS 32BIT INTEGERS TO 32BIT INTEGERS
21 * Assumes that keys are non-negative
22 */
23
24 #include <assert.h>
25
26 #include "utils/int_hash_map.h"
27 #include "utils/memalloc.h"
28
29
30 /*
31 * For debugging: check whether n is 0 or a power of 2
32 */
33 #ifndef NDEBUG
is_power_of_two(uint32_t n)34 static bool is_power_of_two(uint32_t n) {
35 return (n & (n - 1)) == 0;
36 }
37 #endif
38
39
40 /*
41 * Initialization:
42 * - n = initial size, must be a power of 2
43 * - if n = 0, the default size is used
44 */
init_int_hmap(int_hmap_t * hmap,uint32_t n)45 void init_int_hmap(int_hmap_t *hmap, uint32_t n) {
46 uint32_t i;
47 int_hmap_pair_t *tmp;
48
49 if (n == 0) {
50 n = INT_HMAP_DEFAULT_SIZE;
51 }
52
53 if (n >= INT_HMAP_MAX_SIZE) {
54 out_of_memory();
55 }
56
57 assert(is_power_of_two(n));
58
59 tmp = (int_hmap_pair_t *) safe_malloc(n * sizeof(int_hmap_pair_t));
60 for (i=0; i<n; i++) {
61 tmp[i].key = EMPTY_KEY;
62 }
63
64 hmap->data = tmp;
65 hmap->size = n;
66 hmap->nelems = 0;
67 hmap->ndeleted = 0;
68
69 hmap->resize_threshold = (uint32_t)(n * INT_HMAP_RESIZE_RATIO);
70 hmap->cleanup_threshold = (uint32_t) (n * INT_HMAP_CLEANUP_RATIO);
71 }
72
73
74 /*
75 * Free memory
76 */
delete_int_hmap(int_hmap_t * hmap)77 void delete_int_hmap(int_hmap_t *hmap) {
78 safe_free(hmap->data);
79 hmap->data = NULL;
80 }
81
82
83 /*
84 * Hash of a key (Jenkins hash)
85 */
hash_key(int32_t k)86 static uint32_t hash_key(int32_t k) {
87 uint32_t x;
88
89 x = (uint32_t) k;
90 x = (x + 0x7ed55d16) + (x<<12);
91 x = (x ^ 0xc761c23c) ^ (x>>19);
92 x = (x + 0x165667b1) + (x<<5);
93 x = (x + 0xd3a2646c) ^ (x<<9);
94 x = (x + 0xfd7046c5) + (x<<3);
95 x = (x ^ 0xb55a4f09) ^ (x>>16);
96
97 return x;
98 }
99
100 /*
101 * Make a copy of record d in a clean array data
102 * - mask = size of data - 1 (size must be a power of 2)
103 */
int_hmap_clean_copy(int_hmap_pair_t * data,int_hmap_pair_t * d,uint32_t mask)104 static void int_hmap_clean_copy(int_hmap_pair_t *data, int_hmap_pair_t *d, uint32_t mask) {
105 uint32_t j;
106
107 j = hash_key(d->key) & mask;
108 while (data[j].key != EMPTY_KEY) {
109 j ++;
110 j &= mask;
111 }
112
113 data[j].key = d->key;
114 data[j].val = d->val;
115 }
116
117
118 /*
119 * Remove deleted records
120 */
int_hmap_cleanup(int_hmap_t * hmap)121 static void int_hmap_cleanup(int_hmap_t *hmap) {
122 int_hmap_pair_t *tmp, *d;
123 uint32_t j, n, mask;
124
125 n = hmap->size;
126 tmp = (int_hmap_pair_t *) safe_malloc(n * sizeof(int_hmap_pair_t));
127 for (j=0; j<n; j++) {
128 tmp[j].key = EMPTY_KEY;
129 }
130
131 mask = n - 1;
132 d = hmap->data;
133 for (j=0; j<n; j++) {
134 if (d->key >= 0) {
135 int_hmap_clean_copy(tmp, d, mask);
136 }
137 d++;
138 }
139
140 safe_free(hmap->data);
141 hmap->data = tmp;
142 hmap->ndeleted = 0;
143 }
144
145
146 /*
147 * Remove deleted records and make the table twice as large
148 */
int_hmap_extend(int_hmap_t * hmap)149 static void int_hmap_extend(int_hmap_t *hmap) {
150 int_hmap_pair_t *tmp, *d;
151 uint32_t j, n, n2, mask;
152
153 n = hmap->size;
154 n2 = n << 1;
155 if (n2 >= INT_HMAP_MAX_SIZE) {
156 out_of_memory();
157 }
158
159 tmp = (int_hmap_pair_t *) safe_malloc(n2 * sizeof(int_hmap_pair_t));
160 for (j=0; j<n2; j++) {
161 tmp[j].key = EMPTY_KEY;
162 }
163
164 mask = n2 - 1;
165 d = hmap->data;
166 for (j=0; j<n; j++) {
167 if (d->key >= 0) {
168 int_hmap_clean_copy(tmp, d, mask);
169 }
170 d ++;
171 }
172
173 safe_free(hmap->data);
174 hmap->data = tmp;
175 hmap->size = n2;
176 hmap->ndeleted = 0;
177
178 hmap->resize_threshold = (uint32_t)(n2 * INT_HMAP_RESIZE_RATIO);
179 hmap->cleanup_threshold = (uint32_t)(n2 * INT_HMAP_CLEANUP_RATIO);
180 }
181
182
183 /*
184 * Find record with key k
185 * - return NULL if k is not in the table
186 */
int_hmap_find(int_hmap_t * hmap,int32_t k)187 int_hmap_pair_t *int_hmap_find(int_hmap_t *hmap, int32_t k) {
188 uint32_t mask, j;
189 int_hmap_pair_t *d;
190
191 assert(k >= 0);
192
193 mask = hmap->size - 1;
194 j = hash_key(k) & mask;
195 for (;;) {
196 d = hmap->data + j;
197 if (d->key == k) return d;
198 if (d->key == EMPTY_KEY) return NULL;
199 j ++;
200 j &= mask;
201 }
202 }
203
204
205 /*
206 * Add record with key k after hmap was extended:
207 * - initialize val to -1
208 * - we know that no record with key k is present
209 */
int_hmap_get_clean(int_hmap_t * hmap,int32_t k)210 static int_hmap_pair_t *int_hmap_get_clean(int_hmap_t *hmap, int32_t k) {
211 uint32_t mask, j;
212 int_hmap_pair_t *d;
213
214 mask = hmap->size - 1;
215 j = hash_key(k) & mask;
216 for (;;) {
217 d = hmap->data + j;
218 if (d->key < 0) {
219 hmap->nelems ++;
220 d->key = k;
221 d->val = -1;
222 return d;
223 }
224 j ++;
225 j &= mask;
226 }
227 }
228
229
230 /*
231 * Find or add record with key k
232 */
int_hmap_get(int_hmap_t * hmap,int32_t k)233 int_hmap_pair_t *int_hmap_get(int_hmap_t *hmap, int32_t k) {
234 uint32_t mask, j;
235 int_hmap_pair_t *d, *aux;
236
237 assert(k >= 0);
238 assert(hmap->size > hmap->ndeleted + hmap->nelems);
239
240 mask = hmap->size - 1;
241 j = hash_key(k) & mask;
242
243 for (;;) {
244 d = hmap->data + j;
245 if (d->key == k) return d;
246 if (d->key < 0) break;
247 j ++;
248 j &= mask;
249 }
250
251 aux = d; // new record, if needed, will be aux
252 while (d->key != EMPTY_KEY) {
253 j ++;
254 j &= mask;
255 d = hmap->data + j;
256 if (d->key == k) return d;
257 }
258
259 if (aux->key == DELETED_KEY) {
260 assert(hmap->ndeleted > 0);
261 hmap->ndeleted --;
262 }
263
264 if (hmap->nelems + hmap->ndeleted >= hmap->resize_threshold) {
265 int_hmap_extend(hmap);
266 aux = int_hmap_get_clean(hmap, k);
267 } else {
268 hmap->nelems ++;
269 aux->key = k;
270 aux->val = -1;
271 }
272
273 return aux;
274 }
275
276
277 /*
278 * Add record [k -> v ] to hmap
279 * - there must not be a record with the same key
280 */
int_hmap_add(int_hmap_t * hmap,int32_t k,int32_t v)281 void int_hmap_add(int_hmap_t *hmap, int32_t k, int32_t v) {
282 uint32_t i, mask;
283
284 assert(k >= 0 && hmap->nelems + hmap->ndeleted < hmap->size);
285
286 mask = hmap->size - 1;
287 i = hash_key(k) & mask;
288 while (hmap->data[i].key >= 0) {
289 assert(hmap->data[i].key != k);
290 i ++;
291 i &= mask;
292 }
293
294 // store the new record in data[i]
295 if (hmap->data[i].key == DELETED_KEY) {
296 assert(hmap->ndeleted > 0);
297 hmap->ndeleted --;
298 }
299 hmap->data[i].key = k;
300 hmap->data[i].val = v;
301 hmap->nelems ++;
302
303 if (hmap->nelems + hmap->ndeleted >= hmap->resize_threshold) {
304 int_hmap_extend(hmap);
305 }
306 }
307
308
309 /*
310 * Erase record r
311 */
int_hmap_erase(int_hmap_t * hmap,int_hmap_pair_t * r)312 void int_hmap_erase(int_hmap_t *hmap, int_hmap_pair_t *r) {
313 assert(int_hmap_find(hmap, r->key) == r);
314
315 r->key = DELETED_KEY;
316 hmap->nelems --;
317 hmap->ndeleted ++;
318 if (hmap->ndeleted >= hmap->cleanup_threshold) {
319 int_hmap_cleanup(hmap);
320 }
321 }
322
323
324 /*
325 * Empty the map
326 */
int_hmap_reset(int_hmap_t * hmap)327 void int_hmap_reset(int_hmap_t *hmap) {
328 uint32_t i, n;
329 int_hmap_pair_t *d;
330
331 n = hmap->size;
332 d = hmap->data;
333 for (i=0; i<n; i++) {
334 d->key = EMPTY_KEY;
335 d ++;
336 }
337
338 hmap->nelems = 0;
339 hmap->ndeleted = 0;
340 }
341
342
343
344 /*
345 * First non-empty record in the table, starting from p
346 */
int_hmap_get_next(int_hmap_t * hmap,int_hmap_pair_t * p)347 static int_hmap_pair_t *int_hmap_get_next(int_hmap_t *hmap, int_hmap_pair_t *p) {
348 int_hmap_pair_t *end;
349
350 end = hmap->data + hmap->size;
351 while (p < end) {
352 if (p->key != EMPTY_KEY) return p;
353 p ++;
354 }
355
356 return NULL;
357 }
358
359
360 /*
361 * Get the first non-empty record or NULL if the table is empty
362 */
int_hmap_first_record(int_hmap_t * hmap)363 int_hmap_pair_t *int_hmap_first_record(int_hmap_t *hmap) {
364 return int_hmap_get_next(hmap, hmap->data);
365 }
366
367
368 /*
369 * Next record after p or NULL
370 */
int_hmap_next_record(int_hmap_t * hmap,int_hmap_pair_t * p)371 int_hmap_pair_t *int_hmap_next_record(int_hmap_t *hmap, int_hmap_pair_t *p) {
372 assert(p != NULL && p<hmap->data + hmap->size && p->key != EMPTY_KEY);
373 return int_hmap_get_next(hmap, p+1);
374 }
375
376
377
378
379 /*
380 * Remove the records that satisfy filter f
381 * - calls f(aux, p) on every record p stored in hmap
382 * - if f(aux, p) returns true then record p is removed
383 */
int_hmap_remove_records(int_hmap_t * hmap,void * aux,int_hmap_filter_t f)384 void int_hmap_remove_records(int_hmap_t *hmap, void *aux, int_hmap_filter_t f) {
385 int_hmap_pair_t *d;
386 uint32_t i, n, k;
387
388 n = hmap->size;
389 d = hmap->data;
390 k = 0;
391 for (i=0; i<n; i++) {
392 if (d->key >= 0 && f(aux, d)) {
393 // mark d as deleted
394 d->key = DELETED_KEY;
395 k ++;
396 }
397 d ++;
398 }
399
400 // k = number of deleted records
401 assert(k <= hmap->nelems);
402 hmap->nelems -= k;
403 hmap->ndeleted += k;
404 if (hmap->ndeleted >= hmap->cleanup_threshold) {
405 int_hmap_cleanup(hmap);
406 }
407 }
408
409
410
411 /*
412 * Iterator: call f(aux, p) on every record p
413 */
int_hmap_iterate(int_hmap_t * hmap,void * aux,int_hmap_iterator_t f)414 void int_hmap_iterate(int_hmap_t *hmap, void *aux, int_hmap_iterator_t f) {
415 int_hmap_pair_t *d;
416 uint32_t i, n;
417
418 n = hmap->size;
419 d = hmap->data;
420 for (i=0; i<n; i++) {
421 if (d->key >= 0) {
422 f(aux, d);
423 }
424 d ++;
425 }
426 }
427