cprover
|
A map implemented as a tree where subtrees can be shared between different maps. More...
#include <sharing_map.h>
Classes | |
class | delta_view_itemt |
struct | sharing_map_statst |
Stats about sharing between several sharing map instances. More... | |
Public Types | |
typedef keyT | key_type |
typedef valueT | mapped_type |
typedef std::pair< const key_type, mapped_type > | value_type |
typedef hashT | hash |
typedef equalT | key_equal |
typedef std::size_t | size_type |
typedef std::vector< key_type > | keyst |
typedef std::pair< const key_type &, const mapped_type & > | view_itemt |
typedef std::vector< view_itemt > | viewt |
View of the key-value pairs in the map. More... | |
typedef std::vector< delta_view_itemt > | delta_viewt |
Delta view of the key-value pairs in two maps. More... | |
Public Member Functions | |
~sharing_mapt () | |
size_type | erase (const key_type &k, const tvt &key_exists=tvt::unknown()) |
Erase element. More... | |
size_type | erase_all (const keyst &ks, const tvt &key_exists=tvt::unknown()) |
Erase all elements. More... | |
const_find_type | insert (const key_type &k, const mapped_type &v, const tvt &key_exists=tvt::unknown()) |
Insert element, return const reference. More... | |
const_find_type | insert (const value_type &p, const tvt &key_exists=tvt::unknown()) |
find_type | place (const key_type &k, const mapped_type &v) |
Insert element, return non-const reference. More... | |
find_type | place (const value_type &p) |
Insert element, return non-const reference. More... | |
find_type | find (const key_type &k, const tvt &key_exists=tvt::unknown()) |
Find element. More... | |
const_find_type | find (const key_type &k) const |
Find element. More... | |
mapped_type & | at (const key_type &k, const tvt &key_exists=tvt::unknown()) |
Get element at key. More... | |
const mapped_type & | at (const key_type &k) const |
Get element at key. More... | |
mapped_type & | operator[] (const key_type &k) |
Get element at key, insert new if non-existent. More... | |
void | swap (sharing_mapt &other) |
Swap with other map. More... | |
size_type | size () const |
Get number of elements in map. More... | |
bool | empty () const |
Check if map is empty. More... | |
void | clear () |
Clear map. More... | |
bool | has_key (const key_type &k) const |
Check if key is in map. More... | |
void | get_view (viewt &view) const |
Get a view of the elements in the map A view is a list of pairs with the components being const references to the keys and values in the map. More... | |
void | get_delta_view (const sharing_mapt &other, delta_viewt &delta_view, const bool only_common=true) const |
Get a delta view of the elements in the map. More... | |
Static Public Member Functions | |
template<class Iterator > | |
static sharing_map_statst | get_sharing_stats (Iterator begin, Iterator end, std::function< sharing_mapt &(const Iterator)> f=[](const Iterator it) -> sharing_mapt &{ return *it;}) |
Get sharing stats. More... | |
template<class Iterator > | |
static sharing_map_statst | get_sharing_stats_map (Iterator begin, Iterator end) |
Get sharing stats. More... | |
Public Attributes | |
const typedef std::pair< const mapped_type &, const bool > | const_find_type |
Return type of methods that retrieve a const reference to a value. More... | |
const typedef std::pair< mapped_type &, const bool > | find_type |
Return type of methods that retrieve a reference to a value. More... | |
Protected Types | |
typedef sharing_node_innert< key_type, mapped_type > | innert |
typedef sharing_node_leaft< key_type, mapped_type > | leaft |
typedef sharing_node_baset | baset |
typedef innert::to_mapt | to_mapt |
typedef innert::leaf_listt | leaf_listt |
Protected Member Functions | |
innert * | get_container_node (const key_type &k) |
const innert * | get_container_node (const key_type &k) const |
const leaft * | get_leaf_node (const key_type &k) const |
void | iterate (const baset &n, const unsigned start_depth, std::function< void(const key_type &k, const mapped_type &m)> f) const |
void | gather_all (const baset &n, const unsigned depth, delta_viewt &delta_view) const |
std::size_t | count_unmarked_nodes (bool leafs_only, std::set< void * > &marked, bool mark=true) const |
Protected Attributes | |
innert | map |
size_type | num = 0 |
Static Protected Attributes | |
static mapped_type | dummy |
static const std::string | not_found_msg ="key not found" |
static const std::size_t | bits = 18 |
static const std::size_t | chunk = 3 |
static const std::size_t | mask = 0xffff >> (16 - chunk) |
static const std::size_t | steps = bits / chunk |
A map implemented as a tree where subtrees can be shared between different maps.
The map is implemented as a fixed-height n-ary trie. The height H and the maximum number of children per inner node S are determined by the two configuration parameters bits
and chunks
in sharing_map.h. It holds that H = bits
/ chunks
and S = 2 ^ chunks
.
When inserting a key-value pair into the map, first the hash of its key is computed. The bits
number of lower order bits of the hash are deemed significant, and are grouped into bits
/ chunk
chunks. The hash is then treated as a string (with each chunk representing a character) for the purposes of determining the position of the key-value pair in the trie. The actual key-value pairs are stored in the leaf nodes. Collisions (i.e., two different keys yield the same "string"), are handled by chaining the corresponding key-value pairs in a std::list
.
The use of a trie in combination with hashing has the advantage that the tree is unlikely to degenerate (if the number of hash collisions is low). This makes re-balancing operations unnecessary which do not interact well with sharing. A disadvantage is that the height of the tree is likely greater than if the elements had been stored in a balanced tree (with greater differences for sparser maps).
The nodes in the sharing map are objects of type sharing_nodet. Each sharing node has a shared_ptr
to an object of type dt
which can be shared between nodes.
Sharing is initially generated when a map is assigned to another map or copied via the copy constructor. Then both maps contain a pointer to the root node of the tree that represents the maps. On subsequent modifications to one of the maps, nodes are copied and sharing is lessened as described in the following.
Retrieval, insertion, and removal operations interact with sharing as follows:
Several methods take a hint indicating whether the element is known not to be in the map (false
), known to be in the map (true
), or it is unknown whether the element is in the map (unknown
). The value unknown
is always valid. When true
or false
are given they need to be accurate, otherwise the behavior is undefined. A correct hint can prevent the need to follow a path from the root to a key-value pair twice (e.g., once for checking that it exists, and second for copying nodes).
In the descriptions of the methods of the sharing map we also give the complexity of the operations. We use the following symbols:
The first two symbols denote dynamic properties of a given map, whereas the last two symbols are static configuration parameters of the map class.
Definition at line 130 of file sharing_map.h.
|
protected |
Definition at line 164 of file sharing_map.h.
typedef std::vector<delta_view_itemt> sharing_mapt< keyT, valueT, hashT, equalT >::delta_viewt |
Delta view of the key-value pairs in two maps.
A delta view of two maps is a view of the key-value pairs in the maps that are contained in subtrees that are not shared between them (also see get_delta_view()).
Definition at line 286 of file sharing_map.h.
typedef hashT sharing_mapt< keyT, valueT, hashT, equalT >::hash |
Definition at line 141 of file sharing_map.h.
|
protected |
Definition at line 161 of file sharing_map.h.
typedef equalT sharing_mapt< keyT, valueT, hashT, equalT >::key_equal |
Definition at line 142 of file sharing_map.h.
typedef keyT sharing_mapt< keyT, valueT, hashT, equalT >::key_type |
Definition at line 137 of file sharing_map.h.
typedef std::vector<key_type> sharing_mapt< keyT, valueT, hashT, equalT >::keyst |
Definition at line 158 of file sharing_map.h.
|
protected |
Definition at line 167 of file sharing_map.h.
|
protected |
Definition at line 162 of file sharing_map.h.
typedef valueT sharing_mapt< keyT, valueT, hashT, equalT >::mapped_type |
Definition at line 138 of file sharing_map.h.
typedef std::size_t sharing_mapt< keyT, valueT, hashT, equalT >::size_type |
Definition at line 144 of file sharing_map.h.
|
protected |
Definition at line 166 of file sharing_map.h.
typedef std::pair<const key_type, mapped_type> sharing_mapt< keyT, valueT, hashT, equalT >::value_type |
Definition at line 139 of file sharing_map.h.
typedef std::pair<const key_type &, const mapped_type &> sharing_mapt< keyT, valueT, hashT, equalT >::view_itemt |
Definition at line 254 of file sharing_map.h.
typedef std::vector<view_itemt> sharing_mapt< keyT, valueT, hashT, equalT >::viewt |
View of the key-value pairs in the map.
A view is a list of pairs with the components being const references to the keys and values in the map.
Definition at line 258 of file sharing_map.h.
|
inline |
Definition at line 133 of file sharing_map.h.
const sharing_mapt< keyT, valueT, hashT, equalT >::mapped_type & sharing_mapt< keyT, valueT, hashT, equalT >::at | ( | const key_type & | k | ) | const |
Get element at key.
Complexity:
k | The key of the element |
std::out_of_range | if key not found |
Definition at line 1037 of file sharing_map.h.
sharing_mapt< keyT, valueT, hashT, equalT >::mapped_type & sharing_mapt< keyT, valueT, hashT, equalT >::at | ( | const key_type & | k, |
const tvt & | key_exists = tvt::unknown() |
||
) |
Get element at key.
Complexity:
k | The key of the element |
key_exists | Hint to indicate whether the element is known to exist (possible values unknown or true ) |
<tt>std::out_of_range</tt> | if key not found |
Definition at line 1016 of file sharing_map.h.
|
inline |
Clear map.
Definition at line 236 of file sharing_map.h.
|
protected |
Definition at line 425 of file sharing_map.h.
|
inline |
Check if map is empty.
Definition at line 230 of file sharing_map.h.
sharing_mapt< keyT, valueT, hashT, equalT >::size_type sharing_mapt< keyT, valueT, hashT, equalT >::erase | ( | const key_type & | k, |
const tvt & | key_exists = tvt::unknown() |
||
) |
Erase element.
Complexity:
k | The key of the element to erase |
key_exists | Hint to indicate whether the element is known to exist (possible values unknown ortrue ) |
Definition at line 800 of file sharing_map.h.
sharing_mapt< keyT, valueT, hashT, equalT >::size_type sharing_mapt< keyT, valueT, hashT, equalT >::erase_all | ( | const keyst & | ks, |
const tvt & | key_exists = tvt::unknown() |
||
) |
Erase all elements.
Complexity:
ks | The keys of the element to erase |
key_exists | Hint to indicate whether the elements are known to exist (possible values unknown or true ). Applies to all elements (i.e., have to use unknown if for at least one element it is not known whether it exists) |
Definition at line 873 of file sharing_map.h.
const sharing_mapt< keyT, valueT, hashT, equalT >::const_find_type sharing_mapt< keyT, valueT, hashT, equalT >::find | ( | const key_type & | k | ) | const |
Find element.
Complexity:
k | The key of the element to search |
Definition at line 995 of file sharing_map.h.
const sharing_mapt< keyT, valueT, hashT, equalT >::find_type sharing_mapt< keyT, valueT, hashT, equalT >::find | ( | const key_type & | k, |
const tvt & | key_exists = tvt::unknown() |
||
) |
Find element.
Complexity:
k | The key of the element to search for |
key_exists | Hint to indicate whether the element is known to exist (possible values unknown or true ) |
Definition at line 969 of file sharing_map.h.
|
protected |
Definition at line 609 of file sharing_map.h.
|
protected |
Definition at line 752 of file sharing_map.h.
|
protected |
Definition at line 769 of file sharing_map.h.
void sharing_mapt< keyT, valueT, hashT, equalT >::get_delta_view | ( | const sharing_mapt< keyT, valueT, hashT, equalT > & | other, |
delta_viewt & | delta_view, | ||
const bool | only_common = true |
||
) | const |
Get a delta view of the elements in the map.
Informally, a delta view of two maps is a view of the key-value pairs in the maps that are contained in subtrees that are not shared between them.
A delta view is represented as a list of structs, with each struct having four members (in_both
, key
, value1
, value2
). The elements key
, value1
, and value2
are const references to the corresponding elements in the map. The first element indicates whether the key exists in both maps, the second element is the key, the third element is the mapped value of the first map, and the fourth element is the mapped value of the second map, or a dummy element if the key exists only in the first map (in which case in_both
is false).
Calling A.delta_view(B, ...)
yields a view such that for each element in the view one of two things holds:
When only_common=true
, the first case above holds for every element in the view.
Complexity:
The symbols N1, M1 refer to map A, and symbols N2, M2 refer to map B.
other | other map | |
[out] | delta_view | Empty delta view |
only_common | Indicates if the returned delta view should only contain key-value pairs for keys that exist in both maps |
Definition at line 652 of file sharing_map.h.
|
inlineprotected |
Definition at line 330 of file sharing_map.h.
|
static |
Get sharing stats.
Complexity:
begin | begin iterator |
end | end iterator |
f | function applied to the iterator to get a sharing map |
Definition at line 525 of file sharing_map.h.
|
static |
Get sharing stats.
Complexity:
begin | begin iterator of a map |
end | end iterator of a map |
Definition at line 579 of file sharing_map.h.
void sharing_mapt< keyT, valueT, hashT, equalT >::get_view | ( | viewt & | view | ) | const |
Get a view of the elements in the map A view is a list of pairs with the components being const references to the keys and values in the map.
Complexity:
[out] | view | Empty view |
Definition at line 594 of file sharing_map.h.
|
inline |
Check if key is in map.
Complexity:
Definition at line 247 of file sharing_map.h.
const sharing_mapt< keyT, valueT, hashT, equalT >::const_find_type sharing_mapt< keyT, valueT, hashT, equalT >::insert | ( | const key_type & | k, |
const mapped_type & | m, | ||
const tvt & | key_exists = tvt::unknown() |
||
) |
Insert element, return const reference.
Complexity:
k | The key of the element to insert |
m | The mapped value to insert |
key_exists | Hint to indicate whether the element is known to exist (possible values false or unknown ) |
Definition at line 898 of file sharing_map.h.
const sharing_mapt< keyT, valueT, hashT, equalT >::const_find_type sharing_mapt< keyT, valueT, hashT, equalT >::insert | ( | const value_type & | p, |
const tvt & | key_exists = tvt::unknown() |
||
) |
Definition at line 921 of file sharing_map.h.
|
protected |
Definition at line 376 of file sharing_map.h.
sharing_mapt< keyT, valueT, hashT, equalT >::mapped_type & sharing_mapt< keyT, valueT, hashT, equalT >::operator[] | ( | const key_type & | k | ) |
Get element at key, insert new if non-existent.
Complexity:
k | The key of the element |
Definition at line 1054 of file sharing_map.h.
const sharing_mapt< keyT, valueT, hashT, equalT >::find_type sharing_mapt< keyT, valueT, hashT, equalT >::place | ( | const key_type & | k, |
const mapped_type & | m | ||
) |
Insert element, return non-const reference.
Complexity:
k | The key of the element to insert |
m | The mapped value to insert |
Definition at line 936 of file sharing_map.h.
const sharing_mapt< keyT, valueT, hashT, equalT >::find_type sharing_mapt< keyT, valueT, hashT, equalT >::place | ( | const value_type & | p | ) |
Insert element, return non-const reference.
Definition at line 953 of file sharing_map.h.
|
inline |
|
inline |
|
staticprotected |
Definition at line 361 of file sharing_map.h.
|
staticprotected |
Definition at line 362 of file sharing_map.h.
const typedef std::pair<const mapped_type &, const bool> sharing_mapt< keyT, valueT, hashT, equalT >::const_find_type |
Return type of methods that retrieve a const reference to a value.
First component is a reference to the value (or a dummy value if the given key does not exist), and the second component indicates if the value with the given key was found.
Definition at line 150 of file sharing_map.h.
|
staticprotected |
Definition at line 356 of file sharing_map.h.
const typedef std::pair<mapped_type &, const bool> sharing_mapt< keyT, valueT, hashT, equalT >::find_type |
Return type of methods that retrieve a reference to a value.
First component is a reference to the value (or a dummy value if the given key does not exist), and the second component indicates if the value with the given key was found.
Definition at line 156 of file sharing_map.h.
|
protected |
Definition at line 369 of file sharing_map.h.
|
staticprotected |
Definition at line 365 of file sharing_map.h.
|
staticprotected |
Definition at line 358 of file sharing_map.h.
|
protected |
Definition at line 372 of file sharing_map.h.
|
staticprotected |
Definition at line 366 of file sharing_map.h.