Skip to content

Commit 5eb010f

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 69bf02d commit 5eb010f

File tree

1 file changed

+160
-0
lines changed

1 file changed

+160
-0
lines changed

src/util/dense_integer_map.h

+160
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,160 @@
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+
21+
/// Identity functor. When we use C++20 this can be replaced with std::identity.
22+
template <typename T>
23+
class identity_functort
24+
{
25+
public:
26+
constexpr T &&operator()(T &&t) const
27+
{
28+
return std::forward<T>(t);
29+
}
30+
};
31+
32+
/// A map type that is backed by a vector, which relies on the ability to (a)
33+
/// see the keys that might be used in advance of their usage, and (b) map those
34+
/// keys onto a dense range of integers. You should specialise
35+
/// key_to_dense_integer for your key type before using. If it maps your keys
36+
/// onto too sparse a range, considerable memory will be wasted.
37+
///
38+
/// The type is optimised for fast lookups at the expense of flexibility.
39+
/// So far I've only implemented the support needed for use in
40+
/// cfg_basic_blockst. Due to the vector storage the precise interface of
41+
/// std::map is hard to achieve, but something close is practically achievable
42+
/// for the interested developer.
43+
template <class K, class V, class KeyToDenseInteger = identity_functort<K>>
44+
class dense_integer_mapt
45+
{
46+
public:
47+
typedef std::vector<K> possible_keyst;
48+
49+
private:
50+
std::size_t offset;
51+
typedef std::vector<V> backing_storet;
52+
std::vector<V> map;
53+
std::vector<bool> value_set;
54+
std::size_t n_values_set;
55+
possible_keyst possible_keys_vector;
56+
57+
std::size_t key_to_index(const K &key) const
58+
{
59+
std::size_t key_integer = KeyToDenseInteger{}(key);
60+
INVARIANT(key_integer >= offset, "index should be in range");
61+
return key_integer - offset;
62+
}
63+
64+
void mark_index_set(std::size_t index)
65+
{
66+
if(!value_set[index])
67+
{
68+
++n_values_set;
69+
value_set[index] = true;
70+
}
71+
}
72+
73+
public:
74+
dense_integer_mapt() : offset(0), n_values_set(0)
75+
{
76+
}
77+
78+
template <typename Iter>
79+
void setup_for_keys(Iter first, Iter last)
80+
{
81+
std::size_t highest_key = std::numeric_limits<std::size_t>::min();
82+
std::size_t lowest_key = std::numeric_limits<std::size_t>::max();
83+
std::unordered_set<std::size_t> seen_keys;
84+
for(Iter it = first; it != last; ++it)
85+
{
86+
std::size_t integer_key = KeyToDenseInteger{}(*it);
87+
highest_key = std::max(integer_key, highest_key);
88+
lowest_key = std::min(integer_key, lowest_key);
89+
INVARIANT(
90+
seen_keys.insert(integer_key).second,
91+
"keys for use in dense_integer_mapt must be unique");
92+
}
93+
94+
if(highest_key < lowest_key)
95+
{
96+
offset = 0;
97+
}
98+
else
99+
{
100+
offset = lowest_key;
101+
map.resize((highest_key - lowest_key) + 1);
102+
value_set.resize((highest_key - lowest_key) + 1);
103+
}
104+
105+
possible_keys_vector.insert(possible_keys_vector.end(), first, last);
106+
}
107+
108+
const V &at(const K &key) const
109+
{
110+
std::size_t index = key_to_index(key);
111+
INVARIANT(value_set[index], "map value should be set");
112+
return map.at(index);
113+
}
114+
V &at(const K &key)
115+
{
116+
std::size_t index = key_to_index(key);
117+
INVARIANT(value_set[index], "map value should be set");
118+
return map.at(index);
119+
}
120+
121+
const V &operator[](const K &key) const
122+
{
123+
std::size_t index = key_to_index(key);
124+
mark_index_set(index);
125+
return map.at(index);
126+
}
127+
V &operator[](const K &key)
128+
{
129+
std::size_t index = key_to_index(key);
130+
mark_index_set(index);
131+
return map.at(index);
132+
}
133+
134+
bool insert(const std::pair<const K, const V> &pair)
135+
{
136+
std::size_t index = key_to_index(pair.first);
137+
if(value_set[index])
138+
return false;
139+
mark_index_set(index);
140+
map.at(index) = pair.second;
141+
return true;
142+
}
143+
144+
std::size_t count(const K &key) const
145+
{
146+
return value_set[key_to_index(key)];
147+
}
148+
149+
std::size_t size() const
150+
{
151+
return n_values_set;
152+
}
153+
154+
const possible_keyst &possible_keys() const
155+
{
156+
return possible_keys_vector;
157+
}
158+
};
159+
160+
#endif // CPROVER_UTIL_DENSE_INTEGER_MAP_H

0 commit comments

Comments
 (0)