mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-24 01:25:31 +00:00
Code Activity

fix #3699

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2020-04-02 20:35:15 -07:00
parent 26192e848c
commit be3a9b227c
5 changed files with 34 additions and 47 deletions
Download patch file Download diff file Expand all files Collapse all files

12
src/smt/smt_clause_proof.cpp
View file

@ -15,6 +15,7 @@ Revision History:
#include "smt/smt_clause_proof.h"
#include "smt/smt_context.h"
#include "ast/ast_pp.h"
#include "ast/ast_ll_pp.h"
namespace smt {
clause_proof::clause_proof(context& ctx): ctx(ctx), m(ctx.get_manager()), m_lits(m) {}
@ -42,18 +43,19 @@ namespace smt {
void clause_proof::add(clause& c) {
if (ctx.get_fparams().m_clause_proof) {
justification* j = c.get_justification();
proof* pr = justification2proof(j);
proof_ref pr(justification2proof(j), m);
CTRACE("mk_clause", pr.get(), tout << mk_bounded_pp(pr, m, 4) << "\n";);
update(c, kind2st(c.get_kind()), pr);
}
}
void clause_proof::add(unsigned n, literal const* lits, clause_kind k, justification* j) {
if (ctx.get_fparams().m_clause_proof) {
proof* pr = justification2proof(j);
if (ctx.get_fparams().m_clause_proof) {
proof_ref pr(justification2proof(j), m);
CTRACE("mk_clause", pr.get(), tout << mk_bounded_pp(pr, m, 4) << "\n";);
m_lits.reset();
for (unsigned i = 0; i < n; ++i) {
literal lit = lits[i];
m_lits.push_back(ctx.literal2expr(lit));
m_lits.push_back(ctx.literal2expr(lits[i]));
}
update(kind2st(k), m_lits, pr);
}

9
src/smt/smt_conflict_resolution.cpp
View file

@ -1043,7 +1043,7 @@ namespace smt {
*/
proof * conflict_resolution::get_proof(justification * js) {
proof * pr;
if (m_js2proof.find(js, pr)) {
if (false && m_js2proof.find(js, pr)) {
TRACE("proof_gen_bug", tout << "js2pr_cached: #" << js << "\n";);
return pr;
}
@ -1313,10 +1313,9 @@ namespace smt {
}
else {
proof * prs[2] = { nullptr, nullptr};
m_lit2proof.find(not_l, prs[0]);
SASSERT(prs[0]);
prs[1] = get_proof(consequent, conflict);
SASSERT(prs[1]);
prs[0] = m_lit2proof.find(not_l);
prs[1] = get_proof(consequent, conflict);
SASSERT(prs[0] && prs[1]);
pr = m_manager.mk_unit_resolution(2, prs);
}
expr_ref_buffer lits(m_manager);

1
src/smt/smt_context.cpp
View file

@ -3135,6 +3135,7 @@ namespace smt {
}
expr * f = m_asserted_formulas.get_formula(qhead);
proof * pr = m_asserted_formulas.get_formula_proof(qhead);
SASSERT(!pr || f == m.get_fact(pr));
internalize_assertion(f, pr, 0);
qhead++;
}

20
src/smt/smt_internalizer.cpp
View file

@ -1079,6 +1079,7 @@ namespace smt {
clauses because they are deleted during backtracking.
*/
bool context::simplify_aux_clause_literals(unsigned & num_lits, literal * lits, literal_buffer & simp_lits) {
TRACE("simplify_aux_clause_literals", display_literals(tout, num_lits, lits); tout << "\n";);
std::sort(lits, lits + num_lits);
literal prev = null_literal;
unsigned j = 0;
@ -1087,7 +1088,7 @@ namespace smt {
lbool val = get_assignment(curr);
switch(val) {
case l_false:
TRACE("simplify_aux_clause_literals", display_literal(tout << get_assign_level(curr) << " " << get_scope_level() << " ", curr); tout << "\n"; );
TRACE("simplify_aux_clause_literals", display_literal_verbose(tout << get_assign_level(curr) << " " << get_scope_level() << " " << curr << ":", curr); tout << "\n"; );
simp_lits.push_back(~curr);
break; // ignore literal
// fall through
@ -1131,9 +1132,9 @@ namespace smt {
kind of simplification.
*/
bool context::simplify_aux_lemma_literals(unsigned & num_lits, literal * lits) {
TRACE("simplify_aux_lemma_literals", tout << "1) "; display_literals(tout, num_lits, lits); tout << "\n";);
TRACE("simplify_aux_lemma_literals", display_literals(tout << "1) ", num_lits, lits) << "\n";);
std::sort(lits, lits + num_lits);
TRACE("simplify_aux_lemma_literals", tout << "2) "; display_literals(tout, num_lits, lits); tout << "\n";);
TRACE("simplify_aux_lemma_literals", display_literals(tout << "2) ", num_lits, lits) << "\n";);
literal prev = null_literal;
unsigned i = 0;
unsigned j = 0;
@ -1155,7 +1156,7 @@ namespace smt {
}
}
num_lits = j;
TRACE("simplify_aux_lemma_literals", tout << "3) "; display_literals(tout, num_lits, lits); tout << "\n";);
TRACE("simplify_aux_lemma_literals", display_literals(tout << "3) ", num_lits, lits) << "\n";);
return true;
}
@ -1338,7 +1339,7 @@ namespace smt {
}
break;
}
case CLS_TH_LEMMA: {
case CLS_TH_LEMMA:
if (!simplify_aux_lemma_literals(num_lits, lits)) {
if (j && !j->in_region()) {
j->del_eh(m);
@ -1348,16 +1349,13 @@ namespace smt {
}
// simplify_aux_lemma_literals does not delete literals assigned to false, so
// it is not necessary to create a unit_resolution_justification
break;
}
break;
default:
break;
}
TRACE("mk_clause", tout << "after simplification:\n"; display_literals_verbose(tout, num_lits, lits) << "\n";);
TRACE("mk_clause", display_literals_verbose(tout << "after simplification:\n", num_lits, lits) << "\n";);
unsigned activity = 0;
if (activity == 0)
activity = 1;
unsigned activity = 1;
bool lemma = is_lemma(k);
m_stats.m_num_mk_lits += num_lits;
switch (num_lits) {

39
src/smt/smt_justification.cpp
View file

@ -32,6 +32,7 @@ namespace smt {
void justification_proof_wrapper::del_eh(ast_manager & m) {
m.dec_ref(m_proof);
m_proof = nullptr;
}
proof * justification_proof_wrapper::mk_proof(conflict_resolution & cr) {
@ -47,11 +48,7 @@ namespace smt {
SASSERT(!js || js->in_region());
m_literals = new (r) literal[num_lits];
memcpy(m_literals, lits, sizeof(literal) * num_lits);
TRACE("unit_resolution_justification_bug",
for (unsigned i = 0; i < num_lits; i++) {
tout << lits[i] << " ";
}
tout << "\n";);
TRACE("unit_resolution_justification_bug", tout << literal_vector(num_lits, lits) << "\n";);
SASSERT(m_num_literals > 0);
}
@ -64,11 +61,7 @@ namespace smt {
SASSERT(!js || !js->in_region());
m_literals = alloc_vect<literal>(num_lits);
memcpy(m_literals, lits, sizeof(literal) * num_lits);
TRACE("unit_resolution_justification_bug",
for (unsigned i = 0; i < num_lits; i++) {
tout << lits[i] << " ";
}
tout << "\n";);
TRACE("unit_resolution_justification_bug", tout << literal_vector(num_lits, lits) << "\n";);
SASSERT(num_lits != 0);
}
@ -88,29 +81,23 @@ namespace smt {
proof * unit_resolution_justification::mk_proof(conflict_resolution & cr) {
SASSERT(m_antecedent);
ptr_buffer<proof> prs;
proof * pr = cr.get_proof(m_antecedent);
bool visited = pr != nullptr;
ast_manager& m = cr.get_manager();
proof_ref_vector prs(m);
cr.init_mk_proof();
proof * pr = cr.get_proof(m_antecedent);
if (!pr)
return pr;
prs.push_back(pr);
for (unsigned i = 0; i < m_num_literals; i++) {
proof * pr = cr.get_proof(m_literals[i]);
if (pr == nullptr)
visited = false;
if (!pr)
return pr;
else
prs.push_back(pr);
}
if (!visited)
return nullptr;
ast_manager & m = cr.get_manager();
TRACE("unit_resolution_justification_bug",
tout << "in mk_proof\n";
for (unsigned i = 0; i < m_num_literals; i++) {
tout << m_literals[i] << " ";
}
tout << "\n";
for (unsigned i = 0; i < prs.size(); i++) {
tout << mk_ll_pp(m.get_fact(prs[i]), m);
});
tout << "in mk_proof\n" << literal_vector(m_num_literals, m_literals) << "\n";
for (proof* p : prs) tout << mk_ll_pp(m.get_fact(p), m););
return m.mk_unit_resolution(prs.size(), prs.c_ptr());
}