From f7f2ee8f74d73a94265cba23f70baca7bb0a1ef3 Mon Sep 17 00:00:00 2001 From: CEisenhofer Date: Thu, 7 May 2026 15:49:16 +0200 Subject: [PATCH] Using only one solver --- src/smt/nseq_context_solver.h | 115 +++++++++++++++++++++++----------- src/smt/seq/seq_nielsen.cpp | 36 ++--------- src/smt/seq/seq_nielsen.h | 54 ++++++++-------- src/smt/seq_model.cpp | 33 +++++++--- src/smt/seq_model.h | 3 + src/smt/smt_setup.cpp | 1 + src/smt/theory_nseq.cpp | 19 +++++- src/smt/theory_nseq.h | 1 - 8 files changed, 154 insertions(+), 108 deletions(-) diff --git a/src/smt/nseq_context_solver.h b/src/smt/nseq_context_solver.h index c82161647..ed31478ec 100644 --- a/src/smt/nseq_context_solver.h +++ b/src/smt/nseq_context_solver.h @@ -11,6 +11,12 @@ Abstract: that delegates arithmetic feasibility checks to an smt::kernel configured with seq.solver = "seq_len". + Each call to assert_expr(e, dep) with a non-null dep creates a fresh + Boolean assumption literal `a` and asserts `a => e` into the kernel. + The literal-to-dep mapping is maintained across push/pop scopes. + After check() returns l_false, core() returns the joined dep_tracker + for all assumption literals that appear in the kernel's UNSAT core. + Author: Nikolaj Bjorner (nbjorner) 2026-03-10 @@ -22,6 +28,7 @@ Author: #include "smt/smt_kernel.h" #include "smt/smt_arith_value.h" #include "params/smt_params.h" +#include "util/map.h" namespace smt { @@ -29,11 +36,30 @@ 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. + * + * Assertions with a non-null dep_tracker are converted to assumption- + * literal form: a fresh bool `a` is introduced, `(or (not a) e)` is + * asserted, and the mapping a.id -> dep is tracked per push/pop scope. + * After an UNSAT check(), core() returns the union of the deps for the + * literals that appear in the kernel's UNSAT core. + * + * Assertions with dep == nullptr are asserted directly (always active). */ class context_solver : public seq::simple_solver { - smt_params m_params; // must be declared before m_kernel - kernel m_kernel; - arith_value m_arith_value; + smt_params m_params; // must be declared before m_kernel + kernel m_kernel; + arith_value m_arith_value; + + // Tracked assumption literals. + // m_assump_lits[i] and m_frame_bounds together encode a stack of + // frames, one frame per push(). pop(n) removes the top n frames. + expr_ref_vector m_assump_lits; // live assumption exprs + svector m_frame_bounds; // m_assump_lits.size() at each push() + u_map m_lid_to_dep; // literal expr-id -> dep + + // Scratch dep_manager for joining core deps; reset before each check(). + seq::dep_manager m_core_dep_mgr; + seq::dep_tracker m_last_core = nullptr; static smt_params make_seq_len_params() { smt_params p; @@ -45,39 +71,67 @@ namespace smt { context_solver(ast_manager& m) : m_params(make_seq_len_params()), m_kernel(m, m_params), - m_arith_value(m) { + m_arith_value(m), + m_assump_lits(m) { m_arith_value.init(&m_kernel.get_context()); } lbool check() override { - // std::cout << "Checking:\n"; - // for (int i = 0; i < m_kernel.size(); i++) { - // std::cout << "\t" << mk_pp(m_kernel.get_formula(i), m_kernel.m()) << std::endl; - // } - // std::cout << std::endl; - // std::cout << "Checking" << std::endl; - // for (unsigned i = 0; i < m_kernel.size(); i++) { - // std::cout << mk_pp(m_kernel.get_formula(i), m_kernel.m()) << std::endl; - // } - return m_kernel.check(); + m_core_dep_mgr.reset(); + m_last_core = nullptr; + lbool r; + if (m_assump_lits.empty()) { + r = m_kernel.check(); + } else { + r = m_kernel.check(m_assump_lits.size(), m_assump_lits.data()); + if (r == l_false) { + unsigned cnt = m_kernel.get_unsat_core_size(); + for (unsigned i = 0; i < cnt; ++i) { + expr* ce = m_kernel.get_unsat_core_expr(i); + seq::dep_tracker d = nullptr; + if (m_lid_to_dep.find(ce->get_id(), d)) + m_last_core = m_core_dep_mgr.mk_join(m_last_core, d); + } + } + } + return r; } - void assert_expr(expr* e) override { - m_kernel.assert_expr(e); + void assert_expr(expr* e, seq::dep_tracker dep) override { + if (!dep) { + m_kernel.assert_expr(e); + return; + } + ast_manager& m = m_kernel.m(); + expr_ref lit(m.mk_fresh_const("_a", m.mk_bool_sort()), m); + m_kernel.assert_expr(m.mk_or(m.mk_not(lit), e)); + m_lid_to_dep.insert_if_not_there(lit->get_id(), dep); + m_assump_lits.push_back(lit); } void push() override { m_kernel.push(); + m_frame_bounds.push_back((unsigned)m_assump_lits.size()); } - void pop(unsigned num_scopes) override { - m_kernel.pop(num_scopes); + void pop(unsigned n) override { + SASSERT(n <= m_frame_bounds.size()); + unsigned target = m_frame_bounds[m_frame_bounds.size() - n]; + while ((unsigned)m_assump_lits.size() > target) { + m_lid_to_dep.erase(m_assump_lits.back()->get_id()); + m_assump_lits.pop_back(); + } + for (unsigned i = 0; i < n; ++i) + m_frame_bounds.pop_back(); + m_kernel.pop(n); } void get_model(model_ref& mdl) override { m_kernel.get_model(mdl); } + seq::dep_tracker core() override { return m_last_core; } + bool lower_bound(expr* e, rational& lo) const override { bool is_strict = true; return m_arith_value.get_lo(e, lo, is_strict) && !is_strict && lo.is_int(); @@ -89,28 +143,17 @@ namespace smt { } bool current_value(expr* e, rational& v) const override { - return m_arith_value.get_value(e, v) && v.is_int(); - } - - lbool check_with_assumptions(expr_ref_vector& assumptions, expr_ref_vector& core) override { - // TODO: Not ideal - // Replay with assumptions - // std::cout << "Assuming" << std::endl; - // for (unsigned i = 0; i < assumptions.size(); i++) { - // std::cout << mk_pp(assumptions[i].get(), m_kernel.m()) << std::endl; - // } - lbool r = m_kernel.check(assumptions.size(), assumptions.data()); - unsigned cnt = m_kernel.get_unsat_core_size(); - core.resize(cnt); - for (unsigned i = 0; i < cnt; i++) { - core[i] = m_kernel.get_unsat_core_expr(i); - } - return r; - } + return m_arith_value.get_value(e, v) && v.is_int(); + } void reset() override { m_kernel.reset(); m_arith_value.init(&m_kernel.get_context()); + m_assump_lits.reset(); + m_frame_bounds.reset(); + m_lid_to_dep.reset(); + m_core_dep_mgr.reset(); + m_last_core = nullptr; } }; diff --git a/src/smt/seq/seq_nielsen.cpp b/src/smt/seq/seq_nielsen.cpp index b18c80c72..fffb15a72 100644 --- a/src/smt/seq/seq_nielsen.cpp +++ b/src/smt/seq/seq_nielsen.cpp @@ -414,13 +414,12 @@ namespace seq { // nielsen_graph // ----------------------------------------------- - nielsen_graph::nielsen_graph(euf::sgraph &sg, simple_solver &solver, simple_solver &core_solver): + nielsen_graph::nielsen_graph(euf::sgraph &sg, simple_solver &solver): m(sg.get_manager()), a(sg.get_manager()), m_seq(sg.get_seq_util()), m_sg(sg), m_solver(solver), - m_core_solver(core_solver), m_parikh(alloc(seq_parikh, sg)), m_seq_regex(alloc(seq::seq_regex, sg)) {} @@ -534,7 +533,6 @@ namespace seq { m_length_info.reset(); m_dep_mgr.reset(); m_solver.reset(); - m_core_solver.reset(); SASSERT(m_nodes.empty()); SASSERT(m_edges.empty()); SASSERT(m_root == nullptr); @@ -4438,7 +4436,7 @@ namespace seq { SASSERT(m_literal_if_false); for (unsigned i = node->m_parent_ic_count; i < node->constraints().size(); ++i) { auto& c = node->constraints()[i]; - m_solver.assert_expr(c.fml); + m_solver.assert_expr(c.fml, c.dep); auto lit = m_literal_if_false(c.fml); // std::cout << "Internalizing literal " << mk_pp(c.fml, m) << " [" << (lit == sat::null_literal) << "]" << std::endl; if (lit != sat::null_literal) @@ -4505,32 +4503,10 @@ namespace seq { return m_solver.check() != l_false; } - dep_tracker nielsen_graph::get_subsolver_dependency(nielsen_node* n) { - u_map expr_to_dep; - expr_ref_vector assumptions(m); - assumptions.resize(n->constraints().size()); - unsigned j = 0; - for (auto const &c : n->constraints()) { - if (expr_to_dep.contains(c.fml->get_id())) - continue; - expr_to_dep.insert_if_not_there(c.fml->get_id(), c.dep); - assumptions[j++] = c.fml; - } - assumptions.shrink(j); - expr_ref_vector core(m); - lbool res = m_core_solver.check_with_assumptions(assumptions, core); - CTRACE(seq, res != l_false, - tout << "Unexpected satisfiable/unknown result from core solver " - << res << " " << core - << "\nassumptions\n" - << assumptions << "\n"); - VERIFY(res == l_false); - - dep_tracker dep = dep_mgr().mk_empty(); - for (expr* e : core) { - dep = dep_mgr().mk_join(dep, expr_to_dep[e->get_id()]); - } - return dep; + dep_tracker nielsen_graph::get_subsolver_dependency(nielsen_node* /*n*/) { + // check_int_feasibility() already called m_solver.check() which computed + // the UNSAT core in terms of tracked assumption literals and their deps. + return m_solver.core(); } bool nielsen_graph::check_lp_le(expr* lhs, expr* rhs, nielsen_node* n, dep_tracker& dep) { diff --git a/src/smt/seq/seq_nielsen.h b/src/smt/seq/seq_nielsen.h index caa1d76da..3ddcb21b8 100644 --- a/src/smt/seq/seq_nielsen.h +++ b/src/smt/seq/seq_nielsen.h @@ -264,32 +264,6 @@ namespace seq { std::string snode_label_html(euf::snode const* n, ast_manager& m); - /** - * Abstract interface for an incremental solver used by nielsen_graph - * 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. When no solver is provided, - * integer feasibility checks are skipped (optimistically assumed feasible). - */ - class simple_solver { - public: - virtual ~simple_solver() {} - virtual lbool check() = 0; - virtual void assert_expr(expr* e) = 0; - virtual void push() = 0; - virtual void pop(unsigned num_scopes) = 0; - virtual void get_model(model_ref& mdl) { mdl = nullptr; } - virtual lbool check_with_assumptions(expr_ref_vector& assumptions, expr_ref_vector& core) { return l_undef; } - // Optional bound queries on arithmetic expressions (non-strict integer bounds). - // Default implementation reports "unsupported". - virtual bool lower_bound(expr* e, rational& lo) const { return false; } - virtual bool upper_bound(expr* e, rational& hi) const { return false; } - virtual bool current_value(expr *e, rational &v) const { return false; } - - virtual void reset() = 0; - }; - // simplification result for constraint processing // mirrors ZIPT's SimplifyResult enum enum class simplify_result { @@ -362,6 +336,31 @@ namespace seq { // nullptr represents the empty dependency set. using dep_tracker = dep_manager::dependency*; + /** + * Abstract interface for an incremental solver used by nielsen_graph + * 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. When no solver is provided, + * integer feasibility checks are skipped (optimistically assumed feasible). + */ + class simple_solver { + public: + virtual ~simple_solver() {} + virtual lbool check() = 0; + virtual void assert_expr(expr* e, dep_tracker dep = nullptr) = 0; + virtual void push() = 0; + virtual void pop(unsigned num_scopes) = 0; + virtual void get_model(model_ref& mdl) { mdl = nullptr; } + virtual dep_tracker core() { return nullptr; } + // Optional bound queries on arithmetic expressions (non-strict integer bounds). + // Default implementation reports "unsupported". + virtual bool lower_bound(expr* e, rational& lo) const { return false; } + virtual bool upper_bound(expr* e, rational& hi) const { return false; } + virtual bool current_value(expr* e, rational& v) const { return false; } + virtual void reset() = 0; + }; + // partition dep_source leaves from deps into enode pairs, sat literals, // and arithmetic <= dependencies. void deps_to_lits(dep_tracker deps, @@ -852,7 +851,6 @@ namespace seq { // and optimistically assumes feasibility. // ----------------------------------------------- simple_solver& m_solver; - simple_solver& m_core_solver; // Constraint.Shared: guards re-assertion of root-level constraints. // Set to true after assert_root_constraints_to_solver() is first called. @@ -895,7 +893,7 @@ namespace seq { public: // 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, simple_solver &core_solver); + nielsen_graph(euf::sgraph& sg, simple_solver& solver); ~nielsen_graph(); void set_literal_if_false(std::function const& lif) { diff --git a/src/smt/seq_model.cpp b/src/smt/seq_model.cpp index 7fd890813..180bb1415 100644 --- a/src/smt/seq_model.cpp +++ b/src/smt/seq_model.cpp @@ -479,6 +479,26 @@ namespace smt { return val; } + // Gets the arithmetic value of e. In QF_SLIA mode theory_lra does not register + // numeral constants as LP variables, so get_value_equiv misses cases like + // (str.len w) being equivalent to numeral 5 via EUF. Walking the EUF class + // and checking for numerals directly handles this. + bool seq_model::get_arith_value(expr* e, rational& val) const { + if (!m_ctx.e_internalized(e)) + return false; + arith_util a(m); + enode* root = m_ctx.get_enode(e); + enode* it = root; + do { + if (a.is_numeral(it->get_expr(), val)) + return true; + it = it->get_next(); + } while (it != root); + arith_value avalue(m); + avalue.init(const_cast(&m_ctx)); + return avalue.get_value_equiv(e, val); + } + rational seq_model::int_value(expr *_e) { expr_ref e(_e, m); m_ctx.get_rewriter()(e); @@ -487,9 +507,7 @@ namespace smt { if (a.is_numeral(e, val)) return val; - arith_value avalue(m); - avalue.init(&m_ctx); - bool has_val = avalue.get_value(e, val); + bool has_val = get_arith_value(e, val); CTRACE(seq, !has_val, tout << "no value associated with " << mk_pp(e, m) << "\n";); return val; } @@ -508,11 +526,9 @@ namespace smt { SASSERT(re_expr); arith_util arith(m); - arith_value avalue(m); - avalue.init(&m_ctx); expr_ref len_expr(m_seq.str.mk_length(var->get_expr()), m); rational len_val; - bool has_len = avalue.get_value(len_expr, len_val); + bool has_len = get_arith_value(len_expr, len_val); CTRACE(seq, !has_len, tout << "no value associated with " << mk_pp(len_expr, m) << "\n";); if (has_len && len_val.is_unsigned()) { @@ -539,10 +555,7 @@ namespace smt { arith_util arith(m); expr_ref len_expr(m_seq.str.mk_length(var->get_expr()), m); rational len_val; - - arith_value avalue(m); - avalue.init(&m_ctx); - bool has_len = avalue.get_value(len_expr, len_val); + bool has_len = get_arith_value(len_expr, len_val); CTRACE(seq, !has_len, tout << "no value associated with " << mk_pp(len_expr, m) << "\n";); diff --git a/src/smt/seq_model.h b/src/smt/seq_model.h index 3ae371d7a..d8bce09da 100644 --- a/src/smt/seq_model.h +++ b/src/smt/seq_model.h @@ -137,6 +137,9 @@ namespace smt { // extract integer value for an expression. rational int_value(expr *e); + // Get arithmetic value via EUF equivalence class, including numeral check. + bool get_arith_value(expr* e, rational& val) const; + }; } diff --git a/src/smt/smt_setup.cpp b/src/smt/smt_setup.cpp index c6811d41e..ea70866fd 100644 --- a/src/smt/smt_setup.cpp +++ b/src/smt/smt_setup.cpp @@ -796,6 +796,7 @@ namespace smt { } void setup::setup_nseq() { + setup_lra_arith(); // Avoid problems when querying length values when having QF_S(LIA) m_context.register_plugin(alloc(smt::theory_nseq, m_context)); setup_char(); } diff --git a/src/smt/theory_nseq.cpp b/src/smt/theory_nseq.cpp index 620dc2c87..e2f2eca22 100644 --- a/src/smt/theory_nseq.cpp +++ b/src/smt/theory_nseq.cpp @@ -34,8 +34,7 @@ namespace smt { m_egraph(m), m_sgraph(m, m_egraph), m_context_solver(m), - m_core_solver(m), - m_nielsen(m_sgraph, m_context_solver, m_core_solver), + m_nielsen(m_sgraph, m_context_solver), m_axioms(m_th_rewriter), m_regex(m_sgraph), m_model(m, ctx, m_seq, m_rewriter, m_sgraph), @@ -1267,6 +1266,19 @@ namespace smt { // ----------------------------------------------------------------------- bool theory_nseq::get_num_value(expr* e, rational& val) const { + // In QF_SLIA mode theory_lra does not register numeral constants as LP + // variables, so get_value_equiv misses cases where a term is only known + // through an EUF equality with a numeral (e.g. (str.len w) = 5). + // Walk the equivalence class directly first. + if (get_context().e_internalized(e)) { + enode* root = get_context().get_enode(e); + enode* it = root; + do { + if (m_autil.is_numeral(it->get_expr(), val) && val.is_int()) + return true; + it = it->get_next(); + } while (it != root); + } return m_arith_value.get_value_equiv(e, val) && val.is_int(); } @@ -1650,7 +1662,8 @@ namespace smt { continue; rational val_l; - VERIFY(m_arith_value.get_value(len_expr, val_l)); + if (!get_num_value(len_expr, val_l)) + continue; SASSERT(val_l.is_unsigned()); diff --git a/src/smt/theory_nseq.h b/src/smt/theory_nseq.h index 41f36d2c6..35e07d1e7 100644 --- a/src/smt/theory_nseq.h +++ b/src/smt/theory_nseq.h @@ -45,7 +45,6 @@ namespace smt { // 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; - context_solver m_core_solver; seq::nielsen_graph m_nielsen; seq::axioms m_axioms; seq::seq_regex m_regex; // regex membership pre-processing