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

viable explanation depends on assignment

Browse source
This commit is contained in:
Jakob Rath 2024-03-12 16:20:44 +01:00
parent 58c14ba2f9
commit df85eeb581
1 changed files with 13 additions and 2 deletions
Download patch file Download diff file Expand all files Collapse all files

15
src/sat/smt/polysat/viable.cpp
View file

@ -566,7 +566,7 @@ namespace polysat {
auto last = m_explain.back();
auto after = last;
verbose_stream() << m_explain_kind << "\n";
verbose_stream() << "viable::explain: " << m_explain_kind << " v" << m_var << "\n";
if (c.inconsistent())
verbose_stream() << "inconsistent explain\n";
@ -594,8 +594,12 @@ namespace polysat {
result.push_back(d);
}
result.append(e->deps);
if (!index.is_null())
if (!index.is_null()) {
VERIFY_EQ(e->src.size(), 1);
VERIFY_EQ(c.get_constraint(index), e->src[0]);
result.push_back(c.get_dependency(index));
// result.append(c.explain_weak_eval(c.get_constraint(index)));
}
};
if (last.e->interval.is_full()) {
@ -637,6 +641,13 @@ namespace polysat {
result.clear();
result.push_back(exp);
}
else {
// could not propagate to subslice
// conflict depends on evaluation
auto index = last.e->constraint_index;
if (!index.is_null())
result.append(c.explain_weak_eval(c.get_constraint(index)));
}
}
unmark();
if (c.inconsistent())