From 964760cf81eb7414a11bbd89ef3a16e8927d6947 Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Fri, 20 Mar 2020 14:07:37 -0500 Subject: 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 / getConst is allowable in rewriter_str.cpp. --- src/CMakeLists.txt | 6 ++++-- 1 file changed, 4 insertions(+), 2 deletions(-) (limited to 'src/CMakeLists.txt') diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt index 7e31d1494..c35a14800 100644 --- a/src/CMakeLists.txt +++ b/src/CMakeLists.txt @@ -679,18 +679,20 @@ libcvc4_add_sources( theory/strings/regexp_operation.h theory/strings/regexp_solver.cpp theory/strings/regexp_solver.h + theory/strings/sequences_rewriter.cpp + theory/strings/sequences_rewriter.h theory/strings/skolem_cache.cpp theory/strings/skolem_cache.h theory/strings/solver_state.cpp theory/strings/solver_state.h theory/strings/strings_fmf.cpp theory/strings/strings_fmf.h + theory/strings/strings_rewriter.cpp + theory/strings/strings_rewriter.h theory/strings/theory_strings.cpp theory/strings/theory_strings.h theory/strings/theory_strings_preprocess.cpp theory/strings/theory_strings_preprocess.h - theory/strings/theory_strings_rewriter.cpp - theory/strings/theory_strings_rewriter.h theory/strings/theory_strings_type_rules.h theory/strings/theory_strings_utils.cpp theory/strings/theory_strings_utils.h -- cgit v1.2.3