mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-07 09:55:19 +00:00
Code Activity

more graceful proof checks

Browse source
This commit is contained in:
Nikolaj Bjorner 2020-11-27 14:40:46 -08:00
parent 6771e44d93
commit 67a8492bd0
3 changed files with 12 additions and 7 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

12
src/ast/proofs/proof_checker.cpp
View file

@ -104,8 +104,7 @@ bool proof_checker::check(proof* p, expr_ref_vector& side_conditions) {
m_todo.pop_back(); m_todo.pop_back();
result = check1(curr.get(), side_conditions); result = check1(curr.get(), side_conditions);
if (!result) { if (!result) {
IF_VERBOSE(0, ast_ll_pp(verbose_stream() << "Proof check failed\n", m, curr.get());); IF_VERBOSE(1, ast_ll_pp(verbose_stream() << "Proof check failed\n", m, curr.get()););
UNREACHABLE();
} }
} }
@ -1393,7 +1392,7 @@ bool proof_checker::check_arith_proof(proof* p) {
} }
} }
unsigned num_parents = m.get_num_parents(p); unsigned num_parents = m.get_num_parents(p);
for (unsigned i = 0; i < num_parents; i++) { for (unsigned i = 0; i < num_parents; i++) {
proof * a = m.get_parent(p, i); proof * a = m.get_parent(p, i);
SASSERT(m.has_fact(a)); SASSERT(m.has_fact(a));
@ -1401,6 +1400,11 @@ bool proof_checker::check_arith_proof(proof* p) {
return false; return false;
} }
} }
TRACE("proof_checker",
for (unsigned i = 0; i < num_parents; i++)
tout << coeffs[i] << " * " << mk_bounded_pp(m.get_fact(m.get_parent(p, i)), m) << "\n";
tout << "fact:" << mk_bounded_pp(fact, m) << "\n";);
if (m.is_or(fact)) { if (m.is_or(fact)) {
app* disj = to_app(fact); app* disj = to_app(fact);
unsigned num_args = disj->get_num_args(); unsigned num_args = disj->get_num_args();
@ -1435,7 +1439,7 @@ bool proof_checker::check_arith_proof(proof* p) {
rw(sum); rw(sum);
if (!m.is_false(sum)) { if (!m.is_false(sum)) {
IF_VERBOSE(0, verbose_stream() << "Arithmetic proof check failed: " << mk_pp(sum, m) << "\n";); IF_VERBOSE(1, verbose_stream() << "Arithmetic proof check failed: " << mk_pp(sum, m) << "\n";);
m_dump_lemmas = true; m_dump_lemmas = true;
dump_proof(p); dump_proof(p);
return false; return false;

4
src/ast/proofs/proof_utils.h
View file

@ -122,7 +122,7 @@ public:
{ {
DEBUG_CODE(proof_checker pc(m); DEBUG_CODE(proof_checker pc(m);
expr_ref_vector side(m); expr_ref_vector side(m);
SASSERT(pc.check(pr, side)); if (!pc.check(pr, side)) IF_VERBOSE(1, verbose_stream() << "check failed: " << mk_pp(pr, m) << "\n");
); );
obj_map<app, app*> cache; obj_map<app, app*> cache;
bool_rewriter brwr(m); bool_rewriter brwr(m);
@ -236,7 +236,7 @@ public:
DEBUG_CODE( DEBUG_CODE(
proof_checker pc(m); proof_checker pc(m);
expr_ref_vector side(m); expr_ref_vector side(m);
SASSERT(pc.check(r, side)); if (!pc.check(r, side)) IF_VERBOSE(1, verbose_stream() << mk_pp(r, m) << "check failed\n");
); );
res = r ; res = r ;

3
src/smt/theory_arith_core.h
View file

@ -2534,7 +2534,8 @@ namespace smt {
b1->push_justification(ante, numeral(1), coeffs_enabled()); b1->push_justification(ante, numeral(1), coeffs_enabled());
b2->push_justification(ante, numeral(1), coeffs_enabled()); b2->push_justification(ante, numeral(1), coeffs_enabled());
TRACE("arith_conflict", tout << "bound conflict v" << b1->get_var() << "\n"; TRACE("arith_conflict", tout << "bound conflict v" << b1->get_var() << "\n";
tout << "bounds: " << b1 << " " << b2 << "\n";); display_bound(tout, b1, 0);
display_bound(tout, b2, 0););
set_conflict(ante, ante, "farkas"); set_conflict(ante, ante, "farkas");
} }