projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 9cbf861) | patch
Improve rewriting of str.<= (#4848)
authorAndres Noetzli <andres.noetzli@gmail.com>
Tue, 1 Dec 2020 16:58:06 +0000 (08:58 -0800)
committerGitHub <noreply@github.com>
Tue, 1 Dec 2020 16:58:06 +0000 (10:58 -0600)
commit41554fa3d4a8258bbc842aedad87cd218460ee0a
tree8237abb5bbc7441c0a6674bdeff7e1b2e3634a18tree
parent9cbf861d698aaa44d79ca7bd4714064a55f31fbacommit | 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.
src/theory/strings/strings_rewriter.cpp diff | blob | history
test/regress/CMakeLists.txt diff | blob | history
test/regress/regress0/strings/leq.smt2 [new file with mode: 0644] blob
test/unit/theory/CMakeLists.txt diff | blob | history
test/unit/theory/strings_rewriter_white.h [new file with mode: 0644] blob