From c98ea6dc214facb3b0557c4c7284426bda61bfb1 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Tue, 10 Mar 2026 15:10:51 -0700 Subject: [PATCH] make simple solver a reference Signed-off-by: Nikolaj Bjorner --- src/smt/seq/seq_nielsen.cpp | 21 +++++---------------- src/smt/seq/seq_nielsen.h | 7 ++----- src/smt/theory_nseq.cpp | 2 +- 3 files changed, 8 insertions(+), 22 deletions(-) diff --git a/src/smt/seq/seq_nielsen.cpp b/src/smt/seq/seq_nielsen.cpp index 4447eeac4..629179ab3 100644 --- a/src/smt/seq/seq_nielsen.cpp +++ b/src/smt/seq/seq_nielsen.cpp @@ -241,11 +241,7 @@ namespace seq { // nielsen_graph // ----------------------------------------------- - nielsen_graph::nielsen_graph(euf::sgraph& sg): - m_sg(sg) { - } - - nielsen_graph::nielsen_graph(euf::sgraph& sg, simple_solver* solver): + nielsen_graph::nielsen_graph(euf::sgraph& sg, simple_solver& solver): m_sg(sg), m_solver(solver) { } @@ -2394,20 +2390,13 @@ namespace seq { if (constraints.empty()) return true; // no integer constraints, trivially feasible - if (!m_solver) { - // No solver provided: skip arithmetic feasibility checking. - // This makes the Nielsen graph unsound with respect to integer constraints - // but is acceptable for contexts (e.g., unit tests) that only exercise - // string equality patterns without arithmetic path constraints. - return true; - } - m_solver->push(); + m_solver.push(); for (auto const& ic : constraints) - m_solver->assert_expr(int_constraint_to_expr(ic)); + m_solver.assert_expr(int_constraint_to_expr(ic)); - lbool result = m_solver->check(); - m_solver->pop(1); + lbool result = m_solver.check(); + m_solver.pop(1); return result != l_false; } diff --git a/src/smt/seq/seq_nielsen.h b/src/smt/seq/seq_nielsen.h index fb8cc0096..5b9cfcd89 100644 --- a/src/smt/seq/seq_nielsen.h +++ b/src/smt/seq/seq_nielsen.h @@ -660,15 +660,12 @@ namespace seq { // When m_solver is null, check_int_feasibility skips arithmetic checking // and optimistically assumes feasibility. // ----------------------------------------------- - simple_solver* m_solver = nullptr; - scoped_ptr m_owned_solver; // non-null when we own the solver + simple_solver& m_solver; public: - // Construct without a custom solver; integer feasibility checks are skipped. - nielsen_graph(euf::sgraph& sg); // Construct with a caller-supplied solver. Ownership is NOT transferred; // the caller is responsible for keeping the solver alive. - nielsen_graph(euf::sgraph& sg, simple_solver* solver); + nielsen_graph(euf::sgraph& sg, simple_solver& solver); ~nielsen_graph(); euf::sgraph& sg() { return m_sg; } diff --git a/src/smt/theory_nseq.cpp b/src/smt/theory_nseq.cpp index dee9aa4e9..4794fcbd7 100644 --- a/src/smt/theory_nseq.cpp +++ b/src/smt/theory_nseq.cpp @@ -34,7 +34,7 @@ namespace smt { m_egraph(ctx.get_manager()), m_sgraph(ctx.get_manager(), m_egraph), m_context_solver(ctx.get_manager()), - m_nielsen(m_sgraph, &m_context_solver), + 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)