From df3280e86e8c8736946cf190bcc03f0bebb658bc Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Tue, 3 Jun 2014 13:24:27 -0700 Subject: [PATCH] feat(util): add lru cache Signed-off-by: Leonardo de Moura --- src/tests/util/CMakeLists.txt | 3 + src/tests/util/lru_cache.cpp | 56 ++++++++++++++ src/util/lru_cache.h | 140 ++++++++++++++++++++++++++++++++++ 3 files changed, 199 insertions(+) create mode 100644 src/tests/util/lru_cache.cpp create mode 100644 src/util/lru_cache.h diff --git a/src/tests/util/CMakeLists.txt b/src/tests/util/CMakeLists.txt index de168fdf7..6d95ea2b8 100644 --- a/src/tests/util/CMakeLists.txt +++ b/src/tests/util/CMakeLists.txt @@ -73,3 +73,6 @@ add_test(serializer ${CMAKE_CURRENT_BINARY_DIR}/serializer) add_executable(trie trie.cpp) target_link_libraries(trie ${EXTRA_LIBS}) add_test(trie ${CMAKE_CURRENT_BINARY_DIR}/trie) +add_executable(lru_cache lru_cache.cpp) +target_link_libraries(lru_cache ${EXTRA_LIBS}) +add_test(lru_cache ${CMAKE_CURRENT_BINARY_DIR}/lru_cache) diff --git a/src/tests/util/lru_cache.cpp b/src/tests/util/lru_cache.cpp new file mode 100644 index 000000000..a7a4a280c --- /dev/null +++ b/src/tests/util/lru_cache.cpp @@ -0,0 +1,56 @@ +/* +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/test.h" +#include "util/lru_cache.h" +using namespace lean; + +static void tst1(int C = 10000) { + lru_cache m_cache(C); + for (int i = 0; i < 2*C; i++) { + lean_verify(m_cache.insert(i) == nullptr); + } + for (int i = C; i < 2*C; i++) { + lean_verify(*m_cache.insert(i) == i); + } + lean_assert(m_cache.size() == static_cast(C)); + for (int i = 0; i < C; i++) { + lean_assert(!m_cache.contains(i)); + } + for (int i = C; i < 2*C; i++) { + lean_assert(m_cache.contains(i)); + } + m_cache.set_capacity(C/2); + lean_assert(m_cache.capacity() == static_cast(C/2)); + for (int i = C; i < C + C/2; i++) { + lean_assert(!m_cache.contains(i)); + } + for (int i = C + C/2; i < 2*C; i++) { + lean_assert(m_cache.contains(i)); + } + for (int i = C + C/2; i < 2*C; i++) { + lean_assert(*m_cache.find(i) == i); + m_cache.erase(i); + lean_assert(!m_cache.contains(i)); + } + lean_assert(m_cache.size() == 0); +} + +static void tst2() { + lru_cache m_cache(5); + for (int i = 0; i < 10; i++) { + m_cache.insert(i); + } + lean_assert(m_cache.size() == 5); + m_cache.clear(); + lean_assert(m_cache.empty()); +} + +int main() { + tst1(); + tst2(); + return has_violations() ? 1 : 0; +} diff --git a/src/util/lru_cache.h b/src/util/lru_cache.h new file mode 100644 index 000000000..b53945b51 --- /dev/null +++ b/src/util/lru_cache.h @@ -0,0 +1,140 @@ +/* +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 +#include +#include +#include "util/debug.h" + +namespace lean { +/** \brief Simple LRU cache on top of std::unordered_set */ +template, typename Eq = std::equal_to> +class lru_cache { + struct clist { + clist * m_prev; + clist * m_next; + + clist():m_prev(nullptr), m_next(nullptr) {} + clist(clist * p, clist * n):m_prev(p), m_next(n) {} + + void remove() { + m_prev->m_next = m_next; + m_next->m_prev = m_prev; + } + + void move_front(clist & head) { + remove(); + m_prev = &head; + m_next = head.m_next; + head.m_next->m_prev = this; + head.m_next = this; + } + }; + + struct entry : public clist { + Key m_key; + explicit entry(Key const & k):m_key(k) {} + entry(Key const & k, clist & head):clist(&head, head.m_next), m_key(k) { + head.m_next->m_prev = this; + head.m_next = this; + } + // Delete the copy and move constructors. + // So, we get a compilation error if std::unordered_set tries + // to copy entries. An entry object cannot be copied because + // the m_prev, and m_next will not be correct. + entry(entry && s) = delete; + entry(entry const & s) = delete; + }; + + struct entry_hash : private Hash { + entry_hash(Hash const & h):Hash(h) {} + std::size_t operator()(entry const & e) const { return Hash::operator()(e.m_key); } + }; + + struct entry_eq : private Eq { + entry_eq(Eq const & e):Eq(e) {} + bool operator()(entry const & e1, entry const & e2) const { + return Eq::operator()(e1.m_key, e2.m_key); + } + }; + + void remove_last() { + lean_assert(m_cache.size() > 0); + entry * last = static_cast(m_head.m_prev); + last->remove(); + m_cache.erase(entry(last->m_key)); + } + + unsigned m_capacity; + std::unordered_set m_cache; + clist m_head; +public: + lru_cache(unsigned c, Hash const & h = Hash(), Eq const & e = Eq()): + m_capacity(std::max(c, 1u)), m_cache(5, entry_hash(h), entry_eq(e)), m_head(&m_head, &m_head) { + } + + /** + \brief Insert key in the cache. + If the chache alreayd contains an equivalent key, then return a pointer to it. + Otherwise return nullptr. + */ + Key const * insert(Key const & k) { + auto it = m_cache.find(entry(k)); + if (it != m_cache.end()) { + const_cast(*it).move_front(m_head); + return &it->m_key; + } else { + // We must use emplace to instead of insert, to avoid the copy constructor. + m_cache.emplace(k, m_head); + if (m_cache.size() > m_capacity) + remove_last(); + return nullptr; + } + } + + /** + \brief If this cache contains a key equivalent to \c k, then return it. + Otherwise return nullptr. The key is moved to beginning of the queue. + */ + Key const * find(Key const & k) { + auto it = m_cache.find(entry(k)); + if (it != m_cache.end()) { + const_cast(*it).move_front(m_head); + return &it->m_key; + } else { + return nullptr; + } + } + + /** \brief Remove the given key from the cache. */ + void erase(Key const & k) { + auto it = m_cache.find(entry(k)); + if (it != m_cache.end()) { + const_cast(*it).remove(); + m_cache.erase(it); + } + } + + /** \brief Modify the capacity of this cache */ + void set_capacity(unsigned c) { + m_capacity = std::max(c, 1u); + while (m_cache.size() > m_capacity) + remove_last(); + } + + /** \brief Remove all elements. */ + void clear() { m_cache.clear(); } + /** \brief Return true iff the cache contains the given key. */ + bool contains(Key const & k) { return find(k); } + /** \brief Return the number of elements stored in the cache. */ + unsigned size() const { return m_cache.size(); } + /** \brief Return the capacity of this cache. */ + unsigned capacity() const { return m_capacity; } + /** \brief Return true iff the cache is empty. */ + bool empty() const { return size() == 0; } +}; +}