mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-22 08:35:31 +00:00
Code Activity

update assign to check fixed bits afterwards

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2024-01-15 09:18:51 -08:00
parent 42aad423c9
commit a68bbb53e4
1 changed files with 24 additions and 12 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -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);
}