Go to the documentation of this file.
12 #ifndef CPROVER_UTIL_SHARING_NODE_H
13 #define CPROVER_UTIL_SHARING_NODE_H
19 #include <forward_list>
20 #include <type_traits>
23 #define SN_SMALL_MAP 1
27 #define SN_SHARE_KEYS 0
41 #ifdef SN_INTERNAL_CHECKS
42 #define SN_ASSERT(b) INVARIANT(b, "Sharing node internal invariant")
43 #define SN_ASSERT_USE(v, b) SN_ASSERT(b)
46 #define SN_ASSERT_USE(v, b) static_cast<void>(v);
50 #define SN_TYPE_PAR_DECL \
51 template <typename keyT, \
53 typename equalT = std::equal_to<keyT>>
55 #define SN_TYPE_PAR_DEF \
56 template <typename keyT, typename valueT, typename equalT>
59 #define SN_TYPE_ARGS keyT, valueT, equalT
61 #define SN_PTR_TYPE_ARGS d_internalt<SN_TYPE_ARGS>, d_containert<SN_TYPE_ARGS>
63 #define SN_PTR_TYPE_ARG d_leaft<SN_TYPE_ARGS>
84 typedef std::map<std::size_t, innert>
to_mapt;
146 return data.is_derived_u();
151 return data.is_derived_v();
158 data = make_shared_derived_u<SN_PTR_TYPE_ARGS>();
160 else if(
data.use_count() > 1)
162 data = make_shared_derived_u<SN_PTR_TYPE_ARGS>(*
data.get_derived_u());
167 return *
data.get_derived_u();
174 return *
data.get_derived_u();
181 data = make_shared_derived_v<SN_PTR_TYPE_ARGS>();
183 else if(
data.use_count() > 1)
185 data = make_shared_derived_v<SN_PTR_TYPE_ARGS>(*
data.get_derived_v());
190 return *
data.get_derived_v();
197 return *
data.get_derived_v();
230 for(
const auto &n : c)
232 if(equalT()(n.get_key(), k))
247 if(equalT()(n.get_key(), k))
265 c.push_front(
leaft(k, v));
279 const leaft &first = c.front();
281 if(equalT()(first.
get_key(), k))
287 typename leaf_listt::const_iterator last_it = c.begin();
289 typename leaf_listt::const_iterator it = c.begin();
292 for(; it != c.end(); it++)
294 const leaft &leaf = *it;
296 if(equalT()(leaf.
get_key(), k))
298 c.erase_after(last_it);
315 typename to_mapt::const_iterator it = m.
find(n);
336 std::size_t
r = m.
erase(n);
354 #if SN_SHARE_KEYS == 1
355 std::shared_ptr<keyT>
k;
374 #if SN_SHARE_KEYS == 1
376 d.k = std::make_shared<keyT>(k);
411 data = make_small_shared_ptr<d_lt>();
413 else if(
data.use_count() > 1)
415 data = make_small_shared_ptr<d_lt>(*
data);
434 #if SN_SHARE_KEYS == 1
461 make_small_shared_ptr<SN_PTR_TYPE_ARG>();
sharing_node_leaft< keyT, valueT, equalT > leaft
const d_it & read_internal() const
leaft * find_leaf(const keyT &k)
bool shares_with(const sharing_node_innert &other) const
leaft * place_leaf(const keyT &k, const valueT &v)
const_iterator end() const
std::size_t erase(std::size_t idx)
bool is_container() const
This class is similar to small_shared_ptrt and boost's intrusive_ptr.
void remove_child(const std::size_t n)
const valueT & get_value() const
small_shared_two_way_pointeet< unsigned > d_baset
A helper class to store use-counts of objects held by small shared pointers.
#define SN_ASSERT_USE(v, b)
void remove_leaf(const keyT &k)
const to_mapt & get_to_map() const
bool shares_with(const sharing_node_leaft &other) const
#define UNREACHABLE
This should be used to mark dead code.
const d_it::innert * find_child(const std::size_t n) const
small_mapt< innert > to_mapt
d_it::innert * add_child(const std::size_t n)
const leaft * find_leaf(const keyT &k) const
void swap(sharing_node_innert &other)
const d_lt & read() const
static small_shared_two_way_ptrt< d_internalt< keyT, valueT, equalT >, d_containert< SN_TYPE_ARGS > > empty_data
leaf_listt & get_container()
const leaf_listt & get_container() const
d_leaft< keyT, valueT, equalT > d_lt
d_internalt< keyT, valueT, equalT > d_it
small_shared_ptrt< d_leaft< keyT, valueT, equalT > > data
std::forward_list< leaft > leaf_listt
static small_shared_ptrt< d_leaft< keyT, valueT, equalT > > empty_data
d_containert< keyT, valueT, equalT > d_ct
void swap(sharing_node_leaft &other)
const d_ct & read_container() const
d_ct::leaf_listt leaf_listt
This class is really similar to boost's intrusive_pointer, but can be a bit simpler seeing as we're o...
sharing_node_leaft(const keyT &k, const valueT &v)
sharing_node_innert< keyT, valueT, equalT > innert
small_shared_two_way_ptrt< d_internalt< keyT, valueT, equalT >, d_containert< SN_TYPE_ARGS > > data
const keyT & get_key() const
const_iterator find(std::size_t idx) const