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

more unit testing and fixes

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2021-08-09 10:50:30 -07:00
parent 6a829f831d
commit d07b508ecd
3 changed files with 101 additions and 10 deletions
Download patch file Download diff file Expand all files Collapse all files

14
src/math/interval/mod_interval.h
View file

@ -45,7 +45,7 @@ inline std::ostream& operator<<(std::ostream& out, pp<rational> const& p) {
template<typename Numeral>
class mod_interval {
bool emp { false };
bool emp = false;
public:
Numeral lo { 0 };
Numeral hi { 0 };
@ -59,7 +59,7 @@ public:
bool is_empty() const { return emp; }
bool is_singleton() const { return !is_empty() && (lo + 1 == hi || (hi == 0 && is_max(lo))); }
bool contains(Numeral const& n) const;
virtual bool is_max(Numeral const& n) const { return n + 1 == 0; }
virtual bool is_max(Numeral const& n) const { return (Numeral)(n + 1) == 0; }
void set_free() { lo = hi = 0; emp = false; }
void set_bounds(Numeral const& l, Numeral const& h) { lo = l; hi = h; }
@ -89,6 +89,16 @@ public:
return out << "[" << pp(lo) << ", " << pp(hi) << "[";
}
Numeral closest_value(Numeral const& n) const;
bool operator==(mod_interval const& other) const {
if (is_empty())
return other.is_empty();
if (is_free())
return other.is_free();
return lo == other.lo && hi == other.hi;
}
bool operator!=(mod_interval const& other) const {
return !(*this == other);
}
};
template<typename Numeral>

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

@ -143,7 +143,7 @@ Numeral mod_interval<Numeral>::closest_value(Numeral const& n) const {
return n;
if (is_empty())
return n;
if (lo - n < n - hi)
if ((Numeral)(lo - n) < (Numeral)(n - hi))
return lo;
return hi - 1;
}
@ -159,11 +159,13 @@ mod_interval<Numeral>& mod_interval<Numeral>::intersect_uge(Numeral const& l) {
else if (is_free())
lo = l, hi = 0;
else if ((lo < hi || hi == 0) && lo < l)
lo = l;
lo = l;
else if (hi < lo && hi <= l && l <= lo)
hi = 0;
else if (hi < lo && lo < l)
hi = 0, lo = l;
else if (0 < l && l < hi && hi < lo)
lo = l, hi = 0;
return *this;
}
@ -175,14 +177,18 @@ mod_interval<Numeral>& mod_interval<Numeral>::intersect_ugt(Numeral const& l) {
set_empty();
else if (is_free())
lo = l + 1, hi = 0;
else if (lo < hi && hi <= l)
else if (lo < hi && hi - 1 <= l)
set_empty();
else if (lo < hi)
else if (lo < hi && l < lo)
return *this;
else if (lo < hi)
lo = l + 1;
else if (hi < lo && hi <= l + 1 && l < lo)
hi = 0;
else if (hi < lo && lo <= l)
hi = 0, lo = l + 1;
else if (l <= hi && hi < lo)
lo = l + 1, hi = 0;
return *this;
}
@ -194,16 +200,22 @@ mod_interval<Numeral>& mod_interval<Numeral>::intersect_ule(Numeral const& h) {
return *this;
else if (is_free())
lo = 0, hi = h + 1;
else if (hi > lo && lo > h)
else if (h < lo && (lo < hi || hi == 0))
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)
else if (h < hi && hi < lo)
hi = h + 1, lo = 0;
else if (hi <= h && h < lo)
lo = 0;
else if (hi == 0 && hi == h && hi < lo)
set_empty();
else if (0 < hi && hi == h && hi < lo)
lo = 0;
else if (0 < hi && hi < h && hi < lo)
lo = 0, hi = h + 1;
return *this;
}
@ -215,14 +227,16 @@ mod_interval<Numeral>& mod_interval<Numeral>::intersect_ult(Numeral const& h) {
set_empty();
else if (is_free())
lo = 0, hi = h;
else if (hi > lo && lo >= h)
else if (h <= lo && (lo < hi || hi == 0))
set_empty();
else if (hi > lo && h < hi)
else if (h > lo && (h < hi || hi == 0))
hi = h;
else if (hi < lo && h <= hi)
hi = h, lo = 0;
else if (hi < h && h <= lo)
lo = 0;
else if (0 < hi && hi < lo && hi + 1 <= h)
lo = 0, hi = h;
return *this;
}