From 3eefd18c58ffef94c4e3b5f6d6e485d9ad64defa Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Thu, 2 Apr 2020 09:59:16 -0700 Subject: [PATCH] fix #3688 Signed-off-by: Nikolaj Bjorner --- src/ast/macros/macro_manager.cpp | 14 ++++---- src/ast/macros/quasi_macros.cpp | 44 ++++++++++++------------- src/ast/macros/quasi_macros.h | 5 ++- src/tactic/goal.cpp | 2 ++ src/tactic/ufbv/quasi_macros_tactic.cpp | 19 +++-------- 5 files changed, 38 insertions(+), 46 deletions(-) diff --git a/src/ast/macros/macro_manager.cpp b/src/ast/macros/macro_manager.cpp index e732f4de3..dde162047 100644 --- a/src/ast/macros/macro_manager.cpp +++ b/src/ast/macros/macro_manager.cpp @@ -121,7 +121,8 @@ bool macro_manager::insert(func_decl * f, quantifier * q, proof * pr, expr_depen m_macros.push_back(q); if (m.proofs_enabled()) { m_macro_prs.push_back(pr); - m_decl2macro_pr.insert(f, pr); + m_decl2macro_pr.insert(f, pr); + SASSERT(m.get_fact(pr) == q); } m_macro_deps.push_back(dep); m_decl2macro_dep.insert(f, dep); @@ -274,8 +275,7 @@ struct macro_manager::macro_expander_cfg : public default_rewriter_cfg { quantifier * q = nullptr; func_decl * d = n->get_decl(); TRACE("macro_manager", tout << "trying to expand:\n" << mk_pp(n, m) << "\nd:\n" << d->get_name() << "\n";); - if (mm.m_decl2macro.find(d, q)) { - + if (mm.m_decl2macro.find(d, q)) { app * head = nullptr; expr * def = nullptr; bool revert = false; @@ -300,9 +300,7 @@ struct macro_manager::macro_expander_cfg : public default_rewriter_cfg { if (m.proofs_enabled()) { expr_ref instance = s(q->get_expr(), num, subst_args.c_ptr()); proof * qi_pr = m.mk_quant_inst(m.mk_or(m.mk_not(q), instance), num, subst_args.c_ptr()); - proof * q_pr = nullptr; - mm.m_decl2macro_pr.find(d, q_pr); - SASSERT(q_pr); + proof * q_pr = mm.m_decl2macro_pr.find(d); proof * prs[2] = { qi_pr, q_pr }; p = m.mk_unit_resolution(2, prs); if (revert) p = m.mk_symmetry(p); @@ -352,6 +350,7 @@ void macro_manager::expand_macros(expr * n, proof * pr, expr_dependency * dep, e old_pr = new_pr; old_dep = new_dep; change = true; + SASSERT(!new_pr || m.get_fact(new_pr) == r); } // apply th_rewrite to the result. if (change) { @@ -360,6 +359,7 @@ void macro_manager::expand_macros(expr * n, proof * pr, expr_dependency * dep, e expr_ref r1(r, m); rw(r1, r, rw_pr); new_pr = m.mk_modus_ponens(new_pr, rw_pr); + SASSERT(!new_pr || m.get_fact(new_pr) == r); } } else { @@ -367,5 +367,7 @@ void macro_manager::expand_macros(expr * n, proof * pr, expr_dependency * dep, e new_pr = pr; new_dep = dep; } + + SASSERT(!new_pr || m.get_fact(new_pr) == r); } diff --git a/src/ast/macros/quasi_macros.cpp b/src/ast/macros/quasi_macros.cpp index 28d2d1d36..5a62df52a 100644 --- a/src/ast/macros/quasi_macros.cpp +++ b/src/ast/macros/quasi_macros.cpp @@ -329,45 +329,43 @@ bool quasi_macros::find_macros(unsigned n, justified_expr const * exprs) { return res; } -void quasi_macros::apply_macros(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 quasi_macros::apply_macros(expr_ref_vector & exprs, proof_ref_vector & prs, expr_dependency_ref_vector& deps) { + unsigned n = exprs.size(); for (unsigned i = 0 ; i < n ; i++ ) { - expr_ref r(m); - proof_ref pr(m); + expr_ref r(m), rr(m); + proof_ref pr(m), prr(m); expr_dependency_ref dep(m); - proof * p = m.proofs_enabled() ? prs[i] : nullptr; - m_macro_manager.expand_macros(exprs[i], p, deps[i], r, pr, dep); - m_rewriter(r); - new_exprs.push_back(r); - new_prs.push_back(pr); - new_deps.push_back(dep); + proof * p = m.proofs_enabled() ? prs.get(i) : nullptr; + m_macro_manager.expand_macros(exprs.get(i), p, deps.get(i), r, pr, dep); + m_rewriter(r, rr, prr); + if (pr) pr = m.mk_modus_ponens(pr, prr); + exprs[i] = rr; + prs[i] = pr; + deps[i] = dep; } } -bool quasi_macros::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) { - if (find_macros(n, exprs)) { - apply_macros(n, exprs, prs, deps, new_exprs, new_prs, new_deps); +bool quasi_macros::operator()(expr_ref_vector & exprs, proof_ref_vector & prs, expr_dependency_ref_vector & deps) { + unsigned n = exprs.size(); + if (find_macros(n, exprs.c_ptr())) { + apply_macros(exprs, prs, deps); return true; } else { - // just copy them over - for ( unsigned i = 0 ; i < n ; i++ ) { - new_exprs.push_back(exprs[i]); - if (m.proofs_enabled()) - new_prs.push_back(prs[i]); - } return false; } } void quasi_macros::apply_macros(unsigned n, justified_expr const* fmls, vector& new_fmls) { for (unsigned i = 0 ; i < n ; i++) { - expr_ref r(m); - proof_ref pr(m); + expr_ref r(m), rr(m); + proof_ref pr(m), prr(m); proof * p = m.proofs_enabled() ? fmls[i].get_proof() : nullptr; expr_dependency_ref dep(m); m_macro_manager.expand_macros(fmls[i].get_fml(), p, nullptr, r, pr, dep); - m_rewriter(r); - new_fmls.push_back(justified_expr(m, r, pr)); + m_rewriter(r, rr, prr); + if (pr) pr = m.mk_modus_ponens(pr, prr); + new_fmls.push_back(justified_expr(m, rr, pr)); } } @@ -378,7 +376,7 @@ bool quasi_macros::operator()(unsigned n, justified_expr const* fmls, vector& new_fmls); public: @@ -68,7 +67,7 @@ public: */ // bool operator()(unsigned n, expr * const * exprs, proof * const * prs, expr_ref_vector & new_exprs, proof_ref_vector & new_prs); bool operator()(unsigned n, justified_expr const* fmls, vector& new_fmls); - bool 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); + bool operator()(expr_ref_vector & exprs, proof_ref_vector & prs, expr_dependency_ref_vector & deps); }; diff --git a/src/tactic/goal.cpp b/src/tactic/goal.cpp index e7e4e3b8e..5579660b2 100644 --- a/src/tactic/goal.cpp +++ b/src/tactic/goal.cpp @@ -18,6 +18,7 @@ Revision History: --*/ #include "ast/ast_ll_pp.h" #include "ast/ast_smt2_pp.h" +#include "ast/ast_pp.h" #include "ast/for_each_expr.h" #include "ast/well_sorted.h" #include "ast/display_dimacs.h" @@ -255,6 +256,7 @@ void goal::assert_expr(expr * f, proof * pr, expr_dependency * d) { } SASSERT(!m().proofs_enabled() || pr); if (pr) { + CTRACE("goal", f != m().get_fact(pr), tout << mk_pp(f, m()) << "\n" << mk_pp(pr, m()) << "\n";); SASSERT(f == m().get_fact(pr)); slow_process(f, pr, d); } diff --git a/src/tactic/ufbv/quasi_macros_tactic.cpp b/src/tactic/ufbv/quasi_macros_tactic.cpp index 812e6797d..850c03e20 100644 --- a/src/tactic/ufbv/quasi_macros_tactic.cpp +++ b/src/tactic/ufbv/quasi_macros_tactic.cpp @@ -44,11 +44,10 @@ class quasi_macros_tactic : public tactic { macro_manager mm(m_manager); quasi_macros qm(m_manager, mm); - bool more = true; - expr_ref_vector forms(m_manager), new_forms(m_manager); - proof_ref_vector proofs(m_manager), new_proofs(m_manager); - expr_dependency_ref_vector deps(m_manager), new_deps(m_manager); + expr_ref_vector forms(m_manager); + proof_ref_vector proofs(m_manager); + expr_dependency_ref_vector deps(m_manager); unsigned size = g->size(); for (unsigned i = 0; i < size; i++) { @@ -60,19 +59,11 @@ class quasi_macros_tactic : public tactic { do { if (m().canceled()) throw tactic_exception(m().limit().get_cancel_msg()); - - new_forms.reset(); - new_proofs.reset(); - new_deps.reset(); - more = qm(forms.size(), forms.c_ptr(), proofs.c_ptr(), deps.c_ptr(), new_forms, new_proofs, new_deps); - forms.swap(new_forms); - proofs.swap(new_proofs); - deps.swap(new_deps); } - while (more); + while (qm(forms, proofs, deps)); g->reset(); - for (unsigned i = 0; i < new_forms.size(); i++) + for (unsigned i = 0; i < forms.size(); i++) g->assert_expr(forms.get(i), produce_proofs ? proofs.get(i) : nullptr, produce_unsat_cores ? deps.get(i, nullptr) : nullptr);