mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-07 18:05:21 +00:00
Code Activity

fix bug in root setting exposed by incremental mode pb_solver

Browse source
This commit is contained in:
Nikolaj Bjorner 2022-01-18 10:55:27 +01:00
parent 36cfb88f5f
commit 06feb71eb1
3 changed files with 18 additions and 12 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

7
src/sat/sat_elim_eqs.cpp
View file

@ -229,11 +229,12 @@ namespace sat {
literal r = roots[v];
SASSERT(v != r.var());
if (m_solver.m_cut_simplifier) m_solver.m_cut_simplifier->set_root(v, r);
if (m_solver.m_cut_simplifier)
m_solver.m_cut_simplifier->set_root(v, r);
bool set_root = m_solver.set_root(l, r);
bool root_ok = !m_solver.is_external(v) || set_root;
TRACE("elim_eqs", tout << l << " " << r << "\n";);
if (m_solver.is_assumption(v) || (m_solver.is_external(v) && (m_solver.is_incremental() || !root_ok))) {
if (m_solver.is_assumption(v) || (m_solver.is_external(v) && (m_solver.is_incremental() || !set_root))) {
// cannot really eliminate v, since we have to notify extension of future assignments
if (m_solver.m_config.m_drat) {
m_solver.m_drat.add(~l, r, sat::status::redundant());

9
src/sat/smt/euf_solver.cpp
View file

@ -808,13 +808,16 @@ namespace euf {
bool solver::set_root(literal l, literal r) {
if (m_relevancy.enabled())
return false;
expr* e = bool_var2expr(l.var());
if (!e)
return true;
bool ok = true;
for (auto* s : m_solvers)
if (!s->set_root(l, r))
ok = false;
if (!ok)
return false;
expr* e = bool_var2expr(l.var());
if (!e)
return true;
if (m.is_eq(e) && !m.is_iff(e))
ok = false;
euf::enode* n = get_enode(e);

14
src/sat/smt/pb_solver.cpp
View file

@ -2193,12 +2193,13 @@ namespace pb {
}
bool solver::set_root(literal l, literal r) {
if (s().is_assumption(l.var())) {
if (s().is_assumption(l.var()))
return false;
}
reserve_roots();
m_roots[l.index()] = r;
m_roots[(~l).index()] = ~r;
m_roots[r.index()] = r;
m_roots[(~r).index()] = ~r;
m_root_vars[l.var()] = true;
return true;
}
@ -2214,7 +2215,6 @@ namespace pb {
flush_roots(*m_learned[i]);
cleanup_constraints();
// validate();
// validate_eliminated();
}
@ -2225,7 +2225,8 @@ namespace pb {
void solver::validate_eliminated(ptr_vector<constraint> const& cs) {
for (constraint const* c : cs) {
if (c->learned()) continue;
if (c->learned())
continue;
for (auto l : constraint::literal_iterator(*c))
VERIFY(!s().was_eliminated(l.var()));
}
@ -2449,9 +2450,10 @@ namespace pb {
for (unsigned i = 0; !found && i < c.size(); ++i) {
found = m_root_vars[c.get_lit(i).var()];
}
if (!found) return;
if (!found)
return;
clear_watch(c);
// this could create duplicate literals
for (unsigned i = 0; i < c.size(); ++i) {
literal lit = m_roots[c.get_lit(i).index()];