From fcf1778ee0f32ec43c4c3a12b5d284ee020047cc Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Tue, 19 Aug 2014 15:45:00 -0700 Subject: [PATCH] feat(util): add sequence object with O(1) concatenation operation Signed-off-by: Leonardo de Moura --- src/tests/util/CMakeLists.txt | 3 + src/tests/util/sequence.cpp | 33 +++++++++ src/util/sequence.h | 127 ++++++++++++++++++++++++++++++++++ 3 files changed, 163 insertions(+) create mode 100644 src/tests/util/sequence.cpp create mode 100644 src/util/sequence.h diff --git a/src/tests/util/CMakeLists.txt b/src/tests/util/CMakeLists.txt index 2676520183..cbc2c6754a 100644 --- a/src/tests/util/CMakeLists.txt +++ b/src/tests/util/CMakeLists.txt @@ -1,6 +1,9 @@ add_executable(name name.cpp) target_link_libraries(name "util" ${EXTRA_LIBS}) add_test(name ${CMAKE_CURRENT_BINARY_DIR}/name) +add_executable(sequence sequence.cpp) +target_link_libraries(sequence "util" ${EXTRA_LIBS}) +add_test(sequence ${CMAKE_CURRENT_BINARY_DIR}/sequence) add_executable(sexpr_tst sexpr.cpp) target_link_libraries(sexpr_tst "util" "numerics" "sexpr" ${EXTRA_LIBS}) add_test(sexpr ${CMAKE_CURRENT_BINARY_DIR}/sexpr_tst) diff --git a/src/tests/util/sequence.cpp b/src/tests/util/sequence.cpp new file mode 100644 index 0000000000..5af68bd45a --- /dev/null +++ b/src/tests/util/sequence.cpp @@ -0,0 +1,33 @@ +/* +Copyright (c) 2014 Microsoft Corporation. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. + +Author: Leonardo de Moura +*/ +#include "util/sequence.h" +#include "util/test.h" +using namespace lean; + +template class sequence; + +static void tst1() { + sequence l1; + lean_assert(!l1); + sequence l2(10); + lean_assert(l2); + lean_assert(is_eqp(l2, l1 + l2)); + lean_assert(is_eqp(l2, l2 + l1)); + lean_assert(!is_eqp(l2, l2 + l2)); + sequence l3(20); + sequence l4(5); + sequence r = l4 + (l2 + l2) + (l3 + l4) + sequence(3); + buffer b; + r.linearize(b); + for (auto v : b) std::cout << v << " "; std::cout << "\n"; + lean_assert(b[0] == 5 && b[1] == 10 && b[2] == 10 && b[3] == 20 && b[4] == 5 && b[5] == 3); +} + +int main() { + tst1(); + return has_violations() ? 1 : 0; +} diff --git a/src/util/sequence.h b/src/util/sequence.h new file mode 100644 index 0000000000..9a0e7ecc72 --- /dev/null +++ b/src/util/sequence.h @@ -0,0 +1,127 @@ +/* +Copyright (c) 2014 Microsoft Corporation. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. + +Author: Leonardo de Moura +*/ +#pragma once +#include "util/rc.h" +#include "util/debug.h" +#include "util/buffer.h" +#include "util/optional.h" +#include "util/memory_pool.h" + +namespace lean { +/** \brief Sequence datastructure with O(1) concatenation operation */ +template +class sequence { + struct cell { + bool m_join; + MK_LEAN_RC(); + void dealloc(); + cell(bool join):m_join(join), m_rc(1) {} + }; + + struct elem_cell : public cell { + T m_value; + elem_cell(T const & v):cell(false), m_value(v) {} + }; + + struct node { + cell * m_ptr; + node():m_ptr(nullptr) {} + explicit node(T const & v); + node(node const & s):m_ptr(s.m_ptr) { if (m_ptr) m_ptr->inc_ref(); } + node(node && s):m_ptr(s.m_ptr) { s.m_ptr = nullptr; } + node(node const & f, node const & s); + ~node() { if (m_ptr) m_ptr->dec_ref(); } + node & operator=(node const & s) { LEAN_COPY_REF(s); } + node & operator=(node && s) { LEAN_MOVE_REF(s); } + cell * raw() const { return m_ptr; } + explicit operator bool() const { return m_ptr != nullptr; } + }; + + struct join_cell : public cell { + node m_first; + node m_second; + join_cell(node const & f, node const & s):cell(true), m_first(f), m_second(s) {} + }; + + typedef memory_pool elem_cell_allocator; + typedef memory_pool join_cell_allocator; + static elem_cell_allocator & get_elem_cell_allocator() { + LEAN_THREAD_PTR(elem_cell_allocator) g_allocator; + if (!g_allocator.get()) + g_allocator.reset(new elem_cell_allocator()); + return *g_allocator; + } + + static join_cell_allocator & get_join_cell_allocator() { + LEAN_THREAD_PTR(join_cell_allocator) g_allocator; + if (!g_allocator.get()) + g_allocator.reset(new join_cell_allocator()); + return *g_allocator; + } +private: + node m_node; +public: + sequence() {} + explicit sequence(T const & v):m_node(v) {} + sequence(sequence const & f, sequence const & s):m_node(f.m_node, s.m_node) {} + + /** \brief Return true iff it is not the empty/nil sequence. */ + explicit operator bool() const { return m_node.raw() != nullptr; } + + /** \brief Pointer equality. Return true iff \c s1 and \c s2 point to the same memory location. */ + friend bool is_eqp(sequence const & s1, sequence const & s2) { return s1.m_node.raw() == s2.m_node.raw(); } + + friend sequence operator+(sequence const & s1, sequence const & s2) { return sequence(s1, s2); } + + /** \brief Store sequence elements in \c r */ + void linearize(buffer & r) const { + buffer todo; + if (m_node) todo.push_back(m_node.raw()); + while (!todo.empty()) { + cell const * c = todo.back(); + todo.pop_back(); + if (c->m_join) { + todo.push_back(static_cast(c)->m_second.raw()); + todo.push_back(static_cast(c)->m_first.raw()); + } else { + r.push_back(static_cast(c)->m_value); + } + } + } +}; + +template +void sequence::cell::dealloc() { + if (m_join) { + join_cell * c = static_cast(this); + c->~join_cell(); + get_join_cell_allocator().recycle(c); + } else { + elem_cell * c = static_cast(this); + c->~elem_cell(); + get_elem_cell_allocator().recycle(c); + } +} + +template +sequence::node::node(T const & v):m_ptr(new (get_elem_cell_allocator().allocate()) elem_cell(v)) {} + +template +sequence::node::node(node const & f, node const & s) { + if (f && s) { + m_ptr = new (get_join_cell_allocator().allocate()) join_cell(f, s); + } else if (f) { + m_ptr = f.m_ptr; + m_ptr->inc_ref(); + } else if (s) { + m_ptr = s.m_ptr; + m_ptr->inc_ref(); + } else { + m_ptr = nullptr; + } +} +}