Address comments

3 files changed, 21 insertions, 15 deletions

diff --git a/src/theory/strings/theory_strings_rewriter.cpp b/src/theory/strings/theory_strings_rewriter.cpp
index 401e3b231..8e5e22d38 100644
--- a/src/theory/strings/theory_strings_rewriter.cpp
+++ b/src/theory/strings/theory_strings_rewriter.cpp
@@ -392,15 +392,23 @@ Node TheoryStringsRewriter::rewriteStrEqualityExt(Node node)
       Assert(cn.getConst<String>().size() == 1);
       unsigned hchar = cn.getConst<String>().front();
 
+      // The operands of the concat on each side of the equality without
+      // constant strings
       std::vector<Node> trimmed[2];
+      // Counts the number of `hchar`s on each side
       size_t numHChars[2] = {0, 0};
       for (size_t j = 0; j < 2; j++)
       {
+        // Sort the operands of the concats on both sides of the equality
+        // (since both sides may only contain one char, the order does not
+        // matter)
         std::sort(c[j].begin(), c[j].end());
         for (const Node& cc : c[j])
         {
           if (cc.getKind() == CONST_STRING)
           {
+            // Count the number of `hchar`s in the string constant and make
+            // sure that all chars are `hchar`s
             std::vector<unsigned> veccc = cc.getConst<String>().getVec();
             for (size_t k = 0, size = veccc.size(); k < size; k++)
             {
@@ -423,12 +431,16 @@ Node TheoryStringsRewriter::rewriteStrEqualityExt(Node node)
         }
       }
 
+      // We have to remove the same number of `hchar`s from both sides, so the
+      // side with less `hchar`s determines how many we can remove
       size_t trimmedConst = std::min(numHChars[0], numHChars[1]);
       for (size_t j = 0; j < 2; j++)
       {
         size_t diff = numHChars[j] - trimmedConst;
         if (diff != 0)
         {
+          // Add a constant string to the side with more `hchar`s to restore
+          // the difference in number of `hchar`s
           std::vector<unsigned> vec(diff, hchar);
           trimmed[j].push_back(nm->mkConst(String(vec)));
         }
diff --git a/src/theory/strings/theory_strings_rewriter.h b/src/theory/strings/theory_strings_rewriter.h
index c26a4ac50..8b0072f52 100644
--- a/src/theory/strings/theory_strings_rewriter.h
+++ b/src/theory/strings/theory_strings_rewriter.h
@@ -544,9 +544,11 @@ class TheoryStringsRewriter {
    * Checks whether it is always true that `a` is a strict subset of `b` in the
    * multiset domain.
    *
-   * Example:
+   * Examples:
    *
    * a = (str.++ "A" x), b = (str.++ "A" x "B") ---> true
+   * a = (str.++ "A" x), b = (str.++ "B" x "AA") ---> true
+   * a = (str.++ "A" x), b = (str.++ "B" y "AA") ---> false
    *
    * @param a The term for which it should be checked if it is a strict subset
    * of `b` in the multiset domain
diff --git a/test/unit/theory/theory_strings_rewriter_white.h b/test/unit/theory/theory_strings_rewriter_white.h
index ae42fe458..59d36d9e8 100644
--- a/test/unit/theory/theory_strings_rewriter_white.h
+++ b/test/unit/theory/theory_strings_rewriter_white.h
@@ -868,10 +868,10 @@ class TheoryStringsRewriterWhite : public CxxTest::TestSuite
     sameNormalForm(lhs, rhs);
 
     {
-      // (str.contains (str.++ x "A") (str.++ x "B")) ---> false
+      // (str.contains (str.++ x "A") (str.++ "B" x)) ---> false
       Node ctn = d_nm->mkNode(kind::STRING_STRCTN,
                               d_nm->mkNode(kind::STRING_CONCAT, x, a),
-                              d_nm->mkNode(kind::STRING_CONCAT, x, b));
+                              d_nm->mkNode(kind::STRING_CONCAT, b, x));
       sameNormalForm(ctn, f);
     }
   }
@@ -937,7 +937,7 @@ class TheoryStringsRewriterWhite : public CxxTest::TestSuite
 
     // Same normal form for:
     //
-    // (str.prefix x (str.++ x y))
+    // (str.prefix (str.++ x y) x)
     //
     // (= y "")
     Node p_xy = d_nm->mkNode(kind::STRING_PREFIX, xy, x);
@@ -946,7 +946,7 @@ class TheoryStringsRewriterWhite : public CxxTest::TestSuite
 
     // Same normal form for:
     //
-    // (str.suffix x (str.++ x x))
+    // (str.suffix (str.++ x x) x)
     //
     // (= x "")
     Node p_xx = d_nm->mkNode(kind::STRING_SUFFIX, xx, x);
@@ -1120,7 +1120,7 @@ class TheoryStringsRewriterWhite : public CxxTest::TestSuite
     {
       // Same normal form for:
       //
-      // (= (str.++ "A" x) (str.++ "A"))
+      // (= (str.++ "A" x) "A")
       //
       // (= x "")
       Node lhs =
@@ -1137,13 +1137,6 @@ class TheoryStringsRewriterWhite : public CxxTest::TestSuite
     }
 
     {
-      // (= (str.++ x "A") "") ---> false
-      Node eq = d_nm->mkNode(
-          kind::EQUAL, d_nm->mkNode(kind::STRING_CONCAT, x, a), empty);
-      sameNormalForm(eq, f);
-    }
-
-    {
       // (= (str.++ x "B") "AAA") ---> false
       Node eq = d_nm->mkNode(
           kind::EQUAL, d_nm->mkNode(kind::STRING_CONCAT, x, b), aaa);
@@ -1158,8 +1151,7 @@ class TheoryStringsRewriterWhite : public CxxTest::TestSuite
     }
 
     {
-      // (str.contains (str.++ "AAA" (str.substr "A" 0 n)) (str.++ x "B")) --->
-      //   false
+      // (= (str.++ "AAA" (str.substr "A" 0 n)) (str.++ x "B")) ---> false
       Node eq = d_nm->mkNode(
           kind::EQUAL,
           d_nm->mkNode(