mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-13 09:26:15 +00:00
Code Activity

fix proof generation for unit resolution. Issue #691

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2016-07-20 11:54:39 -07:00
parent 6559fd817d
commit 5f39c4371c
3 changed files with 10 additions and 6 deletions
Download patch file Download diff file Expand all files Collapse all files

5
src/ast/ast.cpp
View file

@ -2991,7 +2991,10 @@ proof * ast_manager::mk_unit_resolution(unsigned num_proofs, proof * const * pro
for (unsigned i = 0; i < num_proofs; i++) tout << mk_pp(get_fact(proofs[i]), *this) << "\n"; for (unsigned i = 0; i < num_proofs; i++) tout << mk_pp(get_fact(proofs[i]), *this) << "\n";
tout << "===>\n"; tout << "===>\n";
tout << mk_pp(new_fact, *this) << "\n";); tout << mk_pp(new_fact, *this) << "\n";);
SASSERT(num_proofs == cls_sz || (num_proofs == cls_sz + 1 && is_false(new_fact))); //
// typically: num_proofs == cls_sz || (num_proofs == cls_sz + 1 && is_false(new_fact))
// but formula could have repeated literals that are merged in the clausal representation.
//
unsigned num_matches = 0; unsigned num_matches = 0;
for (unsigned i = 0; i < cls_sz; i++) { for (unsigned i = 0; i < cls_sz; i++) {
expr * lit = cls->get_arg(i); expr * lit = cls->get_arg(i);

9
src/smt/smt_internalizer.cpp
View file

@ -1045,15 +1045,13 @@ namespace smt {
bool context::simplify_aux_clause_literals(unsigned & num_lits, literal * lits, literal_buffer & simp_lits) { bool context::simplify_aux_clause_literals(unsigned & num_lits, literal * lits, literal_buffer & simp_lits) {
std::sort(lits, lits + num_lits); std::sort(lits, lits + num_lits);
literal prev = null_literal; literal prev = null_literal;
unsigned i = 0;
unsigned j = 0; unsigned j = 0;
for (; i < num_lits; i++) { for (unsigned i = 0; i < num_lits; i++) {
literal curr = lits[i]; literal curr = lits[i];
lbool val = get_assignment(curr); lbool val = get_assignment(curr);
if (val == l_false)
simp_lits.push_back(~curr);
switch(val) { switch(val) {
case l_false: case l_false:
simp_lits.push_back(~curr);
break; // ignore literal break; // ignore literal
case l_undef: case l_undef:
if (curr == ~prev) if (curr == ~prev)
@ -1295,8 +1293,9 @@ namespace smt {
SASSERT(get_assignment(simp_lits[i]) == l_true); SASSERT(get_assignment(simp_lits[i]) == l_true);
} }
}); });
if (old_num_lits != num_lits) if (!simp_lits.empty()) {
j = mk_justification(unit_resolution_justification(m_region, j, simp_lits.size(), simp_lits.c_ptr())); j = mk_justification(unit_resolution_justification(m_region, j, simp_lits.size(), simp_lits.c_ptr()));
}
break; break;
} }
case CLS_AUX_LEMMA: { case CLS_AUX_LEMMA: {

2
src/smt/smt_justification.cpp
View file

@ -52,6 +52,7 @@ namespace smt {
tout << lits[i] << " "; tout << lits[i] << " ";
} }
tout << "\n";); tout << "\n";);
SASSERT(m_num_literals > 0);
} }
unit_resolution_justification::unit_resolution_justification(justification * js, unit_resolution_justification::unit_resolution_justification(justification * js,
@ -68,6 +69,7 @@ namespace smt {
tout << lits[i] << " "; tout << lits[i] << " ";
} }
tout << "\n";); tout << "\n";);
SASSERT(num_lits != 0);
} }
unit_resolution_justification::~unit_resolution_justification() { unit_resolution_justification::~unit_resolution_justification() {