From 5455603910da128969dda0fd533806da758db1e4 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Wed, 28 Feb 2024 08:57:54 -0800 Subject: [PATCH] na Signed-off-by: Nikolaj Bjorner --- src/ast/sls/bv_sls.cpp | 19 +++++++++++++++++-- src/ast/sls/bv_sls.h | 1 + src/ast/sls/bv_sls_eval.cpp | 6 +++--- src/ast/sls/sls_valuation.cpp | 12 ++++-------- src/ast/sls/sls_valuation.h | 13 +++++++++++-- 5 files changed, 36 insertions(+), 15 deletions(-) diff --git a/src/ast/sls/bv_sls.cpp b/src/ast/sls/bv_sls.cpp index b930eeaae..50ec5da6b 100644 --- a/src/ast/sls/bv_sls.cpp +++ b/src/ast/sls/bv_sls.cpp @@ -138,6 +138,8 @@ namespace bv { void sls::try_repair_down(app* e) { if (eval_is_correct(e)) { +// if (bv.is_bv(e)) +// verbose_stream() << mk_pp(e, m) << " := " << m_eval.wval(e) << "\n"; m_repair_roots.remove(m_repair_root); m_repair_root = UINT_MAX; return; @@ -147,7 +149,6 @@ namespace bv { if (n == 0) { auto& v = m_eval.wval(e); v.commit_eval(); - verbose_stream() << mk_pp(e, m) << " := " << v << "\n"; for (auto p : m_terms.parents(e)) m_repair_up.insert(p->get_id()); m_repair_roots.remove(m_repair_root); @@ -193,11 +194,25 @@ namespace bv { return false; } + + bool sls::re_eval_is_correct(app* e) { + if (!m_eval.can_eval1(e)) + return false; + if (m.is_bool(e)) + return m_eval.bval0(e) == m_eval.bval1(e); + if (bv.is_bv(e)) { + auto const& v = m_eval.eval(e); + return v.eval == v.bits(); + } + UNREACHABLE(); + return false; + } + model_ref sls::get_model() { model_ref mdl = alloc(model, m); auto& terms = m_eval.sort_assertions(m_terms.assertions()); for (expr* e : terms) { - if (!eval_is_correct(to_app(e))) { + if (!re_eval_is_correct(to_app(e))) { verbose_stream() << "missed evaluation #" << e->get_id() << " " << mk_bounded_pp(e, m) << "\n"; if (bv.is_bv(e)) { auto const& v = m_eval.wval(e); diff --git a/src/ast/sls/bv_sls.h b/src/ast/sls/bv_sls.h index 9e4e6e741..177ac5069 100644 --- a/src/ast/sls/bv_sls.h +++ b/src/ast/sls/bv_sls.h @@ -54,6 +54,7 @@ namespace bv { std::pair next_to_repair(); bool eval_is_correct(app* e); + bool re_eval_is_correct(app* e); void try_repair_down(app* e); void try_repair_up(app* e); void set_repair_down(expr* e) { m_repair_down = e->get_id(); } diff --git a/src/ast/sls/bv_sls_eval.cpp b/src/ast/sls/bv_sls_eval.cpp index 83ccb99f0..d466466f2 100644 --- a/src/ast/sls/bv_sls_eval.cpp +++ b/src/ast/sls/bv_sls_eval.cpp @@ -299,7 +299,6 @@ namespace bv { sls_valuation& sls_eval::eval(app* e) const { auto& val = *m_values[e->get_id()]; eval(e, val); - verbose_stream() << "eval " << mk_pp(e, m) << " := " << val << " " << val.eval << "\n"; return val; } @@ -1021,7 +1020,6 @@ namespace bv { unsigned parity_e = b.parity(e); unsigned parity_b = b.parity(b.bits()); - verbose_stream() << e << " := " << a << " * " << b << "\n"; if (b.is_zero(e)) { a.get_variant(m_tmp, m_rand); for (unsigned i = 0; i < b.bw - parity_b; ++i) @@ -1092,6 +1090,8 @@ namespace bv { y.set_bw(0); // x*a + y*b = 1 + tb.set_bw(b.bw); + tb.set_bw(0); #if Z3DEBUG b.get(y); if (parity_b > 0) @@ -1099,7 +1099,7 @@ namespace bv { a.set_mul(m_tmp, tb, y); SASSERT(a.is_one(m_tmp)); #endif - b.get(m_tmp2); + e.copy_to(b.nw, m_tmp2); if (parity_e > 0 && parity_b > 0) b.shift_right(m_tmp2, std::min(parity_b, parity_e)); a.set_mul(m_tmp, tb, m_tmp2); diff --git a/src/ast/sls/sls_valuation.cpp b/src/ast/sls/sls_valuation.cpp index aad26a367..a410a0157 100644 --- a/src/ast/sls/sls_valuation.cpp +++ b/src/ast/sls/sls_valuation.cpp @@ -338,10 +338,8 @@ namespace bv { } void sls_valuation::min_feasible(bvect& out) const { - if (m_lo < m_hi) { - for (unsigned i = 0; i < nw; ++i) - out[i] = m_lo[i]; - } + if (m_lo < m_hi) + m_lo.copy_to(nw, out); else { for (unsigned i = 0; i < nw; ++i) out[i] = fixed[i] & m_bits[i]; @@ -351,8 +349,7 @@ namespace bv { void sls_valuation::max_feasible(bvect& out) const { if (m_lo < m_hi) { - for (unsigned i = 0; i < nw; ++i) - out[i] = m_hi[i]; + m_hi.copy_to(nw, out); sub1(out); } else { @@ -386,8 +383,7 @@ namespace bv { } void sls_valuation::get(bvect& dst) const { - for (unsigned i = 0; i < nw; ++i) - dst[i] = m_bits[i]; + m_bits.copy_to(nw, dst); } digit_t sls_valuation::random_bits(random_gen& rand) { diff --git a/src/ast/sls/sls_valuation.h b/src/ast/sls/sls_valuation.h index 39b70ce07..88d8509d7 100644 --- a/src/ast/sls/sls_valuation.h +++ b/src/ast/sls/sls_valuation.h @@ -37,6 +37,12 @@ namespace bv { bvect(unsigned sz) : svector(sz, (unsigned)0) {} void set_bw(unsigned bw); + void copy_to(unsigned nw, bvect & dst) const { + SASSERT(nw <= this->size()); + for (unsigned i = 0; i < nw; ++i) + dst[i] = (*this)[i]; + } + void set(unsigned bit_idx, bool val) { auto _val = static_cast(0 - static_cast(val)); get_bit_word(bit_idx) ^= (_val ^ get_bit_word(bit_idx)) & get_pos_mask(bit_idx); @@ -282,8 +288,11 @@ namespace bv { std::ostream& display(std::ostream& out) const { out << m_bits; - out << " fix:"; - out << fixed; + out << " ev: " << eval; + if (!is_zero(fixed)) { + out << " fix:"; + out << fixed; + } if (m_lo != m_hi) out << " [" << m_lo << ", " << m_hi << "["; return out;