mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-08-18 01:02:15 +00:00
Code Activity

always restart find_overlap at smallest size

Browse source
This commit is contained in:
Jakob Rath 2024-04-03 17:38:43 +02:00
parent 583c40de1f
commit b808dece15
1 changed files with 13 additions and 8 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -172,18 +172,23 @@ namespace polysat {
viable::entry* viable::find_overlap(rational& val) { viable::entry* viable::find_overlap(rational& val) {
entry* last = nullptr; entry* last = nullptr;
// TODO: this doesn't always make sure we prefer smaller sizes... different suffixes would have to be interleaved. // TODO: this doesn't always make sure we prefer smaller sizes... different suffixes would have to be interleaved.
next:
for (auto const& [w, offset] : m_suffixes) { for (auto const& [w, offset] : m_suffixes) {
for (auto& layer : m_units[w].get_layers()) { for (auto& layer : m_units[w].get_layers()) {
while (entry* e = find_overlap(w, layer, val)) { entry* e = find_overlap(w, layer, val);
last = e; if (!e)
if (e->interval.is_proper()) continue;
last = e;
if (e->interval.is_proper())
update_value_to_high(val, e); update_value_to_high(val, e);
m_explain.push_back({ e, val }); // display_explain(verbose_stream() << "found: ", {e,val}) << "\n";
if (is_conflict()) { m_explain.push_back({ e, val });
m_explain_kind = explain_t::conflict; if (is_conflict()) {
return nullptr; verbose_stream() << "find_overlap conflict\n";
} m_explain_kind = explain_t::conflict;
return nullptr;
} }
goto next;
} }
} }
return last; return last;