diff options
author | Andres Noetzli <andres.noetzli@gmail.com> | 2019-02-03 09:42:25 -0800 |
---|---|---|
committer | Andres Noetzli <andres.noetzli@gmail.com> | 2019-02-03 09:42:25 -0800 |
commit | ce72634553c585622ec35be72df12443d92af36a (patch) | |
tree | d9e929ed1174bf4c93961b54568f767bcf658b46 | |
parent | 6f5dead04a864bc64203095aaf3bd6a57d47b065 (diff) | |
parent | 602d69928b598d7365ce4b51bc21ee1dcc2db450 (diff) |
Merge branch 'REtoCtn' into cav2019strings
-rw-r--r-- | src/theory/strings/theory_strings_rewriter.cpp | 38 | ||||
-rw-r--r-- | test/unit/theory/theory_strings_rewriter_white.h | 46 |
2 files changed, 79 insertions, 5 deletions
diff --git a/src/theory/strings/theory_strings_rewriter.cpp b/src/theory/strings/theory_strings_rewriter.cpp index 60084d535..8d9d6a230 100644 --- a/src/theory/strings/theory_strings_rewriter.cpp +++ b/src/theory/strings/theory_strings_rewriter.cpp @@ -1251,8 +1251,12 @@ Node TheoryStringsRewriter::rewriteMembership(TNode node) { bool allSigma = true; bool allSigmaStrict = true; unsigned allSigmaMinSize = 0; - for (const Node& rc : r) + Node constStr; + 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) { @@ -1262,6 +1266,19 @@ Node TheoryStringsRewriter::rewriteMembership(TNode node) { { allSigmaStrict = false; } + else if (rc.getKind() == STRING_TO_REGEXP) + { + if (constStr.isNull()) + { + constStr = rc[0]; + constIdx = i; + } + else + { + allSigma = false; + break; + } + } else { allSigma = false; @@ -1270,10 +1287,21 @@ Node TheoryStringsRewriter::rewriteMembership(TNode node) { } if (allSigma) { - Node num = nm->mkConst(Rational(allSigmaMinSize)); - Node lenx = nm->mkNode(STRING_LENGTH, x); - retNode = nm->mkNode(allSigmaStrict ? EQUAL : GEQ, lenx, num); - return returnRewrite(node, retNode, "re-concat-pure-allchar"); + if (constStr.isNull()) + { + // x in re.++(_*, _, _) ---> str.len(x) >= 2 + Node num = nm->mkConst(Rational(allSigmaMinSize)); + Node lenx = nm->mkNode(STRING_LENGTH, x); + retNode = nm->mkNode(allSigmaStrict ? EQUAL : GEQ, lenx, num); + return returnRewrite(node, retNode, "re-concat-pure-allchar"); + } + 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); + return returnRewrite(node, retNode, "re-concat-to-contains"); + } } }else if( r.getKind()==kind::REGEXP_INTER || r.getKind()==kind::REGEXP_UNION ){ std::vector< Node > mvec; diff --git a/test/unit/theory/theory_strings_rewriter_white.h b/test/unit/theory/theory_strings_rewriter_white.h index 494c886b8..6eb022eea 100644 --- a/test/unit/theory/theory_strings_rewriter_white.h +++ b/test/unit/theory/theory_strings_rewriter_white.h @@ -1243,6 +1243,52 @@ class TheoryStringsRewriterWhite : public CxxTest::TestSuite } } + void testRewriteMembership() + { + TypeNode strType = d_nm->stringType(); + + std::vector<Node> vec_empty; + Node abc = d_nm->mkConst(::CVC4::String("ABC")); + Node re_abc = d_nm->mkNode(kind::STRING_TO_REGEXP, abc); + Node x = d_nm->mkVar("x", strType); + + { + // Same normal form for: + // + // (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, + 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, 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: ExprManager* d_em; SmtEngine* d_smt; |