From 6e8d9001dca05f3e5eccbb10bcaa6880b2034cca Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Wed, 8 Apr 2020 11:08:45 -0700 Subject: [PATCH] fix #3843 Signed-off-by: Nikolaj Bjorner --- src/ast/ast.cpp | 4 +++- src/ast/rewriter/rewriter.cpp | 4 ++-- src/ast/rewriter/rewriter_def.h | 14 ++++++++------ src/muz/base/hnf.cpp | 2 +- 4 files changed, 14 insertions(+), 10 deletions(-) diff --git a/src/ast/ast.cpp b/src/ast/ast.cpp index 49ff2426b..7e4607e1c 100644 --- a/src/ast/ast.cpp +++ b/src/ast/ast.cpp @@ -2823,7 +2823,7 @@ proof * ast_manager::mk_modus_ponens(proof * p1, proof * p2) { SASSERT(is_implies(get_fact(p2)) || is_eq(get_fact(p2)) || is_oeq(get_fact(p2))); CTRACE("mk_modus_ponens", to_app(get_fact(p2))->get_arg(0) != get_fact(p1), tout << mk_pp(get_fact(p1), *this) << "\n" << mk_pp(get_fact(p2), *this) << "\n";); - SASSERT(to_app(get_fact(p2))->get_arg(0) == get_fact(p1)); + SASSERT(!proofs_enabled() || to_app(get_fact(p2))->get_arg(0) == get_fact(p1)); CTRACE("mk_modus_ponens", !is_ground(p2) && !has_quantifiers(p2), tout << "Non-ground: " << mk_pp(p2, *this) << "\n";); CTRACE("mk_modus_ponens", !is_ground(p1) && !has_quantifiers(p1), tout << "Non-ground: " << mk_pp(p1, *this) << "\n";); if (is_reflexivity(p2)) @@ -2887,6 +2887,8 @@ proof * ast_manager::mk_transitivity(proof * p1, proof * p2) { return p2; if (!p2) return p1; + if (proofs_disabled()) + return nullptr; SASSERT(has_fact(p1)); SASSERT(has_fact(p2)); SASSERT(is_app(get_fact(p1))); diff --git a/src/ast/rewriter/rewriter.cpp b/src/ast/rewriter/rewriter.cpp index 551e59e0e..8138cff04 100644 --- a/src/ast/rewriter/rewriter.cpp +++ b/src/ast/rewriter/rewriter.cpp @@ -43,11 +43,11 @@ void rewriter_core::del_cache_stack() { } bool rewriter_core::rewrites_from(expr* t, proof* p) { - return !p || (to_app(m().get_fact(p))->get_arg(0) == t); + return !p || m().proofs_disabled() || (to_app(m().get_fact(p))->get_arg(0) == t); } bool rewriter_core::rewrites_to(expr* t, proof* p) { - return !p || (to_app(m().get_fact(p))->get_arg(1) == t); + return !p || m().proofs_disabled() || (to_app(m().get_fact(p))->get_arg(1) == t); } diff --git a/src/ast/rewriter/rewriter_def.h b/src/ast/rewriter/rewriter_def.h index 1cb07a0ee..8fe1c3747 100644 --- a/src/ast/rewriter/rewriter_def.h +++ b/src/ast/rewriter/rewriter_def.h @@ -242,7 +242,6 @@ bool rewriter_tpl::constant_fold(app * t, frame & fr) { template template void rewriter_tpl::process_app(app * t, frame & fr) { - // SASSERT(t->get_num_args() > 0); SASSERT(!frame_stack().empty()); switch (fr.m_state) { case PROCESS_CHILDREN: { @@ -311,13 +310,14 @@ void rewriter_tpl::process_app(app * t, frame & fr) { result_stack().push_back(m_r); if (ProofGen) { result_pr_stack().shrink(fr.m_spos); - if (!m_pr2) + if (!m_pr2) { m_pr2 = m().mk_rewrite(new_t, m_r); + } m_pr = m().mk_transitivity(m_pr, m_pr2); - m_pr2 = nullptr; result_pr_stack().push_back(m_pr); SASSERT(rewrites_to(m_r, m_pr)); SASSERT(rewrites_from(t, m_pr)); + m_pr2 = nullptr; } if (st == BR_DONE) { cache_result(t, m_r, m_pr, fr.m_cache_result); @@ -346,12 +346,14 @@ void rewriter_tpl::process_app(app * t, frame & fr) { result_pr_stack().pop_back(); pr1 = result_pr_stack().back(); result_pr_stack().pop_back(); + SASSERT(rewrites_from(t, pr1)); + SASSERT(rewrites_to(m_r, pr1)); + SASSERT(rewrites_from(m_r, pr2)); + SASSERT(rewrites_to(result_stack().back(), pr2)); m_pr = m().mk_transitivity(pr1, pr2); result_pr_stack().push_back(m_pr); } - m_r = result_stack().back(); - SASSERT(rewrites_to(m_r, m_pr)); - SASSERT(rewrites_from(t, m_pr)); + m_r = result_stack().back(); result_stack().pop_back(); result_stack().pop_back(); result_stack().push_back(m_r); diff --git a/src/muz/base/hnf.cpp b/src/muz/base/hnf.cpp index a9a0b4692..1ab208c9e 100644 --- a/src/muz/base/hnf.cpp +++ b/src/muz/base/hnf.cpp @@ -473,7 +473,7 @@ private: p2 = m.mk_oeq_congruence(e2, fml, defs.size(), defs.c_ptr()); p3 = mk_transitivity(p1, p2); defs.reset(); - return proof_ref(p3, m); + return p3; } }