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

fix #3523

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2020-03-26 09:41:26 -07:00
parent c165f69248
commit 37f080b877
2 changed files with 18 additions and 7 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -106,7 +106,8 @@ bool macro_manager::insert(func_decl * f, quantifier * q, proof * pr, expr_depen
app * head; app * head;
expr * definition; expr * definition;
get_head_def(q, f, head, definition); bool revert = false;
get_head_def(q, f, head, definition, revert);
func_decl_set * s = m_deps.mk_func_decl_set(); func_decl_set * s = m_deps.mk_func_decl_set();
m_deps.collect_func_decls(definition, s); m_deps.collect_func_decls(definition, s);
@ -167,17 +168,19 @@ void macro_manager::mark_forbidden(unsigned n, justified_expr const * exprs) {
} }
void macro_manager::get_head_def(quantifier * q, func_decl * d, app * & head, expr * & def) const { void macro_manager::get_head_def(quantifier * q, func_decl * d, app * & head, expr * & def, bool& revert) const {
app * body = to_app(q->get_expr()); app * body = to_app(q->get_expr());
expr * lhs = nullptr, *rhs = nullptr; expr * lhs = nullptr, *rhs = nullptr;
VERIFY(m.is_eq(body, lhs, rhs)); VERIFY(m.is_eq(body, lhs, rhs));
SASSERT(is_app_of(lhs, d) || is_app_of(rhs, d)); SASSERT(is_app_of(lhs, d) || is_app_of(rhs, d));
SASSERT(!is_app_of(lhs, d) || !is_app_of(rhs, d)); SASSERT(!is_app_of(lhs, d) || !is_app_of(rhs, d));
if (is_app_of(lhs, d)) { if (is_app_of(lhs, d)) {
revert = false;
head = to_app(lhs); head = to_app(lhs);
def = rhs; def = rhs;
} }
else { else {
revert = true;
head = to_app(rhs); head = to_app(rhs);
def = lhs; def = lhs;
} }
@ -191,7 +194,8 @@ void macro_manager::display(std::ostream & out) {
m_decl2macro.find(f, q); m_decl2macro.find(f, q);
app * head; app * head;
expr * def; expr * def;
get_head_def(q, f, head, def); bool r;
get_head_def(q, f, head, def, r);
SASSERT(q); SASSERT(q);
out << mk_pp(head, m) << " ->\n" << mk_pp(def, m) << "\n"; out << mk_pp(head, m) << " ->\n" << mk_pp(def, m) << "\n";
} }
@ -202,7 +206,8 @@ func_decl * macro_manager::get_macro_interpretation(unsigned i, expr_ref & inter
quantifier * q = m_macros.get(i); quantifier * q = m_macros.get(i);
app * head; app * head;
expr * def; expr * def;
get_head_def(q, f, head, def); bool r;
get_head_def(q, f, head, def, r);
TRACE("macro_bug", TRACE("macro_bug",
tout << f->get_name() << "\n" << mk_pp(head, m) << "\n" << mk_pp(q, m) << "\n";); tout << f->get_name() << "\n" << mk_pp(head, m) << "\n" << mk_pp(q, m) << "\n";);
m_util.mk_macro_interpretation(head, q->get_num_decls(), def, interp); m_util.mk_macro_interpretation(head, q->get_num_decls(), def, interp);
@ -256,6 +261,9 @@ struct macro_manager::macro_expander_cfg : public default_rewriter_cfg {
if (erase_patterns) { if (erase_patterns) {
result = m.update_quantifier(old_q, 0, nullptr, 0, nullptr, new_body); result = m.update_quantifier(old_q, 0, nullptr, 0, nullptr, new_body);
} }
if (erase_patterns && m.proofs_enabled()) {
result_pr = m.mk_rewrite(old_q, result);
}
return erase_patterns; return erase_patterns;
} }
@ -270,7 +278,8 @@ struct macro_manager::macro_expander_cfg : public default_rewriter_cfg {
app * head = nullptr; app * head = nullptr;
expr * def = nullptr; expr * def = nullptr;
mm.get_head_def(q, d, head, def); bool revert = false;
mm.get_head_def(q, d, head, def, revert);
unsigned num = n->get_num_args(); unsigned num = n->get_num_args();
SASSERT(head && def); SASSERT(head && def);
TRACE("macro_manager", tout << "expanding: " << mk_pp(n, m) << "\n" << mk_pp(head, m) << " " << mk_pp(def, m) << "\n";); TRACE("macro_manager", tout << "expanding: " << mk_pp(n, m) << "\n" << mk_pp(head, m) << " " << mk_pp(def, m) << "\n";);
@ -293,9 +302,10 @@ struct macro_manager::macro_expander_cfg : public default_rewriter_cfg {
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 = nullptr;
mm.m_decl2macro_pr.find(d, q_pr); mm.m_decl2macro_pr.find(d, q_pr);
SASSERT(q_pr != 0); 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);
} }
else { else {
p = nullptr; p = nullptr;
@ -331,6 +341,7 @@ void macro_manager::expand_macros(expr * n, proof * pr, expr_dependency * dep, e
for (;;) { for (;;) {
macro_expander_rw proc(m, *this); macro_expander_rw proc(m, *this);
proof_ref n_eq_r_pr(m); proof_ref n_eq_r_pr(m);
SASSERT(m.get_fact(old_pr) == old_n);
TRACE("macro_manager_bug", tout << "expand_macros:\n" << mk_pp(n, m) << "\n";); TRACE("macro_manager_bug", tout << "expand_macros:\n" << mk_pp(n, m) << "\n";);
proc(old_n, r, n_eq_r_pr); proc(old_n, r, n_eq_r_pr);
new_pr = m.mk_modus_ponens(old_pr, n_eq_r_pr); new_pr = m.mk_modus_ponens(old_pr, n_eq_r_pr);

2
src/ast/macros/macro_manager.h
View file

@ -83,7 +83,7 @@ public:
func_decl * get_macro_func_decl(unsigned i) const { return m_decls.get(i); } func_decl * get_macro_func_decl(unsigned i) const { return m_decls.get(i); }
func_decl * get_macro_interpretation(unsigned i, expr_ref & interp) const; func_decl * get_macro_interpretation(unsigned i, expr_ref & interp) const;
quantifier * get_macro_quantifier(func_decl * f) const { quantifier * q = nullptr; m_decl2macro.find(f, q); return q; } quantifier * get_macro_quantifier(func_decl * f) const { quantifier * q = nullptr; m_decl2macro.find(f, q); return q; }
void get_head_def(quantifier * q, func_decl * d, app * & head, expr * & def) const; void get_head_def(quantifier * q, func_decl * d, app * & head, expr * & def, bool& revert) const;
void expand_macros(expr * n, proof * pr, expr_dependency * dep, expr_ref & r, proof_ref & new_pr, expr_dependency_ref & new_dep); void expand_macros(expr * n, proof * pr, expr_dependency * dep, expr_ref & r, proof_ref & new_pr, expr_dependency_ref & new_dep);