diff options
| -rw-r--r-- | src/theory/strings/theory_strings_rewriter.cpp | 9 | ||||
| -rw-r--r-- | test/unit/theory/theory_strings_rewriter_white.h | 25 |
2 files changed, 29 insertions, 5 deletions
diff --git a/src/theory/strings/theory_strings_rewriter.cpp b/src/theory/strings/theory_strings_rewriter.cpp index 919c56f54..365e6d33d 100644 --- a/src/theory/strings/theory_strings_rewriter.cpp +++ b/src/theory/strings/theory_strings_rewriter.cpp @@ -1245,8 +1245,11 @@ Node TheoryStringsRewriter::rewriteMembership(TNode node) { bool allSigmaStrict = true; unsigned allSigmaMinSize = 0; Node constStr; - for (const Node& rc : r) + size_t constIdx = 0; + size_t nchildren = r.getNumChildren(); + for (size_t i = 0; i < nchildren; i++) { + Node rc = r[i]; Assert(rc.getKind() != kind::REGEXP_EMPTY); if (rc.getKind() == kind::REGEXP_SIGMA) { @@ -1261,6 +1264,7 @@ Node TheoryStringsRewriter::rewriteMembership(TNode node) { if (constStr.isNull()) { constStr = rc[0]; + constIdx = i; } else { @@ -1284,7 +1288,8 @@ Node TheoryStringsRewriter::rewriteMembership(TNode node) { retNode = nm->mkNode(allSigmaStrict ? EQUAL : GEQ, lenx, num); return returnRewrite(node, retNode, "re-concat-pure-allchar"); } - else if (allSigmaMinSize == 0) + else if (allSigmaMinSize == 0 && nchildren >= 3 && constIdx != 0 + && constIdx != nchildren - 1) { // x in re.++(_*, "abc", _*) ---> str.contains(x, "abc") retNode = nm->mkNode(STRING_STRCTN, x, constStr); diff --git a/test/unit/theory/theory_strings_rewriter_white.h b/test/unit/theory/theory_strings_rewriter_white.h index 0ca5e5c15..1961f9e5e 100644 --- a/test/unit/theory/theory_strings_rewriter_white.h +++ b/test/unit/theory/theory_strings_rewriter_white.h @@ -1209,8 +1209,10 @@ class TheoryStringsRewriterWhite : public CxxTest::TestSuite { // Same normal form for: // - // (str.in.re x (re.++ (re.* re.allchar) (str.to.re "ABC") (re.* - // re.allchar))) + // (str.in.re x (re.++ (re.* re.allchar) + // (re.* re.allchar) + // (str.to.re "ABC") + // (re.* re.allchar))) // // (str.contains x "ABC") Node sig_star = d_nm->mkNode(kind::REGEXP_STAR, @@ -1218,10 +1220,27 @@ class TheoryStringsRewriterWhite : public CxxTest::TestSuite Node lhs = d_nm->mkNode( kind::STRING_IN_REGEXP, x, - d_nm->mkNode(kind::REGEXP_CONCAT, sig_star, re_abc, sig_star)); + d_nm->mkNode( + kind::REGEXP_CONCAT, sig_star, sig_star, re_abc, sig_star)); Node rhs = d_nm->mkNode(kind::STRING_STRCTN, x, abc); sameNormalForm(lhs, rhs); } + + { + // Different normal forms for: + // + // (str.in.re x (re.++ (re.* re.allchar) (str.to.re "ABC"))) + // + // (str.contains x "ABC") + Node sig_star = d_nm->mkNode(kind::REGEXP_STAR, + d_nm->mkNode(kind::REGEXP_SIGMA, vec_empty)); + Node lhs = + d_nm->mkNode(kind::STRING_IN_REGEXP, + x, + d_nm->mkNode(kind::REGEXP_CONCAT, sig_star, re_abc)); + Node rhs = d_nm->mkNode(kind::STRING_STRCTN, x, abc); + differentNormalForms(lhs, rhs); + } } private: |