1 /* Boolector: Satisfiability Modulo Theories (SMT) solver.
2 *
3 * Copyright (C) 2007-2021 by the authors listed in the AUTHORS file.
4 *
5 * This file is part of Boolector.
6 * See COPYING for more information on using this software.
7 */
8
9 #include "utils/btorhashint.h"
10 #include <assert.h>
11
12 /*------------------------------------------------------------------------*/
13
14 #define HOP_RANGE 32
15 #define ADD_RANGE 8 * HOP_RANGE
16
17 /*------------------------------------------------------------------------*/
18
19 static inline uint32_t
hash(uint32_t h)20 hash (uint32_t h)
21 {
22 return h;
23 return h * 2654435761;
24 }
25
26 static inline size_t
pow2size(size_t size)27 pow2size (size_t size)
28 {
29 return size; // - HOP_RANGE;
30 }
31
32 static inline size_t
initsize(size_t size)33 initsize (size_t size)
34 {
35 return size; // + HOP_RANGE;
36 }
37
38 #if 0
39 #ifndef NDEBUG
40 #include <stdio.h>
41 static void
42 print_int_hash_table (BtorIntHashTable * t)
43 {
44 size_t i;
45
46 printf ("keys: ");
47 for (i = 0; i < t->size; i++)
48 {
49 if (i % HOP_RANGE == 0)
50 printf ("|");
51 printf ("%d[%d]", t->keys[i], t->hop_info[i]);
52 if (i < t->size - 1)
53 printf (".");
54 }
55 printf ("|\n");
56 }
57 #endif
58 #endif
59
60 #if 0
61 static void
62 print_density (BtorIntHashTable *t, int32_t key)
63 {
64 size_t j, insert_pos = hash (key) & (pow2size (t->size) - 1);
65 for (j = 0; j < t->size; j++)
66 if (j % 20 == 0)
67 printf ("|");
68 else
69 printf (" ");
70 printf ("\n");
71 for (j = 0; j < t->size; j++)
72 if (j == insert_pos)
73 printf ("%c", t->keys[j] ? 'O' : 'F');
74 else
75 printf ("%c", t->keys[j] ? 'x' : '.');
76 printf ("\n");
77 }
78 #endif
79
80 /*
81 * try to add 'key' to 't'.
82 * if adding 'key' succeeds 'key' is stored in 't->keys' and the function
83 * returns the position of 'key' in 't->keys'.
84 * if adding 'key' does not succeed, the function return 't->size'.
85 */
86 static size_t
add(BtorIntHashTable * t,int32_t key)87 add (BtorIntHashTable *t, int32_t key)
88 {
89 bool found, moved;
90 size_t i, j, size, pos, move_pos, rem_move_dist;
91 uint32_t h;
92 uint8_t move_hop_info, *hop_info;
93 int32_t *keys;
94 BtorHashTableData *data;
95
96 keys = t->keys;
97 hop_info = t->hop_info;
98 size = t->size;
99 data = t->data;
100 h = hash (key);
101 i = h & (pow2size (size) - 1);
102
103 /* search a free position within the ADD_RANGE window */
104 found = false;
105 for (j = 0, pos = i + j; j < ADD_RANGE && pos < size; j++, pos = i + j)
106 {
107 if (!keys[pos])
108 {
109 found = true;
110 break;
111 }
112 /* already in hash table */
113 else if (keys[pos] == key)
114 {
115 assert (pos < i + HOP_RANGE);
116 return pos;
117 }
118 }
119
120 /* no suitable index found for moving key, needs resizing */
121 if (!found) return size;
122
123 found = false;
124 moved = true;
125 do
126 {
127 assert (!keys[pos]);
128 if (pos - i < HOP_RANGE)
129 {
130 found = true;
131 break;
132 }
133
134 /* needs resizing */
135 if (!moved) return size;
136
137 /* 'pos' contains a free index */
138 move_pos = pos - (HOP_RANGE - 1);
139 moved = false;
140 for (j = HOP_RANGE - 1; j > 0; j--)
141 {
142 move_hop_info = hop_info[move_pos];
143 rem_move_dist = HOP_RANGE - 1 - move_hop_info;
144
145 /* not suitable for moving as remaining move distance 'rem_move_dist'
146 * is smaller than the required move distance 'j' */
147 if (rem_move_dist < j)
148 {
149 move_pos++;
150 continue;
151 }
152
153 /* move key to free position 'pos' */
154 keys[pos] = keys[move_pos];
155 hop_info[pos] = move_hop_info + j; /* update hop info */
156 assert (hop_info[pos] < HOP_RANGE);
157 keys[move_pos] = 0;
158 hop_info[move_pos] = 0;
159 if (data)
160 {
161 data[pos] = data[move_pos];
162 memset (&data[move_pos], 0, sizeof (*data));
163 data[move_pos].as_ptr = 0;
164 }
165 pos = move_pos;
166 moved = true;
167 break;
168 }
169 } while (true);
170
171 assert (found);
172 keys[pos] = key;
173 hop_info[pos] = pos - i; /* store number of hops */
174 assert (hop_info[pos] < HOP_RANGE);
175 t->count += 1;
176 return pos;
177 }
178
179 static void
resize(BtorIntHashTable * t)180 resize (BtorIntHashTable *t)
181 {
182 #ifndef NDEBUG
183 size_t old_count;
184 #endif
185 size_t i, new_pos, old_size, new_size;
186 int32_t key, *old_keys;
187 uint8_t *old_hop_info;
188 BtorHashTableData *old_data;
189
190 old_size = t->size;
191 old_keys = t->keys;
192 old_hop_info = t->hop_info;
193 old_data = t->data;
194 #ifndef NDEBUG
195 old_count = t->count;
196 #endif
197 assert (old_size > 0);
198 new_size = initsize ((pow2size (old_size)) * 2);
199 BTOR_CNEWN (t->mm, t->keys, new_size);
200 BTOR_CNEWN (t->mm, t->hop_info, new_size);
201 if (old_data) BTOR_CNEWN (t->mm, t->data, new_size);
202 t->count = 0;
203 t->size = new_size;
204
205 for (i = 0; i < old_size; i++)
206 {
207 key = old_keys[i];
208 if (!key) continue;
209 new_pos = add (t, key);
210 if (old_data) t->data[new_pos] = old_data[i];
211 /* after resizing it should always be possible to find a new position */
212 assert (new_pos < new_size);
213 }
214
215 BTOR_DELETEN (t->mm, old_keys, old_size);
216 BTOR_DELETEN (t->mm, old_hop_info, old_size);
217 if (old_data) BTOR_DELETEN (t->mm, old_data, old_size);
218 assert (old_count == t->count);
219 }
220
221 /*------------------------------------------------------------------------*/
222
223 BtorIntHashTable *
btor_hashint_table_new(BtorMemMgr * mm)224 btor_hashint_table_new (BtorMemMgr *mm)
225 {
226 BtorIntHashTable *res;
227
228 BTOR_CNEW (mm, res);
229 res->mm = mm;
230 res->size = initsize (HOP_RANGE);
231 BTOR_CNEWN (mm, res->keys, res->size);
232 BTOR_CNEWN (mm, res->hop_info, res->size);
233 return res;
234 }
235
236 void
btor_hashint_table_delete(BtorIntHashTable * t)237 btor_hashint_table_delete (BtorIntHashTable *t)
238 {
239 assert (!t->data);
240 BTOR_DELETEN (t->mm, t->keys, t->size);
241 BTOR_DELETEN (t->mm, t->hop_info, t->size);
242 BTOR_DELETE (t->mm, t);
243 }
244
245 size_t
btor_hashint_table_size(BtorIntHashTable * t)246 btor_hashint_table_size (BtorIntHashTable *t)
247 {
248 return sizeof (BtorIntHashTable)
249 + t->size * (sizeof (*t->keys) + sizeof (*t->hop_info));
250 }
251
252 size_t
btor_hashint_table_add(BtorIntHashTable * t,int32_t key)253 btor_hashint_table_add (BtorIntHashTable *t, int32_t key)
254 {
255 assert (key);
256
257 size_t pos;
258
259 // print_density (t, key);
260 pos = add (t, key);
261 /* 'add(...)' returns 't->size' if 'key' could not be added to 't'. hence,
262 * we need to resize 't'. */
263 while (pos == t->size) // TODO: loop may be obsolete
264 {
265 resize (t);
266 pos = add (t, key);
267 }
268 return pos;
269 }
270
271 bool
btor_hashint_table_contains(BtorIntHashTable * t,int32_t key)272 btor_hashint_table_contains (BtorIntHashTable *t, int32_t key)
273 {
274 return btor_hashint_table_get_pos (t, key) != t->size;
275 }
276
277 size_t
btor_hashint_table_remove(BtorIntHashTable * t,int32_t key)278 btor_hashint_table_remove (BtorIntHashTable *t, int32_t key)
279 {
280 size_t pos;
281
282 pos = btor_hashint_table_get_pos (t, key);
283
284 if (pos == t->size) return pos;
285
286 assert (t->keys[pos] == key);
287 t->keys[pos] = 0;
288 t->hop_info[pos] = 0;
289 t->count -= 1;
290 return pos;
291 }
292
293 size_t
btor_hashint_table_get_pos(BtorIntHashTable * t,int32_t key)294 btor_hashint_table_get_pos (BtorIntHashTable *t, int32_t key)
295 {
296 size_t i, size, end;
297 uint32_t h;
298 int32_t *keys;
299
300 keys = t->keys;
301 size = t->size;
302 h = hash (key);
303 i = h & (pow2size (size) - 1);
304 end = i + HOP_RANGE;
305 // assert (end < size);
306 if (end > size) end = size;
307
308 for (; i < end; i++)
309 {
310 if (keys[i] == key) return i;
311 }
312 return size;
313 }
314
315 BtorIntHashTable *
btor_hashint_table_clone(BtorMemMgr * mm,BtorIntHashTable * table)316 btor_hashint_table_clone (BtorMemMgr *mm, BtorIntHashTable *table)
317 {
318 assert (mm);
319
320 BtorIntHashTable *res;
321
322 if (!table) return NULL;
323
324 res = btor_hashint_table_new (mm);
325 while (res->size < table->size) resize (res);
326 assert (res->size == table->size);
327 memcpy (res->keys, table->keys, table->size * sizeof (*table->keys));
328 memcpy (
329 res->hop_info, table->hop_info, table->size * sizeof (*table->hop_info));
330 res->count = table->count;
331 return res;
332 }
333
334 /* map functions */
335
336 BtorIntHashTable *
btor_hashint_map_new(BtorMemMgr * mm)337 btor_hashint_map_new (BtorMemMgr *mm)
338 {
339 BtorIntHashTable *res;
340
341 res = btor_hashint_table_new (mm);
342 BTOR_CNEWN (mm, res->data, res->size);
343 return res;
344 }
345
346 bool
btor_hashint_map_contains(BtorIntHashTable * t,int32_t key)347 btor_hashint_map_contains (BtorIntHashTable *t, int32_t key)
348 {
349 assert (t->data);
350 return btor_hashint_table_contains (t, key);
351 }
352
353 void
btor_hashint_map_remove(BtorIntHashTable * t,int32_t key,BtorHashTableData * stored_data)354 btor_hashint_map_remove (BtorIntHashTable *t,
355 int32_t key,
356 BtorHashTableData *stored_data)
357 {
358 assert (t->data);
359 assert (btor_hashint_map_contains (t, key));
360
361 size_t pos;
362
363 pos = btor_hashint_table_remove (t, key);
364
365 if (stored_data) *stored_data = t->data[pos];
366 memset (&t->data[pos], 0, sizeof (BtorHashTableData));
367 }
368
369 BtorHashTableData *
btor_hashint_map_add(BtorIntHashTable * t,int32_t key)370 btor_hashint_map_add (BtorIntHashTable *t, int32_t key)
371 {
372 assert (t->data);
373
374 size_t pos;
375 pos = btor_hashint_table_add (t, key);
376 return &t->data[pos];
377 }
378
379 BtorHashTableData *
btor_hashint_map_get(BtorIntHashTable * t,int32_t key)380 btor_hashint_map_get (BtorIntHashTable *t, int32_t key)
381 {
382 assert (t->data);
383
384 size_t pos;
385
386 pos = btor_hashint_table_get_pos (t, key);
387 if (pos == t->size) return 0;
388 return &t->data[pos];
389 }
390
391 void
btor_hashint_map_delete(BtorIntHashTable * t)392 btor_hashint_map_delete (BtorIntHashTable *t)
393 {
394 assert (t->data);
395
396 BTOR_DELETEN (t->mm, t->data, t->size);
397 t->data = 0;
398 btor_hashint_table_delete (t);
399 }
400
401 BtorIntHashTable *
btor_hashint_map_clone(BtorMemMgr * mm,BtorIntHashTable * table,BtorCloneHashTableData cdata,const void * data_map)402 btor_hashint_map_clone (BtorMemMgr *mm,
403 BtorIntHashTable *table,
404 BtorCloneHashTableData cdata,
405 const void *data_map)
406 {
407 assert (mm);
408
409 size_t i;
410 BtorIntHashTable *res;
411
412 if (!table) return NULL;
413
414 res = btor_hashint_table_clone (mm, table);
415 BTOR_CNEWN (mm, res->data, res->size);
416 if (cdata)
417 {
418 for (i = 0; i < res->size; i++)
419 {
420 if (!table->keys[i]) continue;
421 cdata (mm, data_map, &table->data[i], &res->data[i]);
422 }
423 }
424 else /* as_ptr does not have to be cloned */
425 memcpy (res->data, table->data, table->size * sizeof (*table->data));
426
427 assert (table->count == res->count);
428
429 return res;
430 }
431
432 /*------------------------------------------------------------------------*/
433 /* iterators */
434 /*------------------------------------------------------------------------*/
435
436 void
btor_iter_hashint_init(BtorIntHashTableIterator * it,const BtorIntHashTable * t)437 btor_iter_hashint_init (BtorIntHashTableIterator *it, const BtorIntHashTable *t)
438 {
439 assert (it);
440 assert (t);
441
442 it->cur_pos = 0;
443 it->t = t;
444 while (it->cur_pos < it->t->size && !it->t->keys[it->cur_pos])
445 it->cur_pos += 1;
446 }
447
448 bool
btor_iter_hashint_has_next(const BtorIntHashTableIterator * it)449 btor_iter_hashint_has_next (const BtorIntHashTableIterator *it)
450 {
451 assert (it);
452 return it->cur_pos < it->t->size;
453 }
454
455 int32_t
btor_iter_hashint_next(BtorIntHashTableIterator * it)456 btor_iter_hashint_next (BtorIntHashTableIterator *it)
457 {
458 assert (it);
459
460 int32_t res;
461
462 res = it->t->keys[it->cur_pos++];
463 while (it->cur_pos < it->t->size && !it->t->keys[it->cur_pos])
464 it->cur_pos += 1;
465 return res;
466 }
467
468 BtorHashTableData *
btor_iter_hashint_next_data(BtorIntHashTableIterator * it)469 btor_iter_hashint_next_data (BtorIntHashTableIterator *it)
470 {
471 assert (it);
472 assert (it->t->data);
473
474 BtorHashTableData *res;
475
476 res = &it->t->data[it->cur_pos++];
477 while (it->cur_pos < it->t->size && !it->t->keys[it->cur_pos])
478 it->cur_pos += 1;
479 return res;
480 }
481
482 /*------------------------------------------------------------------------*/
483