mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-23 09:05:31 +00:00
Code Activity

fix bug in blocked clause elimination: it was ignoring unit literals

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2018-03-31 13:26:20 -07:00
parent aa2721517b
commit 55eb11d91b
5 changed files with 33 additions and 37 deletions
Download patch file Download diff file Expand all files Collapse all files

20
src/sat/sat_model_converter.cpp
View file

@ -79,21 +79,27 @@ namespace sat {
//SASSERT(!m_solver || m_solver->check_clauses(m));
while (it != begin) {
--it;
SASSERT(it->get_kind() != ELIM_VAR || m[it->var()] == l_undef);
// if it->get_kind() == BLOCK_LIT, then it might be the case that m[it->var()] != l_undef,
bool_var v0 = it->var();
SASSERT(it->get_kind() != ELIM_VAR || m[v0] == l_undef);
// if it->get_kind() == BLOCK_LIT, then it might be the case that m[v] != l_undef,
// and the following procedure flips its value.
bool sat = false;
bool var_sign = false;
unsigned index = 0;
literal_vector clause;
VERIFY(legal_to_flip(it->var()));
VERIFY(legal_to_flip(v0));
for (literal l : it->m_clauses) {
if (l == null_literal) {
// end of clause
if (v0 == 36858)
IF_VERBOSE(0, verbose_stream() << "clause: " << clause << "\n";
for (literal lit : clause) verbose_stream() << m[lit.var()] << " ";
verbose_stream() << "\n";);
elim_stack* st = it->m_elim_stack[index];
if (!sat) {
VERIFY(legal_to_flip(it->var()));
m[it->var()] = var_sign ? l_false : l_true;
VERIFY(legal_to_flip(v0));
m[v0] = var_sign ? l_false : l_true;
}
if (st) {
process_stack(m, clause, st->stack());
@ -115,11 +121,11 @@ namespace sat {
bool_var v = l.var();
if (v >= m.size()) std::cout << v << " model size: " << m.size() << "\n";
VERIFY(v < m.size());
if (v == it->var())
if (v == v0)
var_sign = sign;
if (value_at(l, m) == l_true)
sat = true;
else if (!sat && v != it->var() && m[v] == l_undef) {
else if (!sat && v != v0 && m[v] == l_undef) {
VERIFY(legal_to_flip(v));
// clause can be satisfied by assigning v.
m[v] = sign ? l_false : l_true;

6
src/sat/sat_simplifier.cpp
View file

@ -1007,7 +1007,7 @@ namespace sat {
}
bool process_var(bool_var v) {
return !s.s.is_assumption(v) && !s.was_eliminated(v) && !s.is_external(v);
return !s.s.is_assumption(v) && !s.was_eliminated(v) && !s.is_external(v) && s.value(v) == l_undef;
}
enum elim_type {
@ -1184,7 +1184,7 @@ namespace sat {
if (m_covered_antecedent[i] == clause_ante()) s.mark_visited(lit);
if (s.is_marked(lit)) idx = i;
}
if (_blocked.var() == 16774 && false) {
if (false && _blocked.var() == 16774) {
IF_VERBOSE(0, verbose_stream() << "covered: " << m_covered_clause << "\n";
verbose_stream() << "tautology: " << m_tautology << "\n";
verbose_stream() << "index: " << idx << "\n";
@ -1232,7 +1232,7 @@ namespace sat {
// unsigned sz0 = m_covered_clause.size();
m_covered_clause.resize(j);
VERIFY(j >= m_clause.size());
if (_blocked.var() == 16774 && false) {
if (false && _blocked.var() == 16774) {
IF_VERBOSE(0, verbose_stream() << "covered: " << m_covered_clause << "\n");
}
// IF_VERBOSE(0, verbose_stream() << "reduced from size " << sz0 << " to " << m_covered_clause << "\n" << m_clause << "\n";);

13
src/sat/sat_solver.cpp
View file

@ -333,13 +333,6 @@ namespace sat {
}
void solver::mk_bin_clause(literal l1, literal l2, bool learned) {
#if 0
if ((l1 == literal(5981, false) && l2 == literal(16764, false)) ||
(l2 == literal(5981, false) && l1 == literal(16764, false))) {
IF_VERBOSE(0, display(verbose_stream()));
//VERIFY(false);
}
#endif
if (find_binary_watch(get_wlist(~l1), ~l2)) {
assign(l1, justification());
return;
@ -487,6 +480,8 @@ namespace sat {
return reinit;
}
static unsigned s_count = 0;
void solver::attach_clause(clause & c, bool & reinit) {
SASSERT(c.size() > 2);
reinit = false;
@ -1674,7 +1669,9 @@ namespace sat {
if (!m_clone->check_model(m_model)) {
//IF_VERBOSE(0, display(verbose_stream()));
//IF_VERBOSE(0, display_watches(verbose_stream()));
//IF_VERBOSE(0, m_mc.display(verbose_stream()));
IF_VERBOSE(0, m_mc.display(verbose_stream()));
IF_VERBOSE(0, display_units(verbose_stream()));
//IF_VERBOSE(0, m_clone->display(verbose_stream() << "clone\n"));
throw solver_exception("check model failed (for cloned solver)");
}
}