From 7c328647deeae1c348347bd4680d836cf34fa195 Mon Sep 17 00:00:00 2001
From: "copilot-swe-agent[bot]" <198982749+Copilot@users.noreply.github.com>
Date: Tue, 3 Mar 2026 00:17:10 +0000
Subject: [PATCH] Move seq_nielsen from src/ast/rewriter to src/smt/seq with
 new smt_seq component

Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
---
 src/CMakeLists.txt                            | 1 +
 src/ast/rewriter/CMakeLists.txt               | 1 -
 src/smt/seq/CMakeLists.txt                    | 7 +++++++
 src/{ast/rewriter => smt/seq}/seq_nielsen.cpp | 2 +-
 src/{ast/rewriter => smt/seq}/seq_nielsen.h   | 2 +-
 src/test/CMakeLists.txt                       | 2 +-
 src/test/seq_nielsen.cpp                      | 2 +-
 7 files changed, 12 insertions(+), 5 deletions(-)
 create mode 100644 src/smt/seq/CMakeLists.txt
 rename src/{ast/rewriter => smt/seq}/seq_nielsen.cpp (99%)
 rename src/{ast/rewriter => smt/seq}/seq_nielsen.h (99%)

diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt
index 1a6608849..d36b64112 100644
--- a/src/CMakeLists.txt
+++ b/src/CMakeLists.txt
@@ -53,6 +53,7 @@ add_subdirectory(ackermannization)
 add_subdirectory(ast/proofs)
 add_subdirectory(ast/fpa)
 add_subdirectory(smt/proto_model)
+add_subdirectory(smt/seq)
 add_subdirectory(smt)
 add_subdirectory(tactic/bv)
 add_subdirectory(smt/tactic)
diff --git a/src/ast/rewriter/CMakeLists.txt b/src/ast/rewriter/CMakeLists.txt
index 50bd28c2e..9d529f9b5 100644
--- a/src/ast/rewriter/CMakeLists.txt
+++ b/src/ast/rewriter/CMakeLists.txt
@@ -39,7 +39,6 @@ z3_add_component(rewriter
     rewriter.cpp
     seq_axioms.cpp
     seq_eq_solver.cpp
-    seq_nielsen.cpp
     seq_rewriter.cpp
     seq_skolem.cpp
     th_rewriter.cpp
diff --git a/src/smt/seq/CMakeLists.txt b/src/smt/seq/CMakeLists.txt
new file mode 100644
index 000000000..db63e4c6f
--- /dev/null
+++ b/src/smt/seq/CMakeLists.txt
@@ -0,0 +1,7 @@
+z3_add_component(smt_seq
+  SOURCES
+    seq_nielsen.cpp
+  COMPONENT_DEPENDENCIES
+    euf
+    rewriter
+)
diff --git a/src/ast/rewriter/seq_nielsen.cpp b/src/smt/seq/seq_nielsen.cpp
similarity index 99%
rename from src/ast/rewriter/seq_nielsen.cpp
rename to src/smt/seq/seq_nielsen.cpp
index d03586b71..90b1ffa2a 100644
--- a/src/ast/rewriter/seq_nielsen.cpp
+++ b/src/smt/seq/seq_nielsen.cpp
@@ -19,7 +19,7 @@ Author:
 
 --*/
 
-#include "ast/rewriter/seq_nielsen.h"
+#include "smt/seq/seq_nielsen.h"
 #include "ast/ast_pp.h"
 
 namespace seq {
diff --git a/src/ast/rewriter/seq_nielsen.h b/src/smt/seq/seq_nielsen.h
similarity index 99%
rename from src/ast/rewriter/seq_nielsen.h
rename to src/smt/seq/seq_nielsen.h
index 3ee87c5e5..10120dc6e 100644
--- a/src/ast/rewriter/seq_nielsen.h
+++ b/src/smt/seq/seq_nielsen.h
@@ -11,7 +11,7 @@ Abstract:
 
     Ports the constraint types and Nielsen graph structures from
     ZIPT (https://github.com/CEisenhofer/ZIPT/tree/parikh/ZIPT/Constraints)
-    into Z3's rewriter framework.
+    into Z3's smt/seq framework.
 
     The Nielsen graph is used for solving word equations and regex
     membership constraints via Nielsen transformations. Each node
diff --git a/src/test/CMakeLists.txt b/src/test/CMakeLists.txt
index 24db5a848..b0d0a6a1e 100644
--- a/src/test/CMakeLists.txt
+++ b/src/test/CMakeLists.txt
@@ -3,7 +3,7 @@ add_subdirectory(lp)
 ################################################################################
 # z3-test executable
 ################################################################################
-set(z3_test_deps api fuzzing simplex)
+set(z3_test_deps api fuzzing simplex smt_seq)
 z3_expand_dependencies(z3_test_expanded_deps ${z3_test_deps})
 set (z3_test_extra_object_files "")
 foreach (component ${z3_test_expanded_deps})
diff --git a/src/test/seq_nielsen.cpp b/src/test/seq_nielsen.cpp
index 4a3a170c1..19a831427 100644
--- a/src/test/seq_nielsen.cpp
+++ b/src/test/seq_nielsen.cpp
@@ -15,7 +15,7 @@ Abstract:
 
 #include "util/util.h"
 #include "ast/euf/euf_sgraph.h"
-#include "ast/rewriter/seq_nielsen.h"
+#include "smt/seq/seq_nielsen.h"
 #include "ast/reg_decl_plugins.h"
 #include "ast/ast_pp.h"
 #include <iostream>