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:
[legend]

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 78 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 87 of file value_set.h.

◆ data_typet

Definition at line 80 of file value_set.h.

◆ iterator

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

Definition at line 85 of file value_set.h.

◆ key_type

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

Definition at line 91 of file value_set.h.

◆ value_type

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

Definition at line 89 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 111 of file value_set.h.

◆ at() [2/2]

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

Definition at line 115 of file value_set.h.

◆ begin() [1/2]

◆ begin() [2/2]

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

Definition at line 94 of file value_set.h.

◆ cbegin()

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

Definition at line 95 of file value_set.h.

◆ cend()

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

Definition at line 99 of file value_set.h.

◆ empty()

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

Definition at line 102 of file value_set.h.

Referenced by value_sett::get_value_set_rec().

◆ end() [1/2]

◆ end() [2/2]

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

Definition at line 98 of file value_set.h.

◆ erase() [1/2]

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

Definition at line 104 of file value_set.h.

◆ erase() [2/2]

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

Definition at line 105 of file value_set.h.

◆ find()

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

Definition at line 124 of file value_set.h.

Referenced by value_sett::insert().

◆ insert()

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

Definition at line 121 of file value_set.h.

Referenced by value_sett::get_value_set_rec().

◆ operator!=()

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

Definition at line 134 of file value_set.h.

◆ operator==()

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

Definition at line 130 of file value_set.h.

References data.

◆ operator[]()

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

Definition at line 107 of file value_set.h.

◆ size()

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

Definition at line 101 of file value_set.h.

References data::size.

Referenced by value_sett::assign_rec(), and value_sett::get_value_set_rec().

Member Data Documentation

◆ blank

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

Definition at line 126 of file value_set.h.

◆ data

data_typet value_sett::object_map_dt::data
private

Definition at line 81 of file value_set.h.

Referenced by operator==().


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