From 8773f7ac81dede3dcf96983087417c652cbf35b8 Mon Sep 17 00:00:00 2001
From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Mon, 15 Jul 2019 11:03:01 -0500
Subject: [PATCH]  Add string rewrite to distribute character stars over
 concatenation (#3091)

---
 .../strings/theory_strings_rewriter.cpp       | 22 +++++++++++++++++++
 test/regress/CMakeLists.txt                   |  1 +
 test/regress/regress1/strings/issue3090.smt2  |  6 +++++
 3 files changed, 29 insertions(+)
 create mode 100644 test/regress/regress1/strings/issue3090.smt2

diff --git a/src/theory/strings/theory_strings_rewriter.cpp b/src/theory/strings/theory_strings_rewriter.cpp
index daae57659..cb5508fb7 100644
--- 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 f7760a504..b6fa29e28 100644
--- 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
index 000000000..734257a25
--- /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)
-- 
2.30.2