From 55ff49d2d5634810af4c3ec16502ab7bab839a49 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Thu, 12 Sep 2013 10:09:54 -0700 Subject: [PATCH] Replace queue.h with pdeque.h Signed-off-by: Leonardo de Moura --- src/tests/util/CMakeLists.txt | 6 +- src/tests/util/pdeque.cpp | 223 ++++++++++++++ src/tests/util/queue.cpp | 210 ------------- src/util/pdeque.h | 550 ++++++++++++++++++++++++++++++++++ src/util/queue.h | 125 -------- 5 files changed, 776 insertions(+), 338 deletions(-) create mode 100644 src/tests/util/pdeque.cpp delete mode 100644 src/tests/util/queue.cpp create mode 100644 src/util/pdeque.h delete mode 100644 src/util/queue.h diff --git a/src/tests/util/CMakeLists.txt b/src/tests/util/CMakeLists.txt index 94db8d5bb..28b3e5038 100644 --- a/src/tests/util/CMakeLists.txt +++ b/src/tests/util/CMakeLists.txt @@ -25,9 +25,9 @@ add_test(scoped_map ${CMAKE_CURRENT_BINARY_DIR}/scoped_map) add_executable(thread thread.cpp) target_link_libraries(thread ${EXTRA_LIBS}) add_test(thread ${CMAKE_CURRENT_BINARY_DIR}/thread) -add_executable(queue queue.cpp) -target_link_libraries(queue ${EXTRA_LIBS}) -add_test(queue ${CMAKE_CURRENT_BINARY_DIR}/queue) +add_executable(pdeque pdeque.cpp) +target_link_libraries(pdeque ${EXTRA_LIBS}) +add_test(pdeque ${CMAKE_CURRENT_BINARY_DIR}/pdeque) add_executable(pvector pvector.cpp) target_link_libraries(pvector ${EXTRA_LIBS}) add_test(pvector ${CMAKE_CURRENT_BINARY_DIR}/pvector) diff --git a/src/tests/util/pdeque.cpp b/src/tests/util/pdeque.cpp new file mode 100644 index 000000000..073ffa247 --- /dev/null +++ b/src/tests/util/pdeque.cpp @@ -0,0 +1,223 @@ +/* +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 +#include +#include +#include +#include "test.h" +#include "pdeque.h" +using namespace lean; + +// #define PDEQUE_PERF_TEST + +/** + \brief Naive equality test for debugging +*/ +template +bool operator==(pdeque const & q1, pdeque const & q2) { + if (q1.size() != q2.size()) + return false; + for (unsigned i = 0; i < q1.size(); i++) { + if (q1[i] != q2[i]) + return false; + } + return true; +} + + +template +bool operator==(pdeque const & q1, std::deque const & q2) { + if (q1.size() != q2.size()) + return false; + for (unsigned i = 0; i < q1.size(); i++) { + if (q1[i] != q2[i]) + return false; + } + return true; +} + +static void tst1() { + pdeque q; + lean_assert(empty(q)); + lean_assert(size(q) == 0); + q = push_back(q, 1); + lean_assert(size(q) == 1); + std::cout << "q: " << q << "\n"; + lean_assert(front(q) == 1); + lean_assert(back(q) == 1); + lean_assert(!empty(q)); + q = push_back(q, 2); + lean_assert(front(q) == 1); + lean_assert(back(q) == 2); + std::cout << "q: " << q << "\n"; + q = push_front(q, 3); + std::cout << "q: " << q << "\n"; + lean_assert(size(q) == 3); + lean_assert(front(q) == 3); + lean_assert(back(q) == 2); + lean_assert(size(pop_front(q)) == 2); + lean_assert(front(pop_front(q)) == 1); + lean_assert(front(pop_front(pop_front(q))) == 2); + lean_assert(empty(pop_front(pop_front(pop_front(q))))); + lean_assert(pop_front(push_front(q, 3)) == q); + lean_assert(pop_back(push_back(q, 3)) == q); +} + +static void driver(unsigned max_sz, unsigned max_val, unsigned num_ops, double push_freq, double copy_freq) { + std::deque q1; + pdeque q2; + pdeque q3; + std::vector> copies; + for (unsigned i = 0; i < num_ops; i++) { + double f = static_cast(std::rand() % 10000) / 10000.0; + if (f < copy_freq) + copies.push_back(q3); + f = static_cast(std::rand() % 10000) / 10000.0; + if (f < push_freq) { + if (q1.size() >= max_sz) + continue; + int v = std::rand() % max_val; + if (std::rand() % 2 == 0) { + q1.push_front(v); + q2 = push_front(q2, v); + q3.push_front(v); + } else { + q1.push_back(v); + q2 = push_back(q2, v); + q3.push_back(v); + } + } else { + if (q1.size() == 0) + continue; + if (std::rand() % 2 == 0) { + lean_assert(front(q2) == q1.front()); + lean_assert(front(q3) == q1.front()); + q1.pop_front(); + q2 = pop_front(q2); + q3.pop_front(); + } else { + lean_assert(back(q2) == q1.back()); + lean_assert(back(q3) == q1.back()); + q1.pop_back(); + q2 = pop_back(q2); + q3.pop_back(); + } + } + lean_assert(q2 == q1); + lean_assert(q3 == q1); + } + std::cout << "Copies created: " << copies.size() << "\n"; +} + +static void tst2() { + driver(4, 32, 10000, 0.5, 0.01); + driver(4, 32, 10000, 0.5, 0.3); + driver(2, 32, 10000, 0.8, 0.5); + driver(2, 32, 10000, 0.3, 0.01); + driver(4, 32, 10000, 0.3, 0.5); + driver(16, 32, 10000, 0.5, 0.1); + driver(16, 32, 10000, 0.5, 0.01); + driver(16, 32, 10000, 0.5, 0.5); + driver(16, 32, 10000, 0.7, 0.1); + driver(16, 32, 10000, 0.7, 0.5); + driver(16, 32, 10000, 0.7, 0.01); + driver(16, 32, 10000, 0.1, 0.1); + driver(16, 32, 10000, 0.8, 0.1); + driver(16, 32, 10000, 0.8, 0.3); + driver(16, 1000, 10000, 0.8, 0.01); + driver(16, 1000, 10000, 0.8, 0.0); + driver(16, 1000, 10000, 0.8, 0.5); + driver(16, 1000, 10000, 0.8, 0.1); + driver(128, 1000, 10000, 0.5, 0.01); + driver(128, 1000, 10000, 0.5, 0.1); + driver(128, 1000, 10000, 0.5, 0.5); + driver(128, 1000, 10000, 0.2, 0.1); +} + +#ifdef PDEQUE_PERF_TEST +#include "timeit.h" + +static void perf_deque(unsigned n) { + std::deque q; + for (unsigned i = 0; i < n; i++) { + q.push_back(i); + } + for (unsigned i = 0; i < n; i++) { + q.pop_front(); + } +} + +static void perf_pdeque(unsigned n) { + pdeque q; + for (unsigned i = 0; i < n; i++) { + q.push_back(i); + } + for (unsigned i = 0; i < n; i++) { + q.pop_front(); + } +} + +static void tst4() { + unsigned N = 100000; + unsigned M = 100; + { + timeit t(std::cout, "deque time"); + for (unsigned i = 0; i < N; i++) perf_deque(M); + } + { + timeit t(std::cout, "pdeque time"); + for (unsigned i = 0; i < N; i++) perf_pdeque(M); + } +} + + +static void perf_deque2(std::deque q, unsigned n) { + for (unsigned i = 0; i < n; i++) { + q.push_back(i); + } + for (unsigned i = 0; i < n; i++) { + q.pop_front(); + } +} + +static void perf_pdeque2(pdeque q, unsigned n) { + for (unsigned i = 0; i < n; i++) { + q.push_back(i); + } + for (unsigned i = 0; i < n; i++) { + q.pop_front(); + } +} + +static void tst5() { + unsigned N = 100000; + unsigned SZ1 = 10000; + unsigned M = 5; + { + timeit t(std::cout, "deque time"); + std::deque q; + for (unsigned i = 0; i < SZ1; i++) { q.push_back(i); } + for (unsigned i = 0; i < N; i++) perf_deque2(q, M); + } + { + timeit t(std::cout, "pdeque time"); + pdeque q; + for (unsigned i = 0; i < SZ1 + 1; i++) { q.push_back(i); } + for (unsigned i = 0; i < N; i++) perf_pdeque2(q, M); + } +} +#endif + +int main() { + tst1(); + tst2(); +#ifdef PDEQUE_PERF_TEST + tst4(); + tst5(); +#endif + return has_violations() ? 1 : 0; +} diff --git a/src/tests/util/queue.cpp b/src/tests/util/queue.cpp deleted file mode 100644 index f52aa6904..000000000 --- a/src/tests/util/queue.cpp +++ /dev/null @@ -1,210 +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 -#include -#include "test.h" -#include "queue.h" -using namespace lean; - -/** - \brief Naive equality test for debugging -*/ -template -bool operator==(queue q1, queue q2) { - while (!is_empty(q1) && !is_empty(q2)) { - auto p1 = pop_front(q1); - auto p2 = pop_front(q2); - if (p1.second != p2.second) - return false; - q1 = p1.first; - q2 = p2.first; - } - return is_empty(q1) && is_empty(q2); -} - - -template -bool operator==(queue q1, std::deque const & q2) { - for (auto v : q2) { - if (is_empty(q1)) - return false; - auto p = pop_front(q1); - if (p.second != v) - return false; - q1 = p.first; - } - return is_empty(q1); -} - -static void tst1() { - queue q; - lean_assert(is_empty(q)); - q = push_back(q, 1); - lean_assert(pop_front(q).second == 1); - lean_assert(pop_back(q).second == 1); - lean_assert(!is_empty(q)); - q = push_back(q, 2); - q = push_front(q, 3); - lean_assert(size(q) == 3); - lean_assert(pop_front(q).second == 3); - lean_assert(pop_back(q).second == 2); - lean_assert(pop_front(q).first.size() == 2); - std::cout << "q: " << q << "\n"; - std::cout << "pop_front(q): " << pop_front(q).first << "\n"; - lean_assert(pop_front(pop_front(q).first).second == 1); - lean_assert(pop_front(pop_front(pop_front(q).first).first).second == 2); - lean_assert(pop_front(pop_front(pop_front(q).first).first).first.is_empty()); - lean_assert(pop_front(push_front(q, 3)).first == q); - lean_assert(pop_back(push_back(q, 3)).first == q); -} - -static void driver(unsigned max_sz, unsigned max_val, unsigned num_ops, double push_freq) { - std::deque q1; - queue q2; - for (unsigned i = 0; i < num_ops; i++) { - double f = static_cast(std::rand() % 10000) / 10000.0; - if (f < push_freq) { - if (q1.size() >= max_sz) - continue; - int v = std::rand() % max_val; - if (std::rand() % 2 == 0) { - q1.push_front(v); - lean_assert(pop_front(push_front(q2, v)).first == q2); - q2 = push_front(q2, v); - } else { - q1.push_back(v); - lean_assert(pop_back(push_back(q2, v)).first == q2); - q2 = push_back(q2, v); - } - } else { - if (q1.size() == 0) - continue; - if (std::rand() % 2 == 0) { - auto p = pop_front(q2); - lean_assert(p.second == q1.front()); - q1.pop_front(); - q2 = p.first; - } else { - auto p = pop_back(q2); - lean_assert(p.second == q1.back()); - q1.pop_back(); - q2 = p.first; - } - } - lean_assert(q2 == q1); - } -} - -static void tst2() { - driver(4, 32, 10000, 0.5); - driver(2, 32, 10000, 0.8); - driver(2, 32, 10000, 0.3); - driver(4, 32, 10000, 0.3); - driver(16, 32, 10000, 0.5); - driver(16, 32, 10000, 0.7); - driver(16, 32, 10000, 0.1); - driver(16, 32, 10000, 0.8); - driver(16, 1000, 10000, 0.8); - driver(128, 1000, 10000, 0.5); - driver(128, 1000, 10000, 0.2); -} - -static void tst3() { - queue q{1, 2, 3, 4}; - lean_assert(size(q) == 4); - lean_assert(pop_back(q).second == 4); - lean_assert(pop_front(q).second == 1); - lean_assert(pop_front(pop_front(q).first).second == 2); - lean_assert(pop_back(pop_back(q).first).second == 3); -} - -// #define QUEUE_PERF_TEST -#ifdef QUEUE_PERF_TEST -#include "timeit.h" - -static void perf_deque(unsigned n) { - std::deque q; - for (unsigned i = 0; i < n; i++) { - q.push_back(i); - } - for (unsigned i = 0; i < n; i++) { - q.pop_front(); - } -} - -static void perf_queue(unsigned n) { - queue q; - for (unsigned i = 0; i < n; i++) { - q = push_back(q, i); - } - for (unsigned i = 0; i < n; i++) { - q = pop_front(q).first; - } -} - -static void tst4() { - unsigned N = 100000; - unsigned M = 100; - { - timeit t(std::cout, "deque time"); - for (unsigned i = 0; i < N; i++) perf_deque(M); - } - { - timeit t(std::cout, "queue time"); - for (unsigned i = 0; i < N; i++) perf_queue(M); - } -} - - -static void perf_deque2(std::deque q, unsigned n) { - for (unsigned i = 0; i < n; i++) { - q.push_back(i); - } - for (unsigned i = 0; i < n; i++) { - q.pop_front(); - } -} - -static void perf_queue2(queue q, unsigned n) { - for (unsigned i = 0; i < n; i++) { - q = push_back(q, i); - } - for (unsigned i = 0; i < n; i++) { - q = pop_front(q).first; - } -} - -static void tst5() { - unsigned N = 100000; - unsigned SZ1 = 10000; - unsigned M = 5; - { - timeit t(std::cout, "deque time"); - std::deque q; - for (unsigned i = 0; i < SZ1; i++) { q.push_back(i); } - for (unsigned i = 0; i < N; i++) perf_deque2(q, M); - } - { - timeit t(std::cout, "queue time"); - queue q; - for (unsigned i = 0; i < SZ1 + 1; i++) { q = push_back(q, i); } - q = pop_front(q).first; - for (unsigned i = 0; i < N; i++) perf_queue2(q, M); - } -} -#endif - -int main() { - tst1(); - tst2(); - tst3(); -#ifdef QUEUE_PERF_TEST - tst4(); - tst5(); -#endif - return has_violations() ? 1 : 0; -} diff --git a/src/util/pdeque.h b/src/util/pdeque.h new file mode 100644 index 000000000..a91dcfa07 --- /dev/null +++ b/src/util/pdeque.h @@ -0,0 +1,550 @@ +/* +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 +#include +#include "rc.h" + +#ifndef LEAN_PDEQUE_MIN_QUOTA +#define LEAN_PDEQUE_MIN_QUOTA 16 +#endif + +namespace lean { +/** + \brief Deque with O(1) copy operation. + We call it pdeque because it can be used to simulate persistent deques. + + \remark This class uses the same "trick" used to implement pvector. +*/ +template +class pdeque { + enum class cell_kind { PushBack, PopBack, PushFront, PopFront, Set, Root }; + + /** + \brief Base class for representing the data. + We have two kinds of data: delta and root (the actual deque). + The deltas store changes to shared deques. + */ + struct cell { + cell_kind m_kind; + MK_LEAN_RC(); + cell(cell_kind k):m_kind(k), m_rc(0) {} + cell(cell const & c):m_kind(c.m_kind), m_rc(0) {} + void dealloc(); + unsigned size() const; + /** + \brief Return the quota for a cell. When the quota of cell reaches 0, then we perform a deep copy. + */ + unsigned quota() const; + cell_kind kind() const { return m_kind; } + }; + + /** + \brief Cell for wrapping std::deque + */ + struct root_cell : public cell { + std::deque m_deque; + root_cell():cell(cell_kind::Root) {} + }; + + /** + \brief Base class for storing non-destructive updates: Push, Pop, Set. + \remark We can view delta_cell's as delayed operations. + */ + struct delta_cell : public cell { + unsigned m_size; + unsigned m_quota; + cell * m_prev; + delta_cell(cell_kind k, unsigned sz, cell * prev):cell(k), m_size(sz), m_quota(prev->quota() - 1), m_prev(prev) { + lean_assert(m_prev); + m_prev->inc_ref(); + } + delta_cell(delta_cell const & c):cell(c), m_size(c.m_size), m_quota(c.m_quota), m_prev(c.m_prev) { + lean_assert(m_prev); + m_prev->inc_ref(); + } + ~delta_cell() { lean_assert(m_prev); m_prev->dec_ref(); } + }; + + /** + \brief Cell for representing the deque obtained by removing the last element from + the deque represented by \c prev. + */ + struct pop_back_cell : public delta_cell { + pop_back_cell(cell * prev):delta_cell(cell_kind::PopBack, prev->size() - 1, prev) {} + pop_back_cell(pop_back_cell const & c):delta_cell(c) {} + }; + + /** + \brief Cell for representing the deque obtained by removing the first element from + the deque represented by \c prev. + */ + struct pop_front_cell : public delta_cell { + pop_front_cell(cell * prev):delta_cell(cell_kind::PopFront, prev->size() - 1, prev) {} + pop_front_cell(pop_front_cell const & c):delta_cell(c) {} + }; + + /** + \brief Cell for representing the deque obtained by adding \c v + to the end of the queue represented by \c prev. + */ + struct push_back_cell : public delta_cell { + T m_val; + push_back_cell(T const & v, cell * prev):delta_cell(cell_kind::PushBack, prev->size() + 1, prev), m_val(v) {} + push_back_cell(push_back_cell const & c):delta_cell(c), m_val(c.m_val) {} + }; + + /** + \brief Cell for representing the deque obtained by adding \c v + to the beginning of the queue represented by \c prev. + */ + struct push_front_cell : public delta_cell { + T m_val; + push_front_cell(T const & v, cell * prev):delta_cell(cell_kind::PushFront, prev->size() + 1, prev), m_val(v) {} + push_front_cell(push_front_cell const & c):delta_cell(c), m_val(c.m_val) {} + }; + + /** + \brief Cell for representing the deque obtained by updating position \c i with value \c v + in the the deque represented by \c prev. + */ + struct set_cell : public delta_cell { + unsigned m_idx; + T m_val; + set_cell(unsigned i, T const & v, cell * prev):delta_cell(cell_kind::Set, prev->size(), prev), m_idx(i), m_val(v) {} + set_cell(set_cell const & c):delta_cell(c), m_idx(c.m_idx), m_val(c.m_val) {} + }; + + static push_back_cell & to_push_back(cell * c) { lean_assert(c->kind() == cell_kind::PushBack); return *static_cast(c); } + static push_back_cell const & to_push_back(cell const * c) { lean_assert(c->kind() == cell_kind::PushBack); return *static_cast(c); } + static push_front_cell & to_push_front(cell * c) { lean_assert(c->kind() == cell_kind::PushFront); return *static_cast(c); } + static push_front_cell const & to_push_front(cell const * c) { lean_assert(c->kind() == cell_kind::PushFront); return *static_cast(c); } + static pop_back_cell & to_pop_back(cell * c) { lean_assert(c->kind() == cell_kind::PopBack); return *static_cast(c); } + static pop_back_cell const & to_pop_back(cell const * c) { lean_assert(c->kind() == cell_kind::PopBack); return *static_cast(c); } + static pop_front_cell & to_pop_front(cell * c) { lean_assert(c->kind() == cell_kind::PopFront); return *static_cast(c); } + static pop_front_cell const & to_pop_front(cell const * c) { lean_assert(c->kind() == cell_kind::PopFront); return *static_cast(c); } + static set_cell & to_set(cell * c) { lean_assert(c->kind() == cell_kind::Set); return *static_cast(c); } + static set_cell const & to_set(cell const * c) { lean_assert(c->kind() == cell_kind::Set); return *static_cast(c); } + static root_cell & to_root(cell * c) { lean_assert(c->kind() == cell_kind::Root); return *static_cast(c); } + static root_cell const & to_root(cell const * c) { lean_assert(c->kind() == cell_kind::Root); return *static_cast(c); } + + cell * m_ptr; + pdeque(cell * d):m_ptr(d) { lean_assert(m_ptr); m_ptr->inc_ref(); } + + /** \brief Return true iff the cell associated with this deque is shared */ + bool is_shared() const { return m_ptr->get_rc() > 1; } + + /** \brief Update the cell (and reference counters) of this deque */ + void update_cell(cell * new_cell) { + lean_assert(new_cell); + lean_assert(m_ptr); + new_cell->inc_ref(); + m_ptr->dec_ref(); + m_ptr = new_cell; + } + + /** + \brief Auxiliary method for \c flat + Given an empty deque \c r, then flat_core(c, r) will + store in r the deque represented by cell \c c. + That is, the deque obtained after finding the root cell (aka wrapper for std::deque), + and applying all deltas. + */ + static void flat_core(cell * c, std::deque & r) { + lean_assert(r.empty()); + switch(c->kind()) { + case cell_kind::PushBack: + flat_core(to_push_back(c).m_prev, r); + r.push_back(to_push_back(c).m_val); + break; + case cell_kind::PushFront: + flat_core(to_push_front(c).m_prev, r); + r.push_front(to_push_front(c).m_val); + break; + case cell_kind::PopBack: + flat_core(to_pop_back(c).m_prev, r); + r.pop_back(); + break; + case cell_kind::PopFront: + flat_core(to_pop_front(c).m_prev, r); + r.pop_front(); + break; + case cell_kind::Set: + flat_core(to_set(c).m_prev, r); + r[to_set(c).m_idx] = to_set(c).m_val; + break; + case cell_kind::Root: + r = to_root(c).m_deque; + break; + } + } + + /** + \brief Change the representation to a root cell. + */ + void flat() { + lean_assert(m_ptr->kind() != cell_kind::Root); + std::deque r; + flat_core(m_ptr, r); + update_cell(new root_cell()); + to_root(m_ptr).m_deque.swap(r); + lean_assert(!is_shared()); + } + + /** + \brief If the quota associated with m_cell is zero, then + compute a flat representation. That is, represent the deque + using a single root_cell. + */ + void flat_if_needed() { + lean_assert(m_ptr->kind() != cell_kind::Root); + if (static_cast(m_ptr)->m_quota == 0) { + flat(); + } + } + + /** + \brief Update quota based on the cost of a read + Return true if the quota was updated, and false + if the representation had to be updated. + */ + bool update_quota_on_read(unsigned cost) { + cost /= 2; // reads are cheaper than writes + if (cost > 0) { + if (cost >= m_ptr->quota()) { + flat(); + return false; + } else { + if (is_shared()) { + switch (m_ptr->kind()) { + case cell_kind::PushBack: update_cell(new push_back_cell(to_push_back(m_ptr))); break; + case cell_kind::PushFront: update_cell(new push_front_cell(to_push_front(m_ptr))); break; + case cell_kind::PopBack: update_cell(new pop_back_cell(to_pop_back(m_ptr))); break; + case cell_kind::PopFront: update_cell(new pop_front_cell(to_pop_front(m_ptr))); break; + case cell_kind::Set: update_cell(new set_cell(to_set(m_ptr))); break; + case cell_kind::Root: lean_unreachable(); break; + } + } + lean_assert(!is_shared()); + lean_assert(static_cast(m_ptr)->m_quota > cost); + static_cast(m_ptr)->m_quota -= cost; + } + } + return true; + } + + void pop_back_core() { update_cell(new pop_back_cell(m_ptr)); } + void pop_front_core() { update_cell(new pop_front_cell(m_ptr)); } + void push_back_core(T const & v) { update_cell(new push_back_cell(v, m_ptr)); } + void push_front_core(T const & v) { update_cell(new push_front_cell(v, m_ptr)); } + void set_core(unsigned i, T const & v) { update_cell(new set_cell(i, v, m_ptr)); } + + bool is_root() const { return m_ptr->kind() == cell_kind::Root; } + +public: + pdeque():m_ptr(new root_cell()) { m_ptr->inc_ref(); } + pdeque(pdeque const & s):m_ptr(s.m_ptr) { m_ptr->inc_ref(); } + pdeque(pdeque && s):m_ptr(s.m_ptr) { s.m_ptr = nullptr; } + ~pdeque() { if (m_ptr) m_ptr->dec_ref(); } + + pdeque & operator=(pdeque const & s) { LEAN_COPY_REF(pdeque, s); } + pdeque & operator=(pdeque && s) { LEAN_MOVE_REF(pdeque, s); } + + /** \brief Return the number of elements */ + unsigned size() const { return m_ptr->size(); } + + /** \brief Check whether the container is empty */ + bool empty() const { return size() == 0; } + + /** + \brief Access specified element + \pre i < size() + */ + T const & operator[](unsigned i) const { + lean_assert(i < size()); + cell const * it = m_ptr; + unsigned input_i = i; + unsigned cost = 0; + while (true) { + switch (it->kind()) { + case cell_kind::PushBack: + if (i + 1 == to_push_back(it).m_size) { + if (const_cast(this)->update_quota_on_read(cost)) + return to_push_back(it).m_val; + else + return operator[](input_i); // representation was updated + } + break; + case cell_kind::PushFront: + if (i == 0) { + if (const_cast(this)->update_quota_on_read(cost)) + return to_push_front(it).m_val; + else + return operator[](input_i); // representation was updated + } else { + i--; + } + break; + case cell_kind::PopBack: + break; + case cell_kind::PopFront: + i++; + break; + case cell_kind::Set: + if (to_set(it).m_idx == i) { + if (const_cast(this)->update_quota_on_read(cost)) + return to_set(it).m_val; + else + return operator[](input_i); // representation was updated + } + break; + case cell_kind::Root: + if (const_cast(this)->update_quota_on_read(cost)) + return to_root(it).m_deque[i]; + else + return operator[](input_i); // representation was updated + } + it = static_cast(it)->m_prev; + cost++; + } + } + + /** + \brief Return the last element in the deque + \pre !empty() + */ + T const & back() const { + lean_assert(!empty()); + return operator[](size() - 1); + } + + /** + \brief Return the first element in the deque + \pre !empty() + */ + T const & front() const { + lean_assert(!empty()); + return operator[](0); + } + + /** + \brief Add an element to the end of the deque + */ + void push_back(T const & v) { + if (!is_root()) + flat_if_needed(); + switch (m_ptr->kind()) { + case cell_kind::PushBack: case cell_kind::PushFront: case cell_kind::PopBack: + case cell_kind::PopFront: case cell_kind::Set: + push_back_core(v); + break; + case cell_kind::Root: + if (!is_shared()) + to_root(m_ptr).m_deque.push_back(v); + else + push_back_core(v); + break; + } + } + + /** + \brief Add an element in the beginning of the deque + */ + void push_front(T const & v) { + if (!is_root()) + flat_if_needed(); + switch (m_ptr->kind()) { + case cell_kind::PushBack: case cell_kind::PushFront: case cell_kind::PopBack: + case cell_kind::PopFront: case cell_kind::Set: + push_front_core(v); + break; + case cell_kind::Root: + if (!is_shared()) + to_root(m_ptr).m_deque.push_front(v); + else + push_front_core(v); + break; + } + } + + /** + \brief Remove the last element + \pre !empty() + */ + void pop_back() { + lean_assert(!empty()); + if (!is_root()) + flat_if_needed(); + switch (m_ptr->kind()) { + case cell_kind::PushBack: + update_cell(to_push_back(m_ptr).m_prev); + break; + case cell_kind::PushFront: case cell_kind::PopBack: + case cell_kind::PopFront: case cell_kind::Set: + pop_back_core(); + break; + case cell_kind::Root: + if (!is_shared()) + to_root(m_ptr).m_deque.pop_back(); + else + pop_back_core(); + break; + } + } + + /** + \brief Remove the first element + \pre !empty() + */ + void pop_front() { + lean_assert(!empty()); + if (!is_root()) + flat_if_needed(); + switch (m_ptr->kind()) { + case cell_kind::PushFront: + update_cell(to_push_front(m_ptr).m_prev); + break; + case cell_kind::PushBack: case cell_kind::PopBack: + case cell_kind::PopFront: case cell_kind::Set: + pop_front_core(); + break; + case cell_kind::Root: + if (!is_shared()) + to_root(m_ptr).m_deque.pop_front(); + else + pop_front_core(); + break; + } + } + + /** + \brief Update position \c i with value \c v + \pre i < size() + */ + void set(unsigned i, T const & v) { + lean_assert(i < size()); + if (!is_root()) + flat_if_needed(); + switch (m_ptr->kind()) { + case cell_kind::PushBack: + case cell_kind::PopBack: + set_core(i, v); + break; + case cell_kind::Set: + if (!is_shared() && i == to_set(m_ptr).m_idx) + to_set(m_ptr).m_val = v; + else + set_core(i, v); + break; + case cell_kind::Root: + if (!is_shared()) + to_root(m_ptr).m_deque[i] = v; + else + set_core(i, v); + break; + } + } + + class iterator { + friend class pdeque; + pdeque const & m_deque; + unsigned m_it; + iterator(pdeque const & v, unsigned it):m_deque(v), m_it(it) {} + public: + iterator(iterator const & s):m_deque(s.m_deque), m_it(s.m_it) {} + iterator & operator++() { ++m_it; return *this; } + iterator operator++(int) { iterator tmp(*this); operator++(); return tmp; } + bool operator==(iterator const & s) const { lean_assert(&m_deque == &(s.m_deque)); return m_it == s.m_it; } + bool operator!=(iterator const & s) const { return !operator==(s); } + T const & operator*() const { return m_deque[m_it]; } + T const * operator->() const { return &(m_deque[m_it]); } + }; + + /** \brief Return an iterator to the beginning */ + iterator begin() const { return iterator(*this, 0); } + /** \brief Return an iterator to the end */ + iterator end() const { return iterator(*this, size()); } +}; + +template +void pdeque::cell::dealloc() { + switch (kind()) { + case cell_kind::PushBack: delete static_cast(this); break; + case cell_kind::PushFront: delete static_cast(this); break; + case cell_kind::PopBack: delete static_cast(this); break; + case cell_kind::PopFront: delete static_cast(this); break; + case cell_kind::Set: delete static_cast(this); break; + case cell_kind::Root: delete static_cast(this); break; + } +} + +template +unsigned pdeque::cell::size() const { + if (kind() == cell_kind::Root) { + return static_cast(this)->m_deque.size(); + } else { + return static_cast(this)->m_size; + } +} + +template +unsigned pdeque::cell::quota() const { + if (kind() == cell_kind::Root) { + unsigned sz = size(); + if (sz < LEAN_PDEQUE_MIN_QUOTA) + return LEAN_PDEQUE_MIN_QUOTA; + else + return sz; + } else { + return static_cast(this)->m_quota; + } +} + +/** \brief Non-destructive push_back. It is simulated using O(1) copy. */ +template +pdeque push_back(pdeque const & s, T const & v) { pdeque r(s); r.push_back(v); return r; } +/** \brief Non-destructive push_front. It is simulated using O(1) copy. */ +template +pdeque push_front(pdeque const & s, T const & v) { pdeque r(s); r.push_front(v); return r; } +/** \brief Non-destructive pop_back. It is simulated using O(1) copy. */ +template +pdeque pop_back(pdeque const & s) { pdeque r(s); r.pop_back(); return r; } +/** \brief Non-destructive pop_front. It is simulated using O(1) copy. */ +template +pdeque pop_front(pdeque const & s) { pdeque r(s); r.pop_front(); return r; } +/** \brief Non-destructive set. It is simulated using O(1) copy. */ +template +pdeque set(pdeque const & s, unsigned i, T const & v) { pdeque r(s); r.set(i, v); return r; } +/** \brief Return the last element of \c s. */ +template +T const & back(pdeque const & s) { return s.back(); } +/** \brief Return the first element of \c s. */ +template +T const & front(pdeque const & s) { return s.front(); } +/** \brief Return true iff \c s is empty. */ +template +bool empty(pdeque const & s) { return s.empty(); } +/** \brief Return the size of s. */ +template +unsigned size(pdeque const & s) { return s.size(); } + +template inline std::ostream & operator<<(std::ostream & out, pdeque const & d) { + out << "["; + bool first = true; + auto it = d.begin(); + auto end = d.end(); + for (; it != end; ++it) { + if (first) + first = false; + else + out << " "; + out << *it; + } + out << "]"; + return out; +} +} diff --git a/src/util/queue.h b/src/util/queue.h deleted file mode 100644 index 761b662cb..000000000 --- a/src/util/queue.h +++ /dev/null @@ -1,125 +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 "list_fn.h" - -namespace lean { -/** - \brief Functional queue -*/ -template -class queue { - list m_front; - list m_rear; - queue(list const & f, list const & r):m_front(f), m_rear(r) {} -public: - queue() {} - queue(unsigned num, T const * as) { m_front = to_list(as, as + num); } - queue(std::initializer_list const & l):queue(l.size(), l.begin()) {} - - /** \brief Return true iff the list is empty (complexity O(1)) */ - bool is_empty() const { return is_nil(m_front) && is_nil(m_rear); } - - /** \brief Return the size of the queue (complexity O(n)) */ - unsigned size() const { return length(m_front) + length(m_rear); } - - /** \brief Return the queue (v :: q) (complexity O(1)) */ - friend queue push_front(queue const & q, T const & v) { return queue(cons(v, q.m_front), q.m_rear); } - - /** \brief Return the queue (q :: v) (complexity O(1)) */ - friend queue push_back(queue const & q, T const & v) { return queue(q.m_front, cons(v, q.m_rear)); } - - /** - \brief Return the pair (q, v) for a queue (v :: q). - Complexity: worst case is O(n), average O(1) - - \pre !is_empty(q) - */ - friend std::pair, T> pop_front(queue const & q) { - lean_assert(!q.is_empty()); - if (is_nil(q.m_front)) { - if (is_nil(cdr(q.m_rear))) { - return mk_pair(queue(), car(q.m_rear)); - } else { - auto p = split_reverse_second(q.m_rear); - return mk_pair(queue(cdr(p.second), p.first), car(p.second)); - } - } else { - return mk_pair(queue(cdr(q.m_front), q.m_rear), car(q.m_front)); - } - } - - /** - \brief Return the pair (q, v) for a queue (q :: v). - Complexity: worst case is O(n), average O(1) - - \pre !is_empty(q) - */ - friend std::pair, T> pop_back(queue const & q) { - lean_assert(!q.is_empty()); - if (is_nil(q.m_rear)) { - if (is_nil(cdr(q.m_front))) { - return mk_pair(queue(), car(q.m_front)); - } else { - auto p = split_reverse_second(q.m_front); - return mk_pair(queue(p.first, cdr(p.second)), car(p.second)); - } - } else { - return mk_pair(queue(q.m_front, cdr(q.m_rear)), car(q.m_rear)); - } - } - - class iterator { - typename list::iterator m_it; - queue const * m_queue; - iterator(typename list::iterator const & it, queue const * queue) {} - public: - iterator(iterator const & s):m_it(s.m_it), m_queue(s.m_queue) {} - iterator & operator++() { - ++m_it; - if (m_queue && m_it == m_queue->m_front.end()) { - m_it = m_queue->m_rear.begin(); - m_queue = nullptr; - } - return *this; - } - iterator operator++(int) { iterator tmp(*this); operator++(); return tmp; } - bool operator==(iterator const & s) const { return m_it == s.m_it; } - bool operator!=(iterator const & s) const { return !operator==(s); } - T const & operator*() { return m_it.operator*(); } - T const * operator->() { return m_it.operator->(); } - }; - - /** - \brief Return an iterator for the beginning of the queue. - The iterator traverses the queue in an arbitrary order. - */ - iterator begin() const { return iterator(m_front.begin(), this); } - iterator end() const { return iterator(m_rear.end(), nullptr); } -}; -/** \brief Return the size of \c q. */ -template unsigned size(queue const & q) { return q.size(); } -/** \brief Return true iff \c q is empty */ -template bool is_empty(queue const & q) { return q.is_empty(); } - -template inline std::ostream & operator<<(std::ostream & out, queue const & q) { - out << "["; - queue q2 = q; - bool first = true; - while(!is_empty(q2)) { - auto p = pop_front(q2); - if (first) - first = false; - else - out << " "; - out << p.second; - q2 = p.first; - } - out << "]"; - return out; -} -}