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, 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 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 217 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 210 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 219 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 279 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 273 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 325 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 335 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 345 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 350 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 310 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 330 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 340 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 293 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 286 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 320 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 231 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 315 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/cbmc/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 >