Add string rewrite to distribute character stars over concatenation (#3091)

diff --git a/src/theory/strings/theory_strings_rewriter.cpp b/src/theory/strings/theory_strings_rewriter.cpp
index daae576590a9cbca97598d7b7665f04d237a6dc5..cb5508fb777abd0721647c6b7f796694f81b0826 100644 (file)
--- a/src/theory/strings/theory_strings_rewriter.cpp
+++ b/src/theory/strings/theory_strings_rewriter.cpp
@@ -1231,9 +1231,31 @@ Node TheoryStringsRewriter::rewriteMembership(TNode node) {
         }
       }
     }
+    else if (x.getKind() == STRING_CONCAT)
+    {
+      // (str.in.re (str.++ x1 ... xn) (str.* R)) -->
+      //   (str.in.re x1 (re.* R)) AND ... AND (str.in.re xn (re.* R))
+      //     if the length of all strings in R is one.
+      Node flr = getFixedLengthForRegexp(r[0]);
+      if (!flr.isNull())
+      {
+        Node one = nm->mkConst(Rational(1));
+        if (flr == one)
+        {
+          NodeBuilder<> nb(AND);
+          for (const Node& xc : x)
+          {
+            nb << nm->mkNode(STRING_IN_REGEXP, xc, r);
+          }
+          Node retNode = nb.constructNode();
+          return returnRewrite(node, retNode, "re-in-dist-char-star");
+        }
+      }
+    }
     if (r[0].getKind() == kind::REGEXP_SIGMA)
     {
       retNode = NodeManager::currentNM()->mkConst( true );
+      return returnRewrite(node, retNode, "re-in-sigma-star");
     }
   }else if( r.getKind() == kind::REGEXP_CONCAT ){
     bool allSigma = true;

diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt
index f7760a5043e99cd6e6fb5b95a5f15a749150c9a8..b6fa29e2842d1aa6a9c9885bcf9a38a66782ff7b 100644 (file)
--- a/test/regress/CMakeLists.txt
+++ b/test/regress/CMakeLists.txt
@@ -1553,6 +1553,7 @@ set(regress_1_tests
   regress1/strings/issue2429-code.smt2
   regress1/strings/issue2981.smt2
   regress1/strings/issue2982.smt2
+  regress1/strings/issue3090.smt2
   regress1/strings/kaluza-fl.smt2
   regress1/strings/loop002.smt2
   regress1/strings/loop003.smt2

diff --git a/test/regress/regress1/strings/issue3090.smt2 b/test/regress/regress1/strings/issue3090.smt2
new file mode 100644 (file)
index 0000000..734257a
--- /dev/null
+++ b/test/regress/regress1/strings/issue3090.smt2
@@ -0,0 +1,6 @@
+(set-logic ALL_SUPPORTED)
+(set-option :strings-exp true)
+(set-info :status unsat)
+(declare-const id String)
+(assert (and (str.in.re id (re.+ (re.range "0" "9"))) (str.contains id "value")))
+(check-sat)