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

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, optionalt<value>>, where the value optional will always be defined. This is because the backing store uses optionalt 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 53 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 64 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 213 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 206 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 57 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 215 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 275 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 269 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 321 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 331 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 341 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 346 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 306 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 326 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 336 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 109 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 289 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 89 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 99 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 282 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 316 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 227 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 311 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 70 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 81 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 62 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 86 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 77 of file dense_integer_map.h.

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

/home/runner/work/cbmc-documentation/cbmc-documentation/src/util/dense_integer_map.h

Classes

Public Types

Public Member Functions

Private Types

Private Member Functions

Private Attributes

Detailed Description

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

Member Typedef Documentation

◆ backing_storet

◆ const_iterator

◆ iterator

◆ possible_keyst

Constructor & Destructor Documentation

◆ dense_integer_mapt()

Member Function Documentation

◆ at() [1/2]

◆ at() [2/2]

◆ begin() [1/2]

◆ begin() [2/2]

◆ cbegin()

◆ cend()

◆ count()

◆ end() [1/2]

◆ end() [2/2]

◆ index_is_set()

◆ insert()

◆ key_to_index()

◆ mark_index_set()

◆ operator[]()

◆ possible_keys()

◆ setup_for_keys()

◆ size()

Member Data Documentation

◆ map

◆ n_values_set

◆ offset

◆ possible_keys_vector

◆ value_set

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