cprover
Loading...
Searching...
No Matches
dense_integer_map.h
Go to the documentation of this file.
1/*******************************************************************\
2
3Module: Dense integer map
4
5Author: Diffblue Ltd
6
7\*******************************************************************/
8
11
12#ifndef CPROVER_UTIL_DENSE_INTEGER_MAP_H
13#define CPROVER_UTIL_DENSE_INTEGER_MAP_H
14
15#include <limits>
16#include <unordered_set>
17#include <vector>
18
19#include <util/invariant.h>
20#include <util/optional.h>
21
24{
25public:
26 template <typename T>
27 constexpr T &&operator()(T &&t) const
28 {
29 return std::forward<T>(t);
30 }
31};
32
52template <class K, class V, class KeyToDenseInteger = identity_functort>
54{
55public:
57 typedef std::vector<K> possible_keyst;
58
59private:
60 // Offset between keys resulting from KeyToDenseInteger{}(key) and indices
61 // into map.
63
64 typedef std::vector<std::pair<K, V>> backing_storet;
65
66 // Main store: contains <key, value> pairs, where entries at positions with
67 // no corresponding key are default-initialized and entries with a
68 // corresponding key but no value set yet have the correct key but a default-
69 // initialized value. Both of these are skipped by this type's iterators.
71
72 // Indicates whether a given position in \ref map's value has been set, and
73 // therefore whether our iterators should stop at a given location. We use
74 // this auxiliary structure rather than `pair<K, optionalt<V>>` in \ref map
75 // because this way we can more easily return a std::map-like
76 // std::pair<const K, V> & from the iterator.
77 std::vector<bool> value_set;
78
79 // Population count (number of '1's) in value_set, i.e., number of keys whose
80 // values have been set.
81 std::size_t n_values_set;
82
83 // "Allowed" keys passed to \ref setup_for_keys. Attempting to use keys not
84 // included in this vector may result in an invariant failure, but can
85 // sometimes silently succeed
87
88 // Convert a key into an index into \ref map
89 std::size_t key_to_index(const K &key) const
90 {
92 INVARIANT(((int64_t)key_integer) >= offset, "index should be in range");
93 auto ret = (std::size_t)key_integer - (std::size_t)offset;
94 INVARIANT(ret < map.size(), "index should be in range");
95 return ret;
96 }
97
98 // Note that \ref map entry at offset \ref index has been set.
99 void mark_index_set(std::size_t index)
100 {
101 if(!value_set[index])
102 {
103 ++n_values_set;
104 value_set[index] = true;
105 }
106 }
107
108 // Has the \ref map entry at offset \ref index been set?
109 bool index_is_set(std::size_t index) const
110 {
111 return value_set[index];
112 }
113
114 // Support class used to implement both const and non-const iterators
115 // This is just a std::vector iterator pointing into \ref map, but with an
116 // operator++ that skips unset values.
117 template <class UnderlyingIterator, class UnderlyingValue>
119 : public std::iterator<std::forward_iterator_tag, UnderlyingValue>
120 {
121 // Type of the std::iterator support class we inherit
122 typedef std::iterator<std::forward_iterator_tag, UnderlyingValue>
124 // Type of this template instantiation
126 // Type of our containing \ref dense_integer_mapt
128
129 public:
135
139 typename backing_storet::const_iterator,
140 const typename backing_storet::value_type>() const
141 {
143 }
144
146 {
147 self_typet i = *this;
149 return i;
150 }
152 {
154 return *this;
155 }
156 typename base_typet::reference operator*() const
157 {
158 return *underlying_iterator;
159 }
160 typename base_typet::pointer operator->() const
161 {
162 return &*underlying_iterator;
163 }
164 bool operator==(const self_typet &rhs) const
165 {
166 return underlying_iterator == rhs.underlying_iterator;
167 }
168 bool operator!=(const self_typet &rhs) const
169 {
170 return underlying_iterator != rhs.underlying_iterator;
171 }
172
173 private:
174 // Advance \ref it to the next map entry with an initialized value
176 {
177 return skip_unset_values(std::next(it));
178 }
179
180 // Return the next iterator >= it with its value set
182 {
183 auto iterator_pos = (std::size_t)std::distance(
184 underlying_map.map.begin(),
185 (typename backing_storet::const_iterator)it);
186 while((std::size_t)iterator_pos < underlying_map.map.size() &&
187 !underlying_map.value_set.at(iterator_pos))
188 {
189 ++iterator_pos;
190 ++it;
191 }
192 return it;
193 }
194
195 // Wrapped std::vector iterator
198 };
199
200public:
203 typedef iterator_templatet<
204 typename backing_storet::iterator,
205 typename backing_storet::value_type>
207
210 typedef iterator_templatet<
211 typename backing_storet::const_iterator,
212 const typename backing_storet::value_type>
214
216 {
217 }
218
226 template <typename Iter>
228 {
229 INVARIANT(
230 size() == 0,
231 "setup_for_keys must only be called on a newly-constructed container");
232
233 int64_t highest_key = std::numeric_limits<int64_t>::min();
234 int64_t lowest_key = std::numeric_limits<int64_t>::max();
235 std::unordered_set<int64_t> seen_keys;
236 for(Iter it = first; it != last; ++it)
237 {
240 lowest_key = std::min(integer_key, lowest_key);
241 INVARIANT(
242 seen_keys.insert(integer_key).second,
243 "keys for use in dense_integer_mapt must be unique");
244 }
245
247 {
248 offset = 0;
249 }
250 else
251 {
252 std::size_t map_size = (std::size_t)((highest_key - lowest_key) + 1);
253 INVARIANT(
254 map_size > 0, // overflowed?
255 "dense_integer_mapt size should fit in std::size_t");
256 INVARIANT(
257 map_size <= std::numeric_limits<std::size_t>::max(),
258 "dense_integer_mapt size should fit in std::size_t");
260 map.resize(map_size);
261 for(Iter it = first; it != last; ++it)
262 map.at(key_to_index(*it)).first = *it;
263 value_set.resize(map_size);
264 }
265
266 possible_keys_vector.insert(possible_keys_vector.end(), first, last);
267 }
268
269 const V &at(const K &key) const
270 {
271 std::size_t index = key_to_index(key);
272 INVARIANT(index_is_set(index), "map value should be set");
273 return map.at(index).second;
274 }
275 V &at(const K &key)
276 {
277 std::size_t index = key_to_index(key);
278 INVARIANT(index_is_set(index), "map value should be set");
279 return map.at(index).second;
280 }
281
282 V &operator[](const K &key)
283 {
284 std::size_t index = key_to_index(key);
285 mark_index_set(index);
286 return map.at(index).second;
287 }
288
289 std::pair<iterator, bool> insert(const std::pair<const K, V> &pair)
290 {
291 auto index = key_to_index(pair.first);
292 auto signed_index =
293 static_cast<typename backing_storet::iterator::difference_type>(index);
294 iterator it{std::next(map.begin(), signed_index), *this};
295
296 if(index_is_set(index))
297 return {it, false};
298 else
299 {
300 mark_index_set(index);
301 map.at(index).second = pair.second;
302 return {it, true};
303 }
304 }
305
306 std::size_t count(const K &key) const
307 {
309 }
310
311 std::size_t size() const
312 {
313 return n_values_set;
314 }
315
317 {
319 }
320
322 {
323 return iterator{map.begin(), *this};
324 }
325
327 {
328 return iterator{map.end(), *this};
329 }
330
332 {
333 return const_iterator{map.begin(), *this};
334 }
335
337 {
338 return const_iterator{map.end(), *this};
339 }
340
342 {
343 return begin();
344 }
345
347 {
348 return end();
349 }
350};
351
352#endif // CPROVER_UTIL_DENSE_INTEGER_MAP_H
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
Definition ai.h:563
base_typet::reference operator*() const
base_typet::pointer operator->() const
iterator_templatet< UnderlyingIterator, UnderlyingValue > self_typet
std::iterator< std::forward_iterator_tag, UnderlyingValue > base_typet
iterator_templatet(UnderlyingIterator it, const map_typet &underlying_map)
bool operator==(const self_typet &rhs) const
bool operator!=(const self_typet &rhs) const
dense_integer_mapt< K, V, KeyToDenseInteger > map_typet
UnderlyingIterator skip_unset_values(UnderlyingIterator it)
UnderlyingIterator advance(UnderlyingIterator it)
A map type that is backed by a vector, which relies on the ability to (a) see the keys that might be ...
std::pair< iterator, bool > insert(const std::pair< const K, V > &pair)
void setup_for_keys(Iter first, Iter last)
Set the keys that are allowed to be used in this container.
const_iterator cbegin() const
void mark_index_set(std::size_t index)
std::vector< K > possible_keyst
Type of the container returned by possible_keys.
iterator_templatet< typename backing_storet::const_iterator, const typename backing_storet::value_type > const_iterator
const iterator.
possible_keyst possible_keys_vector
std::size_t count(const K &key) const
iterator_templatet< typename backing_storet::iterator, typename backing_storet::value_type > iterator
iterator.
V & at(const K &key)
const possible_keyst & possible_keys() const
V & operator[](const K &key)
bool index_is_set(std::size_t index) const
const V & at(const K &key) const
const_iterator cend() const
std::size_t key_to_index(const K &key) const
std::vector< std::pair< K, V > > backing_storet
const_iterator end() const
std::size_t size() const
const_iterator begin() const
std::vector< bool > value_set
Identity functor. When we use C++20 this can be replaced with std::identity.
constexpr T && operator()(T &&t) const
#define INVARIANT(CONDITION, REASON)
This macro uses the wrapper function 'invariant_violated_string'.
Definition invariant.h:423