mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-08-02 17:30:23 +00:00
Code Activity

validate and fix fixed/diff

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2021-08-09 13:53:15 -07:00
parent d07b508ecd
commit 7b3eaf75ce
2 changed files with 47 additions and 50 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -148,8 +148,6 @@ Numeral mod_interval<Numeral>::closest_value(Numeral const& n) const {
return hi - 1; return hi - 1;
} }
// TBD: correctness and completeness for wrap-around semantics needs to be checked/fixed
template<typename Numeral> template<typename Numeral>
mod_interval<Numeral>& mod_interval<Numeral>::intersect_uge(Numeral const& l) { mod_interval<Numeral>& mod_interval<Numeral>::intersect_uge(Numeral const& l) {
if (is_empty()) if (is_empty())
@ -262,12 +260,17 @@ mod_interval<Numeral>& mod_interval<Numeral>::intersect_diff(Numeral const& a) {
set_empty(); set_empty();
else if (a == lo && hi == 0 && is_max(a)) else if (a == lo && hi == 0 && is_max(a))
set_empty(); set_empty();
else if (is_free())
lo = a + 1, hi = a;
else if (0 < hi && hi < lo && a == lo)
return *this;
else if (a == lo && !is_max(a)) else if (a == lo && !is_max(a))
lo = a + 1; lo = a + 1;
else if (a + 1 == hi) else if (a + 1 == hi)
hi = a; hi = a;
else if (hi == 0 && is_max(a)) else if (hi == 0 && is_max(a))
hi = a; hi = a;
return *this; return *this;
} }
@ -275,9 +278,9 @@ template<typename Numeral>
mod_interval<Numeral>& mod_interval<Numeral>::update_lo(Numeral const& new_lo) { mod_interval<Numeral>& mod_interval<Numeral>::update_lo(Numeral const& new_lo) {
SASSERT(lo <= new_lo); SASSERT(lo <= new_lo);
if (lo < hi && hi <= new_lo) if (lo < hi && hi <= new_lo)
set_empty(); set_empty();
else else
lo = new_lo; lo = new_lo;
return *this; return *this;
} }
@ -285,8 +288,8 @@ template<typename Numeral>
mod_interval<Numeral>& mod_interval<Numeral>::update_hi(Numeral const& new_hi) { mod_interval<Numeral>& mod_interval<Numeral>::update_hi(Numeral const& new_hi) {
SASSERT(new_hi <= hi); SASSERT(new_hi <= hi);
if (new_hi <= lo && lo < hi) if (new_hi <= lo && lo < hi)
set_empty(); set_empty();
else else
hi = new_hi; hi = new_hi;
return *this; return *this;
} }

80
src/test/mod_interval.cpp
View file

@ -92,23 +92,16 @@ static void test_interval2() {
std::cout << " < 501: " << i << " -> " << i.intersect_ult(501) << "\n"; std::cout << " < 501: " << i << " -> " << i.intersect_ult(501) << "\n";
} }
static void test_interval_intersect(unsigned i, unsigned j, unsigned k, unsigned l) { static void validate_is_intersection(char const* t, mod_interval<uint8_t> const& x, mod_interval<uint8_t> const& y, mod_interval<uint8_t> const& r) {
if (i == j && i != 0)
return;
if (k == l && k != 0)
return;
mod_interval<uint8_t> x(i, j);
mod_interval<uint8_t> y(k, l);
auto r = x & y;
bool x_not_y = false, y_not_x = false; bool x_not_y = false, y_not_x = false;
// check that & computes a join // check that & computes a join
// it contains all elements in x, y // it contains all elements in x, y
// it contains no elements neither in x, y // it contains no elements neither in x, y
// it does not contain two elements, one in x\y the other in y\x // it does not contain two elements, one in x\y the other in y\x
for (i = 0; i < 256; ++i) { for (unsigned i = 0; i < 256; ++i) {
uint8_t c = (uint8_t)i; uint8_t c = (uint8_t)i;
if ((x.contains(c) && y.contains(c)) && !r.contains(c)) { if ((x.contains(c) && y.contains(c)) && !r.contains(c)) {
std::cout << x << " & " << y << " = " << r << "\n"; std::cout << t << " " << x << " & " << y << " = " << r << "\n";
std::cout << i << " " << r.contains(c) << " " << x.contains(c) << " " << y.contains(c) << "\n"; std::cout << i << " " << r.contains(c) << " " << x.contains(c) << " " << y.contains(c) << "\n";
} }
VERIFY(!(x.contains(c) && y.contains(c)) || r.contains(c)); VERIFY(!(x.contains(c) && y.contains(c)) || r.contains(c));
@ -119,11 +112,22 @@ static void test_interval_intersect(unsigned i, unsigned j, unsigned k, unsigned
y_not_x = true; y_not_x = true;
} }
if (x_not_y && y_not_x) { if (x_not_y && y_not_x) {
std::cout << x << " & " << y << " = " << r << "\n"; std::cout << t << " " << x << " & " << y << " = " << r << "\n";
VERIFY(!x_not_y || !y_not_x); VERIFY(!x_not_y || !y_not_x);
} }
} }
static void test_interval_intersect(unsigned i, unsigned j, unsigned k, unsigned l) {
if (i == j && i != 0)
return;
if (k == l && k != 0)
return;
mod_interval<uint8_t> x(i, j);
mod_interval<uint8_t> y(k, l);
auto r = x & y;
validate_is_intersection("&", x, y, r);
}
static void test_interval_intersect() { static void test_interval_intersect() {
unsigned bounds[8] = { 0, 1, 2, 3, 252, 253, 254, 255 }; unsigned bounds[8] = { 0, 1, 2, 3, 252, 253, 254, 255 };
@ -140,53 +144,43 @@ static void test_interval_intersect2(unsigned i, unsigned j, uint8_t k) {
mod_interval<uint8_t> x0(i, j); mod_interval<uint8_t> x0(i, j);
auto validate = [&](char const* t, mod_interval<uint8_t> const& y, mod_interval<uint8_t> const& z) { auto validate = [&](char const* t, mod_interval<uint8_t> const& y, mod_interval<uint8_t> const& z) {
if (y == z) validate_is_intersection(t, x0, y, z);
return;
std::cout << t << "(" << (unsigned)k << ") " << x0 << " -> " << y << " " << z << "\n";
SASSERT(false);
}; };
{ {
mod_interval<uint8_t> x = x0; mod_interval<uint8_t> x = x0;
auto uge2 = x & mod_interval<uint8_t>(k, 0); validate("uge", mod_interval<uint8_t>(k, 0), x.intersect_uge(k));
auto uge1 = x.intersect_uge(k);
validate("uge", uge1, uge2);
} }
{ {
mod_interval<uint8_t> x = x0; mod_interval<uint8_t> x = x0;
auto ule1 = x.intersect_ule(k); validate("ule", mod_interval<uint8_t>(0, k + 1), x.intersect_ule(k));
if ((uint8_t)(k + 1) != 0) {
auto ule2 = x0 & mod_interval<uint8_t>(0, k + 1);
validate("ule", ule1, ule2);
}
else {
validate("ule", ule1, x0);
}
} }
{ {
mod_interval<uint8_t> x = x0; mod_interval<uint8_t> x = x0;
auto ult1 = x.intersect_ult(k); if (k != 0)
if (k != 0) { validate("ult", mod_interval<uint8_t>(0, k), x.intersect_ult(k));
auto ult2 = x0 & mod_interval<uint8_t>(0, k); else
validate("ult", ult1, ult2); validate("ult", mod_interval<uint8_t>::empty(), x.intersect_ult(k));
}
else {
validate("ult", ult1, mod_interval<uint8_t>::empty());
}
} }
{ {
mod_interval<uint8_t> x = x0; mod_interval<uint8_t> x = x0;
auto ugt1 = x.intersect_ugt(k); if ((uint8_t)(k + 1) != 0)
validate("ugt", mod_interval<uint8_t>(k + 1, 0), x.intersect_ugt(k));
else
validate("ugt", mod_interval<uint8_t>::empty(), x.intersect_ugt(k));
}
if ((uint8_t)(k + 1) != 0) { {
auto ugt2 = x0 & mod_interval<uint8_t>(k + 1, 0); mod_interval<uint8_t> x = x0;
validate("ugt", ugt1, ugt2); validate("fix", mod_interval<uint8_t>(k, k + 1), x.intersect_fixed(k));
} }
else {
validate("ugt", ugt1, mod_interval<uint8_t>::empty()); {
} mod_interval<uint8_t> x = x0;
validate("diff", mod_interval<uint8_t>(k + 1, k), x.intersect_diff(k));
} }
} }