From 8ed4c75cd0eee3a040d386e41dda93035b0b2425 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Mon, 3 Aug 2026 10:20:05 -0700 Subject: [PATCH] seq_monadic: add state-based search driver Implement the state-based DFS redesign for the monadic regex solver (the TODO in seq_monadic.cpp): keep a cursor per membership and expand one shared variable across all memberships at once, intersecting the per-variable component groups immediately to prune infeasible shared-variable choices early. Gated behind config::m_state_search (default true); the positional dfs_membership/dfs_atoms path is retained. On the 1476-file benchmark set at 10s timeout this raises solved from 1364 to 1368 with no sat/unsat flips. Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com> Copilot-Session: 57b9b87e-950a-49ea-bbb3-ed585646a5a9 --- src/ast/rewriter/seq_monadic.cpp | 250 ++++++++++++++++++++++++++++++- src/ast/rewriter/seq_monadic.h | 43 ++++++ 2 files changed, 292 insertions(+), 1 deletion(-) diff --git a/src/ast/rewriter/seq_monadic.cpp b/src/ast/rewriter/seq_monadic.cpp index ecd1903997..3420cb46fe 100644 --- a/src/ast/rewriter/seq_monadic.cpp +++ b/src/ast/rewriter/seq_monadic.cpp @@ -396,6 +396,8 @@ void seq_monadic::reset_search() { m_der_cache.reset(); m_nullable_cache.reset(); m_undef_vars = 0; + m_cursors.reset(); + m_last_var = UINT_MAX; reset_live_cache(); } @@ -578,6 +580,240 @@ lbool seq_monadic::dfs_atoms(unsigned mi, unsigned i, expr* R) { return any_undef ? l_undef : l_false; } +// ---- state-based search driver ------------------------------------------------------ +// +// This is an alternative to the strictly positional dfs_membership/dfs_atoms above. The +// positional search finishes membership 0 entirely, then membership 1, and so on, so two +// memberships that share a variable only intersect that variable's components deep in the +// tree -- after the first membership's alignment was chosen blindly. The state-based +// search keeps a *cursor* per membership and, at each step, expands ONE variable across +// ALL memberships whose current head is that variable, intersecting the per-variable +// components (m_groups) immediately. An infeasible choice for a shared variable is thus +// pruned as soon as it is made, rather than after committing to a full membership. +// +// A search state is: +// - the set of active (non-complete) cursors == active membership constraints, +// - the per-variable component groups (m_groups) == variable intersection constraints, +// - the last expanded variable (m_last_var) == locality hint for the next choice. +// Every non-complete cursor has a variable head (leading constants are eagerly consumed by +// advance_cursor / initial_normalize). The state is complete when every cursor is +// complete, and accepting when additionally every variable group is non-empty. + +lbool seq_monadic::advance_cursor(cursor& c, unsigned mi, expr* target) { + vector const& atoms = m_atoms[mi]; + // Step past the head variable. target == null encodes "the variable is the last atom", + // i.e. a plain membership component: nothing follows, the cursor is complete. + if (!target) { + c.i = atoms.size(); + c.complete = true; + return l_true; + } + c.i += 1; + c.R = target; + // Eagerly consume the constant atoms following the variable (mirrors dfs_atoms walking + // a run of constants via der_elem), so that the cursor again exposes a variable head. + while (c.i < atoms.size() && !atoms[c.i].is_var) { + expr_ref d = der_elem(c.R, atoms[c.i].elem.get()); + if (re().is_empty(d)) + return l_false; // dead: this continuation is empty + m_pin.push_back(d); + c.R = d; + c.i += 1; + } + if (c.i == atoms.size()) { // the remaining tail is epsilon + c.complete = true; + lbool nb = nullable(c.R); + if (nb == l_false) + return l_false; + if (nb == l_undef) { + m_stats.inc_bail(bail_reason::nullability); + return l_undef; // tail nullability undecidable + } + return l_true; + } + c.complete = false; // stopped on a variable head + return l_true; +} + +lbool seq_monadic::initial_normalize() { + for (unsigned mi = 0; mi < m_cursors.size(); ++mi) { + cursor& c = m_cursors[mi]; + vector const& atoms = m_atoms[mi]; + while (c.i < atoms.size() && !atoms[c.i].is_var) { + expr_ref d = der_elem(c.R, atoms[c.i].elem.get()); + if (re().is_empty(d)) + return l_false; // this membership is already empty + m_pin.push_back(d); + c.R = d; + c.i += 1; + } + // prepare() guarantees every membership has a variable, so c.i now points at a + // variable head (c.complete stays false). A membership of only constants would + // have been rejected by prepare(). + c.complete = (c.i == atoms.size()); + if (c.complete) { + // Defensive: no variable head (shouldn't happen); require the tail nullable. + lbool nb = nullable(c.R); + if (nb == l_false) + return l_false; + if (nb == l_undef) + ++m_undef_vars; + } + } + return l_true; +} + +lbool seq_monadic::accept_state() { + if (m_undef_vars > 0) + return l_undef; // some group / tail nullability gave up + if (!m_config.m_model) + return l_true; // groups already shown non-empty + m_model.reset(); + for (unsigned vi = 0; vi < m_groups.size(); ++vi) { + if (m_groups[vi].empty()) + continue; + expr_ref w(m); + lbool ne = product_nonempty(m_groups[vi], &w); + if (ne != l_true) { + m_model.reset(); + return ne; + } + m_pin.push_back(w); + m_model.insert(m_vars[vi], w.get()); + } + return l_true; +} + +lbool seq_monadic::search() { + if (m_giveup) + return l_undef; + if (m_budget == 0) { + m_stats.inc_bail(bail_reason::budget); + m_giveup = true; + return l_undef; + } + if (!m.inc()) { + m_stats.inc_bail(bail_reason::resource); + m_giveup = true; + return l_undef; + } + --m_budget; + + // Gather the head variables of the active cursors and how often each occurs as a head. + unsigned best_vi = UINT_MAX, best_cnt = 0; + obj_map head_cnt; + for (unsigned mi = 0; mi < m_cursors.size(); ++mi) { + cursor const& c = m_cursors[mi]; + if (c.complete) + continue; + expr* v = m_atoms[mi][c.i].var.get(); + unsigned cnt = 0; + head_cnt.find(v, cnt); + head_cnt.insert(v, ++cnt); + unsigned vi = m_var_idx[v]; + // Prefer the most frequent head variable; break ties toward the smallest index so + // the choice is deterministic. m_last_var (locality) is applied afterwards. + if (cnt > best_cnt || (cnt == best_cnt && (best_vi == UINT_MAX || vi < best_vi))) { + best_cnt = cnt; + best_vi = vi; + } + } + if (best_vi == UINT_MAX) + return accept_state(); // every cursor complete + + // Locality: if the last expanded variable is still an active head, expand it next -- + // its freshly chosen continuation can be checked against the intersection immediately. + unsigned vi = best_vi; + if (m_last_var != UINT_MAX && m_last_var < m_vars.size()) { + unsigned lc = 0; + if (head_cnt.find(m_vars[m_last_var], lc) && lc > 0) + vi = m_last_var; + } + + // All cursors whose current head is variable vi are expanded together at this step. + svector S; + expr* vv = m_vars[vi]; + for (unsigned mi = 0; mi < m_cursors.size(); ++mi) { + cursor const& c = m_cursors[mi]; + if (!c.complete && m_atoms[mi][c.i].var.get() == vv) + S.push_back(mi); + } + return choose_cont(vi, S, 0); +} + +lbool seq_monadic::choose_cont(unsigned vi, svector const& S, unsigned k) { + if (m_giveup) + return l_undef; + if (k == S.size()) { + unsigned saved = m_last_var; + m_last_var = vi; + lbool r = search(); + m_last_var = saved; + return r; + } + unsigned mi = S[k]; + cursor& c = m_cursors[mi]; + vector const& atoms = m_atoms[mi]; + expr* R = c.R; + uint64_t pos = (static_cast(mi) << 32) | c.i; + uint64_t last = 0; + bool finalize = m_last_occ.find(atoms[c.i].var.get(), last) && last == pos; + bool last_atom = (c.i + 1 == atoms.size()); + + // Enumerate this cursor's continuations for variable vi: a plain membership (null) when + // the variable is the last atom, otherwise every live reach target of R. + ptr_vector targets; + if (last_atom) + targets.push_back(nullptr); + else { + expr_ref_vector const* Q = live_states_cached(R); + if (!Q) + return l_undef; // gave up enumerating targets + for (expr* q : *Q) + targets.push_back(q); + } + + bool any_undef = false; + for (expr* target : targets) { + m_groups[vi].push_back(component{ atoms[c.i].var.get(), R, target }); + // Intersect immediately: prune as soon as vi's accumulated components are empty. + // The test is forced once the group is complete (past vi's last occurrence) so the + // accepting state does not need to re-verify; running it earlier (size > 1) prunes. + lbool ne; + if (re().is_empty(R)) + ne = l_false; + else if (finalize || m_groups[vi].size() > 1) + ne = group_nonempty(vi); + else + ne = l_true; + if (ne == l_false) { + m_groups[vi].pop_back(); + continue; // infeasible continuation for vi: prune + } + cursor saved = c; // save/restore cursor across the branch + lbool adv = advance_cursor(c, mi, target); + if (adv == l_false) { + c = saved; + m_groups[vi].pop_back(); + continue; + } + unsigned undef_here = (ne == l_undef ? 1u : 0u) + (adv == l_undef ? 1u : 0u); + m_undef_vars += undef_here; + lbool r = choose_cont(vi, S, k + 1); + m_undef_vars -= undef_here; + c = saved; + m_groups[vi].pop_back(); + if (r == l_true) + return l_true; + if (r == l_undef) { + if (m_giveup) + return l_undef; + any_undef = true; + } + } + return any_undef ? l_undef : l_false; +} + lbool seq_monadic::decide(membership_vec const& memberships) { m_model.reset(); if (memberships.empty()) @@ -590,7 +826,19 @@ lbool seq_monadic::decide(membership_vec const& memberships) { m_giveup = false; if (!prepare(memberships)) return l_undef; - lbool r = dfs_membership(0); + lbool r; + if (m_config.m_state_search) { + // Build one cursor per membership at its regex start; initial_normalize consumes + // leading constants so every active cursor exposes a variable head. + m_cursors.reset(); + for (unsigned mi = 0; mi < m_atoms.size(); ++mi) + m_cursors.push_back(cursor{ 0, m_regexes.get(mi), false }); + m_last_var = UINT_MAX; + lbool norm = initial_normalize(); + r = (norm == l_false) ? l_false : search(); + } + else + r = dfs_membership(0); if (r != l_true) m_model.reset(); return r; diff --git a/src/ast/rewriter/seq_monadic.h b/src/ast/rewriter/seq_monadic.h index f85e30c075..cf52e2cbfb 100644 --- a/src/ast/rewriter/seq_monadic.h +++ b/src/ast/rewriter/seq_monadic.h @@ -112,6 +112,9 @@ private: 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) + bool m_state_search = true; // use the state-based search driver (select next + // membership by the last-expanded / most-frequent + // head variable) instead of the positional DFS config(transition_mode mode) : m_mode(mode) {} }; @@ -195,6 +198,18 @@ private: std::unordered_map m_group_cache; obj_map m_live_cache; // regex -> live split states (null = gave up) + // ---- state-based search driver (see the "search state" note in the .cpp) ---- + // A membership cursor: how far membership `mi` has been consumed on the current + // branch. `i` is the next unconsumed atom, `R` the derivative state of the regex + // after the consumed prefix, `complete` once every atom is consumed (and the tail is + // known nullable / covered by a membership component). The set of non-complete + // cursors is the "set of active membership constraints"; each non-complete cursor has + // a *variable* head (leading constants are eagerly consumed). The per-variable + // component groups (m_groups) are the "variable intersection membership constraints". + struct cursor { unsigned i; expr* R; bool complete; }; + svector m_cursors; // one cursor per membership (parallel to m_atoms) + unsigned m_last_var = UINT_MAX; // index (in m_vars) of the last expanded variable + // Brzozowski derivative of regex `r` by the concrete element `elem`. Memoized on // (r, elem): the search revisits the same constant step on many branches. expr_ref der_elem(expr* r, expr* elem); @@ -246,6 +261,34 @@ private: lbool dfs_membership(unsigned mi); lbool dfs_atoms(unsigned mi, unsigned i, expr* R); + // ---- state-based search driver ---------------------------------------------------- + // Consume the leading constant atoms of every cursor so that each non-complete cursor + // has a variable head. l_false if some membership is already empty (unsat). + lbool initial_normalize(); + + // One search step: pick the next variable to expand (preferring the last-expanded + // variable, else the one occurring most often as a head atom of the active cursors), + // and expand it. Returns l_true (sat leaf found), l_false (this branch is empty), or + // l_undef (gave up on a sub-branch). + lbool search(); + + // Expand variable `vi`, which is the head of the cursors in `S`. Assign a continuation + // (a reach target q, or the epsilon/membership encoding for a last atom) to each cursor + // in turn (k indexes S), pushing the component on m_groups[vi] and pruning as soon as + // the accumulated intersection for vi is empty. When every cursor in S is assigned, + // recurse into search(). + lbool choose_cont(unsigned vi, svector const& S, unsigned k); + + // Advance cursor `mi` past its head variable to continuation `target` (null = the + // variable is a last atom, i.e. a plain membership component), then eagerly consume + // the following constant atoms. l_false = the continuation is empty (prune), + // l_undef = feasible but the tail nullability is unknown, l_true = feasible. + lbool advance_cursor(cursor& c, unsigned mi, expr* target); + + // Every cursor is complete: the state is accepting iff every variable intersection is + // non-empty. Extracts witnesses into m_model when model generation is enabled. + lbool accept_state(); + // Emptiness of the components accumulated for variable `vi` on the current branch, // memoized on their signature. Duplicated components are collapsed before the // product search (they constrain the variable identically).