cprover
value_sett::object_map_dt Class Reference

Represents a set of expressions (exprt instances) with corresponding offsets (offsett instances). More...

#include <value_set.h>

+ Collaboration diagram for value_sett::object_map_dt:

Public Types

typedef data_typet::iterator iterator
 
typedef data_typet::const_iterator const_iterator
 
typedef data_typet::value_type value_type
 
typedef data_typet::key_type key_type
 

Public Member Functions

iterator begin ()
 
const_iterator begin () const
 
const_iterator cbegin () const
 
iterator end ()
 
const_iterator end () const
 
const_iterator cend () const
 
size_t size () const
 
bool empty () const
 
void erase (key_type i)
 
void erase (const_iterator it)
 
offsettoperator[] (key_type i)
 
offsettat (key_type i)
 
const offsettat (key_type i) const
 
template<typename It >
void insert (It b, It e)
 
template<typename T >
const_iterator find (T &&t) const
 
 object_map_dt ()=default
 
bool operator== (const object_map_dt &other) const
 
bool operator!= (const object_map_dt &other) const
 

Static Public Attributes

static const object_map_dt blank {}
 

Protected Member Functions

 ~object_map_dt ()=default
 

Private Types

typedef std::map< object_numberingt::number_type, offsettdata_typet
 

Private Attributes

data_typet data
 

Detailed Description

Represents a set of expressions (exprt instances) with corresponding offsets (offsett instances).

This is the RHS set of a single row of the enclosing value_sett, such as { null, dynamic_object1 }. The set is represented as a map from numbered exprts to offsett instead of a set of pairs to make lookup by exprt easier. All methods matching the interface of std::map forward those methods to the internal map.

Definition at line 80 of file value_set.h.

Member Typedef Documentation

◆ const_iterator

typedef data_typet::const_iterator value_sett::object_map_dt::const_iterator

Definition at line 89 of file value_set.h.

◆ data_typet

Definition at line 82 of file value_set.h.

◆ iterator

typedef data_typet::iterator value_sett::object_map_dt::iterator

Definition at line 87 of file value_set.h.

◆ key_type

typedef data_typet::key_type value_sett::object_map_dt::key_type

Definition at line 93 of file value_set.h.

◆ value_type

typedef data_typet::value_type value_sett::object_map_dt::value_type

Definition at line 91 of file value_set.h.

Constructor & Destructor Documentation

◆ object_map_dt()

value_sett::object_map_dt::object_map_dt ( )
default

◆ ~object_map_dt()

value_sett::object_map_dt::~object_map_dt ( )
protecteddefault

Member Function Documentation

◆ at() [1/2]

offsett& value_sett::object_map_dt::at ( key_type  i)
inline

Definition at line 113 of file value_set.h.

◆ at() [2/2]

const offsett& value_sett::object_map_dt::at ( key_type  i) const
inline

Definition at line 117 of file value_set.h.

◆ begin() [1/2]

iterator value_sett::object_map_dt::begin ( )
inline

Definition at line 95 of file value_set.h.

◆ begin() [2/2]

const_iterator value_sett::object_map_dt::begin ( ) const
inline

Definition at line 96 of file value_set.h.

◆ cbegin()

const_iterator value_sett::object_map_dt::cbegin ( ) const
inline

Definition at line 97 of file value_set.h.

◆ cend()

const_iterator value_sett::object_map_dt::cend ( ) const
inline

Definition at line 101 of file value_set.h.

◆ empty()

bool value_sett::object_map_dt::empty ( ) const
inline

Definition at line 104 of file value_set.h.

◆ end() [1/2]

iterator value_sett::object_map_dt::end ( )
inline

Definition at line 99 of file value_set.h.

◆ end() [2/2]

const_iterator value_sett::object_map_dt::end ( ) const
inline

Definition at line 100 of file value_set.h.

◆ erase() [1/2]

void value_sett::object_map_dt::erase ( const_iterator  it)
inline

Definition at line 107 of file value_set.h.

◆ erase() [2/2]

void value_sett::object_map_dt::erase ( key_type  i)
inline

Definition at line 106 of file value_set.h.

◆ find()

template<typename T >
const_iterator value_sett::object_map_dt::find ( T &&  t) const
inline

Definition at line 126 of file value_set.h.

◆ insert()

template<typename It >
void value_sett::object_map_dt::insert ( It  b,
It  e 
)
inline

Definition at line 123 of file value_set.h.

◆ operator!=()

bool value_sett::object_map_dt::operator!= ( const object_map_dt other) const
inline

Definition at line 136 of file value_set.h.

◆ operator==()

bool value_sett::object_map_dt::operator== ( const object_map_dt other) const
inline

Definition at line 132 of file value_set.h.

◆ operator[]()

offsett& value_sett::object_map_dt::operator[] ( key_type  i)
inline

Definition at line 109 of file value_set.h.

◆ size()

size_t value_sett::object_map_dt::size ( ) const
inline

Definition at line 103 of file value_set.h.

Member Data Documentation

◆ blank

const value_sett::object_map_dt value_sett::object_map_dt::blank {}
static

Definition at line 128 of file value_set.h.

◆ data

data_typet value_sett::object_map_dt::data
private

Definition at line 83 of file value_set.h.


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