From 0d1ee09e62602dd2788529a49c10d35624d17ba5 Mon Sep 17 00:00:00 2001 From: CEisenhofer Date: Tue, 19 May 2026 15:33:20 +0200 Subject: [PATCH] Keep most of the Nielsen graph and do a hot-restart when only external literals changed --- src/smt/seq/seq_nielsen.cpp | 4 +- src/smt/seq/seq_nielsen.h | 16 +++- src/smt/theory_nseq.cpp | 144 +++++++++++++++++++++--------------- 3 files changed, 99 insertions(+), 65 deletions(-) diff --git a/src/smt/seq/seq_nielsen.cpp b/src/smt/seq/seq_nielsen.cpp index 183dd7dc9..778ea6c72 100644 --- a/src/smt/seq/seq_nielsen.cpp +++ b/src/smt/seq/seq_nielsen.cpp @@ -1654,9 +1654,7 @@ namespace seq { try { ++m_stats.m_num_solve_calls; - m_sat_node = nullptr; - m_sat_path.reset(); - m_conflict_sources.reset(); + clear_sat_node(); TRACE(seq, tout << "Solve call " << m_stats.m_num_solve_calls << "\n"); diff --git a/src/smt/seq/seq_nielsen.h b/src/smt/seq/seq_nielsen.h index 940448565..da4e7ee03 100644 --- a/src/smt/seq/seq_nielsen.h +++ b/src/smt/seq/seq_nielsen.h @@ -640,6 +640,8 @@ namespace seq { vector const& constraints() const { return m_constraints; } vector& constraints() { return m_constraints; } + bool is_external_conflict() const { return m_conflict_external_literal != sat::null_literal; } + sat::literal get_external_conflict_literal() const { return m_conflict_external_literal; } // Query current bounds for a variable from the arithmetic subsolver. @@ -653,8 +655,6 @@ namespace seq { u_map> const &char_ranges() const { return m_char_ranges; } - - // add a character range constraint for a symbolic char. // intersects with existing range; sets conflict if result is empty. @@ -674,7 +674,7 @@ namespace seq { } bool is_extended() const { return m_is_extended; } - void set_extended(bool v) { + void set_extended(const bool v) { m_is_extended = v; } @@ -710,7 +710,7 @@ namespace seq { m_conflict_external_literal = sat::null_literal; } - void set_external_conflict(sat::literal lit, dep_tracker confl) { + void set_external_conflict(const sat::literal lit, dep_tracker confl) { if (m_reason != backtrack_reason::unevaluated) return; TRACE(seq, tout << "external conflict " << lit << "\n"); @@ -933,9 +933,17 @@ namespace seq { nielsen_node* sat_node() const { return m_sat_node; } void set_sat_node(nielsen_node* n) { SASSERT(n); + SASSERT(!m_sat_node); + SASSERT(m_sat_path.empty()); m_sat_node = n; } + void clear_sat_node() { + m_sat_node = nullptr; + m_sat_path.clear(); + m_conflict_sources.reset(); + } + // creates a new root for the graph void create_root() { SASSERT(!root()); diff --git a/src/smt/theory_nseq.cpp b/src/smt/theory_nseq.cpp index c41ebf359..54d1ec52b 100644 --- a/src/smt/theory_nseq.cpp +++ b/src/smt/theory_nseq.cpp @@ -22,6 +22,8 @@ Author: #include "util/statistics.h" #include "util/trail.h" +#include + namespace smt { theory_nseq::theory_nseq(context& ctx) : @@ -682,65 +684,90 @@ namespace smt { } // Fast path: if no new string eq/mem arrived and no scope was popped - // since the last successful solve, the Nielsen graph and the chosen - // SAT leaf are identical to what we would rebuild. All of the leaf's - // arithmetic side-constraints are already assigned true by the outer - // solver, so the model is valid — skip the rebuild and re-solve. - if (m_nielsen.sat_node() != nullptr && - m_solved_gen == m_constraint_gen && - !m_nielsen_literals.empty() && - all_of(m_nielsen_literals, [&](auto lit) { return l_true == ctx.get_assignment(lit); })) { - ++m_num_sat_revalidations; - TRACE(seq, tout << "nseq final_check: revalidated cached SAT path, skipping rebuild\n"); - if (!check_length_coherence()) return FC_CONTINUE; - if (!check_stoi_coherence()) return FC_CONTINUE; - if (!has_unhandled_preds()) return FC_DONE; - return FC_GIVEUP; + // since the last successful solve, the Nielsen graph can be (at least) + // partially be reused + if (m_solved_gen == m_constraint_gen) { + // SAT leaf are identical to what we would rebuild. All of the leaf's + // arithmetic side-constraints are already assigned true by the outer + // solver, so the model is valid — skip the rebuild and re-solve. + if (m_nielsen.sat_node() != nullptr && + !m_nielsen_literals.empty() && + all_of(m_nielsen_literals, [&](auto lit) { return l_true == ctx.get_assignment(lit); })) { + ++m_num_sat_revalidations; + TRACE(seq, tout << "nseq final_check: revalidated cached SAT path, skipping rebuild\n"); + if (!check_length_coherence()) return FC_CONTINUE; + if (!check_stoi_coherence()) return FC_CONTINUE; + if (!has_unhandled_preds()) return FC_DONE; + return FC_GIVEUP; + } + // fall through - no reason to rebuild the Nielsen graph + // everything that is not a general conflict needs to be recomputed + // but we can keep the general conflicts (which can be a lot!) + 1 == 1; + 0 == 0; + std::stack to_visit; + to_visit.push(m_nielsen.root()); + while (!to_visit.empty()) { + seq::nielsen_node* node = to_visit.top(); + to_visit.pop(); + if (node->is_general_conflict()) + // all its children are general conflicts as well - nothing to do + continue; + if (node->is_external_conflict()) + node->clear_local_conflict(); + + for (auto& child : node->outgoing()) { + to_visit.push(child->tgt()); + } + } + m_nielsen.clear_sat_node(); } + else { + // let's rebuild the whole Nielsen graph + populate_nielsen_graph(); - populate_nielsen_graph(); - - // assert length constraints derived from string equalities - if (assert_length_constraints()) { - TRACE(seq, tout << "nseq final_check: length constraints asserted, FC_CONTINUE\n"); - return FC_CONTINUE; - } - - SASSERT(m_nielsen.root()); - - m_nielsen.assert_node_new_int_constraints(m_nielsen.root()); - - ++m_num_final_checks; - - m_nielsen.set_max_search_depth(get_fparams().m_nseq_max_depth); - m_nielsen.set_max_nodes(get_fparams().m_nseq_max_nodes); - m_nielsen.set_parikh_enabled(get_fparams().m_nseq_parikh); - m_nielsen.set_signature_split(get_fparams().m_nseq_signature); - m_nielsen.set_regex_factorization_threshold(get_fparams().m_nseq_regex_factorization_threshold); - - SASSERT(!m_nielsen.root()->is_currently_conflict()); - - // Regex membership pre-check: before running DFS, check intersection - // emptiness for each variable's regex constraints. This handles - // regex-only problems that the DFS cannot efficiently solve. - if (!m_nielsen.root()->is_currently_conflict() && get_fparams().m_nseq_regex_precheck) { - switch (check_regex_memberships_precheck()) { - case l_true: - // conflict was asserted inside check_regex_memberships_precheck - TRACE(seq, tout << "nseq final_check: regex precheck UNSAT\n"); + // assert length constraints derived from string equalities + if (assert_length_constraints()) { + TRACE(seq, tout << "nseq final_check: length constraints asserted, FC_CONTINUE\n"); return FC_CONTINUE; - case l_false: - // all regex constraints satisfiable, no word eqs → SAT - TRACE(seq, tout << "nseq final_check: regex precheck SAT\n"); - m_nielsen.set_sat_node(m_nielsen.root()); - if (!check_length_coherence()) + } + + SASSERT(m_nielsen.root()); + + m_nielsen.assert_node_new_int_constraints(m_nielsen.root()); + + ++m_num_final_checks; + + m_nielsen.set_max_search_depth(get_fparams().m_nseq_max_depth); + m_nielsen.set_max_nodes(get_fparams().m_nseq_max_nodes); + m_nielsen.set_parikh_enabled(get_fparams().m_nseq_parikh); + m_nielsen.set_signature_split(get_fparams().m_nseq_signature); + m_nielsen.set_regex_factorization_threshold(get_fparams().m_nseq_regex_factorization_threshold); + + SASSERT(!m_nielsen.root()->is_currently_conflict()); + + // Regex membership pre-check: before running DFS, check intersection + // emptiness for each variable's regex constraints. This handles + // regex-only problems that the DFS cannot efficiently solve. + if (!m_nielsen.root()->is_currently_conflict() && get_fparams().m_nseq_regex_precheck) { + switch (check_regex_memberships_precheck()) { + case l_true: + // conflict was asserted inside check_regex_memberships_precheck + TRACE(seq, tout << "nseq final_check: regex precheck UNSAT\n"); return FC_CONTINUE; - if (!check_stoi_coherence()) - return FC_CONTINUE; - TRACE(seq, tout << "pre-check done\n"); - return FC_DONE; - default: - break; + case l_false: + // all regex constraints satisfiable, no word eqs → SAT + TRACE(seq, tout << "nseq final_check: regex precheck SAT\n"); + m_nielsen.set_sat_node(m_nielsen.root()); + if (!check_length_coherence()) + return FC_CONTINUE; + if (!check_stoi_coherence()) + return FC_CONTINUE; + TRACE(seq, tout << "pre-check done\n"); + return FC_DONE; + default: + break; + } } } @@ -757,6 +784,10 @@ namespace smt { // std::cout << "Got: " << (result == seq::nielsen_graph::search_result::sat ? "sat" : (result == seq::nielsen_graph::search_result::unsat ? "unsat" : "unknown")) << std::endl; #endif + // Snapshot generation so the fast path can skip a full rebuild + // on the next call if no new constraints arrive in the meantime. + m_solved_gen = m_constraint_gen; + if (result == seq::nielsen_graph::search_result::unsat) { IF_VERBOSE(1, verbose_stream() << "nseq final_check: solve UNSAT\n";); TRACE(seq, tout << "nseq final_check: solve UNSAT\n"); @@ -773,9 +804,6 @@ namespace smt { SASSERT(has_eq_or_mem); // we should have axiomatized them bool all_sat = add_nielsen_assumptions(); - // Snapshot generation so the fast path can skip a full rebuild - // on the next call if no new constraints arrive in the meantime. - m_solved_gen = m_constraint_gen; if (!check_length_coherence()) return FC_CONTINUE;