CBMC
|
A map type that is backed by a vector, which relies on the ability to (a) see the keys that might be used in advance of their usage, and (b) map those keys onto a dense range of integers. More...
#include <dense_integer_map.h>
Classes | |
class | iterator_templatet |
Public Types | |
typedef std::vector< K > | possible_keyst |
Type of the container returned by possible_keys. More... | |
typedef iterator_templatet< typename backing_storet::iterator, typename backing_storet::value_type > | iterator |
iterator. More... | |
typedef iterator_templatet< typename backing_storet::const_iterator, const typename backing_storet::value_type > | const_iterator |
const iterator. More... | |
Public Member Functions | |
dense_integer_mapt () | |
template<typename Iter > | |
void | setup_for_keys (Iter first, Iter last) |
Set the keys that are allowed to be used in this container. More... | |
const V & | at (const K &key) const |
V & | at (const K &key) |
V & | operator[] (const K &key) |
std::pair< iterator, bool > | insert (const std::pair< const K, V > &pair) |
std::size_t | count (const K &key) const |
std::size_t | size () const |
const possible_keyst & | possible_keys () const |
iterator | begin () |
iterator | end () |
const_iterator | begin () const |
const_iterator | end () const |
const_iterator | cbegin () const |
const_iterator | cend () const |
Private Types | |
typedef std::vector< std::pair< K, V > > | backing_storet |
Private Member Functions | |
std::size_t | key_to_index (const K &key) const |
void | mark_index_set (std::size_t index) |
bool | index_is_set (std::size_t index) const |
Private Attributes | |
int64_t | offset |
backing_storet | map |
std::vector< bool > | value_set |
std::size_t | n_values_set |
possible_keyst | possible_keys_vector |
A map type that is backed by a vector, which relies on the ability to (a) see the keys that might be used in advance of their usage, and (b) map those keys onto a dense range of integers.
You should specialise key_to_dense_integer for your key type before using. If it maps your keys onto too sparse a range, considerable memory will be wasted, as well as time spent skipping over the unused indices while iterating.
Value type V must be default constructible.
The type is optimised for fast lookups at the expense of flexibility. It makes one compromise on the iterface of std::map / unordered_map: the iterator refers to a pair<key, std::optional<value>>, where the value optional will always be defined. This is because the backing store uses std::optional this way and we don't want to impose the price of copying the key and value each time we move the iterator just so we have a <const K, V> & to give out.
Undocumented functions with matching names have the same semantics as std::map equivalents (including perfect iterator stability, with ordering according to the given KeyToDenseInteger function)
Definition at line 54 of file dense_integer_map.h.
|
private |
Definition at line 65 of file dense_integer_map.h.
typedef iterator_templatet< typename backing_storet::const_iterator, const typename backing_storet::value_type> dense_integer_mapt< K, V, KeyToDenseInteger >::const_iterator |
const iterator.
Stable with respect to all operations on this type once setup_for_keys has been called.
Definition at line 218 of file dense_integer_map.h.
typedef iterator_templatet< typename backing_storet::iterator, typename backing_storet::value_type> dense_integer_mapt< K, V, KeyToDenseInteger >::iterator |
iterator.
Stable with respect to all operations on this type once setup_for_keys has been called.
Definition at line 211 of file dense_integer_map.h.
typedef std::vector<K> dense_integer_mapt< K, V, KeyToDenseInteger >::possible_keyst |
Type of the container returned by possible_keys.
Definition at line 58 of file dense_integer_map.h.
|
inline |
Definition at line 220 of file dense_integer_map.h.
|
inline |
Definition at line 280 of file dense_integer_map.h.
|
inline |
Definition at line 274 of file dense_integer_map.h.
|
inline |
Definition at line 326 of file dense_integer_map.h.
|
inline |
Definition at line 336 of file dense_integer_map.h.
|
inline |
Definition at line 346 of file dense_integer_map.h.
|
inline |
Definition at line 351 of file dense_integer_map.h.
|
inline |
Definition at line 311 of file dense_integer_map.h.
|
inline |
Definition at line 331 of file dense_integer_map.h.
|
inline |
Definition at line 341 of file dense_integer_map.h.
|
inlineprivate |
Definition at line 110 of file dense_integer_map.h.
|
inline |
Definition at line 294 of file dense_integer_map.h.
|
inlineprivate |
Definition at line 90 of file dense_integer_map.h.
|
inlineprivate |
Definition at line 100 of file dense_integer_map.h.
|
inline |
Definition at line 287 of file dense_integer_map.h.
|
inline |
Definition at line 321 of file dense_integer_map.h.
|
inline |
Set the keys that are allowed to be used in this container.
Checks that the integers produced for each key by KeyToDenseInteger
are unique and fall within a std::size_t's range (the integers are allowed to be negative so long as max(integers) - min(integers) <= max-size_t). This should be called before the container is used and not called again. Using keys not provided to this function with operator[], insert, at(...) etc may cause an invariant failure or undefined behaviour.
Definition at line 232 of file dense_integer_map.h.
|
inline |
Definition at line 316 of file dense_integer_map.h.
|
private |
Definition at line 71 of file dense_integer_map.h.
|
private |
Definition at line 82 of file dense_integer_map.h.
|
private |
Definition at line 63 of file dense_integer_map.h.
|
private |
Definition at line 87 of file dense_integer_map.h.
|
private |
Definition at line 78 of file dense_integer_map.h.