12 #ifndef CPROVER_UTIL_SHARING_MAP_H 13 #define CPROVER_UTIL_SHARING_MAP_H 32 #ifdef SM_INTERNAL_CHECKS 33 #define SM_ASSERT(b) INVARIANT(b, "Sharing map internal invariant") 39 #define SHARING_MAPT(R) \ 40 template <class keyT, class valueT, class hashT, class equalT> \ 41 R sharing_mapt<keyT, valueT, hashT, equalT> 43 #define SHARING_MAPT2(CV, ST) \ 44 template <class keyT, class valueT, class hashT, class equalT> \ 45 CV typename sharing_mapt<keyT, valueT, hashT, equalT>::ST \ 46 sharing_mapt<keyT, valueT, hashT, equalT> 48 #define SHARING_MAPT3(T, CV, ST) \ 49 template <class keyT, class valueT, class hashT, class equalT> \ 51 CV typename sharing_mapt<keyT, valueT, hashT, equalT>::ST \ 52 sharing_mapt<keyT, valueT, hashT, equalT> 126 template <
class keyT,
128 class hashT = std::hash<keyT>,
129 class equalT = std::equal_to<keyT>>
156 typedef const std::pair<mapped_type &, const bool>
find_type;
158 typedef std::vector<key_type>
keyst;
216 std::size_t tmp =
num;
254 typedef std::pair<const key_type &, const mapped_type &>
view_itemt;
258 typedef std::vector<view_itemt>
viewt;
293 const bool only_common =
true)
const;
314 template <
class Iterator>
319 [](
const Iterator it) ->
sharing_mapt & {
return *it; });
321 template <
class Iterator>
344 const unsigned start_depth,
352 std::set<void *> &marked,
353 bool mark =
true)
const;
378 unsigned start_depth,
381 typedef std::pair<unsigned, const baset *> stack_itemt;
383 std::stack<stack_itemt>
stack;
384 stack.push({start_depth, &n});
388 const stack_itemt &si =
stack.top();
390 const unsigned depth = si.first;
391 const baset *bp = si.second;
397 const innert *ip = static_cast<const innert *>(bp);
401 for(
const auto &item : m)
403 const innert *i = &item.second;
404 stack.push({depth + 1, i});
411 const innert *cp = static_cast<const innert *>(bp);
415 for(
const auto &l : ll)
417 f(l.get_key(), l.get_value());
421 while(!
stack.empty());
425 ::count_unmarked_nodes(bool leafs_only, std::set<void *> &marked, bool mark)
433 typedef std::pair<unsigned, const baset *> stack_itemt;
435 std::stack<stack_itemt>
stack;
436 stack.push({0, &map});
440 const stack_itemt &si =
stack.top();
442 const unsigned depth = si.first;
443 const baset *bp = si.second;
448 const innert *ip = static_cast<const innert *>(bp);
450 void *raw_ptr = ip->
data.
get();
454 if(marked.find(raw_ptr) != marked.end())
461 marked.insert(raw_ptr);
475 for(
const auto &item : m)
477 const innert *i = &item.second;
478 stack.push({depth + 1, i});
488 for(
const auto &l : ll)
490 const unsigned leaf_use_count = l.data.use_count();
491 void *leaf_raw_ptr = l.data.get();
493 if(leaf_use_count >= 2)
495 if(marked.find(leaf_raw_ptr) != marked.end())
502 marked.insert(leaf_raw_ptr);
509 }
while(!
stack.empty());
530 std::set<void *> marked;
537 for(Iterator it = begin; it != end; it++)
539 sms.
num_nodes += f(it).count_unmarked_nodes(
false, marked,
false);
545 for(Iterator it = begin; it != end; it++)
553 for(Iterator it = begin; it != end; it++)
555 sms.
num_leafs += f(it).count_unmarked_nodes(
true, marked,
false);
561 for(Iterator it = begin; it != end; it++)
579 ::get_sharing_stats_map(Iterator begin, Iterator end)
581 return get_sharing_stats<Iterator>(
582 begin, end, [](
const Iterator it) ->
sharing_mapt & {
return it->second; });
615 iterate(n, depth, f);
655 const bool only_common) const
666 gather_all(map, 0, delta_view);
672 typedef std::tuple<unsigned, const baset *, const baset *> stack_itemt;
673 std::stack<stack_itemt>
stack;
682 stack.push(stack_itemt(0, &map, &other.map));
686 const stack_itemt &si =
stack.top();
688 const unsigned depth = std::get<0>(si);
689 const baset *bp1 = std::get<1>(si);
690 const baset *bp2 = std::get<2>(si);
696 const innert *ip1 = static_cast<const innert *>(bp1);
697 const innert *ip2 = static_cast<const innert *>(bp2);
701 for(
const auto &item : m)
710 gather_all(item.second, depth + 1, delta_view);
713 else if(!item.second.shares_with(*p))
715 stack.push(stack_itemt(depth + 1, &item.second, p));
723 const innert *cp1 = static_cast<const innert *>(bp1);
724 const innert *cp2 = static_cast<const innert *>(bp2);
728 for(
const auto &l1 : ll1)
737 if(!l1.shares_with(*p))
739 delta_view.push_back({
true, k1, l1.get_value(), p->
get_value()});
742 else if(!only_common)
744 delta_view.push_back({
false, l1.get_key(), l1.get_value(), dummy});
749 while(!
stack.empty());
754 std::size_t key =
hash()(k);
757 for(std::size_t i = 0; i < steps; i++)
759 std::size_t bit = key & mask;
774 std::size_t key =
hash()(k);
777 for(std::size_t i = 0; i < steps; i++)
779 std::size_t bit = key & mask;
803 SM_ASSERT(!key_exists.is_true() || has_key(k));
806 if(key_exists.is_unknown() && !has_key(k))
810 std::size_t del_bit = 0;
811 std::size_t del_level = 0;
813 std::size_t key =
hash()(k);
816 for(std::size_t i = 0; i < steps; i++)
818 std::size_t bit = key & mask;
822 if(m.
size() > 1 || del ==
nullptr)
837 if(!ll.empty() && std::next(ll.begin()) == ll.end())
839 if(del_level < steps - 1)
873 ::erase_all(const
keyst &ks, const
tvt &key_exists)
879 cnt+=erase(k, key_exists);
901 SM_ASSERT(!key_exists.is_false() || !has_key(k));
903 if(key_exists.is_unknown())
910 innert *cp = get_container_node(k);
923 return insert(p.first, p.second, key_exists);
938 innert *cp = get_container_node(k);
955 return place(p.first, p.second);
972 SM_ASSERT(!key_exists.is_true() || has_key(k));
974 if(key_exists.is_unknown() && !has_key(k))
977 innert *cp = get_container_node(k);
997 const leaft *lp = get_leaf_node(k);
1018 const
tvt &key_exists)
1023 throw std::out_of_range(not_found_msg);
1041 throw std::out_of_range(not_found_msg);
1061 SHARING_MAPT(
const std::string)::not_found_msg=
"key not found";
1068 SHARING_MAPT(
const std::size_t)::mask = 0xffff >> (16 - chunk);
bool empty() const
Check if map is empty.
void swap(sharing_mapt &other)
Swap with other map.
static sharing_map_statst get_sharing_stats_map(Iterator begin, Iterator end)
Get sharing stats.
void swap(sharing_node_innert &other)
sharing_node_innert< key_type, mapped_type > innert
find_type place(const key_type &k, const mapped_type &v)
Insert element, return non-const reference.
void remove_leaf(const keyT &k)
const to_mapt & get_to_map() const
std::size_t num_unique_leafs
std::size_t count_unmarked_nodes(bool leafs_only, std::set< void * > &marked, bool mark=true) const
leaft * place_leaf(const keyT &k, const valueT &v)
A map implemented as a tree where subtrees can be shared between different maps.
delta_view_itemt(const bool in_both, const key_type &k, const mapped_type &m, const mapped_type &other_m)
const d_it::innert * find_child(const std::size_t n) const
Stats about sharing between several sharing map instances.
use_countt use_count() const
std::vector< key_type > keyst
bool has_key(const key_type &k) const
Check if key is in map.
mapped_type & at(const key_type &k, const tvt &key_exists=tvt::unknown())
Get element at key.
static const std::size_t chunk
mapped_type & operator[](const key_type &k)
Get element at key, insert new if non-existent.
std::vector< view_itemt > viewt
View of the key-value pairs in the map.
size_type size() const
Get number of elements in map.
d_it::innert * add_child(const std::size_t n)
void iterate(const baset &n, const unsigned start_depth, std::function< void(const key_type &k, const mapped_type &m)> f) const
const leaf_listt & get_container() const
unsignedbv_typet size_type()
sharing_node_leaft< key_type, mapped_type > leaft
const std::pair< mapped_type &, const bool > find_type
Return type of methods that retrieve a reference to a value.
size_type erase(const key_type &k, const tvt &key_exists=tvt::unknown())
Erase element.
const valueT & get_value() const
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.
find_type find(const key_type &k, const tvt &key_exists=tvt::unknown())
Find element.
std::pair< const key_type &, const mapped_type & > view_itemt
size_type erase_all(const keyst &ks, const tvt &key_exists=tvt::unknown())
Erase all elements.
innert::leaf_listt leaf_listt
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...
static const std::size_t steps
std::pair< const key_type, mapped_type > value_type
static const std::size_t mask
small_shared_two_way_ptrt< d_internalt< keyT, valueT, equalT >, d_containert< keyT, valueT, equalT > > data
std::size_t num_unique_nodes
static const std::string not_found_msg
d_ct::leaf_listt leaf_listt
#define SHARING_MAPT2(CV, ST)
const_find_type insert(const key_type &k, const mapped_type &v, const tvt &key_exists=tvt::unknown())
Insert element, return const reference.
#define SHARING_MAPT3(T, CV, ST)
const mapped_type & other_m
void gather_all(const baset &n, const unsigned depth, delta_viewt &delta_view) const
static const std::size_t bits
const std::pair< const mapped_type &, const bool > const_find_type
Return type of methods that retrieve a const reference to a value.
const leaft * get_leaf_node(const key_type &k) const
const leaft * find_leaf(const keyT &k) const
void remove_child(const std::size_t n)
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::vector< delta_view_itemt > delta_viewt
Delta view of the key-value pairs in two maps.
innert * get_container_node(const key_type &k)