From 1f448a10a304c68f4ba73d7d6edb1d1539c776db Mon Sep 17 00:00:00 2001 From: CEisenhofer Date: Wed, 1 Jul 2026 14:47:36 +0200 Subject: [PATCH] Bug/Performance fixes Added argument to harvest non-primitive membership constraint benchmarks --- scripts/compare_seq_solvers.py | 6 +- src/params/smt_params.cpp | 3 + src/params/smt_params.h | 2 + src/params/smt_params_helper.pyg | 2 + src/smt/seq/seq_nielsen.cpp | 71 ++++++++++++-- src/smt/seq/seq_nielsen.h | 21 +++++ src/smt/seq/seq_nielsen_pp.cpp | 156 +++++++++++++++++++++++++++++++ src/smt/theory_nseq.cpp | 62 +++++++++++- src/smt/theory_nseq.h | 4 + 9 files changed, 314 insertions(+), 13 deletions(-) diff --git a/scripts/compare_seq_solvers.py b/scripts/compare_seq_solvers.py index bc465a4254..7dbebae9ef 100644 --- a/scripts/compare_seq_solvers.py +++ b/scripts/compare_seq_solvers.py @@ -36,9 +36,9 @@ COMMON_ARGS = ["model_validate=true"] # All three configurations are always run. SOLVERS = { - "nseq_md": ["smt.string_solver=nseq", "smt.nseq.parikh=false", - "smt.nseq.regex_factorization_threshold=100", "smt.nseq.regex_factorization_eager=true"], - "nseq_pa": ["smt.string_solver=nseq", "smt.nseq.parikh=false", + "nseq_md": ["smt.string_solver=nseq", "smt.nseq.parikh=false", "smt.nseq.eager=false", + "smt.nseq.regex_factorization_threshold=10000000", "smt.nseq.regex_factorization_eager=true"], + "nseq_pa": ["smt.string_solver=nseq", "smt.nseq.parikh=false", "smt.nseq.eager=false", "smt.nseq.regex_factorization_threshold=0", "smt.nseq.regex_factorization_eager=false"], "seq": ["smt.string_solver=seq"], } diff --git a/src/params/smt_params.cpp b/src/params/smt_params.cpp index ce07ade25a..f693b08a8d 100644 --- a/src/params/smt_params.cpp +++ b/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); diff --git a/src/params/smt_params.h b/src/params/smt_params.h index 326a9a80a5..2c4c7ff60b 100644 --- a/src/params/smt_params.h +++ b/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")){ diff --git a/src/params/smt_params_helper.pyg b/src/params/smt_params_helper.pyg index 69728bcb27..0659ea158b 100644 --- a/src/params/smt_params_helper.pyg +++ b/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'), diff --git a/src/smt/seq/seq_nielsen.cpp b/src/smt/seq/seq_nielsen.cpp index 8d410f8111..3f168ee9ee 100644 --- a/src/smt/seq/seq_nielsen.cpp +++ b/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 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; diff --git a/src/smt/seq/seq_nielsen.h b/src/smt/seq/seq_nielsen.h index 4d6a73fccb..331eebc2f5 100644 --- a/src/smt/seq/seq_nielsen.h +++ b/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 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; diff --git a/src/smt/seq/seq_nielsen_pp.cpp b/src/smt/seq/seq_nielsen_pp.cpp index 798703382a..7092244035 100644 --- a/src/smt/seq/seq_nielsen_pp.cpp +++ b/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 +#include +#include 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> eqs; // cleaned word equations + vector> 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"; diff --git a/src/smt/theory_nseq.cpp b/src/smt/theory_nseq.cpp index 2a8af4f2da..71cf24dda5 100644 --- a/src/smt/theory_nseq.cpp +++ b/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(item)) { + auto const& eq = std::get(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(item)) { + auto const& deq = std::get(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(item)) { + auto const& mem = std::get(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 // ----------------------------------------------------------------------- diff --git a/src/smt/theory_nseq.h b/src/smt/theory_nseq.h index 78a4bb5446..628e78d1c0 100644 --- a/src/smt/theory_nseq.h +++ b/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;