From 061ac0f23e13e18f842d9afda13bc4d4108feb7a Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Mon, 5 Jan 2015 16:44:33 -0800 Subject: [PATCH] populate proofs in opt specific tactics Signed-off-by: Nikolaj Bjorner --- src/duality/duality_rpfp.cpp | 2 +- src/tactic/arith/card2bv_tactic.cpp | 10 ++++++++-- src/tactic/arith/lia2card_tactic.cpp | 6 +++++- src/tactic/arith/lia2pb_tactic.cpp | 7 +++++-- 4 files changed, 19 insertions(+), 6 deletions(-) diff --git a/src/duality/duality_rpfp.cpp b/src/duality/duality_rpfp.cpp index cdc8fb3b2..cb71bd99c 100755 --- a/src/duality/duality_rpfp.cpp +++ b/src/duality/duality_rpfp.cpp @@ -3147,7 +3147,7 @@ namespace Duality { } if(node->Annotation.IsEmpty() || eq(node->Annotation.Formula,prev_annot) || (repeated_case_count > 0 && !axioms_added) || (repeated_case_count >= 10)){ - looks_bad: +// looks_bad: if(!axioms_added){ // add the axioms in the off chance they are useful const std::vector &theory = ls->get_axioms(); diff --git a/src/tactic/arith/card2bv_tactic.cpp b/src/tactic/arith/card2bv_tactic.cpp index e5f699eaa..933b687b4 100644 --- a/src/tactic/arith/card2bv_tactic.cpp +++ b/src/tactic/arith/card2bv_tactic.cpp @@ -487,11 +487,17 @@ public: unsigned size = g->size(); expr_ref new_f1(m), new_f2(m); + proof_ref new_pr1(m), new_pr2(m); for (unsigned idx = 0; idx < size; idx++) { - m_rw1(g->form(idx), new_f1); + m_rw1(g->form(idx), new_f1, new_pr1); TRACE("card2bv", tout << "Rewriting " << mk_ismt2_pp(new_f1.get(), m) << std::endl;); m_rw2.rewrite(new_f1, new_f2); - g->update(idx, new_f2, g->pr(idx), g->dep(idx)); + if (m.proofs_enabled()) { + new_pr1 = m.mk_modus_ponens(g->pr(idx), new_pr1); + new_pr2 = m.mk_rewrite(new_f1, new_f2); + new_pr1 = m.mk_modus_ponens(new_pr1, new_pr2); + } + g->update(idx, new_f2, new_pr1, g->dep(idx)); } for (unsigned i = 0; i < m_rw2.lemmas().size(); ++i) { g->assert_expr(m_rw2.lemmas()[i].get()); diff --git a/src/tactic/arith/lia2card_tactic.cpp b/src/tactic/arith/lia2card_tactic.cpp index 7ed867155..0afbe62f1 100644 --- a/src/tactic/arith/lia2card_tactic.cpp +++ b/src/tactic/arith/lia2card_tactic.cpp @@ -89,7 +89,11 @@ public: for (unsigned i = 0; i < g->size(); i++) { expr * curr = g->form(i); - sub(curr, new_curr); + sub(curr, new_curr); + if (m.proofs_enabled()) { + new_pr = m.mk_rewrite(curr, new_curr); + new_pr = m.mk_modus_ponens(g->pr(i), new_pr); + } g->update(i, new_curr, new_pr, g->dep(i)); } g->inc_depth(); diff --git a/src/tactic/arith/lia2pb_tactic.cpp b/src/tactic/arith/lia2pb_tactic.cpp index 33d5f138e..8d200c80d 100644 --- a/src/tactic/arith/lia2pb_tactic.cpp +++ b/src/tactic/arith/lia2pb_tactic.cpp @@ -293,9 +293,12 @@ class lia2pb_tactic : public tactic { m_rw(curr, new_curr, new_pr); if (m_produce_unsat_cores) { dep = m.mk_join(m_rw.get_used_dependencies(), g->dep(idx)); - m_rw.reset_used_dependencies(); + m_rw.reset_used_dependencies(); } - g->update(idx, new_curr, 0, dep); + if (m.proofs_enabled()) { + new_pr = m.mk_modus_ponens(g->pr(idx), new_pr); + } + g->update(idx, new_curr, new_pr, dep); } g->inc_depth(); result.push_back(g.get());