12#ifndef CPROVER_UTIL_SHARING_NODE_H
13#define CPROVER_UTIL_SHARING_NODE_H
19#include <forward_list>
28#define SN_SHARE_KEYS 0
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)
47#define SN_ASSERT_USE(v, b) static_cast<void>(v);
51#define SN_TYPE_PAR_DECL \
52 template <typename keyT, \
54 typename equalT = std::equal_to<keyT>>
56#define SN_TYPE_PAR_DEF \
57 template <typename keyT, typename valueT, typename equalT>
59#define SN_TYPE_ARGS keyT, valueT, equalT
61#define SN_PTR_TYPE_ARGS \
62 d_containert<SN_TYPE_ARGS>, d_leaft<SN_TYPE_ARGS>, d_internalt<SN_TYPE_ARGS>
76 typedef std::map<std::size_t, innert>
to_mapt;
95 typedef std::shared_ptr<keyT>
keyt;
100 template <
class valueU>
128 template <
class valueU>
133#if SN_SHARE_KEYS == 1
136 std::make_shared<keyT>(k), std::forward<valueU>(v));
165 return data.use_count();
177 return data.template is_derived<2>();
182 return data.template is_derived<0>();
187 return data.template is_derived<1>();
209 return *
data.template get_derived<2>();
216 return *
data.template get_derived<0>();
223 return *
data.template get_derived<1>();
256 for(
const auto &n : c)
260 if(equalT()(n.get_key(), k))
277 if(equalT()(n.get_key(), k))
286 template <
class valueU>
296 c.emplace_front(k, std::forward<valueU>(v));
309 const leaft &first = c.front();
311 if(equalT()(first.
get_key(), k))
317 typename leaf_listt::const_iterator last_it = c.begin();
319 typename leaf_listt::const_iterator it = c.begin();
322 for(; it != c.end(); it++)
324 const leaft &leaf = *it;
328 if(equalT()(leaf.
get_key(), k))
330 c.erase_after(last_it);
347 typename to_mapt::const_iterator it = m.
find(n);
351 return &it.get_value();
373 std::size_t
r = m.
erase(n);
384#if SN_SHARE_KEYS == 1
398 template <
class valueU>
406 template <
class valueU>
411 if(
data.use_count() > 1)
418 data.template get_derived<1>()->v = std::forward<valueU>(v);
428 if(
data.use_count() > 1)
433 mutator(
data.template get_derived<1>()->v);
447 else if(
data.use_count() > 1)
454 return *
data.template get_derived<2>();
465 else if(
data.use_count() > 1)
472 return *
data.template get_derived<0>();
const T * as_const_ptr(T *t)
Return a pointer to the same object but ensures the type is pointer to const.
sharing_nodet< keyT, valueT, equalT > leaft
std::forward_list< leaft > leaf_listt
sharing_nodet< keyT, valueT, equalT > innert
small_mapt< innert > to_mapt
d_leaft(const keyt &k, valueU &&v)
bool is_defined_container() const
void make_leaf(const keyT &k, valueU &&v)
leaft * find_leaf(const keyT &k)
void set_value(valueU &&v)
d_internalt< keyT, valueT, equalT > d_it
void remove_child(const std::size_t n)
bool is_defined_internal() const
void swap(sharing_nodet &other)
void place_leaf(const keyT &k, valueU &&v)
d_containert< keyT, valueT, equalT > d_ct
small_shared_n_way_ptrt< d_containert< keyT, valueT, equalT >, d_leaft< keyT, valueT, equalT >, d_internalt< keyT, valueT, equalT > > datat
const leaf_listt & get_container() const
d_ct::leaf_listt leaf_listt
void mutate_value(std::function< void(valueT &)> mutator)
bool is_defined_leaf() const
const valueT & get_value() const
const d_it::innert * find_child(const std::size_t n) const
const d_it & read_internal() const
use_countt use_count() const
const leaft * find_leaf(const keyT &k) const
bool shares_with(const sharing_nodet &other) const
d_it::innert & add_child(const std::size_t n)
sharing_nodet(const keyT &k, valueU &&v)
leaf_listt & get_container()
datat::use_countt use_countt
const to_mapt & get_to_map() const
d_leaft< keyT, valueT, equalT > d_lt
bool is_container() const
const d_ct & read_container() const
void remove_leaf(const keyT &k)
const keyT & get_key() const
const d_lt & read_leaf() const
Map from small integers to values.
const_iterator find(std::size_t idx) const
const_iterator end() const
std::size_t erase(std::size_t idx)
This class is similar to small_shared_ptrt and boost's intrusive_ptr.
decltype(std::declval< typename get_typet< 0, Ts... >::type >() .get_use_count()) use_countt
small_shared_n_way_pointee_baset< 3, unsigned > d_baset
#define SN_ASSERT_USE(v, b)
small_shared_n_way_ptrt< U, V, W > make_shared_3(Ts &&... ts)
Constructs a small shared n-way pointer, with three possible pointee types (i.e., n = 3),...
#define UNREACHABLE
This should be used to mark dead code.
#define PRECONDITION(CONDITION)