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

set proper explain_kind in case of full interval

Browse source
This commit is contained in:
Jakob Rath 2024-05-14 19:11:05 +02:00
parent 47d93037f7
commit 962edfd03c
1 changed files with 6 additions and 2 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -122,6 +122,7 @@ namespace polysat {
} }
find_t viable::find_viable(pvar v, rational& lo) { find_t viable::find_viable(pvar v, rational& lo) {
// verbose_stream() << "find_viable v" << v << "\n";
m_explain.reset(); m_explain.reset();
m_var = v; m_var = v;
m_num_bits = c.size(v); m_num_bits = c.size(v);
@ -551,6 +552,7 @@ namespace polysat {
auto last = m_explain.back(); auto last = m_explain.back();
unsigned bw = last.e->bit_width; unsigned bw = last.e->bit_width;
if (last.e->interval.is_full()) { if (last.e->interval.is_full()) {
// this may happen if full interval is created from check_equal_lin or check_disequal_lin
m_explain.reset(); m_explain.reset();
m_explain.push_back(last); m_explain.push_back(last);
return true; return true;
@ -656,7 +658,7 @@ namespace polysat {
}; };
if (last.e->interval.is_full()) { if (last.e->interval.is_full()) {
SASSERT(m_explain_kind == explain_t::none); VERIFY(m_explain_kind == explain_t::none || m_explain_kind == explain_t::conflict);
explain_entry(last.e); explain_entry(last.e);
SASSERT(m_explain.size() == 1); SASSERT(m_explain.size() == 1);
unmark(); unmark();
@ -1571,7 +1573,7 @@ v0[20] := 1048561 v0 [20*v1 + 21 ; 20*v1 + 1[ := [5;-15[ src -20 <= 20*v1 + -1*
return find_t::multiple; return find_t::multiple;
} }
// verbose_stream() << "v" << v << " " << sc << " " << ne->interval << "\n"; // verbose_stream() << "add_unitary v" << v << " " << sc << " " << ne->interval << "\n"; display_one(verbose_stream() << " ", ne) << "\n";
TRACE("bv", tout << "v" << v << " " << sc << " " << ne->interval << "\n"; display_one(tout, ne) << "\n"); TRACE("bv", tout << "v" << v << " " << sc << " " << ne->interval << "\n"; display_one(tout, ne) << "\n");
if (ne->interval.is_currently_empty()) { if (ne->interval.is_currently_empty()) {
@ -1674,6 +1676,7 @@ v0[20] := 1048561 v0 [20*v1 + 21 ; 20*v1 + 1[ := [5;-15[ src -20 <= 20*v1 + -1*
else { else {
ne->interval = eval_interval::full(); ne->interval = eval_interval::full();
ne->coeff = 1; ne->coeff = 1;
m_explain_kind = explain_t::none;
m_explain.reset(); m_explain.reset();
m_explain.push_back({ ne, rational::zero() }); m_explain.push_back({ ne, rational::zero() });
m_fixed_bits.reset(); m_fixed_bits.reset();
@ -1693,6 +1696,7 @@ v0[20] := 1048561 v0 [20*v1 + 21 ; 20*v1 + 1[ := [5;-15[ src -20 <= 20*v1 + -1*
intersect(v, ne); intersect(v, ne);
} }
if (ne->interval.is_full()) { if (ne->interval.is_full()) {
m_explain_kind = explain_t::none;
m_explain.reset(); m_explain.reset();
m_explain.push_back({ ne, rational::zero() }); m_explain.push_back({ ne, rational::zero() });
m_fixed_bits.reset(); m_fixed_bits.reset();