diff --git a/src/tests/util/interval/interval.cpp b/src/tests/util/interval/interval.cpp index 7ef6a0e40..9dbeb1861 100644 --- a/src/tests/util/interval/interval.cpp +++ b/src/tests/util/interval/interval.cpp @@ -91,9 +91,78 @@ static void tst2() { lean_assert_eq(power(qi(), 2), qi(false, 0)); // (-oo, oo)^2 == [0, oo) } +static void check_deps(bound_deps const & deps, bool l1 = false, bool u1 = false, bool l2 = false, bool u2 = false) { + lean_assert(l1 == dep_in_lower1(deps)); + lean_assert(u1 == dep_in_upper1(deps)); + lean_assert(l2 == dep_in_lower2(deps)); + lean_assert(u2 == dep_in_upper2(deps)); +} + +static void check_lower_deps(interval_deps const & deps, bool l1 = false, bool u1 = false, bool l2 = false, bool u2 = false) { + check_deps(deps.m_lower_deps, l1, u1, l2, u2); +} + +static void check_upper_deps(interval_deps const & deps, bool l1 = false, bool u1 = false, bool l2 = false, bool u2 = false) { + check_deps(deps.m_upper_deps, l1, u1, l2, u2); +} + +static void tst3() { + qi i1(3, 10, false, true); + qi i2(-8, 2, true, false); + swap(i1, i2); + lean_assert_eq(i1, qi(-8, 2, true, false)); + lean_assert_eq(i2, qi(3, 10, false, true)); + lean_assert(!qi(2, 3, true, true).contains(qi())); + lean_assert(!qi(2, 10, true, true).contains(qi(0, 10, true, true))); + lean_assert(!qi(2, 10, true, true).contains(qi(2, 10, false, true))); + lean_assert(!qi(2, 10, true, true).contains(qi(true, 5))); + lean_assert(!qi(2, 10, true, true).contains(qi(5, 11, true, true))); + lean_assert(!qi(2, 10, true, true).contains(qi(5, 10, true, false))); + lean_assert(!i1.is_empty()); + i1.set_empty(); + lean_assert(i1.is_empty()); + lean_assert(!i1.is_singleton()); + lean_assert(!i2.is_singleton()); + i1 = qi(4); + lean_assert(i1.is_singleton()); + lean_assert(!qi(true, 1).before(qi(1, 2))); + std::cout << qi(3, true) << "\n"; + lean_assert(!qi(1, 2).before(qi(3, true))); + lean_assert(qi(1, 2).before(qi(3, 4))); + interval_deps deps; + qi().neg_jst(deps); + lean_assert_eq(neg(qi()), qi()); + check_lower_deps(deps); + check_upper_deps(deps); + std::cout << qi(1, true) << "\n"; + qi(1, true).neg_jst(deps); + lean_assert_eq(neg(qi(1, true)), qi(true, -1)); + check_lower_deps(deps, false, true); + check_upper_deps(deps); + qi(true, 1).neg_jst(deps); + lean_assert_eq(neg(qi(true, 1)), qi(-1, true)); + check_lower_deps(deps); + check_upper_deps(deps, true, false); + qi(1, 3).neg_jst(deps); + check_lower_deps(deps, false, true); + check_upper_deps(deps, true, false); + qi(1, 3).add_jst(qi(2, 4), deps); + check_lower_deps(deps, true, false, true, false); + check_upper_deps(deps, false, true, false, true); + qi(1, 3).sub_jst(qi(2, 4), deps); + check_lower_deps(deps, true, false, false, true); + check_upper_deps(deps, false, true, true, false); + qi i3(0); + i3 *= mpq(3); + lean_assert_eq(i3, qi(0)); + i3 /= mpq(4); + lean_assert_eq(i3, qi(0)); +} + int main() { enable_trace("numerics"); tst1(); tst2(); + tst3(); return has_violations() ? 1 : 0; } diff --git a/src/util/interval/interval.cpp b/src/util/interval/interval.cpp index 1cfed59f6..a2a267108 100644 --- a/src/util/interval/interval.cpp +++ b/src/util/interval/interval.cpp @@ -130,7 +130,9 @@ bool interval::contains(interval const & b) const { template bool interval::is_empty() const { - return m_lower == m_upper && m_lower_open && m_upper_open && !m_lower_inf && !m_upper_inf; + return + (m_lower == m_upper && (m_lower_open || m_upper_open) && !m_lower_inf && !m_upper_inf) || + (m_lower > m_upper && !m_lower_inf && !m_upper_inf); } template