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