diff --git a/src/smt/nseq_context_solver.h b/src/smt/nseq_context_solver.h new file mode 100644 index 000000000..4fb5edc5d --- /dev/null +++ b/src/smt/nseq_context_solver.h @@ -0,0 +1,64 @@ +/*++ +Copyright (c) 2026 Microsoft Corporation + +Module Name: + + nseq_context_solver.h + +Abstract: + + context_solver: concrete implementation of seq::simple_solver + that delegates arithmetic feasibility checks to an smt::kernel + configured with seq.solver = "seq_len". + +Author: + + Nikolaj Bjorner (nbjorner) 2026-03-10 + +--*/ +#pragma once + +#include "smt/seq/seq_nielsen.h" +#include "smt/smt_kernel.h" +#include "params/smt_params.h" + +namespace smt { + + /** + * Concrete simple_solver that wraps smt::kernel. + * Initializes the kernel with seq.solver = "seq_len" so that + * sequence length constraints are handled by theory_seq_len. + */ + class context_solver : public seq::simple_solver { + smt_params m_params; // must be declared before m_kernel + smt::kernel m_kernel; + + static smt_params make_seq_len_params() { + smt_params p; + p.m_string_solver = symbol("seq_len"); + return p; + } + + public: + context_solver(ast_manager& m) : + m_params(make_seq_len_params()), + m_kernel(m, m_params) {} + + lbool check() override { + return m_kernel.check(); + } + + void assert_expr(expr* e) override { + m_kernel.assert_expr(e); + } + + void push() override { + m_kernel.push(); + } + + void pop(unsigned num_scopes) override { + m_kernel.pop(num_scopes); + } + }; + +} diff --git a/src/smt/seq/seq_nielsen.cpp b/src/smt/seq/seq_nielsen.cpp index 6decb616d..4447eeac4 100644 --- a/src/smt/seq/seq_nielsen.cpp +++ b/src/smt/seq/seq_nielsen.cpp @@ -22,7 +22,6 @@ Author: #include "smt/seq/seq_nielsen.h" #include "ast/arith_decl_plugin.h" #include "ast/ast_pp.h" -#include "math/lp/lar_solver.h" #include "util/hashtable.h" #include #include @@ -30,179 +29,6 @@ Author: namespace seq { - // ----------------------------------------------- - // lp_simple_solver - // Concrete simple_solver built on top of lp::lar_solver. - // This is the default back-end used by nielsen_graph when no - // custom solver is provided. It translates each asserted - // arithmetic expression into LP bounds / terms and delegates - // feasibility checking to lp::lar_solver::find_feasible_solution(). - // ----------------------------------------------- - - class lp_simple_solver : public simple_solver { - ast_manager& m; - scoped_ptr m_lp; - u_map m_expr2lpvar; - unsigned m_ext_cnt = 0; - - // Stack of assertion counts for push/pop. - svector m_scope_stack; - expr_ref_vector m_asserted; - - public: - lp_simple_solver(ast_manager& m_) : m(m_), m_asserted(m_) {} - - lbool check() override { - // Rebuild LP solver from current assertions - m_lp = alloc(lp::lar_solver); - m_expr2lpvar.reset(); - m_ext_cnt = 0; - - arith_util arith(m); - for (expr* e : m_asserted) - add_to_lp(e, arith); - - lp::lp_status status = m_lp->find_feasible_solution(); - return (status == lp::lp_status::INFEASIBLE) ? l_false : l_true; - } - - void assert_expr(expr* e) override { - m_asserted.push_back(e); - } - - void push() override { - m_scope_stack.push_back(m_asserted.size()); - } - - void pop(unsigned num_scopes) override { - for (unsigned i = 0; i < num_scopes && !m_scope_stack.empty(); ++i) { - unsigned sz = m_scope_stack.back(); - m_scope_stack.pop_back(); - m_asserted.shrink(sz); - } - } - - private: - lp::lpvar ensure_var(expr* e, arith_util& arith) { - if (!e) return lp::null_lpvar; - unsigned eid = e->get_id(); - lp::lpvar j; - if (m_expr2lpvar.find(eid, j)) - return j; - - rational val; - if (arith.is_numeral(e, val)) { - j = m_lp->add_var(m_ext_cnt++, true); - m_lp->add_var_bound(j, lp::EQ, lp::mpq(val)); - m_expr2lpvar.insert(eid, j); - return j; - } - expr* e1 = nullptr, *e2 = nullptr; - if (arith.is_add(e, e1, e2)) { - lp::lpvar j1 = ensure_var(e1, arith); - lp::lpvar j2 = ensure_var(e2, arith); - if (j1 == lp::null_lpvar || j2 == lp::null_lpvar) return lp::null_lpvar; - vector> coeffs; - coeffs.push_back({lp::mpq(1), j1}); - coeffs.push_back({lp::mpq(1), j2}); - j = m_lp->add_term(coeffs, m_ext_cnt++); - m_expr2lpvar.insert(eid, j); - return j; - } - if (arith.is_sub(e, e1, e2)) { - lp::lpvar j1 = ensure_var(e1, arith); - lp::lpvar j2 = ensure_var(e2, arith); - if (j1 == lp::null_lpvar || j2 == lp::null_lpvar) return lp::null_lpvar; - vector> coeffs; - coeffs.push_back({lp::mpq(1), j1}); - coeffs.push_back({lp::mpq(-1), j2}); - j = m_lp->add_term(coeffs, m_ext_cnt++); - m_expr2lpvar.insert(eid, j); - return j; - } - if (arith.is_mul(e, e1, e2)) { - rational coeff; - if (arith.is_numeral(e1, coeff)) { - lp::lpvar jx = ensure_var(e2, arith); - if (jx == lp::null_lpvar) return lp::null_lpvar; - vector> coeffs; - coeffs.push_back({lp::mpq(coeff), jx}); - j = m_lp->add_term(coeffs, m_ext_cnt++); - m_expr2lpvar.insert(eid, j); - return j; - } - if (arith.is_numeral(e2, coeff)) { - lp::lpvar jx = ensure_var(e1, arith); - if (jx == lp::null_lpvar) return lp::null_lpvar; - vector> coeffs; - coeffs.push_back({lp::mpq(coeff), jx}); - j = m_lp->add_term(coeffs, m_ext_cnt++); - m_expr2lpvar.insert(eid, j); - return j; - } - } - if (arith.is_uminus(e, e1)) { - lp::lpvar jx = ensure_var(e1, arith); - if (jx == lp::null_lpvar) return lp::null_lpvar; - vector> coeffs; - coeffs.push_back({lp::mpq(-1), jx}); - j = m_lp->add_term(coeffs, m_ext_cnt++); - m_expr2lpvar.insert(eid, j); - return j; - } - // Leaf: fresh LP integer variable - j = m_lp->add_var(m_ext_cnt++, true); - m_expr2lpvar.insert(eid, j); - return j; - } - - void add_to_lp(expr* e, arith_util& arith) { - // Expected forms: (= lhs rhs), (<= lhs rhs), (>= lhs rhs) - expr* lhs = nullptr, *rhs = nullptr; - rational val; - - auto add_var_bound = [&](lp::lpvar j, lp::lconstraint_kind kind, lp::mpq const& bound) { - if (j != lp::null_lpvar) - m_lp->add_var_bound(j, kind, bound); - }; - - auto add_diff_bound = [&](expr* a, expr* b, lp::lconstraint_kind kind) { - lp::lpvar ja = ensure_var(a, arith); - lp::lpvar jb = ensure_var(b, arith); - if (ja == lp::null_lpvar || jb == lp::null_lpvar) return; - vector> coeffs; - coeffs.push_back({lp::mpq(1), ja}); - coeffs.push_back({lp::mpq(-1), jb}); - lp::lpvar term = m_lp->add_term(coeffs, m_ext_cnt++); - m_lp->add_var_bound(term, kind, lp::mpq(0)); - }; - - if (m.is_eq(e, lhs, rhs) && arith.is_int(lhs)) { - if (arith.is_numeral(rhs, val)) - add_var_bound(ensure_var(lhs, arith), lp::EQ, lp::mpq(val)); - else if (arith.is_numeral(lhs, val)) - add_var_bound(ensure_var(rhs, arith), lp::EQ, lp::mpq(val)); - else - add_diff_bound(lhs, rhs, lp::EQ); - } else if (arith.is_le(e, lhs, rhs)) { - if (arith.is_numeral(rhs, val)) - add_var_bound(ensure_var(lhs, arith), lp::LE, lp::mpq(val)); - else if (arith.is_numeral(lhs, val)) - add_var_bound(ensure_var(rhs, arith), lp::GE, lp::mpq(val)); - else - add_diff_bound(lhs, rhs, lp::LE); - } else if (arith.is_ge(e, lhs, rhs)) { - if (arith.is_numeral(rhs, val)) - add_var_bound(ensure_var(lhs, arith), lp::GE, lp::mpq(val)); - else if (arith.is_numeral(lhs, val)) - add_var_bound(ensure_var(rhs, arith), lp::LE, lp::mpq(val)); - else - add_diff_bound(lhs, rhs, lp::GE); - } - // other shapes are silently ignored - } - }; - // ----------------------------------------------- // str_eq // ----------------------------------------------- @@ -417,18 +243,11 @@ namespace seq { nielsen_graph::nielsen_graph(euf::sgraph& sg): m_sg(sg) { - // Create the default LP-based solver - m_owned_solver = alloc(lp_simple_solver, sg.get_manager()); - m_solver = m_owned_solver.get(); } nielsen_graph::nielsen_graph(euf::sgraph& sg, simple_solver* solver): m_sg(sg), m_solver(solver) { - if (!m_solver) { - m_owned_solver = alloc(lp_simple_solver, sg.get_manager()); - m_solver = m_owned_solver.get(); - } } nielsen_graph::~nielsen_graph() { @@ -2575,7 +2394,14 @@ namespace seq { if (constraints.empty()) return true; // no integer constraints, trivially feasible - SASSERT(m_solver); + 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(); for (auto const& ic : constraints) m_solver->assert_expr(int_constraint_to_expr(ic)); diff --git a/src/smt/seq/seq_nielsen.h b/src/smt/seq/seq_nielsen.h index 7b571b108..fb8cc0096 100644 --- a/src/smt/seq/seq_nielsen.h +++ b/src/smt/seq/seq_nielsen.h @@ -250,8 +250,8 @@ namespace seq { * to check integer/arithmetic feasibility of path constraints. * * Users of nielsen_graph can wrap smt::kernel or any other solver - * to serve as the arithmetic back-end. The default back-end is an - * lp_simple_solver built on top of lp::lar_solver. + * to serve as the arithmetic back-end. When no solver is provided, + * integer feasibility checks are skipped (optimistically assumed feasible). */ class simple_solver { public: @@ -657,14 +657,14 @@ namespace seq { // ----------------------------------------------- // Integer subsolver (abstract interface) - // When m_solver is null, check_int_feasibility uses an - // internal lp_simple_solver (created on demand). + // 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 public: - // Construct without a custom solver; an lp_simple_solver is used internally. + // 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. diff --git a/src/smt/theory_nseq.cpp b/src/smt/theory_nseq.cpp index 46673e91f..dee9aa4e9 100644 --- a/src/smt/theory_nseq.cpp +++ b/src/smt/theory_nseq.cpp @@ -33,7 +33,8 @@ namespace smt { m_arith_value(ctx.get_manager()), m_egraph(ctx.get_manager()), m_sgraph(ctx.get_manager(), m_egraph), - m_nielsen(m_sgraph), + m_context_solver(ctx.get_manager()), + 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) diff --git a/src/smt/theory_nseq.h b/src/smt/theory_nseq.h index 6e7be11b9..24f5ad566 100644 --- a/src/smt/theory_nseq.h +++ b/src/smt/theory_nseq.h @@ -28,6 +28,7 @@ Author: #include "smt/nseq_state.h" #include "smt/nseq_regex.h" #include "smt/nseq_model.h" +#include "smt/nseq_context_solver.h" namespace smt { @@ -38,6 +39,9 @@ namespace smt { arith_value m_arith_value; euf::egraph m_egraph; // private egraph (not shared with smt context) euf::sgraph m_sgraph; // private sgraph + // m_context_solver must be declared before m_nielsen: its address is passed + // to the m_nielsen constructor and must remain stable for the object's lifetime. + context_solver m_context_solver; seq::nielsen_graph m_nielsen; nseq_state m_state; nseq_regex m_regex; // regex membership pre-processing