Support string replace all (#2704)

17 files changed, 296 insertions, 26 deletions

diff --git a/src/parser/cvc/Cvc.g b/src/parser/cvc/Cvc.g
index 3eddf438f..29bc84510 100644
--- a/src/parser/cvc/Cvc.g
+++ b/src/parser/cvc/Cvc.g
@@ -222,6 +222,7 @@ tokens {
   STRING_CHARAT_TOK = 'CHARAT';
   STRING_INDEXOF_TOK = 'INDEXOF';
   STRING_REPLACE_TOK = 'REPLACE';
+  STRING_REPLACE_ALL_TOK = 'REPLACE_ALL';
   STRING_PREFIXOF_TOK = 'PREFIXOF';
   STRING_SUFFIXOF_TOK = 'SUFFIXOF';
   STRING_STOI_TOK = 'STRING_TO_INTEGER';
@@ -2028,6 +2029,8 @@ stringTerm[CVC4::Expr& f]
     { f = MK_EXPR(CVC4::kind::STRING_STRIDOF, f, f2, f3); }
   | STRING_REPLACE_TOK LPAREN formula[f] COMMA formula[f2] COMMA formula[f3] RPAREN
     { f = MK_EXPR(CVC4::kind::STRING_STRREPL, f, f2, f3); }
+  | STRING_REPLACE_ALL_TOK LPAREN formula[f] COMMA formula[f2] COMMA formula[f3] RPAREN
+    { f = MK_EXPR(CVC4::kind::STRING_STRREPLALL, f, f2, f3); }
   | STRING_PREFIXOF_TOK LPAREN formula[f] COMMA formula[f2] RPAREN
     { f = MK_EXPR(CVC4::kind::STRING_PREFIX, f, f2); }
   | STRING_SUFFIXOF_TOK LPAREN formula[f] COMMA formula[f2] RPAREN
diff --git a/src/parser/smt2/smt2.cpp b/src/parser/smt2/smt2.cpp
index 2fd61aabc..d52dd948b 100644
--- a/src/parser/smt2/smt2.cpp
+++ b/src/parser/smt2/smt2.cpp
@@ -129,6 +129,7 @@ void Smt2::addStringOperators() {
   addOperator(kind::STRING_CHARAT, "str.at" );
   addOperator(kind::STRING_STRIDOF, "str.indexof" );
   addOperator(kind::STRING_STRREPL, "str.replace" );
+  addOperator(kind::STRING_STRREPLALL, "str.replaceall");
   addOperator(kind::STRING_PREFIX, "str.prefixof" );
   addOperator(kind::STRING_SUFFIX, "str.suffixof" );
   // at the moment, we only use this syntax for smt2.6.1
diff --git a/src/printer/smt2/smt2_printer.cpp b/src/printer/smt2/smt2_printer.cpp
index b71e9d4c4..259f23afc 100644
--- a/src/printer/smt2/smt2_printer.cpp
+++ b/src/printer/smt2/smt2_printer.cpp
@@ -601,6 +601,7 @@ void Smt2Printer::toStream(std::ostream& out,
   case kind::STRING_STRCTN:
   case kind::STRING_STRIDOF:
   case kind::STRING_STRREPL:
+  case kind::STRING_STRREPLALL:
   case kind::STRING_PREFIX:
   case kind::STRING_SUFFIX:
   case kind::STRING_LEQ:
@@ -1143,6 +1144,7 @@ static string smtKindString(Kind k, Variant v)
   case kind::STRING_CHARAT: return "str.at" ;
   case kind::STRING_STRIDOF: return "str.indexof" ;
   case kind::STRING_STRREPL: return "str.replace" ;
+  case kind::STRING_STRREPLALL: return "str.replaceall";
   case kind::STRING_PREFIX: return "str.prefixof" ;
   case kind::STRING_SUFFIX: return "str.suffixof" ;
   case kind::STRING_LEQ: return "str.<=";
diff --git a/src/theory/datatypes/datatypes_sygus.cpp b/src/theory/datatypes/datatypes_sygus.cpp
index 4c7dcec9a..2fee4f48d 100644
--- a/src/theory/datatypes/datatypes_sygus.cpp
+++ b/src/theory/datatypes/datatypes_sygus.cpp
@@ -759,12 +759,12 @@ Node SygusSymBreakNew::getSimpleSymBreakPred(Node e,
             deq_child[1].push_back(1);
           }
         }
-        if (nk == ITE || nk == STRING_STRREPL)
+        if (nk == ITE || nk == STRING_STRREPL || nk == STRING_STRREPLALL)
         {
           deq_child[0].push_back(1);
           deq_child[1].push_back(2);
         }
-        if (nk == STRING_STRREPL)
+        if (nk == STRING_STRREPL || nk == STRING_STRREPLALL)
         {
           deq_child[0].push_back(0);
           deq_child[1].push_back(1);
diff --git a/src/theory/strings/kinds b/src/theory/strings/kinds
index 7fb2d26c6..df6085422 100644
--- a/src/theory/strings/kinds
+++ b/src/theory/strings/kinds
@@ -22,6 +22,7 @@ operator STRING_LT 2 "string less than"
 operator STRING_LEQ 2 "string less than or equal"
 operator STRING_STRIDOF 3 "string indexof"
 operator STRING_STRREPL 3 "string replace"
+operator STRING_STRREPLALL 3 "string replace all"
 operator STRING_PREFIX 2 "string prefixof"
 operator STRING_SUFFIX 2 "string suffixof"
 operator STRING_ITOS 1 "integer to string"
@@ -93,6 +94,7 @@ typerule STRING_LT ::CVC4::theory::strings::StringRelationTypeRule
 typerule STRING_LEQ ::CVC4::theory::strings::StringRelationTypeRule
 typerule STRING_STRIDOF ::CVC4::theory::strings::StringIndexOfTypeRule
 typerule STRING_STRREPL ::CVC4::theory::strings::StringReplaceTypeRule
+typerule STRING_STRREPLALL ::CVC4::theory::strings::StringReplaceTypeRule
 typerule STRING_PREFIX ::CVC4::theory::strings::StringPrefixOfTypeRule
 typerule STRING_SUFFIX ::CVC4::theory::strings::StringSuffixOfTypeRule
 typerule STRING_ITOS ::CVC4::theory::strings::StringIntToStrTypeRule
diff --git a/src/theory/strings/skolem_cache.cpp b/src/theory/strings/skolem_cache.cpp
index 2b0cc8a1b..7725b1b0d 100644
--- a/src/theory/strings/skolem_cache.cpp
+++ b/src/theory/strings/skolem_cache.cpp
@@ -20,31 +20,51 @@ namespace CVC4 {
 namespace theory {
 namespace strings {
 
-SkolemCache::SkolemCache() {}
+SkolemCache::SkolemCache()
+{
+  d_strType = NodeManager::currentNM()->stringType();
+}
 
 Node SkolemCache::mkSkolemCached(Node a, Node b, SkolemId id, const char* c)
 {
+  return mkTypedSkolemCached(d_strType, a, b, id, c);
+}
+
+Node SkolemCache::mkSkolemCached(Node a, SkolemId id, const char* c)
+{
+  return mkSkolemCached(a, Node::null(), id, c);
+}
+
+Node SkolemCache::mkTypedSkolemCached(
+    TypeNode tn, Node a, Node b, SkolemId id, const char* c)
+{
   a = a.isNull() ? a : Rewriter::rewrite(a);
   b = b.isNull() ? b : Rewriter::rewrite(b);
   std::map<SkolemId, Node>::iterator it = d_skolemCache[a][b].find(id);
   if (it == d_skolemCache[a][b].end())
   {
-    Node sk = mkSkolem(c);
+    Node sk = mkTypedSkolem(tn, c);
     d_skolemCache[a][b][id] = sk;
     return sk;
   }
   return it->second;
 }
-
-Node SkolemCache::mkSkolemCached(Node a, SkolemId id, const char* c)
+Node SkolemCache::mkTypedSkolemCached(TypeNode tn,
+                                      Node a,
+                                      SkolemId id,
+                                      const char* c)
 {
-  return mkSkolemCached(a, Node::null(), id, c);
+  return mkTypedSkolemCached(tn, a, Node::null(), id, c);
 }
 
 Node SkolemCache::mkSkolem(const char* c)
 {
-  NodeManager* nm = NodeManager::currentNM();
-  Node n = nm->mkSkolem(c, nm->stringType(), "string skolem");
+  return mkTypedSkolem(d_strType, c);
+}
+
+Node SkolemCache::mkTypedSkolem(TypeNode tn, const char* c)
+{
+  Node n = NodeManager::currentNM()->mkSkolem(c, tn, "string skolem");
   d_allSkolems.insert(n);
   return n;
 }
diff --git a/src/theory/strings/skolem_cache.h b/src/theory/strings/skolem_cache.h
index 1cd4d7de8..d0eabd4c2 100644
--- a/src/theory/strings/skolem_cache.h
+++ b/src/theory/strings/skolem_cache.h
@@ -100,6 +100,16 @@ class SkolemCache
     // b > 0 =>
     //    exists k. a = a' ++ k ^ len( k ) = ite( len(a)>b, len(a)-b, 0 )
     SK_SUFFIX_REM,
+    // --------------- integer skolems
+    // exists k. ( b occurs k times in a )
+    SK_NUM_OCCUR,
+    // --------------- function skolems
+    // For function k: Int -> Int
+    //   exists k.
+    //     forall 0 <= x <= n,
+    //       k(x) is the end index of the x^th occurrence of b in a
+    //   where n is the number of occurrences of b in a, and k(0)=0.
+    SK_OCCUR_INDEX,
   };
   /**
    * Returns a skolem of type string that is cached for (a,b,id) and has
@@ -111,12 +121,21 @@ class SkolemCache
    * name c.
    */
   Node mkSkolemCached(Node a, SkolemId id, const char* c);
+  /** Same as above, but the skolem to construct has a custom type tn */
+  Node mkTypedSkolemCached(
+      TypeNode tn, Node a, Node b, SkolemId id, const char* c);
+  /** Same as mkTypedSkolemCached above for (a,[null],id) */
+  Node mkTypedSkolemCached(TypeNode tn, Node a, SkolemId id, const char* c);
   /** Returns a (uncached) skolem of type string with name c */
   Node mkSkolem(const char* c);
+  /** Same as above, but for custom type tn */
+  Node mkTypedSkolem(TypeNode tn, const char* c);
   /** Returns true if n is a skolem allocated by this class */
   bool isSkolem(Node n) const;
 
  private:
+  /** string type */
+  TypeNode d_strType;
   /** map from node pairs and identifiers to skolems */
   std::map<Node, std::map<Node, std::map<SkolemId, Node> > > d_skolemCache;
   /** the set of all skolems we have generated */
diff --git a/src/theory/strings/theory_strings.cpp b/src/theory/strings/theory_strings.cpp
index 883683f52..e8b753768 100644
--- a/src/theory/strings/theory_strings.cpp
+++ b/src/theory/strings/theory_strings.cpp
@@ -144,6 +144,7 @@ TheoryStrings::TheoryStrings(context::Context* c,
   getExtTheory()->addFunctionKind(kind::STRING_ITOS);
   getExtTheory()->addFunctionKind(kind::STRING_STOI);
   getExtTheory()->addFunctionKind(kind::STRING_STRREPL);
+  getExtTheory()->addFunctionKind(kind::STRING_STRREPLALL);
   getExtTheory()->addFunctionKind(kind::STRING_STRCTN);
   getExtTheory()->addFunctionKind(kind::STRING_IN_REGEXP);
   getExtTheory()->addFunctionKind(kind::STRING_LEQ);
@@ -162,6 +163,7 @@ TheoryStrings::TheoryStrings(context::Context* c,
     d_equalityEngine.addFunctionKind(kind::STRING_STOI);
     d_equalityEngine.addFunctionKind(kind::STRING_STRIDOF);
     d_equalityEngine.addFunctionKind(kind::STRING_STRREPL);
+    d_equalityEngine.addFunctionKind(kind::STRING_STRREPLALL);
   }
 
   d_zero = NodeManager::currentNM()->mkConst( Rational( 0 ) );
@@ -503,7 +505,7 @@ bool TheoryStrings::doReduction(int effort, Node n, bool& isCd)
     NodeManager* nm = NodeManager::currentNM();
     Assert(k == STRING_SUBSTR || k == STRING_STRCTN || k == STRING_STRIDOF
            || k == STRING_ITOS || k == STRING_STOI || k == STRING_STRREPL
-           || k == STRING_LEQ);
+           || k == STRING_STRREPLALL || k == STRING_LEQ);
     std::vector<Node> new_nodes;
     Node res = d_preproc.simplify(n, new_nodes);
     Assert(res != n);
@@ -817,9 +819,8 @@ void TheoryStrings::preRegisterTerm(TNode n) {
     Kind k = n.getKind();
     if( !options::stringExp() ){
       if (k == kind::STRING_STRIDOF || k == kind::STRING_ITOS
-          || k == kind::STRING_STOI
-          || k == kind::STRING_STRREPL
-          || k == kind::STRING_STRCTN
+          || k == kind::STRING_STOI || k == kind::STRING_STRREPL
+          || k == kind::STRING_STRREPLALL || k == kind::STRING_STRCTN
           || k == STRING_LEQ)
       {
         std::stringstream ss;
diff --git a/src/theory/strings/theory_strings_preprocess.cpp b/src/theory/strings/theory_strings_preprocess.cpp
index a1b37e6fb..d095d6801 100644
--- a/src/theory/strings/theory_strings_preprocess.cpp
+++ b/src/theory/strings/theory_strings_preprocess.cpp
@@ -410,6 +410,82 @@ Node StringsPreprocess::simplify( Node t, std::vector< Node > &new_nodes ) {
 
     // Thus, replace( x, y, z ) = rpw.
     retNode = rpw;
+  }
+  else if (t.getKind() == kind::STRING_STRREPLALL)
+  {
+    // processing term: replaceall( x, y, z )
+    Node x = t[0];
+    Node y = t[1];
+    Node z = t[2];
+    Node rpaw = d_sc->mkSkolemCached(t, SkolemCache::SK_PURIFY, "rpaw");
+
+    Node numOcc = d_sc->mkTypedSkolemCached(
+        nm->integerType(), x, y, SkolemCache::SK_NUM_OCCUR, "numOcc");
+    std::vector<TypeNode> argTypes;
+    argTypes.push_back(nm->integerType());
+    Node us =
+        nm->mkSkolem("Us", nm->mkFunctionType(argTypes, nm->stringType()));
+    TypeNode ufType = nm->mkFunctionType(argTypes, nm->integerType());
+    Node uf = d_sc->mkTypedSkolemCached(
+        ufType, x, y, SkolemCache::SK_OCCUR_INDEX, "Uf");
+
+    Node ufno = nm->mkNode(APPLY_UF, uf, numOcc);
+    Node usno = nm->mkNode(APPLY_UF, us, numOcc);
+    Node rem = nm->mkNode(STRING_SUBSTR, x, ufno, nm->mkNode(STRING_LENGTH, x));
+
+    std::vector<Node> lem;
+    lem.push_back(nm->mkNode(GEQ, numOcc, d_zero));
+    lem.push_back(rpaw.eqNode(nm->mkNode(APPLY_UF, us, d_zero)));
+    lem.push_back(usno.eqNode(rem));
+    lem.push_back(nm->mkNode(APPLY_UF, uf, d_zero).eqNode(d_zero));
+    lem.push_back(nm->mkNode(STRING_STRIDOF, x, y, ufno).eqNode(d_neg_one));
+
+    Node i = nm->mkBoundVar(nm->integerType());
+    Node bvli = nm->mkNode(BOUND_VAR_LIST, i);
+    Node bound =
+        nm->mkNode(AND, nm->mkNode(GEQ, i, d_zero), nm->mkNode(LT, i, numOcc));
+    Node ufi = nm->mkNode(APPLY_UF, uf, i);
+    Node ufip1 = nm->mkNode(APPLY_UF, uf, nm->mkNode(PLUS, i, d_one));
+    Node ii = nm->mkNode(STRING_STRIDOF, x, y, ufi);
+    Node cc = nm->mkNode(
+        STRING_CONCAT,
+        nm->mkNode(STRING_SUBSTR, x, ufi, nm->mkNode(MINUS, ii, ufi)),
+        z,
+        nm->mkNode(APPLY_UF, us, nm->mkNode(PLUS, i, d_one)));
+
+    std::vector<Node> flem;
+    flem.push_back(ii.eqNode(d_neg_one).negate());
+    flem.push_back(nm->mkNode(APPLY_UF, us, i).eqNode(cc));
+    flem.push_back(
+        ufip1.eqNode(nm->mkNode(PLUS, ii, nm->mkNode(STRING_LENGTH, y))));
+
+    Node q = nm->mkNode(
+        FORALL, bvli, nm->mkNode(OR, bound.negate(), nm->mkNode(AND, flem)));
+    lem.push_back(q);
+
+    // assert:
+    //   IF y=""
+    //   THEN: rpaw = x
+    //   ELSE:
+    //     numOcc >= 0 ^
+    //     rpaw = Us(0) ^ Us(numOcc) = substr(x, Uf(numOcc), len(x)) ^
+    //     Uf(0) = 0 ^ indexof( x, y, Uf(numOcc) ) = -1 ^
+    //     forall i. 0 <= i < numOcc =>
+    //        ii != -1 ^
+    //        Us( i ) = str.substr( x, Uf(i), ii - Uf(i) ) ++ z ++ Us(i+1) ^
+    //        Uf( i+1 ) = ii + len(y)
+    //        where ii == indexof( x, y, Uf(i) )
+
+    // Conceptually, numOcc is the number of occurrences of y in x, Uf( i ) is
+    // the index to begin searching in x for y after the i^th occurrence of y in
+    // x, and Us( i ) is the result of processing the remainder after processing
+    // the i^th occurrence of y in x.
+    Node assert = nm->mkNode(
+        ITE, y.eqNode(d_empty_str), rpaw.eqNode(x), nm->mkNode(AND, lem));
+    new_nodes.push_back(assert);
+
+    // Thus, replaceall( x, y, z ) = rpaw
+    retNode = rpaw;
   } else if( t.getKind() == kind::STRING_STRCTN ){
     Node x = t[0];
     Node s = t[1];
@@ -474,7 +550,7 @@ Node StringsPreprocess::simplify( Node t, std::vector< Node > &new_nodes ) {
         nm->mkNode(ITE, t[0].eqNode(t[1]), ltp, nm->mkNode(AND, conj));
     new_nodes.push_back(assert);
 
-    // Thus, str.<=( x, y ) = p_lt
+    // Thus, str.<=( x, y ) = ltp
     retNode = ltp;
   }
 
diff --git a/src/theory/strings/theory_strings_rewriter.cpp b/src/theory/strings/theory_strings_rewriter.cpp
index e94a23c87..b7821d562 100644
--- a/src/theory/strings/theory_strings_rewriter.cpp
+++ b/src/theory/strings/theory_strings_rewriter.cpp
@@ -1392,9 +1392,12 @@ RewriteResponse TheoryStringsRewriter::postRewrite(TNode node) {
   }
   else if (nk == kind::STRING_LENGTH)
   {
+    Kind nk0 = node[0].getKind();
     if( node[0].isConst() ){
       retNode = NodeManager::currentNM()->mkConst( ::CVC4::Rational( node[0].getConst<String>().size() ) );
-    }else if( node[0].getKind() == kind::STRING_CONCAT ){
+    }
+    else if (nk0 == kind::STRING_CONCAT)
+    {
       Node tmpNode = node[0];
       if(tmpNode.isConst()) {
         retNode = NodeManager::currentNM()->mkConst( ::CVC4::Rational( tmpNode.getConst<String>().size() ) );
@@ -1410,7 +1413,7 @@ RewriteResponse TheoryStringsRewriter::postRewrite(TNode node) {
         retNode = NodeManager::currentNM()->mkNode(kind::PLUS, node_vec);
       }
     }
-    else if (node[0].getKind() == STRING_STRREPL)
+    else if (nk0 == STRING_STRREPL || nk0 == STRING_STRREPLALL)
     {
       Node len1 = Rewriter::rewrite(nm->mkNode(STRING_LENGTH, node[0][1]));
       Node len2 = Rewriter::rewrite(nm->mkNode(STRING_LENGTH, node[0][2]));
@@ -1453,6 +1456,10 @@ RewriteResponse TheoryStringsRewriter::postRewrite(TNode node) {
   {
     retNode = rewriteReplace( node );
   }
+  else if (nk == kind::STRING_STRREPLALL)
+  {
+    retNode = rewriteReplaceAll(node);
+  }
   else if (nk == kind::STRING_PREFIX || nk == kind::STRING_SUFFIX)
   {
     retNode = rewritePrefixSuffix(node);
@@ -2437,16 +2444,6 @@ Node TheoryStringsRewriter::rewriteReplace( Node node ) {
   Assert(node.getKind() == kind::STRING_STRREPL);
   NodeManager* nm = NodeManager::currentNM();
 
-  if (node[1] == node[2])
-  {
-    return returnRewrite(node, node[0], "rpl-id");
-  }
-
-  if (node[0] == node[1])
-  {
-    return returnRewrite(node, node[2], "rpl-replace");
-  }
-
   if (node[1].isConst() && node[1].getConst<String>().isEmptyString())
   {
     Node ret = nm->mkNode(STRING_CONCAT, node[2], node[0]);
@@ -2497,6 +2494,14 @@ Node TheoryStringsRewriter::rewriteReplace( Node node ) {
     }
   }
 
+  // rewrites that apply to both replace and replaceall
+  Node rri = rewriteReplaceInternal(node);
+  if (!rri.isNull())
+  {
+    // printing of the rewrite managed by the call above
+    return rri;
+  }
+
   if (node[0] == node[2])
   {
     // ( len( y )>=len(x) ) => str.replace( x, y, x ) ---> x
@@ -2938,6 +2943,78 @@ Node TheoryStringsRewriter::rewriteReplace( Node node ) {
   return node;
 }
 
+Node TheoryStringsRewriter::rewriteReplaceAll(Node node)
+{
+  Assert(node.getKind() == STRING_STRREPLALL);
+  NodeManager* nm = NodeManager::currentNM();
+
+  if (node[0].isConst() && node[1].isConst())
+  {
+    std::vector<Node> children;
+    String s = node[0].getConst<String>();
+    String t = node[1].getConst<String>();
+    if (s.isEmptyString() || t.isEmptyString())
+    {
+      return returnRewrite(node, node[0], "replall-empty-find");
+    }
+    std::size_t index = 0;
+    std::size_t curr = 0;
+    do
+    {
+      curr = s.find(t, index);
+      if (curr != std::string::npos)
+      {
+        if (curr > index)
+        {
+          children.push_back(nm->mkConst(s.substr(index, curr - index)));
+        }
+        children.push_back(node[2]);
+        index = curr + t.size();
+      }
+      else
+      {
+        children.push_back(nm->mkConst(s.substr(index, s.size() - index)));
+      }
+    } while (curr != std::string::npos && curr < s.size());
+    // constant evaluation
+    Node res = mkConcat(STRING_CONCAT, children);
+    return returnRewrite(node, res, "replall-const");
+  }
+
+  // rewrites that apply to both replace and replaceall
+  Node rri = rewriteReplaceInternal(node);
+  if (!rri.isNull())
+  {
+    // printing of the rewrite managed by the call above
+    return rri;
+  }
+
+  Trace("strings-rewrite-nf") << "No rewrites for : " << node << std::endl;
+  return node;
+}
+
+Node TheoryStringsRewriter::rewriteReplaceInternal(Node node)
+{
+  Kind nk = node.getKind();
+  Assert(nk == STRING_STRREPL || nk == STRING_STRREPLALL);
+
+  if (node[1] == node[2])
+  {
+    return returnRewrite(node, node[0], "rpl-id");
+  }
+
+  if (node[0] == node[1])
+  {
+    // only holds for replaceall if non-empty
+    if (nk == STRING_STRREPL || checkEntailNonEmpty(node[1]))
+    {
+      return returnRewrite(node, node[2], "rpl-replace");
+    }
+  }
+
+  return Node::null();
+}
+
 Node TheoryStringsRewriter::rewriteStringLeq(Node n)
 {
   Assert(n.getKind() == kind::STRING_LEQ);
diff --git a/src/theory/strings/theory_strings_rewriter.h b/src/theory/strings/theory_strings_rewriter.h
index 2e356f8f7..69d6ff68e 100644
--- a/src/theory/strings/theory_strings_rewriter.h
+++ b/src/theory/strings/theory_strings_rewriter.h
@@ -187,6 +187,18 @@ class TheoryStringsRewriter {
   * Returns the rewritten form of node.
   */
   static Node rewriteReplace(Node node);
+  /** rewrite replace all
+   * This is the entry point for post-rewriting terms n of the form
+   *   str.replaceall( s, t, r )
+   * Returns the rewritten form of node.
+   */
+  static Node rewriteReplaceAll(Node node);
+  /** rewrite replace internal
+   *
+   * This method implements rewrite rules that apply to both str.replace and
+   * str.replaceall. If it returns a non-null ret, then node rewrites to ret.
+   */
+  static Node rewriteReplaceInternal(Node node);
   /** rewrite string less than or equal
   * This is the entry point for post-rewriting terms n of the form
   *   str.<=( t, s )
diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt
index 6736d712b..a1d5a35aa 100644
--- a/test/regress/CMakeLists.txt
+++ b/test/regress/CMakeLists.txt
@@ -825,6 +825,7 @@ set(regress_0_tests
   regress0/strings/norn-31.smt2
   regress0/strings/norn-simp-rew.smt2
   regress0/strings/repl-rewrites2.smt2
+  regress0/strings/replaceall-eval.smt2
   regress0/strings/rewrites-re-concat.smt2
   regress0/strings/rewrites-v2.smt2
   regress0/strings/std2.6.1.smt2
@@ -1544,6 +1545,8 @@ set(regress_1_tests
   regress1/strings/reloop.smt2
   regress1/strings/repl-empty-sem.smt2
   regress1/strings/repl-soundness-sem.smt2
+  regress1/strings/replaceall-len.smt2
+  regress1/strings/replaceall-replace.smt2
   regress1/strings/rew-020618.smt2
   regress1/strings/stoi-400million.smt2
   regress1/strings/str-code-sat.smt2
@@ -1729,6 +1732,8 @@ set(regress_2_tests
   regress2/strings/non_termination_regular_expression6.smt2
   regress2/strings/norn-dis-0707-3.smt2
   regress2/strings/repl-repl.smt2
+  regress2/strings/replaceall-diffrange.smt2
+  regress2/strings/replaceall-len-c.smt2
   regress2/sygus/MPwL_d1s3.sy
   regress2/sygus/array_sum_dd.sy
   regress2/sygus/cegisunif-depth1-bv.sy
diff --git a/test/regress/regress0/strings/replaceall-eval.smt2 b/test/regress/regress0/strings/replaceall-eval.smt2
new file mode 100644
index 000000000..924515901
--- /dev/null
+++ b/test/regress/regress0/strings/replaceall-eval.smt2
@@ -0,0 +1,10 @@
+(set-info :smt-lib-version 2.5)
+(set-logic ALL)
+(set-info :status sat)
+(declare-fun x () String)
+(declare-fun y () String)
+
+(assert (= x (str.replaceall "AABAABBC" "B" "def")))
+(assert (= y (str.replaceall "AABAABBC" "AB" "BA")))
+
+(check-sat)
diff --git a/test/regress/regress1/strings/replaceall-len.smt2 b/test/regress/regress1/strings/replaceall-len.smt2
new file mode 100644
index 000000000..448d8e98f
--- /dev/null
+++ b/test/regress/regress1/strings/replaceall-len.smt2
@@ -0,0 +1,10 @@
+(set-info :smt-lib-version 2.5)
+(set-logic ALL)
+(set-info :status sat)
+(set-option :strings-exp true)
+(set-option :strings-fmf true)
+(set-option :produce-models true)
+(declare-fun x () String)
+(assert (= (str.len (str.replaceall x "B" "CC")) (+ (str.len x) 2)))
+(assert (> (str.len x) 2))
+(check-sat)
diff --git a/test/regress/regress1/strings/replaceall-replace.smt2 b/test/regress/regress1/strings/replaceall-replace.smt2
new file mode 100644
index 000000000..5bf5b5b16
--- /dev/null
+++ b/test/regress/regress1/strings/replaceall-replace.smt2
@@ -0,0 +1,13 @@
+(set-info :smt-lib-version 2.5)
+(set-logic ALL)
+(set-info :status sat)
+(set-option :strings-exp true)
+(set-option :strings-fmf true)
+(set-option :produce-models true)
+(declare-fun x () String)
+(declare-fun y () String)
+(declare-fun z () String)
+(assert (not (= x "")))
+(assert (not (= y "")))
+(assert (not (= (str.replace x y z) (str.replaceall x y z))))
+(check-sat)
diff --git a/test/regress/regress2/strings/replaceall-diffrange.smt2 b/test/regress/regress2/strings/replaceall-diffrange.smt2
new file mode 100644
index 000000000..5d1ef57bf
--- /dev/null
+++ b/test/regress/regress2/strings/replaceall-diffrange.smt2
@@ -0,0 +1,11 @@
+(set-info :smt-lib-version 2.5)
+(set-logic ALL)
+(set-info :status sat)
+(set-option :strings-exp true)
+(set-option :strings-fmf true)
+(declare-fun x () String)
+(declare-fun y () String)
+(declare-fun z () String)
+(declare-fun w () String)
+(assert (= (str.len (str.replaceall x y z)) (+ (str.len (str.replaceall x y w)) 3)))
+(check-sat)
diff --git a/test/regress/regress2/strings/replaceall-len-c.smt2 b/test/regress/regress2/strings/replaceall-len-c.smt2
new file mode 100644
index 000000000..336ec10e4
--- /dev/null
+++ b/test/regress/regress2/strings/replaceall-len-c.smt2
@@ -0,0 +1,8 @@
+(set-info :smt-lib-version 2.5)
+(set-logic ALL)
+(set-info :status sat)
+(set-option :strings-exp true)
+(set-option :strings-fmf true)
+(declare-fun x () String)
+(assert (= (str.len (str.replaceall "ABBABAAB" x "C")) 5))
+(check-sat)