CBMC
|
#include <numbering.h>
Public Types | |
using | number_type = std::size_t |
using | key_type = keyt |
using | size_type = typename data_typet::size_type |
using | iterator = typename data_typet::iterator |
using | const_iterator = typename data_typet::const_iterator |
Public Member Functions | |
number_type | number (const key_type &a) |
std::optional< number_type > | get_number (const key_type &a) const |
void | clear () |
size_type | size () const |
const key_type & | at (size_type t) const |
key_type & | operator[] (size_type t) |
const key_type & | operator[] (size_type t) const |
iterator | begin () |
const_iterator | begin () const |
const_iterator | cbegin () const |
iterator | end () |
const_iterator | end () const |
const_iterator | cend () const |
Private Types | |
using | data_typet = std::vector< key_type > |
Private Attributes | |
data_typet | data_ |
std::unordered_map< keyt, number_type, hasht > | numbers_ |
keyt | The type of keys which will be numbered. |
hasht | The type of hashing functor used to hash keys. |
Definition at line 21 of file numbering.h.
using numberingt< keyt, hasht >::const_iterator = typename data_typet::const_iterator |
Definition at line 35 of file numbering.h.
|
private |
Definition at line 28 of file numbering.h.
using numberingt< keyt, hasht >::iterator = typename data_typet::iterator |
Definition at line 34 of file numbering.h.
using numberingt< keyt, hasht >::key_type = keyt |
Definition at line 25 of file numbering.h.
using numberingt< keyt, hasht >::number_type = std::size_t |
Definition at line 24 of file numbering.h.
using numberingt< keyt, hasht >::size_type = typename data_typet::size_type |
Definition at line 33 of file numbering.h.
|
inline |
Definition at line 71 of file numbering.h.
|
inline |
Definition at line 85 of file numbering.h.
|
inline |
Definition at line 89 of file numbering.h.
|
inline |
Definition at line 93 of file numbering.h.
|
inline |
Definition at line 106 of file numbering.h.
|
inline |
Definition at line 60 of file numbering.h.
|
inline |
Definition at line 98 of file numbering.h.
|
inline |
Definition at line 102 of file numbering.h.
|
inline |
Definition at line 50 of file numbering.h.
|
inline |
Definition at line 37 of file numbering.h.
|
inline |
Definition at line 76 of file numbering.h.
|
inline |
Definition at line 80 of file numbering.h.
|
inline |
Definition at line 66 of file numbering.h.
|
private |
Definition at line 29 of file numbering.h.
|
private |
Definition at line 30 of file numbering.h.