Only apply testConstStringInRegExp to const regexp (#4120)

Fixes #4070. `TheoryStringsRewriter::rewriteConcatRegExp()` rewrites
`(a)* ++ (_)*` to `(_)*`. To do so, it checks whether the elements
preceding `(_)*` match the empty string using
`TheoryStringsRewriter::testConstStringInRegExp()`. However, this method
only expects to be called on constant regular expressions (i.e. regular
expressions without string variables). This commit adds a corresponding
check before calling `TheoryStringsRewriter::testConstStringInRegExp()`.

diff --git a/src/theory/strings/theory_strings_rewriter.cpp b/src/theory/strings/theory_strings_rewriter.cpp
index f05c9165bf366dbc1e349aa9bfee1c926e62c82e..95f537878522e06a820a44d4cd18111d2c13028b 100644 (file)
--- a/src/theory/strings/theory_strings_rewriter.cpp
+++ b/src/theory/strings/theory_strings_rewriter.cpp
@@ -907,7 +907,7 @@ Node TheoryStringsRewriter::rewriteConcatRegExp(TNode node)
     {
       // if empty, drop it
       // e.g. this ensures we rewrite (_)* ++ (a)* ---> (_)*
-      if (testConstStringInRegExp(emptyStr, 0, curr))
+      if (isConstRegExp(curr) && testConstStringInRegExp(emptyStr, 0, curr))
       {
         curr = Node::null();
       }
@@ -928,7 +928,7 @@ Node TheoryStringsRewriter::rewriteConcatRegExp(TNode node)
           lastAllStar = true;
           // go back and remove empty ones from back of cvec
           // e.g. this ensures we rewrite (a)* ++ (_)* ---> (_)*
-          while (!cvec.empty()
+          while (!cvec.empty() && isConstRegExp(cvec.back())
                  && testConstStringInRegExp(emptyStr, 0, cvec.back()))
           {
             cvec.pop_back();

diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt
index 0ea6114352a293b26ab9b9c9d8142cae84efe747..02eb158263a4e3e79f0dd8eba98797894a85f204 100644 (file)
--- a/test/regress/CMakeLists.txt
+++ b/test/regress/CMakeLists.txt
@@ -932,6 +932,7 @@ set(regress_0_tests
   regress0/strings/issue3440.smt2
   regress0/strings/issue3497.smt2
   regress0/strings/issue3657-evalLeq.smt2
+  regress0/strings/issue4070.smt2
   regress0/strings/itos-entail.smt2
   regress0/strings/large-model.smt2
   regress0/strings/leadingzero001.smt2

diff --git a/test/regress/regress0/strings/issue4070.smt2 b/test/regress/regress0/strings/issue4070.smt2
new file mode 100644 (file)
index 0000000..2de58c4
--- /dev/null
+++ b/test/regress/regress0/strings/issue4070.smt2
@@ -0,0 +1,6 @@
+; EXPECT: sat
+(set-logic QF_S)
+(declare-fun a () String)
+(declare-fun b () String)
+(assert (str.in.re a (re.++ (str.to.re b) (re.* re.allchar))))
+(check-sat)

diff --git a/test/unit/theory/theory_strings_rewriter_white.h b/test/unit/theory/theory_strings_rewriter_white.h
index d71df524cb46af54158fdba8cfca275d72922f28..af8b24a0b006f5abeeaae1fa86f660b69b1fc21d 100644 (file)
--- a/test/unit/theory/theory_strings_rewriter_white.h
+++ b/test/unit/theory/theory_strings_rewriter_white.h
@@ -58,6 +58,15 @@ class TheoryStringsRewriterWhite : public CxxTest::TestSuite
     delete d_em;
   }
 
+  void inNormalForm(Node t)
+  {
+    Node res_t = d_rewriter->extendedRewrite(t);
+
+    std::cout << std::endl;
+    std::cout << t << " ---> " << res_t << std::endl;
+    TS_ASSERT_EQUALS(t, res_t);
+  }
+
   void sameNormalForm(Node t1, Node t2)
   {
     Node res_t1 = d_rewriter->extendedRewrite(t1);
@@ -1528,6 +1537,37 @@ class TheoryStringsRewriterWhite : public CxxTest::TestSuite
     }
   }
 
+  void testRewriteRegexpConcat()
+  {
+    TypeNode strType = d_nm->stringType();
+
+    std::vector<Node> emptyArgs;
+    Node x = d_nm->mkVar("x", strType);
+    Node y = d_nm->mkVar("y", strType);
+    Node allStar = d_nm->mkNode(kind::REGEXP_STAR,
+                                d_nm->mkNode(kind::REGEXP_SIGMA, emptyArgs));
+    Node xReg = d_nm->mkNode(kind::STRING_TO_REGEXP, x);
+    Node yReg = d_nm->mkNode(kind::STRING_TO_REGEXP, y);
+
+    {
+      // In normal form:
+      //
+      // (re.++ (re.* re.allchar) (re.union (str.to.re x) (str.to.re y)))
+      Node n = d_nm->mkNode(kind::REGEXP_CONCAT,
+                            allStar,
+                            d_nm->mkNode(kind::REGEXP_UNION, xReg, yReg));
+      inNormalForm(n);
+    }
+
+    {
+      // In normal form:
+      //
+      // (re.++ (str.to.re x) (re.* re.allchar))
+      Node n = d_nm->mkNode(kind::REGEXP_CONCAT, xReg, allStar);
+      inNormalForm(n);
+    }
+  }
+
  private:
   ExprManager* d_em;
   SmtEngine* d_smt;