Skip to content

Commit 8887378

Browse files
committed
Add dense_integer_mapt type
This gives a map-like interface but vector-like lookup cost, ideal for mapping keys that have a bijection with densely packed integers, such as the location numbers of a well-formed goto_modelt or goto_programt.
1 parent aba7e75 commit 8887378

File tree

1 file changed

+296
-0
lines changed

1 file changed

+296
-0
lines changed

src/util/dense_integer_map.h

Lines changed: 296 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,296 @@
1+
/*******************************************************************\
2+
3+
Module: Dense integer map
4+
5+
Author: Diffblue Ltd
6+
7+
\*******************************************************************/
8+
9+
/// \file
10+
/// Dense integer map
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+
22+
/// Identity functor. When we use C++20 this can be replaced with std::identity.
23+
class identity_functort
24+
{
25+
public:
26+
template <typename T>
27+
constexpr T &&operator()(T &&t) const
28+
{
29+
return std::forward<T>(t);
30+
}
31+
};
32+
33+
/// A map type that is backed by a vector, which relies on the ability to (a)
34+
/// see the keys that might be used in advance of their usage, and (b) map those
35+
/// keys onto a dense range of integers. You should specialise
36+
/// key_to_dense_integer for your key type before using. If it maps your keys
37+
/// onto too sparse a range, considerable memory will be wasted, as well as time
38+
/// spent skipping over the unused indices while iterating.
39+
///
40+
/// Value type V must be default constructible.
41+
///
42+
/// The type is optimised for fast lookups at the expense of flexibility.
43+
/// It makes one compromise on the iterface of std::map / unordered_map: the
44+
/// iterator refers to a pair<key, optionalt<value>>, where the value optional
45+
/// will always be defined. This is because the backing store uses optionalt
46+
/// this way and we don't want to impose the price of copying the key and value
47+
/// each time we move the iterator just so we have a <const K, V> & to give out.
48+
template <class K, class V, class KeyToDenseInteger = identity_functort>
49+
class dense_integer_mapt
50+
{
51+
public:
52+
typedef std::vector<K> possible_keyst;
53+
54+
private:
55+
int64_t offset;
56+
typedef std::vector<std::pair<K, V>> backing_storet;
57+
backing_storet map;
58+
std::vector<bool> value_set;
59+
std::size_t n_values_set;
60+
possible_keyst possible_keys_vector;
61+
62+
std::size_t key_to_index(const K &key) const
63+
{
64+
auto key_integer = KeyToDenseInteger{}(key);
65+
INVARIANT(((int64_t)key_integer) >= offset, "index should be in range");
66+
auto ret = (std::size_t)key_integer - offset;
67+
INVARIANT(ret < map.size(), "index should be in range");
68+
return ret;
69+
}
70+
71+
void mark_index_set(std::size_t index)
72+
{
73+
if(!value_set[index])
74+
{
75+
++n_values_set;
76+
value_set[index] = true;
77+
}
78+
}
79+
80+
bool index_is_set(std::size_t index) const
81+
{
82+
return value_set[index];
83+
}
84+
85+
public:
86+
template <class UnderlyingIterator, class UnderlyingValue>
87+
class iterator_templatet
88+
: public std::iterator<std::forward_iterator_tag, UnderlyingValue>
89+
{
90+
typedef std::iterator<std::forward_iterator_tag, UnderlyingValue>
91+
base_typet;
92+
typedef iterator_templatet<UnderlyingIterator, UnderlyingValue> self_typet;
93+
typedef dense_integer_mapt<K, V, KeyToDenseInteger> map_typet;
94+
95+
public:
96+
iterator_templatet(UnderlyingIterator it, const map_typet &underlying_map)
97+
: underlying_iterator(it), underlying_map(underlying_map)
98+
{
99+
it = skip_unset_values(it);
100+
}
101+
102+
// Convert iterator to const_iterator
103+
// (redundant when defined in the const_iterator itself)
104+
operator iterator_templatet<
105+
typename backing_storet::const_iterator,
106+
const typename backing_storet::value_type>() const
107+
{
108+
return {underlying_iterator, underlying_map};
109+
}
110+
111+
self_typet operator++()
112+
{
113+
self_typet i = *this;
114+
underlying_iterator = advance(underlying_iterator);
115+
return i;
116+
}
117+
self_typet operator++(int junk)
118+
{
119+
underlying_iterator = advance(underlying_iterator);
120+
return *this;
121+
}
122+
typename base_typet::reference operator*() const
123+
{
124+
return *underlying_iterator;
125+
}
126+
typename base_typet::pointer operator->() const
127+
{
128+
return &*underlying_iterator;
129+
}
130+
bool operator==(const self_typet &rhs) const
131+
{
132+
return underlying_iterator == rhs.underlying_iterator;
133+
}
134+
bool operator!=(const self_typet &rhs) const
135+
{
136+
return underlying_iterator != rhs.underlying_iterator;
137+
}
138+
139+
private:
140+
UnderlyingIterator advance(UnderlyingIterator it)
141+
{
142+
return skip_unset_values(std::next(it));
143+
}
144+
145+
UnderlyingIterator skip_unset_values(UnderlyingIterator it)
146+
{
147+
auto iterator_pos = std::distance(
148+
underlying_map.map.begin(),
149+
(typename backing_storet::const_iterator)it);
150+
while((std::size_t)iterator_pos < underlying_map.map.size() &&
151+
!underlying_map.value_set.at(iterator_pos))
152+
{
153+
++iterator_pos;
154+
++it;
155+
}
156+
return it;
157+
}
158+
159+
UnderlyingIterator underlying_iterator;
160+
const map_typet &underlying_map;
161+
};
162+
163+
typedef iterator_templatet<
164+
typename backing_storet::iterator,
165+
typename backing_storet::value_type>
166+
iterator;
167+
typedef iterator_templatet<
168+
typename backing_storet::const_iterator,
169+
const typename backing_storet::value_type>
170+
const_iterator;
171+
172+
dense_integer_mapt() : offset(0), n_values_set(0)
173+
{
174+
}
175+
176+
template <typename Iter>
177+
void setup_for_keys(Iter first, Iter last)
178+
{
179+
int64_t highest_key = std::numeric_limits<int64_t>::min();
180+
int64_t lowest_key = std::numeric_limits<int64_t>::max();
181+
std::unordered_set<int64_t> seen_keys;
182+
for(Iter it = first; it != last; ++it)
183+
{
184+
int64_t integer_key = KeyToDenseInteger{}(*it);
185+
highest_key = std::max(integer_key, highest_key);
186+
lowest_key = std::min(integer_key, lowest_key);
187+
INVARIANT(
188+
seen_keys.insert(integer_key).second,
189+
"keys for use in dense_integer_mapt must be unique");
190+
}
191+
192+
if(highest_key < lowest_key)
193+
{
194+
offset = 0;
195+
}
196+
else
197+
{
198+
auto map_size = (highest_key - lowest_key) + 1;
199+
INVARIANT(
200+
map_size > 0, // overflowed?
201+
"dense_integer_mapt size should fit in std::size_t");
202+
INVARIANT(
203+
((std::size_t)map_size) <= std::numeric_limits<std::size_t>::max(),
204+
"dense_integer_mapt size should fit in std::size_t");
205+
offset = lowest_key;
206+
map.resize((highest_key - lowest_key) + 1);
207+
for(Iter it = first; it != last; ++it)
208+
map.at(key_to_index(*it)).first = *it;
209+
value_set.resize((highest_key - lowest_key) + 1);
210+
}
211+
212+
possible_keys_vector.insert(possible_keys_vector.end(), first, last);
213+
}
214+
215+
const V &at(const K &key) const
216+
{
217+
std::size_t index = key_to_index(key);
218+
INVARIANT(index_is_set(index), "map value should be set");
219+
return map.at(index).second;
220+
}
221+
V &at(const K &key)
222+
{
223+
std::size_t index = key_to_index(key);
224+
INVARIANT(index_is_set(index), "map value should be set");
225+
return map.at(index).second;
226+
}
227+
228+
V &operator[](const K &key)
229+
{
230+
std::size_t index = key_to_index(key);
231+
mark_index_set(index);
232+
return map.at(index).second;
233+
}
234+
235+
std::pair<iterator, bool> insert(const std::pair<const K, V> &pair)
236+
{
237+
std::size_t index = key_to_index(pair.first);
238+
iterator it{std::next(map.begin(), index), *this};
239+
240+
if(index_is_set(index))
241+
return {it, false};
242+
else
243+
{
244+
mark_index_set(index);
245+
map.at(index).second = pair.second;
246+
return {it, true};
247+
}
248+
}
249+
250+
std::size_t count(const K &key) const
251+
{
252+
return index_is_set(key_to_index(key));
253+
}
254+
255+
std::size_t size() const
256+
{
257+
return n_values_set;
258+
}
259+
260+
const possible_keyst &possible_keys() const
261+
{
262+
return possible_keys_vector;
263+
}
264+
265+
iterator begin()
266+
{
267+
return iterator{map.begin(), *this};
268+
}
269+
270+
iterator end()
271+
{
272+
return iterator{map.end(), *this};
273+
}
274+
275+
const_iterator begin() const
276+
{
277+
return const_iterator{map.begin(), *this};
278+
}
279+
280+
const_iterator end() const
281+
{
282+
return const_iterator{map.end(), *this};
283+
}
284+
285+
const_iterator cbegin() const
286+
{
287+
return begin();
288+
}
289+
290+
const_iterator cend() const
291+
{
292+
return end();
293+
}
294+
};
295+
296+
#endif // CPROVER_UTIL_DENSE_INTEGER_MAP_H

0 commit comments

Comments
 (0)