1 /*
2 * This file is part of the Yices SMT Solver.
3 * Copyright (C) 2018 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 * HASH MAPS WITH SUPPORT FOR PUSH/POP
21 *
22 * keys and values are signed 32bit integers that must be non-negative.
23 */
24
25 #include <assert.h>
26 #include <stdbool.h>
27
28 #include "utils/backtrack_int_hash_map.h"
29 #include "utils/memalloc.h"
30
31
32 /*
33 * For debugging: check whether n is 0 or a power of 2
34 */
35 #ifndef NDEBUG
is_power_of_two(uint32_t n)36 static bool is_power_of_two(uint32_t n) {
37 return (n & (n - 1)) == 0;
38 }
39 #endif
40
41
42 /*
43 * Hash of a key (Jenkins hash)
44 */
hash_key(int32_t k)45 static uint32_t hash_key(int32_t k) {
46 uint32_t x;
47
48 assert(k >= 0);
49
50 x = (uint32_t) k;
51 x = (x + 0x7ed55d16) + (x<<12);
52 x = (x ^ 0xc761c23c) ^ (x>>19);
53 x = (x + 0x165667b1) + (x<<5);
54 x = (x + 0xd3a2646c) ^ (x<<9);
55 x = (x + 0xfd7046c5) + (x<<3);
56 x = (x ^ 0xb55a4f09) ^ (x>>16);
57
58 return x;
59 }
60
61
62 /*
63 * DATA ARRAYS
64 */
65
66 /*
67 * Allocate and initialize arrays pair/level
68 * - n = size of both arrays
69 */
alloc_data_arrays(back_hmap_data_t * data,uint32_t n)70 static void alloc_data_arrays(back_hmap_data_t *data, uint32_t n) {
71 uint32_t i;
72
73 data->pair = (back_hmap_elem_t *) safe_malloc(n * sizeof(back_hmap_elem_t));
74 data->level = (uint32_t *) safe_malloc(n * sizeof(uint32_t));
75 for (i=0; i<n; i++) {
76 data->pair[i].key = BACK_HMAP_EMPTY_KEY;
77 }
78 }
79
80 /*
81 * Free both arrays
82 */
free_data_arrays(back_hmap_data_t * data)83 static void free_data_arrays(back_hmap_data_t *data) {
84 safe_free(data->pair);
85 safe_free(data->level);
86 data->pair = NULL;
87 data->level = NULL;
88 }
89
90 /*
91 * Reset all keys to empty:
92 * - n = size of both arrays
93 */
reset_data_arrays(back_hmap_data_t * data,uint32_t n)94 static void reset_data_arrays(back_hmap_data_t *data, uint32_t n) {
95 uint32_t i;
96
97 for (i=0; i<n; i++) {
98 data->pair[i].key = BACK_HMAP_EMPTY_KEY;
99 }
100 }
101
102
103 /*
104 * Copy pair p and level l into a clean data array d
105 * - mask = size of d - 1, where size of d is a power of 2
106 * - d must not be full
107 */
back_hmap_clean_copy(back_hmap_data_t * d,const back_hmap_elem_t * p,uint32_t l,uint32_t mask)108 static void back_hmap_clean_copy(back_hmap_data_t *d, const back_hmap_elem_t *p, uint32_t l, uint32_t mask) {
109 uint32_t i;
110
111 i = hash_key(p->key) & mask;
112 while (d->pair[i].key >= 0) {
113 i ++;
114 i &= mask;
115 }
116
117 assert(d->pair[i].key == BACK_HMAP_EMPTY_KEY);
118
119 d->pair[i] = *p;
120 d->level[i] = l;
121 }
122
123
124 /*
125 * Copy all elements with a positive key from s to d
126 * - d is a clean array
127 * - preserve the levels.
128 * - n = size of d
129 * - m = size of s
130 */
back_hmap_clean_copy_all(back_hmap_data_t * d,const back_hmap_data_t * s,uint32_t n,uint32_t m)131 static void back_hmap_clean_copy_all(back_hmap_data_t *d, const back_hmap_data_t *s, uint32_t n, uint32_t m) {
132 const back_hmap_elem_t *e;
133 uint32_t i, mask;
134
135 assert(n >= m && is_power_of_two(n));
136
137 mask = n-1;
138
139 e = s->pair;
140 for (i=0; i<m; i++) {
141 if (e->key >= 0) {
142 back_hmap_clean_copy(d, e, s->level[i], mask);
143 }
144 e ++;
145 }
146 }
147
148
149 /*
150 * Search for key k in d->pair
151 * - mask = size of d - 1 (the size is a power of two)
152 * - return NULL if it's not found
153 * - return the pair with key == k otherwise
154 */
find(const back_hmap_data_t * d,int32_t k,uint32_t mask)155 static back_hmap_elem_t *find(const back_hmap_data_t *d, int32_t k, uint32_t mask) {
156 back_hmap_elem_t *e;
157 uint32_t i;
158
159 i = hash_key(k) & mask;
160 for (;;) {
161 e = d->pair + i;
162 if (e->key == k) return e;
163 if (e->key == BACK_HMAP_EMPTY_KEY) return NULL;
164 i ++;
165 i &= mask;
166 }
167 }
168
169
170 /*
171 * Create a fresh entry with key k and val = -1 at level l.
172 * - mask = size of d - 1
173 * - d->pair must not be full and contain only valid or empty keys
174 * (i.e., nothing DELETED).
175 * - return a pointer to the new entry
176 */
get_clean(back_hmap_data_t * d,int32_t k,uint32_t l,uint32_t mask)177 static back_hmap_elem_t *get_clean(back_hmap_data_t *d, int32_t k, uint32_t l, uint32_t mask) {
178 uint32_t i;
179
180 i = hash_key(k) & mask;
181 while (d->pair[i].key >= 0) {
182 i ++;
183 i &= mask;
184 }
185
186 assert(d->pair[i].key == BACK_HMAP_EMPTY_KEY);
187
188 d->pair[i].key = k;
189 d->pair[i].val = -1;
190 d->level[i] = l;
191
192 return d->pair + i;
193 }
194
195
196 /*
197 * Mark all elements of d with level >= l as deleted
198 * - n = size of d
199 * return the number of elements removed.
200 */
erase_level(back_hmap_data_t * d,uint32_t l,uint32_t n)201 static uint32_t erase_level(back_hmap_data_t *d, uint32_t l, uint32_t n) {
202 back_hmap_elem_t *e;
203 uint32_t i, deletions;
204
205 deletions = 0;
206
207 e = d->pair;
208 for (i=0; i<n; i++) {
209 if (e->key >= 0 && d->level[i] >= l) {
210 e->key = BACK_HMAP_DELETED_KEY;
211 deletions ++;
212 }
213 e ++;
214 }
215
216 return deletions;
217 }
218
219
220 /*
221 * HMAP
222 */
223
224 /*
225 * Initialization:
226 * - n = initial size, must be a power of 2
227 * - if n = 0, the default size is used
228 */
init_back_hmap(back_hmap_t * hmap,uint32_t n)229 void init_back_hmap(back_hmap_t *hmap, uint32_t n) {
230 if (n == 0) {
231 n = BACK_HMAP_DEF_SIZE;
232 }
233 if (n > BACK_HMAP_MAX_SIZE) {
234 out_of_memory();
235 }
236 assert(is_power_of_two(n) && n>0);
237
238 alloc_data_arrays(&hmap->data, n);
239 hmap->size = n;
240 hmap->nelems = 0;
241 hmap->ndeleted = 0;
242 hmap->resize_threshold = (uint32_t)(n * BACK_HMAP_RESIZE_RATIO);
243 hmap->cleanup_threshold = (uint32_t) (n * BACK_HMAP_CLEANUP_RATIO);
244 hmap->level = 0;
245 }
246
247
248 /*
249 * Free memory
250 */
delete_back_hmap(back_hmap_t * hmap)251 void delete_back_hmap(back_hmap_t *hmap) {
252 free_data_arrays(&hmap->data);
253 }
254
255
256 /*
257 * Empty the table and reset level to 0
258 */
reset_back_hmap(back_hmap_t * hmap)259 void reset_back_hmap(back_hmap_t *hmap) {
260 reset_data_arrays(&hmap->data, hmap->size);
261 hmap->nelems = 0;
262 hmap->ndeleted = 0;
263 hmap->level = 0;
264 }
265
266
267 /*
268 * Find entry with key = k.
269 * - return NULL if there's no such entry
270 */
back_hmap_find(const back_hmap_t * hmap,int32_t k)271 back_hmap_elem_t *back_hmap_find(const back_hmap_t *hmap, int32_t k) {
272 assert(is_power_of_two(hmap->size) && hmap->size > 0);
273 return find(&hmap->data, k, hmap->size - 1);
274 }
275
276
277 /*
278 * Double the size of the table and remove all deleted entries
279 */
back_hmap_extend(back_hmap_t * hmap)280 static void back_hmap_extend(back_hmap_t *hmap) {
281 back_hmap_data_t aux;
282 uint32_t n, new_size;
283
284 n = hmap->size;
285 new_size = n << 1;
286
287 if (new_size > BACK_HMAP_MAX_SIZE) {
288 out_of_memory();
289 }
290
291 assert(is_power_of_two(new_size));
292
293 alloc_data_arrays(&aux, new_size);
294 back_hmap_clean_copy_all(&aux, &hmap->data, new_size, n);
295 free_data_arrays(&hmap->data);
296 hmap->data = aux;
297
298 hmap->size = new_size;
299 hmap->ndeleted = 0;
300 hmap->resize_threshold = (uint32_t) (new_size * BACK_HMAP_RESIZE_RATIO);
301 hmap->cleanup_threshold = (uint32_t) (new_size * BACK_HMAP_CLEANUP_RATIO);
302 }
303
304
305 /*
306 * Remove all deleted entries. Keep the same size.
307 */
back_hmap_cleanup(back_hmap_t * hmap)308 static void back_hmap_cleanup(back_hmap_t *hmap) {
309 back_hmap_data_t aux;
310 uint32_t n;
311
312 n = hmap->size;
313
314 assert(is_power_of_two(n));
315
316 alloc_data_arrays(&aux, n);
317 back_hmap_clean_copy_all(&aux, &hmap->data, n, n);
318 free_data_arrays(&hmap->data);
319 hmap->data = aux;
320
321 hmap->ndeleted = 0;
322 }
323
324
325 /*
326 * Find or add an entry with key = k.
327 * - if the key is not already there, a new record is created with key=k,
328 * and val=-1 at the current level.
329 */
back_hmap_get(back_hmap_t * hmap,int32_t k)330 back_hmap_elem_t *back_hmap_get(back_hmap_t *hmap, int32_t k) {
331 back_hmap_elem_t *d, *aux;
332 uint32_t i, j, mask;
333
334 assert(is_power_of_two(hmap->size) && hmap->size > 0);
335 assert(hmap->size > hmap->ndeleted + hmap->nelems);
336
337 mask = hmap->size - 1;
338 i = hash_key(k) & mask;
339
340 for (;;) {
341 d = hmap->data.pair + i;
342 if (d->key == k) return d;
343 if (d->key < 0) break;
344 i ++;
345 i &= mask;
346 }
347
348 aux = d; // we'll add in this location
349 j = i;
350
351 while (d->key != BACK_HMAP_EMPTY_KEY) {
352 i ++;
353 i &= mask;
354 d = hmap->data.pair + i;
355 if (d->key == k) return d;
356 }
357
358 // k is not in the table
359 if (hmap->nelems + hmap->ndeleted >= hmap->resize_threshold) {
360 back_hmap_extend(hmap);
361 aux = get_clean(&hmap->data, k, hmap->level, hmap->size - 1);
362 hmap->nelems ++;
363 } else {
364 if (aux->key == BACK_HMAP_DELETED_KEY) {
365 assert(hmap->ndeleted > 0);
366 hmap->ndeleted --;
367 }
368 hmap->nelems ++;
369 aux->key = k;
370 aux->val = -1;
371 hmap->data.level[j] = hmap->level;
372 }
373
374 return aux;
375 }
376
377
378 /*
379 * Backtrack to the previous level: remove all elements
380 * added at the current level.
381 * - hmap->level must be positive
382 */
back_hmap_pop(back_hmap_t * hmap)383 void back_hmap_pop(back_hmap_t *hmap) {
384 uint32_t d;
385 assert(hmap->level > 0);
386
387 d = erase_level(&hmap->data, hmap->level, hmap->size);
388 hmap->ndeleted += d;
389 hmap->nelems -= d;
390 hmap->level --;
391 if (hmap->ndeleted >= hmap->cleanup_threshold) {
392 back_hmap_cleanup(hmap);
393 }
394 }
395