mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-29 20:05:51 +00:00
Code Activity

reset cache in ast_translation periodically to avoid congestion

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2017-12-15 07:21:37 -08:00
parent 6b258578f9
commit 030868d8de
5 changed files with 97 additions and 27 deletions
Download patch file Download diff file Expand all files Collapse all files

44
src/ast/ast_translation.cpp
View file

@ -23,6 +23,7 @@ Revision History:
#include "ast/format.h"
#include "ast/ast_translation.h"
#include "ast/ast_ll_pp.h"
#include "ast/ast_pp.h"
ast_translation::~ast_translation() {
reset_cache();
@ -47,7 +48,12 @@ void ast_translation::reset_cache() {
void ast_translation::cache(ast * s, ast * t) {
SASSERT(!m_cache.contains(s));
if (s->get_ref_count() > 1) {
if (m_insert_count > (1 << 17)) {
reset_cache();
m_insert_count = 0;
}
m_cache.insert(s, t);
++m_insert_count;
m_from_manager.inc_ref(s);
m_to_manager.inc_ref(t);
}
@ -76,9 +82,15 @@ void ast_translation::push_frame(ast * n) {
bool ast_translation::visit(ast * n) {
ast * r;
if (n->get_ref_count() > 1 && m_cache.find(n, r)) {
m_result_stack.push_back(r);
return true;
if (n->get_ref_count() > 1) {
if (m_cache.find(n, r)) {
m_result_stack.push_back(r);
++m_hit_count;
return true;
}
else {
++m_miss_count;
}
}
push_frame(n);
return false;
@ -187,20 +199,32 @@ ast * ast_translation::process(ast const * _n) {
SASSERT(m_frame_stack.empty());
SASSERT(m_extra_children_stack.empty());
++m_num_process;
if (m_num_process > (1 << 16)) {
reset_cache();
m_num_process = 0;
}
if (!visit(const_cast<ast*>(_n))) {
while (!m_frame_stack.empty()) {
loop:
++m_loop_count;
frame & fr = m_frame_stack.back();
ast * n = fr.m_n;
ast * r;
TRACE("ast_translation", tout << mk_ll_pp(n, m_from_manager, false) << "\n";);
if (fr.m_idx == 0 && n->get_ref_count() > 1 && m_cache.find(n, r)) {
SASSERT(m_result_stack.size() == fr.m_rpos);
m_result_stack.push_back(r);
m_extra_children_stack.shrink(fr.m_cpos);
m_frame_stack.pop_back();
TRACE("ast_translation", tout << "hit\n";);
continue;
if (fr.m_idx == 0 && n->get_ref_count() > 1) {
if (m_cache.find(n, r)) {
SASSERT(m_result_stack.size() == fr.m_rpos);
m_result_stack.push_back(r);
m_extra_children_stack.shrink(fr.m_cpos);
m_frame_stack.pop_back();
TRACE("ast_translation", tout << "hit\n";);
m_hit_count++;
continue;
}
else {
m_miss_count++;
}
}
switch (n->get_kind()) {
case AST_VAR: {

16
src/ast/ast_translation.h
View file

@ -37,6 +37,11 @@ class ast_translation {
ptr_vector<ast> m_extra_children_stack; // for sort and func_decl, since they have nested AST in their parameters
ptr_vector<ast> m_result_stack;
obj_map<ast, ast*> m_cache;
unsigned m_loop_count;
unsigned m_hit_count;
unsigned m_miss_count;
unsigned m_insert_count;
unsigned m_num_process;
void cache(ast * s, ast * t);
void collect_decl_extra_children(decl * d);
@ -50,6 +55,11 @@ class ast_translation {
public:
ast_translation(ast_manager & from, ast_manager & to, bool copy_plugins = true) : m_from_manager(from), m_to_manager(to) {
m_loop_count = 0;
m_hit_count = 0;
m_miss_count = 0;
m_insert_count = 0;
m_num_process = 0;
if (&from != &to) {
if (copy_plugins)
m_to_manager.copy_families_plugins(m_from_manager);
@ -73,6 +83,12 @@ public:
void reset_cache();
void cleanup();
unsigned loop_count() const { return m_loop_count; }
unsigned hit_count() const { return m_hit_count; }
unsigned miss_count() const { return m_miss_count; }
unsigned insert_count() const { return m_insert_count; }
unsigned long long get_num_collision() const { return m_cache.get_num_collision(); }
};
// Translation with non-persistent cache.