projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 05c0998) | patch
Add support for str.replace_re/str.replace_re_all (#4594)
authorAndres Noetzli <andres.noetzli@gmail.com>
Wed, 10 Jun 2020 19:50:52 +0000 (12:50 -0700)
committerGitHub <noreply@github.com>
Wed, 10 Jun 2020 19:50:52 +0000 (12:50 -0700)
commit2da2646dd65e0458311a2dccfb04850c0b7d9e3c
tree00d31835b3ad0c00064ae2b43a2a59844f418dd0tree
parent05c099890ae908e495ceaf26509b87896fd0ad54commit | diff
Add support for str.replace_re/str.replace_re_all (#4594)

This commit adds support for the last remaining string operators from
the new SMT-LIB standard for the theory of strings. The commit adds the
kinds, type checking, reductions, and evaluation rewrites for
`str.replace_re` and `str.replace_re_all`.
19 files changed:
NEWS diff | blob | history
src/api/cvc4cpp.cpp diff | blob | history
src/api/cvc4cppkind.h diff | blob | history
src/parser/smt2/smt2.cpp diff | blob | history
src/printer/smt2/smt2_printer.cpp diff | blob | history
src/theory/strings/extf_solver.cpp diff | blob | history
src/theory/strings/kinds diff | blob | history
src/theory/strings/rewrites.cpp diff | blob | history
src/theory/strings/rewrites.h diff | blob | history
src/theory/strings/sequences_rewriter.cpp diff | blob | history
src/theory/strings/sequences_rewriter.h diff | blob | history
src/theory/strings/skolem_cache.h diff | blob | history
src/theory/strings/term_registry.cpp diff | blob | history
src/theory/strings/theory_strings.cpp diff | blob | history
src/theory/strings/theory_strings_preprocess.cpp diff | blob | history
test/regress/CMakeLists.txt diff | blob | history
test/regress/regress2/strings/replace_re.smt2 [new file with mode: 0644] blob
test/regress/regress2/strings/replace_re_all.smt2 [new file with mode: 0644] blob
test/unit/theory/sequences_rewriter_white.h diff | blob | history