mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-27 08:28:44 +00:00
Code Activity

fix #3688

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2020-04-02 09:59:16 -07:00
parent 8290cfadcc
commit 3eefd18c58
5 changed files with 38 additions and 46 deletions
Download patch file Download diff file Expand all files Collapse all files

14
src/ast/macros/macro_manager.cpp
View file

@ -121,7 +121,8 @@ bool macro_manager::insert(func_decl * f, quantifier * q, proof * pr, expr_depen
m_macros.push_back(q); m_macros.push_back(q);
if (m.proofs_enabled()) { if (m.proofs_enabled()) {
m_macro_prs.push_back(pr); 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_macro_deps.push_back(dep);
m_decl2macro_dep.insert(f, dep); m_decl2macro_dep.insert(f, dep);
@ -274,8 +275,7 @@ struct macro_manager::macro_expander_cfg : public default_rewriter_cfg {
quantifier * q = nullptr; quantifier * q = nullptr;
func_decl * d = n->get_decl(); func_decl * d = n->get_decl();
TRACE("macro_manager", tout << "trying to expand:\n" << mk_pp(n, m) << "\nd:\n" << d->get_name() << "\n";); 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; app * head = nullptr;
expr * def = nullptr; expr * def = nullptr;
bool revert = false; bool revert = false;
@ -300,9 +300,7 @@ struct macro_manager::macro_expander_cfg : public default_rewriter_cfg {
if (m.proofs_enabled()) { if (m.proofs_enabled()) {
expr_ref instance = s(q->get_expr(), num, subst_args.c_ptr()); 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 * qi_pr = m.mk_quant_inst(m.mk_or(m.mk_not(q), instance), num, subst_args.c_ptr());
proof * q_pr = nullptr; proof * q_pr = mm.m_decl2macro_pr.find(d);
mm.m_decl2macro_pr.find(d, q_pr);
SASSERT(q_pr);
proof * prs[2] = { qi_pr, q_pr }; proof * prs[2] = { qi_pr, q_pr };
p = m.mk_unit_resolution(2, prs); p = m.mk_unit_resolution(2, prs);
if (revert) p = m.mk_symmetry(p); 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_pr = new_pr;
old_dep = new_dep; old_dep = new_dep;
change = true; change = true;
SASSERT(!new_pr || m.get_fact(new_pr) == r);
} }
// apply th_rewrite to the result. // apply th_rewrite to the result.
if (change) { if (change) {
@ -360,6 +359,7 @@ void macro_manager::expand_macros(expr * n, proof * pr, expr_dependency * dep, e
expr_ref r1(r, m); expr_ref r1(r, m);
rw(r1, r, rw_pr); rw(r1, r, rw_pr);
new_pr = m.mk_modus_ponens(new_pr, rw_pr); new_pr = m.mk_modus_ponens(new_pr, rw_pr);
SASSERT(!new_pr || m.get_fact(new_pr) == r);
} }
} }
else { else {
@ -367,5 +367,7 @@ void macro_manager::expand_macros(expr * n, proof * pr, expr_dependency * dep, e
new_pr = pr; new_pr = pr;
new_dep = dep; new_dep = dep;
} }
SASSERT(!new_pr || m.get_fact(new_pr) == r);
} }

44
src/ast/macros/quasi_macros.cpp
View file

@ -329,45 +329,43 @@ bool quasi_macros::find_macros(unsigned n, justified_expr const * exprs) {
return res; 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++ ) { for (unsigned i = 0 ; i < n ; i++ ) {
expr_ref r(m); expr_ref r(m), rr(m);
proof_ref pr(m); proof_ref pr(m), prr(m);
expr_dependency_ref dep(m); expr_dependency_ref dep(m);
proof * p = m.proofs_enabled() ? prs[i] : nullptr; proof * p = m.proofs_enabled() ? prs.get(i) : nullptr;
m_macro_manager.expand_macros(exprs[i], p, deps[i], r, pr, dep); m_macro_manager.expand_macros(exprs.get(i), p, deps.get(i), r, pr, dep);
m_rewriter(r); m_rewriter(r, rr, prr);
new_exprs.push_back(r); if (pr) pr = m.mk_modus_ponens(pr, prr);
new_prs.push_back(pr); exprs[i] = rr;
new_deps.push_back(dep); 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) { bool quasi_macros::operator()(expr_ref_vector & exprs, proof_ref_vector & prs, expr_dependency_ref_vector & deps) {
if (find_macros(n, exprs)) { unsigned n = exprs.size();
apply_macros(n, exprs, prs, deps, new_exprs, new_prs, new_deps); if (find_macros(n, exprs.c_ptr())) {
apply_macros(exprs, prs, deps);
return true; return true;
} }
else { 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; return false;
} }
} }
void quasi_macros::apply_macros(unsigned n, justified_expr const* fmls, vector<justified_expr>& new_fmls) { void quasi_macros::apply_macros(unsigned n, justified_expr const* fmls, vector<justified_expr>& new_fmls) {
for (unsigned i = 0 ; i < n ; i++) { for (unsigned i = 0 ; i < n ; i++) {
expr_ref r(m); expr_ref r(m), rr(m);
proof_ref pr(m); proof_ref pr(m), prr(m);
proof * p = m.proofs_enabled() ? fmls[i].get_proof() : nullptr; proof * p = m.proofs_enabled() ? fmls[i].get_proof() : nullptr;
expr_dependency_ref dep(m); expr_dependency_ref dep(m);
m_macro_manager.expand_macros(fmls[i].get_fml(), p, nullptr, r, pr, dep); m_macro_manager.expand_macros(fmls[i].get_fml(), p, nullptr, r, pr, dep);
m_rewriter(r); m_rewriter(r, rr, prr);
new_fmls.push_back(justified_expr(m, r, pr)); 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<jus
} }
else { else {
// just copy them over // just copy them over
for ( unsigned i = 0 ; i < n ; i++ ) { for (unsigned i = 0 ; i < n ; i++ ) {
new_fmls.push_back(fmls[i]); new_fmls.push_back(fmls[i]);
} }
return false; return false;

5
src/ast/macros/quasi_macros.h
View file

@ -55,8 +55,7 @@ class quasi_macros {
void find_occurrences(expr * e); void find_occurrences(expr * e);
bool find_macros(unsigned n, expr * const * exprs); bool find_macros(unsigned n, expr * const * exprs);
bool find_macros(unsigned n, justified_expr const* expr); bool find_macros(unsigned n, justified_expr const* expr);
void apply_macros(unsigned n, expr * const * exprs, proof * const * prs, expr_dependency * const* deps, void apply_macros(expr_ref_vector & exprs, proof_ref_vector & prs, expr_dependency_ref_vector& deps);
expr_ref_vector & new_exprs, proof_ref_vector & new_prs, expr_dependency_ref_vector& new_deps);
void apply_macros(unsigned n, justified_expr const* fmls, vector<justified_expr>& new_fmls); void apply_macros(unsigned n, justified_expr const* fmls, vector<justified_expr>& new_fmls);
public: 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, 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<justified_expr>& new_fmls); bool operator()(unsigned n, justified_expr const* fmls, vector<justified_expr>& 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);
}; };

2
src/tactic/goal.cpp
View file

@ -18,6 +18,7 @@ Revision History:
--*/ --*/
#include "ast/ast_ll_pp.h" #include "ast/ast_ll_pp.h"
#include "ast/ast_smt2_pp.h" #include "ast/ast_smt2_pp.h"
#include "ast/ast_pp.h"
#include "ast/for_each_expr.h" #include "ast/for_each_expr.h"
#include "ast/well_sorted.h" #include "ast/well_sorted.h"
#include "ast/display_dimacs.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); SASSERT(!m().proofs_enabled() || pr);
if (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)); SASSERT(f == m().get_fact(pr));
slow_process(f, pr, d); slow_process(f, pr, d);
} }

19
src/tactic/ufbv/quasi_macros_tactic.cpp
View file

@ -44,11 +44,10 @@ class quasi_macros_tactic : public tactic {
macro_manager mm(m_manager); macro_manager mm(m_manager);
quasi_macros qm(m_manager, mm); quasi_macros qm(m_manager, mm);
bool more = true;
expr_ref_vector forms(m_manager), new_forms(m_manager); expr_ref_vector forms(m_manager);
proof_ref_vector proofs(m_manager), new_proofs(m_manager); proof_ref_vector proofs(m_manager);
expr_dependency_ref_vector deps(m_manager), new_deps(m_manager); expr_dependency_ref_vector deps(m_manager);
unsigned size = g->size(); unsigned size = g->size();
for (unsigned i = 0; i < size; i++) { for (unsigned i = 0; i < size; i++) {
@ -60,19 +59,11 @@ class quasi_macros_tactic : public tactic {
do { do {
if (m().canceled()) if (m().canceled())
throw tactic_exception(m().limit().get_cancel_msg()); 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(); 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), g->assert_expr(forms.get(i),
produce_proofs ? proofs.get(i) : nullptr, produce_proofs ? proofs.get(i) : nullptr,
produce_unsat_cores ? deps.get(i, nullptr) : nullptr); produce_unsat_cores ? deps.get(i, nullptr) : nullptr);