cprover
sharing_map.h
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module: Sharing map
4 
5 Author: Daniel Poetzl
6 
7 \*******************************************************************/
8 
11 
12 #ifndef CPROVER_UTIL_SHARING_MAP_H
13 #define CPROVER_UTIL_SHARING_MAP_H
14 
15 #include <string>
16 #include <stack>
17 #include <vector>
18 #include <map>
19 #include <stdexcept>
20 #include <functional>
21 #include <memory>
22 #include <iosfwd>
23 #include <cassert>
24 
25 #include <util/string2int.h>
26 #include <util/threeval.h>
27 #include <util/irep.h>
28 #include <util/sharing_node.h>
29 
30 #define _sm_assert(b) assert(b)
31 //#define _sm_assert(b)
32 
33 #define SHARING_MAPT(R) \
34  template <class keyT, class valueT, class hashT, class predT> \
35  R sharing_mapt<keyT, valueT, hashT, predT>
36 
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>
41 
42 template <
43  class keyT,
44  class valueT,
45  class hashT=std::hash<keyT>,
46  class predT=std::equal_to<keyT>>
48 {
49 public:
50  friend void sharing_map_interface_test();
51  friend void sharing_map_copy_test();
52  friend void sharing_map_collision_test();
53  friend void sharing_map_view_test();
54 
56  {
57  }
58 
59  typedef keyT key_type;
60  typedef valueT mapped_type;
61  typedef std::pair<const key_type, mapped_type> value_type;
62 
63  typedef hashT hash;
64  typedef predT key_equal;
65 
68 
69  typedef size_t size_type;
70 
71  typedef const std::pair<const mapped_type &, const bool> const_find_type;
72  typedef const std::pair<mapped_type &, const bool> find_type;
73 
74  typedef std::vector<key_type> keyst;
75 
76  typedef typename node_type::subt subt;
78 
79  // key-value map
80  node_type map;
81 
82  // number of elements in the map
83  size_type num=0;
84 
85  // dummy element returned when no element was found
86  static mapped_type dummy;
87 
88  // compile-time configuration
89 
90  static const std::string not_found_msg;
91 
92  static const size_t bits;
93  static const size_t chunk;
94 
95  static const size_t mask;
96  static const size_t steps;
97 
98  // interface
99 
100  size_type erase(
101  const key_type &k,
102  const tvt &key_exists=tvt::unknown());
103 
104  size_type erase_all(
105  const keyst &ks,
106  const tvt &key_exists=tvt::unknown()); // applies to all keys
107 
108  // return true if element was inserted
109  const_find_type insert(
110  const key_type &k,
111  const mapped_type &v,
112  const tvt &key_exists=tvt::unknown());
113 
114  const_find_type insert(
115  const value_type &p,
116  const tvt &key_exists=tvt::unknown());
117 
118  find_type place(
119  const key_type &k,
120  const mapped_type &v);
121 
122  find_type place(
123  const value_type &p);
124 
125  find_type find(
126  const key_type &k,
127  const tvt &key_exists=tvt::unknown());
128 
129  const_find_type find(const key_type &k) const;
130 
131  mapped_type &at(
132  const key_type &k,
133  const tvt &key_exists=tvt::unknown());
134 
135  const mapped_type &at(const key_type &k) const;
136 
137  mapped_type &operator[](const key_type &k);
138 
139  void swap(self_type &other)
140  {
141  map.swap(other.map);
142 
143  size_t tmp=num;
144  num=other.num;
145  other.num=tmp;
146  }
147 
148  size_type size() const
149  {
150  return num;
151  }
152 
153  bool empty() const
154  {
155  return num==0;
156  }
157 
158  void clear()
159  {
160  map.clear();
161  num=0;
162  }
163 
164  bool has_key(const key_type &k) const
165  {
166  return get_leaf_node(k)!=nullptr;
167  }
168 
169  // views
170 
171  typedef std::pair<const key_type &, const mapped_type &> view_itemt;
172  typedef std::vector<view_itemt> viewt;
173 
175  {
176  public:
178  const bool in_both,
179  const key_type &k,
180  const mapped_type &m,
181  const mapped_type &other_m) :
182  in_both(in_both),
183  k(k),
184  m(m),
185  other_m(other_m) {}
186 
187  // if true key is in both maps, if false key is only in the map
188  // from which the view was obtained
189  const bool in_both;
190 
191  const key_type &k;
192 
193  const mapped_type &m;
194  const mapped_type &other_m;
195  };
196 
197  typedef std::vector<delta_view_itemt> delta_viewt;
198 
199  void get_view(viewt &view) const;
200 
201  void get_delta_view(
202  const self_type &other,
203  delta_viewt &delta_view,
204  const bool only_common=true) const;
205 
206 protected:
207  // helpers
208 
209  node_type *get_container_node(const key_type &k);
210  const node_type *get_container_node(const key_type &k) const;
211 
212  const node_type *get_leaf_node(const key_type &k) const;
213 
214  void gather_all(const node_type &n, delta_viewt &delta_view) const;
215 };
216 
217 SHARING_MAPT(void)::get_view(viewt &view) const
218 {
219  assert(view.empty());
220 
221  std::stack<const node_type *> stack;
222 
223  if(empty())
224  return;
225 
226  stack.push(&map);
227 
228  do
229  {
230  const node_type *n=stack.top();
231  stack.pop();
232 
233  if(n->is_container())
234  {
235  for(const auto &child : n->get_container())
236  {
237  view.push_back(view_itemt(child.get_key(), child.get_value()));
238  }
239  }
240  else
241  {
242  assert(n->is_internal());
243 
244  for(const auto &child : n->get_sub())
245  {
246  stack.push(&child.second);
247  }
248  }
249  }
250  while(!stack.empty());
251 }
252 
253 SHARING_MAPT(void)::gather_all(const node_type &n, delta_viewt &delta_view)
254  const
255 {
256  std::stack<const node_type *> stack;
257  stack.push(&n);
258 
259  do
260  {
261  const node_type *n=stack.top();
262  stack.pop();
263 
264  if(n->is_container())
265  {
266  for(const auto &child : n->get_container())
267  {
268  delta_view.push_back(
270  false,
271  child.get_key(),
272  child.get_value(),
273  dummy));
274  }
275  }
276  else
277  {
278  assert(n->is_internal());
279 
280  for(const auto &child : n->get_sub())
281  {
282  stack.push(&child.second);
283  }
284  }
285  }
286  while(!stack.empty());
287 }
288 
290  const self_type &other,
291  delta_viewt &delta_view,
292  const bool only_common) const
293 {
294  assert(delta_view.empty());
295 
296  typedef std::pair<const node_type *, const node_type *> stack_itemt;
297  std::stack<stack_itemt> stack;
298 
299  if(empty())
300  return;
301 
302  if(other.empty())
303  {
304  if(!only_common)
305  {
306  gather_all(map, delta_view);
307  }
308  return;
309  }
310 
311  stack.push(stack_itemt(&map, &other.map));
312 
313  do
314  {
315  const stack_itemt si=stack.top();
316  stack.pop();
317 
318  const node_type *n1=si.first;
319  const node_type *n2=si.second;
320 
321  if(n1->is_internal())
322  {
323  _sn_assert(n2->is_internal());
324 
325  for(const auto &child : n1->get_sub())
326  {
327  const node_type *p;
328 
329  p=n2->find_child(child.first);
330  if(p==nullptr)
331  {
332  if(!only_common)
333  {
334  gather_all(child.second, delta_view);
335  }
336  }
337  else if(!child.second.shares_with(*p))
338  {
339  stack.push(stack_itemt(&child.second, p));
340  }
341  }
342  }
343  else if(n1->is_container())
344  {
345  _sn_assert(n2->is_container());
346 
347  for(const auto &l1 : n1->get_container())
348  {
349  const key_type &k1=l1.get_key();
350  bool found=false;
351 
352  for(const auto &l2 : n2->get_container())
353  {
354  const key_type &k2=l2.get_key();
355 
356  if(l1.shares_with(l2))
357  {
358  found=true;
359  break;
360  }
361 
362  if(key_equal()(k1, k2))
363  {
364  delta_view.push_back(
366  true,
367  k1,
368  l1.get_value(),
369  l2.get_value()));
370 
371  found=true;
372  break;
373  }
374  }
375 
376  if(!only_common && !found)
377  {
378  delta_view.push_back(
380  false,
381  l1.get_key(),
382  l1.get_value(),
383  dummy));
384  }
385  }
386  }
387  else
388  {
389  assert(false);
390  }
391  }
392  while(!stack.empty());
393 }
394 
395 SHARING_MAPT2(, node_type *)::get_container_node(const key_type &k)
396 {
397  size_t key=hash()(k);
398  node_type *p=&map;
399 
400  for(unsigned i=0; i<steps; i++)
401  {
402  unsigned bit=key&mask;
403  key>>=chunk;
404 
405  p=p->add_child(bit);
406  }
407 
408  return p;
409 }
410 
411 SHARING_MAPT2(const, node_type *)::get_container_node(const key_type &k) const
412 {
413  size_t key=hash()(k);
414  const node_type *p=&map;
415 
416  for(unsigned i=0; i<steps; i++)
417  {
418  unsigned bit=key&mask;
419  key>>=chunk;
420 
421  p=p->find_child(bit);
422  if(p==nullptr)
423  return nullptr;
424  }
425 
426  assert(p->is_container());
427 
428  return p;
429 }
430 
431 SHARING_MAPT2(const, node_type *)::get_leaf_node(const key_type &k) const
432 {
433  const node_type *p=get_container_node(k);
434  if(p==nullptr)
435  return nullptr;
436 
437  p=p->find_leaf(k);
438 
439  return p;
440 }
441 
442 SHARING_MAPT2(, size_type)::erase(
443  const key_type &k,
444  const tvt &key_exists)
445 {
446  assert(!key_exists.is_false());
447 
448  // check if key exists
449  if(key_exists.is_unknown() && !has_key(k))
450  return 0;
451 
452  node_type *del=nullptr;
453  unsigned del_bit;
454 
455  size_t key=hash()(k);
456  node_type *p=&map;
457 
458  for(unsigned i=0; i<steps; i++)
459  {
460  unsigned bit=key&mask;
461  key>>=chunk;
462 
463  const subt &sub=as_const(p)->get_sub();
464  if(sub.size()>1 || del==nullptr)
465  {
466  del=p;
467  del_bit=bit;
468  }
469 
470  p=p->add_child(bit);
471  }
472 
473  _sm_assert(p->is_container());
474 
475  {
476  const containert &c=as_const(p)->get_container();
477 
478  if(c.size()==1)
479  {
480  del->remove_child(del_bit);
481  num--;
482  return 1;
483  }
484  }
485 
486  containert &c=p->get_container();
487  _sm_assert(c.size()>1);
488  p->remove_leaf(k);
489  num--;
490 
491  return 1;
492 }
493 
494 SHARING_MAPT2(, size_type)::erase_all(
495  const keyst &ks,
496  const tvt &key_exists)
497 {
498  size_type cnt=0;
499 
500  for(const key_type &k : ks)
501  {
502  cnt+=erase(k, key_exists);
503  }
504 
505  return cnt;
506 }
507 
508 SHARING_MAPT2(, const_find_type)::insert(
509  const key_type &k,
510  const mapped_type &m,
511  const tvt &key_exists)
512 {
513  _sn_assert(!key_exists.is_true());
514 
515  if(key_exists.is_unknown())
516  {
517  const node_type *p=as_const(this)->get_leaf_node(k);
518  if(p!=nullptr)
519  return const_find_type(p->get_value(), false);
520  }
521 
522  node_type *p=get_container_node(k);
523  _sn_assert(p!=nullptr);
524 
525  p=p->place_leaf(k, m);
526  num++;
527 
528  return const_find_type(as_const(p)->get_value(), true);
529 }
530 
531 SHARING_MAPT2(, const_find_type)::insert(
532  const value_type &p,
533  const tvt &key_exists)
534 {
535  return insert(p.first, p.second, key_exists);
536 }
537 
538 SHARING_MAPT2(, find_type)::place(
539  const key_type &k,
540  const mapped_type &m)
541 {
542  node_type *c=get_container_node(k);
543  _sm_assert(c!=nullptr);
544 
545  node_type *p=c->find_leaf(k);
546 
547  if(p!=nullptr)
548  return find_type(p->get_value(), false);
549 
550  p=c->place_leaf(k, m);
551  num++;
552 
553  return find_type(p->get_value(), true);
554 }
555 
556 SHARING_MAPT2(, find_type)::place(
557  const value_type &p)
558 {
559  return place(p.first, p.second);
560 }
561 
562 SHARING_MAPT2(, find_type)::find(
563  const key_type &k,
564  const tvt &key_exists)
565 {
566  _sm_assert(!key_exists.is_false());
567 
568  if(key_exists.is_unknown() && !has_key(k))
569  return find_type(dummy, false);
570 
571  node_type *p=get_container_node(k);
572  _sm_assert(p!=nullptr);
573 
574  p=p->find_leaf(k);
575  _sm_assert(p!=nullptr);
576 
577  return find_type(p->get_value(), true);
578 
579 }
580 
581 SHARING_MAPT2(, const_find_type)::find(const key_type &k) const
582 {
583  const node_type *p=get_leaf_node(k);
584 
585  if(p==nullptr)
586  return const_find_type(dummy, false);
587 
588  return const_find_type(p->get_value(), true);
589 }
590 
591 SHARING_MAPT2(, mapped_type &)::at(
592  const key_type &k,
593  const tvt &key_exists)
594 {
595  find_type r=find(k, key_exists);
596 
597  if(!r.second)
598  throw std::out_of_range(not_found_msg);
599 
600  return r.first;
601 }
602 
603 SHARING_MAPT2(const, mapped_type &)::at(const key_type &k) const
604 {
605  const_find_type r=find(k);
606  if(!r.second)
607  throw std::out_of_range(not_found_msg);
608 
609  return r.first;
610 }
611 
612 SHARING_MAPT2(, mapped_type &)::operator[](const key_type &k)
613 {
614  return place(k, mapped_type()).first;
615 }
616 
617 // static constants
618 
619 SHARING_MAPT(const std::string)::not_found_msg="key not found";
620 
621 // config
622 SHARING_MAPT(const size_t)::bits=18;
623 SHARING_MAPT(const size_t)::chunk=3;
624 
625 // derived config
626 SHARING_MAPT(const size_t)::mask=0xffff>>(16-chunk);
627 SHARING_MAPT(const size_t)::steps=bits/chunk;
628 
629 SHARING_MAPT2(, mapped_type)::dummy;
630 
631 #endif
const T * as_const(T *t)
Definition: sharing_node.h:24
size_type num
Definition: sharing_map.h:83
static const size_t chunk
Definition: sharing_map.h:93
bool empty() const
Definition: sharing_map.h:153
static int8_t r
Definition: irep_hash.h:59
void swap(self_type &other)
Definition: sharing_map.h:139
void remove_child(const unsigned n)
Definition: sharing_node.h:174
std::pair< const key_type &, const mapped_type & > view_itemt
Definition: sharing_map.h:171
friend void sharing_map_collision_test()
std::vector< delta_view_itemt > delta_viewt
Definition: sharing_map.h:197
sharing_nodet< key_type, mapped_type, key_equal > node_type
Definition: sharing_map.h:67
void remove_leaf(const key_type &k)
Definition: sharing_node.h:222
std::vector< key_type > keyst
Definition: sharing_map.h:74
friend void sharing_map_interface_test()
node_type::subt subt
Definition: sharing_map.h:76
size_type size() const
Definition: sharing_map.h:148
size_type erase(const key_type &k, const tvt &key_exists=tvt::unknown())
Definition: sharing_map.h:442
static tvt unknown()
Definition: threeval.h:33
const_find_type insert(const key_type &k, const mapped_type &v, const tvt &key_exists=tvt::unknown())
Definition: sharing_map.h:508
static const std::string not_found_msg
Definition: sharing_map.h:90
static const size_t steps
Definition: sharing_map.h:96
#define SHARING_MAPT(R)
Definition: sharing_map.h:33
self_type * place_leaf(const key_type &k, const mapped_type &m)
Definition: sharing_node.h:211
void get_delta_view(const self_type &other, delta_viewt &delta_view, const bool only_common=true) const
Definition: sharing_map.h:289
node_type * get_container_node(const key_type &k)
Definition: sharing_map.h:395
#define _sm_assert(b)
Definition: sharing_map.h:30
const mapped_type & other_m
Definition: sharing_map.h:194
predT key_equal
Definition: sharing_map.h:64
const self_type * find_leaf(const key_type &k) const
Definition: sharing_node.h:184
const std::pair< mapped_type &, const bool > find_type
Definition: sharing_map.h:72
#define _sn_assert(b)
Definition: sharing_node.h:20
node_type map
Definition: sharing_map.h:80
const mapped_type & get_value() const
Definition: sharing_node.h:123
containert & get_container()
Definition: sharing_node.h:145
void clear()
Definition: sharing_map.h:158
mapped_type & operator[](const key_type &k)
Definition: sharing_map.h:612
bool has_key(const key_type &k) const
Definition: sharing_map.h:164
friend void sharing_map_view_test()
Definition: threeval.h:19
find_type place(const key_type &k, const mapped_type &v)
Definition: sharing_map.h:538
static const size_t mask
Definition: sharing_map.h:95
node_type::containert containert
Definition: sharing_map.h:77
static const size_t bits
Definition: sharing_map.h:92
bool is_container() const
Definition: sharing_node.h:101
mapped_type & at(const key_type &k, const tvt &key_exists=tvt::unknown())
Definition: sharing_map.h:591
static mapped_type dummy
Definition: sharing_map.h:86
const node_type * get_leaf_node(const key_type &k) const
Definition: sharing_map.h:431
delta_view_itemt(const bool in_both, const key_type &k, const mapped_type &m, const mapped_type &other_m)
Definition: sharing_map.h:177
const std::pair< const mapped_type &, const bool > const_find_type
Definition: sharing_map.h:71
find_type find(const key_type &k, const tvt &key_exists=tvt::unknown())
Definition: sharing_map.h:562
bool is_internal() const
Definition: sharing_node.h:94
#define SHARING_MAPT2(CV, ST)
Definition: sharing_map.h:37
void get_view(viewt &view) const
Definition: sharing_map.h:217
std::pair< const key_type, mapped_type > value_type
Definition: sharing_map.h:61
size_type erase_all(const keyst &ks, const tvt &key_exists=tvt::unknown())
Definition: sharing_map.h:494
sharing_mapt< key_type, mapped_type, hash, key_equal > self_type
Definition: sharing_map.h:66
self_type * add_child(const unsigned n)
Definition: sharing_node.h:168
subt & get_sub()
Definition: sharing_node.h:135
void gather_all(const node_type &n, delta_viewt &delta_view) const
Definition: sharing_map.h:253
Sharing node.
std::vector< view_itemt > viewt
Definition: sharing_map.h:172
size_t size_type
Definition: sharing_map.h:69
void swap(self_type &other)
Definition: sharing_node.h:253
const self_type * find_child(const unsigned n) const
Definition: sharing_node.h:157
std::map< unsigned, self_type > subt
Definition: sharing_node.h:46
#define stack(x)
Definition: parser.h:144
valueT mapped_type
Definition: sharing_map.h:60
friend void sharing_map_copy_test()