From 7b3eaf75ce9cbc678c71089520d7512e43243a77 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Mon, 9 Aug 2021 13:53:15 -0700 Subject: [PATCH] validate and fix fixed/diff Signed-off-by: Nikolaj Bjorner --- src/math/interval/mod_interval_def.h | 15 +++-- src/test/mod_interval.cpp | 82 +++++++++++++--------------- 2 files changed, 47 insertions(+), 50 deletions(-) diff --git a/src/math/interval/mod_interval_def.h b/src/math/interval/mod_interval_def.h index 7e15c9741..06b12b56c 100644 --- a/src/math/interval/mod_interval_def.h +++ b/src/math/interval/mod_interval_def.h @@ -148,8 +148,6 @@ Numeral mod_interval::closest_value(Numeral const& n) const { return hi - 1; } -// TBD: correctness and completeness for wrap-around semantics needs to be checked/fixed - template mod_interval& mod_interval::intersect_uge(Numeral const& l) { if (is_empty()) @@ -262,12 +260,17 @@ mod_interval& mod_interval::intersect_diff(Numeral const& a) { set_empty(); else if (a == lo && hi == 0 && is_max(a)) 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)) lo = a + 1; else if (a + 1 == hi) hi = a; else if (hi == 0 && is_max(a)) hi = a; + return *this; } @@ -275,9 +278,9 @@ template mod_interval& mod_interval::update_lo(Numeral const& new_lo) { SASSERT(lo <= new_lo); if (lo < hi && hi <= new_lo) - set_empty(); + set_empty(); else - lo = new_lo; + lo = new_lo; return *this; } @@ -285,8 +288,8 @@ template mod_interval& mod_interval::update_hi(Numeral const& new_hi) { SASSERT(new_hi <= hi); if (new_hi <= lo && lo < hi) - set_empty(); + set_empty(); else - hi = new_hi; + hi = new_hi; return *this; } diff --git a/src/test/mod_interval.cpp b/src/test/mod_interval.cpp index 92aa03371..ab617e581 100644 --- a/src/test/mod_interval.cpp +++ b/src/test/mod_interval.cpp @@ -92,23 +92,16 @@ static void test_interval2() { std::cout << " < 501: " << i << " -> " << i.intersect_ult(501) << "\n"; } -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 x(i, j); - mod_interval y(k, l); - auto r = x & y; +static void validate_is_intersection(char const* t, mod_interval const& x, mod_interval const& y, mod_interval const& r) { bool x_not_y = false, y_not_x = false; // check that & computes a join // it contains all elements 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 - for (i = 0; i < 256; ++i) { + for (unsigned i = 0; i < 256; ++i) { uint8_t c = (uint8_t)i; - if ((x.contains(c) && y.contains(c)) && !r.contains(c)) { - std::cout << x << " & " << y << " = " << r << "\n"; + if ((x.contains(c) && y.contains(c)) && !r.contains(c)) { + std::cout << t << " " << x << " & " << y << " = " << r << "\n"; std::cout << i << " " << r.contains(c) << " " << x.contains(c) << " " << y.contains(c) << "\n"; } 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; } 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); } } +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 x(i, j); + mod_interval y(k, l); + auto r = x & y; + validate_is_intersection("&", x, y, r); +} + static void test_interval_intersect() { 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 x0(i, j); auto validate = [&](char const* t, mod_interval const& y, mod_interval const& z) { - if (y == z) - return; - std::cout << t << "(" << (unsigned)k << ") " << x0 << " -> " << y << " " << z << "\n"; - SASSERT(false); + validate_is_intersection(t, x0, y, z); }; { mod_interval x = x0; - auto uge2 = x & mod_interval(k, 0); - auto uge1 = x.intersect_uge(k); - validate("uge", uge1, uge2); + validate("uge", mod_interval(k, 0), x.intersect_uge(k)); } { mod_interval x = x0; - auto ule1 = x.intersect_ule(k); - if ((uint8_t)(k + 1) != 0) { - auto ule2 = x0 & mod_interval(0, k + 1); - validate("ule", ule1, ule2); - } - else { - validate("ule", ule1, x0); - } + validate("ule", mod_interval(0, k + 1), x.intersect_ule(k)); } { mod_interval x = x0; - auto ult1 = x.intersect_ult(k); - if (k != 0) { - auto ult2 = x0 & mod_interval(0, k); - validate("ult", ult1, ult2); - } - else { - validate("ult", ult1, mod_interval::empty()); - } + if (k != 0) + validate("ult", mod_interval(0, k), x.intersect_ult(k)); + else + validate("ult", mod_interval::empty(), x.intersect_ult(k)); } + { mod_interval x = x0; - auto ugt1 = x.intersect_ugt(k); - - if ((uint8_t)(k + 1) != 0) { - auto ugt2 = x0 & mod_interval(k + 1, 0); - validate("ugt", ugt1, ugt2); - } - else { - validate("ugt", ugt1, mod_interval::empty()); - } + if ((uint8_t)(k + 1) != 0) + validate("ugt", mod_interval(k + 1, 0), x.intersect_ugt(k)); + else + validate("ugt", mod_interval::empty(), x.intersect_ugt(k)); + } + + { + mod_interval x = x0; + validate("fix", mod_interval(k, k + 1), x.intersect_fixed(k)); + } + + { + mod_interval x = x0; + validate("diff", mod_interval(k + 1, k), x.intersect_diff(k)); } }