diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2019-07-19 09:36:53 -0400 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2019-07-19 09:36:53 -0400 |
| commit | 9fa66413709fbdb1a02f8986d0c332934523b110 (patch) | |
| tree | 39b67dd05ba658c1f8619d3b5156f453f895ea64 | |
| parent | d5ed6a659eaa801fbbd82efc31f03d575351b6ec (diff) | |
Fix case of unfolding negative membership in reg exp concatenation (#3101)
| -rw-r--r-- | src/theory/strings/regexp_operation.cpp | 18 | ||||
| -rw-r--r-- | src/theory/strings/regexp_solver.cpp | 1 | ||||
| -rw-r--r-- | test/regress/CMakeLists.txt | 1 | ||||
| -rw-r--r-- | test/regress/regress1/strings/re-neg-unfold-rev-a.smt2 | 10 |
4 files changed, 22 insertions, 8 deletions
diff --git a/src/theory/strings/regexp_operation.cpp b/src/theory/strings/regexp_operation.cpp index 0360228c6..0d422e823 100644 --- a/src/theory/strings/regexp_operation.cpp +++ b/src/theory/strings/regexp_operation.cpp @@ -850,14 +850,18 @@ void RegExpOpr::simplifyNRegExp( Node s, Node r, std::vector< Node > &new_nodes { b1 = reLength; } - Node s1 = nm->mkNode(STRING_SUBSTR, s, d_zero, b1); - Node s2 = nm->mkNode(STRING_SUBSTR, s, b1, nm->mkNode(MINUS, lens, b1)); - if (indexRm != 0) + Node s1; + Node s2; + if (indexRm == 0) { - // swap if we are removing from the end - Node sswap = s1; - s1 = s2; - s2 = sswap; + s1 = nm->mkNode(STRING_SUBSTR, s, d_zero, b1); + s2 = nm->mkNode(STRING_SUBSTR, s, b1, nm->mkNode(MINUS, lens, b1)); + } + else + { + s1 = nm->mkNode(STRING_SUBSTR, s, nm->mkNode(MINUS, lens, b1), b1); + s2 = + nm->mkNode(STRING_SUBSTR, s, d_zero, nm->mkNode(MINUS, lens, b1)); } Node s1r1 = nm->mkNode(STRING_IN_REGEXP, s1, r[indexRm]).negate(); std::vector<Node> nvec; diff --git a/src/theory/strings/regexp_solver.cpp b/src/theory/strings/regexp_solver.cpp index 5079806ac..65d616c3c 100644 --- a/src/theory/strings/regexp_solver.cpp +++ b/src/theory/strings/regexp_solver.cpp @@ -281,7 +281,6 @@ void RegExpSolver::check() std::vector<Node> exp_n; exp_n.push_back(assertion); Node conc = nvec.size() == 1 ? nvec[0] : nm->mkNode(AND, nvec); - conc = Rewriter::rewrite(conc); d_im.sendInference(rnfexp, exp_n, conc, "REGEXP_Unfold"); addedLemma = true; if (changed) diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt index aae919a2f..af6a9b839 100644 --- a/test/regress/CMakeLists.txt +++ b/test/regress/CMakeLists.txt @@ -1580,6 +1580,7 @@ set(regress_1_tests regress1/strings/re-agg-total2.smt2 regress1/strings/re-elim-exact.smt2 regress1/strings/re-neg-concat-reduct.smt2 + regress1/strings/re-neg-unfold-rev-a.smt2 regress1/strings/re-unsound-080718.smt2 regress1/strings/regexp001.smt2 regress1/strings/regexp002.smt2 diff --git a/test/regress/regress1/strings/re-neg-unfold-rev-a.smt2 b/test/regress/regress1/strings/re-neg-unfold-rev-a.smt2 new file mode 100644 index 000000000..3f99f8507 --- /dev/null +++ b/test/regress/regress1/strings/re-neg-unfold-rev-a.smt2 @@ -0,0 +1,10 @@ +(set-info :smt-lib-version 2.5) +(set-logic QF_S) +(set-info :status unsat) +(set-option :strings-exp true) + +(declare-const x String) +(declare-const y String) +(assert (and (= y "foobar") (str.in.re x (re.++ (str.to.re "ab") (re.* re.allchar) (str.to.re "b") (re.* re.allchar) (str.to.re "b") (re.* re.allchar) (str.to.re "b"))))) +(assert (not (and (= y "foobar") (str.in.re x (re.++ (str.to.re "a") (re.* re.allchar) (str.to.re "b") (re.* re.allchar) (str.to.re "b") (re.* re.allchar) (str.to.re "b")))))) +(check-sat) |