diff --git a/src/params/smt_params.cpp b/src/params/smt_params.cpp index 4f8fceb1b1..fb300f7867 100644 --- a/src/params/smt_params.cpp +++ b/src/params/smt_params.cpp @@ -65,6 +65,7 @@ void smt_params::updt_local_params(params_ref const & _p) { m_nseq_regex_dynamic_decomposition = p.nseq_regex_dynamic_decomposition(); m_nseq_signature = p.nseq_signature(); m_nseq_fine_wilf = p.nseq_fine_wilf(); + m_nseq_monadic_split = p.nseq_monadic_split(); m_nseq_axiomatize_diseq = p.nseq_axiomatize_diseq(); m_nseq_eager = p.nseq_eager(); m_nseq_harvest = p.nseq_harvest(); @@ -186,6 +187,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_fine_wilf); + DISPLAY_PARAM(m_nseq_monadic_split); DISPLAY_PARAM(m_nseq_axiomatize_diseq); DISPLAY_PARAM(m_nseq_harvest); diff --git a/src/params/smt_params.h b/src/params/smt_params.h index f95c04a5de..b7ff43bcc0 100644 --- a/src/params/smt_params.h +++ b/src/params/smt_params.h @@ -260,6 +260,7 @@ struct smt_params : public preprocessor_params, bool m_nseq_regex_dynamic_decomposition = true; bool m_nseq_signature = false; bool m_nseq_fine_wilf = false; + bool m_nseq_monadic_split = false; bool m_nseq_axiomatize_diseq = false; bool m_nseq_eager = true; unsigned m_nseq_harvest = 0; diff --git a/src/params/smt_params_helper.pyg b/src/params/smt_params_helper.pyg index 27269d4e25..0de47a1748 100644 --- a/src/params/smt_params_helper.pyg +++ b/src/params/smt_params_helper.pyg @@ -144,6 +144,7 @@ def_module_params(module_name='smt', ('nseq.regex_dynamic_decomposition', BOOL, True, 'decompose cyles detected by unwinding regexes'), ('nseq.signature', BOOL, False, 'enable heuristic signature-based string equation splitting in Nielsen solver'), ('nseq.fine_wilf', BOOL, False, 'enable Fine & Wilf overlap splitting for equations with different-base power heads in the Nielsen solver (breaks the divergent one-copy peel loop)'), + ('nseq.monadic_split', BOOL, False, 'enable the continuation-regex intersection modifier (seq_monadic) in the Nielsen solver: closes a node when several memberships on the same sequence have a provably empty language intersection'), ('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'), diff --git a/src/smt/seq/seq_nielsen.cpp b/src/smt/seq/seq_nielsen.cpp index c3f9ad81ae..53ecfe3b31 100644 --- a/src/smt/seq/seq_nielsen.cpp +++ b/src/smt/seq/seq_nielsen.cpp @@ -29,13 +29,12 @@ NSB review: #include "ast/ast_pp.h" #include "ast/ast_util.h" #include "ast/rewriter/seq_rewriter.h" +#include "ast/rewriter/seq_monadic.h" #include "ast/rewriter/th_rewriter.h" #include "ast/rewriter/seq_skolem.h" -#include "ast/rewriter/var_subst.h" #include "util/statistics.h" #include #include -#include #include #include #include @@ -165,7 +164,7 @@ namespace seq { SASSERT(d); if (d->is_fail()) continue; // ∇ can't start with c → infeasible split, drop - result[w++] = split_pair(result[i].m_d, d->get_expr(), m); + result[w++] = ::split_pair(result[i].m_d, d->get_expr(), m); } result.shrink(w); } @@ -779,7 +778,7 @@ namespace seq { m(sg.get_manager()), a(sg.get_manager()), m_seq(sg.get_seq_util()), m_sg(sg), m_rw(m), m_a_rw(m), m_sk(m, m_rw), m_length_solver(solver), m_context_solver(ctx_solver), m_parikh(alloc(seq_parikh, sg)), m_seq_regex(alloc(seq::seq_regex, sg)), m_split_rw(sg.get_manager()), m_deriv_rw(sg.get_manager()), - m_partial_dfa_pin(sg.get_manager()) { + m_monadic_rw(sg.get_manager()), m_partial_dfa_pin(sg.get_manager()) { } nielsen_graph::~nielsen_graph() { @@ -885,6 +884,10 @@ namespace seq { dealloc(st); } m_rf_states.reset(); + // continuation-regex service: release its pinned derivative graph so a + // fresh problem starts with a clean cache (its pins would grow forever). + dealloc(m_monadic); + m_monadic = nullptr; m_nodes.reset(); m_edges.reset(); m_root = nullptr; @@ -1582,7 +1585,6 @@ namespace seq { // predicate is not internalized automatically (see the analogous // gradient propagation in theory_nseq). expr_ref div(a.mk_divides(a.mk_int(stride), a.mk_sub(len, a.mk_int(min_len))), m); - m_rw(div); e->add_side_constraint(mk_constraint(div, dep)); } } @@ -3685,6 +3687,13 @@ namespace seq { if (!harvest_mode() && apply_regex_factorization(node)) return ++m_stats.m_mod_regex_factorization, true; + // Priority 8a: MonadicSplit - continuation-regex intersection (seq_monadic): + // close the node if several memberships on the same sequence have a + // provably empty language intersection. Sound one-way (conflict only); + // opt-in via smt.nseq.monadic_split. (skipped in benchmark-harvest mode) + if (!harvest_mode() && apply_monadic_split(node)) + return ++m_stats.m_mod_monadic_split, true; + // Priority 8b: ConstNielsen - char vs var (2 children) if (apply_const_nielsen(node)) return ++m_stats.m_mod_const_nielsen, true; @@ -5202,6 +5211,76 @@ namespace seq { return false; } + // ----------------------------------------------------------------------- + // Modifier: apply_monadic_split (continuation-regex intersection, seq_monadic) + // + // Uses the continuation-regex service in ast/rewriter/seq_monadic.h. Several + // plain memberships s ∈ R_1, …, s ∈ R_k on the SAME left-hand sequence s + // are jointly satisfiable only if L(R_1) ∩ … ∩ L(R_k) ≠ ∅. split_manager + // decides emptiness of that intersection over one shared, globally cached + // Brzozowski-derivative graph, and — unlike apply_regex_factorization, which + // skips primitive memberships (x ∈ R with x a bare variable) — it also fires + // on those, catching groups that are only *jointly* empty. + // + // Only the sound direction is used: seq_monadic::intersect returns l_false + // exactly when the intersection is provably empty (note the convention is the + // OPPOSITE of seq_regex::check_intersection_emptiness, where l_true = empty). + // On l_false the node is a regex conflict. l_true (non-empty) and l_undef + // (STATE_CAP / undecidable nullability) fall through so the ordinary modifiers + // keep driving the node. No witness is consumed (the module's witness + // extraction is not sound yet) and no child is ever created, so this rule can + // never introduce an unsound SAT. Opt-in via smt.nseq.monadic_split. + // ----------------------------------------------------------------------- + bool nielsen_graph::apply_monadic_split(nielsen_node* node) { + if (!m_monadic_split) + return false; + + auto const& mems = node->str_mems(); + const unsigned n = mems.size(); + if (n < 2) + return false; // need at least two memberships to form an intersection + + if (!m_monadic) + m_monadic = alloc(seq::split_manager, m_monadic_rw); + + // Group plain memberships by their (slicing-equal) left-hand sequence and + // test the joint language intersection of each group of size >= 2. + bool_vector done; + done.resize(n, false); + for (unsigned i = 0; i < n; ++i) { + str_mem const& mi = mems[i]; + if (done[i] || !mi.is_plain()) + continue; + + vector crs; + crs.push_back(m_monadic->embed(mi.m_regex->get_expr())); + dep_tracker dep = mi.m_dep; + done[i] = true; + for (unsigned j = i + 1; j < n; ++j) { + str_mem const& mj = mems[j]; + if (done[j] || !mj.is_plain() || !mi.m_str->similar(mj.m_str, m)) + continue; + crs.push_back(m_monadic->embed(mj.m_regex->get_expr())); + dep = m_dep_mgr.mk_join(dep, mj.m_dep); + done[j] = true; + } + if (crs.size() < 2) + continue; // no sibling membership on the same sequence + + expr_ref_vector wit(m); + const lbool r = m_monadic->intersect(crs, 0, UINT_MAX, wit); + if (r != l_false) + continue; // non-empty (l_true) or undecided (l_undef): no conclusion + + TRACE(seq, tout << "monadic split: empty intersection of " << crs.size() + << " memberships on " << mem_pp(mi) << "\n"); + node->set_general_conflict(); + node->set_conflict(backtrack_reason::regex, dep); + return true; + } + return false; + } + bool nielsen_graph::fire_gpower_intro( nielsen_node* node, str_eq const& eq, euf::snode const* var, euf::snode_vector const& ground_prefix_orig, const bool fwd) { @@ -6372,7 +6451,10 @@ namespace seq { } constraint nielsen_graph::mk_constraint(expr *fml, dep_tracker const &dep) const { - return constraint(fml, dep, m); + // we need to rewrite e.g., division or <; otw. the integer solver will cry + expr_ref c(fml, m); + c = normalize_arith(m_rw, c); + return constraint(c, dep, m); } expr* nielsen_graph::get_power_exponent(euf::snode const* power) { @@ -6902,6 +6984,7 @@ namespace seq { st.update("nseq mod view land", m_stats.m_mod_view_land); st.update("nseq mod gpower intr", m_stats.m_mod_gpower_intr); st.update("nseq mod regex fact", m_stats.m_mod_regex_factorization); + st.update("nseq mod monadic split", m_stats.m_mod_monadic_split); st.update("nseq mod const nielsen", m_stats.m_mod_const_nielsen); st.update("nseq mod signature split", m_stats.m_mod_signature_split); st.update("nseq mod regex var", m_stats.m_mod_regex_var_split); diff --git a/src/smt/seq/seq_nielsen.h b/src/smt/seq/seq_nielsen.h index 69cfc7b93b..788de62a7a 100644 --- a/src/smt/seq/seq_nielsen.h +++ b/src/smt/seq/seq_nielsen.h @@ -60,6 +60,7 @@ namespace seq { class nielsen_graph; class seq_parikh; class seq_regex; // forward declaration (defined in smt/seq/seq_regex.h) + class split_manager; // continuation-regex service (defined in ast/rewriter/seq_monadic.h) std::string snode_label_html(euf::snode const* n, obj_map& names, uint64_t& next_id, ast_manager& m, bool html_escape); @@ -866,6 +867,7 @@ namespace seq { unsigned m_mod_view_land = 0; unsigned m_mod_gpower_intr = 0; unsigned m_mod_regex_factorization = 0; + unsigned m_mod_monadic_split = 0; unsigned m_mod_const_nielsen = 0; unsigned m_mod_regex_var_split = 0; unsigned m_mod_signature_split = 0; @@ -943,6 +945,7 @@ namespace seq { bool m_parikh_enabled = true; bool m_signature_split = false; bool m_fine_wilf = false; + bool m_monadic_split = false; unsigned m_regex_factorization_threshold = 1; bool m_regex_factorization_eager = false; bool m_regex_dynamic_decomposition = true; @@ -1003,6 +1006,15 @@ namespace seq { // across calls (a fresh seq_rewriter per consumed character was a // dominant simplification cost). seq_rewriter m_deriv_rw; + // Dedicated rewriter backing the continuation-regex service used by + // apply_monadic_split. Kept separate from m_split_rw / m_deriv_rw so its + // derivative caches never interleave with the suspended factorization + // iterators that reference those engines. + seq_rewriter m_monadic_rw; + // Continuation-regex split / intersection service (seq_monadic). Grows a + // shared, globally cached Brzozowski-derivative graph; allocated lazily on + // first use and released in reset(). + seq::split_manager* m_monadic = nullptr; // Owns the suspended factorization continuations (rf_state); nodes hold // raw pointers into this pool. Freed in reset(). ptr_vector m_rf_states; @@ -1184,7 +1196,9 @@ namespace seq { void set_signature_split(bool e) { m_signature_split = e; } void set_fine_wilf(bool e) { m_fine_wilf = e; } - + + void set_monadic_split(bool e) { m_monadic_split = e; } + void set_regex_factorization_threshold(unsigned max) { m_regex_factorization_threshold = max; } void set_regex_factorization_eager(bool e) { m_regex_factorization_eager = e; } void set_regex_dynamic_decomposition(bool e) { m_regex_dynamic_decomposition = e; } @@ -1668,6 +1682,12 @@ namespace seq { // disjunction is refuted → the continuation node is a regex conflict. bool apply_regex_factorization(nielsen_node* node); + // continuation-regex intersection modifier (seq_monadic). Detects a + // provably empty intersection of several plain memberships sharing the + // same left-hand sequence and reports the node as a regex conflict. + // Sound one-way only: never creates a child, never claims SAT. + bool apply_monadic_split(nielsen_node* node); + // Build a suspended factorization (boundary head/tail + split iterator) // for `mem`. Returns null if the regex shape is unsupported (the engine // cannot even start a split). Allocated into m_rf_states. diff --git a/src/smt/seq_model.cpp b/src/smt/seq_model.cpp index 64d85d4039..6f021afa85 100644 --- a/src/smt/seq_model.cpp +++ b/src/smt/seq_model.cpp @@ -134,8 +134,6 @@ namespace smt { return alloc(expr_wrapper_proc, to_app(e)); } - std::cout << mk_pp(n->get_expr(), m) << std::endl; - // For nth_u (underspecified nth): the Nielsen character-peel / // regex-if-split records the chosen character as a relevant // equality literal (e.g. (= (seq.nth_u x 0) (_ Char 65))), so the @@ -442,7 +440,6 @@ namespace smt { if (a.is_numeral(e, val)) return val; - bool has_val = get_arith_value(_e, val); CTRACE(seq, !has_val, tout << "no value associated with " << mk_pp(e, m) << "\n";); return val; diff --git a/src/smt/theory_nseq.cpp b/src/smt/theory_nseq.cpp index bb15caab19..f31f836703 100644 --- a/src/smt/theory_nseq.cpp +++ b/src/smt/theory_nseq.cpp @@ -1020,6 +1020,7 @@ namespace smt { m_nielsen.set_parikh_enabled(get_fparams().m_nseq_parikh); m_nielsen.set_signature_split(get_fparams().m_nseq_signature); m_nielsen.set_fine_wilf(get_fparams().m_nseq_fine_wilf); + m_nielsen.set_monadic_split(get_fparams().m_nseq_monadic_split); 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_regex_dynamic_decomposition(get_fparams().m_nseq_regex_dynamic_decomposition); @@ -1169,7 +1170,7 @@ namespace smt { bool all_sat = true; ctx.push_trail(reset_vector(m_nielsen_literals)); for (const auto& c : m_nielsen.sat_node()->constraints()) { - std::cout << "Assumption: " << mk_pp(c.fml, m) << std::endl; + // std::cout << "Assumption: " << mk_pp(c.fml, m) << std::endl; auto lit = mk_literal(c.fml); m_nielsen_literals.push_back(lit); // Ensure Nielsen assumptions participate in SAT search instead of @@ -2182,8 +2183,8 @@ namespace smt { expr_ref len_minus_l(m_autil.mk_sub(len_expr, l_expr), m); expr_ref not_divides(m.mk_not(m_autil.mk_divides(g_expr, len_minus_l)), m); prop_expr = m.mk_or(len_lt_l, not_divides); - m_th_rewriter(prop_expr); // the divisibility predicate needs to be rewritten as it won't happen - // automatically + m_th_rewriter(prop_expr); + // the divisibility predicate needs to be rewritten as it won't happen automatically m_gradient_cache[s] = 1; // Reset gradient cache }