From 37498f9fb8d73a279bca460e120ce79c204ce5b0 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Wed, 11 Sep 2013 13:48:49 -0700 Subject: [PATCH] Add persistent queues Signed-off-by: Leonardo de Moura --- src/tests/util/CMakeLists.txt | 3 + src/tests/util/list.cpp | 3 +- src/tests/util/queue.cpp | 130 ++++++++++++++++++++++++++++++++++ src/util/queue.h | 127 +++++++++++++++++++++++++++++++++ 4 files changed, 261 insertions(+), 2 deletions(-) create mode 100644 src/tests/util/queue.cpp create mode 100644 src/util/queue.h diff --git a/src/tests/util/CMakeLists.txt b/src/tests/util/CMakeLists.txt index 470dec0fa..0c763b2f8 100644 --- a/src/tests/util/CMakeLists.txt +++ b/src/tests/util/CMakeLists.txt @@ -25,3 +25,6 @@ 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) diff --git a/src/tests/util/list.cpp b/src/tests/util/list.cpp index 95de1cd4a..0fc938943 100644 --- a/src/tests/util/list.cpp +++ b/src/tests/util/list.cpp @@ -71,8 +71,7 @@ static void tst5() { auto p = split(l); list l2 = append(p.first, p.second); lean_assert(l2 == l); - int diff = static_cast(length(p.first)) - static_cast(length(p.second)); - lean_assert(-1 <= diff && diff <= 1); + lean_assert(-1 <= static_cast(length(p.first)) - static_cast(length(p.second)) && static_cast(length(p.first)) - static_cast(length(p.second)) <= 1); } } diff --git a/src/tests/util/queue.cpp b/src/tests/util/queue.cpp new file mode 100644 index 000000000..b2ebba3b0 --- /dev/null +++ b/src/tests/util/queue.cpp @@ -0,0 +1,130 @@ +/* +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); +} + +int main() { + tst1(); + tst2(); + tst3(); + return has_violations() ? 1 : 0; +} diff --git a/src/util/queue.h b/src/util/queue.h new file mode 100644 index 000000000..025f3aac7 --- /dev/null +++ b/src/util/queue.h @@ -0,0 +1,127 @@ +/* +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 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(q.m_rear); + p.second = reverse(p.second); + 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 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(q.m_front); + p.second = reverse(p.second); + 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; +} +}