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

compile

Browse source
This commit is contained in:
Jakob Rath 2023-11-09 13:03:14 +01:00
parent e45358d9be
commit d3d0a5f635
2 changed files with 5 additions and 1 deletions
Download patch file Download diff file Expand all files Collapse all files

2
src/math/polysat/interval.h
View file

@ -67,7 +67,7 @@ namespace polysat {
// distance from a to b, wrapping around at mod_value. // distance from a to b, wrapping around at mod_value.
// basically mod(b - a, mod_value), but distance(0, mod_value, mod_value) = mod_value. // basically mod(b - a, mod_value), but distance(0, mod_value, mod_value) = mod_value.
rational distance(rational const& a, rational const& b, rational const& mod_value) { inline rational distance(rational const& a, rational const& b, rational const& mod_value) {
SASSERT(mod_value.is_power_of_two()); SASSERT(mod_value.is_power_of_two());
SASSERT(0 <= a && a < mod_value); SASSERT(0 <= a && a < mod_value);
SASSERT(0 <= b && b <= mod_value); SASSERT(0 <= b && b <= mod_value);

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

@ -1435,6 +1435,7 @@ namespace polysat {
e = n; e = n;
} while (e != first); } while (e != first);
UNREACHABLE(); UNREACHABLE();
return {nullptr, false};
} }
// find viable values in half-open interval [to_cover_lo;to_cover_hi[ w.r.t. unit intervals on the given layer // find viable values in half-open interval [to_cover_lo;to_cover_hi[ w.r.t. unit intervals on the given layer
@ -1564,6 +1565,9 @@ namespace polysat {
// TODO: refinement and fallback solver -- can we refine without throwing out all the entry_cursors we have set up? // TODO: refinement and fallback solver -- can we refine without throwing out all the entry_cursors we have set up?
// we only have to chase intervals from the beginning if ec.cur has become inactive // we only have to chase intervals from the beginning if ec.cur has become inactive
NOT_IMPLEMENTED_YET();
return l_undef;
} }
lbool viable::find_viable2(pvar v, rational& lo, rational& hi) { lbool viable::find_viable2(pvar v, rational& lo, rational& hi) {