From 1ba6da827023f0980ad5a00772dd91665620d2a4 Mon Sep 17 00:00:00 2001
From: ajreynol <andrew.j.reynolds@gmail.com>
Date: Tue, 9 May 2017 17:16:06 -0500
Subject: [PATCH] Change str.replace for empty string.

---
 .../strings/theory_strings_rewriter.cpp       | 75 ++++++++++---------
 test/regress/regress0/strings/Makefile.am     |  3 +-
 .../regress0/strings/repl-empty-sem.smt2      | 11 +++
 3 files changed, 53 insertions(+), 36 deletions(-)
 create mode 100644 test/regress/regress0/strings/repl-empty-sem.smt2

diff --git a/src/theory/strings/theory_strings_rewriter.cpp b/src/theory/strings/theory_strings_rewriter.cpp
index 2ee367cfc..6daaddcd7 100644
--- a/src/theory/strings/theory_strings_rewriter.cpp
+++ b/src/theory/strings/theory_strings_rewriter.cpp
@@ -1622,42 +1622,47 @@ Node TheoryStringsRewriter::rewriteReplace( Node node ) {
   if( node[1]==node[2] ){
     return node[0];
   }else{
-    std::vector< Node > children;
-    getConcat( node[0], children );
-    if( children[0].isConst() && node[1].isConst() ){
-      CVC4::String s = children[0].getConst<String>();
-      CVC4::String t = node[1].getConst<String>();
-      std::size_t p = s.find(t);
-      if( p != std::string::npos ) {
-        Node retNode;
-        if( node[2].isConst() ){
-          CVC4::String r = node[2].getConst<String>();
-          CVC4::String ret = s.replace(t, r);
-          retNode = NodeManager::currentNM()->mkConst( ::CVC4::String(ret) );
-        } 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) );
-          retNode = NodeManager::currentNM()->mkNode( kind::STRING_CONCAT, ns1, node[2], ns3 );
-        }
-        if( children.size()>1 ){
-          children[0] = retNode;
-          return mkConcat( kind::STRING_CONCAT, children );
-        }else{
-          return retNode;
-        }
-      }else{
-        //could not find replacement string
-        if( node[0].isConst() ){
-          return node[0];
+    if( node[1].isConst() ){
+      if( node[1].getConst<String>().isEmptyString() ){
+        return node[0];
+      }
+      std::vector< Node > children;
+      getConcat( node[0], children );
+      if( children[0].isConst() ){
+        CVC4::String s = children[0].getConst<String>();
+        CVC4::String t = node[1].getConst<String>();
+        std::size_t p = s.find(t);
+        if( p != std::string::npos ) {
+          Node retNode;
+          if( node[2].isConst() ){
+            CVC4::String r = node[2].getConst<String>();
+            CVC4::String ret = s.replace(t, r);
+            retNode = NodeManager::currentNM()->mkConst( ::CVC4::String(ret) );
+          } 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) );
+            retNode = NodeManager::currentNM()->mkNode( kind::STRING_CONCAT, ns1, node[2], ns3 );
+          }
+          if( children.size()>1 ){
+            children[0] = retNode;
+            return mkConcat( kind::STRING_CONCAT, children );
+          }else{
+            return retNode;
+          }
         }else{
-          //check for overlap, if none, we can remove the prefix
-          if( s.overlap(t)==0 ){
-            std::vector< Node > spl;
-            spl.insert( spl.end(), children.begin()+1, children.end() );
-            return NodeManager::currentNM()->mkNode( kind::STRING_CONCAT, children[0],
-                        NodeManager::currentNM()->mkNode( kind::STRING_STRREPL, mkConcat( kind::STRING_CONCAT, spl ), node[1], node[2] ) );
+          //could not find replacement string
+          if( node[0].isConst() ){
+            return node[0];
+          }else{
+            //check for overlap, if none, we can remove the prefix
+            if( s.overlap(t)==0 ){
+              std::vector< Node > spl;
+              spl.insert( spl.end(), children.begin()+1, children.end() );
+              return NodeManager::currentNM()->mkNode( kind::STRING_CONCAT, children[0],
+                          NodeManager::currentNM()->mkNode( kind::STRING_STRREPL, mkConcat( kind::STRING_CONCAT, spl ), node[1], node[2] ) );
+            }
           }
         }
       }
diff --git a/test/regress/regress0/strings/Makefile.am b/test/regress/regress0/strings/Makefile.am
index f4dc8ebf7..41c500170 100644
--- a/test/regress/regress0/strings/Makefile.am
+++ b/test/regress/regress0/strings/Makefile.am
@@ -86,7 +86,8 @@ TESTS = \
   cmu-inc-nlpp-071516.smt2 \
   strings-index-empty.smt2 \
   bug768.smt2 \
-  username_checker_min.smt2
+  username_checker_min.smt2 \
+  repl-empty-sem.smt2
 
 FAILING_TESTS =
 
diff --git a/test/regress/regress0/strings/repl-empty-sem.smt2 b/test/regress/regress0/strings/repl-empty-sem.smt2
new file mode 100644
index 000000000..61f70bc23
--- /dev/null
+++ b/test/regress/regress0/strings/repl-empty-sem.smt2
@@ -0,0 +1,11 @@
+; COMMAND-LINE: --strings-exp
+; EXPECT: unsat
+(set-logic ALL)
+(set-info :status unsat)
+(declare-fun x () String)
+(declare-fun z () String)
+(assert (= (str.len z) 0))
+(assert (= (str.replace "ab" z "c") x))
+(declare-fun y () String)
+(assert (= x (str.++ "c" y)))
+(check-sat)
-- 
2.30.2