From 1e5c59a06f46fb80f5f98738f922c73d196f3e43 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Thu, 12 Dec 2024 09:15:36 -0800
Subject: [PATCH] add repair step for str.replace

---
 src/ast/sls/sls_seq_plugin.cpp | 28 ++++++++++++++++++++++++++--
 1 file changed, 26 insertions(+), 2 deletions(-)

diff --git a/src/ast/sls/sls_seq_plugin.cpp b/src/ast/sls/sls_seq_plugin.cpp
index fd2b85a2a..78b6cc0c0 100644
--- a/src/ast/sls/sls_seq_plugin.cpp
+++ b/src/ast/sls/sls_seq_plugin.cpp
@@ -414,7 +414,15 @@ namespace sls {
                     return ev.val1.svalue;
                 }
             }
-            case OP_SEQ_REPLACE:
+            case OP_SEQ_REPLACE: {
+                expr* x, * y, * z;
+                VERIFY(seq.str.is_replace(e, x, y, z));
+                zstring r = strval0(x);
+                zstring s = strval0(y);
+                zstring t = strval0(z);
+                ev.val1.svalue = r.replace(s, t);
+                return ev.val1.svalue;
+            }
             case OP_SEQ_NTH:
             case OP_SEQ_NTH_I:
             case OP_SEQ_NTH_U:
@@ -1133,6 +1141,10 @@ namespace sls {
             if (seq.is_string(to_app(e)->get_arg(0)->get_sort()))
                 return repair_down_in_re(e);
             break;
+        case OP_SEQ_REPLACE:
+            if (seq.is_string(e->get_sort()))
+                return repair_down_str_replace(e);
+            break;
         case OP_STRING_UBVTOS:
         case OP_STRING_SBVTOS:
         case OP_STRING_TO_CODE:
@@ -1141,7 +1153,7 @@ namespace sls {
         case OP_SEQ_NTH:
         case OP_SEQ_NTH_I:
         case OP_SEQ_NTH_U:
-        case OP_SEQ_REPLACE:
+
         case OP_SEQ_REPLACE_RE_ALL:
         case OP_SEQ_REPLACE_RE:
         case OP_SEQ_REPLACE_ALL:
@@ -1180,6 +1192,18 @@ namespace sls {
         return false;
     }
 
+    bool seq_plugin::repair_down_str_replace(app* e) {
+        expr* x, * y, * z;
+        VERIFY(seq.str.is_replace(e, x, y, z));
+        zstring r = strval0(e);
+        if (r == strval1(e))
+            return true;
+        if (!is_value(x))
+            m_str_updates.push_back({ x, r, 1 });
+        // TODO some more possible ways, also deal with y, z if they are not values.
+        return apply_update();
+    }
+
     bool seq_plugin::repair_down_str_itos(app* e) {
         expr* x;
         VERIFY(seq.str.is_itos(e, x));