mirror of
https://github.com/Z3Prover/z3
synced 2025-04-07 18:05:21 +00:00
parent
8590876d18
commit
0c1408b30e
|
@ -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<ast> 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;
|
||||
}
|
||||
|
|
|
@ -962,7 +962,8 @@ class ast_translation;
|
|||
|
||||
class ast_table : public chashtable<ast*, obj_ptr_hash<ast>, 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<ast> & 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<typename T>
|
||||
void dec_array_ref(ptr_buffer<ast> & 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]);
|
||||
}
|
||||
}
|
||||
};
|
||||
|
|
|
@ -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))
|
||||
);
|
||||
}
|
||||
|
|
|
@ -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<cell*>(1)) {}
|
||||
bool is_free() const { return m_next == reinterpret_cast<cell*>(1); }
|
||||
void mark_free() { m_next = reinterpret_cast<cell*>(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:
|
||||
|
|
|
@ -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<size_t*>(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<size_t*>(r)) = s;
|
||||
return static_cast<size_t*>(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<size_t*>(r)) = s;
|
||||
return static_cast<size_t*>(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<size_t*>(r)) = s;
|
||||
return static_cast<size_t*>(r) + 1; // we return a pointer to the location after the extra field
|
||||
}
|
||||
|
|
Loading…
Reference in a new issue