cprover
sharing_node.h
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module: Sharing node
4 
5 Author: Daniel Poetzl
6 
7 \*******************************************************************/
8 
11 
12 #ifndef CPROVER_UTIL_SHARING_NODE_H
13 #define CPROVER_UTIL_SHARING_NODE_H
14 
15 #ifdef SN_DEBUG
16 #include <iostream>
17 #endif
18 
19 #include <forward_list>
20 #include <type_traits>
21 
22 #ifndef SN_SMALL_MAP
23 #define SN_SMALL_MAP 1
24 #endif
25 
26 #ifndef SN_SHARE_KEYS
27 #define SN_SHARE_KEYS 0
28 #endif
29 
30 #if SN_SMALL_MAP == 1
31 #include "small_map.h"
32 #else
33 #include <map>
34 #endif
35 
36 #include "as_const.h"
37 #include "invariant.h"
38 #include "make_unique.h"
39 #include "small_shared_n_way_ptr.h"
40 #include "small_shared_ptr.h"
41 
42 #ifdef SN_INTERNAL_CHECKS
43 #define SN_ASSERT(b) INVARIANT(b, "Sharing node internal invariant")
44 #define SN_ASSERT_USE(v, b) SN_ASSERT(b)
45 #else
46 #define SN_ASSERT(b)
47 #define SN_ASSERT_USE(v, b) static_cast<void>(v);
48 #endif
49 
50 // clang-format off
51 #define SN_TYPE_PAR_DECL \
52  template <typename keyT, \
53  typename valueT, \
54  typename equalT = std::equal_to<keyT>>
55 
56 #define SN_TYPE_PAR_DEF \
57  template <typename keyT, typename valueT, typename equalT>
58 
59 #define SN_TYPE_ARGS keyT, valueT, equalT
60 
61 #define SN_PTR_TYPE_ARGS \
62  d_containert<SN_TYPE_ARGS>, d_leaft<SN_TYPE_ARGS>, d_internalt<SN_TYPE_ARGS>
63 // clang-format on
64 
66 
68 
70 {
71 public:
73 #if SN_SMALL_MAP == 1
75 #else
76  typedef std::map<std::size_t, innert> to_mapt;
77 #endif
78 
80 };
81 
83 {
84 public:
86  typedef std::forward_list<leaft> leaf_listt;
87 
89 };
90 
92 {
93 public:
94 #if SN_SHARE_KEYS == 1
95  typedef std::shared_ptr<keyT> keyt;
96 #else
97  typedef keyT keyt;
98 #endif
99 
100  template <class valueU>
101  d_leaft(const keyt &k, valueU &&v) : k(k), v(std::forward<valueU>(v))
102  {
103  }
105 
106  valueT v;
107 };
108 
110 {
111 public:
113  typedef typename datat::use_countt use_countt;
114 
118 
119  typedef typename d_it::to_mapt to_mapt;
120 
121  typedef typename d_ct::leaft leaft;
122  typedef typename d_ct::leaf_listt leaf_listt;
123 
125  {
126  }
127 
128  template <class valueU>
129  sharing_nodet(const keyT &k, valueU &&v)
130  {
131  SN_ASSERT(!data);
132 
133 #if SN_SHARE_KEYS == 1
134  SN_ASSERT(d.k == nullptr);
135  data = make_shared_3<1, SN_PTR_TYPE_ARGS>(
136  std::make_shared<keyT>(k), std::forward<valueU>(v));
137 #else
138  data = make_shared_3<1, SN_PTR_TYPE_ARGS>(k, std::forward<valueU>(v));
139 #endif
140  }
141 
142  bool empty() const
143  {
144  return !data;
145  }
146 
147  void clear()
148  {
149  // only the root node may be cleared which is an internal node
151 
152  data.reset();
153  }
154 
155  bool shares_with(const sharing_nodet &other) const
156  {
157  SN_ASSERT(data);
158  SN_ASSERT(other.data);
159 
160  return data == other.data;
161  }
162 
164  {
165  return data.use_count();
166  }
167 
168  void swap(sharing_nodet &other)
169  {
170  data.swap(other.data);
171  }
172 
173  // Types
174 
175  bool is_internal() const
176  {
177  return data.template is_derived<2>();
178  }
179 
180  bool is_container() const
181  {
182  return data.template is_derived<0>();
183  }
184 
185  bool is_leaf() const
186  {
187  return data.template is_derived<1>();
188  }
189 
190  bool is_defined_internal() const
191  {
192  return !empty() && is_internal();
193  }
194 
195  bool is_defined_container() const
196  {
197  return !empty() && is_container();
198  }
199 
200  bool is_defined_leaf() const
201  {
202  return !empty() && is_leaf();
203  }
204 
205  const d_it &read_internal() const
206  {
207  SN_ASSERT(!empty());
208 
209  return *data.template get_derived<2>();
210  }
211 
212  const d_ct &read_container() const
213  {
214  SN_ASSERT(!empty());
215 
216  return *data.template get_derived<0>();
217  }
218 
219  const d_lt &read_leaf() const
220  {
221  SN_ASSERT(!empty());
222 
223  return *data.template get_derived<1>();
224  }
225 
226  // Accessors
227 
228  const to_mapt &get_to_map() const
229  {
230  return read_internal().m;
231  }
232 
234  {
235  return write_internal().m;
236  }
237 
238  const leaf_listt &get_container() const
239  {
240  return read_container().con;
241  }
242 
244  {
245  return write_container().con;
246  }
247 
248  // Containers
249 
250  const leaft *find_leaf(const keyT &k) const
251  {
253 
254  const leaf_listt &c = get_container();
255 
256  for(const auto &n : c)
257  {
258  SN_ASSERT(n.is_leaf());
259 
260  if(equalT()(n.get_key(), k))
261  return &n;
262  }
263 
264  return nullptr;
265  }
266 
267  leaft *find_leaf(const keyT &k)
268  {
270 
271  leaf_listt &c = get_container();
272 
273  for(auto &n : c)
274  {
275  SN_ASSERT(n.is_leaf());
276 
277  if(equalT()(n.get_key(), k))
278  return &n;
279  }
280 
281  UNREACHABLE;
282  return nullptr;
283  }
284 
285  // add leaf, key must not exist yet
286  template <class valueU>
287  void place_leaf(const keyT &k, valueU &&v)
288  {
289  SN_ASSERT(is_container()); // empty() is allowed
290 
291  // we need to check empty() first as the const version of find_leaf() must
292  // not be called on an empty node
293  PRECONDITION(empty() || as_const_ptr(this)->find_leaf(k) == nullptr);
294 
295  leaf_listt &c = get_container();
296  c.emplace_front(k, std::forward<valueU>(v));
297  SN_ASSERT(c.front().is_defined_leaf());
298  }
299 
300  // remove leaf, key must exist
301  void remove_leaf(const keyT &k)
302  {
304 
305  leaf_listt &c = get_container();
306 
307  SN_ASSERT(!c.empty());
308 
309  const leaft &first = c.front();
310 
311  if(equalT()(first.get_key(), k))
312  {
313  c.pop_front();
314  return;
315  }
316 
317  typename leaf_listt::const_iterator last_it = c.begin();
318 
319  typename leaf_listt::const_iterator it = c.begin();
320  it++;
321 
322  for(; it != c.end(); it++)
323  {
324  const leaft &leaf = *it;
325 
326  SN_ASSERT(leaf.is_defined_leaf());
327 
328  if(equalT()(leaf.get_key(), k))
329  {
330  c.erase_after(last_it);
331  return;
332  }
333 
334  last_it = it;
335  }
336 
337  UNREACHABLE;
338  }
339 
340  // Inner nodes
341 
342  const typename d_it::innert *find_child(const std::size_t n) const
343  {
345 
346  const to_mapt &m = get_to_map();
347  typename to_mapt::const_iterator it = m.find(n);
348 
349  if(it != m.end())
350  return &it->second;
351 
352  return nullptr;
353  }
354 
355  typename d_it::innert &add_child(const std::size_t n)
356  {
357  SN_ASSERT(is_internal()); // empty() is allowed
358 
359  to_mapt &m = get_to_map();
360  return m[n];
361  }
362 
363  void remove_child(const std::size_t n)
364  {
366 
367  to_mapt &m = get_to_map();
368  std::size_t r = m.erase(n);
369 
370  SN_ASSERT_USE(r, r == 1);
371  }
372 
373  // Leafs
374 
375  const keyT &get_key() const
376  {
378 
379 #if SN_SHARE_KEYS == 1
380  return *read_leaf().k;
381 #else
382  return read_leaf().k;
383 #endif
384  }
385 
386  const valueT &get_value() const
387  {
389 
390  return read_leaf().v;
391  }
392 
393  template <class valueU>
394  void make_leaf(const keyT &k, valueU &&v)
395  {
396  SN_ASSERT(!data);
397 
398  data = make_shared_3<1, SN_PTR_TYPE_ARGS>(k, std::forward<valueU>(v));
399  }
400 
401  template <class valueU>
402  void set_value(valueU &&v)
403  {
405 
406  if(data.use_count() > 1)
407  {
408  data =
409  make_shared_3<1, SN_PTR_TYPE_ARGS>(get_key(), std::forward<valueU>(v));
410  }
411  else
412  {
413  data.template get_derived<1>()->v = std::forward<valueU>(v);
414  }
415 
416  SN_ASSERT(data.use_count() == 1);
417  }
418 
419  void mutate_value(std::function<void(valueT &)> mutator)
420  {
422 
423  if(data.use_count() > 1)
424  {
425  data = make_shared_3<1, SN_PTR_TYPE_ARGS>(read_leaf());
426  }
427 
428  mutator(data.template get_derived<1>()->v);
429 
430  SN_ASSERT(data.use_count() == 1);
431  }
432 
433 protected:
435  {
437 
438  if(!data)
439  {
440  data = make_shared_3<2, SN_PTR_TYPE_ARGS>();
441  }
442  else if(data.use_count() > 1)
443  {
444  data = make_shared_3<2, SN_PTR_TYPE_ARGS>(read_internal());
445  }
446 
447  SN_ASSERT(data.use_count() == 1);
448 
449  return *data.template get_derived<2>();
450  }
451 
453  {
455 
456  if(!data)
457  {
458  data = make_shared_3<0, SN_PTR_TYPE_ARGS>();
459  }
460  else if(data.use_count() > 1)
461  {
462  data = make_shared_3<0, SN_PTR_TYPE_ARGS>(read_container());
463  }
464 
465  SN_ASSERT(data.use_count() == 1);
466 
467  return *data.template get_derived<0>();
468  }
469 
471 };
472 
473 #endif
sharing_nodet::read_internal
const d_it & read_internal() const
Definition: sharing_node.h:205
UNREACHABLE
#define UNREACHABLE
This should be used to mark dead code.
Definition: invariant.h:504
SN_TYPE_PAR_DEF
#define SN_TYPE_PAR_DEF
Definition: sharing_node.h:56
sharing_nodet::is_defined_leaf
bool is_defined_leaf() const
Definition: sharing_node.h:200
sharing_nodet::leaf_listt
d_ct::leaf_listt leaf_listt
Definition: sharing_node.h:122
sharing_nodet::get_key
const keyT & get_key() const
Definition: sharing_node.h:375
d_leaft
Definition: sharing_node.h:92
sharing_nodet::is_leaf
bool is_leaf() const
Definition: sharing_node.h:185
sharing_nodet::sharing_nodet
sharing_nodet()
Definition: sharing_node.h:124
sharing_nodet::read_container
const d_ct & read_container() const
Definition: sharing_node.h:212
sharing_nodet::d_ct
d_containert< keyT, valueT, equalT > d_ct
Definition: sharing_node.h:116
data
Definition: kdev_t.h:24
sharing_nodet::use_count
use_countt use_count() const
Definition: sharing_node.h:163
small_mapt::end
const_iterator end() const
Definition: small_map.h:323
sharing_nodet::read_leaf
const d_lt & read_leaf() const
Definition: sharing_node.h:219
small_mapt::erase
std::size_t erase(std::size_t idx)
Definition: small_map.h:428
d_leaft::v
valueT v
Definition: sharing_node.h:106
small_map.h
Small map.
sharing_nodet::is_internal
bool is_internal() const
Definition: sharing_node.h:175
SN_ASSERT_USE
#define SN_ASSERT_USE(v, b)
Definition: sharing_node.h:47
sharing_nodet::is_defined_container
bool is_defined_container() const
Definition: sharing_node.h:195
sharing_nodet::is_defined_internal
bool is_defined_internal() const
Definition: sharing_node.h:190
sharing_nodet::get_container
const leaf_listt & get_container() const
Definition: sharing_node.h:238
sharing_nodet::remove_leaf
void remove_leaf(const keyT &k)
Definition: sharing_node.h:301
d_containert::leaft
sharing_nodet< keyT, valueT, equalT > leaft
Definition: sharing_node.h:85
d_containert::con
leaf_listt con
Definition: sharing_node.h:88
sharing_nodet::use_countt
datat::use_countt use_countt
Definition: sharing_node.h:113
sharing_nodet::get_value
const valueT & get_value() const
Definition: sharing_node.h:386
sharing_nodet::datat
small_shared_n_way_ptrt< d_containert< keyT, valueT, equalT >, d_leaft< keyT, valueT, equalT >, d_internalt< keyT, valueT, equalT > > datat
Definition: sharing_node.h:112
d_internalt
Definition: sharing_node.h:70
small_shared_n_way_ptr.h
small_shared_ptr.h
sharing_nodet::data
datat data
Definition: sharing_node.h:470
d_internalt::to_mapt
small_mapt< innert > to_mapt
Definition: sharing_node.h:74
d_leaft::keyt
keyT keyt
Definition: sharing_node.h:97
sharing_nodet::get_to_map
const to_mapt & get_to_map() const
Definition: sharing_node.h:228
make_unique.h
small_shared_n_way_ptrt
This class is similar to small_shared_ptrt and boost's intrusive_ptr.
Definition: small_shared_n_way_ptr.h:91
PRECONDITION
#define PRECONDITION(CONDITION)
Definition: invariant.h:464
sharing_nodet::write_internal
d_it & write_internal()
Definition: sharing_node.h:434
sharing_nodet::place_leaf
void place_leaf(const keyT &k, valueU &&v)
Definition: sharing_node.h:287
sharing_nodet::swap
void swap(sharing_nodet &other)
Definition: sharing_node.h:168
sharing_nodet::d_lt
d_leaft< keyT, valueT, equalT > d_lt
Definition: sharing_node.h:117
d_internalt::innert
sharing_nodet< keyT, valueT, equalT > innert
Definition: sharing_node.h:72
d_leaft::d_leaft
d_leaft(const keyt &k, valueU &&v)
Definition: sharing_node.h:101
small_mapt< innert >
sharing_nodet::shares_with
bool shares_with(const sharing_nodet &other) const
Definition: sharing_node.h:155
sharing_nodet::to_mapt
d_it::to_mapt to_mapt
Definition: sharing_node.h:119
sharing_nodet::remove_child
void remove_child(const std::size_t n)
Definition: sharing_node.h:363
sharing_nodet::find_leaf
const leaft * find_leaf(const keyT &k) const
Definition: sharing_node.h:250
sharing_nodet::find_child
const d_it::innert * find_child(const std::size_t n) const
Definition: sharing_node.h:342
SN_ASSERT
#define SN_ASSERT(b)
Definition: sharing_node.h:46
d_containert::leaf_listt
std::forward_list< leaft > leaf_listt
Definition: sharing_node.h:86
sharing_nodet::write_container
d_ct & write_container()
Definition: sharing_node.h:452
sharing_nodet
Definition: sharing_node.h:110
sharing_nodet::get_to_map
to_mapt & get_to_map()
Definition: sharing_node.h:233
small_shared_n_way_ptrt< d_containert< keyT, valueT, equalT >, d_leaft< keyT, valueT, equalT >, d_internalt< keyT, valueT, equalT > >::use_countt
decltype(std::declval< typename get_typet< 0, Ts... >::type >() .get_use_count()) typedef use_countt
Definition: small_shared_n_way_ptr.h:98
sharing_nodet::leaft
d_ct::leaft leaft
Definition: sharing_node.h:121
invariant.h
sharing_nodet::add_child
d_it::innert & add_child(const std::size_t n)
Definition: sharing_node.h:355
sharing_nodet::is_container
bool is_container() const
Definition: sharing_node.h:180
d_containert
Definition: sharing_node.h:83
sharing_nodet::find_leaf
leaft * find_leaf(const keyT &k)
Definition: sharing_node.h:267
small_shared_n_way_pointee_baset
Definition: small_shared_n_way_ptr.h:316
sharing_nodet::d_it
d_internalt< keyT, valueT, equalT > d_it
Definition: sharing_node.h:115
sharing_nodet::sharing_nodet
sharing_nodet(const keyT &k, valueU &&v)
Definition: sharing_node.h:129
r
static int8_t r
Definition: irep_hash.h:59
sharing_nodet::set_value
void set_value(valueU &&v)
Definition: sharing_node.h:402
sharing_nodet::mutate_value
void mutate_value(std::function< void(valueT &)> mutator)
Definition: sharing_node.h:419
d_baset
small_shared_n_way_pointee_baset< 3, unsigned > d_baset
Definition: sharing_node.h:65
sharing_nodet::get_container
leaf_listt & get_container()
Definition: sharing_node.h:243
d_leaft::k
keyt k
Definition: sharing_node.h:104
sharing_nodet::empty
bool empty() const
Definition: sharing_node.h:142
sharing_nodet::make_leaf
void make_leaf(const keyT &k, valueU &&v)
Definition: sharing_node.h:394
SN_TYPE_PAR_DECL
#define SN_TYPE_PAR_DECL
Definition: sharing_node.h:51
as_const.h
small_mapt::find
const_iterator find(std::size_t idx) const
Definition: small_map.h:414
sharing_nodet::clear
void clear()
Definition: sharing_node.h:147
as_const_ptr
const T * as_const_ptr(T *t)
Return a pointer to the same object but ensures the type is pointer to const.
Definition: as_const.h:21
d_internalt::m
to_mapt m
Definition: sharing_node.h:79