diff options
author | Andres Noetzli <andres.noetzli@gmail.com> | 2020-12-01 08:58:06 -0800 |
---|---|---|
committer | GitHub <noreply@github.com> | 2020-12-01 10:58:06 -0600 |
commit | 41554fa3d4a8258bbc842aedad87cd218460ee0a (patch) | |
tree | 8237abb5bbc7441c0a6674bdeff7e1b2e3634a18 /src/theory/strings | |
parent | 9cbf861d698aaa44d79ca7bd4714064a55f31fba (diff) |
Improve rewriting of str.<= (#4848)
This commit improves our rewriting of str.<= slightly. If we have
constant prefixes that are different, we can always rewrite the term to
a constant. Previously, we were only doing so when the result was
false.
Diffstat (limited to 'src/theory/strings')
-rw-r--r-- | src/theory/strings/strings_rewriter.cpp | 14 |
1 files changed, 6 insertions, 8 deletions
diff --git a/src/theory/strings/strings_rewriter.cpp b/src/theory/strings/strings_rewriter.cpp index 932b5c8cc..575c33501 100644 --- a/src/theory/strings/strings_rewriter.cpp +++ b/src/theory/strings/strings_rewriter.cpp @@ -251,15 +251,13 @@ Node StringsRewriter::rewriteStringLeq(Node n) { String s = n1[0].getConst<String>(); String t = n2[0].getConst<String>(); - // only need to truncate if s is longer - if (s.size() > t.size()) + size_t prefixLen = std::min(s.size(), t.size()); + s = s.prefix(prefixLen); + t = t.prefix(prefixLen); + // if the prefixes are not the same, then we can already decide the outcome + if (s != t) { - s = s.prefix(t.size()); - } - // if prefix is not leq, then entire string is not leq - if (!s.isLeq(t)) - { - Node ret = nm->mkConst(false); + Node ret = nm->mkConst(s.isLeq(t)); return returnRewrite(n, ret, Rewrite::STR_LEQ_CPREFIX); } } |