From 0308a92ea6982cfa1d3f4f16e094b4cefd3bb4fe Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Thu, 5 Sep 2024 12:19:42 -0700 Subject: [PATCH] Refactor verbose logging and fix logic in range adjustment functions in sls bv modules --- src/ast/sls/sls_bv_eval.cpp | 32 +++---- src/ast/sls/sls_bv_fixed.cpp | 2 - src/ast/sls/sls_bv_plugin.cpp | 4 +- src/ast/sls/sls_bv_valuation.cpp | 151 +++++++++++++------------------ src/ast/sls/sls_bv_valuation.h | 4 +- 5 files changed, 81 insertions(+), 112 deletions(-) diff --git a/src/ast/sls/sls_bv_eval.cpp b/src/ast/sls/sls_bv_eval.cpp index 2c1796294..9e319ab77 100644 --- a/src/ast/sls/sls_bv_eval.cpp +++ b/src/ast/sls/sls_bv_eval.cpp @@ -885,15 +885,15 @@ namespace sls { auto const& uninterp = terms.uninterp_occurs(e); if (uninterp.empty()) return false; - for (auto e : uninterp) - verbose_stream() << mk_bounded_pp(e, m) << " "; - verbose_stream() << "\n"; +// for (auto e : uninterp) +// verbose_stream() << mk_bounded_pp(e, m) << " "; +// verbose_stream() << "\n"; expr* t = uninterp[m_rand() % uninterp.size()]; auto& v = wval(t); if (v.set_random(m_rand)) { - verbose_stream() << "set random " << mk_bounded_pp(t, m) << "\n"; + //verbose_stream() << "set random " << mk_bounded_pp(t, m) << "\n"; ctx.new_value_eh(t); return true; } @@ -1908,8 +1908,8 @@ namespace sls { // set a outside of [hi:lo] to random values with preference to 0 or 1 bits // bool bv_eval::try_repair_extract(bvect const& e, bvval& a, unsigned lo) { - //verbose_stream() << "repair extract a[" << lo << ":" << lo + e.bw - 1 << "] = " << e << "\n"; - if (m_rand(m_config.m_prob_randomize_extract) <= 100) { + // verbose_stream() << "repair extract a[" << lo << ":" << lo + e.bw - 1 << "] = " << e << "\n"; + if (false && m_rand(m_config.m_prob_randomize_extract) <= 100) { a.get_variant(m_tmp, m_rand); if (0 == (m_rand(2))) { auto bit = 0 == (m_rand(2)); @@ -1927,11 +1927,11 @@ namespace sls { for (unsigned i = 0; i < e.bw; ++i) m_tmp.set(i + lo, e.get(i)); m_tmp.set_bw(a.bw); - //verbose_stream() << a << " := " << m_tmp << "\n"; + // verbose_stream() << a << " := " << m_tmp << "\n"; if (m_rand(5) != 0 && a.try_set(m_tmp)) return true; bool ok = a.set_random(m_rand); - //verbose_stream() << "set random " << ok << " " << a << "\n"; + // verbose_stream() << "set random " << ok << " " << a << "\n"; return ok; } @@ -1982,7 +1982,7 @@ namespace sls { for (unsigned i = 0; i < v.nw; ++i) { if (0 != (v.fixed[i] & (v.bits()[i] ^ v.eval[i]))) { - verbose_stream() << "Fail to set " << mk_bounded_pp(e, m) << " " << i << " " << v.fixed[i] << " " << v.bits()[i] << " " << v.eval[i] << "\n"; + //verbose_stream() << "Fail to set " << mk_bounded_pp(e, m) << " " << i << " " << v.fixed[i] << " " << v.bits()[i] << " " << v.eval[i] << "\n"; v.bits().copy_to(v.nw, v.eval); return false; @@ -1991,9 +1991,9 @@ namespace sls { //verbose_stream() << "repair up " << mk_bounded_pp(e, m) << " " << v << "\n"; if (v.commit_eval()) return true; - verbose_stream() << "could not repair up " << mk_bounded_pp(e, m) << " " << v << "\n"; - for (expr* arg : *to_app(e)) - verbose_stream() << mk_bounded_pp(arg, m) << " " << wval(arg) << "\n"; + //verbose_stream() << "could not repair up " << mk_bounded_pp(e, m) << " " << v << "\n"; + //for (expr* arg : *to_app(e)) + // verbose_stream() << mk_bounded_pp(arg, m) << " " << wval(arg) << "\n"; v.bits().copy_to(v.nw, v.eval); return false; } @@ -2007,12 +2007,6 @@ namespace sls { void bv_eval::commit_eval(expr* p, app* e) { if (!bv.is_bv(e)) return; - - if (e->get_id() == 5) { - //verbose_stream() << e->get_id() << " " << mk_bounded_pp(e, m) << " " << wval(e) << "\n"; - //verbose_stream() << "parent " << mk_bounded_pp(p, m) << " := " << wval(p) << "\n"; - } - // SASSERT(wval(e).commit_eval()); VERIFY(wval(e).commit_eval()); } @@ -2103,7 +2097,7 @@ namespace sls { bool is_true = ctx.is_true(e); bool is_true_new = bval1(to_app(e)); bool is_true_old = bval1_tmp(to_app(e)); - verbose_stream() << "parent " << mk_bounded_pp(e, m) << " " << is_true << " " << is_true_new << " " << is_true_old << "\n"; + // verbose_stream() << "parent " << mk_bounded_pp(e, m) << " " << is_true << " " << is_true_new << " " << is_true_old << "\n"; if (is_true == is_true_new && is_true_new != is_true_old) ++make_count; if (is_true == is_true_old && is_true_new != is_true_old) diff --git a/src/ast/sls/sls_bv_fixed.cpp b/src/ast/sls/sls_bv_fixed.cpp index 55688a34a..c564a26e8 100644 --- a/src/ast/sls/sls_bv_fixed.cpp +++ b/src/ast/sls/sls_bv_fixed.cpp @@ -41,8 +41,6 @@ namespace sls { ev.m_fixed.setx(a->get_id(), true, false); } - - for (auto e : ctx.subterms()) propagate_range_up(e); } diff --git a/src/ast/sls/sls_bv_plugin.cpp b/src/ast/sls/sls_bv_plugin.cpp index 2b35bd154..4dd399548 100644 --- a/src/ast/sls/sls_bv_plugin.cpp +++ b/src/ast/sls/sls_bv_plugin.cpp @@ -166,10 +166,10 @@ namespace sls { else if (bv.is_bv(e)) { log(e, true, false); IF_VERBOSE(5, verbose_stream() << "repair-up "; trace_repair(true, e)); - verbose_stream() << "set random " << m_eval.wval(e) << " --> "; + //verbose_stream() << "set random " << m_eval.wval(e) << " --> "; auto& v = m_eval.wval(e); m_eval.set_random(e); - verbose_stream() << m_eval.wval(e) << "\n"; + //verbose_stream() << m_eval.wval(e) << "\n"; ctx.new_value_eh(e); } else diff --git a/src/ast/sls/sls_bv_valuation.cpp b/src/ast/sls/sls_bv_valuation.cpp index 210b542ec..ef6bb57bb 100644 --- a/src/ast/sls/sls_bv_valuation.cpp +++ b/src/ast/sls/sls_bv_valuation.cpp @@ -592,59 +592,86 @@ namespace sls { return index; } + // The least a' >= a, such that the fixed bits in bits agree with a'. + // 0 if there is no such a'. void bv_valuation::inf_feasible(bvect& a) const { unsigned lo_index = diff_index(a); - if (lo_index != 0) { - lo_index--; - SASSERT(a.get(lo_index) != m_bits.get(lo_index)); - SASSERT(fixed.get(lo_index)); - for (unsigned i = 0; i <= lo_index; ++i) { - if (!fixed.get(i)) - a.set(i, false); - else if (fixed.get(i)) - a.set(i, m_bits.get(i)); - } - if (!a.get(lo_index)) { - for (unsigned i = lo_index + 1; i < bw; ++i) - if (!fixed.get(i) && !a.get(i)) { - a.set(i, true); - break; - } + if (lo_index == 0) + return; + --lo_index; + + // decrement a[lo_index:0] maximally + SASSERT(a.get(lo_index) != m_bits.get(lo_index)); + SASSERT(fixed.get(lo_index)); + for (unsigned i = 0; i <= lo_index; ++i) { + if (!fixed.get(i)) + a.set(i, false); + else if (fixed.get(i)) + a.set(i, m_bits.get(i)); + } + + // the previous value of a[lo_index] was 0. + // a[lo_index:0] was incremented, so no need to adjust bits a[:lo_index+1] + if (a.get(lo_index)) + return; + + // find the minimal increment within a[:lo_index+1] + for (unsigned i = lo_index + 1; i < bw; ++i) { + if (!fixed.get(i) && !a.get(i)) { + a.set(i, true); + return; } } + // there is no feasiable value a' >= a, so find the least + // feasiable value a' >= 0. + for (unsigned i = 0; i < bw; ++i) + if (!fixed.get(i)) + a.set(i, false); } + // The greatest a' <= a, such that the fixed bits in bits agree with a'. + // the greatest a' <= -1 if there is no such a'. + void bv_valuation::sup_feasible(bvect& a) const { unsigned hi_index = diff_index(a); - if (hi_index != 0) { - hi_index--; - SASSERT(a.get(hi_index) != m_bits.get(hi_index)); - SASSERT(fixed.get(hi_index)); - for (unsigned i = 0; i <= hi_index; ++i) { - if (!fixed.get(i)) - a.set(i, true); - else if (fixed.get(i)) - a.set(i, m_bits.get(i)); - } - if (a.get(hi_index)) { - for (unsigned i = hi_index + 1; i < bw; ++i) - if (!fixed.get(i) && a.get(i)) { - a.set(i, false); - break; - } + if (hi_index == 0) + return; + --hi_index; + SASSERT(a.get(hi_index) != m_bits.get(hi_index)); + SASSERT(fixed.get(hi_index)); + + // increment a[hi_index:0] maximally + for (unsigned i = 0; i <= hi_index; ++i) { + if (!fixed.get(i)) + a.set(i, true); + else if (fixed.get(i)) + a.set(i, m_bits.get(i)); + } + + // If a[hi_index:0] was decremented, then no need to adjust bits a[:hi_index+1] + if (!a.get(hi_index)) + return; + + // find the minimal decrement within a[:hi_index+1] + for (unsigned i = hi_index + 1; i < bw; ++i) { + if (!fixed.get(i) && a.get(i)) { + a.set(i, false); + return; } } + + // a[hi_index:0] was incremented, but a[:hi_index+1] cannot be decremented. + + } void bv_valuation::tighten_range() { + // verbose_stream() << "tighten " << m_lo << " " << m_hi << " " << m_bits << "\n"; if (m_lo == m_hi) return; - if (!in_range(m_bits)) - m_bits = m_lo; - if (is_zero(m_hi)) return; @@ -658,59 +685,8 @@ namespace sls { add1(hi1); hi1.copy_to(nw, m_hi); - /* - unsigned lo_index = 0, hi_index = 0; - for (unsigned i = nw; i-- > 0; ) { - auto lo_diff = (fixed[i] & (m_bits[i] ^ m_lo[i])); - if (lo_diff != 0 && lo_index == 0) - lo_index = 1 + i * 8 * sizeof(digit_t) + log2(lo_diff); - auto hi_diff = (fixed[i] & (m_bits[i] ^ hi1[i])); - if (hi_diff != 0 && hi_index == 0) - hi_index = 1 + i * 8 * sizeof(digit_t) + log2(hi_diff); - } - - if (lo_index != 0) { - lo_index--; - SASSERT(m_lo.get(lo_index) != m_bits.get(lo_index)); - SASSERT(fixed.get(lo_index)); - for (unsigned i = 0; i <= lo_index; ++i) { - if (!fixed.get(i)) - m_lo.set(i, false); - else if (fixed.get(i)) - m_lo.set(i, m_bits.get(i)); - } - if (!m_bits.get(lo_index)) { - for (unsigned i = lo_index + 1; i < bw; ++i) - if (!fixed.get(i) && !m_lo.get(i)) { - m_lo.set(i, true); - break; - } - } - } - if (hi_index != 0) { - hi_index--; - SASSERT(hi1.get(hi_index) != m_bits.get(hi_index)); - SASSERT(fixed.get(hi_index)); - for (unsigned i = 0; i <= hi_index; ++i) { - if (!fixed.get(i)) - hi1.set(i, true); - else if (fixed.get(i)) - hi1.set(i, m_bits.get(i)); - } - if (m_bits.get(hi_index)) { - for (unsigned i = hi_index + 1; i < bw; ++i) - if (!fixed.get(i) && hi1.get(i)) { - hi1.set(i, false); - break; - } - } - add1(hi1); - hi1.copy_to(nw, m_hi); - } - */ - if (has_range() && !in_range(m_bits)) - m_bits = m_lo; + m_lo.copy_to(nw, m_bits); if (mod(lo() + 1, rational::power_of_two(bw)) == hi()) for (unsigned i = 0; i < nw; ++i) @@ -720,6 +696,7 @@ namespace sls { if (hi() < rational::power_of_two(i)) fixed.set(i, true); + // verbose_stream() << "post tighten " << m_lo << " " << m_hi << " " << m_bits << "\n"; SASSERT(well_formed()); } diff --git a/src/ast/sls/sls_bv_valuation.h b/src/ast/sls/sls_bv_valuation.h index f2d2ae92f..4f7c8f902 100644 --- a/src/ast/sls/sls_bv_valuation.h +++ b/src/ast/sls/sls_bv_valuation.h @@ -166,8 +166,8 @@ namespace sls { bool has_range() const { return m_lo != m_hi; } void tighten_range(); - void save_value() { m_tmp = m_bits; } - void restore_value() { m_bits = m_tmp; } + void save_value() { m_bits.copy_to(nw, m_tmp); } + void restore_value() { m_tmp.copy_to(nw, m_bits); } void clear_overflow_bits(bvect& bits) const { SASSERT(nw > 0);