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())
907 return const_find_type(lp->
get_value(),
false);
910 innert *cp = get_container_node(k);
916 return const_find_type(lp->
get_value(),
true);
923 return insert(p.first, p.second, key_exists);
938 innert *cp = get_container_node(k);
944 return find_type(lp->
get_value(),
false);
949 return find_type(lp->get_value(),
true);
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))
975 return find_type(dummy,
false);
977 innert *cp = get_container_node(k);
997 const leaft *lp = get_leaf_node(k);
1000 return const_find_type(dummy,
false);
1002 return const_find_type(lp->
get_value(),
true);
1018 const
tvt &key_exists)
1020 find_type
r=find(k, key_exists);
1023 throw std::out_of_range(not_found_msg);
1039 const_find_type
r=find(k);
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);