diff options
| -rw-r--r-- | src/theory/strings/theory_strings_rewriter.cpp | 22 | ||||
| -rw-r--r-- | test/regress/CMakeLists.txt | 1 | ||||
| -rw-r--r-- | test/regress/regress1/strings/issue3090.smt2 | 6 |
3 files changed, 29 insertions, 0 deletions
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) |