Bug/Performance fixes

Added argument to harvest non-primitive membership constraint benchmarks

src/params/smt_params.cpp

@@ -64,6 +64,8 @@ void smt_params::updt_local_params(params_ref const & _p) {
     m_nseq_signature = p.nseq_signature();
     m_nseq_axiomatize_diseq = p.nseq_axiomatize_diseq();
     m_nseq_eager = p.nseq_eager();
+    m_nseq_harvest = p.nseq_harvest();
+    m_nseq_harvest_dir = p.nseq_harvest_dir();
     m_up_persist_clauses = p.up_persist_clauses();
     validate_string_solver(m_string_solver);
     if (_p.get_bool("arith.greatest_error_pivot", false))
@@ -181,6 +183,7 @@ void smt_params::display(std::ostream & out) const {
     DISPLAY_PARAM(m_nseq_regex_factorization_eager);
     DISPLAY_PARAM(m_nseq_regex_dynamic_decomposition);
     DISPLAY_PARAM(m_nseq_axiomatize_diseq);
+    DISPLAY_PARAM(m_nseq_harvest);
 
     DISPLAY_PARAM(m_profile_res_sub);
     DISPLAY_PARAM(m_display_bool_var2expr);

src/params/smt_params.h

@@ -259,6 +259,8 @@ struct smt_params : public preprocessor_params,
     bool m_nseq_signature = false;
     bool m_nseq_axiomatize_diseq = false;
     bool m_nseq_eager = true;
+    unsigned m_nseq_harvest = 0;
+    symbol m_nseq_harvest_dir;
 
     smt_params(params_ref const & p = params_ref()):
         m_string_solver(symbol("auto")){

src/params/smt_params_helper.pyg

@@ -143,6 +143,8 @@ def_module_params(module_name='smt',
                           ('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'),
+                          ('nseq.harvest', UINT, 0, 'benchmark-harvest mode: bound on non-progress Nielsen extension steps before dumping the current node as an .smt2 benchmark; 0 = disabled (normal sound reasoning). WARNING: intentionally unsound, for benchmark generation only'),
+                          ('nseq.harvest_dir', SYMBOL, '.', 'output directory for harvested .smt2 benchmarks (used only when nseq.harvest > 0)'),
                           ('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

@@ -134,7 +134,8 @@ namespace seq {
         // (sigma from the paper): head ∈ Δ ∧ tail ∈ ∇ for each ⟨Δ,∇⟩, with the
         // lookahead oracle pruning non-viable ∇ during generation.
         seq_rewriter rw(m);
-        if (!rw.split(regex->get_expr(), result, threshold, split_mode::strong, oracle)) {
+        // "strong" might cause explosive behavior; better do this only in the saturation
+        if (!rw.split(regex->get_expr(), result, threshold, split_mode::weak, oracle)) {
             result.clear();
             return { nullptr, nullptr };
         }
@@ -2030,6 +2031,25 @@ namespace seq {
             // solver at the base level, so they are visible during all feasibility checks.
             assert_root_constraints_to_solver();
 
+            if (harvest_mode()) {
+                // Benchmark-harvest mode: a single fixed-depth DFS pass at the harvest
+                // bound (no iterative deepening, to avoid re-harvesting / divergence).
+                // Every branch reaching the bound dumps a snapshot of the current node
+                // and returns unknown; SAT leaves also return unknown (see search_dfs),
+                // so the whole pass returns unknown.  theory_nseq turns this into a
+                // blocking clause to force the SAT solver onto a different assignment.
+                m_depth_bound = m_harvest;
+                ptr_vector<nielsen_edge> cur_path;
+                m_siblings.clear();
+                const unsigned before = m_stats.m_num_dfs_nodes;
+                search_dfs(m_root, cur_path);
+                IF_VERBOSE(2, verbose_stream() << "nseq harvest: DFS explored "
+                    << (m_stats.m_num_dfs_nodes - before) << " nodes (bound="
+                    << m_depth_bound << ")\n");
+                ++m_stats.m_num_unknown;
+                return search_result::unknown;
+            }
+
             // Iterative deepening: increment by 1 on each failure.
             // m_max_search_depth == 0 means unlimited; otherwise stop when bound exceeds it.
             m_depth_bound = 3;
@@ -2360,6 +2380,12 @@ namespace seq {
         SASSERT(!node->is_currently_conflict());
 
         if (node->is_satisfied()) {
+            // Benchmark-harvest mode: a satisfied node has only primitive memberships
+            // (uninteresting for the regex factorization benchmark) — do NOT declare SAT
+            // (that would terminate the harvest loop) and do NOT harvest; just dead-end
+            // this branch so the search keeps exploring others.
+            if (harvest_mode())
+                return search_result::unknown;
             // Before declaring SAT, check leaf-node regex feasibility:
             // for each variable with multiple regex constraints, verify
             // that the intersection of all its regexes is non-empty.
@@ -2424,14 +2450,31 @@ namespace seq {
         }
 
         // depth bound check
-        if (depth >= m_depth_bound)
+        if (depth >= m_depth_bound) {
+            // Benchmark-harvest mode: this node has reached the configured number of
+            // non-progress extension steps and is a genuine intermediate state
+            // (post-simplify, post-Parikh, not a conflict, not satisfied) whose
+            // memberships are the rewritten (often non-primitive) ones we want.
+            // Dump the snapshot, then backtrack.
+            if (harvest_mode())
+                harvest_node(node);
             return search_result::unknown;
+        }
 
         SASSERT(!node->is_currently_conflict());
 
         // generate extensions only once per node; children persist across runs
         if (!node->is_extended()) {
             const bool ext = generate_extensions(node);
+            // Benchmark-harvest mode: with all regex modifiers disabled, a node whose
+            // only remaining work is on (non-primitive) memberships has no applicable
+            // word-equation modifier, so generate_extensions yields nothing.  This is a
+            // harvest leaf: dump the snapshot and backtrack instead of failing the
+            // VERIFY(ext) below.
+            if (harvest_mode() && !ext) {
+                harvest_node(node);
+                return search_result::unknown;
+            }
             IF_VERBOSE(1, display(verbose_stream(), node));
             CTRACE(seq, !ext, display(tout, node) << to_dot() << "\n");
             if (!ext) {
@@ -3329,11 +3372,13 @@ namespace seq {
             return ++m_stats.m_mod_eq_split, true;
 
         // Priority 5b: CycleSubsumption - eliminate leading variable subsumed by stabilizer
-        if (apply_cycle_subsumption(node))
+        // (regex-related: skipped in benchmark-harvest mode)
+        if (!harvest_mode() && apply_cycle_subsumption(node))
             return ++m_stats.m_mod_cycle_subsumption, true;
 
         // Priority 6: CycleDecomp - stabilizer introduction for regex cycles using partial DFA projection
-        if (apply_cycle_decomposition(node))
+        // (regex-related: skipped in benchmark-harvest mode)
+        if (!harvest_mode() && apply_cycle_decomposition(node))
             return ++m_stats.m_mod_star_intr, true;
 
         // Priority 7: GPowerIntr - ground power introduction
@@ -3341,7 +3386,8 @@ namespace seq {
             return ++m_stats.m_mod_gpower_intr, true;
 
         // Priority 8: Regex Factorization
-        if (apply_regex_factorization(node))
+        // (regex-related: skipped in benchmark-harvest mode)
+        if (!harvest_mode() && apply_regex_factorization(node))
             return ++m_stats.m_mod_regex_factorization, true;
 
         // Priority 8b: ConstNielsen - char vs var (2 children)
@@ -3349,7 +3395,8 @@ namespace seq {
             return ++m_stats.m_mod_const_nielsen, true;
 
         // Priority 9: RegexIfSplit - split str_mem s ∈ ite(c,th,el) by branching on c
-        if (apply_regex_if_split(node))
+        // (regex-related: skipped in benchmark-harvest mode)
+        if (!harvest_mode() && apply_regex_if_split(node))
             return ++m_stats.m_mod_regex_if_split, true;
 
         // Priority 9b: SignatureSplit - heuristic string equation splitting
@@ -3357,7 +3404,8 @@ namespace seq {
             return ++m_stats.m_mod_signature_split, true;
 
         // Priority 10: RegexVarSplit - split str_mem by minterms
-        if (apply_regex_var_split(node))
+        // (regex-related: skipped in benchmark-harvest mode)
+        if (!harvest_mode() && apply_regex_var_split(node))
             return ++m_stats.m_mod_regex_var_split, true;
 
         // Priority 11: PowerSplit - power unwinding with bounded prefix
@@ -3373,11 +3421,16 @@ namespace seq {
             return ++m_stats.m_mod_var_num_unwinding_eq, true;
 
         // Priority 14: variable power unwinding for membership constraints
-        if (apply_var_num_unwinding_mem(node))
+        // (regex/membership-related: skipped in benchmark-harvest mode)
+        if (!harvest_mode() && apply_var_num_unwinding_mem(node))
             return ++m_stats.m_mod_var_num_unwinding_mem, true;
 
         // let's unwindind a disequality
-        if (axiomatize_diseq(node))
+        // (axiomatize_diseq requires the node to be satisfied-except-diseq; in
+        // benchmark-harvest mode a node may still carry non-primitive memberships
+        // because the regex modifiers are disabled, so skip it and let the caller
+        // treat the empty result as a harvest leaf)
+        if (!harvest_mode() && axiomatize_diseq(node))
             return ++m_stats.m_ax_diseq, true;
 
         return false;

src/smt/seq/seq_nielsen.h

@@ -886,6 +886,10 @@ namespace seq {
         unsigned                      m_regex_factorization_threshold = 1;
         bool                          m_regex_factorization_eager = false;
         bool                          m_regex_dynamic_decomposition = true;
+        unsigned                      m_harvest = 0;            // 0 = disabled (benchmark-harvest bound)
+        std::string                   m_harvest_dir = ".";
+        unsigned                      m_harvest_counter = 0;    // file index; spans reset()/blocking iterations
+        std::unordered_set<unsigned>  m_harvested_hashes;       // dedup by structural hash; NOT cleared in reset()
         unsigned                      m_fresh_cnt = 0;
         nielsen_stats                 m_stats;
 
@@ -1072,6 +1076,23 @@ namespace seq {
         void set_regex_factorization_eager(bool e) { m_regex_factorization_eager = e; }
         void set_regex_dynamic_decomposition(bool e) { m_regex_dynamic_decomposition = e; }
 
+        // benchmark-harvest mode (intentionally unsound; for benchmark generation only).
+        // m_harvest > 0 = bound on non-progress Nielsen extension steps before dumping the
+        // current node as an .smt2 benchmark; 0 = disabled (normal sound reasoning).
+        void set_harvest(unsigned b) { m_harvest = b; }
+        void set_harvest_dir(std::string d) { m_harvest_dir = std::move(d); }
+        bool harvest_mode() const { return m_harvest > 0; }
+        // write a snapshot of `n` (regex memberships + residual word equations) to an
+        // .smt2 file, deduplicated by structural hash.  Terms are cleaned for portability
+        // (see clean_harvest_expr); the internal integer/length constraints are dropped.
+        void harvest_node(nielsen_node const* n);
+
+        // Rewrite `e` into portable SMT-LIB: peel seq.slice(...) applications to their
+        // root variable (first argument, chased until non-slice — matching the sgraph
+        // hashing convention).  Sets ok=false if the term still contains an nseq-internal
+        // skolem that cannot be represented (e.g. a power token); the node is then skipped.
+        expr_ref clean_harvest_expr(expr* e, bool& ok);
+
         // display for debugging
         std::ostream& display(std::ostream& out) const;
 

src/smt/seq/seq_nielsen_pp.cpp

@@ -19,8 +19,13 @@ Author:
 #include "smt/seq/seq_nielsen.h"
 #include "ast/arith_decl_plugin.h"
 #include "ast/ast_pp.h"
+#include "ast/ast_smt2_pp.h"
+#include "ast/decl_collector.h"
 #include "util/obj_hashtable.h"
+#include "util/trace.h"
 #include <sstream>
+#include <fstream>
+#include <iomanip>
 
 namespace seq {
 
@@ -88,6 +93,157 @@ namespace seq {
         return out;
     }
 
+    // Rewrite `e` into portable SMT-LIB: peel seq.slice(...) applications to their root
+    // variable (first argument, chased until non-slice — matching the sgraph hashing
+    // convention in euf_sgraph.cpp), rebuilding all other applications with cleaned args.
+    // Sets ok=false if any remaining subterm is an nseq-internal skolem we cannot
+    // represent (e.g. a power token, a Parikh counter); the node is then skipped.
+    expr_ref nielsen_graph::clean_harvest_expr(expr* e, bool& ok) {
+        if (!ok)
+            return expr_ref(m);
+        // peel slice wrappers down to the underlying root variable
+        while (m_sk.is_slice(e))
+            e = to_app(e)->get_arg(0);
+        if (!is_app(e)) { // quantifiers / vars should not appear here
+            ok = false;
+            return expr_ref(e, m);
+        }
+        app* a = to_app(e);
+        // a leaf that is still an nseq-internal skolem (e.g. a power) cannot be emitted
+        if (a->get_num_args() == 0) {
+            if (m_sk.is_skolem(e)) {
+                ok = false;
+                return expr_ref(e, m);
+            }
+            return expr_ref(e, m);
+        }
+        expr_ref_vector args(m);
+        for (expr* arg : *a) {
+            expr_ref c = clean_harvest_expr(arg, ok);
+            if (!ok)
+                return expr_ref(m);
+            args.push_back(c);
+        }
+        return expr_ref(m.mk_app(a->get_decl(), args.size(), args.data()), m);
+    }
+
+    // Benchmark-harvest: dump a snapshot of `n` (regex memberships + residual word
+    // equations) as a self-contained, portable SMT-LIB2 benchmark.  Terms are cleaned
+    // via clean_harvest_expr (slice tails -> root variables); the internal
+    // integer/length side constraints are dropped (they carry non-portable Parikh /
+    // slice-length skolems and are implied by the memberships).  Deduplicated by
+    // structural node hash.  Intended purely for benchmark generation; the surrounding
+    // harvest mode is unsound.
+    void nielsen_graph::harvest_node(nielsen_node const* n) {
+        // dedup by structural hash (computed earlier in search_dfs)
+        const unsigned h = n->hash();
+        IF_VERBOSE(2, verbose_stream() << "nseq harvest: node " << n->id()
+            << " hash=" << h << " #eq=" << n->str_eqs().size()
+            << " #mem=" << n->str_mems().size() << "\n");
+        if (!m_harvested_hashes.insert(h).second) {
+            IF_VERBOSE(2, verbose_stream() << "nseq harvest: deduped\n");
+            return;
+        }
+        // only interesting if there is at least one membership
+        if (n->str_mems().empty()) {
+            IF_VERBOSE(2, verbose_stream() << "nseq harvest: no memberships, skip\n");
+            return;
+        }
+
+        // clean every term first; skip the whole node if anything is unrepresentable
+        bool ok = true;
+        vector<std::pair<expr_ref, expr_ref>> eqs;    // cleaned word equations
+        vector<std::pair<expr_ref, expr_ref>> mems;   // cleaned memberships (str, regex)
+        for (auto const& eq : n->str_eqs()) {
+            if (eq.is_trivial())
+                continue;
+            expr_ref l = clean_harvest_expr(eq.m_lhs->get_expr(), ok);
+            expr_ref r = clean_harvest_expr(eq.m_rhs->get_expr(), ok);
+            if (!ok) break;
+            eqs.push_back({l, r});
+        }
+        for (auto const& mem : n->str_mems()) {
+            if (!ok) break;
+            expr_ref s = clean_harvest_expr(mem.m_str->get_expr(), ok);
+            expr_ref re = clean_harvest_expr(mem.m_regex->get_expr(), ok);
+            if (!ok) break;
+            mems.push_back({s, re});
+        }
+        if (!ok) {
+            IF_VERBOSE(2, verbose_stream() << "nseq harvest: unrepresentable term, skip\n");
+            return;
+        }
+
+        std::ostringstream fname;
+        fname << m_harvest_dir << "/harvest_"
+              << std::setw(6) << std::setfill('0') << m_harvest_counter << ".smt2";
+        std::ofstream out(fname.str());
+        if (!out) {
+            // fall back to the current working directory on open failure
+            std::ostringstream alt;
+            alt << "harvest_" << std::setw(6) << std::setfill('0') << m_harvest_counter << ".smt2";
+            out.open(alt.str());
+            if (!out) {
+                IF_VERBOSE(0, verbose_stream()
+                    << "nseq harvest: could not open output file " << fname.str() << "\n");
+                return;
+            }
+        }
+        ++m_harvest_counter;
+
+        // collect all uninterpreted declarations used by the cleaned snapshot
+        decl_collector coll(m);
+        for (auto const& [l, r] : eqs) {
+            coll.visit(l);
+            coll.visit(r);
+        }
+        for (auto const& [s, re] : mems) {
+            coll.visit(s);
+            coll.visit(re);
+        }
+        coll.order_deps(0);
+
+        smt2_pp_environment_dbg env(m);
+        params_ref pp;
+
+        out << "; harvested from nseq node " << n->id() << " (hash " << h << ")\n";
+        out << "(set-logic QF_S)\n";
+
+        // user-defined (uninterpreted) sorts, if any
+        for (sort* s : coll.get_sorts()) {
+            if (s->get_family_id() == null_family_id)
+                out << "(declare-sort " << s->get_name() << " 0)\n";
+        }
+        // function/constant declarations
+        for (func_decl* f : coll.get_func_decls()) {
+            if (coll.should_declare(f)) {
+                ast_smt2_pp(out, f, env, pp);
+                out << "\n";
+            }
+        }
+
+        // residual word equations
+        for (auto const& [l, r] : eqs) {
+            out << "(assert (= ";
+            ast_smt2_pp(out, l, env, pp);
+            out << " ";
+            ast_smt2_pp(out, r, env, pp);
+            out << "))\n";
+        }
+        // regex memberships (the rewritten, often non-primitive, ones we are after)
+        for (auto const& [s, re] : mems) {
+            out << "(assert (str.in_re ";
+            ast_smt2_pp(out, s, env, pp);
+            out << " ";
+            ast_smt2_pp(out, re, env, pp);
+            out << "))\n";
+        }
+
+        out << "(check-sat)\n";
+        IF_VERBOSE(1, verbose_stream() << "nseq harvest: wrote " << fname.str()
+            << " (" << mems.size() << " memberships)\n");
+    }
+
     std::ostream& nielsen_graph::display(std::ostream& out) const {
         out << "nielsen_graph with " << m_nodes.size() << " nodes, "
             << m_edges.size() << " edges\n";

src/smt/theory_nseq.cpp

@@ -518,6 +518,10 @@ namespace smt {
     void theory_nseq::eager_structural_check() {
         if (!get_fparams().m_nseq_eager)
             return;
+        // Benchmark-harvest mode must see the full constraint set in final_check; the
+        // eager closure could resolve conflicts during propagation and bypass harvesting.
+        if (get_fparams().m_nseq_harvest)
+            return;
         // Only re-run when the Nielsen-relevant constraint set actually grew.
         if (m_eager_dirty == m_eager_seen)
             return;
@@ -1001,6 +1005,8 @@ namespace smt {
                 m_nielsen.set_signature_split(get_fparams().m_nseq_signature);
                 m_nielsen.set_regex_factorization_threshold(get_fparams().m_nseq_regex_factorization_threshold);
                 m_nielsen.set_regex_factorization_eager(get_fparams().m_nseq_regex_factorization_eager);
+                m_nielsen.set_harvest(get_fparams().m_nseq_harvest);
+                m_nielsen.set_harvest_dir(get_fparams().m_nseq_harvest_dir.str());
 
                 // assert length constraints derived from string equalities
                 if (assert_length_constraints()) {
@@ -1034,7 +1040,10 @@ namespace smt {
             // 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) {
+            // In benchmark-harvest mode the pre-check would short-circuit SAT/UNSAT on
+            // the regex memberships before any word-equation rewriting happens, so skip it.
+            if (!m_nielsen.root()->is_currently_conflict() && get_fparams().m_nseq_regex_precheck
+                && !get_fparams().m_nseq_harvest) {
                 switch (check_regex_memberships_precheck()) {
                 case l_true:
                     // conflict was asserted inside check_regex_memberships_precheck
@@ -1099,6 +1108,19 @@ namespace smt {
                     return FC_DONE;
             }
 
+            // Benchmark-harvest mode: solve() returns unknown after dumping the snapshots
+            // reachable under the current assignment.  Block the current assignment so the
+            // SAT solver moves on to a different set of primitive constraints to harvest
+            // from.  This is intentionally unsound (the run only ends once the SAT solver
+            // exhausts all assignments, yielding overall unsat) — for benchmark generation.
+            if (get_fparams().m_nseq_harvest) {
+                IF_VERBOSE(1, verbose_stream() << "nseq final_check: harvest, blocking assignment\n";);
+                if (block_current_assignment())
+                    return FC_CONTINUE;
+                // nothing left to block → let the search conclude
+                return FC_GIVEUP;
+            }
+
             TRACE(seq, display(tout << "unknown\n"));
             IF_VERBOSE(1, verbose_stream() << "nseq final_check: solve UNKNOWN, FC_GIVEUP\n";);
             return FC_GIVEUP;
@@ -1160,6 +1182,44 @@ namespace smt {
         return all_sat;
     }
 
+    // -----------------------------------------------------------------------
+    // Benchmark-harvest: block the current assignment
+    // -----------------------------------------------------------------------
+
+    bool theory_nseq::block_current_assignment() {
+        // Build a clause that excludes the current assignment of the constraint
+        // literals (memberships, disequalities) and equalities feeding the Nielsen
+        // graph, so the SAT solver moves on to a different combination.
+        literal_vector clause;
+        for (auto const& item : m_prop_queue) {
+            if (std::holds_alternative<eq_item>(item)) {
+                auto const& eq = std::get<eq_item>(item);
+                // the two terms are currently equal in the egraph; forbid that
+                clause.push_back(~mk_eq(eq.m_l->get_expr(), eq.m_r->get_expr(), false));
+            }
+            else if (std::holds_alternative<deq_item>(item)) {
+                auto const& deq = std::get<deq_item>(item);
+                switch (ctx.get_assignment(deq.lit)) {
+                case l_true:  clause.push_back(~deq.lit); break;
+                case l_false: clause.push_back(deq.lit);  break;
+                default: break;
+                }
+            }
+            else if (std::holds_alternative<mem_item>(item)) {
+                auto const& mem = std::get<mem_item>(item);
+                switch (ctx.get_assignment(mem.lit)) {
+                case l_true:  clause.push_back(~mem.lit); break;
+                case l_false: clause.push_back(mem.lit);  break;
+                default: break;
+                }
+            }
+        }
+        if (clause.empty())
+            return false;
+        ctx.mk_th_axiom(get_id(), clause.size(), clause.data());
+        return true;
+    }
+
     // -----------------------------------------------------------------------
     // Conflict explanation
     // -----------------------------------------------------------------------

src/smt/theory_nseq.h

@@ -148,6 +148,10 @@ namespace smt {
         void populate_nielsen_graph();
         void eager_structural_check();
         void explain_nielsen_conflict();
+        // benchmark-harvest: block the current assignment of membership/equation
+        // literals so the SAT solver tries a different one.  Returns false if there
+        // is nothing to block (empty clause).  Intentionally unsound.
+        bool block_current_assignment();
         void set_conflict(enode_pair_vector const& eqs, literal_vector const& lits) const;
         void set_conflict(literal_vector const& lits) {
             const enode_pair_vector eqs;