mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-06 22:23:22 +00:00
Code Activity

fix #3554

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2020-03-30 15:02:55 -07:00
parent 0ca5f59e35
commit 8a961a5ce9
5 changed files with 8 additions and 9 deletions
Download patch file Download diff file Expand all files Collapse all files

1
src/ast/ast.cpp
View file

@ -3353,7 +3353,6 @@ proof * ast_manager::mk_redundant_del(expr* e) {
proof * ast_manager::mk_clause_trail(unsigned n, proof* const* ps) { proof * ast_manager::mk_clause_trail(unsigned n, proof* const* ps) {
ptr_buffer<expr> args; ptr_buffer<expr> args;
args.append(n, (expr**) ps); args.append(n, (expr**) ps);
args.push_back(mk_false());
return mk_app(m_basic_family_id, PR_CLAUSE_TRAIL, 0, nullptr, args.size(), args.c_ptr()); return mk_app(m_basic_family_id, PR_CLAUSE_TRAIL, 0, nullptr, args.size(), args.c_ptr());
} }

6
src/smt/smt_clause_proof.cpp
View file

@ -114,7 +114,7 @@ namespace smt {
} }
} }
proof_ref clause_proof::get_proof() { proof_ref clause_proof::get_proof(bool inconsistent) {
TRACE("context", tout << "get-proof " << ctx.get_fparams().m_clause_proof << "\n";); TRACE("context", tout << "get-proof " << ctx.get_fparams().m_clause_proof << "\n";);
if (!ctx.get_fparams().m_clause_proof) { if (!ctx.get_fparams().m_clause_proof) {
return proof_ref(m); return proof_ref(m);
@ -141,8 +141,8 @@ namespace smt {
break; break;
} }
} }
proof_ref result(m.mk_clause_trail(ps.size(), ps.c_ptr()), m); ps.push_back(m.mk_bool_val(!inconsistent));
return result; return proof_ref(m.mk_clause_trail(ps.size(), ps.c_ptr()), m);
} }
std::ostream& operator<<(std::ostream& out, clause_proof::status st) { std::ostream& operator<<(std::ostream& out, clause_proof::status st) {

2
src/smt/smt_clause_proof.h
View file

@ -67,7 +67,7 @@ namespace smt {
void add(clause& c); void add(clause& c);
void add(unsigned n, literal const* lits, clause_kind k, justification* j); void add(unsigned n, literal const* lits, clause_kind k, justification* j);
void del(clause& c); void del(clause& c);
proof_ref get_proof(); proof_ref get_proof(bool inconsistent);
}; };
std::ostream& operator<<(std::ostream& out, clause_proof::status st); std::ostream& operator<<(std::ostream& out, clause_proof::status st);

4
src/smt/smt_context.cpp
View file

@ -4173,7 +4173,7 @@ namespace smt {
return true; return true;
} }
else if (m_fparams.m_clause_proof && !m.proofs_enabled()) { else if (m_fparams.m_clause_proof && !m.proofs_enabled()) {
m_unsat_proof = m_clause_proof.get_proof(); m_unsat_proof = m_clause_proof.get_proof(inconsistent());
} }
else if (m.proofs_enabled()) { else if (m.proofs_enabled()) {
m_unsat_proof = m_conflict_resolution->get_lemma_proof(); m_unsat_proof = m_conflict_resolution->get_lemma_proof();
@ -4500,7 +4500,7 @@ namespace smt {
proof * context::get_proof() { proof * context::get_proof() {
if (!m_unsat_proof) { if (!m_unsat_proof) {
m_unsat_proof = m_clause_proof.get_proof(); m_unsat_proof = m_clause_proof.get_proof(inconsistent());
} }
TRACE("context", tout << m_unsat_proof << "\n";); TRACE("context", tout << m_unsat_proof << "\n";);
return m_unsat_proof; return m_unsat_proof;

4
src/smt/tactic/smt_tactic.cpp
View file

@ -208,7 +208,7 @@ public:
} }
SASSERT(m_ctx); SASSERT(m_ctx);
m_ctx->collect_statistics(m_stats); m_ctx->collect_statistics(m_stats);
proof * pr = m_ctx->get_proof(); proof_ref pr(m_ctx->get_proof(), m);
TRACE("smt_tactic", tout << r << " " << pr << "\n";); TRACE("smt_tactic", tout << r << " " << pr << "\n";);
switch (r) { switch (r) {
case l_true: { case l_true: {
@ -267,7 +267,7 @@ public:
result.push_back(in.get()); result.push_back(in.get());
if (pr) { if (pr) {
in->reset(); in->reset();
in->assert_expr(m.mk_const(symbol("trail"), m.mk_bool_sort()), pr, nullptr); in->assert_expr(m.get_fact(pr), pr, nullptr);
} }
if (m_candidate_models) { if (m_candidate_models) {
switch (m_ctx->last_failure()) { switch (m_ctx->last_failure()) {