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> 120 template <
class keyT,
122 class hashT = std::hash<keyT>,
123 class equalT = std::equal_to<keyT>>
155 typedef const std::pair<mapped_type &, const bool>
find_type;
157 typedef std::vector<key_type>
keyst;
215 std::size_t tmp =
num;
253 typedef std::pair<const key_type &, const mapped_type &>
view_itemt;
257 typedef std::vector<view_itemt>
viewt;
292 const bool only_common =
true)
const;
314 const unsigned depth,
346 typedef std::pair<unsigned, const baset *> stack_itemt;
348 std::stack<stack_itemt>
stack;
349 stack.push({depth, &n});
353 const stack_itemt &si =
stack.top();
355 const unsigned depth = si.first;
356 const baset *bp = si.second;
366 for(
const auto &item : m)
368 const innert *i = &item.second;
369 stack.push({depth + 1, i});
380 for(
const auto &l : ll)
382 f(l.get_key(), l.get_value());
386 while(!
stack.empty());
419 iterate(n, depth, f);
459 const bool only_common) const
470 gather_all(map, 0, delta_view);
476 typedef std::tuple<unsigned, const baset *, const baset *> stack_itemt;
477 std::stack<stack_itemt>
stack;
486 stack.push(stack_itemt(0, &map, &other.map));
490 const stack_itemt &si =
stack.top();
492 const unsigned depth = std::get<0>(si);
493 const baset *bp1 = std::get<1>(si);
494 const baset *bp2 = std::get<2>(si);
505 for(
const auto &item : m)
514 gather_all(item.second, depth + 1, delta_view);
517 else if(!item.second.shares_with(*p))
519 stack.push(stack_itemt(depth + 1, &item.second, p));
532 for(
const auto &l1 : ll1)
541 if(!l1.shares_with(*p))
543 delta_view.push_back({
true, k1, l1.get_value(), p->
get_value()});
546 else if(!only_common)
548 delta_view.push_back({
false, l1.get_key(), l1.get_value(), dummy});
553 while(!
stack.empty());
558 std::size_t key =
hash()(k);
561 for(std::size_t i = 0; i < steps; i++)
563 std::size_t bit = key & mask;
578 std::size_t key =
hash()(k);
581 for(std::size_t i = 0; i < steps; i++)
583 std::size_t bit = key & mask;
607 SM_ASSERT(!key_exists.is_true() || has_key(k));
610 if(key_exists.is_unknown() && !has_key(k))
614 std::size_t del_bit = 0;
615 std::size_t del_level = 0;
617 std::size_t key =
hash()(k);
620 for(std::size_t i = 0; i < steps; i++)
622 std::size_t bit = key & mask;
626 if(m.
size() > 1 || del ==
nullptr)
641 if(!ll.empty() && std::next(ll.begin()) == ll.end())
643 if(del_level < steps - 1)
677 ::erase_all(const
keyst &ks, const
tvt &key_exists)
683 cnt+=erase(k, key_exists);
705 SM_ASSERT(!key_exists.is_false() || !has_key(k));
707 if(key_exists.is_unknown())
714 innert *cp = get_container_node(k);
727 return insert(p.first, p.second, key_exists);
742 innert *cp = get_container_node(k);
759 return place(p.first, p.second);
776 SM_ASSERT(!key_exists.is_true() || has_key(k));
778 if(key_exists.is_unknown() && !has_key(k))
781 innert *cp = get_container_node(k);
801 const leaft *lp = get_leaf_node(k);
822 const
tvt &key_exists)
827 throw std::out_of_range(not_found_msg);
845 throw std::out_of_range(not_found_msg);
865 SHARING_MAPT(
const std::string)::not_found_msg=
"key not found";
872 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.
void swap(sharing_node_innert &other)
sharing_node_innert< key_type, mapped_type > innert
friend void sharing_map_collision_test()
void iterate(const baset &n, const unsigned depth, std::function< void(const key_type &k, const mapped_type &m)> f) const
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
friend void sharing_map_interface_test()
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
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)
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.
friend void sharing_map_view_test()
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
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.
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)
friend void sharing_map_copy_test()
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)