mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-27 00:18:45 +00:00
Code Activity

bug fixes

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2017-10-08 14:35:31 -07:00
parent 356835533a
commit 10e4235b4c
4 changed files with 72 additions and 72 deletions
Download patch file Download diff file Expand all files Collapse all files

78
src/sat/ba_solver.cpp
View file

@ -363,8 +363,8 @@ namespace sat {
} }
if (p.k() == 1 && p.lit() == null_literal) { if (p.k() == 1 && p.lit() == null_literal) {
literal_vector lits(p.literals()); literal_vector lits(p.literals());
IF_VERBOSE(10, display(verbose_stream() << "add clause: " << lits << "\n", p, true););
s().mk_clause(lits.size(), lits.c_ptr(), p.learned()); s().mk_clause(lits.size(), lits.c_ptr(), p.learned());
IF_VERBOSE(10, display(verbose_stream() << "add clause: " << lits << "\n", p, true););
remove_constraint(p, "implies clause"); remove_constraint(p, "implies clause");
} }
else if (true_val == 0 && num_false == 0) { else if (true_val == 0 && num_false == 0) {
@ -415,8 +415,8 @@ namespace sat {
p.set_k(p.k() - true_val); p.set_k(p.k() - true_val);
if (p.k() == 1 && p.lit() == null_literal) { if (p.k() == 1 && p.lit() == null_literal) {
literal_vector lits(p.literals()); literal_vector lits(sz, p.literals().c_ptr());
s().mk_clause(lits.size(), lits.c_ptr(), p.learned()); s().mk_clause(sz, lits.c_ptr(), p.learned());
remove_constraint(p, "is clause"); remove_constraint(p, "is clause");
return; return;
} }
@ -756,14 +756,13 @@ namespace sat {
unsigned k = p.k(); unsigned k = p.k();
unsigned sz = p.size(); unsigned sz = p.size();
bool all_units = true; bool all_units = true;
unsigned j = 0;
for (unsigned i = 0; i < sz && 0 < k; ++i) { for (unsigned i = 0; i < sz && 0 < k; ++i) {
literal l = p[i].second; literal l = p[i].second;
unsigned w1 = m_weights[l.index()]; unsigned w1 = m_weights[l.index()];
unsigned w2 = m_weights[(~l).index()]; unsigned w2 = m_weights[(~l).index()];
if (w1 == 0 || w1 < w2) { if (w1 == 0 || w1 < w2) {
p.swap(i, sz - 1); continue;
--sz;
--i;
} }
else if (k <= w2) { else if (k <= w2) {
k = 0; k = 0;
@ -776,16 +775,16 @@ namespace sat {
m_weights[l.index()] = 0; m_weights[l.index()] = 0;
m_weights[(~l).index()] = 0; m_weights[(~l).index()] = 0;
if (w1 == 0) { if (w1 == 0) {
p.swap(i, sz - 1); continue;
--sz;
--i;
} }
else { else {
p[i] = wliteral(w1, l); p[j] = wliteral(w1, l);
all_units &= w1 == 1; all_units &= w1 == 1;
++j;
} }
} }
} }
sz = j;
// clear weights // clear weights
for (wliteral wl : p) { for (wliteral wl : p) {
m_weights[wl.second.index()] = 0; m_weights[wl.second.index()] = 0;
@ -800,27 +799,28 @@ namespace sat {
return; return;
} }
if (k == 1 && p.lit() == null_literal) { else if (k == 1 && p.lit() == null_literal) {
literal_vector lits(p.literals()); literal_vector lits(sz, p.literals().c_ptr());
s().mk_clause(sz, lits.c_ptr(), p.learned()); s().mk_clause(sz, lits.c_ptr(), p.learned());
remove_constraint(p, "recompiled to clause"); remove_constraint(p, "recompiled to clause");
return; return;
} }
if (all_units) { else if (all_units) {
literal_vector lits(sz, p.literals().c_ptr()); literal_vector lits(sz, p.literals().c_ptr());
add_at_least(p.lit(), lits, k, p.learned()); add_at_least(p.lit(), lits, k, p.learned());
remove_constraint(p, "recompiled to cardinality"); remove_constraint(p, "recompiled to cardinality");
return; return;
} }
p.set_size(sz); else {
p.set_k(k); p.set_size(sz);
SASSERT(p.well_formed()); p.set_k(k);
SASSERT(p.well_formed());
// this could become a cardinality constraint by now. if (p.lit() == null_literal || value(p.lit()) == l_true) {
if (p.lit() == null_literal || value(p.lit()) == l_true) { init_watch(p, true);
init_watch(p, true); }
} }
} }
@ -1281,13 +1281,8 @@ namespace sat {
if (!create_asserting_lemma()) { if (!create_asserting_lemma()) {
goto bail_out; goto bail_out;
} }
active2card(); active2card();
if (m_overflow) {
goto bail_out;
}
DEBUG_CODE(VERIFY(validate_conflict(m_lemma, m_A));); DEBUG_CODE(VERIFY(validate_conflict(m_lemma, m_A)););
TRACE("ba", tout << m_lemma << "\n";); TRACE("ba", tout << m_lemma << "\n";);
@ -1407,7 +1402,7 @@ namespace sat {
IF_VERBOSE(10, verbose_stream() << "(sat.backjump :new-level " << m_conflict_lvl << " :old-level " << old_level << ")\n";); IF_VERBOSE(10, verbose_stream() << "(sat.backjump :new-level " << m_conflict_lvl << " :old-level " << old_level << ")\n";);
goto adjust_conflict_level; goto adjust_conflict_level;
} }
return true; return !m_overflow;
} }
/* /*
@ -2564,7 +2559,6 @@ namespace sat {
if (m_roots.empty()) return; if (m_roots.empty()) return;
// validate(); // validate();
m_visited.resize(s().num_vars()*2, false); m_visited.resize(s().num_vars()*2, false);
m_constraint_removed = false; m_constraint_removed = false;
for (unsigned sz = m_constraints.size(), i = 0; i < sz; ++i) for (unsigned sz = m_constraints.size(), i = 0; i < sz; ++i)
@ -2572,7 +2566,6 @@ namespace sat {
for (unsigned sz = m_learned.size(), i = 0; i < sz; ++i) for (unsigned sz = m_learned.size(), i = 0; i < sz; ++i)
flush_roots(*m_learned[i]); flush_roots(*m_learned[i]);
cleanup_constraints(); cleanup_constraints();
// validate(); // validate();
} }
@ -2596,6 +2589,7 @@ namespace sat {
} }
void ba_solver::recompile(card& c) { void ba_solver::recompile(card& c) {
// pre-condition is that the literals, except c.lit(), in c are watched.
if (c.id() == _bad_id) std::cout << "recompile: " << c << "\n"; if (c.id() == _bad_id) std::cout << "recompile: " << c << "\n";
// IF_VERBOSE(0, verbose_stream() << "re: " << c << "\n";); // IF_VERBOSE(0, verbose_stream() << "re: " << c << "\n";);
m_weights.resize(2*s().num_vars(), 0); m_weights.resize(2*s().num_vars(), 0);
@ -2606,14 +2600,14 @@ namespace sat {
bool all_units = true; bool all_units = true;
unsigned sz = c.size(); unsigned sz = c.size();
unsigned_vector coeffs; unsigned_vector coeffs;
literal_vector lits;
unsigned j = 0;
for (unsigned i = 0; i < sz && 0 < k; ++i) { for (unsigned i = 0; i < sz && 0 < k; ++i) {
literal l = c[i]; literal l = c[i];
unsigned w = m_weights[l.index()]; unsigned w = m_weights[l.index()];
unsigned w2 = m_weights[(~l).index()]; unsigned w2 = m_weights[(~l).index()];
if (w == 0 || w < w2) { if (w == 0 || w < w2) {
c.swap(i, sz - 1); continue;
--sz;
--i;
} }
else if (k <= w2) { else if (k <= w2) {
k = 0; k = 0;
@ -2626,30 +2620,31 @@ namespace sat {
m_weights[(~l).index()] = 0; m_weights[(~l).index()] = 0;
m_weights[l.index()] = 0; m_weights[l.index()] = 0;
if (w == 0) { if (w == 0) {
c.swap(i, sz - 1); continue;
--sz;
--i;
} }
else { else {
all_units &= (w == 1); all_units &= (w == 1);
coeffs.push_back(w); coeffs.push_back(w);
c[j++] = l;
} }
} }
} }
sz = j;
// clear weights // clear weights
for (literal l : c) { for (literal l : c) {
m_weights[l.index()] = 0; m_weights[l.index()] = 0;
m_weights[(~l).index()] = 0; m_weights[(~l).index()] = 0;
} }
if (k == 0) { if (k == 0 && c.lit() == null_literal) {
remove_constraint(c, "recompiled to true"); remove_constraint(c, "recompiled to true");
return; return;
} }
if (k == 1) { if (k == 1 && c.lit() == null_literal) {
literal_vector lits(c.size(), c.begin()); literal_vector lits(sz, c.literals().c_ptr());
s().mk_clause(lits.size(), lits.c_ptr(), c.learned()); s().mk_clause(sz, lits.c_ptr(), c.learned());
remove_constraint(c, "recompiled to clause"); remove_constraint(c, "recompiled to clause");
return; return;
} }
@ -2671,6 +2666,7 @@ namespace sat {
if (c.lit() == null_literal || value(c.lit()) == l_true) { if (c.lit() == null_literal || value(c.lit()) == l_true) {
init_watch(c, true); init_watch(c, true);
} }
SASSERT(c.lit() == null_literal || is_watched(c.lit(), c));
SASSERT(c.well_formed()); SASSERT(c.well_formed());
} }
} }
@ -2692,7 +2688,6 @@ namespace sat {
found = m_root_vars[c.get_lit(i).var()]; found = m_root_vars[c.get_lit(i).var()];
} }
if (!found) return; if (!found) return;
//std::cout << "reroot " << c << "\n";
clear_watch(c); clear_watch(c);
// this could create duplicate literals // this could create duplicate literals
@ -2730,7 +2725,6 @@ namespace sat {
found_root |= l.var() == root.var(); found_root |= l.var() == root.var();
} }
//std::cout << "reroot " << c << "\n";
if (found_root) { if (found_root) {
split_root(c); split_root(c);
c.negate(); c.negate();
@ -2837,8 +2831,9 @@ namespace sat {
for (unsigned v = 0; v < s().num_vars(); ++v) { for (unsigned v = 0; v < s().num_vars(); ++v) {
literal lit(v, false); literal lit(v, false);
if (s().is_external(v) && if (s().is_external(v) &&
m_cnstr_use_list[lit.index()].size() == 0 && m_cnstr_use_list[lit.index()].empty() &&
m_cnstr_use_list[(~lit).index()].size() == 0 && !s().is_assumption(v)) { m_cnstr_use_list[(~lit).index()].empty() &&
!s().is_assumption(v)) {
s().set_non_external(v); s().set_non_external(v);
++ext; ++ext;
} }
@ -3723,6 +3718,7 @@ namespace sat {
constraint* c = add_at_least(null_literal, lits, k, true); constraint* c = add_at_least(null_literal, lits, k, true);
if (c) { if (c) {
// IF_VERBOSE(0, verbose_stream() << *c << "\n";);
lits.reset(); lits.reset();
for (wliteral wl : m_wlits) { for (wliteral wl : m_wlits) {
if (value(wl.second) == l_false) lits.push_back(wl.second); if (value(wl.second) == l_false) lits.push_back(wl.second);

56
src/sat/sat_elim_eqs.cpp
View file

@ -101,12 +101,13 @@ namespace sat {
c[i] = norm(roots, c[i]); c[i] = norm(roots, c[i]);
} }
std::sort(c.begin(), c.end()); std::sort(c.begin(), c.end());
for (literal l : c) VERIFY(l == norm(roots, l));
TRACE("sats", tout << "after normalization/sorting: " << c << "\n"; tout.flush();); TRACE("sats", tout << "after normalization/sorting: " << c << "\n"; tout.flush(););
DEBUG_CODE({ DEBUG_CODE({
for (unsigned i = 0; i < sz; i++) { for (literal l : c) {
CTRACE("sats", c[i] != norm(roots, c[i]), tout << c[i] << " " << norm(roots, c[i]) << "\n"; tout.flush();); CTRACE("sat", l != norm(roots, l), tout << l << " " << norm(roots, l) << "\n"; tout.flush(););
SASSERT(c[i] == norm(roots, c[i])); SASSERT(l == norm(roots, l));
} }); } });
// remove duplicates, and check if it is a tautology // remove duplicates, and check if it is a tautology
literal l_prev = null_literal; literal l_prev = null_literal;
unsigned j = 0; unsigned j = 0;
@ -122,13 +123,11 @@ namespace sat {
break; // clause was satisfied break; // clause was satisfied
if (val == l_false) if (val == l_false)
continue; // skip continue; // skip
if (i != j) { c[j] = l;
std::swap(c[i], c[j]);
}
j++; j++;
} }
if (i < sz) { if (i < sz) {
// clause is a tautology or was simplified // clause is a tautology or was simplified to true
m_solver.del_clause(c); m_solver.del_clause(c);
continue; continue;
} }
@ -164,10 +163,7 @@ namespace sat {
else else
c.update_approx(); c.update_approx();
DEBUG_CODE({ DEBUG_CODE(for (literal l : c) VERIFY(l == norm(roots, l)););
for (unsigned i = 0; i < j; i++) {
SASSERT(c[i] == norm(roots, c[i]));
} });
*it2 = *it; *it2 = *it;
it2++; it2++;
@ -187,7 +183,6 @@ namespace sat {
literal r = roots[v]; literal r = roots[v];
SASSERT(v != r.var()); SASSERT(v != r.var());
if (m_solver.is_external(v) && !m_solver.set_root(l, r)) { if (m_solver.is_external(v) && !m_solver.set_root(l, r)) {
std::cout << "skip: " << l << " == " << r << "\n";
// cannot really eliminate v, since we have to notify extension of future assignments // cannot really eliminate v, since we have to notify extension of future assignments
m_solver.mk_bin_clause(~l, r, false); m_solver.mk_bin_clause(~l, r, false);
m_solver.mk_bin_clause(l, ~r, false); m_solver.mk_bin_clause(l, ~r, false);
@ -199,29 +194,33 @@ namespace sat {
mc.insert(e, ~l, r); mc.insert(e, ~l, r);
mc.insert(e, l, ~r); mc.insert(e, l, ~r);
} }
m_solver.flush_roots();
} }
m_solver.flush_roots();
} }
bool elim_eqs::check_clauses(literal_vector const & roots) const { bool elim_eqs::check_clause(clause const& c, literal_vector const& roots) const {
clause_vector * vs[2] = { &m_solver.m_clauses, &m_solver.m_learned }; for (literal l : c) {
for (unsigned i = 0; i < 2; i++) { CTRACE("elim_eqs_bug", m_solver.was_eliminated(l.var()), tout << "lit: " << l << " " << norm(roots, l) << "\n";
clause_vector & cs = *(vs[i]); tout << c << "\n";);
clause_vector::iterator it = cs.begin(); if (m_solver.was_eliminated(l.var())) {
clause_vector::iterator end = cs.end(); IF_VERBOSE(0, verbose_stream() << c << " contains eliminated literal " << l << " " << norm(roots, l) << "\n";);
for (; it != end; ++it) { UNREACHABLE();
clause & c = *(*it);
unsigned sz = c.size();
for (unsigned i = 0; i < sz; i++) {
CTRACE("elim_eqs_bug", m_solver.was_eliminated(c[i].var()), tout << "lit: " << c[i] << " " << norm(roots, c[i]) << "\n";
tout << c << "\n";);
SASSERT(!m_solver.was_eliminated(c[i].var()));
}
} }
} }
return true; return true;
} }
bool elim_eqs::check_clauses(literal_vector const & roots) const {
for (clause * cp : m_solver.m_clauses)
if (!check_clause(*cp, roots))
return false;
for (clause * cp : m_solver.m_learned)
if (!check_clause(*cp, roots))
return false;
return true;
}
void elim_eqs::operator()(literal_vector const & roots, bool_var_vector const & to_elim) { void elim_eqs::operator()(literal_vector const & roots, bool_var_vector const & to_elim) {
cleanup_bin_watches(roots); cleanup_bin_watches(roots);
TRACE("elim_eqs", tout << "after bin cleanup\n"; m_solver.display(tout);); TRACE("elim_eqs", tout << "after bin cleanup\n"; m_solver.display(tout););
@ -230,6 +229,7 @@ namespace sat {
cleanup_clauses(roots, m_solver.m_learned); cleanup_clauses(roots, m_solver.m_learned);
if (m_solver.inconsistent()) return; if (m_solver.inconsistent()) return;
save_elim(roots, to_elim); save_elim(roots, to_elim);
VERIFY(check_clauses(roots));
m_solver.propagate(false); m_solver.propagate(false);
SASSERT(check_clauses(roots)); SASSERT(check_clauses(roots));
} }

1
src/sat/sat_elim_eqs.h
View file

@ -30,6 +30,7 @@ namespace sat {
void cleanup_clauses(literal_vector const & roots, clause_vector & cs); void cleanup_clauses(literal_vector const & roots, clause_vector & cs);
void cleanup_bin_watches(literal_vector const & roots); void cleanup_bin_watches(literal_vector const & roots);
bool check_clauses(literal_vector const & roots) const; bool check_clauses(literal_vector const & roots) const;
bool check_clause(clause const& c, literal_vector const& roots) const;
public: public:
elim_eqs(solver & s); elim_eqs(solver & s);
void operator()(literal_vector const & roots, bool_var_vector const & to_elim); void operator()(literal_vector const & roots, bool_var_vector const & to_elim);

3
src/sat/sat_solver.cpp
View file

@ -372,6 +372,9 @@ namespace sat {
clause * solver::mk_nary_clause(unsigned num_lits, literal * lits, bool learned) { clause * solver::mk_nary_clause(unsigned num_lits, literal * lits, bool learned) {
m_stats.m_mk_clause++; m_stats.m_mk_clause++;
for (unsigned i = 0; i + 1 < num_lits; ++i) {
VERIFY (lits[i] != ~lits[i + 1]);
}
clause * r = m_cls_allocator.mk_clause(num_lits, lits, learned); clause * r = m_cls_allocator.mk_clause(num_lits, lits, learned);
SASSERT(!learned || r->is_learned()); SASSERT(!learned || r->is_learned());
bool reinit = attach_nary_clause(*r); bool reinit = attach_nary_clause(*r);