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 #ifndef __BACKTRACK_INT_HASH_MAP_H
26 #define __BACKTRACK_INT_HASH_MAP_H
27
28 #include <stdint.h>
29
30
31 /*
32 * Records stored in the table
33 */
34 typedef struct back_hmap_elem_s {
35 int32_t key;
36 int32_t val;
37 } back_hmap_elem_t;
38
39
40 /*
41 * Markers for empty and deleted pairs
42 */
43 enum {
44 BACK_HMAP_EMPTY_KEY = -1,
45 BACK_HMAP_DELETED_KEY = -2,
46 };
47
48
49 /*
50 * map = two arrays of the same size
51 * - pair = array of pairs (key, value)
52 * - level = array of unsigned integer
53 * - if pair[i] contains a pair (k, v) with k>=0
54 * then level[i] is the base_level at which the pair was added to the table.
55 * - when we backtrack from a level b, we delete pair[i] if level[i] == b.
56 */
57 typedef struct back_hmap_data_s {
58 back_hmap_elem_t *pair;
59 uint32_t *level;
60 } back_hmap_data_t;
61
62
63 /*
64 * Full table: size is a power of 2
65 * - nelems = number of elements stored in the table (i.e., data.pair[i].key >= 0)
66 * - ndeleted = number of deleted elements (i.e., data.pair[i].key == -2).
67 */
68 typedef struct back_hmap_s {
69 back_hmap_data_t data;
70 uint32_t size;
71 uint32_t nelems;
72 uint32_t ndeleted;
73 uint32_t resize_threshold;
74 uint32_t cleanup_threshold;
75 uint32_t level;
76 } back_hmap_t;
77
78
79 #define BACK_HMAP_DEF_SIZE 32
80 #define BACK_HMAP_MAX_SIZE (UINT32_MAX/sizeof(back_hmap_elem_t))
81
82 #define BACK_HMAP_RESIZE_RATIO 0.6
83 #define BACK_HMAP_CLEANUP_RATIO 0.2
84
85
86 /*
87 * Initialization
88 * - n = initialize size. It must be 0 or a power of 2.
89 * - if n is zero, the default is used.
90 * - base_level is set to 0.
91 */
92 extern void init_back_hmap(back_hmap_t *hmap, uint32_t n);
93
94
95 /*
96 * Delete: free memory
97 */
98 extern void delete_back_hmap(back_hmap_t *hmap);
99
100
101 /*
102 * Reset: empty the table and reset level to 0
103 */
104 extern void reset_back_hmap(back_hmap_t *hmap);
105
106
107 /*
108 * Increase level
109 */
back_hmap_push(back_hmap_t * hmap)110 static inline void back_hmap_push(back_hmap_t *hmap) {
111 hmap->level ++;
112 }
113
114
115 /*
116 * Set the level to n
117 * - this can be use to set the initial level to something other than 0.
118 */
back_hmap_set_level(back_hmap_t * hmap,uint32_t n)119 static inline void back_hmap_set_level(back_hmap_t *hmap, uint32_t n) {
120 hmap->level = n;
121 }
122
123
124 /*
125 * Backtrack to the previous level: remove all elements
126 * added at the current level.
127 * - hmap->level must be positive
128 */
129 extern void back_hmap_pop(back_hmap_t *hmap);
130
131
132 /*
133 * Find record with key k. Return NULL if this key is not in the map.
134 */
135 extern back_hmap_elem_t *back_hmap_find(const back_hmap_t *hmap, int32_t k);
136
137
138 /*
139 * Get record with key k. If there's no such record, create a new one
140 * with key = k, val = -1, and level = current hmap level.
141 */
142 extern back_hmap_elem_t *back_hmap_get(back_hmap_t *hmap, int32_t k);
143
144
145 #endif /* __BACKTRACK_INT_HASH_MAP_H */
146