projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: aa44c35) | patch
Split string-specific operators from TheoryStringsRewriter (#3920)
authorAndrew Reynolds <andrew.j.reynolds@gmail.com>
Fri, 20 Mar 2020 19:07:37 +0000 (14:07 -0500)
committerGitHub <noreply@github.com>
Fri, 20 Mar 2020 19:07:37 +0000 (14:07 -0500)
commit964760cf81eb7414a11bbd89ef3a16e8927d6947
tree0c574e99433c722e69af6efeeefbe0901010f7b7tree
parentaa44c35f035f1cab03de0c5fe7c0f16b20f44696commit | diff
Split string-specific operators from TheoryStringsRewriter (#3920)

Organization towards theory of sequences.

The motivation of this PR is to ensure that string-specific operators in the rewriter are in their own file; thus the use of mkConst<String> / getConst<String> is allowable in rewriter_str.cpp.
22 files changed:
src/CMakeLists.txt diff | blob | history
src/theory/quantifiers/extended_rewrite.cpp diff | blob | history
src/theory/strings/base_solver.cpp diff | blob | history
src/theory/strings/core_solver.cpp diff | blob | history
src/theory/strings/extf_solver.cpp diff | blob | history
src/theory/strings/inference_manager.cpp diff | blob | history
src/theory/strings/kinds diff | blob | history
src/theory/strings/regexp_elim.cpp diff | blob | history
src/theory/strings/regexp_operation.cpp diff | blob | history
src/theory/strings/regexp_solver.cpp diff | blob | history
src/theory/strings/sequences_rewriter.cpp [new file with mode: 0644] blob
src/theory/strings/sequences_rewriter.h [new file with mode: 0644] blob
src/theory/strings/skolem_cache.cpp diff | blob | history
src/theory/strings/strings_rewriter.cpp [new file with mode: 0644] blob
src/theory/strings/strings_rewriter.h [new file with mode: 0644] blob
src/theory/strings/theory_strings.cpp diff | blob | history
src/theory/strings/theory_strings_preprocess.cpp diff | blob | history
src/theory/strings/theory_strings_rewriter.cpp [deleted file] blob | history
src/theory/strings/theory_strings_rewriter.h [deleted file] blob | history
test/unit/theory/CMakeLists.txt diff | blob | history
test/unit/theory/sequences_rewriter_white.h [new file with mode: 0644] blob
test/unit/theory/theory_strings_rewriter_white.h [deleted file] blob | history