mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-07-03 11:25:40 +00:00
Code Activity

enable removal of redundant explanations

Browse source
This commit is contained in:
Jakob Rath 2024-04-03 11:40:18 +02:00
parent c5b02f8360
commit 017ae78c81
1 changed files with 11 additions and 10 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -729,7 +729,6 @@ namespace polysat {
// We add lower-width intervals such as v0[2] first, to be able to detect conflicts on lower widths. // We add lower-width intervals such as v0[2] first, to be able to detect conflicts on lower widths.
// But it means we sometimes get redundant entries like this. // But it means we sometimes get redundant entries like this.
void viable::remove_redundant_explanations() { void viable::remove_redundant_explanations() {
verbose_stream() << "SUBSUMPTION\n";
SASSERT(all_of(m_explain, [](auto const& e) { return !e.e->marked; })); SASSERT(all_of(m_explain, [](auto const& e) { return !e.e->marked; }));
explanation const& last = m_explain.back(); explanation const& last = m_explain.back();
@ -749,30 +748,32 @@ namespace polysat {
for (unsigned i = k; i < m_explain.size() - 1; ++i) { for (unsigned i = k; i < m_explain.size() - 1; ++i) {
explanation const& cur = m_explain[i]; explanation const& cur = m_explain[i];
display_explain(verbose_stream() << "check subsumption: cur: ", cur) << "\n";
if (m_explain[i].e->marked) if (m_explain[i].e->marked)
continue; // already pruned continue; // already pruned
// next interval contains current endpoint (because of how it was chosen) // next interval contains current endpoint (because of how it was chosen)
explanation const& next = m_explain[i + 1]; DEBUG_CODE({
SASSERT(get_covered_interval(next).contains(cur.value)); explanation const& next = m_explain[i + 1];
SASSERT(get_covered_interval(next).contains(cur.value));
});
// if the interval after 'next' still contains 'cur.value', we may skip 'next' (and so on) // if the interval after 'next' still contains 'cur.value', we may skip 'next' (and so on)
unsigned j = i + 2; unsigned j = i + 2;
for (; j < m_explain.size(); ++j) { for (; j < m_explain.size(); ++j) {
r_interval ivl = get_covered_interval(m_explain[j]); r_interval ivl = get_covered_interval(m_explain[j]);
if (ivl.contains(cur.value)) { if (ivl.contains(cur.value))
display_explain(verbose_stream() << " subsumed: ", m_explain[j-1]) << "\n";
#if 0 // TODO: disabled for testing
m_explain[j - 1].e->marked = true; m_explain[j - 1].e->marked = true;
#endif
}
else else
break; break;
} }
} }
IF_VERBOSE(1, {
for (auto const& e : m_explain)
if (e.e->marked)
display_explain(verbose_stream() << "redundant: ", e) << "\n";
});
// Actually perform the removal // Actually perform the removal
m_explain.erase_if([](auto const& e) { m_explain.erase_if([](auto const& e) {
if (e.e->marked) { if (e.e->marked) {