diff --git a/src/smt/CMakeLists.txt b/src/smt/CMakeLists.txt index 04aadac54..add3f1ba7 100644 --- a/src/smt/CMakeLists.txt +++ b/src/smt/CMakeLists.txt @@ -66,7 +66,6 @@ z3_add_component(smt theory_lra.cpp theory_nseq.cpp nseq_state.cpp - nseq_regex.cpp nseq_model.cpp theory_opt.cpp theory_pb.cpp diff --git a/src/smt/nseq_model.cpp b/src/smt/nseq_model.cpp index 8eb8d5a59..6fd9779b1 100644 --- a/src/smt/nseq_model.cpp +++ b/src/smt/nseq_model.cpp @@ -17,7 +17,7 @@ Author: --*/ #include "smt/nseq_model.h" #include "smt/theory_nseq.h" -#include "smt/nseq_regex.h" +#include "smt/seq/nseq_regex.h" #include "smt/nseq_state.h" #include "smt/smt_context.h" #include "smt/smt_model_generator.h" diff --git a/src/smt/seq/CMakeLists.txt b/src/smt/seq/CMakeLists.txt index e6ed34c34..faa3a1ec7 100644 --- a/src/smt/seq/CMakeLists.txt +++ b/src/smt/seq/CMakeLists.txt @@ -1,5 +1,6 @@ z3_add_component(smt_seq SOURCES + nseq_regex.cpp seq_parikh.cpp seq_nielsen.cpp COMPONENT_DEPENDENCIES diff --git a/src/smt/nseq_regex.cpp b/src/smt/seq/nseq_regex.cpp similarity index 99% rename from src/smt/nseq_regex.cpp rename to src/smt/seq/nseq_regex.cpp index 743b74ef6..e62843bb7 100644 --- a/src/smt/nseq_regex.cpp +++ b/src/smt/seq/nseq_regex.cpp @@ -14,7 +14,7 @@ Author: Nikolaj Bjorner (nbjorner) 2026-03-01 --*/ -#include "smt/nseq_regex.h" +#include "smt/seq/nseq_regex.h" #include namespace smt { diff --git a/src/smt/nseq_regex.h b/src/smt/seq/nseq_regex.h similarity index 100% rename from src/smt/nseq_regex.h rename to src/smt/seq/nseq_regex.h diff --git a/src/smt/seq/seq_nielsen.cpp b/src/smt/seq/seq_nielsen.cpp index 52d3ec36b..45352e747 100644 --- a/src/smt/seq/seq_nielsen.cpp +++ b/src/smt/seq/seq_nielsen.cpp @@ -21,7 +21,7 @@ Author: #include "smt/seq/seq_nielsen.h" #include "smt/seq/seq_parikh.h" -#include "smt/nseq_regex.h" +#include "smt/seq/nseq_regex.h" #include "ast/arith_decl_plugin.h" #include "ast/ast_pp.h" #include "ast/rewriter/seq_rewriter.h" diff --git a/src/smt/seq/seq_nielsen.h b/src/smt/seq/seq_nielsen.h index 987350924..11f594098 100644 --- a/src/smt/seq/seq_nielsen.h +++ b/src/smt/seq/seq_nielsen.h @@ -245,7 +245,7 @@ Author: #include "model/model.h" namespace smt { - class nseq_regex; // forward declaration (defined in smt/nseq_regex.h) + class nseq_regex; // forward declaration (defined in smt/seq/nseq_regex.h) } namespace seq { diff --git a/src/smt/theory_nseq.h b/src/smt/theory_nseq.h index 24f5ad566..bd1dd961c 100644 --- a/src/smt/theory_nseq.h +++ b/src/smt/theory_nseq.h @@ -26,7 +26,7 @@ Author: #include "smt/smt_arith_value.h" #include "smt/seq/seq_nielsen.h" #include "smt/nseq_state.h" -#include "smt/nseq_regex.h" +#include "smt/seq/nseq_regex.h" #include "smt/nseq_model.h" #include "smt/nseq_context_solver.h" diff --git a/src/test/nseq_regex.cpp b/src/test/nseq_regex.cpp index 6970413b0..8d9533005 100644 --- a/src/test/nseq_regex.cpp +++ b/src/test/nseq_regex.cpp @@ -15,7 +15,7 @@ Abstract: #include "ast/reg_decl_plugins.h" #include "ast/euf/euf_egraph.h" #include "ast/euf/euf_sgraph.h" -#include "smt/nseq_regex.h" +#include "smt/seq/nseq_regex.h" #include "smt/seq/seq_nielsen.h" #include "util/lbool.h" #include "util/zstring.h"