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(const keyT &k, const valueT &v)
void swap(sharing_node_innert &other)
static small_shared_ptrt< d_leaft< keyT, valueT, equalT > > empty_data
bool shares_with(const sharing_node_leaft &other) const
void remove_leaf(const keyT &k)
const to_mapt & get_to_map() const
A helper class to store use-counts of objects held by small shared pointers.
#define SN_ASSERT_USE(v, b)
leaft * place_leaf(const keyT &k, const valueT &v)
const d_it::innert * find_child(const std::size_t n) const
sharing_node_leaft< keyT, valueT, equalT > leaft
d_it::innert * add_child(const std::size_t n)
const leaf_listt & get_container() const
std::forward_list< leaft > leaf_listt
bool is_container() const
const valueT & get_value() const
This class is really similar to boost's intrusive_pointer, but can be a bit simpler seeing as we're o...
const_iterator end() const
const_iterator find(std::size_t idx) const
std::size_t erase(std::size_t idx)
small_shared_two_way_ptrt< d_internalt< keyT, valueT, equalT >, d_containert< keyT, valueT, equalT > > data
const d_ct & read_container() const
const d_lt & read() const
d_containert< keyT, valueT, equalT > d_ct
leaf_listt & get_container()
d_internalt< keyT, valueT, equalT > d_it
d_ct::leaf_listt leaf_listt
d_leaft< keyT, valueT, equalT > d_lt
leaft * find_leaf(const keyT &k)
bool shares_with(const sharing_node_innert &other) const
void swap(sharing_node_leaft &other)
#define UNREACHABLE
This should be used to mark dead code.
static small_shared_two_way_ptrt< d_internalt< keyT, valueT, equalT >, d_containert< keyT, valueT, equalT > > empty_data
const d_it & read_internal() const
const keyT & get_key() const
small_shared_two_way_pointeet< unsigned > d_baset
This class is similar to small_shared_ptrt and boost's intrusive_ptr.
sharing_node_innert< keyT, valueT, equalT > innert
small_shared_ptrt< d_leaft< keyT, valueT, equalT > > data
small_mapt< innert > to_mapt
const leaft * find_leaf(const keyT &k) const
void remove_child(const std::size_t n)