mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-13 09:26:15 +00:00
Code Activity

add proper garbage collection to ast_manager. Issue #679

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2016-07-14 09:05:16 -07:00
parent b080e3a216
commit 4720d578a4
1 changed files with 55 additions and 15 deletions
Download patch file Download diff file Expand all files Collapse all files

70
src/ast/ast.cpp
View file

@ -1386,6 +1386,14 @@ void ast_manager::init() {
inc_ref(m_false); inc_ref(m_false);
} }
template<typename T>
static void mark_array_ref(ast_mark& mark, unsigned sz, T * const * a) {
for(unsigned i = 0; i < sz; i++) {
mark.mark(a[i], true);
}
}
ast_manager::~ast_manager() { ast_manager::~ast_manager() {
SASSERT(is_format_manager() || !m_family_manager.has_family(symbol("format"))); SASSERT(is_format_manager() || !m_family_manager.has_family(symbol("format")));
@ -1405,26 +1413,58 @@ ast_manager::~ast_manager() {
if (*it) if (*it)
dealloc(*it); dealloc(*it);
} }
DEBUG_CODE({ while (!m_ast_table.empty()) {
if (!m_ast_table.empty()) DEBUG_CODE(std::cout << "ast_manager LEAKED: " << m_ast_table.size() << std::endl;);
std::cout << "ast_manager LEAKED: " << m_ast_table.size() << std::endl; ptr_vector<ast> roots;
}); ast_mark mark;
#if 1
DEBUG_CODE({
ast_table::iterator it_a = m_ast_table.begin(); ast_table::iterator it_a = m_ast_table.begin();
ast_table::iterator end_a = m_ast_table.end(); ast_table::iterator end_a = m_ast_table.end();
for (; it_a != end_a; ++it_a) { for (; it_a != end_a; ++it_a) {
ast* a = (*it_a); ast* n = (*it_a);
std::cout << "Leaked: "; switch (n->get_kind()) {
if (is_sort(a)) { case AST_SORT:
std::cout << to_sort(a)->get_name() << "\n"; break;
} case AST_FUNC_DECL:
else { mark_array_ref(mark, to_func_decl(n)->get_arity(), to_func_decl(n)->get_domain());
std::cout << mk_ll_pp(a, *this, false) << "id: " << a->get_id() << "\n"; mark.mark(to_func_decl(n)->get_range(), true);
break;
case AST_APP:
mark.mark(to_app(n)->get_decl(), true);
mark_array_ref(mark, to_app(n)->get_num_args(), to_app(n)->get_args());
break;
case AST_VAR:
mark.mark(to_var(n)->get_sort(), true);
break;
case AST_QUANTIFIER:
mark_array_ref(mark, to_quantifier(n)->get_num_decls(), to_quantifier(n)->get_decl_sorts());
mark.mark(to_quantifier(n)->get_expr(), true);
mark_array_ref(mark, to_quantifier(n)->get_num_patterns(), to_quantifier(n)->get_patterns());
mark_array_ref(mark, to_quantifier(n)->get_num_no_patterns(), to_quantifier(n)->get_no_patterns());
break;
}
}
it_a = m_ast_table.begin();
for (; it_a != end_a; ++it_a) {
ast* n = *it_a;
if (!mark.is_marked(n)) {
roots.push_back(n);
} }
}
SASSERT(!roots.empty());
for (unsigned i = 0; i < roots.size(); ++i) {
ast* a = roots[i];
DEBUG_CODE(
std::cout << "Leaked: ";
if (is_sort(a)) {
std::cout << to_sort(a)->get_name() << "\n";
}
else {
std::cout << mk_ll_pp(a, *this, false) << "id: " << a->get_id() << "\n";
});
dec_ref(a);
} }
}); }
#endif
if (m_format_manager != 0) if (m_format_manager != 0)
dealloc(m_format_manager); dealloc(m_format_manager);
if (m_trace_stream_owner) { if (m_trace_stream_owner) {