rename files to streamline naming

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

src/ast/rewriter/CMakeLists.txt

@@ -35,9 +35,9 @@ z3_add_component(rewriter
     pb2bv_rewriter.cpp
     push_app_ite.cpp
     quant_hoist.cpp
-    range_predicate.cpp
+    seq_range_predicate.cpp
     recfun_rewriter.cpp
-    regex_range_collapse.cpp
+    seq_range_collapse.cpp
     rewriter.cpp
     seq_axioms.cpp
     seq_eq_solver.cpp

src/ast/rewriter/seq_range_collapse.cpp

@@ -3,7 +3,7 @@ Copyright (c) 2026 Microsoft Corporation
 
 Module Name:
 
-    regex_range_collapse.cpp
+    seq_range_collapse.cpp
 
 Abstract:
 
@@ -17,7 +17,7 @@ Authors:
 
 --*/
 
-#include "ast/rewriter/regex_range_collapse.h"
+#include "ast/rewriter/seq_range_collapse.h"
 
 namespace seq {
 

src/ast/rewriter/seq_range_collapse.h

@@ -3,7 +3,7 @@ Copyright (c) 2026 Microsoft Corporation
 
 Module Name:
 
-    regex_range_collapse.h
+    seq_range_collapse.h
 
 Abstract:
 
@@ -25,7 +25,7 @@ Authors:
 --*/
 #pragma once
 
-#include "ast/rewriter/range_predicate.h"
+#include "ast/rewriter/seq_range_predicate.h"
 #include "ast/seq_decl_plugin.h"
 
 namespace seq {

src/ast/rewriter/seq_range_predicate.cpp

@@ -3,12 +3,12 @@ Copyright (c) 2026 Microsoft Corporation
 
 Module Name:
 
-    range_predicate.cpp
+    seq_range_predicate.cpp
 
 Abstract:
 
     Implementation of the specialized range-algebra used by symbolic
-    derivative computation and regex rewriting. See range_predicate.h
+    derivative computation and regex rewriting. See seq_range_predicate.h
     for the algebraic specification.
 
     All Boolean operations are implemented as single linear sweeps over
@@ -21,7 +21,7 @@ Authors:
 
 --*/
 
-#include "ast/rewriter/range_predicate.h"
+#include "ast/rewriter/seq_range_predicate.h"
 #include "util/debug.h"
 #include <algorithm>
 #include <ostream>

src/ast/rewriter/seq_range_predicate.h

@@ -3,7 +3,7 @@ Copyright (c) 2026 Microsoft Corporation
 
 Module Name:
 
-    range_predicate.h
+    seq_range_predicate.h
 
 Abstract:
 

src/ast/rewriter/seq_rewriter.cpp

@@ -21,7 +21,7 @@ Authors:
 #include "util/uint_set.h"
 #include "ast/rewriter/seq_rewriter.h"
 #include "ast/rewriter/seq_regex_bisim.h"
-#include "ast/rewriter/regex_range_collapse.h"
+#include "ast/rewriter/seq_range_collapse.h"
 #include "ast/arith_decl_plugin.h"
 #include "ast/array_decl_plugin.h"
 #include "ast/ast_pp.h"

src/ast/rewriter/seq_rewriter.h

@@ -253,7 +253,7 @@ class seq_rewriter {
     // Range-set collapse helpers: if the operands form a boolean
     // combination of character-class regexes, materialize the result as a
     // canonical regex over a single range_predicate.  See
-    // ast/rewriter/regex_range_collapse.h for the recognized fragment.
+    // ast/rewriter/seq_range_collapse.h for the recognized fragment.
     // NOTE: re.complement is intentionally not in this set because it
     // operates at the sequence level, not the character-class level.
     bool try_collapse_re_union(expr* a, expr* b, expr_ref& result);

src/test/range_predicate.cpp

@@ -22,7 +22,7 @@ Author:
 
 --*/
 
-#include "ast/rewriter/range_predicate.h"
+#include "ast/rewriter/seq_range_predicate.h"
 #include "util/debug.h"
 #include <cstdint>
 #include <iostream>

src/test/regex_range_collapse.cpp

@@ -7,7 +7,7 @@ Module Name:
 
 --*/
 
-#include "ast/rewriter/regex_range_collapse.h"
+#include "ast/rewriter/seq_range_collapse.h"
 #include "ast/reg_decl_plugins.h"
 #include "ast/ast_pp.h"
 #include "ast/arith_decl_plugin.h"