mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-03-17 18:43:45 +00:00
Code Activity

seq_model: remove theory_nseq dependency; get family_id from seq_util

Browse source 
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
This commit is contained in:
copilot-swe-agent[bot] 2026-03-14 17:20:47 +00:00
parent e01872dc70
commit 1437ec25ce
3 changed files with 7 additions and 9 deletions
Download patch file Download diff file Expand all files Collapse all files

7
src/smt/seq/seq_model.cpp
View file

@ -17,7 +17,6 @@ Author:
--*/
#include "smt/seq/seq_model.h"
#include "smt/theory_nseq.h"
#include "smt/seq/seq_regex.h"
#include "smt/seq/seq_state.h"
#include "smt/smt_context.h"
@ -27,9 +26,9 @@ Author:
namespace smt {
seq_model::seq_model(theory_nseq& th, ast_manager& m, seq_util& seq,
seq_model::seq_model(ast_manager& m, seq_util& seq,
seq_rewriter& rw, euf::sgraph& sg, seq::seq_regex& regex)
: m_th(th), m(m), m_seq(seq), m_rewriter(rw), m_sg(sg), m_regex(regex), m_trail(m)
: m(m), m_seq(seq), m_rewriter(rw), m_sg(sg), m_regex(regex), m_trail(m)
{}
void seq_model::init(model_generator& mg, seq::nielsen_graph& nielsen, seq_state const& state) {
@ -39,7 +38,7 @@ namespace smt {
m_int_model = nullptr;
m_mg = &mg;
m_factory = alloc(seq_factory, m, m_th.get_family_id(), mg.get_model());
m_factory = alloc(seq_factory, m, m_seq.get_family_id(), mg.get_model());
mg.register_factory(m_factory);
register_existing_values(nielsen);

7
src/smt/seq/seq_model.h
View file

@ -31,7 +31,6 @@ Author:
#include "ast/seq_decl_plugin.h"
#include "ast/rewriter/seq_rewriter.h"
#include "ast/euf/euf_sgraph.h"
#include "smt/smt_types.h"
#include "smt/seq/seq_nielsen.h"
#include "model/seq_factory.h"
@ -43,12 +42,12 @@ namespace seq {
namespace smt {
class theory_nseq;
class enode;
class model_generator;
class seq_state;
class model_value_proc;
class seq_model {
theory_nseq& m_th;
ast_manager& m;
seq_util& m_seq;
seq_rewriter& m_rewriter;
@ -74,7 +73,7 @@ namespace smt {
u_map<euf::snode*> m_var_regex;
public:
seq_model(theory_nseq& th, ast_manager& m, seq_util& seq,
seq_model(ast_manager& m, seq_util& seq,
seq_rewriter& rw, euf::sgraph& sg, seq::seq_regex& regex);
// Phase 1: initialize model construction.

2
src/smt/theory_nseq.cpp
View file

@ -37,7 +37,7 @@ namespace smt {
m_nielsen(m_sgraph, m_context_solver),
m_state(m_sgraph),
m_regex(m_sgraph),
m_model(*this, ctx.get_manager(), m_seq, m_rewriter, m_sgraph, m_regex)
m_model(ctx.get_manager(), m_seq, m_rewriter, m_sgraph, m_regex)
{}
// -----------------------------------------------------------------------