From 4c14668bf05d5fa063f9dac0411604d8d43ce033 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Thu, 12 Apr 2018 09:48:48 -0700 Subject: [PATCH] chore(util/lru_cache): remove dead code --- src/kernel/expr.cpp | 1 - src/tests/util/CMakeLists.txt | 3 - src/tests/util/lru_cache.cpp | 56 -------------- src/util/lru_cache.h | 140 ---------------------------------- 4 files changed, 200 deletions(-) delete mode 100644 src/tests/util/lru_cache.cpp delete mode 100644 src/util/lru_cache.h diff --git a/src/kernel/expr.cpp b/src/kernel/expr.cpp index 5a9f8ee3d4..3e8459b9d5 100644 --- a/src/kernel/expr.cpp +++ b/src/kernel/expr.cpp @@ -14,7 +14,6 @@ Author: Leonardo de Moura #include "util/hash.h" #include "util/buffer.h" #include "util/object_serializer.h" -#include "util/lru_cache.h" #include "util/memory_pool.h" #include "kernel/expr.h" #include "kernel/expr_eq_fn.h" diff --git a/src/tests/util/CMakeLists.txt b/src/tests/util/CMakeLists.txt index 12c15106c1..39f1b0315a 100644 --- a/src/tests/util/CMakeLists.txt +++ b/src/tests/util/CMakeLists.txt @@ -58,9 +58,6 @@ add_exec_test(serializer "serializer") add_executable(trie trie.cpp $) target_link_libraries(trie ${EXTRA_LIBS}) add_exec_test(trie "trie") -add_executable(lru_cache lru_cache.cpp $) -target_link_libraries(lru_cache ${EXTRA_LIBS}) -add_exec_test(lru_cache "lru_cache") add_executable(worker_queue worker_queue.cpp $) target_link_libraries(worker_queue ${EXTRA_LIBS}) add_exec_test(worker_queue "worker_queue") diff --git a/src/tests/util/lru_cache.cpp b/src/tests/util/lru_cache.cpp deleted file mode 100644 index a7a4a280c6..0000000000 --- a/src/tests/util/lru_cache.cpp +++ /dev/null @@ -1,56 +0,0 @@ -/* -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 deleted file mode 100644 index 946793f771..0000000000 --- a/src/util/lru_cache.h +++ /dev/null @@ -1,140 +0,0 @@ -/* -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(c, 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; } -}; -}