From aec867586a67b5153677a47f2cd554c8da79ef42 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Mon, 2 Dec 2024 13:41:18 -0800
Subject: [PATCH] updates to equality solving search
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
src/ast/sls/sls_arith_base.cpp | 2 +-
src/ast/sls/sls_seq_plugin.cpp | 11 +++++++++++
2 files changed, 12 insertions(+), 1 deletion(-)
diff --git a/src/ast/sls/sls_arith_base.cpp b/src/ast/sls/sls_arith_base.cpp
index 590c4c6df..a31304831 100644
--- a/src/ast/sls/sls_arith_base.cpp
+++ b/src/ast/sls/sls_arith_base.cpp
@@ -2191,7 +2191,7 @@ namespace sls {
auto const& vi = m_vars[v];
if (vi.m_def_idx == UINT_MAX)
return true;
- IF_VERBOSE(2, verbose_stream() << " repair def " << mk_bounded_pp(vi.m_expr, m) << "\n");
+ IF_VERBOSE(4, verbose_stream() << vi.m_op << " repair def " << mk_bounded_pp(vi.m_expr, m) << "\n");
TRACE("sls", tout << "repair def " << mk_bounded_pp(vi.m_expr, m) << "\n");
switch (vi.m_op) {
case arith_op_kind::LAST_ARITH_OP:
diff --git a/src/ast/sls/sls_seq_plugin.cpp b/src/ast/sls/sls_seq_plugin.cpp
index d8e42d234..1f7d927e2 100644
--- a/src/ast/sls/sls_seq_plugin.cpp
+++ b/src/ast/sls/sls_seq_plugin.cpp
@@ -605,11 +605,15 @@ namespace sls {
zstring ch(m_chars[ctx.rand(m_chars.size())]);
m_str_updates.push_back({ x, strval1(y) + ch, 1 });
m_str_updates.push_back({ x, ch + strval1(y), 1 });
+ m_str_updates.push_back({ x, ch, 1 });
+ m_str_updates.push_back({ x, zstring(), 1 });
}
if (!is_value(y) && !m_chars.empty()) {
zstring ch(m_chars[ctx.rand(m_chars.size())]);
m_str_updates.push_back({ y, strval1(x) + ch, 1 });
m_str_updates.push_back({ y, ch + strval1(x), 1 });
+ m_str_updates.push_back({ x, ch, 1 });
+ m_str_updates.push_back({ x, zstring(), 1});
}
}
return apply_update();
@@ -826,6 +830,7 @@ namespace sls {
expr* x, * y;
VERIFY(seq.str.is_at(e, x, y));
zstring se = strval0(e);
+ verbose_stream() << "repair down at " << mk_pp(e, m) << " " << se << "\n";
if (se.length() > 1)
return false;
zstring sx = strval0(x);
@@ -886,6 +891,12 @@ namespace sls {
if (offset_r.is_unsigned())
offset_u = offset_r.get_unsigned();
+ // set to not a member:
+ if (value == -1) {
+ m_str_updates.push_back({ y, zstring(m_chars[ctx.rand(m_chars.size())]), 1 });
+ if (lenx > 0)
+ m_str_updates.push_back({ x, zstring(), 1 });
+ }
// change x:
// insert y into x at offset
if (offset_r.is_unsigned() && 0 <= value && offset_u + value <= lenx && leny > 0) {