michael/lean2
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

refactor(kernel): move replace_cache to separate .h file

Browse source
This commit is contained in:
Leonardo de Moura 2015-09-21 15:24:45 -07:00
parent 3d4475b7d9
commit a7c2d798de
2 changed files with 50 additions and 42 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

49
src/kernel/replace_cache.h Normal file
View file

@ -0,0 +1,49 @@
/*
Copyright (c) 2013-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 <vector>
#include "kernel/expr.h"
namespace lean {
struct replace_cache {
struct entry {
expr_cell * m_cell;
unsigned m_offset;
expr m_result;
entry():m_cell(nullptr) {}
};
unsigned m_capacity;
std::vector<entry> m_cache;
std::vector<unsigned> m_used;
replace_cache(unsigned c):m_capacity(c), m_cache(c) {}
expr * find(expr const & e, unsigned offset) {
unsigned i = hash(e.hash_alloc(), offset) % m_capacity;
if (m_cache[i].m_cell == e.raw() && m_cache[i].m_offset == offset)
return &m_cache[i].m_result;
else
return nullptr;
}
void insert(expr const & e, unsigned offset, expr const & v) {
unsigned i = hash(e.hash_alloc(), offset) % m_capacity;
if (m_cache[i].m_cell == nullptr)
m_used.push_back(i);
m_cache[i].m_cell = e.raw();
m_cache[i].m_offset = offset;
m_cache[i].m_result = v;
}
void clear() {
for (unsigned i : m_used) {
m_cache[i].m_cell = nullptr;
m_cache[i].m_result = expr();
}
m_used.clear();
}
};
}

43
src/kernel/replace_fn.cpp
View file

@ -8,54 +8,13 @@ Author: Leonardo de Moura
#include <memory>
#include "kernel/replace_fn.h"
#include "kernel/cache_stack.h"
#include "kernel/replace_cache.h"
#ifndef LEAN_DEFAULT_REPLACE_CACHE_CAPACITY
#define LEAN_DEFAULT_REPLACE_CACHE_CAPACITY 1024*8
#endif
#ifndef LEAN_REPLACE_SMALL_TERM_THRESHOLD
#define LEAN_REPLACE_SMALL_TERM_THRESHOLD 10000
#endif
namespace lean {
struct replace_cache {
struct entry {
expr_cell * m_cell;
unsigned m_offset;
expr m_result;
entry():m_cell(nullptr) {}
};
unsigned m_capacity;
std::vector<entry> m_cache;
std::vector<unsigned> m_used;
replace_cache(unsigned c):m_capacity(c), m_cache(c) {}
expr * find(expr const & e, unsigned offset) {
unsigned i = hash(e.hash_alloc(), offset) % m_capacity;
if (m_cache[i].m_cell == e.raw() && m_cache[i].m_offset == offset)
return &m_cache[i].m_result;
else
return nullptr;
}
void insert(expr const & e, unsigned offset, expr const & v) {
unsigned i = hash(e.hash_alloc(), offset) % m_capacity;
if (m_cache[i].m_cell == nullptr)
m_used.push_back(i);
m_cache[i].m_cell = e.raw();
m_cache[i].m_offset = offset;
m_cache[i].m_result = v;
}
void clear() {
for (unsigned i : m_used) {
m_cache[i].m_cell = nullptr;
m_cache[i].m_result = expr();
}
m_used.clear();
}
};
MK_CACHE_STACK(replace_cache, LEAN_DEFAULT_REPLACE_CACHE_CAPACITY)
class replace_rec_fn {