From ab0459e5aa8d2b3389813ce5b656c9355f536951 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Tue, 20 Feb 2024 13:38:04 -0800
Subject: [PATCH] bugfixes
---
src/ast/sls/bv_sls.cpp | 37 ++++++++++++++++++++---------------
src/ast/sls/bv_sls.h | 1 +
src/ast/sls/bv_sls_eval.cpp | 2 +-
src/ast/sls/bv_sls_fixed.cpp | 4 ++--
src/ast/sls/bv_sls_terms.h | 2 ++
src/ast/sls/sls_valuation.cpp | 3 ++-
6 files changed, 29 insertions(+), 20 deletions(-)
diff --git a/src/ast/sls/bv_sls.cpp b/src/ast/sls/bv_sls.cpp
index d63bd4f0f..7cfd3f78d 100644
--- a/src/ast/sls/bv_sls.cpp
+++ b/src/ast/sls/bv_sls.cpp
@@ -38,13 +38,22 @@ namespace bv {
void sls::init_eval(std::function<bool(expr*, unsigned)>& eval) {
m_eval.init_eval(m_terms.assertions(), eval);
+ m_eval.init_fixed(m_terms.assertions());
+ init_repair();
+ }
+
+ void sls::init_repair() {
+ 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());
}
}
- m_eval.init_fixed(m_terms.assertions());
+ for (app* t : m_terms.terms())
+ if (t && !eval_is_correct(t))
+ m_repair_down.insert(t->get_id());
}
void sls::reinit_eval() {
@@ -64,14 +73,7 @@ namespace bv {
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());
- }
- }
+ init_repair();
}
std::pair<bool, app*> sls::next_to_repair() {
@@ -95,12 +97,14 @@ namespace bv {
auto [down, e] = next_to_repair();
if (!e)
return l_true;
+ bool is_correct = eval_is_correct(e);
IF_VERBOSE(20, verbose_stream() << (down ? "d #" : "u #")
- << e->get_id() << ": "
- << mk_bounded_pp(e, m, 1) << " ";
- if (bv.is_bv(e)) verbose_stream() << m_eval.wval0(e);
- verbose_stream() << "\n");
- if (eval_is_correct(e)) {
+ << e->get_id() << ": "
+ << mk_bounded_pp(e, m, 1) << " ";
+ if (bv.is_bv(e)) verbose_stream() << m_eval.wval0(e) << " ";
+ if (m.is_bool(e)) verbose_stream() << m_eval.bval0(e) << " ";
+ verbose_stream() << (is_correct?"C":"U") << "\n");
+ if (is_correct) {
if (down)
m_repair_down.remove(e->get_id());
else
@@ -185,8 +189,8 @@ namespace bv {
model_ref sls::get_model() {
model_ref mdl = alloc(model, m);
- m_eval.sort_assertions(m_terms.assertions());
- for (expr* e : m_todo) {
+ auto& terms = m_eval.sort_assertions(m_terms.assertions());
+ for (expr* e : terms) {
if (!is_uninterp_const(e))
continue;
auto f = to_app(e)->get_decl();
@@ -199,6 +203,7 @@ namespace bv {
mdl->register_decl(f, bv.mk_numeral(n, v.bw));
}
}
+ terms.reset();
return mdl;
}
diff --git a/src/ast/sls/bv_sls.h b/src/ast/sls/bv_sls.h
index 753cf58ff..e2030986d 100644
--- a/src/ast/sls/bv_sls.h
+++ b/src/ast/sls/bv_sls.h
@@ -59,6 +59,7 @@ namespace bv {
lbool search();
void reinit_eval();
+ void init_repair();
void trace();
public:
diff --git a/src/ast/sls/bv_sls_eval.cpp b/src/ast/sls/bv_sls_eval.cpp
index c01acf88a..3a128bfcd 100644
--- a/src/ast/sls/bv_sls_eval.cpp
+++ b/src/ast/sls/bv_sls_eval.cpp
@@ -1020,7 +1020,7 @@ namespace bv {
unsigned parity_e = e.parity(e.bits);
unsigned parity_b = b.parity(b.bits);
-#if 1
+#if 0
auto& x = m_tmp;
auto& y = m_tmp2;
diff --git a/src/ast/sls/bv_sls_fixed.cpp b/src/ast/sls/bv_sls_fixed.cpp
index f7cd4c23a..cb82a50dd 100644
--- a/src/ast/sls/bv_sls_fixed.cpp
+++ b/src/ast/sls/bv_sls_fixed.cpp
@@ -103,9 +103,9 @@ namespace bv {
else if (!sign && m.is_eq(e, s, t)) {
if (bv.is_numeral(s, a))
// t - a <= 0
- init_range(t, -a, nullptr, rational(0), !sign);
+ init_range(t, -a, nullptr, rational(0), false);
else if (bv.is_numeral(t, a))
- init_range(s, -a, nullptr, rational(0), !sign);
+ init_range(s, -a, nullptr, rational(0), false);
}
else if (bv.is_bit2bool(e, s, idx)) {
auto& val = wval0(s);
diff --git a/src/ast/sls/bv_sls_terms.h b/src/ast/sls/bv_sls_terms.h
index 95d9a508e..2f9aee225 100644
--- a/src/ast/sls/bv_sls_terms.h
+++ b/src/ast/sls/bv_sls_terms.h
@@ -67,6 +67,8 @@ namespace bv {
app* term(unsigned id) const { return m_terms.get(id); }
+ app_ref_vector const& terms() const { return m_terms; }
+
bool is_assertion(expr* e) const { return m_assertion_set.contains(e->get_id()); }
};
diff --git a/src/ast/sls/sls_valuation.cpp b/src/ast/sls/sls_valuation.cpp
index db977cc2e..21e44b3fe 100644
--- a/src/ast/sls/sls_valuation.cpp
+++ b/src/ast/sls/sls_valuation.cpp
@@ -243,9 +243,10 @@ namespace bv {
void sls_valuation::get_value(svector<digit_t> const& bits, rational& r) const {
rational p(1);
+ r = 0;
for (unsigned i = 0; i < nw; ++i) {
r += p * rational(bits[i]);
- p *= rational::power_of_two(bw);
+ p *= rational::power_of_two(8*sizeof(digit_t));
}
}