diff --git a/src/ast/ast.cpp b/src/ast/ast.cpp index 9a5e1de9c..067c4d127 100644 --- a/src/ast/ast.cpp +++ b/src/ast/ast.cpp @@ -595,8 +595,7 @@ unsigned get_node_hash(ast const * n) { return 0; } -void ast_table::erase(ast * n) { - // Customized erase method +void ast_table::push_erase(ast * n) { // It uses two important properties: // 1. n is known to be in the table. // 2. operator== can be used instead of compare_nodes (big savings) @@ -604,36 +603,59 @@ void ast_table::erase(ast * n) { unsigned h = n->hash(); unsigned idx = h & mask; cell * c = m_table + idx; - SASSERT(!c->is_free()); cell * prev = nullptr; while (true) { + SASSERT(!c->is_free()); + cell * next = c->m_next; if (c->m_data == n) { m_size--; if (prev == nullptr) { - cell * next = c->m_next; if (next == nullptr) { m_used_slots--; + push_recycle_cell(c); c->mark_free(); SASSERT(c->is_free()); } else { *c = *next; - recycle_cell(next); + next->m_data = n; + push_recycle_cell(next); } } else { - prev->m_next = c->m_next; - recycle_cell(c); + prev->m_next = next; + push_recycle_cell(c); } return; } CHS_CODE(m_collisions++;); prev = c; - c = c->m_next; + c = next; SASSERT(c); } } +ast* ast_table::pop_erase() { + cell* c = m_tofree_cell; + if (c == nullptr) { + return nullptr; + } + if (c->is_free()) { + // cell was marked free, should not be recycled. + c->unmark_free(); + m_tofree_cell = c->m_next; + c->mark_free(); + } + else { + // cell should be recycled with m_free_cell + m_tofree_cell = c->m_next; + recycle_cell(c); + } + return c->m_data; +} + + + // ----------------------------------- // // decl_plugin @@ -1827,21 +1849,17 @@ ast * ast_manager::register_node_core(ast * n) { void ast_manager::delete_node(ast * n) { TRACE("delete_node_bug", tout << mk_ll_pp(n, *this) << "\n";); - ptr_buffer worklist; - worklist.push_back(n); - while (!worklist.empty()) { - n = worklist.back(); - worklist.pop_back(); + SASSERT(m_ast_table.contains(n)); + m_ast_table.push_erase(n); + + while ((n = m_ast_table.pop_erase())) { TRACE("ast", tout << "Deleting object " << n->m_id << " " << n << "\n";); CTRACE("del_quantifier", is_quantifier(n), tout << "deleting quantifier " << n->m_id << " " << n << "\n";); TRACE("mk_var_bug", tout << "del_ast: " << n->m_id << "\n";); TRACE("ast_delete_node", tout << mk_bounded_pp(n, *this) << "\n";); - SASSERT(m_ast_table.contains(n)); - m_ast_table.erase(n); - SASSERT(!m_ast_table.contains(n)); SASSERT(!m_debug_ref_count || !m_debug_free_indices.contains(n->m_id)); #ifdef RECYCLE_FREE_AST_INDICES @@ -1860,29 +1878,35 @@ void ast_manager::delete_node(ast * n) { dealloc(info); } break; - case AST_FUNC_DECL: - if (to_func_decl(n)->m_info != nullptr && !m_debug_ref_count) { - func_decl_info * info = to_func_decl(n)->get_info(); + case AST_FUNC_DECL: { + func_decl* f = to_func_decl(n); + if (f->m_info != nullptr && !m_debug_ref_count) { + func_decl_info * info = f->get_info(); info->del_eh(*this); dealloc(info); } - dec_array_ref(worklist, to_func_decl(n)->get_arity(), to_func_decl(n)->get_domain()); - dec_ref(worklist, to_func_decl(n)->get_range()); + push_dec_array_ref(f->get_arity(), f->get_domain()); + push_dec_ref(f->get_range()); break; - case AST_APP: - dec_ref(worklist, to_app(n)->get_decl()); - dec_array_ref(worklist, to_app(n)->get_num_args(), to_app(n)->get_args()); + } + case AST_APP: { + app* a = to_app(n); + push_dec_ref(a->get_decl()); + push_dec_array_ref(a->get_num_args(), a->get_args()); break; + } case AST_VAR: - dec_ref(worklist, to_var(n)->get_sort()); + push_dec_ref(to_var(n)->get_sort()); break; - case AST_QUANTIFIER: - dec_array_ref(worklist, to_quantifier(n)->get_num_decls(), to_quantifier(n)->get_decl_sorts()); - dec_ref(worklist, to_quantifier(n)->get_expr()); - dec_ref(worklist, to_quantifier(n)->get_sort()); - dec_array_ref(worklist, to_quantifier(n)->get_num_patterns(), to_quantifier(n)->get_patterns()); - dec_array_ref(worklist, to_quantifier(n)->get_num_no_patterns(), to_quantifier(n)->get_no_patterns()); + case AST_QUANTIFIER: { + quantifier* q = to_quantifier(n); + push_dec_array_ref(q->get_num_decls(), q->get_decl_sorts()); + push_dec_ref(q->get_expr()); + push_dec_ref(q->get_sort()); + push_dec_array_ref(q->get_num_patterns(), q->get_patterns()); + push_dec_array_ref(q->get_num_no_patterns(), q->get_no_patterns()); break; + } default: break; } diff --git a/src/ast/ast.h b/src/ast/ast.h index 4054b32dc..b81db5196 100644 --- a/src/ast/ast.h +++ b/src/ast/ast.h @@ -962,7 +962,8 @@ class ast_translation; class ast_table : public chashtable, ast_eq_proc> { public: - void erase(ast * n); + void push_erase(ast * n); + ast* pop_erase(); }; // ----------------------------------- @@ -2297,17 +2298,17 @@ protected: bool check_nnf_proof_parents(unsigned num_proofs, proof * const * proofs) const; private: - void dec_ref(ptr_buffer & worklist, ast * n) { + void push_dec_ref(ast * n) { n->dec_ref(); if (n->get_ref_count() == 0) { - worklist.push_back(n); + m_ast_table.push_erase(n); } } template - void dec_array_ref(ptr_buffer & worklist, unsigned sz, T * const * a) { + void push_dec_array_ref(unsigned sz, T * const * a) { for(unsigned i = 0; i < sz; i++) { - dec_ref(worklist, a[i]); + push_dec_ref(a[i]); } } }; diff --git a/src/tactic/smtlogics/qfnia_tactic.cpp b/src/tactic/smtlogics/qfnia_tactic.cpp index 02e3349aa..d28034a1d 100644 --- a/src/tactic/smtlogics/qfnia_tactic.cpp +++ b/src/tactic/smtlogics/qfnia_tactic.cpp @@ -116,5 +116,6 @@ tactic * mk_qfnia_tactic(ast_manager & m, params_ref const & p) { or_else(mk_qfnia_sat_solver(m, p), try_for(mk_qfnia_smt_solver(m, p), 2000), mk_qfnia_nlsat_solver(m, p), - mk_qfnia_smt_solver(m, p))); + mk_qfnia_smt_solver(m, p)) + ); } diff --git a/src/util/chashtable.h b/src/util/chashtable.h index 9bc5988e5..e49ac3bd4 100644 --- a/src/util/chashtable.h +++ b/src/util/chashtable.h @@ -31,6 +31,7 @@ Revision History: #include "util/memory_manager.h" #include "util/debug.h" #include "util/trace.h" +#include "util/tptr.h" #ifdef Z3DEBUG #include "util/hashtable.h" #endif @@ -54,8 +55,9 @@ protected: cell * m_next; T m_data; cell():m_next(reinterpret_cast(1)) {} - bool is_free() const { return m_next == reinterpret_cast(1); } - void mark_free() { m_next = reinterpret_cast(1); } + bool is_free() const { return GET_TAG(m_next) == 1; } + void mark_free() { m_next = TAG(cell*, m_next, 1); } + void unmark_free() { m_next = UNTAG(cell*, m_next); } }; cell * m_table; // array of cells. @@ -70,6 +72,7 @@ protected: #endif cell * m_next_cell; cell * m_free_cell; + cell * m_tofree_cell; unsigned get_hash(T const & d) const { return HashProc::operator()(d); } bool equals(T const & e1, T const & e2) const { return EqProc::operator()(e1, e2); } @@ -171,6 +174,7 @@ protected: m_slots = new_slots; m_next_cell = next_cell; m_free_cell = nullptr; + m_tofree_cell = nullptr; CASSERT("chashtable", check_invariant()); return; } @@ -204,6 +208,12 @@ protected: m_free_cell = c; } + void push_recycle_cell(cell* c) { + SASSERT(c < m_table + m_capacity); + c->m_next = m_tofree_cell; + m_tofree_cell = c; + } + void init(unsigned slots, unsigned cellar) { m_capacity = slots + cellar; m_table = alloc_table(m_capacity); @@ -212,6 +222,7 @@ protected: m_size = 0; m_next_cell = m_table + slots; m_free_cell = nullptr; + m_tofree_cell = nullptr; } public: diff --git a/src/util/memory_manager.cpp b/src/util/memory_manager.cpp index 0a1d360c8..148306fbd 100644 --- a/src/util/memory_manager.cpp +++ b/src/util/memory_manager.cpp @@ -292,8 +292,10 @@ void memory::deallocate(void * p) { void * memory::allocate(size_t s) { s = s + sizeof(size_t); // we allocate an extra field! void * r = malloc(s); - if (r == 0) + if (r == 0) { throw_out_of_memory(); + return nullptr; + } *(static_cast(r)) = s; g_memory_thread_alloc_size += s; g_memory_thread_alloc_count += 1; @@ -317,8 +319,10 @@ void* memory::reallocate(void *p, size_t s) { } void *r = realloc(real_p, s); - if (r == 0) + if (r == 0) { throw_out_of_memory(); + return nullptr; + } *(static_cast(r)) = s; return static_cast(r) + 1; // we return a pointer to the location after the extra field } @@ -361,8 +365,10 @@ void * memory::allocate(size_t s) { if (counts_exceeded) throw_alloc_counts_exceeded(); void * r = malloc(s); - if (r == nullptr) + if (r == nullptr) { throw_out_of_memory(); + return nullptr; + } *(static_cast(r)) = s; return static_cast(r) + 1; // we return a pointer to the location after the extra field } @@ -389,8 +395,10 @@ void* memory::reallocate(void *p, size_t s) { if (counts_exceeded) throw_alloc_counts_exceeded(); void *r = realloc(real_p, s); - if (r == nullptr) + if (r == nullptr) { throw_out_of_memory(); + return nullptr; + } *(static_cast(r)) = s; return static_cast(r) + 1; // we return a pointer to the location after the extra field }