mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-11-04 13:29:11 +00:00
Code Activity

fixes to clause proof tracking

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2018-05-29 15:40:39 -07:00 • committed by Arie Gurfinkel
parent f7d015de8d
commit 0c2e3c0894
5 changed files with 19 additions and 37 deletions
Download patch file Download diff file Expand all files Collapse all files

4
src/muz/spacer/spacer_antiunify.cpp
View file

@ -57,8 +57,8 @@ struct var_abs_rewriter : public default_rewriter_cfg {
{
bool contains_const_child = false;
app* a = to_app(t);
for (unsigned i=0, sz = a->get_num_args(); i < sz; ++i) {
if (m_util.is_numeral(a->get_arg(i))) {
for (expr * arg : *a) {
if (m_util.is_numeral(arg)) {
contains_const_child = true;
}
}

1
src/smt/smt_conflict_resolution.cpp
View file

@ -1033,6 +1033,7 @@ namespace smt {
return pr;
}
SASSERT(js != 0);
TRACE("proof_gen_bug", tout << js << "\n";);
m_todo_pr.push_back(tp_elem(js));
return nullptr;
}

2
src/smt/smt_conflict_resolution.h
View file

@ -96,7 +96,7 @@ namespace smt {
};
tp_elem(literal l):m_kind(LITERAL), m_lidx(l.index()) {}
tp_elem(enode * lhs, enode * rhs):m_kind(EQUALITY), m_lhs(lhs), m_rhs(rhs) {}
tp_elem(justification * js):m_kind(JUSTIFICATION), m_js(js) {}
tp_elem(justification * js):m_kind(JUSTIFICATION), m_js(js) { SASSERT(js);}
};
svector<tp_elem> m_todo_pr;

46
src/smt/smt_context.cpp
View file

@ -3144,8 +3144,14 @@ namespace smt {
mark_as_relevant(lit);
m_clause_lits.push_back(get_literal(lit));
}
if (m_clause_lits.size() > 2)
m_clause = clause::mk(m_manager, m_clause_lits.size(), m_clause_lits.c_ptr(), CLS_AUX);
if (m_clause_lits.size() >= 2) {
justification* js = nullptr;
if (m_manager.proofs_enabled()) {
proof * pr = mk_clause_def_axiom(m_clause_lits.size(), m_clause_lits.c_ptr(), nullptr);
js = mk_justification(justification_proof_wrapper(*this, pr));
}
m_clause = clause::mk(m_manager, m_clause_lits.size(), m_clause_lits.c_ptr(), CLS_AUX, js);
}
}
lbool context::decide_clause() {
@ -3163,38 +3169,12 @@ namespace smt {
return l_undef;
}
}
for (unsigned i = m_assigned_literals.size(); i-- > 0; ) {
literal nlit = ~m_assigned_literals[i];
if (m_clause_lits.contains(nlit)) {
switch (m_clause_lits.size()) {
case 1: {
b_justification js;
set_conflict(js, ~nlit);
break;
}
case 2: {
if (nlit == m_clause_lits[1]) {
std::swap(m_clause_lits[0], m_clause_lits[1]);
}
b_justification js(~m_clause_lits[1]);
set_conflict(js, ~nlit);
break;
}
default: {
for (unsigned j = 0, sz = m_clause->get_num_literals(); j < sz; ++j) {
if (m_clause->get_literal(j) == nlit) {
if (j > 0) m_clause->swap_lits(j, 0);
break;
}
}
b_justification js(m_clause);
set_conflict(js, ~nlit);
break;
}
}
break;
}
if (m_clause_lits.size() == 1) {
set_conflict(b_justification(), ~m_clause_lits[0]);
}
else {
set_conflict(b_justification(m_clause), null_literal);
}
VERIFY(!resolve_conflict());
return l_false;
}

3
src/smt/smt_setup.cpp
View file

@ -730,7 +730,8 @@ namespace smt {
}
void setup::setup_i_arith() {
m_context.register_plugin(alloc(smt::theory_i_arith, m_manager, m_params));
m_context.register_plugin(alloc(smt::theory_lra, m_manager, m_params));
// m_context.register_plugin(alloc(smt::theory_i_arith, m_manager, m_params));
}
void setup::setup_r_arith() {