feat(util): add lru cache

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>

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)

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<int> 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<unsigned>(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<unsigned>(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<int> 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;
+}

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 <unordered_set>
+#include <algorithm>
+#include <functional>
+#include "util/debug.h"
+
+namespace lean {
+/** \brief Simple LRU cache on top of std::unordered_set */
+template<typename Key, typename Hash = std::hash<Key>, typename Eq = std::equal_to<Key>>
+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<entry*>(m_head.m_prev);
+        last->remove();
+        m_cache.erase(entry(last->m_key));
+    }
+
+    unsigned                                        m_capacity;
+    std::unordered_set<entry, entry_hash, entry_eq> 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<entry &>(*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<entry &>(*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<entry &>(*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; }
+};
+}