mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-08-09 23:42:21 +00:00
Code Activity

Emit the root first when enumerating live states

Browse source 
The lazy traversal appends to `m_live_frontier` in the order liveness is
*discovered*, which is bottom-up: `mark_live` records a state when it is found
nullable and then propagates backwards through predecessors. A root is rarely
nullable itself, so it becomes live only by back-propagation and lands at the
*end* of the frontier. The eager traversal this replaced emitted states in
interning order, i.e. root first.

`dfs_atoms` consumes that sequence as a search order and stops at the first
`l_true`, so dropping the root to the back reordered every split search. Four
`split_membership` benchmarks lost their witness-first branch and timed out.

This restores the root to index 0 and leaves the rest of the frontier order
untouched. The remap is well defined because every state in a search is
reachable from the root, so liveness propagates to the root within the same
`expand()` step: whenever the frontier is non-empty at an `ensure()` boundary
the root is already live and in it. The element count is unchanged, so
`ensure`'s bound still holds.

Note this is deliberately narrower than restoring full interning order. That
alternative was prototyped in #10381 and rejected: it fixed the same
regressions but lost `medium_sat_0003/0026/0036/0052`, which the discovery
order wins, and cost 31% on light-antimirov because per-state forward liveness
is quadratic where backward propagation is linear. Moving only the root keeps
both.

ClemensRegex, 1178 benchmarks, 10s timeout, `smt.seq.regex_monadic=true`,
against master:

| | before this commit | after |
|---|---|---|
| decided | +2 / -5 | **+6 / -1** |
| time, 1072 commonly decided | +23.3% | **-22.5%** |

No sat/unsat contradictions. 23 benchmarks are >=2x faster, 7 are >=2x slower.
MargusRegex (298) is unchanged: 297/298 decided by both sides, no verdict
differences.

The one remaining loss, `split_membership_medium_unsat_0047`, is unrelated to
ordering. It regressed with lazy consumption (#10381): master detects the
state cap before exploring anything and hands over to the fallback in 0.7s,
whereas the lazy loop explores the truncated frontier first and builds very
large derivative terms doing so. The node budget does not see it because the
cost is in term size, not node count. Bounding the speculative work by budget
units was tried and rejected -- it did not recover 0047 and lost
`medium_sat_0026`.

Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
Copilot-Session: a2ce3573-4e15-4a4a-afb5-21e3cb04e4a2
This commit is contained in:
Margus Veanes 2026-08-07 18:33:07 -07:00
parent e1b3dc9af0
commit 1fea78d5d1
1 changed files with 29 additions and 0 deletions
Download patch file Download diff file Expand all files Collapse all files

29
src/ast/rewriter/seq_regex_live.cpp
View file

@ -26,6 +26,7 @@ namespace seq {
bool_vector m_live;
bool_vector m_closed;
svector<unsigned> m_live_frontier;
unsigned m_root_id = 0;
failure m_failure = failure::none;
bool m_complete = false;
};
@ -185,6 +186,7 @@ namespace seq {
return s;
s = alloc(search);
unsigned root_id = intern(root);
s->m_root_id = root_id;
add_state(*s, root_id);
m_searches.insert(root, s);
return s;
@ -272,7 +274,34 @@ namespace seq {
return m_imp->ensure(*s, index);
}
/*
Yield the root before the rest of the frontier.
States enter m_live_frontier in the order their liveness is *discovered*, which is
bottom-up: a nullable state is marked first and liveness then propagates backwards to
its predecessors, so the root -- reachable to every state, and rarely nullable itself
-- is typically marked last. Callers use this order as a search order, and the
eager traversal this replaced emitted states in interning order with the root at
index 0. Dropping the root to the back therefore reordered the consumer's search and
cost several benchmarks their witness-first branch.
The remap is well defined because every state in the search is reachable from the
root, so liveness of any state propagates to the root within the same expand() step:
whenever the frontier is non-empty at an ensure() boundary the root is already live
and present in it, and the element count is unchanged.
*/
expr* live_states::get_live(search* s, unsigned index) const {
unsigned root = s->m_root_id;
if (!s->m_live.get(root, false))
return m_imp->m_states.get(s->m_live_frontier[index]);
if (index == 0)
return m_imp->m_states.get(root);
for (unsigned i = 0, seen = 0; i < s->m_live_frontier.size(); ++i) {
if (s->m_live_frontier[i] == root)
continue;
if (++seen == index)
return m_imp->m_states.get(s->m_live_frontier[i]);
}
return m_imp->m_states.get(s->m_live_frontier[index]);
}