cprover
|
#include <numbering.h>
Public Types | |
using | number_type = typename Map::mapped_type |
using | key_type = typename Map::key_type |
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) |
optionalt< 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_ |
Map | numbers_ |
Map | a map from a key type to some numeric type |
Definition at line 21 of file numbering.h.
using template_numberingt< Map >::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 template_numberingt< Map >::iterator = typename data_typet::iterator |
Definition at line 34 of file numbering.h.
using template_numberingt< Map >::key_type = typename Map::key_type |
Definition at line 25 of file numbering.h.
using template_numberingt< Map >::number_type = typename Map::mapped_type |
Definition at line 24 of file numbering.h.
using template_numberingt< Map >::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.
Referenced by union_find< exprt >::begin(), bv_pointerst::do_postponed(), union_find< exprt >::find(), union_find< exprt >::find_number(), pointer_logict::get_dynamic_objects(), union_find< exprt >::is_root(), union_find< exprt >::isolate(), union_find< exprt >::make_union(), and union_find< exprt >::same_set().
|
inline |
Definition at line 89 of file numbering.h.
|
inline |
Definition at line 93 of file numbering.h.
Referenced by union_find< exprt >::cbegin().
|
inline |
Definition at line 106 of file numbering.h.
Referenced by union_find< exprt >::cend().
|
inline |
Definition at line 60 of file numbering.h.
Referenced by irep_hash_container_baset::clear(), and union_find< exprt >::clear().
|
inline |
Definition at line 98 of file numbering.h.
Referenced by bv_pointerst::do_postponed(), union_find< exprt >::end(), and pointer_logict::get_dynamic_objects().
|
inline |
Definition at line 102 of file numbering.h.
|
inline |
Definition at line 50 of file numbering.h.
Referenced by inv_object_storet::get(), union_find< exprt >::get_number(), union_find< exprt >::is_root(), and union_find< exprt >::same_set().
|
inline |
Definition at line 37 of file numbering.h.
Referenced by inv_object_storet::add(), pointer_logict::add_object(), inv_object_storet::get(), custom_bitvector_analysist::get_bit_nr(), value_set_fit::insert(), value_sett::insert(), value_set_fivrt::insert_from(), value_set_fivrnst::insert_from(), value_set_fivrnst::insert_to(), value_set_fivrt::insert_to(), irep_hash_container_baset::number(), union_find< exprt >::number(), output_vcd(), and pointer_logict::pointer_logict().
|
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.
Referenced by partial_order_concurrencyt::build_clock_type(), union_find< exprt >::number(), custom_bitvector_domaint::output(), pointer_logict::pointer_expr(), and union_find< exprt >::size().
|
private |
Definition at line 29 of file numbering.h.
Referenced by template_numberingt< exprt >::at(), template_numberingt< exprt >::begin(), template_numberingt< exprt >::cbegin(), template_numberingt< exprt >::cend(), template_numberingt< exprt >::clear(), template_numberingt< exprt >::end(), template_numberingt< exprt >::number(), template_numberingt< exprt >::operator[](), and template_numberingt< exprt >::size().
|
private |
Definition at line 30 of file numbering.h.
Referenced by template_numberingt< exprt >::clear(), template_numberingt< exprt >::get_number(), and template_numberingt< exprt >::number().