mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-10-08 08:51:55 +00:00
Code Activity

fix another recompilation bug

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2018-02-09 13:47:55 -08:00
parent 4f7b6a2f18
commit f28b158d57
2 changed files with 50 additions and 19 deletions
Download patch file Download diff file Expand all files Collapse all files

33
src/sat/ba_solver.cpp
View file

@ -2615,8 +2615,9 @@ namespace sat {
// pre-condition is that the literals, except c.lit(), in c are unwatched.
if (c.id() == _bad_id) std::cout << "recompile: " << c << "\n";
// IF_VERBOSE(0, verbose_stream() << c << "\n";);
m_weights.resize(2*s().num_vars(), 0);
// for (unsigned w : m_weights) VERIFY(w == 0);
for (literal l : c) {
++m_weights[l.index()];
}
@ -2673,6 +2674,36 @@ namespace sat {
return;
}
if (sz == 0) {
if (c.lit() == null_literal) {
if (k > 0) {
s().mk_clause(0, nullptr, true);
}
}
else if (k > 0) {
literal lit = ~c.lit();
s().mk_clause(1, &lit, c.learned());
}
else {
literal lit = c.lit();
s().mk_clause(1, &lit, c.learned());
}
remove_constraint(c, "recompiled to clause");
return;
}
if (all_units && sz < k) {
// IF_VERBOSE(0, verbose_stream() << "all units " << sz << " " << k << "\n");
if (c.lit() == null_literal) {
s().mk_clause(0, nullptr, true);
}
else {
literal lit = ~c.lit();
s().mk_clause(1, &lit, c.learned());
}
remove_constraint(c, "recompiled to clause");
return;
}
// IF_VERBOSE(0, verbose_stream() << "csz: " << c.size() << " ck:" << c.k() << " sz:" << sz << " k:" << k << "\n");
VERIFY(!all_units || c.size() - c.k() >= sz - k);
c.set_size(sz);
c.set_k(k);