Skip to content

Commit 18ba777

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 b625e0a commit 18ba777

File tree

1 file changed

+141
-0
lines changed

1 file changed

+141
-0
lines changed

Diff for: src/util/dense_integer_map.h

+141
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,141 @@
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 <vector>
17+
18+
#include <util/invariant.h>
19+
20+
/// Hash-like function that is expected to turn a key type into a dense integer
21+
/// without losing information (e.g. for a given instance of dense_integer_mapt,
22+
/// using a function that maps 1000 keys onto the range 1000000 - 1005000 would
23+
/// be acceptable)
24+
/// For small integer types, or large integers that you know will fall into a
25+
/// small range for a given use case, the identity function suffices.
26+
template <typename T>
27+
std::size_t key_to_dense_integer(const T &);
28+
29+
/// A map type that is backed by a vector, which relies on the ability to (a)
30+
/// see the keys that might be used in advance of their usage, and (b) map those
31+
/// keys onto a dense range of integers. You should specialise
32+
/// key_to_dense_integer for your key type before using. If it maps your keys
33+
/// onto too sparse a range, considerable memory will be wasted.
34+
///
35+
/// The type is optimised for fast lookups at the expense of flexibility.
36+
/// So far I've only implemented the support needed for use in
37+
/// cfg_basic_blockst. Due to the vector storage the precise interface of
38+
/// std::map is hard to achieve, but something close is practically achievable
39+
/// for the interested developer.
40+
template <class K, class V>
41+
class dense_integer_mapt
42+
{
43+
std::size_t offset;
44+
typedef std::vector<V> backing_storet;
45+
std::vector<V> map;
46+
std::vector<bool> value_set;
47+
std::size_t n_values_set;
48+
49+
std::size_t key_to_index(const K &key) const
50+
{
51+
std::size_t key_integer = key_to_dense_integer(key);
52+
INVARIANT(key_integer >= offset, "index should be in range");
53+
return key_integer - offset;
54+
}
55+
56+
void mark_index_set(std::size_t index)
57+
{
58+
if(!value_set[index])
59+
{
60+
++n_values_set;
61+
value_set[index] = true;
62+
}
63+
}
64+
65+
public:
66+
dense_integer_mapt() : offset(0), n_values_set(0)
67+
{
68+
}
69+
70+
template <typename Iter>
71+
void setup_for_keys(Iter first, Iter last)
72+
{
73+
std::size_t highest_key = std::numeric_limits<std::size_t>::min();
74+
std::size_t lowest_key = std::numeric_limits<std::size_t>::max();
75+
for(Iter it = first; it != last; ++it)
76+
{
77+
std::size_t integer_key = key_to_dense_integer(*it);
78+
highest_key = std::max(integer_key, highest_key);
79+
lowest_key = std::min(integer_key, lowest_key);
80+
}
81+
82+
if(highest_key < lowest_key)
83+
{
84+
offset = 0;
85+
}
86+
else
87+
{
88+
offset = lowest_key;
89+
map.resize((highest_key - lowest_key) + 1);
90+
value_set.resize((highest_key - lowest_key) + 1);
91+
}
92+
}
93+
94+
const V &at(const K &key) const
95+
{
96+
std::size_t index = key_to_index(key);
97+
INVARIANT(value_set[index], "map value should be set");
98+
return map.at(index);
99+
}
100+
V &at(const K &key)
101+
{
102+
std::size_t index = key_to_index(key);
103+
INVARIANT(value_set[index], "map value should be set");
104+
return map.at(index);
105+
}
106+
107+
const V &operator[](const K &key) const
108+
{
109+
std::size_t index = key_to_index(key);
110+
mark_index_set(index);
111+
return map.at(index);
112+
}
113+
V &operator[](const K &key)
114+
{
115+
std::size_t index = key_to_index(key);
116+
mark_index_set(index);
117+
return map.at(index);
118+
}
119+
120+
bool insert(const std::pair<const K, const V> &pair)
121+
{
122+
std::size_t index = key_to_index(pair.first);
123+
if(value_set[index])
124+
return false;
125+
mark_index_set(index);
126+
map.at(index) = pair.second;
127+
return true;
128+
}
129+
130+
std::size_t count(const K &key) const
131+
{
132+
return value_set[key_to_index(key)];
133+
}
134+
135+
std::size_t size() const
136+
{
137+
return n_values_set;
138+
}
139+
};
140+
141+
#endif // CPROVER_UTIL_DENSE_INTEGER_MAP_H

0 commit comments

Comments
 (0)