mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-28 08:58:44 +00:00
Code Activity

reduce hash table lookups in expr_abstract in half

Browse source
This commit is contained in:
Nuno Lopes 2024-12-16 11:00:55 +00:00
parent a6e59ea45e
commit 6f24123f0c
2 changed files with 8 additions and 10 deletions
Download patch file Download diff file Expand all files Collapse all files

15
src/ast/expr_abstract.cpp
View file

@ -41,13 +41,14 @@ void expr_abstractor::operator()(unsigned base, unsigned num_bound, expr* const*
while(!m_stack.empty()) { while(!m_stack.empty()) {
curr = m_stack.back(); curr = m_stack.back();
if (m_map.contains(curr)) { auto &val = m_map.insert_if_not_there(curr, nullptr);
if (val) {
m_stack.pop_back(); m_stack.pop_back();
continue; continue;
} }
switch(curr->get_kind()) { switch(curr->get_kind()) {
case AST_VAR: { case AST_VAR: {
m_map.insert(curr, curr); val = curr;
m_stack.pop_back(); m_stack.pop_back();
break; break;
} }
@ -56,7 +57,7 @@ void expr_abstractor::operator()(unsigned base, unsigned num_bound, expr* const*
bool all_visited = true; bool all_visited = true;
bool changed = false; bool changed = false;
m_args.reset(); m_args.reset();
for (unsigned i = 0; i < a->get_num_args(); ++i) { for (unsigned i = 0, e = a->get_num_args(); i < e; ++i) {
if (!m_map.find(a->get_arg(i), b)) { if (!m_map.find(a->get_arg(i), b)) {
m_stack.push_back(a->get_arg(i)); m_stack.push_back(a->get_arg(i));
all_visited = false; all_visited = false;
@ -73,7 +74,7 @@ void expr_abstractor::operator()(unsigned base, unsigned num_bound, expr* const*
} else { } else {
b = curr; b = curr;
} }
m_map.insert(curr, b); val = b;
m_stack.pop_back(); m_stack.pop_back();
} }
break; break;
@ -84,14 +85,14 @@ void expr_abstractor::operator()(unsigned base, unsigned num_bound, expr* const*
expr_ref result1(m); expr_ref result1(m);
unsigned new_base = base + q->get_num_decls(); unsigned new_base = base + q->get_num_decls();
for (unsigned i = 0; i < q->get_num_patterns(); ++i) { for (unsigned i = 0, e = q->get_num_patterns(); i < e; ++i) {
result1 = expr_abstract(m, new_base, num_bound, bound, q->get_pattern(i)); result1 = expr_abstract(m, new_base, num_bound, bound, q->get_pattern(i));
patterns.push_back(result1.get()); patterns.push_back(result1.get());
} }
result1 = expr_abstract(m, new_base, num_bound, bound, q->get_expr()); result1 = expr_abstract(m, new_base, num_bound, bound, q->get_expr());
b = m.update_quantifier(q, patterns.size(), patterns.data(), result1.get()); b = m.update_quantifier(q, patterns.size(), patterns.data(), result1.get());
m_pinned.push_back(b); m_pinned.push_back(b);
m_map.insert(curr, b); val = b;
m_stack.pop_back(); m_stack.pop_back();
break; break;
} }
@ -115,7 +116,7 @@ void expr_abstract(ast_manager& m, unsigned base, unsigned num_bound, expr* cons
tout << result << "\n";); tout << result << "\n";);
} }
expr_ref mk_quantifier(quantifier_kind k, ast_manager& m, unsigned num_bound, app* const* bound, expr* n) { static expr_ref mk_quantifier(quantifier_kind k, ast_manager& m, unsigned num_bound, app* const* bound, expr* n) {
expr_ref result(m); expr_ref result(m);
expr_abstract(m, 0, num_bound, (expr* const*)bound, n, result); expr_abstract(m, 0, num_bound, (expr* const*)bound, n, result);
if (num_bound > 0) { if (num_bound > 0) {

3
src/ast/expr_abstract.h
View file

@ -39,6 +39,3 @@ expr_ref mk_forall(ast_manager& m, unsigned num_bound, app* const* bound, expr*
expr_ref mk_exists(ast_manager& m, unsigned num_bound, app* const* bound, expr* n); expr_ref mk_exists(ast_manager& m, unsigned num_bound, app* const* bound, expr* n);
inline expr_ref mk_forall(ast_manager& m, app* b, expr* n) { return mk_forall(m, 1, &b, n); } inline expr_ref mk_forall(ast_manager& m, app* b, expr* n) { return mk_forall(m, 1, &b, n); }
inline expr_ref mk_forall(ast_manager& m, expr* b, expr* n) { return mk_forall(m, to_app(b), n); } inline expr_ref mk_forall(ast_manager& m, expr* b, expr* n) { return mk_forall(m, to_app(b), n); }