From 6ca039c855f2fcf2e3bd1791fe73dd848d872c73 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sat, 11 Apr 2020 12:30:03 -0700 Subject: [PATCH] fix #3919 Signed-off-by: Nikolaj Bjorner --- src/ast/fpa/fpa2bv_rewriter.cpp | 16 ++++++++++------ src/tactic/fpa/fpa2bv_tactic.cpp | 30 ++++++++++++------------------ 2 files changed, 22 insertions(+), 24 deletions(-) diff --git a/src/ast/fpa/fpa2bv_rewriter.cpp b/src/ast/fpa/fpa2bv_rewriter.cpp index b9a8a346c..6c3e70017 100644 --- a/src/ast/fpa/fpa2bv_rewriter.cpp +++ b/src/ast/fpa/fpa2bv_rewriter.cpp @@ -186,12 +186,13 @@ bool fpa2bv_rewriter_cfg::pre_visit(expr * t) } -bool fpa2bv_rewriter_cfg::reduce_quantifier(quantifier * old_q, - expr * new_body, - expr * const * new_patterns, - expr * const * new_no_patterns, - expr_ref & result, - proof_ref & result_pr) { +bool fpa2bv_rewriter_cfg::reduce_quantifier( + quantifier * old_q, + expr * new_body, + expr * const * new_patterns, + expr * const * new_no_patterns, + expr_ref & result, + proof_ref & result_pr) { if (is_lambda(old_q)) { return false; } @@ -228,6 +229,9 @@ bool fpa2bv_rewriter_cfg::reduce_quantifier(quantifier * old_q, new_body, old_q->get_weight(), old_q->get_qid(), old_q->get_skid(), old_q->get_num_patterns(), new_patterns, old_q->get_num_no_patterns(), new_no_patterns); result_pr = nullptr; + if (m().proofs_enabled()) { + result_pr = m().mk_rewrite(old_q, result); + } m_bindings.shrink(old_sz); TRACE("fpa2bv", tout << "reduce_quantifier[" << old_q->get_depth() << "]: " << mk_ismt2_pp(old_q->get_expr(), m()) << std::endl << diff --git a/src/tactic/fpa/fpa2bv_tactic.cpp b/src/tactic/fpa/fpa2bv_tactic.cpp index e7804e05e..13cb4c3e7 100644 --- a/src/tactic/fpa/fpa2bv_tactic.cpp +++ b/src/tactic/fpa/fpa2bv_tactic.cpp @@ -29,17 +29,10 @@ class fpa2bv_tactic : public tactic { fpa2bv_rewriter m_rw; unsigned m_num_steps; - bool m_proofs_enabled; - bool m_produce_models; - bool m_produce_unsat_cores; - imp(ast_manager & _m, params_ref const & p): m(_m), m_conv(m), - m_rw(m, m_conv, p), - m_proofs_enabled(false), - m_produce_models(false), - m_produce_unsat_cores(false) { + m_rw(m, m_conv, p) { } void updt_params(params_ref const & p) { @@ -48,15 +41,12 @@ class fpa2bv_tactic : public tactic { void operator()(goal_ref const & g, goal_ref_buffer & result) { - m_proofs_enabled = g->proofs_enabled(); - m_produce_models = g->models_enabled(); - m_produce_unsat_cores = g->unsat_core_enabled(); - + bool proofs_enabled = g->proofs_enabled(); result.reset(); tactic_report report("fpa2bv", *g); m_rw.reset(); - TRACE("fpa2bv", tout << "BEFORE: " << std::endl; g->display(tout);); + TRACE("fpa2bv", g->display(tout << "BEFORE: " << std::endl);); if (g->inconsistent()) { result.push_back(g.get()); @@ -73,7 +63,7 @@ class fpa2bv_tactic : public tactic { expr * curr = g->form(idx); m_rw(curr, new_curr, new_pr); m_num_steps += m_rw.get_num_steps(); - if (m_proofs_enabled) { + if (proofs_enabled) { proof * pr = g->pr(idx); new_pr = m.mk_modus_ponens(pr, new_pr); } @@ -101,11 +91,15 @@ class fpa2bv_tactic : public tactic { g->inc_depth(); result.push_back(g.get()); - for (unsigned i = 0; i < m_conv.m_extra_assertions.size(); i++) - result.back()->assert_expr(m_conv.m_extra_assertions[i].get()); + for (expr* e : m_conv.m_extra_assertions) { + proof* pr = nullptr; + if (proofs_enabled) + pr = m.mk_asserted(e); + result.back()->assert_expr(e, pr); + } - TRACE("fpa2bv", tout << "AFTER: " << std::endl; g->display(tout); - if (g->mc()) g->mc()->display(tout); tout << std::endl; ); + TRACE("fpa2bv", g->display(tout << "AFTER:\n"); + if (g->mc()) g->mc()->display(tout); tout << std::endl; ); } };