From 5be8872d6a90e6a4133fab4f25f5d880eff8ee11 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Thu, 29 Feb 2024 08:54:21 -0800 Subject: [PATCH] na Signed-off-by: Nikolaj Bjorner --- src/ast/sls/bv_sls.cpp | 11 +++-- src/ast/sls/bv_sls_eval.cpp | 80 +++++++++++++++++++++--------- src/ast/sls/bv_sls_eval.h | 6 ++- src/ast/sls/bv_sls_fixed.cpp | 6 +-- src/ast/sls/sls_valuation.cpp | 92 ++++++++++++++++------------------- src/ast/sls/sls_valuation.h | 7 ++- 6 files changed, 117 insertions(+), 85 deletions(-) diff --git a/src/ast/sls/bv_sls.cpp b/src/ast/sls/bv_sls.cpp index 3902957fc..5c7c16fb1 100644 --- a/src/ast/sls/bv_sls.cpp +++ b/src/ast/sls/bv_sls.cpp @@ -38,8 +38,10 @@ namespace bv { void sls::init_eval(std::function& eval) { m_eval.init_eval(m_terms.assertions(), eval); - m_eval.init_fixed(m_terms.assertions()); + m_eval.tighten_range(m_terms.assertions()); init_repair(); + display(verbose_stream()); + exit(0); } void sls::init_repair() { @@ -160,8 +162,11 @@ namespace bv { unsigned n = e->get_num_args(); if (n == 0) { - auto& v = m_eval.wval(e); - VERIFY(v.commit_eval()); + if (m.is_bool(e)) + m_eval.set(e, m_eval.bval1(e)); + else + VERIFY(m_eval.wval(e).commit_eval()); + for (auto p : m_terms.parents(e)) m_repair_up.insert(p->get_id()); return; diff --git a/src/ast/sls/bv_sls_eval.cpp b/src/ast/sls/bv_sls_eval.cpp index 931364e30..36f0ebcb3 100644 --- a/src/ast/sls/bv_sls_eval.cpp +++ b/src/ast/sls/bv_sls_eval.cpp @@ -643,11 +643,21 @@ namespace bv { mk_rotate_left(val.bw - n.get_unsigned()); break; } + case OP_BCOMP: { + auto const& a = wval(e->get_arg(0)); + auto const& b = wval(e->get_arg(1)); + if (a.bits() == b.bits()) + val.set(val.eval, 1); + else + val.set(val.eval, 0); + break; + } case OP_BREDAND: case OP_BREDOR: case OP_BXNOR: case OP_INT2BV: - case OP_BCOMP: + + verbose_stream() << mk_bounded_pp(e, m) << "\n"; NOT_IMPLEMENTED_YET(); break; case OP_BIT2BOOL: @@ -829,8 +839,10 @@ namespace bv { return try_repair_umul_ovfl(!bval0(e), wval(e, 0), wval(e, 1), i); case OP_BUMUL_OVFL: return try_repair_umul_ovfl(bval0(e), wval(e, 0), wval(e, 1), i); + case OP_BCOMP: + return try_repair_comp(eval_value(e), wval(e, 0), wval(e, 1), i); case OP_BUADD_OVFL: - case OP_BCOMP: + case OP_BNAND: case OP_BREDAND: case OP_BREDOR: @@ -887,29 +899,33 @@ namespace bv { else if (bv.is_bv(child)) { auto & a = wval(e->get_arg(i)); auto & b = wval(e->get_arg(1 - i)); - if (is_true) - return a.try_set(b.bits()); - else { - bool try_above = m_rand() % 2 == 0; - if (try_above) { - a.set_add(m_tmp, b.bits(), m_one); - if (!a.is_zero(m_tmp) && a.set_random_at_least(m_tmp, m_tmp2, m_rand)) - return true; - } - a.set_sub(m_tmp, b.bits(), m_one); - if (!a.is_zero(m_tmp) && a.set_random_at_most(m_tmp, m_tmp2, m_rand)) - return true; - if (!try_above) { - a.set_add(m_tmp, b.bits(), m_one); - if (!a.is_zero(m_tmp) && a.set_random_at_least(m_tmp, m_tmp2, m_rand)) - return true; - } - return false; - } + return try_repair_eq(is_true, a, b); } return false; } + bool sls_eval::try_repair_eq(bool is_true, bvval& a, bvval const& b) { + if (is_true) + return a.try_set(b.bits()); + else { + bool try_above = m_rand() % 2 == 0; + if (try_above) { + a.set_add(m_tmp, b.bits(), m_one); + if (!a.is_zero(m_tmp) && a.set_random_at_least(m_tmp, m_tmp2, m_rand)) + return true; + } + a.set_sub(m_tmp, b.bits(), m_one); + if (!a.is_zero(m_tmp) && a.set_random_at_most(m_tmp, m_tmp2, m_rand)) + return true; + if (!try_above) { + a.set_add(m_tmp, b.bits(), m_one); + if (!a.is_zero(m_tmp) && a.set_random_at_least(m_tmp, m_tmp2, m_rand)) + return true; + } + return false; + } + } + bool sls_eval::try_repair_xor(app* e, unsigned i) { bool ev = bval0(e); bool bv = bval0(e->get_arg(1 - i)); @@ -1285,6 +1301,7 @@ namespace bv { m_tmp.set(i, e.get(sh + i)); for (unsigned i = a.bw - sh; i < a.bw; ++i) m_tmp.set(i, a.get_bit(i)); + a.clear_overflow_bits(m_tmp); return a.try_set(m_tmp); } } @@ -1335,6 +1352,12 @@ namespace bv { return try_repair_ashr(e, a, b, i); } + bool sls_eval::try_repair_comp(bvect const& e, bvval& a, bvval& b, unsigned i) { + SASSERT(e[0] == 0 || e[0] == 1); + SASSERT(e.bw == 1); + return try_repair_eq(e[0] == 1, i == 0 ? a : b, i == 0 ? b : a); + } + // e = a udiv b // e = 0 => a != ones // b = 0 => e = -1 // nothing to repair on a @@ -1368,7 +1391,8 @@ namespace bv { while (b.bits() < m_tmp2) m_tmp2.set(b.msb(m_tmp2), false); while (a.set_add(m_tmp3, m_tmp, m_tmp2)) - m_tmp2.set(b.msb(m_tmp2), false); + m_tmp2.set(b.msb(m_tmp2), false); + a.clear_overflow_bits(m_tmp3); return a.set_repair(true, m_tmp3); } else { @@ -1561,18 +1585,21 @@ namespace bv { } bool sls_eval::try_repair_concat(bvect const& e, bvval& a, bvval& b, unsigned idx) { + bool r = false; if (idx == 0) { for (unsigned i = 0; i < a.bw; ++i) m_tmp.set(i, e.get(i + b.bw)); a.clear_overflow_bits(m_tmp); - return a.try_set(m_tmp); + r = a.try_set(m_tmp); } else { for (unsigned i = 0; i < b.bw; ++i) m_tmp.set(i, e.get(i)); b.clear_overflow_bits(m_tmp); - return b.try_set(m_tmp); + r = b.try_set(m_tmp); } + verbose_stream() << e << " := " << a << " " << b << "\n"; + return r; } // @@ -1644,6 +1671,11 @@ namespace bv { return false; } + sls_valuation& sls_eval::wval(expr* e) const { + if (!m_values[e->get_id()]) verbose_stream() << mk_bounded_pp(e, m) << "\n"; + return *m_values[e->get_id()]; + } + std::ostream& sls_eval::display(std::ostream& out, expr_ref_vector const& es) { auto& terms = sort_assertions(es); for (expr* e : terms) { diff --git a/src/ast/sls/bv_sls_eval.h b/src/ast/sls/bv_sls_eval.h index 310892f2b..42e67609d 100644 --- a/src/ast/sls/bv_sls_eval.h +++ b/src/ast/sls/bv_sls_eval.h @@ -106,6 +106,8 @@ namespace bv { bool try_repair_sign_ext(bvect const& e, bvval& a); bool try_repair_concat(bvect const& e, bvval& a, bvval& b, unsigned i); bool try_repair_extract(bvect const& e, bvval& a, unsigned lo); + 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); void add_p2_1(bvval const& a, bvect& t) const; bool add_overflow_on_fixed(bvval const& a, bvect const& t); @@ -127,7 +129,7 @@ namespace bv { void init_eval(expr_ref_vector const& es, std::function const& eval); - void init_fixed(expr_ref_vector const& es) { m_fix.init(es); } + void tighten_range(expr_ref_vector const& es) { m_fix.init(es); } ptr_vector& sort_assertions(expr_ref_vector const& es); @@ -139,7 +141,7 @@ namespace bv { bool bval0(expr* e) const { return m_eval[e->get_id()]; } - sls_valuation& wval(expr* e) const { return *m_values[e->get_id()]; } + sls_valuation& wval(expr* e) const; bool is_fixed0(expr* e) const { return m_fixed[e->get_id()]; } diff --git a/src/ast/sls/bv_sls_fixed.cpp b/src/ast/sls/bv_sls_fixed.cpp index 609842790..e2bd87922 100644 --- a/src/ast/sls/bv_sls_fixed.cpp +++ b/src/ast/sls/bv_sls_fixed.cpp @@ -112,7 +112,7 @@ namespace bv { auto& val = wval(s); val.try_set_bit(idx, !sign); val.fixed.set(idx, true); - val.init_fixed(); + val.tighten_range(); } } @@ -185,7 +185,7 @@ namespace bv { auto& val_el = wval(e->get_arg(2)); for (unsigned i = 0; i < val.nw; ++i) val.fixed[i] = val_el.fixed[i] & val_th.fixed[i] & ~(val_el.bits(i) ^ val_th.bits(i)); - val.init_fixed(); + val.tighten_range(); } } @@ -420,6 +420,6 @@ namespace bv { UNREACHABLE(); break; } - v.init_fixed(); + v.tighten_range(); } } diff --git a/src/ast/sls/sls_valuation.cpp b/src/ast/sls/sls_valuation.cpp index d4bf33353..225bf9e1e 100644 --- a/src/ast/sls/sls_valuation.cpp +++ b/src/ast/sls/sls_valuation.cpp @@ -446,8 +446,8 @@ namespace bv { if (h == l) return; - //verbose_stream() << "[" << l << ", " << h << "[\n"; - //verbose_stream() << *this << "\n"; + verbose_stream() << "[" << l << ", " << h << "[\n"; + verbose_stream() << *this << "\n"; SASSERT(is_zero(fixed)); // ranges can only be added before fixed bits are set. @@ -481,9 +481,10 @@ namespace bv { SASSERT(!has_overflow(m_lo)); SASSERT(!has_overflow(m_hi)); - if (!in_range(m_bits)) + if (!in_range(m_bits)) set(m_bits, m_lo); SASSERT(well_formed()); + verbose_stream() << *this << "\n"; } // @@ -499,7 +500,9 @@ namespace bv { // lo + 1 = hi -> set bits = lo // lo < hi, set most significant bits based on hi // - void sls_valuation::init_fixed() { + void sls_valuation::tighten_range() { + + verbose_stream() << "tighten " << *this << "\n"; if (m_lo == m_hi) return; for (unsigned i = bw; i-- > 0; ) { @@ -518,56 +521,47 @@ namespace bv { } break; } - bvect hi1(nw + 1); - bvect one(nw + 1); - one[0] = 1; - digit_t c; - mpn_manager().sub(m_hi.data(), nw, one.data(), nw, hi1.data(), &c); - clear_overflow_bits(hi1); - for (unsigned i = bw; i-- > 0; ) { - if (!fixed.get(i)) - continue; - if (m_bits.get(i) == hi1.get(i)) - continue; - if (hi1.get(i)) { - hi1.set(i, false); - for (unsigned j = i; j-- > 0; ) - hi1.set(j, !fixed.get(j) || m_bits.get(j)); + + if (!in_range(m_bits)) { + verbose_stream() << "not in range\n"; + bool compatible = true; + for (unsigned i = 0; i < nw && compatible; ++i) + compatible = 0 == (fixed[i] && (m_bits[i] ^ m_lo[i])); + verbose_stream() << (fixed[0] && (m_bits[0] ^ m_lo[0])) << "\n"; + + if (compatible) { + verbose_stream() << "compatible\n"; + set(m_bits, m_lo); } else { - for (unsigned j = bw; j-- > 0; ) - hi1.set(j, fixed.get(j) && m_bits.get(j)); + bvect tmp(m_bits.nw); + tmp.set_bw(bw); + set(tmp, m_lo); + unsigned max_diff = bw; + for (unsigned i = 0; i < bw; ++i) { + if (fixed.get(i) && (m_bits.get(i) ^ m_lo.get(i))) { + tmp.set(i, m_bits.get(i)); + max_diff = i; + } + } + SASSERT(max_diff != bw); + + for (unsigned i = 0; i <= max_diff; ++i) + tmp.set(i, fixed.get(i) && m_bits.get(i)); + + bool found0 = false; + for (unsigned i = max_diff + 1; i < bw; ++i) { + if (found0 || m_lo.get(i) || fixed.get(i)) + tmp.set(i, m_lo.get(i) && fixed.get(i)); + else { + tmp.set(i, true); + found0 = true; + } + } + set(m_bits, tmp); } - mpn_manager().add(hi1.data(), nw, one.data(), nw, m_hi.data(), nw + 1, &c); - clear_overflow_bits(m_hi); - break; } - // set fixed bits based on bounds - auto set_fixed_bit = [&](unsigned i, bool b) { - if (!fixed.get(i)) { - fixed.set(i, true); - eval.set(i, b); - } - }; - - // set most significant bits - if (m_lo < m_hi) { - unsigned i = bw; - for (; i-- > 0 && !m_hi.get(i); ) - set_fixed_bit(i, false); - - if (is_power_of2(m_hi)) - set_fixed_bit(i, false); - } - - // lo + 1 = hi: then bits = lo - mpn_manager().add(m_lo.data(), nw, one.data(), nw, hi1.data(), nw + 1, &c); - clear_overflow_bits(hi1); - if (m_hi == hi1) { - for (unsigned i = 0; i < bw; ++i) - set_fixed_bit(i, m_lo.get(i)); - } SASSERT(well_formed()); } diff --git a/src/ast/sls/sls_valuation.h b/src/ast/sls/sls_valuation.h index 0cd357d4d..cbe1a35a4 100644 --- a/src/ast/sls/sls_valuation.h +++ b/src/ast/sls/sls_valuation.h @@ -140,7 +140,7 @@ namespace bv { void get(bvect& dst) const; void add_range(rational lo, rational hi); bool has_range() const { return m_lo != m_hi; } - void init_fixed(); + void tighten_range(); void clear_overflow_bits(bvect& bits) const { SASSERT(nw > 0); @@ -156,11 +156,10 @@ namespace bv { bool is_zero() const { return is_zero(m_bits); } bool is_zero(bvect const& a) const { - SASSERT(!has_overflow(a)); - for (unsigned i = 0; i < nw; ++i) + for (unsigned i = 0; i < nw - 1; ++i) if (a[i] != 0) return false; - return true; + return (a[nw - 1] & mask) == 0; } bool is_ones() const { return is_ones(m_bits); }