Minor improvement for rewriter for str.replace (#3124)

diff --git a/src/theory/strings/theory_strings_rewriter.cpp b/src/theory/strings/theory_strings_rewriter.cpp
index d720fedc82aa65b1d0ef7cc351add974a258eb9c..aac2477ea1403f09a6d29f6ea2c5014473677817 100644 (file)
--- a/src/theory/strings/theory_strings_rewriter.cpp
+++ b/src/theory/strings/theory_strings_rewriter.cpp
@@ -2456,14 +2456,20 @@ Node TheoryStringsRewriter::rewriteReplace( Node node ) {
     }
     else
     {
-      CVC4::String s1 = s.substr(0, (int)p);
-      CVC4::String s3 = s.substr((int)p + (int)t.size());
-      Node ns1 = NodeManager::currentNM()->mkConst(::CVC4::String(s1));
-      Node ns3 = NodeManager::currentNM()->mkConst(::CVC4::String(s3));
+      String s1 = s.substr(0, (int)p);
+      String s3 = s.substr((int)p + (int)t.size());
       std::vector<Node> children;
-      children.push_back(ns1);
+      if (s1.size() > 0)
+      {
+        Node ns1 = nm->mkConst(String(s1));
+        children.push_back(ns1);
+      }
       children.push_back(node[2]);
-      children.push_back(ns3);
+      if (s3.size() > 0)
+      {
+        Node ns3 = nm->mkConst(String(s3));
+        children.push_back(ns3);
+      }
       children.insert(children.end(), children0.begin() + 1, children0.end());
       Node ret = utils::mkConcat(STRING_CONCAT, children);
       return returnRewrite(node, ret, "rpl-const-find");

diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt
index 90641fe2fc525702e677b937cb3f554bbdc1f634..0ac2d4142f3334d7494ec26cf19d37560dfe0757 100644 (file)
--- a/test/regress/CMakeLists.txt
+++ b/test/regress/CMakeLists.txt
@@ -853,6 +853,7 @@ set(regress_0_tests
   regress0/strings/norn-simp-rew.smt2
   regress0/strings/re.all.smt2
   regress0/strings/repl-rewrites2.smt2
+  regress0/strings/replace-const.smt2
   regress0/strings/replaceall-eval.smt2
   regress0/strings/rewrites-re-concat.smt2
   regress0/strings/rewrites-v2.smt2

diff --git a/test/regress/regress0/strings/replace-const.smt2 b/test/regress/regress0/strings/replace-const.smt2
new file mode 100644 (file)
index 0000000..a7f225e
--- /dev/null
+++ b/test/regress/regress0/strings/replace-const.smt2
@@ -0,0 +1,12 @@
+(set-info :smt-lib-version 2.5)
+(set-logic ALL)
+(set-info :status sat)
+(declare-fun x () String)
+(declare-fun y () String)
+(declare-fun z () String)
+
+(assert (= x (str.replace "AA" "AA" "def")))
+(assert (= y (str.replace "BAA" "B" "def")))
+(assert (= z (str.replace "AAB" "B" "def")))
+
+(check-sat)