diff --git a/scripts/compare_seq_solvers.py b/scripts/compare_seq_solvers.py index ce464f1409..b30a7405f3 100644 --- a/scripts/compare_seq_solvers.py +++ b/scripts/compare_seq_solvers.py @@ -41,8 +41,8 @@ SOLVERS = { "smt.nseq.regex_factorization_threshold=0", "smt.nseq.regex_factorization_eager=false", "smt.nseq.regex_dynamic_decomposition=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=false", "smt.nseq.regex_dynamic_decomposition=false"], - #"nseq_md2": ["smt.string_solver=nseq", "smt.nseq.parikh=false", "smt.nseq.eager=false", - # "smt.nseq.monadic_split=true", "smt.nseq.regex_factorization_threshold=0", "smt.nseq.regex_factorization_eager=false", "smt.nseq.regex_dynamic_decomposition=false"], + "nseq_md2": ["smt.string_solver=nseq", "smt.nseq.parikh=false", "smt.nseq.eager=false", + "smt.nseq.monadic_split=true", "smt.nseq.regex_factorization_threshold=0", "smt.nseq.regex_factorization_eager=false", "smt.nseq.regex_dynamic_decomposition=false"], "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", "smt.nseq.regex_dynamic_decomposition=true"], "seq": ["smt.string_solver=seq"], diff --git a/src/ast/rewriter/seq_monadic.h b/src/ast/rewriter/seq_monadic.h index 4567af48a1..dc2bf8efae 100644 --- a/src/ast/rewriter/seq_monadic.h +++ b/src/ast/rewriter/seq_monadic.h @@ -84,7 +84,7 @@ class seq_monadic { seq::transition_mode m_mode; bool m_model = true; // whether solve()/check() extract a feasible model bool m_min_core = true; // whether check() minimizes the unsat core (else: all deps) - +solve config(seq::transition_mode mode) : m_mode(mode) {} }; diff --git a/src/smt/seq/seq_nielsen.cpp b/src/smt/seq/seq_nielsen.cpp index 6837c5c7e9..36483a84a7 100644 --- a/src/smt/seq/seq_nielsen.cpp +++ b/src/smt/seq/seq_nielsen.cpp @@ -5288,11 +5288,10 @@ namespace seq { return false; } -#if false // ----------------------------------------------------------------------- // Modifier: apply_monadic_split (whole-language monadic decomposition) bool nielsen_graph::monadic_abstract_subject(euf::snode const* str, expr_ref_vector& pin, - obj_map& extra, expr_ref& out) { + ptr_vector& unit_vars, expr_ref& out) { expr_ref_vector args(m); bool has_var = false; for (euf::snode const* t : *str) { @@ -5304,12 +5303,9 @@ namespace seq { const std::string name = "nseq.mon!" + std::to_string(t->id()); expr_ref v(m.mk_const(symbol(name.c_str()), s), m); pin.push_back(v); - if (t->is_unit()) { - // symbolic character: value unknown, length exactly 1. - expr_ref sigma(m_seq.re.mk_full_char(m_seq.re.mk_re(s)), m); - pin.push_back(sigma); - extra.insert(v, sigma); - } + // A symbolic character has unknown value but length exactly 1. + if (t->is_unit()) + unit_vars.push_back(v); args.push_back(v); has_var = true; } @@ -5319,23 +5315,24 @@ namespace seq { pin.push_back(out); return true; } -#endif bool nielsen_graph::apply_monadic_split(nielsen_node* node) { if (!m_monadic_split) return false; -#if false auto const& mems = node->str_mems(); if (mems.empty()) return false; - if (!m_monadic) - m_monadic = alloc(seq_monadic, m_monadic_rw); + if (!m_monadic) { + m_monadic = alloc(seq_monadic, m_monadic_rw, m_monadic_trail); + // Conflict-only use: no witness is ever consumed, so skip model extraction. + m_monadic->set_gen_model(false); + } // Abstract the plain memberships once; `src` maps back to the mems index. expr_ref_vector pin(m); - obj_map extra; vector> abstracted; + vector> unit_vars; unsigned_vector src; for (unsigned i = 0; i < mems.size(); ++i) { str_mem const& mi = mems[i]; @@ -5344,9 +5341,13 @@ namespace seq { if (!mi.is_plain() || mi.m_regex->is_ite()) continue; expr_ref term(m); - if (!monadic_abstract_subject(mi.m_str, pin, extra, term)) + ptr_vector uvars; + if (!monadic_abstract_subject(mi.m_str, pin, uvars, term)) + continue; + if (!m_monadic->can_decide_term(term)) continue; abstracted.push_back(std::make_pair(term.get(), mi.m_regex->get_expr())); + unit_vars.push_back(uvars); src.push_back(i); } const unsigned n = abstracted.size(); @@ -5354,28 +5355,42 @@ namespace seq { return false; // Decide the memberships selected by `sel` jointly; close the node if empty. + // The conflict dependency joins only the memberships seq_monadic's core kept. auto close = [&](unsigned_vector const& sel) { - vector> ms; - dep_tracker dep = mems[src[sel[0]]].m_dep; + m_monadic_trail.push_scope(); + obj_hashtable seen; for (unsigned k : sel) { - ms.push_back(abstracted[k]); - if (ms.size() > 1) - dep = m_dep_mgr.mk_join(dep, mems[src[k]].m_dep); + m_monadic->add(abstracted[k].first, abstracted[k].second, mems[src[k]].m_dep); + for (expr* v : unit_vars[k]) { + if (seen.contains(v)) + continue; + seen.insert(v); + // Length-1 is unconditionally true of a symbolic character, so it + // carries no dependency; whenever it matters, the membership that + // introduced v is itself in the core. + expr_ref sigma(m_seq.re.mk_full_char(m_seq.re.mk_re(v->get_sort())), m); + pin.push_back(sigma); + m_monadic->add(v, sigma, nullptr); + } } - const lbool r = ms.size() == 1 ? m_monadic->solve(ms[0].first, ms[0].second, extra) - : m_monadic->solve_and(ms, extra); - TRACE(seq, tout << "MONPROBE n=" << ms.size() << " r=" << r - << " subj=" << mk_pp(ms[0].first, m) << "\n"); + const lbool r = m_monadic->check(); + dep_tracker dep = nullptr; + if (r == l_false) + for (void* d : m_monadic->core()) + dep = m_dep_mgr.mk_join(dep, static_cast(d)); + m_monadic_trail.pop_scope(1); + TRACE(seq, tout << "MONPROBE n=" << sel.size() << " r=" << r + << " subj=" << mk_pp(abstracted[sel[0]].first, m) << "\n"); if (r != l_false) return false; // non-empty (l_true) or undecided (l_undef): no conclusion - TRACE(seq, tout << "monadic split: " << ms.size() << " membership(s) jointly empty, at " + TRACE(seq, tout << "monadic split: " << sel.size() << " membership(s) jointly empty, at " << mem_pp(mems[src[sel[0]]]) << "\n"); node->set_general_conflict(); node->set_conflict(backtrack_reason::regex, dep); return true; }; - // 1. each non-primitive membership on its own. + // 1. each non-primitive membership on its own (cheap, and conclusive most often). for (unsigned k = 0; k < n; ++k) { if (mems[src[k]].m_str->length() < 2) continue; // single token: plain emptiness of L(R), checked elsewhere @@ -5384,40 +5399,15 @@ namespace seq { if (close(sel)) return true; } + + // 2. all of them jointly: catches subjects that are only jointly empty through a + // shared variable. check() minimizes the core, so no pre-grouping is needed. if (n < 2) return false; - - // 2. memberships grouped by their (slicing-equal) subject. - bool_vector done; - done.resize(n, false); - unsigned num_groups = 0; - for (unsigned k = 0; k < n; ++k) { - if (done[k]) - continue; - unsigned_vector sel; - sel.push_back(k); - done[k] = true; - for (unsigned j = k + 1; j < n; ++j) { - if (done[j] || !mems[src[k]].m_str->similar(mems[src[j]].m_str, m)) - continue; - sel.push_back(j); - done[j] = true; - } - ++num_groups; - if (sel.size() >= 2 && close(sel)) - return true; - } - - // 3. all of them: catches subjects that are only jointly empty through a - // shared variable. Skipped when phase 2 already made this exact call. - if (num_groups < 2) - return false; unsigned_vector all; for (unsigned k = 0; k < n; ++k) all.push_back(k); return close(all); -#endif - return false; } bool nielsen_graph::fire_gpower_intro( diff --git a/src/smt/seq/seq_nielsen.h b/src/smt/seq/seq_nielsen.h index b2993eada4..67c3577d5d 100644 --- a/src/smt/seq/seq_nielsen.h +++ b/src/smt/seq/seq_nielsen.h @@ -1020,6 +1020,10 @@ namespace seq { // derivative cache across seq_monadic calls (the module itself keeps no // state between them). seq_rewriter m_monadic_rw; + // Backtracking scope for the memberships asserted into m_monadic: they stay + // asserted until this trail is popped, so each probe runs in its own scope. + // Declared before m_monadic so it outlives it. + trail_stack m_monadic_trail; // Monadic-decomposition membership solver (seq_monadic); allocated lazily // on first use and released in reset(). seq_monadic* m_monadic = nullptr; @@ -1709,14 +1713,12 @@ namespace seq { // Sound one-way only: never creates a child, never claims SAT. bool apply_monadic_split(nielsen_node* node); -#if false // Abstract a membership subject into the term shape seq_monadic parses - // (a concatenation of constant characters and 0-ary constants), pinning - // the constructed terms in `pin` and collecting per-constant - // over-approximating regexes in `extra`. false: the subject is ground. + // (a concatenation of constant characters and 0-ary constants), pinning the + // constructed terms in `pin` and reporting in `unit_vars` the constants that + // stand for symbolic characters (length exactly 1). false: the subject is ground. bool monadic_abstract_subject(euf::snode const* str, expr_ref_vector& pin, - obj_map& extra, expr_ref& out); -#endif + ptr_vector& unit_vars, expr_ref& out); // Build a suspended factorization (boundary head/tail + split iterator) // for `mem`. Returns null if the regex shape is unsupported (the engine