From 219891b2a3b23c2bff0a99e56e6510786d274ddf Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Tue, 7 Aug 2018 22:06:19 -0500 Subject: [PATCH] Fix simple reg exp consume rewrite (#2281) --- .../strings/theory_strings_rewriter.cpp | 15 +++++++++++++-- test/regress/Makefile.tests | 1 + .../regress1/strings/re-unsound-080718.smt2 | 19 +++++++++++++++++++ 3 files changed, 33 insertions(+), 2 deletions(-) create mode 100644 test/regress/regress1/strings/re-unsound-080718.smt2 diff --git a/src/theory/strings/theory_strings_rewriter.cpp b/src/theory/strings/theory_strings_rewriter.cpp index fe92dd8ff..10bce3a29 100644 --- a/src/theory/strings/theory_strings_rewriter.cpp +++ b/src/theory/strings/theory_strings_rewriter.cpp @@ -983,12 +983,23 @@ Node TheoryStringsRewriter::rewriteMembership(TNode node) { return scn; }else{ if( (children.size() + mchildren.size())!=prevSize ){ + // Given a membership (str.++ x1 ... xn) in (re.++ r1 ... rm), + // above, we strip components to construct an equivalent membership: + // (str.++ xi .. xj) in (re.++ rk ... rl). + Node xn = mkConcat(kind::STRING_CONCAT, mchildren); + Node emptyStr = nm->mkConst(String("")); if( children.empty() ){ - retNode = NodeManager::currentNM()->mkConst( mchildren.empty() ); + // If we stripped all components on the right, then the left is + // equal to the empty string. + // e.g. (str.++ "a" x) in (re.++ (str.to.re "a")) ---> (= x "") + retNode = xn.eqNode(emptyStr); }else{ - retNode = NodeManager::currentNM()->mkNode( kind::STRING_IN_REGEXP, mkConcat( kind::STRING_CONCAT, mchildren ), mkConcat( kind::REGEXP_CONCAT, children ) ); + // otherwise, construct the updated regular expression + retNode = nm->mkNode( + STRING_IN_REGEXP, xn, mkConcat(REGEXP_CONCAT, children)); } Trace("regexp-ext-rewrite") << "Regexp : rewrite : " << node << " -> " << retNode << std::endl; + return returnRewrite(node, retNode, "re-simple-consume"); } } } diff --git a/test/regress/Makefile.tests b/test/regress/Makefile.tests index 2be59087b..0724fc163 100644 --- a/test/regress/Makefile.tests +++ b/test/regress/Makefile.tests @@ -1473,6 +1473,7 @@ REG1_TESTS = \ regress1/strings/norn-nel-bug-052116.smt2 \ regress1/strings/norn-simp-rew-sat.smt2 \ regress1/strings/pierre150331.smt2 \ + regress1/strings/re-unsound-080718.smt2 \ regress1/strings/regexp001.smt2 \ regress1/strings/regexp002.smt2 \ regress1/strings/regexp003.smt2 \ diff --git a/test/regress/regress1/strings/re-unsound-080718.smt2 b/test/regress/regress1/strings/re-unsound-080718.smt2 new file mode 100644 index 000000000..96353e746 --- /dev/null +++ b/test/regress/regress1/strings/re-unsound-080718.smt2 @@ -0,0 +1,19 @@ +; COMMAND-LINE: --strings-print-ascii --strings-exp +; EXPECT: sat +(set-info :smt-lib-version 2.5) +(set-logic ALL) +(set-info :status sat) +(declare-fun x () String) +(assert +(and +(not (= + (str.in.re x (re.++ (str.to.re "B") (re.* (str.to.re "B")))) + (str.in.re x (re.++ (str.to.re "B") (str.to.re (str.++ "B" "B")))) +)) +(not (= + (str.in.re x (re.++ (re.union (re.++ (str.to.re "A") re.allchar ) re.allchar ) (str.to.re "B"))) + (str.in.re x (re.++ (str.to.re "A") (str.to.re "B"))) +)) +) +) +(check-sat) -- 2.30.2