From e983bc76d41df92bcd0fe580495abb188fdb98c6 Mon Sep 17 00:00:00 2001 From: CEisenhofer Date: Sat, 27 Jun 2026 12:53:57 +0200 Subject: [PATCH] Try to do some processing already during assignments --- src/params/smt_params.cpp | 1 + src/params/smt_params.h | 1 + src/params/smt_params_helper.pyg | 1 + src/smt/seq/seq_nielsen.cpp | 113 +++++++++++++++++++++++++++++++ src/smt/seq/seq_nielsen.h | 39 +++++++++++ src/smt/theory_nseq.cpp | 89 ++++++++++++++++++++++++ src/smt/theory_nseq.h | 12 ++++ 7 files changed, 256 insertions(+) diff --git a/src/params/smt_params.cpp b/src/params/smt_params.cpp index 03b4795dd3..597a253f26 100644 --- a/src/params/smt_params.cpp +++ b/src/params/smt_params.cpp @@ -62,6 +62,7 @@ void smt_params::updt_local_params(params_ref const & _p) { m_nseq_regex_factorization_eager = p.nseq_regex_factorization_eager(); m_nseq_signature = p.nseq_signature(); m_nseq_axiomatize_diseq = p.nseq_axiomatize_diseq(); + m_nseq_eager = p.nseq_eager(); m_up_persist_clauses = p.up_persist_clauses(); validate_string_solver(m_string_solver); if (_p.get_bool("arith.greatest_error_pivot", false)) diff --git a/src/params/smt_params.h b/src/params/smt_params.h index 174016bb26..729d502962 100644 --- a/src/params/smt_params.h +++ b/src/params/smt_params.h @@ -257,6 +257,7 @@ struct smt_params : public preprocessor_params, bool m_nseq_regex_factorization_eager = false; bool m_nseq_signature = false; bool m_nseq_axiomatize_diseq = false; + bool m_nseq_eager = true; smt_params(params_ref const & p = params_ref()): m_string_solver(symbol("auto")){ diff --git a/src/params/smt_params_helper.pyg b/src/params/smt_params_helper.pyg index 54848eb599..d64c946ffb 100644 --- a/src/params/smt_params_helper.pyg +++ b/src/params/smt_params_helper.pyg @@ -141,6 +141,7 @@ def_module_params(module_name='smt', ('nseq.regex_factorization_eager', BOOL, False, 'apply regex factorization (sigma splitting) eagerly in the theory interface (propagate_pos_mem) instead of lazily inside the Nielsen graph'), ('nseq.signature', BOOL, False, 'enable heuristic signature-based string equation splitting in Nielsen solver'), ('nseq.axiomatize_diseq', BOOL, False, 'eagerly axiomatize sequence disequalities'), + ('nseq.eager', BOOL, True, 'enable the incremental eager structural Nielsen closure during propagation, detecting conflicts before final_check'), ('core.validate', BOOL, False, '[internal] validate unsat core produced by SMT context. This option is intended for debugging'), ('seq.split_w_len', BOOL, True, 'enable splitting guided by length constraints'), ('seq.validate', BOOL, False, 'enable self-validation of theory axioms created by seq theory'), diff --git a/src/smt/seq/seq_nielsen.cpp b/src/smt/seq/seq_nielsen.cpp index 00db498a3b..6faf0f1aed 100644 --- a/src/smt/seq/seq_nielsen.cpp +++ b/src/smt/seq/seq_nielsen.cpp @@ -674,6 +674,9 @@ namespace seq { m_explored_automaton.reset(); m_unsat_node_cache.clear(); m_num_cache_hits = 0; + m_eager_active = false; + m_eager_leaf = nullptr; + m_eager_substs.reset(); // m_length_trail.reset(); // m_length_info.reset(); m_dep_mgr.reset(); @@ -1985,6 +1988,115 @@ namespace seq { } } + void nielsen_graph::eager_begin() { + reset(); + create_root(); + m_eager_leaf = m_root; + m_eager_substs.reset(); + m_eager_active = true; + } + + euf::snode const* nielsen_graph::eager_rewrite(euf::snode const* s, dep_tracker& dep) { + for (auto const& sub : m_eager_substs) { + s = m_sg.subst(s, sub.m_var, sub.m_replacement); + dep = m_dep_mgr.mk_join(dep, sub.m_dep); + } + return s; + } + + void nielsen_graph::eager_add_str_eq(euf::snode const* lhs, euf::snode const* rhs, smt::enode* l, smt::enode* r) { + SASSERT(m_eager_active && m_eager_leaf); + dep_tracker dep = m_dep_mgr.mk_leaf(enode_pair(l, r)); + lhs = eager_rewrite(lhs, dep); + rhs = eager_rewrite(rhs, dep); + str_eq eq(lhs, rhs, dep); + eq.sort(); + m_eager_leaf->add_str_eq(eq); + } + + void nielsen_graph::eager_add_str_deq(euf::snode const* lhs, euf::snode const* rhs, sat::literal lit) { + SASSERT(m_eager_active && m_eager_leaf); + dep_tracker dep = m_dep_mgr.mk_leaf(lit); + lhs = eager_rewrite(lhs, dep); + rhs = eager_rewrite(rhs, dep); + m_eager_leaf->add_str_deq(str_deq(lhs, rhs, dep)); + } + + void nielsen_graph::eager_add_str_mem(euf::snode const* str, euf::snode const* regex, sat::literal lit) { + SASSERT(m_eager_active && m_eager_leaf); + dep_tracker dep = m_dep_mgr.mk_leaf(lit); + str = eager_rewrite(str, dep); + regex = eager_rewrite(regex, dep); // no-op for ground regexes, mirrors apply_subst + m_eager_leaf->add_str_mem(str_mem(str, regex, dep)); + } + + // Drive the deterministic chain from the current leaf to a fixpoint. Each step + // is a single-child apply_det_modifier (progress, strictly token-reducing), so + // this terminates without a budget. An EMPTY path makes simplify_and_init take + // only its assignment-independent branches (LP/arith passes 3c-else/3e are gated + // on !cur_path.empty()); no arithmetic/length solver is touched. + nielsen_graph::search_result nielsen_graph::eager_close() { + SASSERT(m_eager_active && m_eager_leaf); + ++m_stats.m_num_eager_calls; + ptr_vector empty_path; + + // Rigid defined ops (str.replace_all, …) must never be Nielsen-substituted; + // a rigid term is inherited down the whole chain, so a single check on the + // leaf (which holds all current constraints) suffices — bail before any det + // step (mirrors final_check's guard). + if (m_eager_leaf->references_rigid()) + return search_result::unknown; + + auto report_conflict = [&](nielsen_node* n) { + // The conflict node's deps already transitively include the source deps + // of every constraint that fed it (apply_subst + eager_rewrite join the + // substitution deps). We must NOT use collect_conflict_deps() — it walks + // from the root and asserts every visited node is a conflict, but only + // the chain's last node is. + dep_tracker deps = nullptr; + if (n->m_conflict_external_literal != sat::null_literal) + deps = m_dep_mgr.mk_join(deps, m_dep_mgr.mk_leaf(n->m_conflict_external_literal)); + if (n->m_conflict_internal) + deps = m_dep_mgr.mk_join(deps, n->m_conflict_internal); + m_conflict_sources.reset(); + m_dep_mgr.linearize(deps, m_conflict_sources); + }; + + while (true) { + if (!m.inc()) + return search_result::unknown; + nielsen_node* node = m_eager_leaf; + + // a substitution applied in the previous step may have produced a + // conflict directly (e.g. an empty character-range intersection) + if (node->is_currently_conflict()) { + report_conflict(node); + return search_result::unsat; + } + + const simplify_result sr = node->simplify_and_init(empty_path); + if (sr == simplify_result::conflict || node->is_currently_conflict()) { + report_conflict(node); + return search_result::unsat; + } + if (sr == simplify_result::satisfied || node->is_satisfied()) + return search_result::unknown; // no eager conflict; defer to solve() + + // deterministic, single-child substitution closure. apply_det_modifier + // only acts on word equations; membership-only structural conflicts are + // already caught by simplify_and_init's post-passes above. + if (!apply_det_modifier(node)) + return search_result::unknown; // would need branching; stop here + + // record the det substitution(s) and advance the leaf + SASSERT(!node->outgoing().empty()); + nielsen_edge* e = node->outgoing().back(); + for (auto const& s : e->subst()) + m_eager_substs.push_back(s); + m_eager_leaf = e->tgt(); + } + } + // ---- Transposition-table helpers (node memoization) ---------------------- static bool reason_is_string_only(backtrack_reason r) { @@ -5264,6 +5376,7 @@ namespace seq { void nielsen_graph::collect_statistics(::statistics& st) const { st.update("nseq solve calls", m_stats.m_num_solve_calls); + st.update("nseq eager calls", m_stats.m_num_eager_calls); st.update("nseq dfs nodes", m_stats.m_num_dfs_nodes); st.update("nseq sat", m_stats.m_num_sat); st.update("nseq unsat", m_stats.m_num_unsat); diff --git a/src/smt/seq/seq_nielsen.h b/src/smt/seq/seq_nielsen.h index c6658f18a9..ebc05d682e 100644 --- a/src/smt/seq/seq_nielsen.h +++ b/src/smt/seq/seq_nielsen.h @@ -682,6 +682,7 @@ namespace seq { // search statistics collected during Nielsen graph solving struct nielsen_stats { unsigned m_num_solve_calls = 0; + unsigned m_num_eager_calls = 0; unsigned m_num_dfs_nodes = 0; unsigned m_num_sat = 0; unsigned m_num_unsat = 0; @@ -841,6 +842,18 @@ namespace seq { std::set> m_unsat_node_cache; unsigned m_num_cache_hits = 0; + // Incremental eager-closure chain state (see eager_begin / eager_close). + // The chain is a single deterministic path root → … → m_eager_leaf; + // m_eager_substs is its composed substitution (root→leaf order), applied to + // late-arriving constraints so they land in leaf coordinates. + bool m_eager_active = false; + nielsen_node* m_eager_leaf = nullptr; + vector m_eager_substs; + + // apply the accumulated chain substitution to a single snode, joining the + // substitutions' deps into `dep`. + euf::snode const* eager_rewrite(euf::snode const* s, dep_tracker& dep); + public: // Construct with a caller-supplied solver. Ownership is NOT transferred; @@ -956,6 +969,32 @@ namespace seq { // main search entry point: iterative deepening DFS search_result solve(); + // ---- Incremental eager structural closure ----------------------------- + // The deterministic Nielsen chain is grown incrementally as constraints + // arrive (driven by theory_nseq::eager_structural_check), so we do NOT + // rebuild from scratch on every propagation. Lifecycle: + // eager_begin() — start a fresh chain (reset + root + empty subst); + // eager_add_str_*() — fold one new constraint into the current LEAF, + // rewriting it through the chain's accumulated + // substitution so it lands in leaf coordinates; + // eager_close() — drive simplify_and_init (EMPTY path ⇒ no LP/arith + // passes) + single-child apply_det_modifier from the + // leaf to a fixpoint, extending the chain. + // Returns unsat (conflict_sources() = the conflict node's own deps) on a + // purely structural contradiction (symbol clash / empty-side / regex fail / + // widening); unknown otherwise. Sound for early-conflict detection because + // the current set is a SUBSET of any completion. Bails on + // references_rigid() (det substitution of a rigid defined op is unsound). + // reset()/pop (eager_invalidate) discard the chain; never declares SAT. + bool eager_active() const { return m_eager_active && m_root != nullptr; } + void eager_begin(); + void eager_invalidate() { m_eager_active = false; m_eager_leaf = nullptr; m_eager_substs.reset(); } + nielsen_node* eager_leaf() const { return m_eager_leaf; } + void eager_add_str_eq(euf::snode const* lhs, euf::snode const* rhs, smt::enode* l, smt::enode* r); + void eager_add_str_deq(euf::snode const* lhs, euf::snode const* rhs, sat::literal lit); + void eager_add_str_mem(euf::snode const* str, euf::snode const* regex, sat::literal lit); + search_result eager_close(); + // generate child nodes by applying modifier rules // returns true if at least one child was generated bool generate_extensions(nielsen_node *node); diff --git a/src/smt/theory_nseq.cpp b/src/smt/theory_nseq.cpp index 20a43f5c57..96263acf77 100644 --- a/src/smt/theory_nseq.cpp +++ b/src/smt/theory_nseq.cpp @@ -227,6 +227,7 @@ namespace smt { m_prop_queue.push_back(eq_item(s1, s2, get_enode(v1), get_enode(v2), dep)); m_last_constraint_added = ctx.get_scope_level(); m_can_hot_restart = false; + ++m_eager_dirty; } catch(const std::exception&) { #ifdef Z3DEBUG @@ -274,6 +275,7 @@ namespace smt { m_prop_queue.push_back(deq_item(s1, s2, ~ctx.get_literal(eq_expr), dep)); m_last_constraint_added = ctx.get_scope_level(); m_can_hot_restart = false; + ++m_eager_dirty; } } else @@ -300,6 +302,7 @@ namespace smt { m_prop_queue.push_back(mem_item(sn_str, sn_re, lit, dep)); m_last_constraint_added = ctx.get_scope_level(); m_can_hot_restart = false; + ++m_eager_dirty; } else { // ¬(str ∈ R) ≡ str ∈ complement(R): store as a positive membership @@ -311,6 +314,7 @@ namespace smt { m_prop_queue.push_back(mem_item(sn_str, sn_re_compl, lit, dep)); m_last_constraint_added = ctx.get_scope_level(); m_can_hot_restart = false; + ++m_eager_dirty; } } else if (m_seq.str.is_prefix(e)) { @@ -429,6 +433,11 @@ namespace smt { try { theory::pop_scope_eh(num_scopes); m_sg.pop(num_scopes); + // The sgraph pop released snodes the incremental eager chain references; + // discard it so the next eager run rebuilds rather than extending a + // dangling chain (see eager_structural_check). + m_nielsen.eager_invalidate(); + m_eager_processed = 0; // A pop may remove constraints and/or unassign forced Nielsen // literals; conservatively invalidate the cached SAT path. if (m_can_hot_restart && ctx.get_scope_level() - num_scopes < m_last_constraint_added) @@ -484,6 +493,13 @@ namespace smt { UNREACHABLE(); } } + + // Eager structural pruning: once the queue is drained, run a cheap + // branch-free Nielsen closure over the currently-asserted constraints to + // surface structural conflicts long before final_check. Sound because + // the current set is a subset of any completion (see eager_structural_check). + if (!ctx.inconsistent()) + eager_structural_check(); } catch(const std::exception&) { #ifdef Z3DEBUG @@ -493,6 +509,78 @@ namespace smt { } } + // Rebuild-don't-undo, INCREMENTALLY: rather than maintaining the full Nielsen + // graph along the DPLL(T) trail (the error-prone undo bookkeeping that sank the + // earlier manual engine), we grow a single deterministic chain in `m_nielsen` as + // constraints arrive — each new constraint is folded into the current leaf with + // the chain's accumulated substitution applied (`eager_add_*`), then the chain is + // extended (`eager_close`). No per-propagation rebuild. Any structural UNSAT is + // a real conflict (subset-monotonicity); we never declare SAT or short-circuit + // final_check. The chain is discarded on pop (`eager_invalidate`) and whenever + // `m_nielsen.reset()` runs (e.g. final_check's `populate_nielsen_graph`), after + // which it is rebuilt from scratch on the next call. + void theory_nseq::eager_structural_check() { + if (!get_fparams().m_nseq_eager) + return; + // Only re-run when the Nielsen-relevant constraint set actually grew. + if (m_eager_dirty == m_eager_seen) + return; + m_eager_seen = m_eager_dirty; + + // (Re)start the chain if it was discarded (first call, after a pop, or after + // final_check reset m_nielsen). + if (!m_nielsen.eager_active()) { + m_nielsen.eager_begin(); + m_eager_processed = 0; + m_can_hot_restart = false; // m_nielsen now holds the eager chain + } + + // Fold newly-arrived prop-queue items into the current leaf. Membership + // handling mirrors populate_nielsen_graph (trivial check, ignored skip, + // ground-prefix consumption via process_str_mem). + for (; m_eager_processed < m_prop_queue.size(); ++m_eager_processed) { + auto const& item = m_prop_queue[m_eager_processed]; + if (std::holds_alternative(item)) { + auto const& eq = std::get(item); + m_nielsen.eager_add_str_eq(eq.m_lhs, eq.m_rhs, eq.m_l, eq.m_r); + } + else if (std::holds_alternative(item)) { + auto const& dq = std::get(item); + m_nielsen.eager_add_str_deq(dq.m_lhs, dq.m_rhs, dq.lit); + } + else if (std::holds_alternative(item)) { + auto const& mem = std::get(item); + int triv = m_regex.check_trivial(mem); + if (triv > 0) + continue; // trivially satisfied + if (triv < 0) { + m_nielsen.eager_add_str_mem(mem.m_str, mem.m_regex, mem.lit); + continue; + } + if (m_ignored_mem.contains(mem.lit)) + continue; // already handled via Boolean closure + vector processed; + if (!m_regex.process_str_mem(mem, processed)) { + m_nielsen.eager_add_str_mem(mem.m_str, mem.m_regex, mem.lit); + continue; + } + for (auto const& pm : processed) + m_nielsen.eager_add_str_mem(pm.m_str, pm.m_regex, mem.lit); + } + // axiom_item: not Nielsen-relevant, skip + } + + const auto r = m_nielsen.eager_close(); + if (r == seq::nielsen_graph::search_result::unsat) { + IF_VERBOSE(1, verbose_stream() << "nseq eager: structural conflict\n";); + TRACE(seq, tout << "nseq eager: structural conflict\n"); + ++m_num_eager_conflicts; + explain_nielsen_conflict(); // reads conflict_sources() + root, then sets the conflict + } + // Keep the chain for the next propagation (incremental). It is discarded by + // pop_scope_eh / final_check's reset, never here. + } + void theory_nseq::propagate_eq(tracked_str_eq const &eq) const { // When s1 = s2 is learned, ensure len(s1) and len(s2) are // internalized so congruence closure propagates len(s1) = len(s2). @@ -1289,6 +1377,7 @@ namespace smt { void theory_nseq::collect_statistics(::statistics& st) const { st.update("nseq conflicts", m_num_conflicts); + st.update("nseq eager conflicts", m_num_eager_conflicts); st.update("nseq final checks", m_num_final_checks); st.update("nseq sat revalidations", m_num_sat_revalidations); st.update("nseq length axioms", m_num_length_axioms); diff --git a/src/smt/theory_nseq.h b/src/smt/theory_nseq.h index 499d2017c1..78a4bb5446 100644 --- a/src/smt/theory_nseq.h +++ b/src/smt/theory_nseq.h @@ -77,8 +77,19 @@ namespace smt { unsigned m_last_constraint_added = 0; bool m_can_hot_restart = false; + // Eager structural pre-check (see eager_structural_check): m_eager_dirty is + // a monotone counter bumped whenever a Nielsen-relevant constraint (word eq, + // diseq, or membership) is enqueued; m_eager_seen records the value at the + // last eager run, so the cheap closure is re-run only when the set changed. + // m_eager_processed = how many m_prop_queue items are already folded into the + // incremental eager chain (`m_nielsen`'s deterministic leaf). + unsigned m_eager_dirty = 0; + unsigned m_eager_seen = 0; + unsigned m_eager_processed = 0; + // statistics unsigned m_num_conflicts = 0; + unsigned m_num_eager_conflicts = 0; // conflicts found by the eager structural closure unsigned m_num_final_checks = 0; unsigned m_num_sat_revalidations = 0; // times the cached SAT path was reused instead of rebuilding unsigned m_num_length_axioms = 0; @@ -135,6 +146,7 @@ namespace smt { // private helpers void populate_nielsen_graph(); + void eager_structural_check(); void explain_nielsen_conflict(); void set_conflict(enode_pair_vector const& eqs, literal_vector const& lits) const; void set_conflict(literal_vector const& lits) {