diff options
author | Andres Noetzli <andres.noetzli@gmail.com> | 2020-01-13 00:40:15 -0800 |
---|---|---|
committer | Andres Noetzli <andres.noetzli@gmail.com> | 2020-01-21 02:29:21 -0800 |
commit | f4ebd4e2cccf3e4dcd412c0ca19aaa1505c8524e (patch) | |
tree | ca383cf21c74718116685e4ee6a87cdc12caa17a | |
parent | 459b4c64d4bb7a53ddf619e571c61d4d5a9628f3 (diff) |
more aggressive elim
-rw-r--r-- | src/theory/strings/regexp_elim.cpp | 38 |
1 files changed, 28 insertions, 10 deletions
diff --git a/src/theory/strings/regexp_elim.cpp b/src/theory/strings/regexp_elim.cpp index 1942938c3..3bc77ab3d 100644 --- a/src/theory/strings/regexp_elim.cpp +++ b/src/theory/strings/regexp_elim.cpp @@ -350,19 +350,37 @@ Node RegExpElimination::eliminateConcat(Node atom) { unsigned index = r == 0 ? 0 : nchildren - 1; Node c = children[index]; - if (c.getKind() == STRING_TO_REGEXP) + + while (true) { - Assert(children[index + (r == 0 ? 1 : -1)].getKind() != STRING_TO_REGEXP); - Node s = c[0]; - Node lens = nm->mkNode(STRING_LENGTH, s); - Node sss = r == 0 ? d_zero : nm->mkNode(MINUS, lenx, lens); - Node ss = nm->mkNode(STRING_SUBSTR, x, sss, lens); - sConstraints.push_back(ss.eqNode(s)); - if (r == 0) + if (c.getKind() == STRING_TO_REGEXP) + { + Assert(children[index + (r == 0 ? 1 : -1)].getKind() + != STRING_TO_REGEXP); + Node s = c[0]; + Node lens = nm->mkNode(STRING_LENGTH, s); + Node sss = r == 0 ? d_zero : nm->mkNode(MINUS, lenx, lens); + Node ss = nm->mkNode(STRING_SUBSTR, x, sss, lens); + sConstraints.push_back(ss.eqNode(s)); + if (r == 0) + { + sStartIndex = nm->mkNode(PLUS, sStartIndex, lens); + } + sLength = nm->mkNode(MINUS, sLength, lens); + } + else if (c.getKind() == REGEXP_SIGMA) { - sStartIndex = lens; + if (r == 0) + { + sStartIndex = nm->mkNode(PLUS, sStartIndex, d_one); + } + sLength = nm->mkNode(MINUS, sLength, d_one); + } + else + { + break; } - sLength = nm->mkNode(MINUS, sLength, lens); + index += (r == 0) ? 1 : -1; } if (r == 1 && !sConstraints.empty()) { |