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

Drop the unread m_closed bit vector from live_states

Browse source 
close() ran an O(|states|) loop writing a per-search bool_vector that no caller
ever read, and resize() grew that vector alongside every state the shared table
interned.

The verdict it recorded is real and stronger than it looks: close() runs only
when a search drains its queue without hitting the state cap or a resource
limit, so m_to_explore is then the complete, fully expanded forward cone of the
root, and a state in it that liveness never reached has empty language for every
root, not just that one.

Retaining that verdict globally and pruning on it was implemented and measured
against this commit's parent, over 1476 bench regexes and a 500-file QF_S
sample, pre-warmed and scored by minimum of repeated runs:

  regexes, smt.seq.regex_monadic=true   1382 decided, unchanged      -1.3%
  regexes, default (legacy seq_regex)    385 decided, unchanged      +1.2%
  QF_S sample, regex_monadic=true        450 decided, unchanged      +1.7%

No benchmark was decided either way and no verdict contradicted, but nothing was
gained either, on any of the three, even though the prune fired heavily (837
prunes on split_membership_easy_sat_0019 alone). The reason is structural: by
the time close() can prove a state empty, the search has already expanded it and
its entire cone, so the only work left to save is on revisits -- which the
successor, cofactor and product-visited caches already make cheap -- while the
lookups sit in the product search's inner loop.

Remove the field and record the finding in close(), so a filter here is next
attempted in a form that prunes before exploration rather than after.
This commit is contained in:
Margus Veanes 2026-08-08 17:39:17 -07:00
parent cf203e1a78
commit 2afc8a254b
1 changed files with 15 additions and 6 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -24,7 +24,6 @@ namespace seq {
uint_set m_seen;
vector<svector<unsigned>> m_predecessors;
bool_vector m_live;
bool_vector m_closed;
svector<unsigned> m_live_frontier;
unsigned m_root_id = 0;
failure m_failure = failure::none;
@ -76,8 +75,6 @@ namespace seq {
s.m_predecessors.resize(size);
if (s.m_live.size() < size)
s.m_live.resize(size, false);
if (s.m_closed.size() < size)
s.m_closed.resize(size, false);
}
char nullable(unsigned id) {
@ -143,10 +140,22 @@ namespace seq {
return true;
}
/*
Reaching this point means the queue drained without hitting the state cap or a
resource limit, so m_to_explore is the complete, fully expanded forward cone of
the root and any state in it that liveness never reached has empty language --
a verdict that holds for every root, not just this one.
That verdict used to be recorded per search in a m_closed bit vector which no
caller ever read. Retaining it globally and pruning on it was measured and does
not pay: by the time close() can prove a state empty, the search has already
expanded it and its whole cone, so the only work saved is on revisits, which the
successor, cofactor and product-visited caches already make cheap. Over the
bench regexes corpus the result was -1.3% (seq monadic path) and +1.2% (legacy
path), and +1.7% on a QF_S sample, with no benchmark decided either way. A
filter has to prune before exploration to be worth its lookups.
*/
void close(search& s) {
for (unsigned id : s.m_to_explore)
if (!s.m_live[id])
s.m_closed[id] = true;
s.m_complete = true;
}