From 55fc57b5c72f7fcda7b996edda780f116fedecaa Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sun, 26 Jan 2025 11:24:26 -0800 Subject: [PATCH] relax out of range restrictions to handle large intervals --- src/ast/sls/sls_arith_base.cpp | 85 +++++++++++++++++++++++++++++----- src/ast/sls/sls_arith_base.h | 22 ++++++--- 2 files changed, 89 insertions(+), 18 deletions(-) diff --git a/src/ast/sls/sls_arith_base.cpp b/src/ast/sls/sls_arith_base.cpp index 2fc595c5a4..cc8e8a3be1 100644 --- a/src/ast/sls/sls_arith_base.cpp +++ b/src/ast/sls/sls_arith_base.cpp @@ -444,7 +444,7 @@ namespace sls { auto old_value = value(v); auto new_value = old_value + delta; if (!vi.in_range(new_value)) { - TRACE("arith", tout << "out of range: v" << v << " " << old_value << " " << delta << " " << new_value << "\n";); + TRACE("arith", display(tout, v) << "out of range: v" << v << " " << old_value << " " << delta << " " << new_value << "\n";); return false; } @@ -746,10 +746,14 @@ namespace sls { auto old_value = vi.value(); if (old_value == new_value) return true; - if (!vi.in_range(new_value)) + if (!vi.in_range(new_value)) { + TRACE("arith", display(tout << "out of range " << new_value << ": ", v) << "\n"; ); return false; - if (!in_bounds(v, new_value) && in_bounds(v, old_value)) + } + if (!in_bounds(v, new_value) && in_bounds(v, old_value)) { + TRACE("arith", tout << "out of bounds: v" << v << " " << old_value << " " << new_value << "\n";); return false; + } // check for overflow try { @@ -1873,22 +1877,64 @@ namespace sls { template bool arith_base::repair_idiv(op_def const& od) { + + auto val = value(od.m_var); auto v1 = value(od.m_arg1); auto v2 = value(od.m_arg2); - IF_VERBOSE(0, verbose_stream() << "TODO repair div"); + if (v2 == 0 && val == 0) + return true; + if (v2 != 0 && val == div(v1, v2)) + return true; + if (repair_div_idiv(od, val, v1, v2)) + return true; + + IF_VERBOSE(1, verbose_stream() << "revert repair-down " << val << " = " << v1 << " div " << v2 << "\n"); // bail return update(od.m_var, v2 == 0 ? num_t(0) : div(v1, v2)); - } + } template bool arith_base::repair_div(op_def const& od) { + auto val = value(od.m_var); auto v1 = value(od.m_arg1); auto v2 = value(od.m_arg2); - IF_VERBOSE(0, verbose_stream() << "TODO repair /"); + if (v2 == 0 && val == 0) + return true; + if (v2 != 0 && val == v1 / v2) + return true; + + if (repair_div_idiv(od, val, v1, v2)) + return true; + + IF_VERBOSE(1, verbose_stream() << "revert repair-down " << val << " = " << v1 << "/" << v2 << "\n"); // bail return update(od.m_var, v2 == 0 ? num_t(0) : v1 / v2); } + template + bool arith_base::repair_div_idiv(op_def const& od, num_t const& val, num_t const& v1, num_t const& v2) { + if (val == 1) { + if (v2 != 0 && ctx.rand(2) == 0) + return update(od.m_arg1, v2); + if (v1 != 0 && ctx.rand(2) == 0) + return update(od.m_arg2, v1); + } + if (val == 0) { + SASSERT(v2 != 0); + if (ctx.rand(2) == 0) + return update(od.m_arg1, num_t(0)); + if (ctx.rand(2) == 0) + return update(od.m_arg2, num_t(0)); + } + if (val == -1) { + if (v2 != 0 && ctx.rand(2) == 0) + return update(od.m_arg1, -v2); + if (v1 != 0 && ctx.rand(2) == 0) + return update(od.m_arg2, -v1); + } + return false; + } + template double arith_base::compute_score(var_t x, num_t const& delta) { int result = 0; @@ -2245,6 +2291,8 @@ namespace sls { bool r = update(w, n); if (!r) { + TRACE("arith", tout << "set value failed " << mk_pp(e, m) << " := " << mk_pp(v, m) << "\n"; + display(tout, w) << " := " << value(w) << "\n";); IF_VERBOSE(3, verbose_stream() << "set value failed " << mk_pp(e, m) << " := " << mk_pp(v, m) << "\n"; display(verbose_stream(), w) << " := " << value(w) << "\n"); @@ -2368,15 +2416,20 @@ namespace sls { return out; } + template<> + bool arith_base::var_info::is_big_num() const { return true; } + template - std::ostream& arith_base::display(std::ostream& out, var_t v) const { - auto const& vi = m_vars[v]; - auto const& lo = vi.m_lo; - auto const& hi = vi.m_hi; - out << "v" << v << " := " << vi.value() << " "; + bool arith_base::var_info::is_big_num() const { return false; } + + template + std::ostream& arith_base::var_info::display_range(std::ostream& out) const { + auto const& lo = m_lo; + auto const& hi = m_hi; + if (lo || hi) { if (lo) - out << (lo->is_strict ? "(": "[") << lo->value; + out << (lo->is_strict ? "(" : "[") << lo->value; else out << "("; out << " "; @@ -2386,6 +2439,14 @@ namespace sls { out << ")"; out << " "; } + return out; + } + + template + std::ostream& arith_base::display(std::ostream& out, var_t v) const { + auto const& vi = m_vars[v]; + out << "v" << v << " := " << vi.value() << " "; + vi.display_range(out); out << mk_bounded_pp(vi.m_expr, m) << " "; if (is_add(v)) display(out << "add: ", get_add(v)) << " "; diff --git a/src/ast/sls/sls_arith_base.h b/src/ast/sls/sls_arith_base.h index a504583751..1d99588d6d 100644 --- a/src/ast/sls/sls_arith_base.h +++ b/src/ast/sls/sls_arith_base.h @@ -127,20 +127,27 @@ namespace sls { num_t const& best_value() const { return m_best_value; } void set_best_value(num_t const& v) { m_best_value = v; } + bool is_big_num() const; + bool in_range(num_t const& n) { if (-m_range < n && n < m_range) return true; bool result = false; +#if 0 + if (m_lo && m_lo->value > n) + return false; + if (m_hi && m_hi->value < n) + return false; +#endif if (m_lo) result = n < m_lo->value + m_range; if (!result && m_hi) result = n > m_hi->value - m_range; -#if 0 - if (!result) - out_of_range(); - else - ++m_num_in_range; -#endif + if (!result && m_lo && m_hi) + result = m_hi->value - m_lo->value > 2 * m_range; + if (!result && is_big_num() && !m_lo && !m_hi) + result = true; + return result; } unsigned m_tabu_pos = 0, m_tabu_neg = 0; @@ -166,6 +173,8 @@ namespace sls { m_num_out_of_range = 0; m_num_in_range = 0; } + + std::ostream& display_range(std::ostream& out) const; }; struct mul_def { @@ -232,6 +241,7 @@ namespace sls { bool repair_mod(op_def const& od); bool repair_idiv(op_def const& od); bool repair_div(op_def const& od); + bool repair_div_idiv(op_def const& od, num_t const& val, num_t const& v1, num_t const& v2); bool repair_rem(op_def const& od); bool repair_power(op_def const& od); bool repair_abs(op_def const& od);