mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-08-09 20:50:50 +00:00
Code Activity

guard against stale explain_kind

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

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

@ -590,6 +590,7 @@ namespace polysat {
case viable::explain_t::propagation: return out << "propagation"; case viable::explain_t::propagation: return out << "propagation";
case viable::explain_t::assignment: return out << "assignment"; case viable::explain_t::assignment: return out << "assignment";
case viable::explain_t::none: return out << "none"; case viable::explain_t::none: return out << "none";
case viable::explain_t::explained: return out << "explained";
default: UNREACHABLE(); default: UNREACHABLE();
} }
return out; return out;
@ -607,6 +608,7 @@ namespace polysat {
verbose_stream() << "\n\n\n\n\nviable::explain: " << m_explain_kind << " v" << m_var << "\n"; verbose_stream() << "\n\n\n\n\nviable::explain: " << m_explain_kind << " v" << m_var << "\n";
display_explain(verbose_stream() << "before subsumption:\n") << "\n"; display_explain(verbose_stream() << "before subsumption:\n") << "\n";
#endif #endif
SASSERT(m_explain_kind != explain_t::explained);
// prune redundant intervals // prune redundant intervals
while (remove_redundant_explanations()) while (remove_redundant_explanations())
@ -795,6 +797,7 @@ namespace polysat {
#if DEBUG_EXPLAIN #if DEBUG_EXPLAIN
verbose_stream() << "explain done: " << result << "\n"; verbose_stream() << "explain done: " << result << "\n";
#endif #endif
m_explain_kind = explain_t::explained;
return result; return result;
} }
@ -1676,7 +1679,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_kind = explain_t::conflict;
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();
@ -1696,7 +1699,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_kind = explain_t::conflict;
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();

5
src/sat/smt/polysat/viable.h
View file

@ -147,10 +147,11 @@ namespace polysat {
bool is_propagation(rational const& val); bool is_propagation(rational const& val);
enum class explain_t { enum class explain_t {
conflict, conflict, // conflict due to overlapping intervals
propagation, propagation,
assignment, assignment,
none none,
explained,
}; };
friend std::ostream& operator<<(std::ostream& out, explain_t e); friend std::ostream& operator<<(std::ostream& out, explain_t e);