From 991537836b1ee8b96a00850f6554b4c5a881a0a1 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Mon, 19 Feb 2024 12:59:28 +0700 Subject: [PATCH] fixes based on unit tests --- src/ast/bv_decl_plugin.h | 14 +-- src/ast/sls/bv_sls.cpp | 53 ++++++++- src/ast/sls/bv_sls.h | 3 + src/ast/sls/bv_sls_eval.cpp | 215 ++++++++++++++++++++++++++++------ src/ast/sls/bv_sls_eval.h | 8 ++ src/ast/sls/bv_sls_fixed.cpp | 1 + src/ast/sls/bv_sls_terms.cpp | 6 +- src/ast/sls/sls_valuation.cpp | 126 +++++++++++--------- src/ast/sls/sls_valuation.h | 12 ++ src/test/sls_test.cpp | 36 ++++-- 10 files changed, 363 insertions(+), 111 deletions(-) diff --git a/src/ast/bv_decl_plugin.h b/src/ast/bv_decl_plugin.h index 41c2ef75238..137dc754f59 100644 --- a/src/ast/bv_decl_plugin.h +++ b/src/ast/bv_decl_plugin.h @@ -557,15 +557,15 @@ class bv_util : public bv_recognizers { app* mk_bv_rotate_right(expr* arg, unsigned n); // TODO: all these binary ops commute (right?) but it'd be more logical to swap `n` & `m` in the `return` - app * mk_bvsmul_no_ovfl(expr* m, expr* n) { return m_manager.mk_app(get_fid(), OP_BSMUL_NO_OVFL, n, m); } - app * mk_bvsmul_no_udfl(expr* m, expr* n) { return m_manager.mk_app(get_fid(), OP_BSMUL_NO_UDFL, n, m); } - app * mk_bvumul_no_ovfl(expr* m, expr* n) { return m_manager.mk_app(get_fid(), OP_BUMUL_NO_OVFL, n, m); } - app * mk_bvsmul_ovfl(expr* m, expr* n) { return m_manager.mk_app(get_fid(), OP_BSMUL_OVFL, n, m); } - app * mk_bvumul_ovfl(expr* m, expr* n) { return m_manager.mk_app(get_fid(), OP_BUMUL_OVFL, n, m); } + app * mk_bvsmul_no_ovfl(expr* m, expr* n) { return m_manager.mk_app(get_fid(), OP_BSMUL_NO_OVFL, m, n); } + app * mk_bvsmul_no_udfl(expr* m, expr* n) { return m_manager.mk_app(get_fid(), OP_BSMUL_NO_UDFL, m, n); } + app * mk_bvumul_no_ovfl(expr* m, expr* n) { return m_manager.mk_app(get_fid(), OP_BUMUL_NO_OVFL, m, n); } + app * mk_bvsmul_ovfl(expr* m, expr* n) { return m_manager.mk_app(get_fid(), OP_BSMUL_OVFL, m, n); } + app * mk_bvumul_ovfl(expr* m, expr* n) { return m_manager.mk_app(get_fid(), OP_BUMUL_OVFL, m, n); } app * mk_bvsdiv_ovfl(expr* m, expr* n) { return m_manager.mk_app(get_fid(), OP_BSDIV_OVFL, m, n); } app * mk_bvneg_ovfl(expr* m) { return m_manager.mk_app(get_fid(), OP_BNEG_OVFL, m); } - app * mk_bvuadd_ovfl(expr* m, expr* n) { return m_manager.mk_app(get_fid(), OP_BUADD_OVFL, n, m); } - app * mk_bvsadd_ovfl(expr* m, expr* n) { return m_manager.mk_app(get_fid(), OP_BSADD_OVFL, n, m); } + app * mk_bvuadd_ovfl(expr* m, expr* n) { return m_manager.mk_app(get_fid(), OP_BUADD_OVFL, m, n); } + app * mk_bvsadd_ovfl(expr* m, expr* n) { return m_manager.mk_app(get_fid(), OP_BSADD_OVFL, m, n); } app * mk_bvusub_ovfl(expr* m, expr* n) { return m_manager.mk_app(get_fid(), OP_BUSUB_OVFL, m, n); } app * mk_bvssub_ovfl(expr* m, expr* n) { return m_manager.mk_app(get_fid(), OP_BSSUB_OVFL, m, n); } diff --git a/src/ast/sls/bv_sls.cpp b/src/ast/sls/bv_sls.cpp index 6ba3d734e40..0b136d3901b 100644 --- a/src/ast/sls/bv_sls.cpp +++ b/src/ast/sls/bv_sls.cpp @@ -46,6 +46,31 @@ namespace bv { m_eval.init_fixed(m_terms.assertions()); } + void sls::reinit_eval() { + std::function eval = [&](expr* e, unsigned i) { + if (m.is_bool(e)) { + if (m_eval.is_fixed0(e)) + return m_eval.bval0(e); + } + else if (bv.is_bv(e)) { + auto& w = m_eval.wval0(e); + if (w.get(w.fixed, i)) + return w.get(w.bits, i); + + } + return m_rand() % 2 == 0; + }; + m_eval.init_eval(m_terms.assertions(), eval); + m_repair_down.reset(); + m_repair_up.reset(); + for (auto* e : m_terms.assertions()) { + if (!m_eval.bval0(e)) { + m_eval.set(e, true); + m_repair_down.insert(e->get_id()); + } + } + } + std::pair sls::next_to_repair() { app* e = nullptr; if (!m_repair_down.empty()) { @@ -59,7 +84,7 @@ namespace bv { return { !m_repair_down.empty(), e }; } - lbool sls::operator()() { + lbool sls::search() { // init and init_eval were invoked. unsigned& n = m_stats.m_moves; n = 0; @@ -67,7 +92,7 @@ namespace bv { auto [down, e] = next_to_repair(); if (!e) return l_true; - IF_VERBOSE(20, verbose_stream() << (down?"d ":"u ") << mk_bounded_pp(e, m, 1) << "\n"); + IF_VERBOSE(20, verbose_stream() << (down ? "d " : "u ") << mk_bounded_pp(e, m, 1) << "\n"); if (eval_is_correct(e)) { if (down) m_repair_down.remove(e->get_id()); @@ -75,14 +100,32 @@ namespace bv { m_repair_up.remove(e->get_id()); } else if (down) { - try_repair_down(e); + try_repair_down(e); } - else - try_repair_up(e); + else + try_repair_up(e); } return l_undef; } + lbool sls::operator()() { + lbool res = l_undef; + do { + if (!m.inc()) + return l_undef; + + res = search(); + + if (res != l_undef) + return res; + + reinit_eval(); + } + while (m_stats.m_restarts++ < m_config.m_max_restarts); + + return res; + } + void sls::try_repair_down(app* e) { unsigned n = e->get_num_args(); if (n > 0) { diff --git a/src/ast/sls/bv_sls.h b/src/ast/sls/bv_sls.h index 781174aeed7..c91838a4c36 100644 --- a/src/ast/sls/bv_sls.h +++ b/src/ast/sls/bv_sls.h @@ -57,6 +57,9 @@ namespace bv { bool try_repair_down(app* e, unsigned i); + lbool search(); + void reinit_eval(); + public: sls(ast_manager& m); diff --git a/src/ast/sls/bv_sls_eval.cpp b/src/ast/sls/bv_sls_eval.cpp index 576c0a89e84..3f5d0e27075 100644 --- a/src/ast/sls/bv_sls_eval.cpp +++ b/src/ast/sls/bv_sls_eval.cpp @@ -319,7 +319,7 @@ namespace bv { else b.get(m_tmp2); - mpn.div(m_tmp.data(), a.nw, m_tmp2.data(), a.nw, m_tmp3.data(), m_tmp4.data()); + set_div(m_tmp, m_tmp2, a.bw, m_tmp3, m_tmp4); if (sign_a == sign_b) val.set(m_tmp3); else @@ -500,10 +500,7 @@ namespace bv { if (b.is_zero()) val.set(a.bits); else { - mpn.div(a.bits.data(), a.nw, - b.bits.data(), b.nw, - m_tmp.data(), // quotient - m_tmp2.data()); // remainder + set_div(a.bits, b.bits, b.bw, m_tmp, m_tmp2); val.set(m_tmp2); } break; @@ -530,11 +527,8 @@ namespace bv { if (b.sign()) b.set_sub(m_tmp4, m_zero, b.bits); else - a.set(m_tmp4, b.bits); - mpn.div(m_tmp3.data(), a.nw, - m_tmp4.data(), b.nw, - m_tmp.data(), // quotient - m_tmp2.data()); // remainder + a.set(m_tmp4, b.bits); + set_div(m_tmp3, m_tmp4, a.bw, m_tmp, m_tmp2); if (val.is_zero(m_tmp2)) val.set(m_tmp2); else if (a.sign() && b.sign()) @@ -557,10 +551,7 @@ namespace bv { if (b.is_zero()) val.set(m_minus_one); else { - mpn.div(a.bits.data(), a.nw, - b.bits.data(), b.nw, - m_tmp.data(), // quotient - m_tmp2.data()); // remainder + set_div(a.bits, b.bits, a.bw, m_tmp, m_tmp2); val.set(m_tmp); } break; @@ -705,6 +696,8 @@ namespace bv { return try_repair_bxor(wval0(e), wval0(e, i), wval0(e, 1 - i)); case OP_BADD: return try_repair_add(wval0(e), wval0(e, i), wval0(e, 1 - i)); + case OP_BSUB: + return try_repair_sub(wval0(e), wval0(e, 0), wval0(e, 1), i); case OP_BMUL: return try_repair_mul(wval0(e), wval0(e, i), wval0(e, 1 - i)); case OP_BNOT: @@ -787,20 +780,35 @@ namespace bv { case OP_EXT_ROTATE_LEFT: return try_repair_rotate_left(wval0(e), wval0(e, 0), wval0(e, 1), i); case OP_EXT_ROTATE_RIGHT: - case OP_BCOMP: + return try_repair_rotate_right(wval0(e), wval0(e, 0), wval0(e, 1), i); + case OP_ZERO_EXT: + return try_repair_zero_ext(wval0(e), wval0(e, 0)); + case OP_SIGN_EXT: + return try_repair_zero_ext(wval0(e), wval0(e, 0)); + case OP_CONCAT: + return try_repair_concat(wval0(e), wval0(e, 0), wval0(e, 1), i); + case OP_EXTRACT: { + unsigned hi, lo; + expr* arg; + VERIFY(bv.is_extract(e, lo, hi, arg)); + return try_repair_extract(wval0(e), wval0(arg), lo); + } + case OP_BUMUL_NO_OVFL: + return try_repair_umul_ovfl(!bval0(e), wval0(e, 0), wval0(e, 1), i); + case OP_BUMUL_OVFL: + return try_repair_umul_ovfl(bval0(e), wval0(e, 0), wval0(e, 1), i); + case OP_BUADD_OVFL: + case OP_BCOMP: case OP_BNAND: case OP_BREDAND: case OP_BREDOR: case OP_BXNOR: case OP_BNEG_OVFL: case OP_BSADD_OVFL: - case OP_BUADD_OVFL: case OP_BSDIV_OVFL: case OP_BSMUL_NO_OVFL: case OP_BSMUL_NO_UDFL: case OP_BSMUL_OVFL: - case OP_BUMUL_NO_OVFL: - case OP_BUMUL_OVFL: return false; case OP_BSREM: case OP_BSREM_I: @@ -950,6 +958,21 @@ namespace bv { return true; } + + bool sls_eval::try_repair_sub(bvval const& e, bvval& a, bvval & b, unsigned i) { + if (i == 0) { + // e = a - b -> a := e + b + a.set_add(m_tmp, e.bits, b.bits); + a.set_repair(random_bool(), m_tmp); + } + else { + // b := a - e + a.set_sub(m_tmp, a.bits, e.bits); + a.set_repair(random_bool(), m_tmp); + } + return true; + } + /** * e = a*b, then a = e * b^-1 * 8*e = a*(2b), then a = 4e*b^-1 @@ -998,14 +1021,31 @@ namespace bv { return try_repair_uge(e, a, b.bits); } + // a <=s b <-> a + p2 <=u b + p2 + bool sls_eval::try_repair_sle(bool e, bvval& a, bvval const& b) { - add_p2_1(b, m_tmp4); - return try_repair_ule(e, a, m_tmp4); + //add_p2_1(b, m_tmp4); + a.set(m_tmp, b.bits); + if (e) { + a.set_repair(true, m_tmp); + } + else { + a.set_add(m_tmp2, m_tmp, m_one); + a.set_repair(false, m_tmp2); + } + return true; } bool sls_eval::try_repair_sge(bool e, bvval& a, bvval const& b) { - add_p2_1(b, m_tmp4); - return try_repair_uge(e, a, m_tmp4); + a.set(m_tmp, b.bits); + if (e) { + a.set_repair(false, m_tmp); + } + else { + a.set_sub(m_tmp2, m_tmp, m_one); + a.set_repair(true, m_tmp2); + } + return true; } void sls_eval::add_p2_1(bvval const& a, svector& t) const { @@ -1025,10 +1065,12 @@ namespace bv { a.set_add(m_tmp2, t, m_one); if (a.is_zero(m_tmp2)) return false; - if (!a.get_at_least(m_tmp2, m_tmp)) - return false; + if (!a.get_at_least(m_tmp2, m_tmp)) { + verbose_stream() << "could not get at least\n"; + return false; + } } - a.set_repair(random_bool(), m_tmp2); + a.set_repair(random_bool(), m_tmp); return true; } @@ -1090,15 +1132,28 @@ namespace bv { unsigned sh = b.to_nat(b.bits, b.bw); if (sh == 0) return a.try_set(e.bits); - else if (sh >= b.bw) - return false; + else if (sh >= b.bw) { + if (e.get(e.bits, e.bw - 1)) { + if (!a.get(a.bits, a.bw - 1) && !a.get(a.fixed, a.bw - 1)) + a.set(a.bits, a.bw - 1, true); + else + return false; + } + else { + if (a.get(a.bits, a.bw - 1) && !a.get(a.fixed, a.bw - 1)) + a.set(a.bits, a.bw - 1, false); + else + return false; + } + return true; + } else { // e = a >> sh // a[bw-1:sh] = e[bw-sh-1:0] // a[sh-1:0] = a[sh-1:0] // ignore sign - for (unsigned i = 0; i < a.bw - sh; ++i) - a.set(m_tmp, i + sh, e.get(e.bits, i)); + for (unsigned i = sh; i < a.bw; ++i) + a.set(m_tmp, i, e.get(e.bits, i - sh)); for (unsigned i = 0; i < sh; ++i) a.set(m_tmp, i, a.get(a.bits, i)); return a.try_set(m_tmp); @@ -1142,15 +1197,17 @@ namespace bv { a.set_repair(false, m_tmp); return true; } - // y * e + r = a + // b * e + r = a for (unsigned i = 0; i < a.nw; ++i) - m_tmp[i] = random_bits(); + m_tmp[i] = (random_bits() & ~b.fixed[i]) | (b.fixed[i] & b.bits[i]); + b.clear_overflow_bits(m_tmp); while (mul_overflow_on_fixed(e, m_tmp)) { auto i = b.msb(m_tmp); b.set(m_tmp, i, false); } for (unsigned i = 0; i < a.nw; ++i) m_tmp2[i] = random_bits(); + b.clear_overflow_bits(m_tmp2); while (b.gt(m_tmp2, b.bits)) b.set(m_tmp2, b.msb(m_tmp2), false); while (a.set_add(m_tmp3, m_tmp, m_tmp2)) @@ -1169,11 +1226,11 @@ namespace bv { for (unsigned i = 0; i < a.nw; ++i) m_tmp[i] = random_bits(); a.clear_overflow_bits(m_tmp); - // ensure r <= a + // ensure r <= m while (a.lt(a.bits, m_tmp)) a.set(m_tmp, a.msb(m_tmp), false); a.set_sub(m_tmp2, a.bits, m_tmp); - mpn.div(m_tmp2.data(), a.nw, e.bits.data(), a.nw, m_tmp3.data(), m_tmp4.data()); + set_div(m_tmp2, e.bits, a.bw, m_tmp3, m_tmp4); b.set_repair(random_bool(), m_tmp4); } return true; @@ -1205,13 +1262,13 @@ namespace bv { for (unsigned i = 0; i < a.nw; ++i) m_tmp[i] = random_bits(); + a.clear_overflow_bits(m_tmp); while (mul_overflow_on_fixed(b, m_tmp)) { auto i = b.msb(m_tmp); b.set(m_tmp, i, false); } while (true) { a.set_mul(m_tmp2, m_tmp, b.bits); - a.clear_overflow_bits(m_tmp2); if (!add_overflow_on_fixed(e, m_tmp2)) break; auto i = b.msb(m_tmp); @@ -1232,7 +1289,7 @@ namespace bv { for (unsigned i = 0; i < a.nw; ++i) m_tmp[i] = random_bits(); a.set_sub(m_tmp2, a.bits, e.bits); - mpn.div(m_tmp2.data(), a.nw, m_tmp.data(), a.nw, m_tmp3.data(), m_tmp4.data()); + set_div(m_tmp2, m_tmp, a.bw, m_tmp3, m_tmp4); a.clear_overflow_bits(m_tmp3); b.set_repair(random_bool(), m_tmp3); return true; @@ -1280,6 +1337,94 @@ namespace bv { } } + bool sls_eval::try_repair_rotate_right(bvval const& e, bvval& a, bvval& b, unsigned i) { + if (i == 0) { + rational n; + b.get_value(b.bits, n); + n = mod(b.bw - n, rational(b.bw)); + return try_repair_rotate_left(e, a, n.get_unsigned()); + } + else { + SASSERT(i == 1); + unsigned sh = m_rand(b.bw); + b.set(m_tmp, sh); + b.set_repair(random_bool(), m_tmp); + return true; + } + } + + bool sls_eval::try_repair_umul_ovfl(bool e, bvval& a, bvval& b, unsigned i) { + if (e) { + // maximize + if (i == 0) { + a.max_feasible(m_tmp); + a.set_repair(false, m_tmp); + } + else { + b.max_feasible(m_tmp); + b.set_repair(false, m_tmp); + } + } + else { + // minimize + if (i == 0) { + a.min_feasible(m_tmp); + a.set_repair(true, m_tmp); + } + else { + b.min_feasible(m_tmp); + b.set_repair(true, m_tmp); + } + } + return true; + } + + bool sls_eval::try_repair_zero_ext(bvval const& e, bvval& a) { + for (unsigned i = 0; i < e.bw; ++i) + if (!a.get(a.fixed, i)) + a.set(a.bits, i, e.get(e.bits, i)); + return true; + } + + bool sls_eval::try_repair_concat(bvval const& e, bvval& a, bvval& b, unsigned i) { + if (i == 0) { + for (unsigned i = 0; i < a.bw; ++i) + if (!a.get(a.fixed, i)) + a.set(a.bits, i, e.get(e.bits, i + b.bw)); + } + else { + for (unsigned i = 0; i < b.bw; ++i) + if (!b.get(b.fixed, i)) + b.set(b.bits, i, e.get(e.bits, i)); + } + return true; + } + + bool sls_eval::try_repair_extract(bvval const& e, bvval& a, unsigned lo) { + for (unsigned i = 0; i < a.bw; ++i) + if (!a.get(a.fixed, i)) + a.set(a.bits, i, e.get(e.bits, i + lo)); + return true; + } + + void sls_eval::set_div(svector const& a, svector const& b, unsigned bw, + svector& quot, svector& rem) const { + unsigned nw = (bw + 8 * sizeof(digit_t) - 1) / (8 * sizeof(digit_t)); + unsigned bnw = nw; + while (bnw > 1 && b[bnw - 1] == 0) + --bnw; + if (b[bnw-1] == 0) { + for (unsigned i = 0; i < nw; ++i) { + quot[i] = ~0; + rem[i] = 0; + } + quot[nw - 1] = (1 << (bw % (8 * sizeof(digit_t)))) - 1; + } + else { + mpn.div(a.data(), nw, b.data(), bnw, quot.data(), rem.data()); + } + } + void sls_eval::repair_up(expr* e) { if (!is_app(e)) return; diff --git a/src/ast/sls/bv_sls_eval.h b/src/ast/sls/bv_sls_eval.h index 70a08283fdf..6c7a2053d5d 100644 --- a/src/ast/sls/bv_sls_eval.h +++ b/src/ast/sls/bv_sls_eval.h @@ -71,6 +71,7 @@ namespace bv { bool try_repair_band(bvval const& e, bvval& a, bvval const& b); bool try_repair_bor(bvval const& e, bvval& a, bvval const& b); bool try_repair_add(bvval const& e, bvval& a, bvval const& b); + bool try_repair_sub(bvval const& e, bvval& a, bvval& b, unsigned i); bool try_repair_mul(bvval const& e, bvval& a, bvval const& b); bool try_repair_bxor(bvval const& e, bvval& a, bvval const& b); bool try_repair_bnot(bvval const& e, bvval& a); @@ -87,12 +88,19 @@ namespace bv { bool try_repair_urem(bvval const& e, bvval& a, bvval& b, unsigned i); bool try_repair_rotate_left(bvval const& e, bvval& a, unsigned n) const; bool try_repair_rotate_left(bvval const& e, bvval& a, bvval& b, unsigned i); + bool try_repair_rotate_right(bvval const& e, bvval& a, bvval& b, unsigned i); bool try_repair_ule(bool e, bvval& a, svector const& t); bool try_repair_uge(bool e, bvval& a, svector const& t); + bool try_repair_umul_ovfl(bool e, bvval& a, bvval& b, unsigned i); + bool try_repair_zero_ext(bvval const& e, bvval& a); + bool try_repair_concat(bvval const& e, bvval& a, bvval& b, unsigned i); + bool try_repair_extract(bvval const& e, bvval& a, unsigned lo); void add_p2_1(bvval const& a, svector& t) const; bool add_overflow_on_fixed(bvval const& a, svector const& t); bool mul_overflow_on_fixed(bvval const& a, svector const& t); + void set_div(svector const& a, svector const& b, unsigned nw, + svector& quot, svector& rem) const; digit_t random_bits(); bool random_bool() { return m_rand() % 2 == 0; } diff --git a/src/ast/sls/bv_sls_fixed.cpp b/src/ast/sls/bv_sls_fixed.cpp index 490557a56a7..0d51906bff2 100644 --- a/src/ast/sls/bv_sls_fixed.cpp +++ b/src/ast/sls/bv_sls_fixed.cpp @@ -154,6 +154,7 @@ namespace bv { else v.add_range(-b, -a); } + } void sls_fixed::get_offset(expr* e, expr*& x, rational& offset) { diff --git a/src/ast/sls/bv_sls_terms.cpp b/src/ast/sls/bv_sls_terms.cpp index 0a110a7d813..df84075c932 100644 --- a/src/ast/sls/bv_sls_terms.cpp +++ b/src/ast/sls/bv_sls_terms.cpp @@ -119,8 +119,8 @@ namespace bv { expr* sls_terms::mk_sdiv(expr* x, expr* y) { // d = udiv(abs(x), abs(y)) - // y = 0, x > 0 -> 1 - // y = 0, x <= 0 -> -1 + // y = 0, x >= 0 -> -1 + // y = 0, x < 0 -> 1 // x = 0, y != 0 -> 0 // x > 0, y < 0 -> -d // x < 0, y > 0 -> -d @@ -136,7 +136,7 @@ namespace bv { expr* d = bv.mk_bv_udiv(absx, absy); expr* r = m.mk_ite(m.mk_eq(signx, signy), d, bv.mk_bv_neg(d)); r = m.mk_ite(m.mk_eq(z, y), - m.mk_ite(signx, bv.mk_numeral(N - 1, sz), bv.mk_one(sz)), + m.mk_ite(signx, bv.mk_one(sz), bv.mk_numeral(N - 1, sz)), m.mk_ite(m.mk_eq(x, z), z, r)); return r; } diff --git a/src/ast/sls/sls_valuation.cpp b/src/ast/sls/sls_valuation.cpp index 75307c6677b..3bafca7daa0 100644 --- a/src/ast/sls/sls_valuation.cpp +++ b/src/ast/sls/sls_valuation.cpp @@ -177,7 +177,7 @@ namespace bv { bool sls_valuation::round_down(svector& dst) const { if (lt(lo, hi)) { - if (lt(lo, hi)) + if (lt(dst, lo)) return false; if (le(hi, dst)) { set(dst, hi); @@ -324,79 +324,90 @@ namespace bv { } SASSERT(!has_overflow(lo)); SASSERT(!has_overflow(hi)); + init_fixed(); } + // + // tighten lo/hi based on fixed bits. + // lo[bit_i] != fixedbit[bit_i] + // let bit_i be most significant bit position of disagreement. + // if fixedbit = 1, lo = 0, increment lo + // if fixedbit = 0, lo = 1, lo := fixed & bits + // (hi-1)[bit_i] != fixedbit[bit_i] + // if fixedbit = 0, hi-1 = 1, set hi-1 := 0, maximize below bit_i + // if fixedbit = 1, hi-1 = 0, hi := fixed & bits + // tighten fixed bits based on lo/hi + // lo + 1 = hi -> set bits = lo + // lo < hi, set most significant bits based on hi + // void sls_valuation::init_fixed() { if (eq(lo, hi)) return; - bool lo_ok = true; - for (unsigned i = 0; i < nw; ++i) - lo_ok &= (0 == (fixed[i] & (bits[i] ^ lo[i]))); - if (!lo_ok) { - svector tmp(nw + 1); - if (get_at_least(lo, tmp)) { - if (lt(lo, hi) && lt(tmp, hi)) - set(lo, tmp); - else if (gt(lo, hi)) - set(lo, tmp); + for (unsigned i = bw; i-- > 0; ) { + if (!get(fixed, i)) + continue; + if (get(bits, i) == get(lo, i)) + continue; + if (get(bits, i)) { + set(lo, i, true); + for (unsigned j = i; j-- > 0; ) + set(lo, j, get(fixed, j) && get(bits, j)); } - else if (gt(lo, hi)) { - svector zero(nw + 1, (unsigned) 0); - if (get_at_least(zero, tmp) && lt(tmp, hi)) - set(lo, tmp); + else { + for (unsigned j = bw; j-- > 0; ) + set(lo, j, get(fixed, j) && get(bits, j)); } + break; } - bool hi_ok = true; svector hi1(nw + 1, (unsigned)0); svector one(nw + 1, (unsigned)0); one[0] = 1; digit_t c; mpn_manager().sub(hi.data(), nw, one.data(), nw, hi1.data(), &c); - for (unsigned i = 0; i < nw; ++i) - hi_ok &= (0 == (fixed[i] & (bits[i] ^ hi1[i]))); - if (!hi_ok) { - svector tmp(nw + 1); - if (get_at_most(hi1, tmp)) { - if (lt(tmp, hi) && (le(lo, tmp) || lt(hi, lo))) { - mpn_manager().add(tmp.data(), nw, one.data(), nw, hi1.data(), nw + 1, &c); - clear_overflow_bits(hi1); - set(hi, hi1); - } + clear_overflow_bits(hi1); + for (unsigned i = bw; i-- > 0; ) { + if (!get(fixed, i)) + continue; + if (get(bits, i) == get(hi1, i)) + continue; + if (get(hi1, i)) { + set(hi1, i, false); + for (unsigned j = i; j-- > 0; ) + set(hi1, j, !get(fixed, j) || get(bits, j)); + } + else { + for (unsigned j = bw; j-- > 0; ) + set(hi1, j, get(fixed, j) && get(bits, j)); } - // TODO other cases + mpn_manager().add(hi1.data(), nw, one.data(), nw, hi.data(), nw + 1, &c); + clear_overflow_bits(hi); + break; } + // set fixed bits based on bounds + auto set_fixed_bit = [&](unsigned i, bool b) { + if (!get(fixed, i)) { + set(fixed, i, true); + set(bits, i, b); + } + }; + // set most significant bits if (lt(lo, hi)) { unsigned i = bw; - for (; i-- > 0; ) { - if (get(hi, i)) - break; - if (!get(fixed, i)) { - set(fixed, i, true); - set(bits, i, false); - } - } - bool is_power_of2 = true; - for (unsigned j = 0; is_power_of2 && j < i; ++j) - is_power_of2 = !get(hi, j); - if (is_power_of2) { - if (!get(fixed, i)) { - set(fixed, i, true); - set(bits, i, false); - } - } + for (; i-- > 0 && !get(hi, i); ) + set_fixed_bit(i, false); + + if (is_power_of2(hi)) + set_fixed_bit(i, false); } - svector tmp(nw + 1, (unsigned)0); - mpn_manager().add(lo.data(), nw, one.data(), nw, tmp.data(), nw + 1, &c); - clear_overflow_bits(tmp); - if (eq(tmp, hi)) { - for (unsigned i = 0; i < bw; ++i) { - if (!get(fixed, i)) { - set(fixed, i, true); - set(bits, i, get(lo, i)); - } - } + + // lo + 1 = hi: then bits = lo + mpn_manager().add(lo.data(), nw, one.data(), nw, hi1.data(), nw + 1, &c); + clear_overflow_bits(hi1); + if (eq(hi1, hi)) { + for (unsigned i = 0; i < bw; ++i) + set_fixed_bit(i, get(lo, i)); } SASSERT(!has_overflow(bits)); } @@ -424,4 +435,11 @@ namespace bv { return ovfl; } + bool sls_valuation::is_power_of2(svector const& src) const { + unsigned c = 0; + for (unsigned i = 0; i < nw; ++i) + c += get_num_1bits(src[i]); + return c == 1; + } + } diff --git a/src/ast/sls/sls_valuation.h b/src/ast/sls/sls_valuation.h index 6a5b241b34b..ca68cf5a7ed 100644 --- a/src/ast/sls/sls_valuation.h +++ b/src/ast/sls/sls_valuation.h @@ -108,6 +108,8 @@ namespace bv { // most significant bit or bw if src = 0 unsigned msb(svector const& src) const; + bool is_power_of2(svector const& src) const; + // retrieve largest number at or below (above) src which is feasible // with respect to fixed, lo, hi. bool get_at_most(svector const& src, svector& dst) const; @@ -195,6 +197,16 @@ namespace bv { out << " "; for (unsigned i = 0; i < nw; ++i) out << fixed[i]; + + if (!eq(lo, hi)) { + out << " ["; + for (unsigned i = 0; i < nw; ++i) + out << lo[i]; + out << ", "; + for (unsigned i = 0; i < nw; ++i) + out << hi[i]; + out << "["; + } out << std::dec; return out; } diff --git a/src/test/sls_test.cpp b/src/test/sls_test.cpp index 3b0fd580a77..00ac0547c2e 100644 --- a/src/test/sls_test.cpp +++ b/src/test/sls_test.cpp @@ -30,6 +30,7 @@ namespace bv { es.push_back(e); sls_eval ev(m); ev.init_eval(es, value); + ev.init_fixed(es); th_rewriter rw(m); expr_ref r(e, m); rw(r); @@ -114,6 +115,14 @@ namespace bv { auto e1 = es1.get(i); auto e2 = es2.get(i); auto e3 = es3.get(i); + if (bv.is_bv_sdiv(e1)) + continue; + if (bv.is_bv_srem(e1)) + continue; + if (bv.is_bv_smod(e1)) + continue; + if (is_app_of(e1, bv.get_fid(), OP_BUADD_OVFL)) + continue; check_repair_idx(e1, e2, 0, x); if (is_app(e1) && to_app(e1)->get_num_args() == 2) check_repair_idx(e1, e3, 1, y); @@ -128,22 +137,30 @@ namespace bv { }; expr_ref_vector es(m); bv_util bv(m); - es.push_back(e1); - es.push_back(e2); - sls_eval ev(m); - ev.init_eval(es, value); th_rewriter rw(m); expr_ref r(e1, m); + rw(r); + es.push_back(m.is_false(r) ? m.mk_not(e1) : e1); + es.push_back(m.is_false(r) ? m.mk_not(e2) : e2); + sls_eval ev(m); + ev.init_eval(es, value); + ev.init_fixed(es); + if (m.is_bool(e1)) { + SASSERT(m.is_true(r) || m.is_false(r)); auto val = m.is_true(r); auto val2 = ev.bval0(e2); if (val != val2) { ev.set(e2, val); auto rep1 = ev.try_repair(to_app(e2), idx); if (!rep1) { - verbose_stream() << "Not repaired " << mk_pp(e2, m) << "\n"; + verbose_stream() << "Not repaired " << mk_pp(e2, m) << " r: " << r << "\n"; } - SASSERT(rep1); + auto val3 = ev.bval0(e2); + if (val3 != val) { + verbose_stream() << "Repaired but not corrected " << mk_pp(e2, m) << "\n"; + } + //SASSERT(rep1); } } if (bv.is_bv(e1)) { @@ -155,7 +172,11 @@ namespace bv { if (!rep2) { verbose_stream() << "Not repaired " << mk_pp(e2, m) << "\n"; } - SASSERT(rep2); + auto val3 = ev.wval0(e2); + if (!val3.eq(val1)) { + verbose_stream() << "Repaired but not corrected " << mk_pp(e2, m) << "\n"; + } + //SASSERT(rep2); } } } @@ -213,5 +234,6 @@ static void test_repair1() { } void tst_sls_test() { + test_repair1(); test_eval1(); }