Simplify rewrite for character matching (#3545)

diff --git a/src/theory/strings/theory_strings_rewriter.cpp b/src/theory/strings/theory_strings_rewriter.cpp
index fa3650b589b510e5b51d8dac60101fad3c6f1218..5ae0d87b3cb621163a1b63517162375e4a35fbe3 100644 (file)
--- a/src/theory/strings/theory_strings_rewriter.cpp
+++ b/src/theory/strings/theory_strings_rewriter.cpp
@@ -2064,46 +2064,20 @@ Node TheoryStringsRewriter::rewriteContains( Node node ) {
       }
       else if (checkEntailLengthOne(t))
       {
-        std::vector<unsigned> svec = s.getVec();
-        std::sort(svec.begin(), svec.end());
+        const std::vector<unsigned>& vec = s.getVec();
 
         NodeBuilder<> nb(OR);
         nb << nm->mkConst(String("")).eqNode(t);
-
-        Node tc = nm->mkNode(STRING_CODE, t);
-        unsigned lb = svec[0];
-        unsigned curr = lb;
-        for (size_t i = 0, size = svec.size(); i <= size; i++)
+        for (unsigned c : vec)
         {
-          if (i == size || (svec[i] != curr && svec[i] != curr + 1))
-          {
-            Node nlb = nm->mkConst(Rational(CVC4::String::convertUnsignedIntToCode(lb)));
-            Node nub = nm->mkConst(Rational(CVC4::String::convertUnsignedIntToCode(svec[i - 1])));
-            if (nlb == nub)
-            {
-              nb << nm->mkNode(EQUAL, tc, nlb);
-            }
-            else
-            {
-              nb << nm->mkNode(
-                  AND, nm->mkNode(LEQ, nlb, tc), nm->mkNode(LEQ, tc, nub));
-            }
-
-            if (i != size) {
-            lb = svec[i];
-            curr = lb;
-            }
-          } else {
-            curr = svec[i];
-          }
+          std::vector<unsigned> sv = {c};
+          nb << nm->mkConst(String(sv)).eqNode(t);
         }
 
-        Node ret = nb;
-
-        // str.contains("ABCDEFabcdef", t) --->
-        // t = "" v str.code("A") <= str.code(t) <= str.code("F") v
-        //          str.code("a") <= str.code(t) <= str.code("f")
+        // str.contains("ABCabc", t) --->
+        // t = "" v t = "A" v t = "B" v t = "C" v t = "a" v t = "b" v t = "c"
         // if len(t) <= 1
+        Node ret = nb;
         return returnRewrite(node, ret, "ctn-split");
       }
       else if (node[1].getKind() == kind::STRING_CONCAT)

diff --git a/test/unit/theory/theory_strings_rewriter_white.h b/test/unit/theory/theory_strings_rewriter_white.h
index b5eb92900fc373b496e28660e7a09b525bfe9023..d71df524cb46af54158fdba8cfca275d72922f28 100644 (file)
--- a/test/unit/theory/theory_strings_rewriter_white.h
+++ b/test/unit/theory/theory_strings_rewriter_white.h
@@ -710,7 +710,6 @@ class TheoryStringsRewriterWhite : public CxxTest::TestSuite
     Node abc = d_nm->mkConst(::CVC4::String("ABC"));
     Node def = d_nm->mkConst(::CVC4::String("DEF"));
     Node ghi = d_nm->mkConst(::CVC4::String("GHI"));
-    Node abbchijp = d_nm->mkConst(::CVC4::String("ABBCHIJP"));
     Node x = d_nm->mkVar("x", strType);
     Node y = d_nm->mkVar("y", strType);
     Node xy = d_nm->mkNode(kind::STRING_CONCAT, x, y);
@@ -1009,31 +1008,17 @@ class TheoryStringsRewriterWhite : public CxxTest::TestSuite
     {
       // Same normal form for:
       //
-      // (str.contains "ABBCHIJP" (str.at x n))
+      // (str.contains "ABC" (str.at x n))
       //
       // (or (= x "")
-      //     (and (<= (str.code "A") (str.code (str.at x n)))
-      //          (<= (str.code (str.at x n)) (str.code "C")))
-      //     (and (<= (str.code "H") (str.code (str.at x n)))
-      //          (<= (str.code (str.at x n)) (str.code "J")))
-      //     (= (str.code (str.at x n)) (str.code "P")))
+      //     (= x "A") (= x "B") (= x "C"))
       Node cat = d_nm->mkNode(kind::STRING_CHARAT, x, n);
-      lhs = d_nm->mkNode(kind::STRING_STRCTN, abbchijp, cat);
-      Node ca = d_nm->mkNode(kind::STRING_CODE, a);
-      Node cc = d_nm->mkNode(kind::STRING_CODE, c);
-      Node ch = d_nm->mkNode(kind::STRING_CODE, h);
-      Node cj = d_nm->mkNode(kind::STRING_CODE, j);
-      Node cp = d_nm->mkNode(kind::STRING_CODE, p);
-      Node ccat = d_nm->mkNode(kind::STRING_CODE, cat);
+      lhs = d_nm->mkNode(kind::STRING_STRCTN, abc, cat);
       rhs = d_nm->mkNode(kind::OR,
                          d_nm->mkNode(kind::EQUAL, cat, empty),
-                         d_nm->mkNode(kind::AND,
-                                      d_nm->mkNode(kind::LEQ, ca, ccat),
-                                      d_nm->mkNode(kind::LEQ, ccat, cc)),
-                         d_nm->mkNode(kind::AND,
-                                      d_nm->mkNode(kind::LEQ, ch, ccat),
-                                      d_nm->mkNode(kind::LEQ, ccat, cj)),
-                         d_nm->mkNode(kind::EQUAL, ccat, cp));
+                         d_nm->mkNode(kind::EQUAL, cat, a),
+                         d_nm->mkNode(kind::EQUAL, cat, b),
+                         d_nm->mkNode(kind::EQUAL, cat, c));
       sameNormalForm(lhs, rhs);
     }
   }