mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-03-11 15:50:29 +00:00
Code Activity

make simple solver a reference

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2026-03-10 15:10:51 -07:00
parent 3e3c3f106d
commit c98ea6dc21
3 changed files with 8 additions and 22 deletions
Download patch file Download diff file Expand all files Collapse all files

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

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

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

@ -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<simple_solver> 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; }

2
src/smt/theory_nseq.cpp
View file

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