mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-08-14 17:55:36 +00:00
Code Activity

seq_monadic: add state-based search driver

Browse source 
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
This commit is contained in:
Nikolaj Bjorner 2026-08-03 10:20:05 -07:00
parent 8d95ca4dc1
commit 8ed4c75cd0
2 changed files with 292 additions and 1 deletions
Download patch file Download diff file Expand all files Collapse all files

250
src/ast/rewriter/seq_monadic.cpp
View file

@ -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<atom> 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<atom> 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<expr, unsigned> 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<unsigned> 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<unsigned> 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<atom> const& atoms = m_atoms[mi];
expr* R = c.R;
uint64_t pos = (static_cast<uint64_t>(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<expr> 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;