1 /*++
2 Copyright (c) 2006 Microsoft Corporation
3
4 Module Name:
5
6 map.h
7
8 Abstract:
9
10 Simple mapping based on the hashtable.
11
12 Author:
13
14 Leonardo de Moura (leonardo) 2006-10-14.
15
16 Revision History:
17
18 --*/
19 #pragma once
20
21 #include "util/hashtable.h"
22
23 template<typename Key, typename Value>
24 struct _key_data {
25 Key m_key;
26 Value m_value;
_key_data_key_data27 _key_data() {
28 }
_key_data_key_data29 _key_data(Key const & k):
30 m_key(k) {
31 }
_key_data_key_data32 _key_data(Key const & k, Value const & v):
33 m_key(k),
34 m_value(v) {
35 }
36 };
37
38 template<typename Entry, typename HashProc, typename EqProc>
39 class table2map {
40 public:
41 typedef Entry entry;
42 typedef typename Entry::key key;
43 typedef typename Entry::value value;
44 typedef typename Entry::key_data key_data;
45
46
47 struct entry_hash_proc : private HashProc {
entry_hash_procentry_hash_proc48 entry_hash_proc(HashProc const & p):
49 HashProc(p) {
50 }
51
operatorentry_hash_proc52 unsigned operator()(key_data const & d) const {
53 return HashProc::operator()(d.m_key);
54 }
55 };
56
57 struct entry_eq_proc : private EqProc {
entry_eq_procentry_eq_proc58 entry_eq_proc(EqProc const & p):
59 EqProc(p) {
60 }
61
operatorentry_eq_proc62 bool operator()(key_data const & d1, key_data const & d2) const {
63 return EqProc::operator()(d1.m_key, d2.m_key);
64 }
65 };
66
67 typedef core_hashtable<entry, entry_hash_proc, entry_eq_proc> table;
68
69 table m_table;
70
71 public:
72 table2map(HashProc const & h = HashProc(), EqProc const & e = EqProc()):
m_table(DEFAULT_HASHTABLE_INITIAL_CAPACITY,entry_hash_proc (h),entry_eq_proc (e))73 m_table(DEFAULT_HASHTABLE_INITIAL_CAPACITY, entry_hash_proc(h), entry_eq_proc(e)) {
74 }
75
76 typedef typename table::iterator iterator;
77
reset()78 void reset() {
79 m_table.reset();
80 }
81
finalize()82 void finalize() {
83 m_table.finalize();
84 }
85
empty()86 bool empty() const {
87 return m_table.empty();
88 }
89
size()90 unsigned size() const {
91 return m_table.size();
92 }
93
capacity()94 unsigned capacity() const {
95 return m_table.capacity();
96 }
97
begin()98 iterator begin() const {
99 return m_table.begin();
100 }
101
end()102 iterator end() const {
103 return m_table.end();
104 }
105
insert(key const & k,value const & v)106 void insert(key const & k, value const & v) {
107 m_table.insert(key_data(k, v));
108 }
109
insert_if_not_there_core(key const & k,value const & v,entry * & et)110 bool insert_if_not_there_core(key const & k, value const & v, entry *& et) {
111 return m_table.insert_if_not_there_core(key_data(k,v), et);
112 }
113
insert_if_not_there(key const & k,value const & v)114 value & insert_if_not_there(key const & k, value const & v) {
115 return m_table.insert_if_not_there2(key_data(k, v))->get_data().m_value;
116 }
117
insert_if_not_there3(key const & k,value const & v)118 entry * insert_if_not_there3(key const & k, value const & v) {
119 return m_table.insert_if_not_there2(key_data(k, v));
120 }
121
find_core(key const & k)122 entry * find_core(key const & k) const {
123 return m_table.find_core(key_data(k));
124 }
125
find(key const & k,value & v)126 bool find(key const & k, value & v) const {
127 entry * e = find_core(k);
128 if (e) {
129 v = e->get_data().m_value;
130 }
131 return (nullptr != e);
132 }
133
get(key const & k,value const & default_value)134 value const& get(key const& k, value const& default_value) const {
135 entry* e = find_core(k);
136 if (e) {
137 return e->get_data().m_value;
138 }
139 else {
140 return default_value;
141 }
142 }
143
find_iterator(key const & k)144 iterator find_iterator(key const & k) const {
145 return m_table.find(key_data(k));
146 }
147
find(key const & k)148 value const & find(key const& k) const {
149 entry * e = find_core(k);
150 SASSERT(e);
151 return e->get_data().m_value;
152 }
153
find(key const & k)154 value & find(key const& k) {
155 entry * e = find_core(k);
156 SASSERT(e);
157 return e->get_data().m_value;
158 }
159
160 value const& operator[](key const& k) const { return find(k); }
161
162 value& operator[](key const& k) { return find(k); }
163
164
contains(key const & k)165 bool contains(key const & k) const {
166 return find_core(k) != nullptr;
167 }
168
remove(key const & k)169 void remove(key const & k) {
170 m_table.remove(key_data(k));
171 }
172
erase(key const & k)173 void erase(key const & k) {
174 remove(k);
175 }
176
get_num_collision()177 unsigned long long get_num_collision() const { return m_table.get_num_collision(); }
178
swap(table2map & other)179 void swap(table2map & other) {
180 m_table.swap(other.m_table);
181 }
182
183 bool operator==(table2map const& other) const {
184 if (size() != other.size()) return false;
185 for (auto const& kv : *this) {
186 auto* e = other.find_core(kv.m_key);
187 if (!e) return false;
188 if (e->get_data().m_value != kv.m_value) return false;
189 }
190 return true;
191 }
192
193 #ifdef Z3DEBUG
194
check_invariant()195 bool check_invariant() {
196 return m_table.check_invariant();
197 }
198
199 #endif
200 };
201
202 template<typename Key, typename Value>
203 class default_map_entry : public default_hash_entry<_key_data<Key, Value> > {
204 public:
205 typedef Key key;
206 typedef Value value;
207 typedef _key_data<Key, Value> key_data;
208 };
209
210
211 template<typename Key, typename Value, typename HashProc, typename EqProc>
212 class map : public table2map<default_map_entry<Key, Value>, HashProc, EqProc> {
213 public:
214 map(HashProc const & h = HashProc(), EqProc const & e = EqProc()):
215 table2map<default_map_entry<Key, Value>, HashProc, EqProc>(h, e) {
216 }
217 };
218
219 template<typename Key, typename Value>
220 struct _key_ptr_data {
221 Key * m_key;
222 Value m_value;
_key_ptr_data_key_ptr_data223 _key_ptr_data():
224 m_key(0) {
225 }
_key_ptr_data_key_ptr_data226 _key_ptr_data(Key * k):
227 m_key(k) {
228 }
_key_ptr_data_key_ptr_data229 _key_ptr_data(Key * k, Value const & v):
230 m_key(k),
231 m_value(v) {
232 }
233 };
234
235 template<typename Key, typename Value>
236 class ptr_map_entry {
237 public:
238 typedef _key_ptr_data<Key, Value> key_data;
239 typedef _key_ptr_data<Key, Value> data;
240 private:
241 unsigned m_hash; //!< cached hash code
242 data m_data;
243 public:
244 typedef Key * key;
245 typedef Value value;
get_hash()246 unsigned get_hash() const { return m_hash; }
is_free()247 bool is_free() const { return m_data.m_key == 0; }
is_deleted()248 bool is_deleted() const { return m_data.m_key == reinterpret_cast<Key *>(1); }
is_used()249 bool is_used() const { return m_data.m_key != reinterpret_cast<Key *>(0) && m_data.m_key != reinterpret_cast<Key *>(1); }
get_data()250 key_data const & get_data() const { return m_data; }
get_data()251 key_data & get_data() { return m_data; }
set_data(key_data const & d)252 void set_data(key_data const & d) { m_data = d; }
set_hash(unsigned h)253 void set_hash(unsigned h) { m_hash = h; }
mark_as_deleted()254 void mark_as_deleted() { m_data.m_key = reinterpret_cast<Key *>(1); }
mark_as_free()255 void mark_as_free() { m_data.m_key = 0; }
256 };
257
258 template<typename Key, typename Value>
259 class ptr_addr_map_entry {
260 public:
261 typedef _key_ptr_data<Key, Value> key_data;
262 typedef _key_ptr_data<Key, Value> data;
263 private:
264 data m_data;
265 public:
266 typedef Key * key;
267 typedef Value value;
get_hash()268 unsigned get_hash() const { return get_ptr_hash(m_data.m_key); }
is_free()269 bool is_free() const { return m_data.m_key == 0; }
is_deleted()270 bool is_deleted() const { return m_data.m_key == reinterpret_cast<Key *>(1); }
is_used()271 bool is_used() const { return m_data.m_key != reinterpret_cast<Key *>(0) && m_data.m_key != reinterpret_cast<Key *>(1); }
get_data()272 key_data const & get_data() const { return m_data; }
get_data()273 key_data & get_data() { return m_data; }
set_data(key_data const & d)274 void set_data(key_data const & d) { m_data = d; }
set_hash(unsigned h)275 void set_hash(unsigned h) { SASSERT(h == get_ptr_hash(m_data.m_key)); /* do nothing */ }
mark_as_deleted()276 void mark_as_deleted() { m_data.m_key = reinterpret_cast<Key *>(1); }
mark_as_free()277 void mark_as_free() { m_data.m_key = 0; }
278 };
279
280 template<typename Key, typename Value>
281 class ptr_addr_map : public table2map<ptr_addr_map_entry<Key, Value>, ptr_hash<Key>, ptr_eq<Key> > {
282 public:
283 };
284
operatoru_hash285 struct u_hash { unsigned operator()(unsigned u) const { return u; } };
286
operatoru_eq287 struct u_eq { bool operator()(unsigned u1, unsigned u2) const { return u1 == u2; } };
288
289
operatoru64_hash290 struct u64_hash { unsigned operator()(uint64_t u) const { return mk_mix((unsigned)u, (unsigned)(u >> 32ull), 0); } };
291
operatoru64_eq292 struct u64_eq { bool operator()(uint64_t u1, uint64_t u2) const { return u1 == u2; } };
293
operatorsize_t_eq294 struct size_t_eq { bool operator()(size_t u1, size_t u2) const { return u1 == u2; } };
295
operatorint_eq296 struct int_eq { bool operator()(int u1, int u2) const { return u1 == u2; } };
297
298 template<typename Value>
299 class u_map : public map<unsigned, Value, u_hash, u_eq> {};
300
301 template<typename Value>
302 class size_t_map : public map<size_t, Value, size_t_hash, size_t_eq> {};
303
304 template<typename Value>
305 class u64_map : public map<uint64_t, Value, u64_hash, u64_eq> {};
306
307