mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-03-18 02:53:46 +00:00
Code Activity

build verified: nseq_regex moved to smt/seq

Browse source 
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
This commit is contained in:
copilot-swe-agent[bot] 2026-03-14 16:49:28 +00:00
parent 323d2f7fec
commit 974386d793
9 changed files with 7 additions and 7 deletions
Download patch file Download diff file Expand all files Collapse all files

1
src/smt/CMakeLists.txt
View file

@ -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

2
src/smt/nseq_model.cpp
View file

@ -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"

1
src/smt/seq/CMakeLists.txt
View file

@ -1,5 +1,6 @@
z3_add_component(smt_seq
SOURCES
nseq_regex.cpp
seq_parikh.cpp
seq_nielsen.cpp
COMPONENT_DEPENDENCIES

2
src/smt/nseq_regex.cpp → src/smt/seq/nseq_regex.cpp
View file

@ -14,7 +14,7 @@ Author:
Nikolaj Bjorner (nbjorner) 2026-03-01
--*/
#include "smt/nseq_regex.h"
#include "smt/seq/nseq_regex.h"
#include <unordered_set>
namespace smt {

0
src/smt/nseq_regex.h → src/smt/seq/nseq_regex.h
View file

2
src/smt/seq/seq_nielsen.cpp
View file

@ -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"

2
src/smt/seq/seq_nielsen.h
View file

@ -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 {

2
src/smt/theory_nseq.h
View file

@ -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"

2
src/test/nseq_regex.cpp
View file

@ -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"