diff --git a/src/ast/rewriter/CMakeLists.txt b/src/ast/rewriter/CMakeLists.txt index 80aab976ba..98043d695b 100644 --- a/src/ast/rewriter/CMakeLists.txt +++ b/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 diff --git a/src/ast/rewriter/regex_range_collapse.cpp b/src/ast/rewriter/seq_range_collapse.cpp similarity index 98% rename from src/ast/rewriter/regex_range_collapse.cpp rename to src/ast/rewriter/seq_range_collapse.cpp index 7b63108367..3bd40e7bcd 100644 --- a/src/ast/rewriter/regex_range_collapse.cpp +++ b/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 { diff --git a/src/ast/rewriter/regex_range_collapse.h b/src/ast/rewriter/seq_range_collapse.h similarity index 97% rename from src/ast/rewriter/regex_range_collapse.h rename to src/ast/rewriter/seq_range_collapse.h index 5e02a67d94..16cd5fd67b 100644 --- a/src/ast/rewriter/regex_range_collapse.h +++ b/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 { diff --git a/src/ast/rewriter/range_predicate.cpp b/src/ast/rewriter/seq_range_predicate.cpp similarity index 98% rename from src/ast/rewriter/range_predicate.cpp rename to src/ast/rewriter/seq_range_predicate.cpp index 53b31a84a7..7bb9eac821 100644 --- a/src/ast/rewriter/range_predicate.cpp +++ b/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 #include diff --git a/src/ast/rewriter/range_predicate.h b/src/ast/rewriter/seq_range_predicate.h similarity index 99% rename from src/ast/rewriter/range_predicate.h rename to src/ast/rewriter/seq_range_predicate.h index 31226e4a91..4fbf4938f5 100644 --- a/src/ast/rewriter/range_predicate.h +++ b/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: diff --git a/src/ast/rewriter/seq_rewriter.cpp b/src/ast/rewriter/seq_rewriter.cpp index 774664c097..4f804b4b47 100644 --- a/src/ast/rewriter/seq_rewriter.cpp +++ b/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" diff --git a/src/ast/rewriter/seq_rewriter.h b/src/ast/rewriter/seq_rewriter.h index 39084deeff..ce64817929 100644 --- a/src/ast/rewriter/seq_rewriter.h +++ b/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); diff --git a/src/test/range_predicate.cpp b/src/test/range_predicate.cpp index 7d332f4131..e526a63302 100644 --- a/src/test/range_predicate.cpp +++ b/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 #include diff --git a/src/test/regex_range_collapse.cpp b/src/test/regex_range_collapse.cpp index a8ba90d5b6..fa55a25db4 100644 --- a/src/test/regex_range_collapse.cpp +++ b/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"