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 |
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 const std::pair< const mapped_type &, const bool > | const_find_type |
Return type of methods that retrieve a const reference to a value. More... | |
typedef const std::pair< mapped_type &, const bool > | find_type |
Return type of methods that retrieve a reference to a value. More... | |
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... | |
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 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 |
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 |
Friends | |
void | sharing_map_interface_test () |
void | sharing_map_copy_test () |
void | sharing_map_collision_test () |
void | sharing_map_view_test () |
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 124 of file sharing_map.h.
|
protected |
Definition at line 163 of file sharing_map.h.
typedef const 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 149 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 285 of file sharing_map.h.
typedef const 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 155 of file sharing_map.h.
typedef hashT sharing_mapt< keyT, valueT, hashT, equalT >::hash |
Definition at line 140 of file sharing_map.h.
|
protected |
Definition at line 160 of file sharing_map.h.
typedef equalT sharing_mapt< keyT, valueT, hashT, equalT >::key_equal |
Definition at line 141 of file sharing_map.h.
typedef keyT sharing_mapt< keyT, valueT, hashT, equalT >::key_type |
Definition at line 136 of file sharing_map.h.
typedef std::vector<key_type> sharing_mapt< keyT, valueT, hashT, equalT >::keyst |
Definition at line 157 of file sharing_map.h.
|
protected |
Definition at line 166 of file sharing_map.h.
|
protected |
Definition at line 161 of file sharing_map.h.
typedef valueT sharing_mapt< keyT, valueT, hashT, equalT >::mapped_type |
Definition at line 137 of file sharing_map.h.
typedef std::size_t sharing_mapt< keyT, valueT, hashT, equalT >::size_type |
Definition at line 143 of file sharing_map.h.
|
protected |
Definition at line 165 of file sharing_map.h.
typedef std::pair<const key_type, mapped_type> sharing_mapt< keyT, valueT, hashT, equalT >::value_type |
Definition at line 138 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 253 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 257 of file sharing_map.h.
|
inline |
Definition at line 132 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 820 of file sharing_map.h.
References r.
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 841 of file sharing_map.h.
References r.
|
inline |
Clear map.
Definition at line 235 of file sharing_map.h.
References sharing_node_innert< keyT, valueT, equalT >::clear(), sharing_mapt< keyT, valueT, hashT, equalT >::map, and sharing_mapt< keyT, valueT, hashT, equalT >::num.
|
inline |
Check if map is empty.
Definition at line 229 of file sharing_map.h.
References sharing_mapt< keyT, valueT, hashT, equalT >::num.
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 604 of file sharing_map.h.
References sharing_node_innert< keyT, valueT, equalT >::add_child(), as_const(), sharing_node_innert< keyT, valueT, equalT >::remove_child(), sharing_node_innert< keyT, valueT, equalT >::remove_leaf(), small_mapt< T, Ind, Num >::size(), and SM_ASSERT.
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 677 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 773 of file sharing_map.h.
References sharing_node_innert< keyT, valueT, equalT >::find_leaf(), sharing_node_leaft< keyT, valueT, equalT >::get_value(), and SM_ASSERT.
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 799 of file sharing_map.h.
References sharing_node_leaft< keyT, valueT, equalT >::get_value().
|
protected |
Definition at line 413 of file sharing_map.h.
|
protected |
Definition at line 556 of file sharing_map.h.
References sharing_node_innert< keyT, valueT, equalT >::add_child().
Referenced by sharing_mapt< keyT, valueT, hashT, equalT >::get_leaf_node().
|
protected |
Definition at line 573 of file sharing_map.h.
References sharing_node_innert< keyT, valueT, equalT >::find_child().
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 456 of file sharing_map.h.
References sharing_node_innert< keyT, valueT, equalT >::find_child(), sharing_node_innert< keyT, valueT, equalT >::find_leaf(), sharing_node_innert< keyT, valueT, equalT >::get_container(), sharing_node_innert< keyT, valueT, equalT >::get_to_map(), sharing_node_leaft< keyT, valueT, equalT >::get_value(), SM_ASSERT, and stack.
|
inlineprotected |
Definition at line 300 of file sharing_map.h.
References sharing_node_innert< keyT, valueT, equalT >::find_leaf(), and sharing_mapt< keyT, valueT, hashT, equalT >::get_container_node().
Referenced by sharing_mapt< keyT, valueT, hashT, equalT >::has_key().
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 398 of file sharing_map.h.
References SM_ASSERT.
|
inline |
Check if key is in map.
Complexity:
Definition at line 246 of file sharing_map.h.
References sharing_mapt< keyT, valueT, hashT, equalT >::get_leaf_node().
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 702 of file sharing_map.h.
References as_const(), sharing_node_leaft< keyT, valueT, equalT >::get_value(), sharing_node_innert< keyT, valueT, equalT >::place_leaf(), and SM_ASSERT.
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 725 of file sharing_map.h.
|
protected |
Definition at line 341 of file sharing_map.h.
References small_mapt< T, Ind, Num >::empty(), sharing_node_innert< keyT, valueT, equalT >::get_container(), sharing_node_innert< keyT, valueT, equalT >::get_to_map(), SM_ASSERT, and stack.
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 858 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 740 of file sharing_map.h.
References sharing_node_innert< keyT, valueT, equalT >::find_leaf(), sharing_node_leaft< keyT, valueT, equalT >::get_value(), sharing_node_innert< keyT, valueT, equalT >::place_leaf(), and SM_ASSERT.
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 757 of file sharing_map.h.
|
inline |
Get number of elements in map.
Complexity: O(1)
Definition at line 223 of file sharing_map.h.
References sharing_mapt< keyT, valueT, hashT, equalT >::num.
|
inline |
Swap with other map.
Complexity: O(1)
Definition at line 211 of file sharing_map.h.
References sharing_mapt< keyT, valueT, hashT, equalT >::map, sharing_mapt< keyT, valueT, hashT, equalT >::num, and sharing_node_innert< keyT, valueT, equalT >::swap().
|
friend |
|
friend |
|
friend |
|
friend |
|
staticprotected |
Definition at line 326 of file sharing_map.h.
|
staticprotected |
Definition at line 327 of file sharing_map.h.
|
staticprotected |
Definition at line 321 of file sharing_map.h.
|
protected |
Definition at line 334 of file sharing_map.h.
Referenced by sharing_mapt< keyT, valueT, hashT, equalT >::clear(), and sharing_mapt< keyT, valueT, hashT, equalT >::swap().
|
staticprotected |
Definition at line 330 of file sharing_map.h.
|
staticprotected |
Definition at line 323 of file sharing_map.h.
|
protected |
|
staticprotected |
Definition at line 331 of file sharing_map.h.