From d7e419b7ed2ea4df65334767db0ac48ef5ba4424 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Tue, 20 Feb 2024 14:14:12 -0800
Subject: [PATCH] fixes and checks
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
src/ast/sls/bv_sls.cpp | 10 ++++++++++
src/ast/sls/bv_sls_eval.cpp | 10 +++++-----
2 files changed, 15 insertions(+), 5 deletions(-)
diff --git a/src/ast/sls/bv_sls.cpp b/src/ast/sls/bv_sls.cpp
index 7cfd3f78d..d977ff401 100644
--- a/src/ast/sls/bv_sls.cpp
+++ b/src/ast/sls/bv_sls.cpp
@@ -171,6 +171,7 @@ namespace bv {
}
else {
m_eval.repair_up(e);
+ SASSERT(eval_is_correct(e));
for (auto p : m_terms.parents(e))
m_repair_up.insert(p->get_id());
}
@@ -191,8 +192,17 @@ namespace bv {
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))) {
+ verbose_stream() << "missed evaluation #" << e->get_id() << " " << mk_bounded_pp(e, m) << "\n";
+ if (bv.is_bv(e)) {
+ auto const& v0 = m_eval.wval0(e);
+ auto const& v1 = m_eval.wval1(to_app(e));
+ verbose_stream() << v0 << "\n" << v1 << "\n";
+ }
+ }
if (!is_uninterp_const(e))
continue;
+
auto f = to_app(e)->get_decl();
if (m.is_bool(e))
mdl->register_decl(f, m.mk_bool_val(m_eval.bval0(e)));
diff --git a/src/ast/sls/bv_sls_eval.cpp b/src/ast/sls/bv_sls_eval.cpp
index 3a128bfcd..0693ce7cc 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 0
+#if 1
auto& x = m_tmp;
auto& y = m_tmp2;
@@ -1521,9 +1521,9 @@ namespace bv {
}
bool sls_eval::try_repair_extract(bvval const& e, bvval& a, unsigned lo) {
- for (unsigned i = 0; i < a.bw; ++i)
- if (!a.get(a.fixed, i))
- a.set(a.bits, i, e.get(e.bits, i + lo));
+ for (unsigned i = 0; i < e.bw; ++i)
+ if (!a.get(a.fixed, i + lo))
+ a.set(a.bits, i + lo, e.get(e.bits, i));
return true;
}
@@ -1553,6 +1553,6 @@ namespace bv {
if (m.is_bool(e))
set(e, bval1(to_app(e)));
else if (bv.is_bv(e))
- wval0(e).try_set(wval1(to_app(e)));
+ wval0(e).set(wval1(to_app(e)));
}
}