From 5a57636cd89911f3cec15e67fdf53f62c4d4fbf6 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Fri, 3 Jan 2025 10:56:15 -0800 Subject: [PATCH] use native sdiv Signed-off-by: Nikolaj Bjorner --- src/ast/sls/sls_bv_eval.cpp | 57 +++++++++++++++++++++++++++++--- src/ast/sls/sls_bv_eval.h | 2 ++ src/ast/sls/sls_bv_lookahead.cpp | 10 +++++- src/ast/sls/sls_bv_terms.cpp | 2 +- src/util/uint_set.h | 5 +++ 5 files changed, 69 insertions(+), 7 deletions(-) diff --git a/src/ast/sls/sls_bv_eval.cpp b/src/ast/sls/sls_bv_eval.cpp index 1e5c9822ce3..2d59b8c34ae 100644 --- a/src/ast/sls/sls_bv_eval.cpp +++ b/src/ast/sls/sls_bv_eval.cpp @@ -724,11 +724,11 @@ namespace sls { case OP_BSMOD: case OP_BSMOD_I: case OP_BSMOD0: + return true; + default: case OP_BSDIV: case OP_BSDIV_I: case OP_BSDIV0: - return true; - default: return false; } } @@ -916,15 +916,17 @@ namespace sls { case OP_BSMUL_OVFL: verbose_stream() << mk_pp(e, m) << "\n"; return false; + case OP_BSDIV: + case OP_BSDIV_I: + case OP_BSDIV0: + return try_repair_sdiv(assign_value(e), wval(e, 0), wval(e, 1), i); case OP_BSREM: case OP_BSREM_I: case OP_BSREM0: case OP_BSMOD: case OP_BSMOD_I: case OP_BSMOD0: - case OP_BSDIV: - case OP_BSDIV_I: - case OP_BSDIV0: + UNREACHABLE(); // these are currently compiled to udiv and urem. // there is an equation that enforces equality between the semantics @@ -1223,6 +1225,51 @@ namespace sls { return a.set_random(m_rand); } + + bool bv_eval::try_repair_sdiv(bvect const& e, bvval& a, bvval& b, unsigned i) { + + bool sign_a = a.sign(); + bool sign_b = b.sign(); + bool sign_e = e.get(a.bw - 1); + + // y = 0, x >= 0 -> -1 + if (i == 0 && b.is_zero() && a.is_ones(e) && a.try_set(m_zero)) + return true; + if (i == 0 && b.is_zero() && a.is_ones(e) && a.try_set_bit(a.bw - 1, false)) + return true; + + if (i == 1 && !sign_a && a.is_ones(e) && b.try_set(m_zero)) + return true; + + // y = 0, x < 0 -> 1 + if (i == 0 && b.is_zero() && a.is_one(e) && a.try_set(m_minus_one)) + return true; + + if (i == 1 && sign_a && a.is_one(e) && b.try_set(m_zero)) + return true; + + // x = 0, y != 0 -> 0 + if (i == 0 && a.is_zero(e) && !b.is_zero() && a.try_set(m_zero)) + return true; + if (i == 1 && a.is_zero(e) && a.is_zero() && b.try_set_bit(ctx.rand(a.bw), true)) + return true; + + // e = x udiv y + // e = 0 => x != ones + // y = 0 => e = -1 // nothing to repair on a + // e != -1 => max(y) >=u e + + //IF_VERBOSE(0, verbose_stream() << "sdiv " << e << " " << a << " " << b << "\n";); + + // e = udiv(abs(x), abs(y)) + // x > 0, y < 0 -> -e + // x < 0, y > 0 -> -e + // x > 0, y > 0 -> e + // x < 0, y < 0 -> e + + return try_repair_udiv(e, a, b, i); + } + bool bv_eval::try_repair_bnot(bvect const& e, bvval& a) { for (unsigned i = 0; i < a.nw; ++i) m_tmp[i] = ~e[i]; diff --git a/src/ast/sls/sls_bv_eval.h b/src/ast/sls/sls_bv_eval.h index b8d977ca82f..ef016c7d50a 100644 --- a/src/ast/sls/sls_bv_eval.h +++ b/src/ast/sls/sls_bv_eval.h @@ -110,6 +110,7 @@ namespace sls { bool try_repair_lshr1(bvect const& e, bvval const& a, bvval& b); bool try_repair_ashr0(bvect const& e, bvval& a, bvval const& b); bool try_repair_ashr1(bvect const& e, bvval const& a, bvval& b); + bool try_repair_sdiv(bvect const& e, bvval& a, bvval& b, unsigned i); bool try_repair_bit2bool(bvval& a, unsigned idx); bool try_repair_udiv(bvect const& e, bvval& a, bvval& b, unsigned i); bool try_repair_urem(bvect const& e, bvval& a, bvval& b, unsigned i); @@ -126,6 +127,7 @@ namespace sls { bool try_repair_comp(bvect const& e, bvval& a, bvval& b, unsigned i); bool try_repair_eq(bool is_true, bvval& a, bvval const& b); bool try_repair_eq(app* e, unsigned i); + bool try_repair_int2bv(bvect const& e, expr* arg); void add_p2_1(bvval const& a, bvect& t) const; diff --git a/src/ast/sls/sls_bv_lookahead.cpp b/src/ast/sls/sls_bv_lookahead.cpp index 69d092d00f9..2e24d0c1a5e 100644 --- a/src/ast/sls/sls_bv_lookahead.cpp +++ b/src/ast/sls/sls_bv_lookahead.cpp @@ -587,8 +587,16 @@ namespace sls { #endif #if 1 - if (allow_costly_flips(mt)) + if (allow_costly_flips(mt)) ctx.flip(v); + else if (false) { + sat::bool_var_set rotated; + unsigned budget = 100; + bool rot = ctx.try_rotate(v, rotated, budget); + (void)rot; + TRACE("bv", tout << "rotate " << v << " " << rot << " " << rotated << "\n";); + verbose_stream() << "rotate " << v << " " << rot << " " << rotated << "\n"; + } #endif } diff --git a/src/ast/sls/sls_bv_terms.cpp b/src/ast/sls/sls_bv_terms.cpp index 0621850c6a8..a46cd589a01 100644 --- a/src/ast/sls/sls_bv_terms.cpp +++ b/src/ast/sls/sls_bv_terms.cpp @@ -40,7 +40,7 @@ namespace sls { expr_ref bv_terms::ensure_binary(expr* e) { expr* x, * y; expr_ref r(m); - if (bv.is_bv_sdiv(e, x, y) || bv.is_bv_sdiv0(e, x, y) || bv.is_bv_sdivi(e, x, y)) + if (false && (bv.is_bv_sdiv(e, x, y) || bv.is_bv_sdiv0(e, x, y) || bv.is_bv_sdivi(e, x, y))) r = mk_sdiv(x, y); else if (bv.is_bv_smod(e, x, y) || bv.is_bv_smod0(e, x, y) || bv.is_bv_smodi(e, x, y)) r = mk_smod(x, y); diff --git a/src/util/uint_set.h b/src/util/uint_set.h index f936f1134c1..196930d178b 100644 --- a/src/util/uint_set.h +++ b/src/util/uint_set.h @@ -369,3 +369,8 @@ inline std::ostream& operator<<(std::ostream& out, indexed_uint_set const& s) { for (unsigned i : s) out << i << " "; return out; } + +inline std::ostream& operator<<(std::ostream& out, tracked_uint_set const& s) { + for (unsigned i : s) out << i << " "; + return out; +}