From 801d53f9e048e6e4906ec098e076e256820eccc8 Mon Sep 17 00:00:00 2001
From: Andres Noetzli <andres.noetzli@gmail.com>
Date: Wed, 4 Jul 2018 19:32:29 -0700
Subject: [PATCH] sygusComp2018: Improve string rewriter (#2141)

---
 .../strings/theory_strings_rewriter.cpp       | 423 +++++++++++++++++-
 src/theory/strings/theory_strings_rewriter.h  |  16 +
 .../theory/theory_strings_rewriter_white.h    | 243 ++++++++++
 3 files changed, 673 insertions(+), 9 deletions(-)

diff --git a/src/theory/strings/theory_strings_rewriter.cpp b/src/theory/strings/theory_strings_rewriter.cpp
index 66514fde2..cd7c6eeb4 100644
--- a/src/theory/strings/theory_strings_rewriter.cpp
+++ b/src/theory/strings/theory_strings_rewriter.cpp
@@ -19,10 +19,13 @@
 #include <stdint.h>
 #include <algorithm>
 
+#include "expr/node_builder.h"
 #include "options/strings_options.h"
 #include "smt/logic_exception.h"
 #include "theory/arith/arith_msum.h"
 #include "theory/theory.h"
+#include "util/integer.h"
+#include "util/rational.h"
 
 using namespace std;
 using namespace CVC4;
@@ -864,12 +867,15 @@ RewriteResponse TheoryStringsRewriter::postRewrite(TNode node) {
         }
         retNode = NodeManager::currentNM()->mkNode(kind::PLUS, node_vec);
       }
