chore(util): remove dead code
This commit is contained in:
Leonardo de Moura
parent
9561b45af1
commit
83f64ef8b3
5 changed files with 1 additions and 782 deletions
|
|
@ -34,15 +34,9 @@ add_test(rb_tree "${CMAKE_CURRENT_BINARY_DIR}/rb_tree")
|
|||
add_executable(rb_map rb_map.cpp $<TARGET_OBJECTS:util>)
|
||||
target_link_libraries(rb_map ${EXTRA_LIBS})
|
||||
add_test(rb_map "${CMAKE_CURRENT_BINARY_DIR}/rb_map")
|
||||
add_executable(splay_tree splay_tree.cpp $<TARGET_OBJECTS:util>)
|
||||
target_link_libraries(splay_tree ${EXTRA_LIBS})
|
||||
add_test(parray "${CMAKE_CURRENT_BINARY_DIR}/parray")
|
||||
add_executable(parray parray.cpp $<TARGET_OBJECTS:util>)
|
||||
target_link_libraries(parray ${EXTRA_LIBS})
|
||||
add_test(splay_tree "${CMAKE_CURRENT_BINARY_DIR}/splay_tree")
|
||||
add_executable(splay_map splay_map.cpp $<TARGET_OBJECTS:util>)
|
||||
target_link_libraries(splay_map ${EXTRA_LIBS})
|
||||
add_test(splay_map "${CMAKE_CURRENT_BINARY_DIR}/splay_map")
|
||||
add_test(parray "${CMAKE_CURRENT_BINARY_DIR}/parray")
|
||||
add_executable(exception exception.cpp $<TARGET_OBJECTS:util>)
|
||||
target_link_libraries(exception ${EXTRA_LIBS})
|
||||
add_test(exception "${CMAKE_CURRENT_BINARY_DIR}/exception")
|
||||
|
|
|
|||
|
|
@ -1,49 +0,0 @@
|
|||
/*
|
||||
Copyright (c) 2013 Microsoft Corporation. All rights reserved.
|
||||
Released under Apache 2.0 license as described in the file LICENSE.
|
||||
|
||||
Author: Leonardo de Moura
|
||||
*/
|
||||
#include <iostream>
|
||||
#include <sstream>
|
||||
#include "util/test.h"
|
||||
#include "util/splay_map.h"
|
||||
#include "util/name.h"
|
||||
using namespace lean;
|
||||
|
||||
struct int_cmp { int operator()(int i1, int i2) const { return i1 < i2 ? -1 : (i1 > i2 ? 1 : 0); } };
|
||||
|
||||
typedef splay_map<int, name, int_cmp> int2name;
|
||||
|
||||
static void tst0() {
|
||||
int2name m1;
|
||||
m1[10] = name("t1");
|
||||
m1[20] = name("t2");
|
||||
int2name m2(m1);
|
||||
m2[10] = name("t3");
|
||||
lean_assert(m1[10] == name("t1"));
|
||||
lean_assert(m1[20] == name("t2"));
|
||||
lean_assert(m2[10] == name("t3"));
|
||||
lean_assert(m2[20] == name("t2"));
|
||||
lean_assert(m2.size() == 2);
|
||||
lean_assert(m2[100] == name());
|
||||
lean_assert(m2.size() == 3);
|
||||
lean_assert(m2[100] == name());
|
||||
lean_assert(m2.size() == 3);
|
||||
}
|
||||
|
||||
static void tst1() {
|
||||
int2name m1, m2;
|
||||
m1[10] = name("t1");
|
||||
lean_assert(m1.size() == 1);
|
||||
lean_assert(m2.size() == 0);
|
||||
swap(m1, m2);
|
||||
lean_assert(m2.size() == 1);
|
||||
lean_assert(m1.size() == 0);
|
||||
}
|
||||
|
||||
int main() {
|
||||
tst0();
|
||||
tst1();
|
||||
return has_violations() ? 1 : 0;
|
||||
}
|
||||
|
|
@ -1,174 +0,0 @@
|
|||
/*
|
||||
Copyright (c) 2013 Microsoft Corporation. All rights reserved.
|
||||
Released under Apache 2.0 license as described in the file LICENSE.
|
||||
|
||||
Author: Leonardo de Moura
|
||||
*/
|
||||
#include <iostream>
|
||||
#include <vector>
|
||||
#include <random>
|
||||
#include <ctime>
|
||||
#include <unordered_set>
|
||||
#include <sstream>
|
||||
#include "util/test.h"
|
||||
#include "util/splay_tree.h"
|
||||
#include "util/timeit.h"
|
||||
using namespace lean;
|
||||
|
||||
struct int_lt { int operator()(int i1, int i2) const { return i1 < i2 ? -1 : (i1 > i2 ? 1 : 0); } };
|
||||
|
||||
typedef splay_tree<int, int_lt> int_splay_tree;
|
||||
typedef std::unordered_set<int> int_set;
|
||||
|
||||
static void tst0() {
|
||||
int_splay_tree s;
|
||||
s.insert(10);
|
||||
s.insert(11);
|
||||
s.insert(9);
|
||||
std::cout << s << "\n";
|
||||
int_splay_tree s2 = s;
|
||||
std::cout << s2 << "\n";
|
||||
s.insert(20);
|
||||
std::cout << s << "\n";
|
||||
s.insert(15);
|
||||
}
|
||||
|
||||
static void tst1() {
|
||||
int_splay_tree s;
|
||||
s.insert(10);
|
||||
s.insert(3);
|
||||
s.insert(20);
|
||||
std::cout << s << "\n";
|
||||
s.insert(40);
|
||||
std::cout << s << "\n";
|
||||
s.insert(5);
|
||||
std::cout << s << "\n";
|
||||
s.insert(11);
|
||||
std::cout << s << "\n";
|
||||
s.insert(20);
|
||||
std::cout << s << "\n";
|
||||
s.insert(30);
|
||||
std::cout << s << "\n";
|
||||
s.insert(25);
|
||||
std::cout << s << "\n";
|
||||
s.insert(15);
|
||||
lean_assert(s.contains(40));
|
||||
lean_assert(s.contains(11));
|
||||
lean_assert(s.contains(20));
|
||||
lean_assert(s.contains(25));
|
||||
lean_assert(s.contains(5));
|
||||
lean_assert(s.contains(10));
|
||||
lean_assert(s.contains(3));
|
||||
lean_assert(s.contains(20));
|
||||
std::cout << s << "\n";
|
||||
int_splay_tree s2(s);
|
||||
std::cout << s2 << "\n";
|
||||
s.insert(34);
|
||||
std::cout << s2 << "\n";
|
||||
std::cout << s << "\n";
|
||||
int const * v = s.find(11);
|
||||
lean_assert(*v == 11);
|
||||
std::cout << s << "\n";
|
||||
lean_assert(!s.empty());
|
||||
s.clear();
|
||||
lean_assert(s.empty());
|
||||
}
|
||||
|
||||
static bool operator==(int_set const & v1, int_splay_tree const & v2) {
|
||||
buffer<int> b;
|
||||
// std::cout << v2 << "\n";
|
||||
// std::for_each(v1.begin(), v1.end(), [](int v) { std::cout << v << " "; }); std::cout << "\n";
|
||||
v2.to_buffer(b);
|
||||
if (v1.size() != b.size())
|
||||
return false;
|
||||
for (unsigned i = 0; i < b.size(); i++) {
|
||||
if (v1.find(b[i]) == v1.end())
|
||||
return false;
|
||||
}
|
||||
return true;
|
||||
}
|
||||
|
||||
static void driver(unsigned max_sz, unsigned max_val, unsigned num_ops, double insert_freq, double copy_freq) {
|
||||
int_set v1;
|
||||
int_splay_tree v2;
|
||||
int_splay_tree v3;
|
||||
std::mt19937 rng;
|
||||
size_t acc_sz = 0;
|
||||
rng.seed(static_cast<unsigned int>(time(0)));
|
||||
std::uniform_int_distribution<unsigned int> uint_dist;
|
||||
|
||||
std::vector<int_splay_tree> copies;
|
||||
for (unsigned i = 0; i < num_ops; i++) {
|
||||
acc_sz += v1.size();
|
||||
double f = static_cast<double>(uint_dist(rng) % 10000) / 10000.0;
|
||||
if (f < copy_freq) {
|
||||
copies.push_back(v2);
|
||||
}
|
||||
f = static_cast<double>(uint_dist(rng) % 10000) / 10000.0;
|
||||
// read random positions of v3
|
||||
for (unsigned int j = 0; j < uint_dist(rng) % 5; j++) {
|
||||
int a = uint_dist(rng) % max_val;
|
||||
lean_assert(v3.contains(a) == (v1.find(a) != v1.end()));
|
||||
}
|
||||
if (f < insert_freq) {
|
||||
if (v1.size() >= max_sz)
|
||||
continue;
|
||||
int a = uint_dist(rng) % max_val;
|
||||
v1.insert(a);
|
||||
v2.insert(a);
|
||||
v3 = insert(v3, a);
|
||||
} else {
|
||||
int a = uint_dist(rng) % max_val;
|
||||
v1.erase(a);
|
||||
v2.erase(a);
|
||||
v3 = erase(v3, a);
|
||||
}
|
||||
lean_assert(v1 == v2);
|
||||
lean_assert(v1 == v3);
|
||||
lean_assert(v1.size() == v2.size());
|
||||
}
|
||||
std::cout << "\n";
|
||||
std::cout << "Copies created: " << copies.size() << "\n";
|
||||
std::cout << "Average size: " << static_cast<double>(acc_sz) / static_cast<double>(num_ops) << "\n";
|
||||
}
|
||||
|
||||
static void tst2() {
|
||||
driver(4, 32, 10000, 0.5, 0.01);
|
||||
driver(4, 10000, 10000, 0.5, 0.01);
|
||||
driver(16, 16, 10000, 0.5, 0.1);
|
||||
driver(128, 64, 10000, 0.5, 0.1);
|
||||
driver(128, 64, 10000, 0.4, 0.1);
|
||||
driver(128, 1000, 10000, 0.5, 0.5);
|
||||
driver(128, 1000, 10000, 0.5, 0.01);
|
||||
}
|
||||
|
||||
static void tst3() {
|
||||
int_splay_tree v;
|
||||
v.insert(10);
|
||||
v.insert(5);
|
||||
v.insert(1);
|
||||
v.insert(3);
|
||||
lean_assert_eq(fold(v, [](int a, int b) { return a + b; }, 0), 19);
|
||||
std::ostringstream out;
|
||||
for_each(v, [&](int a) { out << a << " "; });
|
||||
std::cout << out.str() << "\n";
|
||||
lean_assert(out.str() == "1 3 5 10 ");
|
||||
}
|
||||
|
||||
static void tst4() {
|
||||
int_splay_tree s;
|
||||
s.insert(10);
|
||||
s.insert(20);
|
||||
lean_assert(s.find(30) == nullptr);
|
||||
lean_assert(*(s.find(20)) == 20);
|
||||
lean_assert(*(s.find(10)) == 10);
|
||||
}
|
||||
|
||||
int main() {
|
||||
tst0();
|
||||
tst1();
|
||||
tst2();
|
||||
tst3();
|
||||
tst4();
|
||||
return has_violations() ? 1 : 0;
|
||||
}
|
||||
|
|
@ -1,103 +0,0 @@
|
|||
/*
|
||||
Copyright (c) 2013 Microsoft Corporation. All rights reserved.
|
||||
Released under Apache 2.0 license as described in the file LICENSE.
|
||||
|
||||
Author: Leonardo de Moura
|
||||
*/
|
||||
#pragma once
|
||||
#include <utility>
|
||||
#include "util/pair.h"
|
||||
#include "util/splay_tree.h"
|
||||
|
||||
namespace lean {
|
||||
/**
|
||||
\brief Wrapper for implementing maps using splay trees.
|
||||
*/
|
||||
template<typename K, typename T, typename CMP>
|
||||
class splay_map : public CMP {
|
||||
public:
|
||||
typedef pair<K, T> entry;
|
||||
private:
|
||||
struct entry_cmp : public CMP {
|
||||
entry_cmp(CMP const & c):CMP(c) {}
|
||||
int operator()(entry const & e1, entry const & e2) const { return CMP::operator()(e1.first, e2.first); }
|
||||
};
|
||||
splay_tree<entry, entry_cmp> m_map;
|
||||
public:
|
||||
splay_map(CMP const & cmp = CMP()):m_map(entry_cmp(cmp)) {
|
||||
// the return type of CMP()(k1, k2) should be int
|
||||
static_assert(std::is_same<typename std::result_of<decltype(std::declval<CMP>())(K const &, K const &)>::type,
|
||||
int>::value,
|
||||
"The return type of CMP()(k1, k2) is not int.");
|
||||
}
|
||||
friend void swap(splay_map & a, splay_map & b) { swap(a.m_map, b.m_map); }
|
||||
bool empty() const { return m_map.empty(); }
|
||||
void clear() { m_map.clear(); }
|
||||
bool is_eqp(splay_map const & m) const { return m_map.is_eqp(m); }
|
||||
unsigned size() const { return m_map.size(); }
|
||||
void insert(K const & k, T const & v) { m_map.insert(mk_pair(k, v)); }
|
||||
T const * find(K const & k) const { auto e = m_map.find(mk_pair(k, T())); return e ? &(e->second) : nullptr; }
|
||||
T * find(K const & k) { auto e = m_map.find(mk_pair(k, T())); return e ? &(const_cast<T&>(e->second)) : nullptr; }
|
||||
bool contains(K const & k) const { return m_map.contains(mk_pair(k, T())); }
|
||||
void erase(K const & k) { m_map.erase(mk_pair(k, T())); }
|
||||
|
||||
class ref {
|
||||
splay_map & m_map;
|
||||
K const & m_key;
|
||||
public:
|
||||
ref(splay_map & m, K const & k):m_map(m), m_key(k) {}
|
||||
ref & operator=(T const & v) { m_map.insert(m_key, v); return *this; }
|
||||
operator T const &() const {
|
||||
T const * e = m_map.find(m_key);
|
||||
if (e) {
|
||||
return *e;
|
||||
} else {
|
||||
m_map.insert(m_key, T());
|
||||
return *(m_map.find(m_key));
|
||||
}
|
||||
}
|
||||
};
|
||||
|
||||
/**
|
||||
\brief Returns a reference to the value that is mapped to a key equivalent to key,
|
||||
performing an insertion if such key does not already exist.
|
||||
*/
|
||||
ref operator[](K const & k) { return ref(*this, k); }
|
||||
|
||||
template<typename F>
|
||||
void for_each(F f) const {
|
||||
static_assert(std::is_same<typename std::result_of<F(K const &, T const &)>::type, void>::value,
|
||||
"for_each: return type of f is not void");
|
||||
auto f_prime = [&](entry const & e) { f(e.first, e.second); };
|
||||
return m_map.for_each(f_prime);
|
||||
}
|
||||
|
||||
/** \brief (For debugging) Display the content of this splay map. */
|
||||
friend std::ostream & operator<<(std::ostream & out, splay_map const & m) {
|
||||
out << "{";
|
||||
m.for_each([&out](K const & k, T const & v) {
|
||||
out << k << " |-> " << v << "; ";
|
||||
});
|
||||
out << "}";
|
||||
return out;
|
||||
}
|
||||
};
|
||||
template<typename K, typename T, typename CMP>
|
||||
splay_map<K, T, CMP> insert(splay_map<K, T, CMP> const & m, K const & k, T const & v) {
|
||||
auto r = m;
|
||||
r.insert(k, v);
|
||||
return r;
|
||||
}
|
||||
template<typename K, typename T, typename CMP>
|
||||
splay_map<K, T, CMP> erase(splay_map<K, T, CMP> const & m, K const & k) {
|
||||
auto r = m;
|
||||
r.erase(k);
|
||||
return r;
|
||||
}
|
||||
template<typename K, typename T, typename CMP, typename F>
|
||||
void for_each(splay_map<K, T, CMP> const & m, F f) {
|
||||
static_assert(std::is_same<typename std::result_of<F(K const &, T const &)>::type, void>::value,
|
||||
"for_each: return type of f is not void");
|
||||
return m.for_each(f);
|
||||
}
|
||||
}
|
||||
|
|
@ -1,449 +0,0 @@
|
|||
/*
|
||||
Copyright (c) 2013 Microsoft Corporation. All rights reserved.
|
||||
Released under Apache 2.0 license as described in the file LICENSE.
|
||||
|
||||
Author: Leonardo de Moura
|
||||
*/
|
||||
#pragma once
|
||||
#include <iostream>
|
||||
#include <algorithm>
|
||||
#include <utility>
|
||||
#include "util/rc.h"
|
||||
#include "util/pair.h"
|
||||
#include "util/debug.h"
|
||||
#include "util/buffer.h"
|
||||
#include "util/thread.h"
|
||||
|
||||
namespace lean {
|
||||
/**
|
||||
\brief Splay trees (see http://en.wikipedia.org/wiki/Splay_tree)
|
||||
|
||||
It uses a O(1) copy operation. Different tree can share nodes.
|
||||
The sharing is thread-safe.
|
||||
|
||||
\c CMP is a functional object for comparing values of type T.
|
||||
It must have a method
|
||||
<code>
|
||||
int operator()(T const & v1, T const & v2) const;
|
||||
</code>
|
||||
The method must return
|
||||
- -1 if <tt>v1 < v2</tt>,
|
||||
- 0 if <tt>v1 == v2</tt>,
|
||||
- 1 if <tt>v1 > v2</tt>
|
||||
*/
|
||||
template<typename T, typename CMP>
|
||||
class splay_tree : public CMP {
|
||||
struct node {
|
||||
node * m_left;
|
||||
node * m_right;
|
||||
T m_value;
|
||||
MK_LEAN_RC();
|
||||
static void inc_ref(node * n) { if (n) n->inc_ref(); }
|
||||
static void dec_ref(node * n) { if (n) n->dec_ref(); }
|
||||
explicit node(T const & v, node * left = nullptr, node * right = nullptr):
|
||||
m_left(left), m_right(right), m_value(v), m_rc(0) {
|
||||
// the return type of CMP()(t1, 2) should be int
|
||||
static_assert(std::is_same<typename std::result_of<decltype(std::declval<CMP>())(T const &, T const &)>::type,
|
||||
int>::value,
|
||||
"The return type of CMP()(t1, t2) is not int.");
|
||||
inc_ref(m_left);
|
||||
inc_ref(m_right);
|
||||
}
|
||||
node(node const & n):node(n.m_value, n.m_left, n.m_right) {}
|
||||
~node() {
|
||||
dec_ref(m_left);
|
||||
dec_ref(m_right);
|
||||
}
|
||||
void dealloc() {
|
||||
delete this;
|
||||
}
|
||||
bool is_shared() const { return m_rc > 1; }
|
||||
|
||||
static void display(std::ostream & out, node const * n) {
|
||||
if (n) {
|
||||
if (n->m_left == nullptr && n->m_right == nullptr) {
|
||||
out << n->m_value << ":" << n->m_rc;
|
||||
} else {
|
||||
out << "(" << n->m_value << ":" << n->m_rc << " ";
|
||||
display(out, n->m_left);
|
||||
out << " ";
|
||||
display(out, n->m_right);
|
||||
out << ")";
|
||||
}
|
||||
} else {
|
||||
out << "()";
|
||||
}
|
||||
}
|
||||
};
|
||||
|
||||
node * m_ptr;
|
||||
|
||||
int cmp(T const & v1, T const & v2) const {
|
||||
return CMP::operator()(v1, v2);
|
||||
}
|
||||
|
||||
void update(node * n, node * l, node * r) {
|
||||
lean_assert(!n->is_shared());
|
||||
n->m_left = l;
|
||||
n->m_right = r;
|
||||
}
|
||||
|
||||
struct entry {
|
||||
bool m_right;
|
||||
node * m_node;
|
||||
entry(bool r, node * n):m_right(r), m_node(n) {}
|
||||
};
|
||||
|
||||
void splay_to_top(buffer<entry, 32> & path, node * n) {
|
||||
lean_assert(!n->is_shared());
|
||||
while (path.size() > 1) {
|
||||
auto p_entry = path.back(); path.pop_back();
|
||||
auto g_entry = path.back(); path.pop_back();
|
||||
bool g_right = g_entry.m_right;
|
||||
bool p_right = p_entry.m_right;
|
||||
node * g = g_entry.m_node;
|
||||
node * p = p_entry.m_node;
|
||||
lean_assert(!g->is_shared());
|
||||
lean_assert(!p->is_shared());
|
||||
if (!g_right && !p_right) {
|
||||
// zig-zig left
|
||||
// (g (p (n A B) C) D) ==> (n A (p B (g C D)))
|
||||
lean_assert(g->m_left == p);
|
||||
node * A = n->m_left;
|
||||
node * B = n->m_right;
|
||||
node * C = p->m_right;
|
||||
node * D = g->m_right;
|
||||
update(g, C, D);
|
||||
update(p, B, g);
|
||||
update(n, A, p);
|
||||
} else if (!g_right && p_right) {
|
||||
// zig-zag left-right
|
||||
// (g (p A (n B C)) D) ==> (n (p A B) (g C D))
|
||||
lean_assert(g->m_left == p);
|
||||
node * A = p->m_left;
|
||||
node * B = n->m_left;
|
||||
node * C = n->m_right;
|
||||
node * D = g->m_right;
|
||||
update(p, A, B);
|
||||
update(g, C, D);
|
||||
update(n, p, g);
|
||||
} else if (g_right && !p_right) {
|
||||
// zig-zag right-left
|
||||
// (g A (p (n B C) D)) ==> (n (g A B) (p C D))
|
||||
lean_assert(g->m_right == p);
|
||||
node * A = g->m_left;
|
||||
node * B = n->m_left;
|
||||
node * C = n->m_right;
|
||||
node * D = p->m_right;
|
||||
update(g, A, B);
|
||||
update(p, C, D);
|
||||
update(n, g, p);
|
||||
} else {
|
||||
lean_assert(g_right && p_right);
|
||||
lean_assert(g->m_right == p);
|
||||
// zig-zig right
|
||||
// (g A (p B (n C D))) ==> (n (p (g A B) C) D)
|
||||
node * A = g->m_left;
|
||||
node * B = p->m_left;
|
||||
node * C = n->m_left;
|
||||
node * D = n->m_right;
|
||||
update(g, A, B);
|
||||
update(p, g, C);
|
||||
update(n, p, D);
|
||||
}
|
||||
}
|
||||
lean_assert(!n->is_shared());
|
||||
if (path.size() == 1) {
|
||||
auto p_entry = path.back(); path.pop_back();
|
||||
bool p_right = p_entry.m_right;
|
||||
node * p = p_entry.m_node;
|
||||
if (!p_right) {
|
||||
// zig left
|
||||
// (p (n A B) C) ==> (n A (p B C))
|
||||
node * A = n->m_left;
|
||||
node * B = n->m_right;
|
||||
node * C = p->m_right;
|
||||
update(p, B, C);
|
||||
update(n, A, p);
|
||||
} else {
|
||||
// zig right
|
||||
// (p A (n B C)) ==> (n (p A B) C)
|
||||
node * A = p->m_left;
|
||||
node * B = n->m_left;
|
||||
node * C = n->m_right;
|
||||
update(p, A, B);
|
||||
update(n, p, C);
|
||||
}
|
||||
}
|
||||
lean_assert(path.empty());
|
||||
lean_assert(!n->is_shared());
|
||||
}
|
||||
|
||||
bool check_invariant(node const * n) const {
|
||||
if (n) {
|
||||
if (n->m_left) {
|
||||
check_invariant(n->m_left);
|
||||
lean_assert_lt(cmp(n->m_left->m_value, n->m_value), 0);
|
||||
}
|
||||
if (n->m_right) {
|
||||
check_invariant(n->m_right);
|
||||
lean_assert_lt(cmp(n->m_value, n->m_right->m_value), 0);
|
||||
}
|
||||
}
|
||||
return true;
|
||||
}
|
||||
|
||||
void update_parent(buffer<entry, 32> const & path, node * child) {
|
||||
lean_assert(child);
|
||||
if (path.empty()) {
|
||||
child->inc_ref();
|
||||
node::dec_ref(m_ptr);
|
||||
m_ptr = child;
|
||||
} else {
|
||||
child->inc_ref();
|
||||
entry const & last = path.back();
|
||||
node * parent = last.m_node;
|
||||
lean_assert(!parent->is_shared());
|
||||
if (last.m_right) {
|
||||
node::dec_ref(parent->m_right);
|
||||
parent->m_right = child;
|
||||
} else {
|
||||
node::dec_ref(parent->m_left);
|
||||
parent->m_left = child;
|
||||
}
|
||||
}
|
||||
}
|
||||
|
||||
static void to_buffer(node const * n, buffer<T> & r) {
|
||||
if (n) {
|
||||
to_buffer(n->m_left, r);
|
||||
r.push_back(n->m_value);
|
||||
to_buffer(n->m_right, r);
|
||||
}
|
||||
}
|
||||
|
||||
bool insert_pull(T const & v, bool is_insert) {
|
||||
buffer<entry, 32> path;
|
||||
node * n = m_ptr;
|
||||
bool found = false;
|
||||
while (true) {
|
||||
if (n == nullptr) {
|
||||
if (is_insert) {
|
||||
n = new node(v);
|
||||
update_parent(path, n);
|
||||
} else {
|
||||
if (path.empty())
|
||||
return false;
|
||||
n = path.back().m_node;
|
||||
path.pop_back();
|
||||
}
|
||||
break;
|
||||
} else {
|
||||
if (n->is_shared()) {
|
||||
n = new node(*n);
|
||||
update_parent(path, n);
|
||||
}
|
||||
lean_assert(!n->is_shared());
|
||||
int c = cmp(v, n->m_value);
|
||||
if (c < 0) {
|
||||
path.emplace_back(false, n);
|
||||
n = n->m_left;
|
||||
} else if (c > 0) {
|
||||
path.emplace_back(true, n);
|
||||
n = n->m_right;
|
||||
} else {
|
||||
if (is_insert)
|
||||
n->m_value = v;
|
||||
found = true;
|
||||
break;
|
||||
}
|
||||
}
|
||||
}
|
||||
splay_to_top(path, n);
|
||||
m_ptr = n;
|
||||
lean_assert(check_invariant());
|
||||
return found;
|
||||
}
|
||||
|
||||
bool pull(T const & v) {
|
||||
return insert_pull(v, false);
|
||||
}
|
||||
|
||||
void pull_max() {
|
||||
if (!m_ptr) return;
|
||||
buffer<entry, 32> path;
|
||||
node * n = m_ptr;
|
||||
while (true) {
|
||||
lean_assert(n);
|
||||
if (n->is_shared()) {
|
||||
n = new node(*n);
|
||||
update_parent(path, n);
|
||||
}
|
||||
if (n->m_right) {
|
||||
path.emplace_back(true, n);
|
||||
n = n->m_right;
|
||||
} else {
|
||||
splay_to_top(path, n);
|
||||
m_ptr = n;
|
||||
lean_assert(check_invariant());
|
||||
return;
|
||||
}
|
||||
}
|
||||
}
|
||||
|
||||
template<typename F, typename R>
|
||||
static R fold(node const * n, F && f, R r) {
|
||||
static_assert(std::is_same<typename std::result_of<F(T const &, R)>::type, R>::value,
|
||||
"fold: return type of f(t : T, r : R) is not R");
|
||||
if (n) {
|
||||
r = fold(n->m_left, f, r);
|
||||
r = f(n->m_value, r);
|
||||
return fold(n->m_right, f, r);
|
||||
} else {
|
||||
return r;
|
||||
}
|
||||
}
|
||||
|
||||
template<typename F>
|
||||
static void for_each(node const * n, F && f) {
|
||||
static_assert(std::is_same<typename std::result_of<F(T const &)>::type, void>::value,
|
||||
"for_each: return type of f is not void");
|
||||
if (n) {
|
||||
for_each(n->m_left, f);
|
||||
f(n->m_value);
|
||||
for_each(n->m_right, f);
|
||||
}
|
||||
}
|
||||
|
||||
splay_tree(splay_tree const & s, node * new_root):CMP(s), m_ptr(new_root) { node::inc_ref(m_ptr); }
|
||||
|
||||
public:
|
||||
splay_tree(CMP const & cmp = CMP()):CMP(cmp), m_ptr(nullptr) {}
|
||||
splay_tree(splay_tree const & s):CMP(s), m_ptr(s.m_ptr) { node::inc_ref(m_ptr); }
|
||||
splay_tree(splay_tree && s):CMP(s), m_ptr(s.m_ptr) { s.m_ptr = nullptr; }
|
||||
~splay_tree() { node::dec_ref(m_ptr); }
|
||||
|
||||
/** \brief O(1) copy */
|
||||
splay_tree & operator=(splay_tree const & s) { LEAN_COPY_REF(s); }
|
||||
/** \brief O(1) move */
|
||||
splay_tree & operator=(splay_tree && s) { LEAN_MOVE_REF(s); }
|
||||
|
||||
friend void swap(splay_tree & t1, splay_tree & t2) { std::swap(t1.m_ptr, t2.m_ptr); }
|
||||
|
||||
/** \brief Return true iff this splay tree is empty. */
|
||||
bool empty() const { return m_ptr == nullptr; }
|
||||
|
||||
/** \brief Remove all elements from the splay tree. */
|
||||
void clear() { node::dec_ref(m_ptr); m_ptr = nullptr; }
|
||||
|
||||
/** \brief Return true iff this splay tree and \c t point to the same node */
|
||||
bool is_eqp(splay_tree const & t) const { return m_ptr == t.m_ptr; }
|
||||
|
||||
/** \brief Return the size of the splay tree */
|
||||
unsigned size() const { return fold([](T const &, unsigned a) { return a + 1; }, 0u); }
|
||||
|
||||
/** \brief Insert \c v in this splay tree. */
|
||||
void insert(T const & v) {
|
||||
insert_pull(v, true);
|
||||
}
|
||||
|
||||
/**
|
||||
\brief Return a pointer to a value equal to \c v that is stored in this splay tree.
|
||||
If the splay tree does not contain any value equal to \c v, then return \c nullptr.
|
||||
|
||||
\remark <tt>find(v) != nullptr</tt> iff <tt>contains(v)</tt>
|
||||
|
||||
\warning The content of the tree is not modified, but it is "reorganized".
|
||||
*/
|
||||
T const * find(T const & v) const {
|
||||
if (const_cast<splay_tree*>(this)->pull(v)) {
|
||||
lean_assert(cmp(m_ptr->m_value, v) == 0);
|
||||
return &(m_ptr->m_value);
|
||||
} else {
|
||||
return nullptr;
|
||||
}
|
||||
}
|
||||
|
||||
/** \brief Return true iff the splay tree contains an element equal to \c v. */
|
||||
bool contains(T const & v) const {
|
||||
return find(v);
|
||||
}
|
||||
|
||||
/** \brief Remove \c v from this splay tree. Actually, it removes an element that is equal to \c v. */
|
||||
void erase(T const & v) {
|
||||
if (pull(v)) {
|
||||
lean_assert(cmp(m_ptr->m_value, v) == 0);
|
||||
splay_tree left(*this, m_ptr->m_left);
|
||||
splay_tree right(*this, m_ptr->m_right);
|
||||
if (left.empty()) {
|
||||
swap(*this, right);
|
||||
} else if (right.empty()) {
|
||||
swap(*this, left);
|
||||
} else {
|
||||
clear();
|
||||
left.pull_max();
|
||||
lean_assert(left.m_ptr->m_right == nullptr);
|
||||
right.m_ptr->inc_ref();
|
||||
left.m_ptr->m_right = right.m_ptr;
|
||||
swap(*this, left);
|
||||
}
|
||||
}
|
||||
}
|
||||
|
||||
/** \brief (For debugging) Check whether this splay tree is well formed. */
|
||||
bool check_invariant() const {
|
||||
return check_invariant(m_ptr);
|
||||
}
|
||||
|
||||
/**
|
||||
\brief Copy the contents of this splay tree to the given buffer.
|
||||
The elements will be stored in increasing order.
|
||||
*/
|
||||
void to_buffer(buffer<T> & r) const {
|
||||
to_buffer(m_ptr, r);
|
||||
}
|
||||
|
||||
/** \brief (For debugging) Display the content of this splay tree. */
|
||||
friend std::ostream & operator<<(std::ostream & out, splay_tree const & t) {
|
||||
node::display(out, t.m_ptr);
|
||||
return out;
|
||||
}
|
||||
|
||||
/**
|
||||
\brief Return <tt>f(a_k, ..., f(a_1, f(a_0, r)) ...)</tt>, where
|
||||
<tt>a_0, a_1, ... a_k</tt> are the elements is stored in the splay tree.
|
||||
*/
|
||||
template<typename F, typename R>
|
||||
R fold(F && f, R r) const {
|
||||
static_assert(std::is_same<typename std::result_of<F(T const &, R)>::type, R>::value,
|
||||
"fold: return type of f(t : T, r : R) is not R");
|
||||
return fold(m_ptr, std::forward<F>(f), r);
|
||||
}
|
||||
|
||||
/**
|
||||
\brief Apply \c f to each value stored in the splay tree.
|
||||
*/
|
||||
template<typename F>
|
||||
void for_each(F && f) const {
|
||||
static_assert(std::is_same<typename std::result_of<F(T const &)>::type, void>::value,
|
||||
"for_each: return type of f is not void");
|
||||
for_each(m_ptr, std::forward<F>(f));
|
||||
}
|
||||
};
|
||||
template<typename T, typename CMP>
|
||||
splay_tree<T, CMP> insert(splay_tree<T, CMP> & t, T const & v) { splay_tree<T, CMP> r(t); r.insert(v); return r; }
|
||||
template<typename T, typename CMP>
|
||||
splay_tree<T, CMP> erase(splay_tree<T, CMP> & t, T const & v) { splay_tree<T, CMP> r(t); r.erase(v); return r; }
|
||||
template<typename T, typename CMP, typename F, typename R>
|
||||
R fold(splay_tree<T, CMP> const & t, F && f, R r) {
|
||||
static_assert(std::is_same<typename std::result_of<F(T const &, R)>::type, R>::value,
|
||||
"fold: return type of f(t : T, r : R) is not R");
|
||||
return t.fold(std::forward<F>(f), r);
|
||||
}
|
||||
template<typename T, typename CMP, typename F>
|
||||
void for_each(splay_tree<T, CMP> const & t, F && f) {
|
||||
static_assert(std::is_same<typename std::result_of<F(T const &)>::type, void>::value,
|
||||
"for_each: return type of f is not void");
|
||||
return t.for_each(std::forward<F>(f));
|
||||
}
|
||||
}
|
||||
Loading…
Add table
Reference in a new issue