From a68bbb53e4f053ab44a8ee008062996691992780 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Mon, 15 Jan 2024 09:18:51 -0800 Subject: [PATCH] update assign to check fixed bits afterwards Signed-off-by: Nikolaj Bjorner --- src/sat/smt/polysat/viable.cpp | 36 ++++++++++++++++++++++------------ 1 file changed, 24 insertions(+), 12 deletions(-) diff --git a/src/sat/smt/polysat/viable.cpp b/src/sat/smt/polysat/viable.cpp index 0ffc19a72..32509875f 100644 --- a/src/sat/smt/polysat/viable.cpp +++ b/src/sat/smt/polysat/viable.cpp @@ -90,20 +90,31 @@ namespace polysat { m_fixed_bits.init(v); m_explain.reset(); init_overlaps(v); - check_fixed_bits(v, value); - check_disequal_lin(v, value); - check_equal_lin(v, value); - for (auto const& [w, offset] : m_overlaps) { - for (auto& layer : m_units[w].get_layers()) { - entry* e = find_overlap(w, layer, value); - if (!e) - continue; - - m_explain.push_back({ e, value }); - m_explain_kind = explain_t::assignment; - return false; + bool first = true; + while (true) { + for (auto const& [w, offset] : m_overlaps) { + for (auto& layer : m_units[w].get_layers()) { + entry* e = find_overlap(w, layer, value); + if (!e) + continue; + + m_explain.push_back({ e, value }); + m_explain_kind = explain_t::assignment; + return false; + } } + if (!first) + return true; + first = false; + if (!check_fixed_bits(v, value)) + continue; + if (!check_disequal_lin(v, value)) + continue; + if (!check_equal_lin(v, value)) + continue; + break; } + return true; } @@ -397,6 +408,7 @@ namespace polysat { if (!intersect(v, e)) { display(verbose_stream()); display_explain(verbose_stream() << "explain\n"); + UNREACHABLE(); SASSERT(false); }