CBMC
dense_integer_mapt< K, V, KeyToDenseInteger > Class Template Reference

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>

+ Inheritance diagram for dense_integer_mapt< K, V, KeyToDenseInteger >:
+ Collaboration diagram for dense_integer_mapt< K, V, KeyToDenseInteger >:

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_keystpossible_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
 

Detailed Description

template<class K, class V, class KeyToDenseInteger = identity_functort>
class dense_integer_mapt< K, V, KeyToDenseInteger >

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.

Member Typedef Documentation

◆ backing_storet

template<class K , class V , class KeyToDenseInteger = identity_functort>
typedef std::vector<std::pair<K, V> > dense_integer_mapt< K, V, KeyToDenseInteger >::backing_storet
private

Definition at line 65 of file dense_integer_map.h.

◆ const_iterator

template<class K , class V , class KeyToDenseInteger = identity_functort>
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.

◆ iterator

template<class K , class V , class KeyToDenseInteger = identity_functort>
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.

◆ possible_keyst

template<class K , class V , class KeyToDenseInteger = identity_functort>
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.

Constructor & Destructor Documentation

◆ dense_integer_mapt()

template<class K , class V , class KeyToDenseInteger = identity_functort>
dense_integer_mapt< K, V, KeyToDenseInteger >::dense_integer_mapt ( )
inline

Definition at line 220 of file dense_integer_map.h.

Member Function Documentation

◆ at() [1/2]

template<class K , class V , class KeyToDenseInteger = identity_functort>
V& dense_integer_mapt< K, V, KeyToDenseInteger >::at ( const K &  key)
inline

Definition at line 280 of file dense_integer_map.h.

◆ at() [2/2]

template<class K , class V , class KeyToDenseInteger = identity_functort>
const V& dense_integer_mapt< K, V, KeyToDenseInteger >::at ( const K &  key) const
inline

Definition at line 274 of file dense_integer_map.h.

◆ begin() [1/2]

template<class K , class V , class KeyToDenseInteger = identity_functort>
iterator dense_integer_mapt< K, V, KeyToDenseInteger >::begin ( )
inline

Definition at line 326 of file dense_integer_map.h.

◆ begin() [2/2]

template<class K , class V , class KeyToDenseInteger = identity_functort>
const_iterator dense_integer_mapt< K, V, KeyToDenseInteger >::begin ( ) const
inline

Definition at line 336 of file dense_integer_map.h.

◆ cbegin()

template<class K , class V , class KeyToDenseInteger = identity_functort>
const_iterator dense_integer_mapt< K, V, KeyToDenseInteger >::cbegin ( ) const
inline

Definition at line 346 of file dense_integer_map.h.

◆ cend()

template<class K , class V , class KeyToDenseInteger = identity_functort>
const_iterator dense_integer_mapt< K, V, KeyToDenseInteger >::cend ( ) const
inline

Definition at line 351 of file dense_integer_map.h.

◆ count()

template<class K , class V , class KeyToDenseInteger = identity_functort>
std::size_t dense_integer_mapt< K, V, KeyToDenseInteger >::count ( const K &  key) const
inline

Definition at line 311 of file dense_integer_map.h.

◆ end() [1/2]

template<class K , class V , class KeyToDenseInteger = identity_functort>
iterator dense_integer_mapt< K, V, KeyToDenseInteger >::end ( )
inline

Definition at line 331 of file dense_integer_map.h.

◆ end() [2/2]

template<class K , class V , class KeyToDenseInteger = identity_functort>
const_iterator dense_integer_mapt< K, V, KeyToDenseInteger >::end ( ) const
inline

Definition at line 341 of file dense_integer_map.h.

◆ index_is_set()

template<class K , class V , class KeyToDenseInteger = identity_functort>
bool dense_integer_mapt< K, V, KeyToDenseInteger >::index_is_set ( std::size_t  index) const
inlineprivate

Definition at line 110 of file dense_integer_map.h.

◆ insert()

template<class K , class V , class KeyToDenseInteger = identity_functort>
std::pair<iterator, bool> dense_integer_mapt< K, V, KeyToDenseInteger >::insert ( const std::pair< const K, V > &  pair)
inline

Definition at line 294 of file dense_integer_map.h.

◆ key_to_index()

template<class K , class V , class KeyToDenseInteger = identity_functort>
std::size_t dense_integer_mapt< K, V, KeyToDenseInteger >::key_to_index ( const K &  key) const
inlineprivate

Definition at line 90 of file dense_integer_map.h.

◆ mark_index_set()

template<class K , class V , class KeyToDenseInteger = identity_functort>
void dense_integer_mapt< K, V, KeyToDenseInteger >::mark_index_set ( std::size_t  index)
inlineprivate

Definition at line 100 of file dense_integer_map.h.

◆ operator[]()

template<class K , class V , class KeyToDenseInteger = identity_functort>
V& dense_integer_mapt< K, V, KeyToDenseInteger >::operator[] ( const K &  key)
inline

Definition at line 287 of file dense_integer_map.h.

◆ possible_keys()

template<class K , class V , class KeyToDenseInteger = identity_functort>
const possible_keyst& dense_integer_mapt< K, V, KeyToDenseInteger >::possible_keys ( ) const
inline

Definition at line 321 of file dense_integer_map.h.

◆ setup_for_keys()

template<class K , class V , class KeyToDenseInteger = identity_functort>
template<typename Iter >
void dense_integer_mapt< K, V, KeyToDenseInteger >::setup_for_keys ( Iter  first,
Iter  last 
)
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.

◆ size()

template<class K , class V , class KeyToDenseInteger = identity_functort>
std::size_t dense_integer_mapt< K, V, KeyToDenseInteger >::size ( ) const
inline

Definition at line 316 of file dense_integer_map.h.

Member Data Documentation

◆ map

template<class K , class V , class KeyToDenseInteger = identity_functort>
backing_storet dense_integer_mapt< K, V, KeyToDenseInteger >::map
private

Definition at line 71 of file dense_integer_map.h.

◆ n_values_set

template<class K , class V , class KeyToDenseInteger = identity_functort>
std::size_t dense_integer_mapt< K, V, KeyToDenseInteger >::n_values_set
private

Definition at line 82 of file dense_integer_map.h.

◆ offset

template<class K , class V , class KeyToDenseInteger = identity_functort>
int64_t dense_integer_mapt< K, V, KeyToDenseInteger >::offset
private

Definition at line 63 of file dense_integer_map.h.

◆ possible_keys_vector

template<class K , class V , class KeyToDenseInteger = identity_functort>
possible_keyst dense_integer_mapt< K, V, KeyToDenseInteger >::possible_keys_vector
private

Definition at line 87 of file dense_integer_map.h.

◆ value_set

template<class K , class V , class KeyToDenseInteger = identity_functort>
std::vector<bool> dense_integer_mapt< K, V, KeyToDenseInteger >::value_set
private

Definition at line 78 of file dense_integer_map.h.


The documentation for this class was generated from the following file: