12#ifndef CPROVER_UTIL_SHARING_MAP_H
13#define CPROVER_UTIL_SHARING_MAP_H
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>
48#define SHARING_MAPT(type) \ …
57#define SHARING_MAPTV(return_type, V) \
65 return_type sharing_mapt<keyT, valueT, fail_if_equal, hashT, equalT>
57#define SHARING_MAPTV(return_type, V) \ …
72#define SHARING_MAPT2(cv_qualifiers, return_type) \
79 cv_qualifiers typename \
80 sharing_mapt<keyT, valueT, fail_if_equal, hashT, equalT>::return_type \
81 sharing_mapt<keyT, valueT, fail_if_equal, hashT, equalT>
72#define SHARING_MAPT2(cv_qualifiers, return_type) \ …
90#define SHARING_MAPT3(template_parameter, cv_qualifiers, return_type) \
97 template <class template_parameter> \
98 cv_qualifiers typename \
99 sharing_mapt<keyT, valueT, fail_if_equal, hashT, equalT>::return_type \
100 sharing_mapt<keyT, valueT, fail_if_equal, hashT, equalT>
90#define SHARING_MAPT3(template_parameter, cv_qualifiers, return_type) \ …
107#define SHARING_MAPT4(template_parameter, return_type) \
111 bool fail_if_equal, \
114 template <class template_parameter> \
115 return_type sharing_mapt<keyT, valueT, fail_if_equal, hashT, equalT>
107#define SHARING_MAPT4(template_parameter, return_type) \ …
187 typename hashT = std::hash<keyT>,
188 typename equalT = std::equal_to<keyT>>
204 typedef std::vector<key_type>
keyst;
221 typename std::conditional<fail_if_equal, std::equal_to<valueT>, falset>
::
250 typedef typename std::conditional<
252 real_value_comparatort,
288 template <
class valueU>
291 template <
class valueU>
296 replace(k, std::forward<valueU>(m));
300 insert(k, std::forward<valueU>(m));
312 template <
class valueU>
336 std::optional<std::reference_wrapper<const mapped_type>>
384 typedef std::pair<const key_type &, const mapped_type &>
view_itemt;
388 typedef std::vector<view_itemt>
viewt;
523#if !defined(_MSC_VER)
553 template <
class Iterator>
569 template <
class Iterator>
597 template <
class valueU>
627 const std::size_t level,
635 std::set<const void *> &
marked,
636 bool mark =
true)
const;
662 std::stack<const nodet *> stack;
667 const nodet *ip = stack.top();
677 for(
const auto item : m)
679 stack.push(&
item.second);
693 for(
const auto &l :
ll)
695 f(l.get_key(), l.get_value());
698 }
while(!stack.empty());
702::count_unmarked_nodes(
712 std::stack<const nodet *> stack;
717 const nodet *ip = stack.top();
721 const unsigned use_count = ip->
use_count();
751 for(
const auto item : m)
753 stack.push(&
item.second);
772 for(
const auto &l :
ll)
777 }
while(!stack.empty());
702::count_unmarked_nodes( {
…}
782#if !defined(_MSC_VER)
789 std::set<const void *>
marked;
796 for(
Iterator it = begin; it != end; it++)
798 sms.num_nodes += f(it).count_unmarked_nodes(
false,
marked,
false);
804 for(
Iterator it = begin; it != end; it++)
806 sms.num_unique_nodes += f(it).count_unmarked_nodes(
false,
marked,
true);
812 for(
Iterator it = begin; it != end; it++)
814 sms.num_leafs += f(it).count_unmarked_nodes(
true,
marked,
false);
820 for(
Iterator it = begin; it != end; it++)
822 sms.num_unique_leafs += f(it).count_unmarked_nodes(
true,
marked,
true);
784::get_sharing_stats( {
…}
867 const auto &k = leaf.get_key();
870 key >>= level * chunk;
877 std::size_t
bit =
key & mask;
899 if(leaf.shares_with(
l2))
902 if(leaf.get_key() ==
l2.get_key())
904 delta_view.push_back({k, leaf.get_value(),
l2.get_value()});
959 typedef std::pair<const nodet *, const nodet *>
stack_itemt;
960 std::stack<stack_itemt> stack;
971 if(map.shares_with(other.map))
994 if(
ip1->is_internal())
998 if(
ip2->is_internal())
1000 for(
const auto item :
ip1->get_to_map())
1005 p =
ip2->find_child(
item.first);
1014 else if(!
child.shares_with(*p))
1025 for(
const auto item :
ip1->get_to_map())
1041 else if(
ip1->is_leaf())
1045 if(
ip2->is_internal())
1058 {
ip1->get_key(),
ip1->get_value(),
ip2->get_value()});
1073 for(
const auto &
l1 :
ip1->get_container())
1075 if(
l1.shares_with(*
ip2))
1096 for(
const auto &
l1 :
ip1->get_container())
1101 p =
ip2->find_leaf(
k1);
1105 if(!
l1.shares_with(*p))
1119 }
while(!stack.empty());
1141 std::size_t
bit =
key & mask;
1169 const nodet *ip = ↦
1174 std::size_t
bit =
key & mask;
1215 std::size_t
bit =
key & mask;
1219 if(m.size() > 1 ||
del ==
nullptr)
1250 if(std::next(
ll.begin()) ==
ll.end())
1308 std::size_t
bit =
key & mask;
1320 l2.make_leaf(k, std::forward<valueU>(m));
1332 }
while(level < levels);
1358 std::size_t level = 0;
1362 std::size_t
bit =
key & mask;
1373 if(level < levels - 1)
1376 child.make_leaf(k, m);
1383 child.place_leaf(k, std::forward<valueU>(m));
1392 else if(
child.is_internal())
1400 else if(
child.is_leaf())
1403 migrate(level,
key,
bit, *ip, k, std::forward<valueU>(m));
1415 child.place_leaf(k, std::forward<valueU>(m));
1431 "values should not be replaced with equal values to maximize sharing");
1433 lp.set_value(std::forward<valueU>(m));
1447 "sharing_mapt::update should make some change. Consider using read-only "
1448 "method to check if an update is needed beforehand");
1454 const nodet *
lp = get_leaf_node(k);
1457 return std::nullopt;
1459 return std::optional<std::reference_wrapper<const mapped_type>>(
1470SHARING_MAPT(
const std::size_t)::mask = 0xffff >> (16 - chunk);
const T * as_const_ptr(T *t)
Return a pointer to the same object but ensures the type is pointer to const.
virtual void clear()
Reset the abstract state.
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
delta_view_itemt(const key_type &k, const mapped_type &m)
const mapped_type & get_other_map_value() const
const mapped_type * other_m
delta_view_itemt(const key_type &k, const mapped_type &m, const mapped_type &other_m)
bool is_in_both_maps() const
A map implemented as a tree where subtrees can be shared between different maps.
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 nodet * get_leaf_node(const key_type &k) const
sharing_nodet< key_type, mapped_type > nodet
std::size_t count_unmarked_nodes(bool leafs_only, std::set< const void * > &marked, bool mark=true) const
void erase_if_exists(const key_type &k)
Erase element if it exists.
std::conditional< fail_if_equal, std::equal_to< valueT >, falset >::type value_equalt
static void insert_view_item(sorted_viewt &v, view_itemt &&vi)
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.
size_type size() const
Get number of elements in map.
void gather_all(const nodet &n, delta_viewt &delta_view) const
static const std::size_t mask
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, real_value_comparatort, noop_value_comparatort >::type value_comparatort
void iterate(const nodet &n, std::function< void(const key_type &k, const mapped_type &m)> f) const
std::vector< view_itemt > viewt
View of the key-value pairs in the map.
static void insert_view_item(viewt &v, view_itemt &&vi)
std::vector< key_type > keyst
void insert(const key_type &k, valueU &&m)
Insert element, element must not exist in map.
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.
void erase(const key_type &k)
Erase element, element must exist in map.
bool has_key(const key_type &k) const
Check if key is in map.
std::pair< const key_type &, const mapped_type & > view_itemt
nodet & get_leaf_node(const key_type &k)
void replace(const key_type &k, valueU &&m)
Replace element, element must exist in map.
static sharing_map_statst get_sharing_stats_map(Iterator begin, Iterator end)
Get sharing stats.
std::vector< delta_view_itemt > delta_viewt
Delta view of the key-value pairs in two maps.
static const std::size_t bits
bool empty() const
Check if map is empty.
void swap(sharing_mapt &other)
Swap with other map.
sorted_viewt get_sorted_view() const
Convenience function to get a sorted view of the map elements.
std::optional< std::reference_wrapper< const mapped_type > > find(const key_type &k) const
Find element.
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.
static const std::size_t levels
static const std::size_t chunk
std::set< view_itemt > sorted_viewt
nodet::leaf_listt leaf_listt
static const std::size_t dummy_level
void insert_or_replace(const key_type &k, valueU &&m)
delta_viewt get_delta_view(const sharing_mapt &other, const bool only_common=true) const
void get_view(V &view) const
Get a view of the elements in the map A view is a list of pairs with the components being const refer...
void update(const key_type &k, std::function< void(mapped_type &)> mutator)
Update an element in place; element must exist in map.
bool is_defined_container() const
bool is_defined_internal() const
void swap(sharing_nodet &other)
void place_leaf(const keyT &k, valueU &&v)
d_ct::leaf_listt leaf_listt
const leaf_listt & get_container() const
bool is_defined_leaf() const
const valueT & get_value() const
const d_it::innert * find_child(const std::size_t n) const
const d_it & read_internal() const
use_countt use_count() const
const leaft * find_leaf(const keyT &k) const
bool shares_with(const sharing_nodet &other) const
d_it::innert & add_child(const std::size_t n)
const to_mapt & get_to_map() const
bool is_container() const
const d_ct & read_container() const
void remove_leaf(const keyT &k)
const keyT & get_key() const
const d_lt & read_leaf() const
#define SHARING_MAPT(type)
Macro to abbreviate the out-of-class definitions of methods and static variables of sharing_mapt.
#define SHARING_MAPTV(return_type, V)
#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...
#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...
#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...
#define UNREACHABLE
This should be used to mark dead code.
#define PRECONDITION(CONDITION)
#define INVARIANT(CONDITION, REASON)
This macro uses the wrapper function 'invariant_violated_string'.
void replace(const union_find_replacet &replace_map, string_not_contains_constraintt &constraint)
bool operator()(const mapped_type &lhs, const mapped_type &rhs)
bool operator()(const mapped_type &)
noop_value_comparatort(const mapped_type &)
bool operator()(const mapped_type &new_value)
real_value_comparatort(const mapped_type &old_value)
Stats about sharing between several sharing map instances.
std::size_t num_unique_leafs
std::size_t num_unique_nodes