michael/lean2
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

refactor(util/rb_tree): remove optimization that creates problems for

Browse source 
some compilers
This commit is contained in:
Leonardo de Moura 2014-09-24 10:33:25 -07:00
parent 9b61b18eaa
commit 41433a4002
1 changed files with 0 additions and 28 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

28
src/util/rb_tree.h
View file

@ -14,11 +14,6 @@ Author: Leonardo de Moura
#include "util/memory_pool.h"
namespace lean {
#if defined(__CLANG__) && defined(__APPLE__) && !defined(LEAN_USE_BOOST)
// TODO(Leo): remove when problen on clang++ OSX thread local storage implementation is fixed
#define LEAN_TEMPLATE_THREAD_LOCAL_UNSAFE
#endif
/**
\brief Left-leaning Red-Black Trees
@ -68,27 +63,13 @@ class rb_tree : public CMP {
node_cell(node_cell const & s):m_left(s.m_left), m_right(s.m_right), m_value(s.m_value), m_red(s.m_red), m_rc(0) {}
};
#if !defined(LEAN_TEMPLATE_THREAD_LOCAL_UNSAFE)
typedef memory_pool<sizeof(node_cell)> node_allocator;
static node_allocator & get_node_allocator() {
LEAN_THREAD_PTR(node_allocator) g_allocator;
if (!g_allocator.get())
g_allocator.reset(new node_allocator());
return *g_allocator;
}
#endif
int cmp(T const & v1, T const & v2) const {
return CMP::operator()(v1, v2);
}
static node ensure_unshared(node && n) {
if (n.is_shared()) {
#if defined(LEAN_TEMPLATE_THREAD_LOCAL_UNSAFE)
return node(new node_cell(*n.m_ptr));
#else
return node(new (get_node_allocator().allocate()) node_cell(*n.m_ptr));
#endif
} else {
return n;
}
@ -147,11 +128,7 @@ class rb_tree : public CMP {
node insert(node && n, T const & v) {
if (!n) {
#if defined(LEAN_TEMPLATE_THREAD_LOCAL_UNSAFE)
return node(new node_cell(v));
#else
return node(new (get_node_allocator().allocate()) node_cell(v));
#endif
}
node h = ensure_unshared(n.steal());
@ -400,12 +377,7 @@ public:
template<typename T, typename CMP>
void rb_tree<T, CMP>::node_cell::dealloc() {
#if defined(LEAN_TEMPLATE_THREAD_LOCAL_UNSAFE)
delete this;
#else
this->~node_cell();
get_node_allocator().recycle(this);
#endif
}
template<typename T, typename CMP>