mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-08-07 19:51:22 +00:00
Code Activity

fixing corner cases for viable intervals

Browse source
This commit is contained in:
Nikolaj Bjorner 2022-02-01 13:21:51 -08:00
parent c48f14e537
commit 18291543d6
1 changed files with 19 additions and 4 deletions
Download patch file Download diff file Expand all files Collapse all files

23
src/math/polysat/viable.cpp
View file

@ -122,6 +122,7 @@ namespace polysat {
m_alloc.push_back(ne); m_alloc.push_back(ne);
return false; return false;
} }
auto create_entry = [&]() { auto create_entry = [&]() {
m_trail.push_back({ v, entry_kind::unit_e, ne }); m_trail.push_back({ v, entry_kind::unit_e, ne });
@ -136,6 +137,13 @@ namespace polysat {
e->remove_from(m_units[v], e); e->remove_from(m_units[v], e);
}; };
if (ne->interval.is_full()) {
while (m_units[v])
remove_entry(m_units[v]);
m_units[v] = create_entry();
return true;
}
if (!e) if (!e)
m_units[v] = create_entry(); m_units[v] = create_entry();
else { else {
@ -257,16 +265,21 @@ namespace polysat {
lo = val - lambda_l; lo = val - lambda_l;
increase_hi(hi); increase_hi(hi);
} }
LOG("forbidden interval " << e->coeff << " * " << e->interval << " [" << lo << ", " << hi << "["); LOG("forbidden interval v" << v << " " << val << " " << e->coeff << " * " << e->interval << " [" << lo << ", " << hi << "[");
SASSERT(hi <= mod_value); SASSERT(hi <= mod_value);
if (hi == mod_value) hi = 0; bool full = (lo == 0 && hi == mod_value);
if (hi == mod_value)
hi = 0;
pdd lop = s.var2pdd(v).mk_val(lo); pdd lop = s.var2pdd(v).mk_val(lo);
pdd hip = s.var2pdd(v).mk_val(hi); pdd hip = s.var2pdd(v).mk_val(hi);
entry* ne = alloc_entry(); entry* ne = alloc_entry();
ne->src = e->src; ne->src = e->src;
ne->side_cond = e->side_cond; ne->side_cond = e->side_cond;
ne->coeff = 1; ne->coeff = 1;
ne->interval = eval_interval::proper(lop, lo, hip, hi); if (full)
ne->interval = eval_interval::full();
else
ne->interval = eval_interval::proper(lop, lo, hip, hi);
intersect(v, ne); intersect(v, ne);
return false; return false;
} }
@ -384,6 +397,8 @@ namespace polysat {
entry* first = e; entry* first = e;
entry* last = e->prev(); entry* last = e->prev();
if (e->interval.is_full())
return false;
// quick check: last interval doesn't wrap around, so hi_val // quick check: last interval doesn't wrap around, so hi_val
// has not been covered // has not been covered
if (last->interval.lo_val() < last->interval.hi_val()) if (last->interval.lo_val() < last->interval.hi_val())
@ -616,7 +631,7 @@ namespace polysat {
std::ostream& viable::display(std::ostream& out) const { std::ostream& viable::display(std::ostream& out) const {
for (pvar v = 0; v < m_units.size(); ++v) for (pvar v = 0; v < m_units.size(); ++v)
display(out << "v" << v << ": ", v); display(out << "v" << v << ": ", v) << "\n";
return out; return out;
} }