mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-24 23:03:41 +00:00
Code Activity

fix #3034

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2020-02-17 19:09:46 -10:00
parent 41ab578593
commit 23a474655b
3 changed files with 18 additions and 16 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -262,29 +262,30 @@ macro_finder::macro_finder(ast_manager & m, macro_manager & mm):
macro_finder::~macro_finder() { macro_finder::~macro_finder() {
} }
bool macro_finder::expand_macros(unsigned num, expr * const * exprs, proof * const * prs, expr_dependency * const * deps, expr_ref_vector & new_exprs, proof_ref_vector & new_prs, expr_dependency_ref_vector & new_deps) { bool macro_finder::expand_macros(expr_ref_vector const& exprs, proof_ref_vector const& prs, expr_dependency_ref_vector const& deps, expr_ref_vector & new_exprs, proof_ref_vector & new_prs, expr_dependency_ref_vector & new_deps) {
TRACE("macro_finder", tout << "starting expand_macros:\n"; TRACE("macro_finder", tout << "starting expand_macros:\n";
m_macro_manager.display(tout);); m_macro_manager.display(tout););
bool found_new_macro = false; bool found_new_macro = false;
unsigned num = exprs.size();
for (unsigned i = 0; i < num; i++) { for (unsigned i = 0; i < num; i++) {
expr * n = exprs[i]; expr * n = exprs[i];
proof * pr = m.proofs_enabled() ? prs[i] : nullptr; proof * pr = m.proofs_enabled() ? prs[i] : nullptr;
expr_dependency * depi = deps != nullptr ? deps[i] : nullptr; expr_dependency * depi = i < deps.size() ? deps[i] : nullptr;
expr_ref new_n(m), def(m); expr_ref new_n(m), def(m);
proof_ref new_pr(m); proof_ref new_pr(m);
expr_dependency_ref new_dep(m); expr_dependency_ref new_dep(m);
m_macro_manager.expand_macros(n, pr, depi, new_n, new_pr, new_dep); m_macro_manager.expand_macros(n, pr, depi, new_n, new_pr, new_dep);
app_ref head(m), t(m); app_ref head(m), t(m);
if (is_macro(new_n, head, def) && m_macro_manager.insert(head->get_decl(), to_quantifier(new_n.get()), new_pr, new_dep)) { if (is_macro(new_n, head, def) && m_macro_manager.insert(head->get_decl(), to_quantifier(new_n.get()), new_pr, new_dep)) {
TRACE("macro_finder_found", tout << "found new macro: " << head->get_decl()->get_name() << "\n" << new_n << "\n";); TRACE("macro_finder", tout << "found new macro: " << head->get_decl()->get_name() << "\n" << new_n << "\n";);
found_new_macro = true; found_new_macro = true;
} }
else if (is_arith_macro(new_n, new_pr, new_dep, new_exprs, new_prs, new_deps)) { else if (is_arith_macro(new_n, new_pr, new_dep, new_exprs, new_prs, new_deps)) {
TRACE("macro_finder_found", tout << "found new arith macro:\n" << new_n << "\n";); TRACE("macro_finder", tout << "found new arith macro:\n" << new_n << "\n";);
found_new_macro = true; found_new_macro = true;
} }
else if (m_util.is_pseudo_predicate_macro(new_n, head, t, def)) { else if (m_util.is_pseudo_predicate_macro(new_n, head, t, def)) {
TRACE("macro_finder_found", tout << "found new pseudo macro:\n" << head << "\n" << t << "\n" << def << "\n";); TRACE("macro_finder", tout << "found new pseudo macro:\n" << head << "\n" << t << "\n" << def << "\n";);
pseudo_predicate_macro2macro(m, head, t, def, to_quantifier(new_n), new_pr, new_dep, new_exprs, new_prs, new_deps); pseudo_predicate_macro2macro(m, head, t, def, to_quantifier(new_n), new_pr, new_dep, new_exprs, new_prs, new_deps);
found_new_macro = true; found_new_macro = true;
} }
@ -292,20 +293,21 @@ bool macro_finder::expand_macros(unsigned num, expr * const * exprs, proof * con
new_exprs.push_back(new_n); new_exprs.push_back(new_n);
if (m.proofs_enabled()) if (m.proofs_enabled())
new_prs.push_back(new_pr); new_prs.push_back(new_pr);
if (deps != nullptr) if (i < deps.size())
new_deps.push_back(new_dep); new_deps.push_back(new_dep);
} }
} }
return found_new_macro; return found_new_macro;
} }
void macro_finder::operator()(unsigned num, expr * const * exprs, proof * const * prs, expr_dependency * const * deps, expr_ref_vector & new_exprs, proof_ref_vector & new_prs, expr_dependency_ref_vector & new_deps) { void macro_finder::operator()(expr_ref_vector const& exprs, proof_ref_vector const & prs, expr_dependency_ref_vector const & deps, expr_ref_vector & new_exprs, proof_ref_vector & new_prs, expr_dependency_ref_vector & new_deps) {
TRACE("macro_finder", tout << "processing macros...\n";); TRACE("macro_finder", tout << "processing macros...\n";);
expr_ref_vector _new_exprs(m); expr_ref_vector _new_exprs(m);
proof_ref_vector _new_prs(m); proof_ref_vector _new_prs(m);
expr_dependency_ref_vector _new_deps(m); expr_dependency_ref_vector _new_deps(m);
if (expand_macros(num, exprs, prs, deps, _new_exprs, _new_prs, _new_deps)) { unsigned num = exprs.size();
while (true) { if (expand_macros(exprs, prs, deps, _new_exprs, _new_prs, _new_deps)) {
for (unsigned i = 0; i < num; ++i) {
expr_ref_vector old_exprs(m); expr_ref_vector old_exprs(m);
proof_ref_vector old_prs(m); proof_ref_vector old_prs(m);
expr_dependency_ref_vector old_deps(m); expr_dependency_ref_vector old_deps(m);
@ -315,7 +317,7 @@ void macro_finder::operator()(unsigned num, expr * const * exprs, proof * const
SASSERT(_new_exprs.empty()); SASSERT(_new_exprs.empty());
SASSERT(_new_prs.empty()); SASSERT(_new_prs.empty());
SASSERT(_new_deps.empty()); SASSERT(_new_deps.empty());
if (!expand_macros(old_exprs.size(), old_exprs.c_ptr(), old_prs.c_ptr(), old_deps.c_ptr(), if (!expand_macros(old_exprs, old_prs, old_deps,
_new_exprs, _new_prs, _new_deps)) _new_exprs, _new_prs, _new_deps))
break; break;
} }
@ -340,15 +342,15 @@ bool macro_finder::expand_macros(unsigned num, justified_expr const * fmls, vect
m_macro_manager.expand_macros(n, pr, nullptr, new_n, new_pr, new_dep); m_macro_manager.expand_macros(n, pr, nullptr, new_n, new_pr, new_dep);
app_ref head(m), t(m); app_ref head(m), t(m);
if (is_macro(new_n, head, def) && m_macro_manager.insert(head->get_decl(), to_quantifier(new_n.get()), new_pr)) { if (is_macro(new_n, head, def) && m_macro_manager.insert(head->get_decl(), to_quantifier(new_n.get()), new_pr)) {
TRACE("macro_finder_found", tout << "found new macro: " << head->get_decl()->get_name() << "\n" << new_n << "\n";); TRACE("macro_finder", tout << "found new macro: " << head->get_decl()->get_name() << "\n" << new_n << "\n";);
found_new_macro = true; found_new_macro = true;
} }
else if (is_arith_macro(new_n, new_pr, new_fmls)) { else if (is_arith_macro(new_n, new_pr, new_fmls)) {
TRACE("macro_finder_found", tout << "found new arith macro:\n" << new_n << "\n";); TRACE("macro_finder", tout << "found new arith macro:\n" << new_n << "\n";);
found_new_macro = true; found_new_macro = true;
} }
else if (m_util.is_pseudo_predicate_macro(new_n, head, t, def)) { else if (m_util.is_pseudo_predicate_macro(new_n, head, t, def)) {
TRACE("macro_finder_found", tout << "found new pseudo macro:\n" << head << "\n" << t << "\n" << def << "\n";); TRACE("macro_finder", tout << "found new pseudo macro:\n" << head << "\n" << t << "\n" << def << "\n";);
pseudo_predicate_macro2macro(m, head, t, def, to_quantifier(new_n), new_pr, new_fmls); pseudo_predicate_macro2macro(m, head, t, def, to_quantifier(new_n), new_pr, new_fmls);
found_new_macro = true; found_new_macro = true;
} }

4
src/ast/macros/macro_finder.h
View file

@ -31,7 +31,7 @@ class macro_finder {
macro_manager & m_macro_manager; macro_manager & m_macro_manager;
macro_util & m_util; macro_util & m_util;
arith_util m_autil; arith_util m_autil;
bool expand_macros(unsigned num, expr * const * exprs, proof * const * prs, expr_dependency * const* deps, bool expand_macros(expr_ref_vector const& exprs, proof_ref_vector const& prs, expr_dependency_ref_vector const & deps,
expr_ref_vector & new_exprs, proof_ref_vector & new_prs, expr_dependency_ref_vector& new_deps); expr_ref_vector & new_exprs, proof_ref_vector & new_prs, expr_dependency_ref_vector& new_deps);
bool expand_macros(unsigned n, justified_expr const * fmls, vector<justified_expr>& new_fmls); bool expand_macros(unsigned n, justified_expr const * fmls, vector<justified_expr>& new_fmls);
bool is_arith_macro(expr * n, proof * pr, expr_ref_vector & new_exprs, proof_ref_vector & new_prs); bool is_arith_macro(expr * n, proof * pr, expr_ref_vector & new_exprs, proof_ref_vector & new_prs);
@ -43,7 +43,7 @@ class macro_finder {
public: public:
macro_finder(ast_manager & m, macro_manager & mm); macro_finder(ast_manager & m, macro_manager & mm);
~macro_finder(); ~macro_finder();
void operator()(unsigned n, expr * const * exprs, proof * const * prs, expr_dependency * const* deps, expr_ref_vector & new_exprs, proof_ref_vector & new_prs, expr_dependency_ref_vector & new_deps); void operator()(expr_ref_vector const& exprs, proof_ref_vector const& prs, expr_dependency_ref_vector const& deps, expr_ref_vector & new_exprs, proof_ref_vector & new_prs, expr_dependency_ref_vector & new_deps);
void operator()(unsigned n, justified_expr const* fmls, vector<justified_expr>& new_fmls); void operator()(unsigned n, justified_expr const* fmls, vector<justified_expr>& new_fmls);
}; };

2
src/tactic/ufbv/macro_finder_tactic.cpp
View file

@ -57,7 +57,7 @@ class macro_finder_tactic : public tactic {
deps.push_back(g->dep(idx)); deps.push_back(g->dep(idx));
} }
mf(forms.size(), forms.c_ptr(), proofs.c_ptr(), deps.c_ptr(), new_forms, new_proofs, new_deps); mf(forms, proofs, deps, new_forms, new_proofs, new_deps);
g->reset(); g->reset();
for (unsigned i = 0; i < new_forms.size(); i++) for (unsigned i = 0; i < new_forms.size(); i++)