Try to do some processing already during assignments

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

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")){

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'),

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<nielsen_edge> 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);

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<std::vector<unsigned>> 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<nielsen_subst> 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);

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<eq_item>(item)) {
+                auto const& eq = std::get<eq_item>(item);
+                m_nielsen.eager_add_str_eq(eq.m_lhs, eq.m_rhs, eq.m_l, eq.m_r);
+            }
+            else if (std::holds_alternative<deq_item>(item)) {
+                auto const& dq = std::get<deq_item>(item);
+                m_nielsen.eager_add_str_deq(dq.m_lhs, dq.m_rhs, dq.lit);
+            }
+            else if (std::holds_alternative<mem_item>(item)) {
+                auto const& mem = std::get<mem_item>(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<seq::str_mem> 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);

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