mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-24 23:03:41 +00:00
Code Activity

Fix helper function viable::find_value

Browse source
This commit is contained in:
Jakob Rath 2023-11-10 10:54:14 +01:00
parent 5a03d13913
commit 115a82cd82
1 changed files with 7 additions and 7 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -1488,18 +1488,18 @@ namespace polysat {
std::pair<viable::entry*, bool> viable::find_value(rational const& val, entry* entries) { std::pair<viable::entry*, bool> viable::find_value(rational const& val, entry* entries) {
SASSERT(entries); SASSERT(entries);
// display_all(std::cerr << "entries:\n\t", 0, entries, "\n\t"); // display_all(std::cerr << "entries:\n\t", 0, entries, "\n\t");
// SASSERT(well_formed(entries)); entry* const first = entries;
// SASSERT(!limit || entry::contains(entries, limit));
// if (!limit)
// limit = entries;
entry* first = entries;
entry* e = entries; entry* e = entries;
do { do {
if (e->interval.currently_contains(val)) if (e->interval.currently_contains(val))
return {e, true}; return {e, true};
entry* n = e->next(); entry* const n = e->next();
// there is only one interval, and it does not contain 'val'
if (e == n)
return {e, false};
// check whether 'val' is contained in the gap between e and n // check whether 'val' is contained in the gap between e and n
if (r_interval::contains(e->interval.hi_val(), n->interval.lo_val(), val)) bool const overlapping = e->interval.currently_contains(n->interval.lo_val());
if (!overlapping && r_interval::contains(e->interval.hi_val(), n->interval.lo_val(), val))
return {n, false}; return {n, false};
e = n; e = n;
} while (e != first); } while (e != first);