updates to equality solving search

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
Z3Prover · Dec 2, 2024 · aec8675 · aec8675
1 parent e6feb84
commit aec8675
Show file tree

Hide file tree

Showing 2 changed files with 12 additions and 1 deletion.
diff --git 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
@@ -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) {