Go to the documentation of this file.
12 #ifndef CPROVER_UTIL_SHARING_MAP_H
13 #define CPROVER_UTIL_SHARING_MAP_H
27 #include <type_traits>
36 #ifdef SM_INTERNAL_CHECKS
37 #define SM_ASSERT(b) INVARIANT(b, "Sharing map internal invariant")
48 #define SHARING_MAPT(type) \
55 type sharing_mapt<keyT, valueT, fail_if_equal, hashT, equalT>
62 #define SHARING_MAPT2(cv_qualifiers, return_type) \
69 cv_qualifiers typename \
70 sharing_mapt<keyT, valueT, fail_if_equal, hashT, equalT>::return_type \
71 sharing_mapt<keyT, valueT, fail_if_equal, hashT, equalT>
80 #define SHARING_MAPT3(template_parameter, cv_qualifiers, return_type) \
87 template <class template_parameter> \
88 cv_qualifiers typename \
89 sharing_mapt<keyT, valueT, fail_if_equal, hashT, equalT>::return_type \
90 sharing_mapt<keyT, valueT, fail_if_equal, hashT, equalT>
97 #define SHARING_MAPT4(template_parameter, return_type) \
101 bool fail_if_equal, \
104 template <class template_parameter> \
105 return_type sharing_mapt<keyT, valueT, fail_if_equal, hashT, equalT>
176 bool fail_if_equal =
false,
177 typename hashT = std::hash<keyT>,
178 typename equalT = std::equal_to<keyT>>
194 typedef std::vector<key_type>
keyst;
211 typename std::conditional<fail_if_equal, std::equal_to<valueT>, falset>::
240 typedef typename std::conditional<
242 real_value_comparatort,
278 template <
class valueU>
289 template <
class valueU>
323 std::size_t tmp =
num;
361 typedef std::pair<const key_type &, const mapped_type &>
view_itemt;
365 typedef std::vector<view_itemt>
viewt;
454 const bool only_common =
true)
const;
468 #if !defined(_MSC_VER)
469 struct sharing_map_statst
498 template <
class Iterator>
503 [](
const Iterator it) ->
sharing_mapt & {
return *it; });
514 template <
class Iterator>
542 template <
class valueU>
544 const std::size_t starting_level,
545 const std::size_t key_suffix,
546 const std::size_t bit_last,
572 const std::size_t level,
574 const bool only_common)
const;
580 std::set<const void *> &marked,
581 bool mark =
true)
const;
607 std::stack<const nodet *> stack;
612 const nodet *ip = stack.top();
622 for(
const auto item : m)
624 stack.push(&item.second);
638 for(
const auto &l : ll)
640 f(l.get_key(), l.get_value());
644 while(!stack.empty());
648 ::count_unmarked_nodes(
650 std::set<const void *> &marked,
658 std::stack<const nodet *> stack;
663 const nodet *ip = stack.top();
667 const unsigned use_count = ip->
use_count();
669 const void *raw_ptr =
676 if(marked.find(raw_ptr) != marked.end())
683 marked.insert(raw_ptr);
697 for(
const auto item : m)
699 stack.push(&item.second);
718 for(
const auto &l : ll)
723 }
while(!stack.empty());
728 #if !defined(_MSC_VER)
735 std::set<const void *> marked;
742 for(Iterator it = begin; it != end; it++)
744 sms.num_nodes += f(it).count_unmarked_nodes(
false, marked,
false);
750 for(Iterator it = begin; it != end; it++)
752 sms.num_unique_nodes += f(it).count_unmarked_nodes(
false, marked,
true);
758 for(Iterator it = begin; it != end; it++)
760 sms.num_leafs += f(it).count_unmarked_nodes(
true, marked,
false);
766 for(Iterator it = begin; it != end; it++)
768 sms.num_unique_leafs += f(it).count_unmarked_nodes(
true, marked,
true);
775 ::get_sharing_stats_map(Iterator begin, Iterator end)
777 return get_sharing_stats<Iterator>(
778 begin, end, [](
const Iterator it) ->
sharing_mapt & {
return it->second; });
809 const std::size_t level,
811 const bool only_common) const
813 const auto &k = leaf.get_key();
814 std::size_t key =
hash()(k);
816 key >>= level * chunk;
818 const nodet *ip = &inner;
823 std::size_t bit = key & mask;
832 delta_view.push_back({k, leaf.get_value()});
845 if(leaf.shares_with(l2))
848 if(leaf.get_key() == l2.get_key())
850 delta_view.push_back({k, leaf.get_value(), l2.get_value()});
855 delta_view.push_back({k, leaf.get_value()});
865 if(equalT()(leaf.get_key(), ip->
get_key()))
867 delta_view.push_back({k, leaf.get_value(), ip->
get_value()});
871 delta_view.push_back({k, leaf.get_value()});
884 const bool only_common) const
895 gather_all(map, delta_view);
901 typedef std::pair<const nodet *, const nodet *> stack_itemt;
902 std::stack<stack_itemt> stack;
904 std::stack<std::size_t> level_stack;
913 if(map.shares_with(other.map))
916 stack.push(stack_itemt(&map, &other.map));
921 const stack_itemt &si = stack.top();
923 const nodet *ip1 = si.first;
924 const nodet *ip2 = si.second;
930 const std::size_t level = level_stack.top();
944 const nodet &child = item.second;
953 gather_all(child, delta_view);
958 stack.push(stack_itemt(&child, p));
959 level_stack.push(level + 1);
969 const nodet &child = item.second;
973 stack.push(stack_itemt(&child, ip2));
978 level_stack.push(dummy_level);
991 add_item_if_not_shared(*ip1, *ip2, level, delta_view, only_common);
999 delta_view.push_back(
1002 else if(!only_common)
1017 if(l1.shares_with(*ip2))
1024 if(equalT()(k1, ip2->
get_key()))
1026 delta_view.push_back({k1, l1.get_value(), ip2->
get_value()});
1028 else if(!only_common)
1030 delta_view.push_back({k1, l1.get_value()});
1047 if(!l1.shares_with(*p))
1050 delta_view.push_back({k1, l1.get_value(), p->
get_value()});
1053 else if(!only_common)
1056 delta_view.push_back({k1, l1.get_value()});
1062 while(!stack.empty());
1069 std::size_t key =
hash()(k);
1075 std::size_t bit = key & mask;
1102 std::size_t key =
hash()(k);
1103 const nodet *ip = ↦
1108 std::size_t bit = key & mask;
1124 return equalT()(ip->
get_key(), k) ? ip :
nullptr;
1141 nodet *del =
nullptr;
1142 std::size_t del_bit = 0;
1144 std::size_t key =
hash()(k);
1149 std::size_t bit = key & mask;
1153 if(m.
size() > 1 || del ==
nullptr)
1184 if(std::next(ll.begin()) == ll.end())
1205 const std::size_t starting_level,
1206 const std::size_t key_suffix,
1207 const std::size_t bit_last,
1218 std::size_t key_existing =
hash()(leaf.
get_key());
1219 key_existing >>= chunk * starting_level;
1222 leaf_kept.
swap(leaf);
1229 std::size_t level = starting_level + 1;
1230 std::size_t key = key_suffix;
1232 key_existing >>= chunk;
1241 std::size_t bit_existing = key_existing & mask;
1242 std::size_t bit = key & mask;
1244 if(bit != bit_existing)
1254 l2.
make_leaf(k, std::forward<valueU>(m));
1263 key_existing >>= chunk;
1266 }
while(level < levels);
1286 std::size_t key =
hash()(k);
1292 std::size_t level = 0;
1296 std::size_t bit = key & mask;
1307 if(level < levels - 1)
1317 child.
place_leaf(k, std::forward<valueU>(m));
1337 migrate(level, key, bit, *ip, k, std::forward<valueU>(m));
1349 child.
place_leaf(k, std::forward<valueU>(m));
1361 nodet &lp = get_leaf_node(k);
1365 "values should not be replaced with equal values to maximize sharing");
1373 nodet &lp = get_leaf_node(k);
1381 "sharing_mapt::update should make some change. Consider using read-only "
1382 "method to check if an update is needed beforehand");
1388 const nodet *lp = get_leaf_node(k);
1403 SHARING_MAPT(
const std::size_t)::mask = 0xffff >> (16 - chunk);
1404 SHARING_MAPT(
const std::size_t)::levels = bits / chunk;
const d_it & read_internal() const
std::vector< delta_view_itemt > delta_viewt
Delta view of the key-value pairs in two maps.
#define UNREACHABLE
This should be used to mark dead code.
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
bool is_defined_leaf() const
Stats about sharing between several sharing map instances.
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.
void gather_all(const nodet &n, delta_viewt &delta_view) const
d_ct::leaf_listt leaf_listt
#define SHARING_MAPT(type)
Macro to abbreviate the out-of-class definitions of methods and static variables of sharing_mapt.
size_type size() const
Get number of elements in map.
const keyT & get_key() const
bool is_in_both_maps() const
A map implemented as a tree where subtrees can be shared between different maps.
static const std::size_t levels
void update(const key_type &k, std::function< void(mapped_type &)> mutator)
Update an element in place; element must exist in map.
const d_ct & read_container() const
std::conditional< fail_if_equal, real_value_comparatort, noop_value_comparatort >::type value_comparatort
void erase_if_exists(const key_type &k)
Erase element if it exists.
use_countt use_count() const
void replace(const union_find_replacet &replace_map, string_not_contains_constraintt &constraint)
std::size_t count_unmarked_nodes(bool leafs_only, std::set< const void * > &marked, bool mark=true) const
bool operator()(const mapped_type &)
const d_lt & read_leaf() const
static const std::size_t chunk
bool is_defined_container() const
bool is_defined_internal() const
const leaf_listt & get_container() const
void remove_leaf(const keyT &k)
std::size_t num_unique_leafs
void add_item_if_not_shared(const nodet &leaf, const nodet &inner, const std::size_t level, delta_viewt &delta_view, const bool only_common) const
Add a delta item to the delta view if the value in the container (which must only contain a single le...
const valueT & get_value() const
#define SHARING_MAPT4(template_parameter, return_type)
Macro to abbreviate the out-of-class definitions of template methods of sharing_mapt with a single te...
static sharing_map_statst get_sharing_stats_map(Iterator begin, Iterator end)
Get sharing stats.
real_value_comparatort(const mapped_type &old_value)
std::pair< const key_type &, const mapped_type & > view_itemt
std::vector< view_itemt > viewt
View of the key-value pairs in the map.
void iterate(const nodet &n, std::function< void(const key_type &k, const mapped_type &m)> f) const
const to_mapt & get_to_map() const
std::size_t num_unique_nodes
std::vector< key_type > keyst
const mapped_type & get_other_map_value() const
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.
std::conditional< fail_if_equal, std::equal_to< valueT >, falset >::type value_equalt
#define PRECONDITION(CONDITION)
static const std::size_t mask
void place_leaf(const keyT &k, valueU &&v)
bool empty() const
Check if map is empty.
void swap(sharing_nodet &other)
bool shares_with(const sharing_nodet &other) const
void remove_child(const std::size_t n)
delta_view_itemt(const key_type &k, const mapped_type &m)
nonstd::optional< T > optionalt
bool has_key(const key_type &k) const
Check if key is in map.
void insert(const key_type &k, valueU &&m)
Insert element, element must not exist in map.
static const std::size_t dummy_level
void swap(sharing_mapt &other)
Swap with other map.
const leaft * find_leaf(const keyT &k) const
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 refer...
const d_it::innert * find_child(const std::size_t n) const
sharing_nodet< key_type, mapped_type > nodet
static const std::size_t bits
void replace(const key_type &k, valueU &&m)
Replace element, element must exist in map.
void migrate(const std::size_t starting_level, const std::size_t key_suffix, const std::size_t bit_last, nodet &inner, const key_type &k, valueU &&m)
Move a leaf node further down the tree such as to resolve a collision with another key-value pair.
nodet & get_leaf_node(const key_type &k)
bool operator()(const mapped_type &lhs, const mapped_type &rhs)
const mapped_type * other_m
noop_value_comparatort(const mapped_type &)
#define SHARING_MAPT3(template_parameter, cv_qualifiers, return_type)
Macro to abbreviate the out-of-class definitions of template methods of sharing_mapt with a single te...
const nodet * get_leaf_node(const key_type &k) const
d_it::innert & add_child(const std::size_t n)
bool is_container() const
void iterate(std::function< void(const key_type &k, const mapped_type &m)> f) const
Call a function for every key-value pair in the map.
#define SHARING_MAPT2(cv_qualifiers, return_type)
Macro to abbreviate the out-of-class definitions of methods of sharing_mapt with a return type that i...
void set_value(valueU &&v)
#define INVARIANT(CONDITION, REASON)
This macro uses the wrapper function 'invariant_violated_string'.
void mutate_value(std::function< void(valueT &)> mutator)
void erase(const key_type &k)
Erase element, element must exist in map.
void make_leaf(const keyT &k, valueU &&v)
const T * as_const_ptr(T *t)
Return a pointer to the same object but ensures the type is pointer to const.
optionalt< std::reference_wrapper< const mapped_type > > find(const key_type &k) const
Find element.
bool operator()(const mapped_type &new_value)
delta_view_itemt(const key_type &k, const mapped_type &m, const mapped_type &other_m)
nodet::leaf_listt leaf_listt