mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-07-18 10:30:44 +00:00
Code Activity

find_overlap should stay on lower bit-width to find conflicts

Browse source
This commit is contained in:
Jakob Rath 2024-04-02 16:27:29 +02:00
parent f127d12e4c
commit 47f28c6857
1 changed files with 4 additions and 2 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -170,10 +170,11 @@ 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.
for (auto const& [w, offset] : m_overlaps) { for (auto const& [w, offset] : m_overlaps) {
for (auto& layer : m_units[w].get_layers()) { for (auto& layer : m_units[w].get_layers()) {
again:
entry* e = find_overlap(w, layer, val); entry* e = find_overlap(w, layer, val);
if (!e) if (!e)
continue; continue;
@ -185,12 +186,13 @@ namespace polysat {
m_explain_kind = explain_t::conflict; m_explain_kind = explain_t::conflict;
return nullptr; return nullptr;
} }
goto again;
} }
} }
return last; return last;
} }
viable::entry* viable::find_overlap(pvar w, layer& l, rational const& val) { viable::entry* viable::find_overlap(pvar /* w */, layer& l, rational const& val) {
if (!l.entries) if (!l.entries)
return nullptr; return nullptr;
unsigned v_width = m_num_bits; unsigned v_width = m_num_bits;