diff --git a/src/smt/CMakeLists.txt b/src/smt/CMakeLists.txt index 538b7d224..00072f4e3 100644 --- a/src/smt/CMakeLists.txt +++ b/src/smt/CMakeLists.txt @@ -65,6 +65,7 @@ z3_add_component(smt theory_intblast.cpp theory_lra.cpp theory_nseq.cpp + seq_model.cpp theory_opt.cpp theory_pb.cpp theory_recfun.cpp diff --git a/src/smt/seq/CMakeLists.txt b/src/smt/seq/CMakeLists.txt index afc5bcdd8..d05d2c9af 100644 --- a/src/smt/seq/CMakeLists.txt +++ b/src/smt/seq/CMakeLists.txt @@ -2,7 +2,6 @@ z3_add_component(smt_seq SOURCES seq_regex.cpp seq_state.cpp - seq_model.cpp seq_parikh.cpp seq_nielsen.cpp COMPONENT_DEPENDENCIES diff --git a/src/smt/seq/seq_state.h b/src/smt/seq/seq_state.h index 30574bee7..29ace6308 100644 --- a/src/smt/seq/seq_state.h +++ b/src/smt/seq/seq_state.h @@ -83,7 +83,7 @@ namespace smt { m_eq_sources.push_back({n1, n2}); } - void add_str_mem(euf::snode* str, euf::snode* regex, sat:literal lit) { + void add_str_mem(euf::snode* str, euf::snode* regex, sat::literal lit) { seq::dep_tracker dep; m_str_mems.push_back(seq::str_mem(str, regex, nullptr, m_next_mem_id++, dep)); m_mem_sources.push_back({lit}); diff --git a/src/smt/seq/seq_model.cpp b/src/smt/seq_model.cpp similarity index 99% rename from src/smt/seq/seq_model.cpp rename to src/smt/seq_model.cpp index 951039928..7177ec05f 100644 --- a/src/smt/seq/seq_model.cpp +++ b/src/smt/seq_model.cpp @@ -16,9 +16,10 @@ Author: Nikolaj Bjorner (nbjorner) 2026-03-01 --*/ -#include "smt/seq/seq_model.h" +#include "smt/seq_model.h" #include "smt/seq/seq_regex.h" #include "smt/seq/seq_state.h" +#include "smt/smt_context.h" #include "smt/smt_model_generator.h" #include "smt/proto_model/proto_model.h" #include "ast/ast_pp.h" diff --git a/src/smt/seq/seq_model.h b/src/smt/seq_model.h similarity index 100% rename from src/smt/seq/seq_model.h rename to src/smt/seq_model.h diff --git a/src/smt/theory_nseq.h b/src/smt/theory_nseq.h index b581235c1..d44c6d67c 100644 --- a/src/smt/theory_nseq.h +++ b/src/smt/theory_nseq.h @@ -27,7 +27,7 @@ Author: #include "smt/seq/seq_nielsen.h" #include "smt/seq/seq_state.h" #include "smt/seq/seq_regex.h" -#include "smt/seq/seq_model.h" +#include "smt/seq_model.h" #include "smt/nseq_context_solver.h" namespace smt {