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 /src/theory/strings | |
| parent | d5ed6a659eaa801fbbd82efc31f03d575351b6ec (diff) | |
Fix case of unfolding negative membership in reg exp concatenation (#3101)
Diffstat (limited to 'src/theory/strings')
| -rw-r--r-- | src/theory/strings/regexp_operation.cpp | 18 | ||||
| -rw-r--r-- | src/theory/strings/regexp_solver.cpp | 1 |
2 files changed, 11 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) |