12 #ifndef CPROVER_UTIL_SHARING_MAP_H 13 #define CPROVER_UTIL_SHARING_MAP_H 30 #define _sm_assert(b) assert(b) 33 #define SHARING_MAPT(R) \ 34 template <class keyT, class valueT, class hashT, class predT> \ 35 R sharing_mapt<keyT, valueT, hashT, predT> 37 #define SHARING_MAPT2(CV, ST) \ 38 template <class keyT, class valueT, class hashT, class predT> \ 39 CV typename sharing_mapt<keyT, valueT, hashT, predT>::ST \ 40 sharing_mapt<keyT, valueT, hashT, predT> 45 class hashT=std::hash<keyT>,
46 class predT=std::equal_to<keyT>>
61 typedef std::pair<const key_type, mapped_type>
value_type;
72 typedef const std::pair<mapped_type &, const bool>
find_type;
74 typedef std::vector<key_type>
keyst;
111 const mapped_type &v,
120 const mapped_type &v);
123 const value_type &p);
129 const_find_type
find(
const key_type &k)
const;
135 const mapped_type &
at(
const key_type &k)
const;
171 typedef std::pair<const key_type &, const mapped_type &>
view_itemt;
172 typedef std::vector<view_itemt>
viewt;
180 const mapped_type &
m,
193 const mapped_type &
m;
202 const self_type &other,
203 delta_viewt &delta_view,
204 const bool only_common=
true)
const;
214 void gather_all(
const node_type &n, delta_viewt &delta_view)
const;
219 assert(view.empty());
221 std::stack<const node_type *>
stack;
230 const node_type *n=stack.top();
237 view.push_back(
view_itemt(child.get_key(), child.get_value()));
244 for(
const auto &child : n->
get_sub())
246 stack.push(&child.second);
250 while(!stack.empty());
256 std::stack<const node_type *>
stack;
261 const node_type *n=stack.top();
268 delta_view.push_back(
280 for(
const auto &child : n->
get_sub())
282 stack.push(&child.second);
286 while(!stack.empty());
290 const self_type &other,
292 const bool only_common) const
294 assert(delta_view.empty());
296 typedef std::pair<const node_type *, const node_type *> stack_itemt;
297 std::stack<stack_itemt>
stack;
311 stack.push(stack_itemt(&map, &other.map));
315 const stack_itemt si=stack.top();
318 const node_type *n1=si.first;
319 const node_type *n2=si.second;
325 for(
const auto &child : n1->
get_sub())
337 else if(!child.second.shares_with(*p))
339 stack.push(stack_itemt(&child.second, p));
349 const key_type &k1=l1.get_key();
354 const key_type &k2=l2.get_key();
356 if(l1.shares_with(l2))
364 delta_view.push_back(
376 if(!only_common && !found)
378 delta_view.push_back(
392 while(!stack.empty());
397 size_t key=
hash()(
k);
400 for(
unsigned i=0; i<
steps; i++)
402 unsigned bit=key&
mask;
413 size_t key=
hash()(
k);
414 const node_type *p=&
map;
416 for(
unsigned i=0; i<
steps; i++)
418 unsigned bit=key&
mask;
444 const
tvt &key_exists)
446 assert(!key_exists.is_false());
449 if(key_exists.is_unknown() && !
has_key(k))
452 node_type *del=
nullptr;
455 size_t key=
hash()(
k);
458 for(
unsigned i=0; i<
steps; i++)
460 unsigned bit=key&
mask;
463 const subt &sub=
as_const(p)->get_sub();
464 if(sub.size()>1 || del==
nullptr)
476 const containert &c=
as_const(p)->get_container();
496 const
tvt &key_exists)
500 for(
const key_type &k : ks)
502 cnt+=
erase(k, key_exists);
510 const mapped_type &
m,
511 const
tvt &key_exists)
515 if(key_exists.is_unknown())
517 const node_type *p=
as_const(
this)->get_leaf_node(k);
525 p=p->place_leaf(k,
m);
533 const
tvt &key_exists)
535 return insert(p.first, p.second, key_exists);
540 const mapped_type &
m)
559 return place(p.first, p.second);
564 const
tvt &key_exists)
568 if(key_exists.is_unknown() && !
has_key(k))
593 const
tvt &key_exists)
595 find_type
r=
find(k, key_exists);
598 throw std::out_of_range(not_found_msg);
605 const_find_type
r=
find(k);
607 throw std::out_of_range(not_found_msg);
619 SHARING_MAPT(
const std::string)::not_found_msg=
"key not found";
static const size_t chunk
void swap(self_type &other)
void remove_child(const unsigned n)
std::pair< const key_type &, const mapped_type & > view_itemt
friend void sharing_map_collision_test()
std::vector< delta_view_itemt > delta_viewt
sharing_nodet< key_type, mapped_type, key_equal > node_type
void remove_leaf(const key_type &k)
std::vector< key_type > keyst
friend void sharing_map_interface_test()
size_type erase(const key_type &k, const tvt &key_exists=tvt::unknown())
const_find_type insert(const key_type &k, const mapped_type &v, const tvt &key_exists=tvt::unknown())
static const std::string not_found_msg
static const size_t steps
self_type * place_leaf(const key_type &k, const mapped_type &m)
void get_delta_view(const self_type &other, delta_viewt &delta_view, const bool only_common=true) const
node_type * get_container_node(const key_type &k)
const mapped_type & other_m
const self_type * find_leaf(const key_type &k) const
const std::pair< mapped_type &, const bool > find_type
const mapped_type & get_value() const
containert & get_container()
mapped_type & operator[](const key_type &k)
bool has_key(const key_type &k) const
friend void sharing_map_view_test()
find_type place(const key_type &k, const mapped_type &v)
node_type::containert containert
bool is_container() const
mapped_type & at(const key_type &k, const tvt &key_exists=tvt::unknown())
const node_type * get_leaf_node(const key_type &k) const
delta_view_itemt(const bool in_both, const key_type &k, const mapped_type &m, const mapped_type &other_m)
const std::pair< const mapped_type &, const bool > const_find_type
find_type find(const key_type &k, const tvt &key_exists=tvt::unknown())
#define SHARING_MAPT2(CV, ST)
void get_view(viewt &view) const
std::pair< const key_type, mapped_type > value_type
size_type erase_all(const keyst &ks, const tvt &key_exists=tvt::unknown())
sharing_mapt< key_type, mapped_type, hash, key_equal > self_type
self_type * add_child(const unsigned n)
void gather_all(const node_type &n, delta_viewt &delta_view) const
std::vector< view_itemt > viewt
void swap(self_type &other)
const self_type * find_child(const unsigned n) const
std::map< unsigned, self_type > subt
std::list< self_type > containert
friend void sharing_map_copy_test()