mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-08 02:15:19 +00:00
Code Activity

remove unfinished ite-macro finder, tune ast GC to ensure nodes are roots only once

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2016-07-14 09:46:09 -07:00
parent 4720d578a4
commit 3a83788b97
4 changed files with 3 additions and 19 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

4
src/ast/ast.cpp
View file

@ -1461,8 +1461,8 @@ ast_manager::~ast_manager() {
else {
std::cout << mk_ll_pp(a, *this, false) << "id: " << a->get_id() << "\n";
});
dec_ref(a);
a->m_ref_count = 0;
delete_node(a);
}
}
if (m_format_manager != 0)

2
src/ast/macros/macro_finder.cpp
View file

@ -28,7 +28,7 @@ bool macro_finder::is_macro(expr * n, app_ref & head, expr_ref & def) {
TRACE("macro_finder", tout << "processing: " << mk_pp(n, m_manager) << "\n";);
expr * body = to_quantifier(n)->get_expr();
unsigned num_decls = to_quantifier(n)->get_num_decls();
return m_util.is_ite_macro(body, num_decls, head, def);
return m_util.is_simple_macro(body, num_decls, head, def);
}
/**

15
src/ast/macros/macro_util.cpp
View file

@ -189,21 +189,6 @@ bool macro_util::is_left_simple_macro(expr * n, unsigned num_decls, app_ref & he
return false;
}
bool macro_util::is_ite_macro(expr * n, unsigned num_decls, app_ref& head, expr_ref& def) const {
if (is_simple_macro(n, num_decls, head, def)) {
return true;
}
expr* c, *t, *e;
expr_ref def1(m_manager), def2(m_manager);
app_ref head2(m_manager);
if (m_manager.is_ite(n, c, t, e) &&
is_ite_macro(t, num_decls, head, def1) &&
is_ite_macro(e, num_decls, head2, def2) && head == head2) {
def = m_manager.mk_ite(c, def1, def2);
return true;
}
return false;
}
/**
\brief Return true if n is of the form

1
src/ast/macros/macro_util.h
View file

@ -107,7 +107,6 @@ public:
bool is_simple_macro(expr * n, unsigned num_decls, app_ref& head, expr_ref & def) const {
return is_left_simple_macro(n, num_decls, head, def) || is_right_simple_macro(n, num_decls, head, def);
}
bool is_ite_macro(expr * n, unsigned num_decls, app_ref& head, expr_ref& def) const;
bool is_arith_macro(expr * n, unsigned num_decls, app_ref & head, expr_ref & def, bool & inv) const;
bool is_arith_macro(expr * n, unsigned num_decls, app_ref & head, expr_ref & def) const {