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

redo marking mechanism as marked literals can disappear from lemma

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2013-12-16 07:50:24 +02:00
parent b1caadee49
commit e38729a1c6
2 changed files with 18 additions and 25 deletions
Download patch file Download diff file Expand all files Collapse all files

39
src/smt/theory_pb.cpp
View file

@ -998,6 +998,7 @@ namespace smt {
m_conseq_index.resize(v+1, null_index); m_conseq_index.resize(v+1, null_index);
} }
SASSERT(!is_marked(v) || m_conseq_index[v] == idx); SASSERT(!is_marked(v) || m_conseq_index[v] == idx);
m_marked.push_back(v);
m_conseq_index[v] = idx; m_conseq_index[v] = idx;
} }
@ -1007,14 +1008,20 @@ namespace smt {
(m_conseq_index[v] != null_index); (m_conseq_index[v] != null_index);
} }
void theory_pb::unset_mark(literal l) { void theory_pb::unset_mark(bool_var v) {
bool_var v = l.var();
SASSERT(v != null_bool_var); SASSERT(v != null_bool_var);
if (v < static_cast<bool_var>(m_conseq_index.size())) { if (v < static_cast<bool_var>(m_conseq_index.size())) {
m_conseq_index[v] = null_index; m_conseq_index[v] = null_index;
} }
} }
void theory_pb::unset_marks() {
for (unsigned i = 0; i < m_marked.size(); ++i) {
unset_mark(m_marked[i]);
}
m_marked.reset();
}
void theory_pb::process_antecedent(literal l, numeral coeff) { void theory_pb::process_antecedent(literal l, numeral coeff) {
context& ctx = get_context(); context& ctx = get_context();
bool_var v = l.var(); bool_var v = l.var();
@ -1112,6 +1119,7 @@ namespace smt {
return false; return false;
} }
unset_marks();
m_num_marks = 0; m_num_marks = 0;
m_lemma.reset(); m_lemma.reset();
m_ineq_literals.reset(); m_ineq_literals.reset();
@ -1128,11 +1136,11 @@ namespace smt {
lbool is_sat = m_lemma.normalize(); lbool is_sat = m_lemma.normalize();
if (is_sat != l_undef) { if (is_sat != l_undef) {
if (is_sat == l_false) {
break;
}
IF_VERBOSE(0, display(verbose_stream() << "lemma already evaluated ", m_lemma, true);); IF_VERBOSE(0, display(verbose_stream() << "lemma already evaluated ", m_lemma, true););
TRACE("pb", display(tout << "lemma already evaluated ", m_lemma, true);); TRACE("pb", display(tout << "lemma already evaluated ", m_lemma, true););
for (unsigned i = 0; i < m_lemma.size(); ++i) {
unset_mark(m_lemma.lit(i));
}
return false; return false;
} }
TRACE("pb", display(tout, m_lemma, true);); TRACE("pb", display(tout, m_lemma, true););
@ -1157,9 +1165,6 @@ namespace smt {
// It is not a correctness bug but causes to miss lemmas. // It is not a correctness bug but causes to miss lemmas.
// //
IF_VERBOSE(1, display_resolved_lemma(verbose_stream());); IF_VERBOSE(1, display_resolved_lemma(verbose_stream()););
for (unsigned i = 0; i < m_lemma.size(); ++i) {
unset_mark(m_lemma.lit(i));
}
return false; return false;
} }
@ -1186,12 +1191,8 @@ namespace smt {
justification* cjs = cls.get_justification(); justification* cjs = cls.get_justification();
if (cjs) { if (cjs) {
IF_VERBOSE(1, verbose_stream() << "skipping justification for clause over: " << conseq << "\n";); IF_VERBOSE(1, verbose_stream() << "skipping justification for clause over: " << conseq << "\n";);
TRACE("pb", tout << "skipping justification for clause over: " << conseq << "\n";);
m_ineq_literals.push_back(conseq); m_ineq_literals.push_back(conseq);
m_lemma.m_k -= conseq_coeff;
for (unsigned i = 0; i < m_lemma.size(); ++i) {
unset_mark(m_lemma.lit(i));
}
return false;
break; break;
} }
unsigned num_lits = cls.get_num_literals(); unsigned num_lits = cls.get_num_literals();
@ -1225,11 +1226,6 @@ namespace smt {
TRACE("pb", tout << "skipping justification for " << conseq TRACE("pb", tout << "skipping justification for " << conseq
<< " from theory " << j.get_from_theory() << "\n";); << " from theory " << j.get_from_theory() << "\n";);
m_ineq_literals.push_back(conseq); m_ineq_literals.push_back(conseq);
m_lemma.m_k -= conseq_coeff;
for (unsigned i = 0; i < m_lemma.size(); ++i) {
unset_mark(m_lemma.lit(i));
}
return false;
} }
else { else {
pb_justification& pbj = dynamic_cast<pb_justification&>(j); pb_justification& pbj = dynamic_cast<pb_justification&>(j);
@ -1244,11 +1240,6 @@ namespace smt {
} }
} }
for (unsigned i = 0; i < m_lemma.size(); ++i) {
unset_mark(m_lemma.lit(i));
}
TRACE("pb", TRACE("pb",
for (unsigned i = 0; i < m_ineq_literals.size(); ++i) { for (unsigned i = 0; i < m_ineq_literals.size(); ++i) {
tout << m_ineq_literals[i] << " "; tout << m_ineq_literals[i] << " ";
@ -1304,7 +1295,7 @@ namespace smt {
m_conseq_index[c.lit(idx).var()] = idx; m_conseq_index[c.lit(idx).var()] = idx;
} }
c.m_args.pop_back(); c.m_args.pop_back();
unset_mark(lit); unset_mark(lit.var());
--m_num_marks; --m_num_marks;
} }

4
src/smt/theory_pb.h
View file

@ -143,13 +143,15 @@ namespace smt {
unsigned m_conflict_lvl; unsigned m_conflict_lvl;
ineq m_lemma; ineq m_lemma;
literal_vector m_ineq_literals; literal_vector m_ineq_literals;
svector<bool_var> m_marked;
// bool_var |-> index into m_lemma // bool_var |-> index into m_lemma
unsigned_vector m_conseq_index; unsigned_vector m_conseq_index;
static const unsigned null_index = UINT_MAX; static const unsigned null_index = UINT_MAX;
bool is_marked(bool_var v) const; bool is_marked(bool_var v) const;
void set_mark(bool_var v, unsigned idx); void set_mark(bool_var v, unsigned idx);
void unset_mark(literal l); void unset_mark(bool_var v);
void unset_marks();
bool resolve_conflict(ineq& c); bool resolve_conflict(ineq& c);
void process_antecedent(literal l, numeral coeff); void process_antecedent(literal l, numeral coeff);