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.

1 files changed, 3 insertions, 3 deletions

diff --git a/src/theory/strings/regexp_operation.cpp b/src/theory/strings/regexp_operation.cpp
index f91b59834..d5105a489 100644
--- a/src/theory/strings/regexp_operation.cpp
+++ b/src/theory/strings/regexp_operation.cpp
@@ -18,7 +18,7 @@
 
 #include "expr/kind.h"
 #include "options/strings_options.h"
-#include "theory/strings/theory_strings_rewriter.h"
+#include "theory/strings/sequences_rewriter.h"
 #include "theory/strings/theory_strings_utils.h"
 #include "theory/strings/word.h"
 
@@ -920,12 +920,12 @@ void RegExpOpr::simplifyNRegExp( Node s, Node r, std::vector< Node > &new_nodes
         // all strings in the language of R1 have the same length, say n,
         // then the conclusion of the reduction is quantifier-free:
         //    ~( substr(s,0,n) in R1 ) OR ~( substr(s,n,len(s)-n) in R2)
-        Node reLength = TheoryStringsRewriter::getFixedLengthForRegexp(r[0]);
+        Node reLength = SequencesRewriter::getFixedLengthForRegexp(r[0]);
         if (reLength.isNull())
         {
           // try from the opposite end
           unsigned indexE = r.getNumChildren() - 1;
-          reLength = TheoryStringsRewriter::getFixedLengthForRegexp(r[indexE]);
+          reLength = SequencesRewriter::getFixedLengthForRegexp(r[indexE]);
           if (!reLength.isNull())
           {
             indexRm = indexE;