From dfd5c27fec205f9fd939e6a208dac7ffab73cad4 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Wed, 28 Feb 2024 17:09:41 -0800
Subject: [PATCH] na
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
src/ast/sls/bv_sls.cpp | 41 ++++++++++++++++++++++-------------
src/ast/sls/bv_sls.h | 2 +-
src/ast/sls/bv_sls_eval.cpp | 7 +++++-
src/ast/sls/bv_sls_fixed.cpp | 2 +-
src/ast/sls/sls_valuation.cpp | 20 +++++++++++------
src/ast/sls/sls_valuation.h | 2 +-
6 files changed, 48 insertions(+), 26 deletions(-)
diff --git a/src/ast/sls/bv_sls.cpp b/src/ast/sls/bv_sls.cpp
index 50ec5da6b64..3902957fc71 100644
--- a/src/ast/sls/bv_sls.cpp
+++ b/src/ast/sls/bv_sls.cpp
@@ -52,6 +52,19 @@ namespace bv {
m_repair_roots.insert(e->get_id());
}
}
+ for (auto* t : m_terms.terms()) {
+ if (t && !re_eval_is_correct(t))
+ m_repair_roots.insert(t->get_id());
+ }
+ }
+
+ void sls::init_repair_goal(app* t) {
+ if (m.is_bool(t))
+ m_eval.set(t, m_eval.bval1(t));
+ else if (bv.is_bv(t)) {
+ auto& v = m_eval.wval(t);
+ v.bits().copy_to(v.nw, v.eval);
+ }
}
void sls::reinit_eval() {
@@ -89,11 +102,18 @@ namespace bv {
return { false, e };
}
- if (!m_repair_roots.empty()) {
+ while (!m_repair_roots.empty()) {
unsigned index = m_repair_roots.elem_at(m_rand(m_repair_roots.size()));
e = m_terms.term(index);
- m_repair_root = index;
- return { true, e };
+ if (m_terms.is_assertion(e) && !m_eval.bval1(e)) {
+ SASSERT(m_eval.bval0(e));
+ return { true, e };
+ }
+ if (!re_eval_is_correct(e)) {
+ init_repair_goal(e);
+ return { true, e };
+ }
+ m_repair_roots.remove(index);
}
return { false, nullptr };
@@ -103,11 +123,12 @@ namespace bv {
// init and init_eval were invoked
unsigned n = 0;
for (; n++ < m_config.m_max_repairs && m.inc(); ) {
- ++m_stats.m_moves;
auto [down, e] = next_to_repair();
if (!e)
return l_true;
+ ++m_stats.m_moves;
+
trace_repair(down, e);
if (down)
@@ -137,22 +158,12 @@ 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;
- }
-
unsigned n = e->get_num_args();
if (n == 0) {
auto& v = m_eval.wval(e);
- v.commit_eval();
+ VERIFY(v.commit_eval());
for (auto p : m_terms.parents(e))
m_repair_up.insert(p->get_id());
- m_repair_roots.remove(m_repair_root);
- m_repair_root = UINT_MAX;
return;
}
diff --git a/src/ast/sls/bv_sls.h b/src/ast/sls/bv_sls.h
index 177ac5069d4..bbcd59aea95 100644
--- a/src/ast/sls/bv_sls.h
+++ b/src/ast/sls/bv_sls.h
@@ -46,7 +46,6 @@ namespace bv {
sls_stats m_stats;
indexed_uint_set m_repair_up, m_repair_roots;
unsigned m_repair_down = UINT_MAX;
- unsigned m_repair_root = UINT_MAX;
ptr_vector<expr> m_todo;
random_gen m_rand;
config m_config;
@@ -55,6 +54,7 @@ namespace bv {
bool eval_is_correct(app* e);
bool re_eval_is_correct(app* e);
+ void init_repair_goal(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 a215fd5c6ed..931364e308e 100644
--- a/src/ast/sls/bv_sls_eval.cpp
+++ b/src/ast/sls/bv_sls_eval.cpp
@@ -1100,7 +1100,7 @@ namespace bv {
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);
- return a.set_repair(random_bool(), m_tmp);
+ return a.set_repair(random_bool(), m_tmp);
}
bool sls_eval::try_repair_bnot(bvect const& e, bvval& a) {
@@ -1633,6 +1633,11 @@ namespace bv {
}
if (bv.is_bv(e)) {
auto& v = eval(to_app(e));
+ for (unsigned i = 0; i < v.nw; ++i)
+ if (0 != (v.fixed[i] & (v.bits()[i] ^ v.eval[i]))) {
+ v.bits().copy_to(v.nw, v.eval);
+ return false;
+ }
v.commit_eval();
return true;
}
diff --git a/src/ast/sls/bv_sls_fixed.cpp b/src/ast/sls/bv_sls_fixed.cpp
index 4f49f26486a..60984279051 100644
--- a/src/ast/sls/bv_sls_fixed.cpp
+++ b/src/ast/sls/bv_sls_fixed.cpp
@@ -25,7 +25,7 @@ namespace bv {
{}
void sls_fixed::init(expr_ref_vector const& es) {
- // init_ranges(es);
+ init_ranges(es);
ev.sort_assertions(es);
for (expr* e : ev.m_todo) {
if (!is_app(e))
diff --git a/src/ast/sls/sls_valuation.cpp b/src/ast/sls/sls_valuation.cpp
index a410a015784..d4bf333534e 100644
--- a/src/ast/sls/sls_valuation.cpp
+++ b/src/ast/sls/sls_valuation.cpp
@@ -95,14 +95,14 @@ namespace bv {
mask = ~(digit_t)0;
}
- void sls_valuation::commit_eval() {
- DEBUG_CODE(
- for (unsigned i = 0; i < nw; ++i)
- VERIFY(0 == (fixed[i] & (m_bits[i] ^ eval[i])));
- );
+ bool sls_valuation::commit_eval() {
+ for (unsigned i = 0; i < nw; ++i)
+ if (0 != (fixed[i] & (m_bits[i] ^ eval[i])))
+ return false;
for (unsigned i = 0; i < nw; ++i)
m_bits[i] = eval[i];
SASSERT(well_formed());
+ return true;
}
bool sls_valuation::in_range(bvect const& bits) const {
@@ -446,6 +446,9 @@ namespace bv {
if (h == l)
return;
+ //verbose_stream() << "[" << l << ", " << h << "[\n";
+ //verbose_stream() << *this << "\n";
+
SASSERT(is_zero(fixed)); // ranges can only be added before fixed bits are set.
if (m_lo == m_hi) {
@@ -473,10 +476,13 @@ namespace bv {
set_value(m_hi, h);
}
}
+
+
+
SASSERT(!has_overflow(m_lo));
SASSERT(!has_overflow(m_hi));
- if (!in_range(eval))
- set(eval, m_lo);
+ if (!in_range(m_bits))
+ set(m_bits, m_lo);
SASSERT(well_formed());
}
diff --git a/src/ast/sls/sls_valuation.h b/src/ast/sls/sls_valuation.h
index 88d8509d76f..0cd357d4da2 100644
--- a/src/ast/sls/sls_valuation.h
+++ b/src/ast/sls/sls_valuation.h
@@ -115,7 +115,7 @@ namespace bv {
digit_t bits(unsigned i) const { return m_bits[i]; }
bvect const& bits() const { return m_bits; }
- void commit_eval();
+ bool commit_eval();
bool get_bit(unsigned i) const { return m_bits.get(i); }
bool try_set_bit(unsigned i, bool b) {