mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-28 11:25:51 +00:00
Code Activity

test / fix wrap-around for mod-interval

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2021-07-03 10:49:22 -07:00
parent 1355ea432a
commit ff717a9db1
5 changed files with 120 additions and 51 deletions
Download patch file Download diff file Expand all files Collapse all files

78
src/math/interval/mod_interval_def.h
View file

@ -123,20 +123,6 @@ Numeral mod_interval<Numeral>::closest_value(Numeral const& n) const {
// TBD: correctness and completeness for wrap-around semantics needs to be checked/fixed
template<typename Numeral>
mod_interval<Numeral>& mod_interval<Numeral>::intersect_ule(Numeral const& h) {
if (is_empty())
return *this;
if (is_max(h))
return *this;
else if (is_free())
lo = 0, hi = h + 1;
else if (hi > lo && lo > h)
set_empty();
else if (hi == 0 || h + 1 < hi)
hi = h + 1;
return *this;
}
template<typename Numeral>
mod_interval<Numeral>& mod_interval<Numeral>::intersect_uge(Numeral const& l) {
@ -148,6 +134,50 @@ mod_interval<Numeral>& mod_interval<Numeral>::intersect_uge(Numeral const& l) {
lo = l, hi = 0;
else if ((lo < hi || hi == 0) && lo < l)
lo = l;
else if (hi < lo && hi <= l && l <= lo)
hi = 0;
else if (hi < lo && lo < l)
hi = 0, lo = l;
return *this;
}
template<typename Numeral>
mod_interval<Numeral>& mod_interval<Numeral>::intersect_ugt(Numeral const& l) {
if (is_empty())
return *this;
if (is_max(l))
set_empty();
else if (is_free())
lo = l + 1, hi = 0;
else if (lo < hi && hi <= l)
set_empty();
else if (lo < hi)
lo = l + 1;
else if (hi < lo && hi <= l + 1 && l <= lo - 1)
hi = 0;
else if (hi < lo && lo <= l)
hi = 0, lo = l + 1;
return *this;
}
template<typename Numeral>
mod_interval<Numeral>& mod_interval<Numeral>::intersect_ule(Numeral const& h) {
if (is_empty())
return *this;
if (is_max(h))
return *this;
else if (is_free())
lo = 0, hi = h + 1;
else if (hi > lo && lo > h)
set_empty();
else if (hi == 0 && h >= lo)
hi = h + 1;
else if (lo <= h && h + 1 < hi)
hi = h + 1;
else if (hi < lo && h < hi)
hi = h + 1, lo = 0;
else if (hi <= h && h < lo)
lo = 0;
return *this;
}
@ -163,25 +193,13 @@ mod_interval<Numeral>& mod_interval<Numeral>::intersect_ult(Numeral const& h) {
set_empty();
else if (hi > lo && h < hi)
hi = h;
else if (hi < lo && h <= hi)
hi = h, lo = 0;
else if (hi < h && h <= lo)
lo = 0;
return *this;
}
template<typename Numeral>
mod_interval<Numeral>& mod_interval<Numeral>::intersect_ugt(Numeral const& l) {
if (is_empty())
return *this;
if (is_max(l))
set_empty();
else if (is_free())
lo = l + 1, hi = 0;
else if (lo > l)
return *this;
else if (lo < hi && hi <= l)
set_empty();
else if (lo < hi)
lo = l + 1;
return *this;
}
template<typename Numeral>
mod_interval<Numeral>& mod_interval<Numeral>::intersect_fixed(Numeral const& a) {