12 #ifndef CPROVER_UTIL_DENSE_INTEGER_MAP_H
13 #define CPROVER_UTIL_DENSE_INTEGER_MAP_H
16 #include <unordered_set>
29 return std::forward<T>(t);
52 template <
class K,
class V,
class KeyToDenseInteger =
identity_functort>
91 auto key_integer = KeyToDenseInteger{}(key);
92 INVARIANT(((int64_t)key_integer) >=
offset,
"index should be in range");
93 auto ret = (std::size_t)key_integer - (std::size_t)
offset;
117 template <
class UnderlyingIterator,
class UnderlyingValue>
119 :
public std::iterator<std::forward_iterator_tag, UnderlyingValue>
122 typedef std::iterator<std::forward_iterator_tag, UnderlyingValue>
139 typename backing_storet::const_iterator,
140 const typename backing_storet::value_type>()
const
175 UnderlyingIterator
advance(UnderlyingIterator it)
183 auto iterator_pos = (std::size_t)std::distance(
185 (
typename backing_storet::const_iterator)it);
204 typename backing_storet::iterator,
205 typename backing_storet::value_type>
210 typedef iterator_templatet<
211 typename backing_storet::const_iterator,
212 const typename backing_storet::value_type>
226 template <
typename Iter>
231 "setup_for_keys must only be called on a newly-constructed container");
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)
238 int64_t integer_key = (int64_t)KeyToDenseInteger{}(*it);
239 highest_key = std::max(integer_key, highest_key);
240 lowest_key = std::min(integer_key, lowest_key);
242 seen_keys.insert(integer_key).second,
243 "keys for use in dense_integer_mapt must be unique");
246 if(highest_key < lowest_key)
252 std::size_t map_size = (std::size_t)((highest_key - lowest_key) + 1);
255 "dense_integer_mapt size should fit in std::size_t");
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)
269 const V &
at(
const K &key)
const
273 return map.at(index).second;
279 return map.at(index).second;
286 return map.at(index).second;
289 std::pair<iterator, bool>
insert(
const std::pair<const K, V> &pair)
293 static_cast<typename backing_storet::iterator::difference_type
>(index);
294 iterator it{std::next(
map.begin(), signed_index), *
this};
301 map.at(index).second = pair.second;
306 std::size_t
count(
const K &key)
const
352 #endif // CPROVER_UTIL_DENSE_INTEGER_MAP_H