-    }else if( node[0].getKind()==kind::STRING_STRREPL ){
-      if( node[0][1].isConst() && node[0][2].isConst() ){
-        // TODO (#1180) length entailment here
-        if( node[0][1].getConst<String>().size()==node[0][2].getConst<String>().size() ){
-          retNode = NodeManager::currentNM()->mkNode( kind::STRING_LENGTH, node[0][0] );
-        }
+    }
+    else if (node[0].getKind() == STRING_STRREPL)
+    {
+      Node len1 = Rewriter::rewrite(nm->mkNode(STRING_LENGTH, node[0][1]));
+      Node len2 = Rewriter::rewrite(nm->mkNode(STRING_LENGTH, node[0][2]));
+      if (len1 == len2)
+      {
+        // len( y ) == len( z ) => len( str.replace( x, y, z ) ) ---> len( x )
+        retNode = nm->mkNode(STRING_LENGTH, node[0][0]);
       }
     }
   }else if( node.getKind() == kind::STRING_CHARAT ){
@@ -1295,6 +1301,8 @@ Node TheoryStringsRewriter::rewriteSubstr(Node node)
 
 Node TheoryStringsRewriter::rewriteContains( Node node ) {
   Assert(node.getKind() == kind::STRING_STRCTN);
+  NodeManager* nm = NodeManager::currentNM();
+
   if( node[0] == node[1] ){
     Node ret = NodeManager::currentNM()->mkConst(true);
     return returnRewrite(node, ret, "ctn-eq");
@@ -1321,9 +1329,6 @@ Node TheoryStringsRewriter::rewriteContains( Node node ) {
           Node ret = NodeManager::currentNM()->mkConst(false);
           return returnRewrite(node, ret, "ctn-lhs-emptystr");
         }
-        // contains( "", x ) ---> ( "" = x )
-        Node ret = node[0].eqNode(node[1]);
-        return returnRewrite(node, ret, "ctn-lhs-emptystr-eq");
       }
       else if (node[1].getKind() == kind::STRING_CONCAT)
       {
@@ -1370,6 +1375,34 @@ Node TheoryStringsRewriter::rewriteContains( Node node ) {
     return returnRewrite(node, ret, "ctn-strip-endpt");
   }
 
+  for (const Node& n : nc2)
+  {
+    if (n.getKind() == kind::STRING_STRREPL)
+    {
+      // (str.contains x (str.replace y z w)) --> false
+      // if (str.contains x y) = false and (str.contains x w) = false
+      //
+      // Reasoning: (str.contains x y) checks that x does not contain y if the
+      // replacement does not change y. (str.contains x w) checks that if the
+      // replacement changes anything in y, the w makes it impossible for it to
+      // occur in x.
+      Node ctnUnchanged = nm->mkNode(kind::STRING_STRCTN, node[0], n[0]);
+      Node ctnUnchangedR = Rewriter::rewrite(ctnUnchanged);
+
+      if (ctnUnchangedR.isConst() && !ctnUnchangedR.getConst<bool>())
+      {
+        Node ctnChange = nm->mkNode(kind::STRING_STRCTN, node[0], n[2]);
+        Node ctnChangeR = Rewriter::rewrite(ctnChange);
+
+        if (ctnChangeR.isConst() && !ctnChangeR.getConst<bool>())
+        {
+          Node res = nm->mkConst(false);
+          return returnRewrite(node, res, "ctn-rpl-non-ctn");
+        }
+      }
+    }
+  }
+
   // length entailment
   Node len_n1 = NodeManager::currentNM()->mkNode(kind::STRING_LENGTH, node[0]);
   Node len_n2 = NodeManager::currentNM()->mkNode(kind::STRING_LENGTH, node[1]);
@@ -1438,6 +1471,7 @@ Node TheoryStringsRewriter::rewriteContains( Node node ) {
       }
     }
     Trace("strings-rewrite-multiset") << "For " << node << " : " << std::endl;
+    bool sameConst = true;
     for (const Node& ch : chars)
     {
       Trace("strings-rewrite-multiset") << "  # occurrences of substring ";
@@ -1449,7 +1483,66 @@ Node TheoryStringsRewriter::rewriteContains( Node node ) {
         Node ret = NodeManager::currentNM()->mkConst(false);
         return returnRewrite(node, ret, "ctn-mset-nss");
       }
+      else if (count_const[0][ch] > count_const[1][ch])
+      {
+        sameConst = false;
+      }
+    }
+
+    if (sameConst)
+    {
+      // At this point, we know that both the first and the second argument
+      // both contain the same constants. Now we can check if there are
+      // non-const components that appear in the second argument but not the
+      // first. If there are, we know that the str.contains is true iff those
+      // components are empty, so we can pull them out of the str.contains. For
+      // example:
+      //
+      // (str.contains (str.++ "A" x) (str.++ y x "A")) -->
+      //   (and (str.contains (str.++ "A" x) (str.++ x "A")) (= y ""))
+      //
+      // These equalities can be used by other rewrites for subtitutions.
+
+      // Find all non-const components that appear more times in second
+      // argument than the first
+      std::unordered_set<Node, NodeHashFunction> nConstEmpty;
+      for (std::pair<const Node, unsigned>& nncp : num_nconst[1])
+      {
+        if (nncp.second > num_nconst[0][nncp.first])
+        {
+          nConstEmpty.insert(nncp.first);
+        }
+      }
+
+      // Check if there are any non-const components that must be empty
+      if (nConstEmpty.size() > 0)
+      {
+        // Generate str.contains of the (potentially) non-empty parts
+        std::vector<Node> cs;
+        std::vector<Node> nnc2;
+        for (const Node& n : nc2)
+        {
+          if (nConstEmpty.find(n) == nConstEmpty.end())
+          {
+            nnc2.push_back(n);
+          }
+        }
+        cs.push_back(nm->mkNode(
+            kind::STRING_STRCTN, node[0], mkConcat(kind::STRING_CONCAT, nnc2)));
+
+        // Generate equalities for the parts that must be empty
+        Node emptyStr = nm->mkConst(String(""));
+        for (const Node& n : nConstEmpty)
+        {
+          cs.push_back(nm->mkNode(kind::EQUAL, n, emptyStr));
+        }
+
+        Assert(cs.size() >= 2);
+        Node res = nm->mkNode(kind::AND, cs);
+        return returnRewrite(node, res, "ctn-mset-substs");
+      }
     }
+
     // TODO (#1180): count the number of 2,3,4,.. character substrings
     // for example:
     // str.contains( str.++( x, "cbabc" ), str.++( "cabbc", x ) ) ---> false
@@ -1457,6 +1550,7 @@ Node TheoryStringsRewriter::rewriteContains( Node node ) {
     // note this is orthogonal reasoning to inductive reasoning
     // via regular membership reduction in Liang et al CAV 2015.
   }
+
   // TODO (#1180): abstract interpretation with multi-set domain
   // to show first argument is a strict subset of second argument
 
@@ -1666,6 +1760,31 @@ Node TheoryStringsRewriter::rewriteIndexof( Node node ) {
       return returnRewrite(node, negone, "idof-nctn");
     }
   }
+  else
+  {
+    Node new_len = node[2];
+    std::vector<Node> nr;
+    if (stripSymbolicLength(children0, nr, 1, new_len))
+    {
+      // Normalize the string before the start index.
+      //
+      // For example:
+      // str.indexof(str.++("ABCD", x), y, 3) --->
+      // str.indexof(str.++("AAAD", x), y, 3)
+      Node nodeNr = mkConcat(kind::STRING_CONCAT, nr);
+      Node normNr = lengthPreserveRewrite(nodeNr);
+      if (normNr != nodeNr)
+      {
+        std::vector<Node> normNrChildren;
+        getConcat(normNr, normNrChildren);
+        std::vector<Node> children(normNrChildren);
+        children.insert(children.end(), children0.begin(), children0.end());
+        Node nn = mkConcat(kind::STRING_CONCAT, children);
+        Node res = nm->mkNode(kind::STRING_STRIDOF, nn, node[1], node[2]);
+        return returnRewrite(node, res, "idof-norm-prefix");
+      }
+    }
+  }
 
   if (node[2].isConst() && node[2].getConst<Rational>().sgn()==0)
   {
@@ -1814,6 +1933,64 @@ Node TheoryStringsRewriter::rewriteReplace( Node node ) {
       return returnRewrite(node, node[0], "rpl-nctn");
     }
   }
+  else if (cmp_conr.getKind() == kind::EQUAL || cmp_conr.getKind() == kind::AND)
+  {
+    // Rewriting the str.contains may return equalities of the form (= x "").
+    // In that case, we can substitute the variables appearing in those
+    // equalities with the empty string in the third argument of the
+    // str.replace. For example:
+    //
+    // (str.replace x (str.++ x y) y) --> (str.replace x (str.++ x y) "")
+    //
+    // This can be done because str.replace changes x iff (str.++ x y) is in x
+    // but that means that y must be empty in that case. Thus, we can
+    // substitute y with "" in the third argument. Note that the third argument
+    // does not matter when the str.replace does not apply.
+    //
+    Node empty = nm->mkConst(::CVC4::String(""));
+
+    // Collect the equalities of the form (= x "")
+    std::set<TNode> emptyNodes;
+    if (cmp_conr.getKind() == kind::EQUAL)
+    {
+      if (cmp_conr[0] == empty)
+      {
+        emptyNodes.insert(cmp_conr[1]);
+      }
+      else if (cmp_conr[1] == empty)
+      {
+        emptyNodes.insert(cmp_conr[0]);
+      }
+    }
+    else
+    {
+      for (const Node& c : cmp_conr)
+      {
+        if (c[0] == empty)
+        {
+          emptyNodes.insert(c[1]);
+        }
+        else if (c[1] == empty)
+        {
+          emptyNodes.insert(c[0]);
+        }
+      }
+    }
+
+    if (emptyNodes.size() > 0)
+    {
+      // Perform the substitutions
+      std::vector<TNode> substs(emptyNodes.size(), TNode(empty));
+      Node nn2 = node[2].substitute(
+          emptyNodes.begin(), emptyNodes.end(), substs.begin(), substs.end());
+
+      if (nn2 != node[2])
+      {
+        Node res = nm->mkNode(kind::STRING_STRREPL, node[0], node[1], nn2);
+        return returnRewrite(node, res, "rpl-cnts-substs");
+      }
+    }
+  }
 
   if (cmp_conr != cmp_con)
   {
@@ -1841,6 +2018,170 @@ Node TheoryStringsRewriter::rewriteReplace( Node node ) {
     }
   }
 
+  children1.clear();
+  getConcat(node[1], children1);
+  Node lastChild1 = children1[children1.size() - 1];
+  if (lastChild1.getKind() == kind::STRING_SUBSTR)
+  {
+    // (str.replace x (str.++ t (str.substr y i j)) z) --->
+    // (str.replace x (str.++ t
+    //                  (str.substr y i (+ (str.len x) 1 (- (str.len t))))) z)
+    // if j > len(x)
+    //
+    // Reasoning: If the string to be replaced is longer than x, then it does
+    // not matter how much longer it is, the result is always x. Thus, it is
+    // fine to only look at the prefix of length len(x) + 1 - len(t).
+
+    children1.pop_back();
+    // Length of the non-substr components in the second argument
+    Node partLen1 = nm->mkNode(kind::STRING_LENGTH,
+                               mkConcat(kind::STRING_CONCAT, children1));
+    Node maxLen1 = nm->mkNode(kind::PLUS, partLen1, lastChild1[2]);
+
+    Node zero = nm->mkConst(Rational(0));
+    Node one = nm->mkConst(Rational(1));
+    Node len0 = nm->mkNode(kind::STRING_LENGTH, node[0]);
+    Node len0_1 = nm->mkNode(kind::PLUS, len0, one);
+    // Check len(t) + j > len(x) + 1
+    if (checkEntailArith(maxLen1, len0_1, true))
+    {
+      children1.push_back(nm->mkNode(
+          kind::STRING_SUBSTR,
+          lastChild1[0],
+          lastChild1[1],
+          nm->mkNode(
+              kind::PLUS, len0, one, nm->mkNode(kind::UMINUS, partLen1))));
+      Node res = nm->mkNode(kind::STRING_STRREPL,
+                            node[0],
+                            mkConcat(kind::STRING_CONCAT, children1),
+                            node[2]);
+      return returnRewrite(node, res, "repl-subst-idx");
+    }
+  }
+  if (node[1].getKind() == STRING_STRREPL)
+  {
+    if (node[1][0] == node[0])
+    {
+      if (node[1][0] == node[1][2] && node[1][0] == node[2])
+      {
+        // str.replace( x, str.replace( x, y, x ), x ) ---> x
+        return returnRewrite(node, node[0], "repl-repl2-inv-id");
+      }
+      bool dualReplIteSuccess = false;
+      Node cmp_con = nm->mkNode(STRING_STRCTN, node[1][0], node[1][2]);
+      cmp_con = Rewriter::rewrite(cmp_con);
+      if (cmp_con.isConst() && !cmp_con.getConst<bool>())
+      {
+        // str.contains( x, z ) ---> false
+        //   implies
+        // str.replace( x, str.replace( x, y, z ), w ) --->
+        // ite( str.contains( x, y ), x, w )
+        dualReplIteSuccess = true;
+      }
+      else
+      {
+        // str.contains( y, z ) ---> false and str.contains( z, y ) ---> false
+        //   implies
+        // str.replace( x, str.replace( x, y, z ), w ) --->
+        // ite( str.contains( x, y ), x, w )
+        cmp_con = nm->mkNode(STRING_STRCTN, node[1][1], node[1][2]);
+        cmp_con = Rewriter::rewrite(cmp_con);
+        if (cmp_con.isConst() && !cmp_con.getConst<bool>())
+        {
+          cmp_con = nm->mkNode(STRING_STRCTN, node[1][2], node[1][1]);
+          cmp_con = Rewriter::rewrite(cmp_con);
+          if (cmp_con.isConst() && !cmp_con.getConst<bool>())
+          {
+            dualReplIteSuccess = true;
+          }
+        }
+      }
+      if (dualReplIteSuccess)
+      {
+        Node res = nm->mkNode(ITE,
+                              nm->mkNode(STRING_STRCTN, node[0], node[1][1]),
+                              node[0],
+                              node[2]);
+        return returnRewrite(node, res, "repl-dual-repl-ite");
+      }
+    }
+
+    bool invSuccess = false;
+    if (node[1][1] == node[0])
+    {
+      if (node[1][0] == node[1][2])
+      {
+        // str.replace(x, str.replace(y, x, y), w) ---> str.replace(x, y, w)
+        invSuccess = true;
+      }
+      else if (node[1][1] == node[2] || node[1][0] == node[2])
+      {
+        // str.contains(y, z) ----> false and ( y == w or x == w ) implies
+        //   implies
+        // str.replace(x, str.replace(y, x, z), w) ---> str.replace(x, y, w)
+        Node cmp_con = nm->mkNode(STRING_STRCTN, node[1][0], node[1][2]);
+        cmp_con = Rewriter::rewrite(cmp_con);
+        invSuccess = cmp_con.isConst() && !cmp_con.getConst<bool>();
+      }
+    }
+    else
+    {
+      // str.contains(x, z) ----> false and str.contains(x, w) ----> false
+      //   implies
+      // str.replace(x, str.replace(y, z, w), u) ---> str.replace(x, y, u)
+      Node cmp_con = nm->mkNode(STRING_STRCTN, node[0], node[1][1]);
+      cmp_con = Rewriter::rewrite(cmp_con);
+      if (cmp_con.isConst() && !cmp_con.getConst<bool>())
+      {
+        cmp_con = nm->mkNode(STRING_STRCTN, node[0], node[1][2]);
+        cmp_con = Rewriter::rewrite(cmp_con);
+        invSuccess = cmp_con.isConst() && !cmp_con.getConst<bool>();
+      }
+    }
+    if (invSuccess)
+    {
+      Node res = nm->mkNode(kind::STRING_STRREPL, node[0], node[1][0], node[2]);
+      return returnRewrite(node, res, "repl-repl2-inv");
+    }
+  }
+  if (node[2].getKind() == STRING_STRREPL)
+  {
+    if (node[2][1] == node[0])
+    {
+      // str.contains( z, w ) ----> false implies
+      // str.replace( x, w, str.replace( z, x, y ) ) ---> str.replace( x, w, z )
+      Node cmp_con = nm->mkNode(STRING_STRCTN, node[1], node[2][0]);
+      cmp_con = Rewriter::rewrite(cmp_con);
+      if (cmp_con.isConst() && !cmp_con.getConst<bool>())
+      {
+        Node res =
+            nm->mkNode(kind::STRING_STRREPL, node[0], node[1], node[2][0]);
+        return returnRewrite(node, res, "repl-repl3-inv");
+      }
+    }
+    if (node[2][0] == node[1])
+    {
+      bool success = false;
+      if (node[2][0] == node[2][2] && node[2][1] == node[0])
+      {
+        // str.replace( x, y, str.replace( y, x, y ) ) ---> x
+        success = true;
+      }
+      else
+      {
+        // str.contains( x, z ) ----> false implies
+        // str.replace( x, y, str.replace( y, z, w ) ) ---> x
+        cmp_con = nm->mkNode(STRING_STRCTN, node[0], node[2][1]);
+        cmp_con = Rewriter::rewrite(cmp_con);
+        success = cmp_con.isConst() && !cmp_con.getConst<bool>();
+      }
+      if (success)
+      {
+        return returnRewrite(node, node[0], "repl-repl3-inv-id");
+      }
+    }
+  }
+
   // TODO (#1180) incorporate these?
   // contains( t, s ) =>
   //   replace( replace( x, t, s ), s, r ) ----> replace( x, t, r )
@@ -2686,6 +3027,70 @@ bool TheoryStringsRewriter::stripConstantEndpoints(std::vector<Node>& n1,
   return changed;
 }
 
+Node TheoryStringsRewriter::canonicalStrForSymbolicLength(Node len)
+{
+  NodeManager* nm = NodeManager::currentNM();
+
+  Node res;
+  if (len.getKind() == kind::CONST_RATIONAL)
+  {
+    // c -> "A" repeated c times
+    Rational ratLen = len.getConst<Rational>();
+    Assert(ratLen.getDenominator() == 1);
+    Integer intLen = ratLen.getNumerator();
+    res = nm->mkConst(String(std::string(intLen.getUnsignedInt(), 'A')));
+  }
+  else if (len.getKind() == kind::PLUS)
+  {
+    // x + y -> norm(x) + norm(y)
+    NodeBuilder<> concatBuilder(kind::STRING_CONCAT);
+    for (const auto& n : len)
+    {
+      Node sn = canonicalStrForSymbolicLength(n);
+      if (sn.isNull())
+      {
+        return Node::null();
+      }
+      std::vector<Node> snChildren;
+      getConcat(sn, snChildren);
+      concatBuilder.append(snChildren);
+    }
+    res = concatBuilder.constructNode();
+  }
+  else if (len.getKind() == kind::MULT && len.getNumChildren() == 2
+           && len[0].isConst())
+  {
+    // c * x -> norm(x) repeated c times
+    Rational ratReps = len[0].getConst<Rational>();
+    Assert(ratReps.getDenominator() == 1);
+    Integer intReps = ratReps.getNumerator();
+
+    Node nRep = canonicalStrForSymbolicLength(len[1]);
+    std::vector<Node> nRepChildren;
+    getConcat(nRep, nRepChildren);
+    NodeBuilder<> concatBuilder(kind::STRING_CONCAT);
+    for (size_t i = 0, reps = intReps.getUnsignedInt(); i < reps; i++)
+    {
+      concatBuilder.append(nRepChildren);
+    }
+    res = concatBuilder.constructNode();
+  }
+  else if (len.getKind() == kind::STRING_LENGTH)
+  {
+    // len(x) -> x
+    res = len[0];
+  }
+  return res;
+}
+
+Node TheoryStringsRewriter::lengthPreserveRewrite(Node n)
+{
+  NodeManager* nm = NodeManager::currentNM();
+  Node len = Rewriter::rewrite(nm->mkNode(kind::STRING_LENGTH, n));
+  Node res = canonicalStrForSymbolicLength(len);
+  return res.isNull() ? n : res;
+}
+
 bool TheoryStringsRewriter::checkEntailNonEmpty(Node a)
 {
   Node len = NodeManager::currentNM()->mkNode(STRING_LENGTH, a);
diff --git a/src/theory/strings/theory_strings_rewriter.h b/src/theory/strings/theory_strings_rewriter.h
index 616e31017..732d64095 100644
--- a/src/theory/strings/theory_strings_rewriter.h
+++ b/src/theory/strings/theory_strings_rewriter.h
@@ -373,6 +373,22 @@ class TheoryStringsRewriter {
                                      std::vector<Node>& nb,
                                      std::vector<Node>& ne,
                                      int dir = 0);
+
+  /**
+   * Given a symbolic length n, returns the canonical string for that length.
+   * For example if n is constant, this function returns a string consisting of
+   * "A" repeated n times. Returns the null node if no such string exists.
+   */
+  static Node canonicalStrForSymbolicLength(Node n);
+
+  /** length preserving rewrite
+   *
+   * Given input n, this returns a string n' whose length is equivalent to n.
+   * We apply certain normalizations to n', such as replacing all constants
+   * that are not relevant to length by "A".
+   */
+  static Node lengthPreserveRewrite(Node n);
+
   /** entail non-empty
    *
    * Checks whether string a is entailed to be non-empty. Is equivalent to
diff --git a/test/unit/theory/theory_strings_rewriter_white.h b/test/unit/theory/theory_strings_rewriter_white.h
index 29a9ff9c4..fc073b5a4 100644
--- a/test/unit/theory/theory_strings_rewriter_white.h
+++ b/test/unit/theory/theory_strings_rewriter_white.h
@@ -245,4 +245,247 @@ class TheoryStringsRewriterWhite : public CxxTest::TestSuite
     Node res_a_repl_substr = Rewriter::rewrite(a_repl_substr);
     TS_ASSERT_EQUALS(res_repl_substr_a, res_a_repl_substr);
   }
+
+  void testLengthPreserveRewrite()
+  {
+    TypeNode intType = d_nm->integerType();
+    TypeNode strType = d_nm->stringType();
+
+    Node empty = d_nm->mkConst(::CVC4::String(""));
+    Node abcd = d_nm->mkConst(::CVC4::String("ABCD"));
+    Node f = d_nm->mkConst(::CVC4::String("F"));
+    Node gh = d_nm->mkConst(::CVC4::String("GH"));
+    Node ij = d_nm->mkConst(::CVC4::String("IJ"));
+
+    Node i = d_nm->mkVar("i", intType);
+    Node s = d_nm->mkVar("s", strType);
+    Node x = d_nm->mkVar("x", strType);
+    Node y = d_nm->mkVar("y", strType);
+
+    // Same length preserving rewrite for:
+    //
+    // (str.++ "ABCD" (str.++ x x))
+    //
+    // (str.++ "GH" (str.repl "GH" "IJ") "IJ")
+    Node concat1 = d_nm->mkNode(
+        kind::STRING_CONCAT, abcd, d_nm->mkNode(kind::STRING_CONCAT, x, x));
+    Node concat2 = d_nm->mkNode(kind::STRING_CONCAT,
+                                gh,
+                                x,
+                                d_nm->mkNode(kind::STRING_STRREPL, x, gh, ij),
+                                ij);
+    Node res_concat1 = TheoryStringsRewriter::lengthPreserveRewrite(concat1);
+    Node res_concat2 = TheoryStringsRewriter::lengthPreserveRewrite(concat2);
+    TS_ASSERT_EQUALS(res_concat1, res_concat2);
+  }
+
+  void testRewriteIndexOf()
+  {
+    TypeNode strType = d_nm->stringType();
+
+    Node a = d_nm->mkConst(::CVC4::String("A"));
+    Node abcd = d_nm->mkConst(::CVC4::String("ABCD"));
+    Node aaad = d_nm->mkConst(::CVC4::String("AAAD"));
+    Node b = d_nm->mkConst(::CVC4::String("B"));
+    Node x = d_nm->mkVar("x", strType);
+    Node y = d_nm->mkVar("y", strType);
+    Node one = d_nm->mkConst(Rational(2));
+    Node three = d_nm->mkConst(Rational(3));
+
+    // Same normal form for:
+    //
+    // (str.to.int (str.indexof "A" x 1))
+    //
+    // (str.to.int (str.indexof "B" x 1))
+    Node a_idof_x = d_nm->mkNode(kind::STRING_STRIDOF, a, x, one);
+    Node itos_a_idof_x = d_nm->mkNode(kind::STRING_ITOS, a_idof_x);
+    Node b_idof_x = d_nm->mkNode(kind::STRING_STRIDOF, b, x, one);
+    Node itos_b_idof_x = d_nm->mkNode(kind::STRING_ITOS, b_idof_x);
+    Node res_itos_a_idof_x = Rewriter::rewrite(itos_a_idof_x);
+    Node res_itos_b_idof_x = Rewriter::rewrite(itos_b_idof_x);
+    TS_ASSERT_EQUALS(res_itos_a_idof_x, res_itos_b_idof_x);
+
+    // Same normal form for:
+    //
+    // (str.indexof (str.++ "ABCD" x) y 3)
+    //
+    // (str.indexof (str.++ "AAAD" x) y 3)
+    Node idof_abcd = d_nm->mkNode(kind::STRING_STRIDOF,
+                                  d_nm->mkNode(kind::STRING_CONCAT, abcd, x),
+                                  y,
+                                  three);
+    Node idof_aaad = d_nm->mkNode(kind::STRING_STRIDOF,
+                                  d_nm->mkNode(kind::STRING_CONCAT, aaad, x),
+                                  y,
+                                  three);
+    Node res_idof_abcd = Rewriter::rewrite(idof_abcd);
+    Node res_idof_aaad = Rewriter::rewrite(idof_aaad);
+    TS_ASSERT_EQUALS(res_idof_abcd, res_idof_aaad);
+  }
+
+  void testRewriteReplace()
+  {
+    TypeNode strType = d_nm->stringType();
+
+    Node empty = d_nm->mkConst(::CVC4::String(""));
+    Node a = d_nm->mkConst(::CVC4::String("A"));
+    Node b = d_nm->mkConst(::CVC4::String("B"));
+    Node c = d_nm->mkConst(::CVC4::String("C"));
+    Node d = d_nm->mkConst(::CVC4::String("D"));
+    Node x = d_nm->mkVar("x", strType);
+    Node y = d_nm->mkVar("y", strType);
+    Node z = d_nm->mkVar("z", strType);
+
+    // (str.replace "A" (str.replace "B", x, "C") "D") --> "A"
+    Node repl_repl = d_nm->mkNode(kind::STRING_STRREPL,
+                                  a,
+                                  d_nm->mkNode(kind::STRING_STRREPL, b, x, c),
+                                  d);
+    Node res_repl_repl = Rewriter::rewrite(repl_repl);
+    TS_ASSERT_EQUALS(res_repl_repl, a);
+
+    // (str.replace "A" (str.replace "B", x, "A") "D") -/-> "A"
+    repl_repl = d_nm->mkNode(kind::STRING_STRREPL,
+                             a,
+                             d_nm->mkNode(kind::STRING_STRREPL, b, x, a),
+                             d);
+    res_repl_repl = Rewriter::rewrite(repl_repl);
+    TS_ASSERT_DIFFERS(res_repl_repl, a);
+
+    // Same normal form for:
+    //
+    // (str.replace x (str.++ x y z) y)
+    //
+    // (str.replace x (str.++ x y z) z)
+    Node xyz = d_nm->mkNode(kind::STRING_CONCAT, x, y, z);
+    Node repl_x_xyz = d_nm->mkNode(kind::STRING_STRREPL, x, xyz, y);
+    Node repl_x_zyx = d_nm->mkNode(kind::STRING_STRREPL, x, xyz, z);
+    Node res_repl_x_xyz = Rewriter::rewrite(repl_x_xyz);
+    Node res_repl_x_zyx = Rewriter::rewrite(repl_x_zyx);
+    TS_ASSERT_EQUALS(res_repl_x_xyz, res_repl_x_zyx);
+
+    // (str.replace "" (str.++ x x) x) --> ""
+    Node repl_empty_xx = d_nm->mkNode(kind::STRING_STRREPL,
+                                      empty,
+                                      d_nm->mkNode(kind::STRING_CONCAT, x, x),
+                                      x);
+    Node res_repl_empty_xx = Rewriter::rewrite(repl_empty_xx);
+    TS_ASSERT_EQUALS(res_repl_empty_xx, empty);
+
+    // (str.replace "AB" (str.++ x "A") x) --> (str.replace "AB" (str.++ x "A")
+    // "")
+    Node repl_ab_xa_x = d_nm->mkNode(kind::STRING_STRREPL,
+                                     d_nm->mkNode(kind::STRING_CONCAT, a, b),
+                                     d_nm->mkNode(kind::STRING_CONCAT, x, a),
+                                     x);
+    Node repl_ab_xa_e = d_nm->mkNode(kind::STRING_STRREPL,
+                                     d_nm->mkNode(kind::STRING_CONCAT, a, b),
+                                     d_nm->mkNode(kind::STRING_CONCAT, x, a),
+                                     empty);
+    Node res_repl_ab_xa_x = Rewriter::rewrite(repl_ab_xa_x);
+    Node res_repl_ab_xa_e = Rewriter::rewrite(repl_ab_xa_e);
+    TS_ASSERT_EQUALS(res_repl_ab_xa_x, res_repl_ab_xa_e);
+
+    // (str.replace "AB" (str.++ x "A") x) -/-> (str.replace "AB" (str.++ "A" x)
+    // "")
+    Node repl_ab_ax_e = d_nm->mkNode(kind::STRING_STRREPL,
+                                     d_nm->mkNode(kind::STRING_CONCAT, a, b),
+                                     d_nm->mkNode(kind::STRING_CONCAT, a, x),
+                                     empty);
+    Node res_repl_ab_ax_e = Rewriter::rewrite(repl_ab_ax_e);
+    TS_ASSERT_DIFFERS(res_repl_ab_xa_x, res_repl_ab_ax_e);
+  }
+
+  void testRewriteContains()
+  {
+    TypeNode strType = d_nm->stringType();
+
+    Node empty = d_nm->mkConst(::CVC4::String(""));
+    Node a = d_nm->mkConst(::CVC4::String("A"));
+    Node b = d_nm->mkConst(::CVC4::String("B"));
+    Node c = d_nm->mkConst(::CVC4::String("C"));
+    Node x = d_nm->mkVar("x", strType);
+    Node y = d_nm->mkVar("y", strType);
+    Node z = d_nm->mkVar("z", strType);
+    Node one = d_nm->mkConst(Rational(2));
+    Node three = d_nm->mkConst(Rational(3));
+    Node four = d_nm->mkConst(Rational(4));
+    Node f = d_nm->mkConst(false);
+
+    // Same normal form for:
+    //
+    // (str.replace "A" (str.substr x 1 3) y z)
+    //
+    // (str.replace "A" (str.substr x 1 4) y z)
+    Node substr_3 =
+        d_nm->mkNode(kind::STRING_STRREPL,
+                     a,
+                     d_nm->mkNode(kind::STRING_SUBSTR, x, one, three),
+                     z);
+    Node substr_4 =
+        d_nm->mkNode(kind::STRING_STRREPL,
+                     a,
+                     d_nm->mkNode(kind::STRING_SUBSTR, x, one, four),
+                     z);
+    Node res_substr_3 = Rewriter::rewrite(substr_3);
+    Node res_substr_4 = Rewriter::rewrite(substr_4);
+    TS_ASSERT_EQUALS(res_substr_3, res_substr_4);
+
+    // Same normal form for:
+    //
+    // (str.replace "A" (str.++ y (str.substr x 1 3)) y z)
+    //
+    // (str.replace "A" (str.++ y (str.substr x 1 4)) y z)
+    Node concat_substr_3 = d_nm->mkNode(
+        kind::STRING_STRREPL,
+        a,
+        d_nm->mkNode(kind::STRING_CONCAT,
+                     y,
+                     d_nm->mkNode(kind::STRING_SUBSTR, x, one, three)),
+        z);
+    Node concat_substr_4 = d_nm->mkNode(
+        kind::STRING_STRREPL,
+        a,
+        d_nm->mkNode(kind::STRING_CONCAT,
+                     y,
+                     d_nm->mkNode(kind::STRING_SUBSTR, x, one, four)),
+        z);
+    Node res_concat_substr_3 = Rewriter::rewrite(concat_substr_3);
+    Node res_concat_substr_4 = Rewriter::rewrite(concat_substr_4);
+    TS_ASSERT_EQUALS(res_concat_substr_3, res_concat_substr_4);
+
+    // (str.contains "A" (str.++ a (str.replace "B", x, "C")) --> false
+    Node ctn_repl =
+        d_nm->mkNode(kind::STRING_STRCTN,
+                     a,
+                     d_nm->mkNode(kind::STRING_CONCAT,
+                                  a,
+                                  d_nm->mkNode(kind::STRING_STRREPL, b, x, c)));
+    Node res_ctn_repl = Rewriter::rewrite(ctn_repl);
+    TS_ASSERT_EQUALS(res_ctn_repl, f);
+
+    // (str.contains x (str.++ x x)) --> (= x "")
+    Node x_cnts_x_x = d_nm->mkNode(
+        kind::STRING_STRCTN, x, d_nm->mkNode(kind::STRING_CONCAT, x, x));
+    Node res_x_cnts_x_x = Rewriter::rewrite(x_cnts_x_x);
+    Node res_x_eq_empty =
+        Rewriter::rewrite(d_nm->mkNode(kind::EQUAL, x, empty));
+    TS_ASSERT_EQUALS(res_x_cnts_x_x, res_x_eq_empty);
+
+    // Same normal form for:
+    //
+    // (str.contains (str.++ y x) (str.++ x z y))
+    //
+    // (and (str.contains (str.++ y x) (str.++ x y)) (= z ""))
+    Node yx = d_nm->mkNode(kind::STRING_CONCAT, y, x);
+    Node yx_cnts_xzy = d_nm->mkNode(
+        kind::STRING_STRCTN, yx, d_nm->mkNode(kind::STRING_CONCAT, x, z, y));
+    Node res_yx_cnts_xzy = Rewriter::rewrite(yx_cnts_xzy);
+    Node xy = d_nm->mkNode(kind::STRING_CONCAT, x, y);
+    Node yx_cnts_xy = d_nm->mkNode(kind::AND,
+                                   d_nm->mkNode(kind::STRING_STRCTN, yx, xy),
+                                   d_nm->mkNode(kind::EQUAL, z, empty));
+    Node res_yx_cnts_xy = Rewriter::rewrite(yx_cnts_xy);
+    TS_ASSERT_EQUALS(res_yx_cnts_xzy, res_yx_cnts_xy);
+  }
 };
-- 
2.30.2