mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-07-31 00:13:16 +00:00
Code Activity

fix #3538, turn on proof checking assertions in goal.cpp for earlier coverage

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2020-03-28 12:54:06 -07:00
parent 907d310600
commit 1a995da0ae
4 changed files with 15 additions and 8 deletions
Download patch file Download diff file Expand all files Collapse all files

9
src/ast/rewriter/pb2bv_rewriter.cpp
View file

@ -936,6 +936,9 @@ struct pb2bv_rewriter::imp {
bool flat_assoc(func_decl * f) const { return false; } bool flat_assoc(func_decl * f) const { return false; }
br_status reduce_app(func_decl * f, unsigned num, expr * const * args, expr_ref & result, proof_ref & result_pr) { br_status reduce_app(func_decl * f, unsigned num, expr * const * args, expr_ref & result, proof_ref & result_pr) {
result_pr = nullptr; result_pr = nullptr;
if (m_r.m.proofs_enabled()) {
return BR_FAILED;
}
return m_r.mk_app_core(f, num, args, result); return m_r.mk_app_core(f, num, args, result);
} }
card2bv_rewriter_cfg(imp& i, ast_manager & m):m_r(i, m) {} card2bv_rewriter_cfg(imp& i, ast_manager & m):m_r(i, m) {}
@ -958,9 +961,13 @@ struct pb2bv_rewriter::imp {
void set_min_arity(unsigned ma) { m_cfg.set_min_arity(ma); } void set_min_arity(unsigned ma) { m_cfg.set_min_arity(ma); }
void rewrite(bool full, expr* e, expr_ref& r, proof_ref& p) { void rewrite(bool full, expr* e, expr_ref& r, proof_ref& p) {
expr_ref ee(e, m()); expr_ref ee(e, m());
if (m().proofs_enabled()) {
r = e;
return;
}
proof_ref rp(m());
if (m_cfg.m_r.mk_app(full, e, r)) { if (m_cfg.m_r.mk_app(full, e, r)) {
ee = r; ee = r;
// mp proof?
} }
(*this)(ee, r, p); (*this)(ee, r, p);
} }

2
src/tactic/arith/card2bv_tactic.cpp
View file

@ -65,8 +65,8 @@ public:
} }
expr_ref new_f1(m), new_f2(m); expr_ref new_f1(m), new_f2(m);
proof_ref new_pr1(m), new_pr2(m);
for (unsigned idx = 0; !g->inconsistent() && idx < g->size(); idx++) { for (unsigned idx = 0; !g->inconsistent() && idx < g->size(); idx++) {
proof_ref new_pr1(m), new_pr2(m);
rw1(g->form(idx), new_f1, new_pr1); rw1(g->form(idx), new_f1, new_pr1);
TRACE("card2bv", tout << "Rewriting " << new_f1 << "\n" << new_pr1 << std::endl;); TRACE("card2bv", tout << "Rewriting " << new_f1 << "\n" << new_pr1 << std::endl;);
rw2(false, new_f1, new_f2, new_pr2); rw2(false, new_f1, new_f2, new_pr2);

6
src/tactic/arith/lia2card_tactic.cpp
View file

@ -204,11 +204,11 @@ public:
if (g->form(i) != tmp && m.proofs_enabled()) { if (g->form(i) != tmp && m.proofs_enabled()) {
pr1 = m.mk_rewrite(g->form(i), tmp); pr1 = m.mk_rewrite(g->form(i), tmp);
} }
m_rw(tmp, new_curr, new_pr); m_rw(tmp, new_curr, pr2);
if (m.proofs_enabled() && tmp != new_curr) { if (m.proofs_enabled() && tmp != new_curr && !pr2) {
pr2 = m.mk_rewrite(tmp, new_curr); pr2 = m.mk_rewrite(tmp, new_curr);
} }
if (m.proofs_enabled()) { if (m.proofs_enabled() && g->pr(i)) {
new_pr = m.mk_transitivity(pr1, pr2); new_pr = m.mk_transitivity(pr1, pr2);
new_pr = m.mk_modus_ponens(g->pr(i), new_pr); new_pr = m.mk_modus_ponens(g->pr(i), new_pr);
} }

6
src/tactic/goal.cpp
View file

@ -133,7 +133,7 @@ void goal::push_back(expr * f, proof * pr, expr_dependency * d) {
m().push_back(m_dependencies, saved_d); m().push_back(m_dependencies, saved_d);
} }
else { else {
// SASSERT(!pr || m().get_fact(pr) == f); SASSERT(!pr || m().get_fact(pr) == f);
SASSERT(!m_inconsistent); SASSERT(!m_inconsistent);
m().push_back(m_forms, f); m().push_back(m_forms, f);
m().push_back(m_proofs, pr); m().push_back(m_proofs, pr);
@ -253,7 +253,7 @@ void goal::assert_expr(expr * f, proof * pr, expr_dependency * d) {
return; return;
} }
if (pr) { if (pr) {
// SASSERT(f == m().get_fact(pr)); SASSERT(f == m().get_fact(pr));
slow_process(f, pr, d); slow_process(f, pr, d);
} }
else { else {
@ -284,7 +284,7 @@ void goal::update(unsigned i, expr * f, proof * pr, expr_dependency * d) {
if (m_inconsistent) if (m_inconsistent)
return; return;
if (pr) { if (pr) {
// SASSERT(f == m().get_fact(pr)); SASSERT(f == m().get_fact(pr));
expr_ref out_f(m()); expr_ref out_f(m());
proof_ref out_pr(m()); proof_ref out_pr(m());
slow_process(true, f, pr, d, out_f, out_pr); slow_process(true, f, pr, d, out_f, out_pr);