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 #include <list>
16 #include <map>
17 #include <memory>
18 #include <cassert>
19 
20 #define _sn_assert(b) assert(b)
21 //#define _sn_assert(b)
22 
23 template <class T>
24 const T *as_const(T *t)
25 {
26  return t;
27 }
28 
29 template <
30  class keyT,
31  class valueT,
32  class predT=std::equal_to<keyT>,
33  bool no_sharing=false>
35 {
36 public:
37  friend void sharing_node_test();
38 
39  typedef keyT key_type;
40  typedef valueT mapped_type;
41 
42  typedef predT key_equal;
43 
45 
46  typedef std::map<unsigned, self_type> subt;
47  typedef std::list<self_type> containert;
48 
49  typedef const std::pair<const self_type &, const bool> const_find_type;
50  typedef const std::pair<self_type &, const bool> find_type;
51 
53  {
54  _sn_assert(data.use_count()>=2);
55  }
56 
58  {
59  _sn_assert(data.use_count()>=2);
60 
61  dt &d=write();
62 
63  _sn_assert(d.k==nullptr);
64  d.k=std::make_shared<key_type>(k);
65 
66  _sn_assert(d.m==nullptr);
67  d.m.reset(new mapped_type(m));
68  }
69 
70  sharing_nodet(const self_type &other)
71  {
72 #ifdef SM_NO_SHARING
73  data=std::make_shared<dt>(*other.data);
74 #else
75  if(no_sharing)
76  {
77  data=std::make_shared<dt>(*other.data);
78  }
79  else
80  {
81  data=other.data;
82  }
83 #endif
84  }
85 
86  // check type of node
87 
88  bool is_empty() const
89  {
91  return data==empty_data;
92  }
93 
94  bool is_internal() const
95  {
97  _sn_assert(!is_empty());
98  return !get_sub().empty();
99  }
100 
101  bool is_container() const
102  {
104  _sn_assert(!is_empty());
105  return !get_container().empty();
106  }
107 
108  bool is_leaf() const
109  {
111  _sn_assert(!is_empty());
112  return read().is_leaf();
113  }
114 
115  // accessors
116 
117  const key_type &get_key() const
118  {
119  _sn_assert(is_leaf());
120  return *read().k;
121  }
122 
123  const mapped_type &get_value() const
124  {
125  _sn_assert(is_leaf());
126  return *read().m;
127  }
128 
130  {
131  _sn_assert(is_leaf());
132  return *write().m;
133  }
134 
136  {
137  return write().sub;
138  }
139 
140  const subt &get_sub() const
141  {
142  return read().sub;
143  }
144 
146  {
147  return write().con;
148  }
149 
150  const containert &get_container() const
151  {
152  return read().con;
153  }
154 
155  // internal nodes
156 
157  const self_type *find_child(const unsigned n) const
158  {
159  const subt &s=get_sub();
160  typename subt::const_iterator it=s.find(n);
161 
162  if(it!=s.end())
163  return &it->second;
164 
165  return nullptr;
166  }
167 
168  self_type *add_child(const unsigned n)
169  {
170  subt &s=get_sub();
171  return &s[n];
172  }
173 
174  void remove_child(const unsigned n)
175  {
176  subt &s=get_sub();
177  size_t r=s.erase(n);
178 
179  _sn_assert(r==1);
180  }
181 
182  // container nodes
183 
184  const self_type *find_leaf(const key_type &k) const
185  {
186  const containert &c=get_container();
187 
188  for(const auto &n : c)
189  {
190  if(key_equal()(n.get_key(), k))
191  return &n;
192  }
193 
194  return nullptr;
195  }
196 
198  {
200 
201  for(auto &n : c)
202  {
203  if(key_equal()(n.get_key(), k))
204  return &n;
205  }
206 
207  return nullptr;
208  }
209 
210  // add leaf, key must not exist yet
212  {
213  _sn_assert(as_const(this)->find_leaf(k)==nullptr);
214 
216  c.push_back(self_type(k, m));
217 
218  return &c.back();
219  }
220 
221  // remove leaf, key must exist
222  void remove_leaf(const key_type &k)
223  {
225 
226  for(typename containert::const_iterator it=c.begin();
227  it!=c.end(); it++)
228  {
229  const self_type &n=*it;
230 
231  if(key_equal()(n.get_key(), k))
232  {
233  c.erase(it);
234  return;
235  }
236  }
237 
238  assert(false);
239  }
240 
241  // misc
242 
243  void clear()
244  {
245  *this=self_type();
246  }
247 
248  bool shares_with(const self_type &other) const
249  {
250  return data==other.data;
251  }
252 
253  void swap(self_type &other)
254  {
255  data.swap(other.data);
256  }
257 
258 protected:
259  class dt
260  {
261  public:
262  dt() {}
263 
264  dt(const dt &d) : k(d.k), sub(d.sub), con(d.con)
265  {
266  if(d.is_leaf())
267  {
268  _sn_assert(m==nullptr);
269  m.reset(new mapped_type(*d.m));
270  }
271  }
272 
273  bool is_leaf() const
274  {
275  _sn_assert(k==nullptr || m!=nullptr);
276  return k!=nullptr;
277  }
278 
279  std::shared_ptr<key_type> k;
280  std::unique_ptr<mapped_type> m;
281 
284  };
285 
286  const dt &read() const
287  {
288  return *data;
289  }
290 
291  dt &write()
292  {
293  detach();
294  return *data;
295  }
296 
297  void detach()
298  {
299  _sn_assert(data.use_count()>0);
300 
301  if(data==empty_data)
302  data=std::make_shared<dt>();
303  else if(data.use_count()>1)
304  data=std::make_shared<dt>(*data);
305 
306  _sn_assert(data.use_count()==1);
307  }
308 
309  bool is_well_formed() const
310  {
311  if(data==nullptr)
312  return false;
313 
314  const dt &d=*data;
315 
316  bool b;
317 
318  // empty node
319  b=data==empty_data;
320  // internal node
321  b|=d.k==nullptr && d.m==nullptr && get_container().empty() &&
322  !get_sub().empty();
323  // container node
324  b|=d.k==nullptr && d.m==nullptr && !get_container().empty() &&
325  get_sub().empty();
326  // leaf node
327  b|=d.k!=nullptr && d.m!=nullptr && get_container().empty() &&
328  get_sub().empty();
329 
330  return b;
331  }
332 
333  std::shared_ptr<dt> data;
334  static std::shared_ptr<dt> empty_data;
335 
336  // dummy node returned when node was not found
338 };
339 
340 template <class keyT, class valueT, class predT, bool no_sharing>
341 std::shared_ptr<typename sharing_nodet<keyT, valueT, predT, no_sharing>::dt>
344 
345 template <class keyT, class valueT, class predT, bool no_sharing>
348 
349 #endif
const T * as_const(T *t)
Definition: sharing_node.h:24
static std::shared_ptr< dt > empty_data
Definition: sharing_node.h:334
static int8_t r
Definition: irep_hash.h:59
void remove_child(const unsigned n)
Definition: sharing_node.h:174
bool shares_with(const self_type &other) const
Definition: sharing_node.h:248
void remove_leaf(const key_type &k)
Definition: sharing_node.h:222
bool is_well_formed() const
Definition: sharing_node.h:309
const std::pair< const self_type &, const bool > const_find_type
Definition: sharing_node.h:49
self_type * place_leaf(const key_type &k, const mapped_type &m)
Definition: sharing_node.h:211
const self_type * find_leaf(const key_type &k) const
Definition: sharing_node.h:184
#define _sn_assert(b)
Definition: sharing_node.h:20
const mapped_type & get_value() const
Definition: sharing_node.h:123
containert & get_container()
Definition: sharing_node.h:145
const containert & get_container() const
Definition: sharing_node.h:150
std::shared_ptr< key_type > k
Definition: sharing_node.h:279
sharing_nodet(const key_type &k, const mapped_type &m)
Definition: sharing_node.h:57
static sharing_nodet dummy
Definition: sharing_node.h:337
dt(const dt &d)
Definition: sharing_node.h:264
const dt & read() const
Definition: sharing_node.h:286
bool is_container() const
Definition: sharing_node.h:101
mapped_type & get_value()
Definition: sharing_node.h:129
valueT mapped_type
Definition: sharing_node.h:40
const key_type & get_key() const
Definition: sharing_node.h:117
bool is_internal() const
Definition: sharing_node.h:94
self_type * find_leaf(const key_type &k)
Definition: sharing_node.h:197
bool is_empty() const
Definition: sharing_node.h:88
bool is_leaf() const
Definition: sharing_node.h:273
bool is_leaf() const
Definition: sharing_node.h:108
sharing_nodet< key_type, mapped_type, key_equal > self_type
Definition: sharing_node.h:44
sharing_nodet(const self_type &other)
Definition: sharing_node.h:70
const subt & get_sub() const
Definition: sharing_node.h:140
self_type * add_child(const unsigned n)
Definition: sharing_node.h:168
friend void sharing_node_test()
subt & get_sub()
Definition: sharing_node.h:135
const std::pair< self_type &, const bool > find_type
Definition: sharing_node.h:50
void swap(self_type &other)
Definition: sharing_node.h:253
std::shared_ptr< dt > data
Definition: sharing_node.h:333
std::unique_ptr< mapped_type > m
Definition: sharing_node.h:280
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
Definition: kdev_t.h:24
std::list< self_type > containert
Definition: sharing_node.h:47