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

Live-state traversal and interval-refinement product for seq_monadic, minus the postponed prunes (#10455)

Browse source 
Rebases the `seq-live-states` work onto current `master`, drops the two
additions that are being postponed, and fixes a live-state ordering
regression
that the rebase exposed.

### What is in

1. **`63ad8f944` Add lazy regex live-state traversal** — moves
live-state
   computation out of `seq_monadic`/`seq_regex` into a shared
`seq::live_states` that interns derivative states, keeps a predecessor
graph, and marks liveness by backward propagation from nullable states.
The
reachable set is exposed as a lazy iterator instead of being
materialised.
2. **`42e82f3e8` Consume live states lazily in `dfs_atoms` (#10381)** —
makes
the only consumer actually lazy. It previously drained the iterator into
a
`ptr_vector` before exploring anything, so a root with an exponential
live
   set was paid for in full even when a witness appeared immediately.
3. **`d67bbfab6` Build the `seq_monadic` product from interval
refinement
(#10384)** — replaces the cartesian product over cofactor guards with a
   cursor merge over per-state ordered-interval forms.
4. **`e1b3dc9af`** — reconciles the state display with upstream #10431,
which
   started reading `m_live_cache` after this work had replaced it. Adds
   `live_states::num_states()`.
5. **`1fea78d5d` Emit the root first when enumerating live states** —
new here,
   see below.

### What is out

* **The Bloom-filter / `atom_sig` prune** (`f96e37753` on
`seq-live-states`) is
  dropped. It keys on syntactic features and is a maintenance liability.
* **The approximate semilinear length abstraction** is dropped. It is
worth
revisiting, but with a real semilinear representation for `∃k. k·SL(R)`
rather than the gcd approximation, and after surveying what the Parikh
solver
  already provides.

Neither is on `master`; nothing is being reverted from upstream.

### The ordering fix

Evaluating commits 1–4 against `master` initially looked bad: +2/−5
decided and
**+23.3%** time on commonly decided benchmarks. Bisecting over
per-commit
builds put four of the five losses on commit 1, and the cause is an
enumeration
order change.

`m_live_frontier` is appended in the order liveness is *discovered*,
which is
bottom-up — `mark_live` records a nullable state and then propagates
backwards
through predecessors. A root is rarely nullable itself, so it becomes
live only
by back-propagation and lands **last**. The eager traversal that was
removed
emitted states in interning order, i.e. **root first**. `dfs_atoms` uses
that
sequence as a search order and stops at the first `l_true`, so the root
moving
to the back reordered every split search, and four `split_membership`
benchmarks lost their witness-first branch.

`1fea78d5d` restores the root to index 0 and leaves the rest of the
frontier
order alone. This is deliberately narrower than restoring full interning
order,
which was prototyped in #10381 and rejected — that fixed the same
regressions
but lost `medium_sat_0003/0026/0036/0052` and cost 31% on
light-antimirov,
because per-state forward liveness is quadratic where backward
propagation is
linear. Moving only the root keeps both.

The remap is well defined: every state in a search is reachable from the
root,
so liveness reaches the root within the same `expand()` step, and
whenever the
frontier is non-empty at an `ensure()` boundary the root is already in
it. The
element count is unchanged, so `ensure`'s bound still holds.

### Results

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

| | commits 1–4 | + ordering fix |
|---|---|---|
| decided | +2 / −5 | **+6 / −1** |
| time, 1072 commonly decided | +23.3% | **−22.5%** (197.3s → 152.9s) |

No sat/unsat contradictions. 23 benchmarks ≥2x faster, 7 ≥2x slower.

| family | n | both | base | new | Δ |
|---|---|---|---|---|---|
| `Automatic/generated` | 80 | 17 | 29.6s | 11.4s | −61.3% |
| `Automatic/generated_easy` | 20 | 11 | 14.0s | 3.9s | −72.4% |
| `Automatic/generated_tiny` | 30 | 30 | 6.6s | 5.2s | −21.4% |
| `Manual/with_lengths` | 12 | 5 | 7.0s | 7.1s | +0.7% |
| `Manual/without_lengths` | 120 | 113 | 29.9s | 20.0s | −33.2% |
| `QF_S_extracted_with_equations` | 52 | 32 | 10.2s | 9.5s | −6.9% |
| `QF_S_extracted_without_equations` | 864 | 864 | 100.0s | 95.9s |
−4.1% |

Newly decided: `medium_sat_0026/0036/0038`, `easy_unsat_0007/0010/0011`.
Largest single gains are `medium_unsat_0027` (7.4s → 1.3s),
`medium_unsat_0058`
(6.6s → 1.4s) and `noodler_killer_11_symmetric_nth` (3.8s → 0.15s).

MargusRegex (298) is unchanged — 297/298 decided by both sides, no
verdict
differences. That corpus is startup-dominated at ~25ms per benchmark and
serves
as a correctness net rather than a performance signal.

`test-z3 seq_monadic` and `test-z3 seq_rewriter` pass.

### What the interval-refinement product contributes on its own

Since #10384 is the largest diff here, it was re-measured in isolation:
two
builds differing only in `d67bbfab6`, both with the ordering fix, so
nothing is
confounded. +2 decided, 0 lost, 0 contradictions, and the benefit scales
with
how solver-bound the goal is:

| baseline cost | n | base | new | speedup |
|---|---|---|---|---|
| <100 ms | 821 | 61.5s | 63.2s | 1.00x |
| 100–250 ms | 209 | 26.6s | 24.8s | 1.07x |
| 250 ms–1 s | 33 | 12.2s | 10.3s | 1.19x |
| 1–5 s | 11 | 25.5s | 16.0s | 1.59x |
| >5 s | 3 | 19.5s | 3.1s | 6.35x |
| **solver-bound (≥250 ms)** | **47** | **57.3s** | **29.4s** |
**1.95x** |

The +2.8% on sub-100ms files is measurement noise: median-of-3 repeat
runs over
a 150-file sample give −0.1%, so the per-state interval cache costs
nothing on
cheap goals.

Split by verdict it is sharper still — the refinement is an **unsat
accelerator and exactly neutral on sat**, which follows from the
mechanism:
unsat has to exhaust the product state space so cell enumeration is the
entire
cost, while sat short-circuits at the first witness.

| | n | base | new | speedup |
|---|---|---|---|---|
| sat | 903 | 89.3s | 89.3s | 1.00x |
| unsat | 174 | 56.1s | 28.1s | 1.99x |
| unsat, ≥250 ms | 24 | 43.0s | 15.1s | **2.84x** |

This corroborates the 2.05x/2.36x reported in #10384, and locates it:
~1.0x on
three quarters of the corpus, 2.8x on the two dozen files that dominate
runtime.

### Known regression

`split_membership_medium_unsat_0047` (1.0s → timeout) is not an ordering
problem; it regressed with commit 2 and the ordering fix does not touch
it.
`master` hits the live-state cap before exploring anything and hands
over to
the legacy fallback in 0.7s, which then decides it in three further
monadic
checks. The lazy loop instead explores the truncated frontier first, and
those
explorations build very large derivative terms — 96k cofactor calls take
20s
against 165k in 0.7s on `master`, at 82MB versus 18MB.

The node budget does not catch 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 it lost `medium_sat_0026`. Charging the budget
by term
size would likely fix it, but that is a broader change than belongs
here.

### Follow-up: the budget is now miscalibrated

Worth flagging because it makes the numbers above an understatement. The
DFS
budget is a hard 200,000 pops, calibrated when each pop was ~8x more
expensive.
`split_membership_easy_sat_0019` is the only ≥2x slowdown attributable
to the
interval product, and it is entirely this effect: at 200k the merge
build bails
on budget 25 times and falls back to legacy (3.6s, against 1.8s for the
cartesian build), while at 1,000,000 it returns in **0.17s after 131
cofactor
calls** with no bails. #10384 measured +5/+6 decided at the raised
budget. That
is a policy change affecting all users, so it belongs in its own PR.

---------

Co-authored-by: Nikolaj Bjorner <nbjorner@microsoft.com>
Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
Co-authored-by: veanes <veanes@microsoft.com>
Copilot-Session: 2bcccba7-ac7d-476e-8dfe-718a21d37554
Copilot-Session: a2ce3573-4e15-4a4a-afb5-21e3cb04e4a2
This commit is contained in:
Margus Veanes 2026-08-07 21:39:20 -07:00 • committed by GitHub
parent 4e0ec5d01b
commit 9866fee194
No known key found for this signature in database
GPG key ID: B5690EEEBB952194
9 changed files with 640 additions and 248 deletions
Download patch file Download diff file Expand all files Collapse all files

1
src/ast/rewriter/CMakeLists.txt
View file

@ -48,6 +48,7 @@ z3_add_component(rewriter
seq_range_predicate.cpp
seq_rewriter.cpp
seq_regex_bisim.cpp
seq_regex_live.cpp
seq_skolem.cpp
term_enumeration.cpp
th_rewriter.cpp

11
src/ast/rewriter/seq_derive.cpp
View file

@ -39,7 +39,8 @@ namespace seq {
m_br(m),
m_re(re),
m_trail(m),
m_cofactor_cache(m),
m_brz_cofactor_cache(m),
m_ant_cofactor_cache(m),
m_ele(m),
m_path_expr(m) {
m_br.set_flat_and_or(false);
@ -1572,15 +1573,18 @@ namespace seq {
}
expr_ref_pair_vector const &derive::get_cached_cofactors(transition_mode mode, expr *r) {
cofactor_cache& cache =
mode == transition_mode::light_antimirov_tm ?
m_ant_cofactor_cache : m_brz_cofactor_cache;
expr_ref_pair_vector *v = nullptr;
if (m_cofactor_cache.find(r, v))
if (cache.find(r, v))
return *v;
v = alloc(expr_ref_pair_vector, m);
if (mode == transition_mode::light_antimirov_tm)
light_ant_derivative_cofactors(r, *v);
else
derivative_cofactors(r, *v);
m_cofactor_cache.insert(r, v); // takes ownership of v and pins the key r
cache.insert(r, v); // takes ownership of v and pins the key r
return *v;
}
@ -1659,4 +1663,3 @@ namespace seq {
}
}

6
src/ast/rewriter/seq_derive.h
View file

@ -95,7 +95,8 @@ namespace seq {
obj_pair_map<expr, expr, expr*> m_atop_cache, m_btop_cache; // post-simplify cache
expr_ref_vector m_trail; // pin cached results
cofactor_cache m_cofactor_cache;
cofactor_cache m_brz_cofactor_cache;
cofactor_cache m_ant_cofactor_cache;
// Op cache for ITE-hoisting operations (union, inter, concat, complement)
// Path-aware caches: key is (a, b, path_expr) for binary ops, (a, path_expr) for complement
@ -276,7 +277,8 @@ namespace seq {
expr_ref_pair_vector const &get_cached_cofactors(transition_mode mode, expr *r);
void maybe_reset_cached_cofactors(unsigned cap) {
m_cofactor_cache.maybe_reset(cap);
m_brz_cofactor_cache.maybe_reset(cap);
m_ant_cofactor_cache.maybe_reset(cap);
}
/**

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

@ -51,6 +51,7 @@ Author:
#include "ast/rewriter/seq_monadic.h"
#include "ast/rewriter/guard_set.h"
#include "ast/rewriter/seq_range_collapse.h"
#include <set>
#include <vector>
#include <map>
@ -131,74 +132,91 @@ expr_ref_pair_vector const& seq_monadic::derivative_cofactors(expr* r) {
return m_rw.get_derive().get_cached_cofactors(m_config.m_mode, r);
}
bool seq_monadic::live_states(expr* R, expr_ref_vector& out) {
obj_map<expr, unsigned> id;
expr_ref_vector states(m);
vector<svector<unsigned>> succ;
bool_vector maybe_null;
auto intern = [&](expr* s) -> unsigned {
unsigned k;
if (id.find(s, k)) return k;
k = states.size();
id.insert(s, k);
states.push_back(s);
succ.push_back(svector<unsigned>());
maybe_null.push_back(nullable(s) != l_false); // unknown nullability => keep (conservative)
return k;
};
intern(R);
const unsigned STATE_CAP = 1u << 12;
for (unsigned i = 0; i < states.size(); ++i) {
if (states.size() > STATE_CAP) {
m_stats.inc_bail(bail_reason::state_cap);
return false;
}
if (!m.inc()) {
m_stats.inc_bail(bail_reason::resource);
return false;
}
expr_ref_pair_vector const& cof = derivative_cofactors(states.get(i));
for (auto const& [g, t] : cof) {
if (re().is_empty(t)) continue;
unsigned k = intern(t); // MUST precede succ[i] indexing: intern may
succ[i].push_back(k); // grow (realloc) succ, invalidating succ[i]&
}
}
unsigned n = states.size();
bool_vector live;
live.resize(n, false);
for (unsigned i = 0; i < n; ++i)
live[i] = maybe_null[i];
for (bool ch = true; ch; ) {
ch = false;
for (unsigned i = 0; i < n; ++i)
if (!live[i])
for (unsigned j : succ[i])
if (live[j]) { live[i] = true; ch = true; break; }
}
for (unsigned i = 0; i < n; ++i)
if (live[i]) { out.push_back(states.get(i)); m_pin.push_back(states.get(i)); }
return true;
void seq_monadic::reset_ivl_cache() {
for (auto& kv : m_ivl_cache)
dealloc(kv.m_value);
m_ivl_cache.reset();
m_ivl_pin.reset();
}
expr_ref_vector const* seq_monadic::live_states_cached(expr* R) {
expr_ref_vector* v = nullptr;
if (m_live_cache.find(R, v))
return v; // may be null: previously gave up on R
v = alloc(expr_ref_vector, m);
if (!live_states(R, *v)) {
dealloc(v);
v = nullptr;
}
m_pin.push_back(R); // keep the key alive for the cache's lifetime
m_live_cache.insert(R, v);
return v;
}
// Canonical interval form of r's derivative: the cofactor guards, translated into the
// range algebra, refined into a sorted list of disjoint ranges, each labelled with the
// targets reachable on it. Adjacent ranges with identical target sets are merged, so the
// result is the minimal ordered-ITE ("t-regex") representation of the transition relation.
// Returns null when some guard falls outside the range algebra.
seq_monadic::ivl_list const* seq_monadic::interval_cofactors(expr* r, expr* v0) {
ivl_list* res = nullptr;
if (m_ivl_cache.find(r, res))
return res && res->ok ? res : nullptr;
void seq_monadic::reset_live_cache() {
for (auto const& [k, v] : m_live_cache)
dealloc(v);
m_live_cache.reset();
unsigned max_char = u().max_char();
res = alloc(ivl_list);
m_ivl_cache.insert(r, res);
m_ivl_pin.push_back(r);
// (lo, hi, target) triples, plus the boundary set of this state's own partition.
struct tr_t { unsigned lo, hi; expr* t; };
svector<tr_t> tr;
svector<unsigned> bounds;
bounds.push_back(0);
for (auto const& [g, t] : derivative_cofactors(r)) {
if (re().is_empty(t))
continue;
seq::range_predicate* p = nullptr;
if (!m_rp_cache.find(g, p)) {
p = m_rp_cache.fresh(max_char);
if (!seq::guard_to_range_predicate(u(), v0, g, *p)) {
m_rp_cache.insert(g, nullptr);
res->ok = false;
return nullptr;
}
m_rp_cache.insert(g, p);
}
else if (!p) {
res->ok = false;
return nullptr;
}
m_ivl_pin.push_back(t);
for (auto const& rg : p->ranges()) {
tr.push_back({ rg.first, rg.second, t });
bounds.push_back(rg.first);
if (rg.second < max_char)
bounds.push_back(rg.second + 1);
}
}
if (tr.empty())
return res; // dead state: no outgoing transition
std::sort(bounds.begin(), bounds.end());
bounds.shrink((unsigned)(std::unique(bounds.begin(), bounds.end()) - bounds.begin()));
ptr_vector<expr> hits;
for (unsigned bi = 0; bi < bounds.size(); ++bi) {
unsigned lo = bounds[bi];
unsigned hi = bi + 1 < bounds.size() ? bounds[bi + 1] - 1 : max_char;
hits.reset();
for (auto const& e : tr)
if (e.lo <= lo && lo <= e.hi)
hits.push_back(e.t);
if (hits.empty())
continue; // gap: no transition on this range
// extend the previous range when it carries exactly the same target set
if (!res->ranges.empty()) {
ivl_range& prev = res->ranges.back();
if (prev.hi + 1 == lo && prev.count == hits.size()) {
bool same = true;
for (unsigned k = 0; k < hits.size() && same; ++k)
same = res->targets[prev.first + k] == hits[k];
if (same) {
prev.hi = hi;
continue;
}
}
}
res->ranges.push_back({ lo, hi, res->targets.size(), hits.size() });
res->targets.append(hits.size(), hits.data());
}
return res;
}
lbool seq_monadic::product_nonempty(svector<component> const& comps, expr_ref* witness_word) {
@ -290,6 +308,92 @@ lbool seq_monadic::product_nonempty(svector<component> const& comps, expr_ref* w
branches.resize(n);
key st_key;
bool bail = false;
// ---- interval-refinement ("t-regex merge") product --------------------------
// Over the character sort every cofactor guard denotes a union of ranges, so each
// component's derivative has a canonical ordered-interval ("t-regex") form, cached
// per state by interval_cofactors. The joint transitions are then exactly the cells
// of the common refinement of those n interval lists, obtained by a cursor merge in
// O(sum_i intervals_i) -- whereas the cartesian enumeration below tries
// prod_i(k_i) combinations, almost all of which are pruned as empty.
bool const sweep_ok = u().is_char(m_elem_sort);
unsigned const max_char = sweep_ok ? u().max_char() : 0;
svector<ivl_list const*> sw_lists;
svector<unsigned> sw_cur, sw_odo;
sw_lists.resize(n);
sw_cur.resize(n);
sw_odo.resize(n);
// Returns false when some guard falls outside the range algebra, in which case the
// caller falls back to the cartesian enumeration for this product state.
auto sweep = [&]() -> bool {
for (unsigned i = 0; i < n; ++i) {
sw_lists[i] = interval_cofactors(st[i], var0);
if (!sw_lists[i])
return false;
if (sw_lists[i]->ranges.empty())
return true; // component is stuck: no joint transition
sw_cur[i] = 0;
}
uint64_t b = 0;
while (b <= max_char) {
uint64_t next = (uint64_t)max_char + 1;
bool covered = true, done = false;
for (unsigned i = 0; i < n; ++i) {
auto const& rs = sw_lists[i]->ranges;
unsigned& c = sw_cur[i];
while (c < rs.size() && rs[c].hi < b)
++c;
if (c == rs.size()) { // this component has no transition left
done = true;
break;
}
if (rs[c].lo > b) { // gap in this component: skip ahead
covered = false;
next = std::min(next, (uint64_t)rs[c].lo);
}
else
next = std::min(next, (uint64_t)rs[c].hi + 1);
}
if (done)
break;
if (covered) {
// Emit every combination of the targets active on this cell. The modes
// whose cofactors partition the domain give exactly one target per
// component; the antimirov-style modes may give several.
for (unsigned i = 0; i < n; ++i)
sw_odo[i] = 0;
while (true) {
for (unsigned i = 0; i < n; ++i) {
auto const& r = sw_lists[i]->ranges[sw_cur[i]];
cur[i] = sw_lists[i]->targets[r.first + sw_odo[i]];
}
key const& ck = fill_key(cur);
if (visited.find(ck) == visited.end()) {
visited.insert(ck);
if (witness_word) {
expr* e = u().mk_char((unsigned)b);
m_pin.push_back(e);
parent[ck] = { st_key, e };
}
for (unsigned j = 0; j < n; ++j)
work.push_back(cur[j]);
}
unsigned i = n;
while (i-- > 0) {
if (++sw_odo[i] < sw_lists[i]->ranges[sw_cur[i]].count)
break;
sw_odo[i] = 0;
}
if (i == UINT_MAX)
break; // odometer wrapped: cell exhausted
}
}
b = next;
}
return true;
};
std::function<void(unsigned, guard_set const&)> rec =
[&](unsigned i, guard_set const& acc) {
if (bail) return;
@ -352,13 +456,17 @@ lbool seq_monadic::product_nonempty(svector<component> const& comps, expr_ref* w
return l_undef;
}
if (witness_word)
st_key = fill_key(st);
if (sweep_ok && sweep())
continue;
for (unsigned i = 0; i < n; ++i)
branches[i] = &derivative_cofactors(st[i]);
// joint transitions = cartesian product of the branches with the guards
// conjoined; prune as soon as the accumulated guard is empty, bail on unknown.
if (witness_word)
st_key = fill_key(st);
guard_set top(m, u(), m_elem_sort, var0, &m_rp_cache);
rec(0, top);
if (bail)
@ -417,7 +525,7 @@ void seq_monadic::reset_search() {
m_der_cache.reset();
m_nullable_cache.reset();
m_undef_vars = 0;
reset_live_cache();
m_live_states.reset();
}
bool seq_monadic::prepare(membership_vec const& memberships) {
@ -546,23 +654,13 @@ lbool seq_monadic::dfs_atoms(unsigned mi, unsigned i, expr* R) {
// A variable: the last atom is a plain membership in R, otherwise the variable drives
// the derivative automaton from R to some live state q, which splits the search.
bool last_atom = (i + 1 == atoms.size());
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;
for (expr* q : *Q)
targets.push_back(q);
}
unsigned vi = var_index(a.var.get());
uint64_t pos = (static_cast<uint64_t>(mi) << 32) | i;
uint64_t last = 0;
bool finalize = m_last_occ.find(a.var.get(), last) && last == pos;
bool any_undef = false;
for (expr* target : targets) {
// Explores one split target; the caller stops at the first l_true.
auto explore = [&](expr* target) -> lbool {
m_groups[vi].push_back(component{ a.var.get(), R, target });
// The group's emptiness test has to be run at some point anyway; running it as
// soon as the group is complete (or as soon as it holds several components, where
@ -583,6 +681,19 @@ lbool seq_monadic::dfs_atoms(unsigned mi, unsigned i, expr* R) {
--m_undef_vars;
}
m_groups[vi].pop_back();
return r;
};
if (last_atom)
return explore(nullptr);
// The live states are consumed as they are produced, so a satisfying branch under an
// early state means the rest of the reachable set is never expanded. That is what
// makes a root with an exponential live set tractable when a witness is found early.
bool any_undef = false;
auto live = m_live_states.reachable_live(R);
for (expr* q : live) {
lbool r = explore(q);
if (r == l_true)
return l_true;
if (r == l_undef) {
@ -591,6 +702,14 @@ lbool seq_monadic::dfs_atoms(unsigned mi, unsigned i, expr* R) {
any_undef = true;
}
}
// Short of the full reachable set the unexplored split states could still hold a
// solution, so the l_false the loop would otherwise report is not justified.
if (live.failed()) {
m_stats.inc_bail(
live.failure_reason() == seq::live_states::failure::state_cap ?
bail_reason::state_cap : bail_reason::resource);
return l_undef;
}
return any_undef ? l_undef : l_false;
}
@ -600,6 +719,7 @@ lbool seq_monadic::decide(membership_vec const& memberships) {
reset_search(); // clear the caches before dropping the
m_pin.reset(); // pins that keep their keys alive
m_rp_cache.maybe_reset(1u << 16);
reset_ivl_cache();
m_rw.get_derive().maybe_reset_cached_cofactors(1u << 16);
m_budget = 200000;
m_giveup = false;
@ -835,7 +955,7 @@ std::ostream& seq_monadic::display(std::ostream& out) const {
<< " :group-cache-size " << m_group_cache.size() << "\n"
<< " :derivative-cache-size " << m_der_cache.size() << "\n"
<< " :nullable-cache-size " << m_nullable_cache.size() << "\n"
<< " :live-cache-size " << m_live_cache.size() << "\n"
<< " :live-cache-size " << m_live_states.num_states() << "\n"
<< " :pinned-expressions " << m_pin.size() << ")\n";
out << " :statistics\n"

37
src/ast/rewriter/seq_monadic.h
View file

@ -63,6 +63,7 @@ Author:
#include "ast/rewriter/seq_rewriter.h"
#include "ast/rewriter/seq_range_predicate.h"
#include "ast/rewriter/seq_regex_live.h"
#include "ast/rewriter/guard_set.h"
#include "ast/rewriter/th_rewriter.h"
#include "util/lbool.h"
@ -113,6 +114,20 @@ class seq_monadic {
statistics m_stats;
obj_map<expr, expr*> m_model; // last extracted model (var -> witness); see get_model()
guard_set::cache m_rp_cache; // cofactor guard -> range predicate
// Interval ("t-regex") form of a state's derivative cofactors over the character sort:
// a canonical list of disjoint ranges in increasing order, each carrying the targets
// reachable on that range. Built once per state and merged by the product, so the
// product enumerates only the cells of the common refinement.
struct ivl_range { unsigned lo, hi, first, count; };
struct ivl_list {
svector<ivl_range> ranges;
ptr_vector<expr> targets; // ranges[i] owns targets[first .. first+count)
bool ok = true; // false: some guard is outside the range algebra
};
obj_map<expr, ivl_list*> m_ivl_cache;
expr_ref_vector m_ivl_pin; // pins the states and targets the cache refers to
ivl_list const* interval_cofactors(expr* r, expr* v0);
void reset_ivl_cache();
obj_pair_map<expr, expr, expr*> m_der_cache; // memoizes der_elem per (regex, element)
obj_map<expr, char> m_nullable_cache; // memoizes nullability (0 false / 1 true / 2 unknown);
// seq_rewriter's own cache is capped and flushed whole
@ -166,7 +181,7 @@ class seq_monadic {
};
group_sig m_sig_buf; // reused by group_nonempty (avoids allocating per lookup)
std::unordered_map<group_sig, lbool, group_sig_hash> m_group_cache;
obj_map<expr, expr_ref_vector*> m_live_cache; // regex -> live split states (null = gave up)
seq::live_states m_live_states;
// Brzozowski derivative of regex `r` by the concrete element `elem`. Memoized on
// (r, elem): the search revisits the same constant step on many branches.
@ -175,20 +190,10 @@ class seq_monadic {
// Memoized nullability of a derivative state: l_true / l_false / l_undef (unknown).
lbool nullable(expr* r);
// Symbolic transition cofactors in the selected mode. Memoized per regex `r` in
// m_cofactors: the returned vector is owned by that cache (see the cofactor_cache
// class above for the persistence/reset policy).
// Symbolic transition cofactors in the selected mode. The returned vector is owned
// by seq_rewriter's mode-specific cofactor cache.
expr_ref_pair_vector const& derivative_cofactors(expr* r);
// Live reachable derivative states of R (BFS over cofactor targets + liveness
// least-fixpoint). These are the split states q. Returns false on a cap overrun.
bool live_states(expr* R, expr_ref_vector& out);
// Memoized live_states. Returns null if the computation gave up for this regex.
expr_ref_vector const* live_states_cached(expr* R);
void reset_live_cache();
// Product-reachability emptiness of a conjunction of components (all on one
// variable). l_false = empty (unsat), l_true = non-empty (sat), l_undef = gave up
// (cap overrun, non-range guard, or undecidable nullability).
@ -248,10 +253,10 @@ public:
seq_monadic(seq_rewriter& rw, trail_stack& undo_trail,
seq::transition_mode mode = seq::transition_mode::light_antimirov_tm) :
m(rw.m()), m_rw(rw), m_thrw(rw.m()), m_undo_trail(undo_trail),
m_pin(rw.m()), m_config(mode), m_rp_cache(rw.m()),
m_regexes(rw.m()) {}
m_pin(rw.m()), m_config(mode), m_rp_cache(rw.m()), m_ivl_pin(rw.m()),
m_regexes(rw.m()), m_live_states(rw, mode, 1u << 12) {}
~seq_monadic() { reset_live_cache(); }
~seq_monadic() { reset_ivl_cache(); }
void collect_statistics(::statistics &st) const;

312
src/ast/rewriter/seq_regex_live.cpp Normal file
View file

@ -0,0 +1,312 @@
/*++
Copyright (c) 2026 Microsoft Corporation
Module Name:
seq_regex_live.cpp
Abstract:
Shared lazy live-state traversal for regular-expression derivatives.
--*/
#include "ast/rewriter/seq_regex_live.h"
#include "ast/rewriter/seq_rewriter.h"
#include "util/obj_hashtable.h"
#include "util/uint_set.h"
namespace seq {
struct live_states::search {
svector<unsigned> m_to_explore;
unsigned m_explore_head = 0;
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;
bool m_complete = false;
};
struct live_states::imp {
seq_rewriter& m_rw;
ast_manager& m;
seq_util::rex& m_re;
transition_mode m_mode;
unsigned m_max_states;
obj_map<expr, unsigned> m_ids;
expr_ref_vector m_states;
vector<svector<unsigned>> m_successors;
svector<char> m_nullable;
bool_vector m_expanded;
obj_map<expr, search*> m_searches;
imp(seq_rewriter& rw, transition_mode mode, unsigned max_states) :
m_rw(rw),
m(rw.m()),
m_re(rw.u().re),
m_mode(mode),
m_max_states(max_states),
m_states(m) {
}
~imp() {
reset();
}
unsigned intern(expr* r) {
unsigned id = 0;
if (m_ids.find(r, id))
return id;
id = m_states.size();
m_ids.insert(r, id);
m_states.push_back(r);
m_successors.push_back(svector<unsigned>());
m_nullable.push_back(2);
m_expanded.push_back(false);
return id;
}
void resize(search& s) {
unsigned size = m_states.size();
if (s.m_predecessors.size() < size)
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) {
if (m_nullable[id] != 2)
return m_nullable[id];
expr* r = m_states.get(id);
lbool n = m_re.get_info(r).nullable;
if (n == l_undef) {
expr_ref f = m_rw.is_nullable(r);
n = m.is_true(f) ? l_true : m.is_false(f) ? l_false : l_undef;
}
m_nullable[id] = n == l_true ? 1 : n == l_false ? 0 : 3;
return m_nullable[id];
}
void mark_live(search& s, unsigned id) {
svector<unsigned> todo;
todo.push_back(id);
while (!todo.empty()) {
id = todo.back();
todo.pop_back();
if (!s.m_seen.contains(id) || s.m_live[id])
continue;
s.m_live[id] = true;
s.m_live_frontier.push_back(id);
for (unsigned predecessor : s.m_predecessors[id])
todo.push_back(predecessor);
}
}
bool add_state(search& s, unsigned id) {
if (s.m_seen.contains(id))
return true;
if (s.m_to_explore.size() >= m_max_states) {
s.m_failure = failure::state_cap;
return false;
}
resize(s);
s.m_seen.insert(id);
s.m_to_explore.push_back(id);
if (nullable(id) != 0)
mark_live(s, id);
return true;
}
bool expand_state(unsigned id, failure& f) {
if (m_expanded[id])
return true;
if (!m.inc()) {
f = failure::resource;
return false;
}
m_expanded[id] = true;
nullable(id);
auto const& cofactors = m_rw.get_derive().get_cached_cofactors(m_mode, m_states.get(id));
for (auto const& [guard, target] : cofactors) {
if (m_re.is_empty(target))
continue;
unsigned target_id = intern(target);
if (!m_successors[id].contains(target_id))
m_successors[id].push_back(target_id);
}
return true;
}
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;
}
void expand(search& s) {
if (s.m_complete || s.m_failure != failure::none)
return;
if (s.m_explore_head == s.m_to_explore.size()) {
close(s);
return;
}
unsigned id = s.m_to_explore[s.m_explore_head++];
if (!expand_state(id, s.m_failure))
return;
resize(s);
for (unsigned target : m_successors[id]) {
if (!add_state(s, target))
return;
if (!s.m_predecessors[target].contains(id))
s.m_predecessors[target].push_back(id);
if (s.m_live[target])
mark_live(s, id);
}
}
bool ensure(search& s, unsigned index) {
while (index >= s.m_live_frontier.size() &&
!s.m_complete &&
s.m_failure == failure::none)
expand(s);
return index < s.m_live_frontier.size();
}
search* get_search(expr* root) {
search* s = nullptr;
if (m_searches.find(root, s))
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;
}
void reset() {
for (auto const& [root, s] : m_searches)
dealloc(s);
m_searches.reset();
m_ids.reset();
m_states.reset();
m_successors.reset();
m_nullable.reset();
m_expanded.reset();
}
};
live_states::live_states(seq_rewriter& rw, transition_mode mode, unsigned max_states) :
m_imp(alloc(imp, rw, mode, max_states)) {
}
live_states::~live_states() {
dealloc(m_imp);
}
expr* live_states::iterator::operator*() const {
return m_owner->get_live(m_search, m_index);
}
live_states::iterator& live_states::iterator::operator++() {
++m_index;
return *this;
}
bool live_states::iterator::operator!=(iterator const& other) const {
if (other.m_end)
return m_owner->ensure(m_search, m_index);
return m_owner != other.m_owner ||
m_search != other.m_search ||
m_index != other.m_index ||
m_end != other.m_end;
}
live_states::iterator live_states::reachable::begin() const {
return iterator(m_owner, m_search, 0, false);
}
live_states::iterator live_states::reachable::end() const {
return iterator(m_owner, m_search, 0, true);
}
bool live_states::reachable::failed() const {
return m_owner->get_failure(m_search) != failure::none;
}
live_states::failure live_states::reachable::failure_reason() const {
return m_owner->get_failure(m_search);
}
bool live_states::reachable::is_dead() {
return !m_owner->ensure(m_search, 0) && !failed();
}
live_states::reachable live_states::reachable_live(expr* r) {
return reachable(this, m_imp->get_search(r));
}
bool live_states::contains(expr* r) const {
return m_imp->m_ids.contains(r);
}
unsigned live_states::state_id(expr* r) {
return m_imp->intern(r) + 1;
}
unsigned live_states::num_states() const {
return m_imp->m_states.size();
}
void live_states::reset() {
m_imp->reset();
}
bool live_states::ensure(search* s, unsigned index) {
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]);
}
live_states::failure live_states::get_failure(search* s) const {
return s->m_failure;
}
}

83
src/ast/rewriter/seq_regex_live.h Normal file
View file

@ -0,0 +1,83 @@
/*++
Copyright (c) 2026 Microsoft Corporation
Module Name:
seq_regex_live.h
Abstract:
Shared lazy live-state traversal for regular-expression derivatives.
--*/
#pragma once
#include "ast/rewriter/seq_derive.h"
#include "ast/ast.h"
class seq_rewriter;
namespace seq {
class live_states {
struct search;
struct imp;
public:
enum class failure {
none,
state_cap,
resource
};
class iterator {
live_states* m_owner = nullptr;
search* m_search = nullptr;
unsigned m_index = 0;
bool m_end = false;
public:
iterator(live_states* owner, search* s, unsigned index, bool end) :
m_owner(owner), m_search(s), m_index(index), m_end(end) {}
expr* operator*() const;
iterator& operator++();
bool operator!=(iterator const& other) const;
};
class reachable {
live_states* m_owner = nullptr;
search* m_search = nullptr;
public:
reachable(live_states* owner, search* s) :
m_owner(owner), m_search(s) {}
iterator begin() const;
iterator end() const;
bool failed() const;
failure failure_reason() const;
bool is_dead();
};
private:
imp* m_imp;
bool ensure(search* s, unsigned index);
expr* get_live(search* s, unsigned index) const;
failure get_failure(search* s) const;
public:
live_states(seq_rewriter& rw,
transition_mode mode = transition_mode::brzozowski_tm,
unsigned max_states = UINT_MAX);
~live_states();
live_states(live_states const&) = delete;
live_states& operator=(live_states const&) = delete;
reachable reachable_live(expr* r);
bool contains(expr* r) const;
unsigned state_id(expr* r);
// Number of interned derivative states, i.e. the size of the shared state table.
unsigned num_states() const;
void reset();
};
}

107
src/smt/seq_regex.cpp
View file

@ -31,8 +31,7 @@ namespace smt {
ctx(th.get_context()),
m(th.get_manager()),
m_monadic(seq_rw(), ctx.get_trail_stack()),
m_state_to_expr(m),
m_state_graph(state_graph::state_pp(this, pp_state)) {
m_live_states(seq_rw(), seq::transition_mode::brzozowski_tm, 10000) {
m_monadic.set_is_var([&th](expr *e) { return th.is_var(e); });
}
@ -640,8 +639,8 @@ namespace smt {
}
if (info.interpreted) {
update_state_graph(r);
if (m_state_graph.is_dead(get_state_id(r))) {
auto live = m_live_states.reachable_live(r);
if (live.is_dead()) {
STRACE(seq_regex_brief, tout << "(dead) ";);
th.add_axiom(~lit);
return true;
@ -665,8 +664,7 @@ namespace smt {
/**
* Propagate the atom (accept s i r)
*
* Propagation triggers updating the state graph for dead state detection:
* (accept s i r) => update_state_graph(r)
* Propagation triggers derivative reachability for dead state detection:
* (accept s i r) & dead(r) => false
*
* Propagation is also blocked under certain conditions to throttle
@ -1292,101 +1290,10 @@ namespace smt {
return sk().mk("re.first", n, a().mk_int(r->get_id()), elem_sort);
}
/**
* Dead state elimination using the state_graph class
*/
unsigned seq_regex::get_state_id(expr* e) {
// Assign increasing IDs starting from 1
if (!m_expr_to_state.contains(e)) {
m_state_to_expr.push_back(e);
unsigned new_id = m_state_to_expr.size();
m_expr_to_state.insert(e, new_id);
STRACE(seq_regex_brief, tout << "new(" << expr_id_str(e)
<< ")=" << state_str(e) << " ";);
STRACE(seq_regex, tout
<< "New state ID: " << new_id
<< " = " << mk_pp(e, m) << std::endl;);
SASSERT(get_expr_from_id(new_id) == e);
}
return m_expr_to_state.find(e);
}
expr* seq_regex::get_expr_from_id(unsigned id) {
SASSERT(id >= 1);
SASSERT(id <= m_state_to_expr.size());
return m_state_to_expr.get(id - 1);
}
bool seq_regex::can_be_in_cycle(expr *r1, expr *r2) {
// TBD: This can be used to optimize the state graph:
// return false here if it is known that r1 -> r2 can never be
// in a cycle. There are various easy syntactic checks on r1 and r2
// that can be used to infer this (e.g. star height, or length if
// both are star-free).
// This check need not be sound, but if it is not, some dead states
// will be missed.
return true;
}
/*
Update the state graph with expression r and all its derivatives.
*/
bool seq_regex::update_state_graph(expr* r) {
unsigned r_id = get_state_id(r);
if (m_state_graph.is_done(r_id)) return false;
if (m_state_graph.get_size() >= m_max_state_graph_size) {
STRACE(seq_regex, tout << "Warning: ignored state graph update -- max size of seen states reached!" << std::endl;);
STRACE(seq_regex_brief, tout << "(MAX SIZE REACHED) ";);
return false;
}
STRACE(seq_regex, tout << "Updating state graph for regex "
<< mk_pp(r, m) << ") ";);
STRACE(state_graph,
if (!m_state_graph.is_seen(r_id))
tout << std::endl << "state(" << r_id << ") = " << re().to_str(r) << std::endl << "info(" << r_id << ") = " << re().get_info(r) << std::endl;);
// Add state
m_state_graph.add_state(r_id);
STRACE(seq_regex, tout << "Updating state graph for regex "
<< mk_pp(r, m) << ") " << std::endl;);
STRACE(seq_regex_brief, tout << std::endl << "USG("
<< state_str(r) << ") ";);
expr_ref r_nullable = is_nullable_wrapper(r);
if (m.is_true(r_nullable)) {
m_state_graph.mark_live(r_id);
}
else {
// Add edges to all derivatives
expr_ref_vector derivatives(m);
STRACE(seq_regex_verbose, tout
<< "getting all derivs: " << r_id << " " << std::endl;);
get_derivative_targets(r, derivatives);
for (auto const& dr: derivatives) {
unsigned dr_id = get_state_id(dr);
STRACE(seq_regex_verbose, tout
<< std::endl << " traversing deriv: " << dr_id << " ";);
STRACE(state_graph,
if (!m_state_graph.is_seen(dr_id))
tout << "state(" << dr_id << ") = " << re().to_str(dr) << std::endl << "info(" << dr_id << ") = " << re().get_info(dr) << std::endl;);
// Add state
m_state_graph.add_state(dr_id);
bool maybecycle = can_be_in_cycle(r, dr);
m_state_graph.add_edge(r_id, dr_id, maybecycle);
}
m_state_graph.mark_done(r_id);
}
STRACE(seq_regex, m_state_graph.display(tout););
STRACE(seq_regex_brief, tout << std::endl;);
STRACE(seq_regex_brief, m_state_graph.display(tout););
return true;
}
std::string seq_regex::state_str(expr* e) {
if (m_expr_to_state.contains(e))
return std::to_string(get_state_id(e));
else
return expr_id_str(e);
if (m_live_states.contains(e))
return std::to_string(m_live_states.state_id(e));
return expr_id_str(e);
}
std::string seq_regex::expr_id_str(expr* e) {
return std::string("id") + std::to_string(e->get_id());

47
src/smt/seq_regex.h
View file

@ -17,9 +17,9 @@ Author:
#pragma once
#include "util/scoped_vector.h"
#include "util/state_graph.h"
#include "ast/seq_decl_plugin.h"
#include "ast/rewriter/seq_monadic.h"
#include "ast/rewriter/seq_regex_live.h"
#include "ast/rewriter/seq_rewriter.h"
#include "ast/rewriter/seq_skolem.h"
#include "smt/smt_context.h"
@ -56,13 +56,6 @@ Author:
(next states)
d(r1)=r2: r2 is the derivative of r1
n(r1)=b: b = whether r1 is nullable or not
USG(r): updating state graph for regex r (add all derivatives)
-tr:state_graph
This is the tracing done by util/state_graph, the data structure
that seq_regex uses to track live and dead regexes, which can
altneratively be used to get a high-level picture of what states
are being explored and updated as the solver progresses.
-tr:seq_regex_verbose
Used for some more frequent tracing (in the style of seq_regex,
@ -72,21 +65,12 @@ Author:
These are the underlying sequence theory tracing, often used by
the rewriter.
DEBUGGING AND VIEWING STATE GRAPH GRAPHICAL OUTPUT
DEBUGGING
-dbg:seq_regex
Debugging that checks invariants. Currently, checks that derivative
normal form is correctly preserved in the rewriter.
-dbg:state_graph
Debugging for the state graph, which
1. Checks state graph invariants, and
2. Generates the files .z3-state-graph.dgml and .z3-state-graph.dot
which can be used to visually view the state graph being explored,
during or after executing Z3.
The output can be viewed:
- Using Visual Studio for .dgml
- Using a tool such as xdot (`xdot .z3-state-graph.dot`) for .dot
*/
namespace smt {
@ -163,23 +147,9 @@ namespace smt {
unsigned m_monadic_assumption_generation = UINT_MAX;
unsigned m_monadic_fallback_generation = UINT_MAX;
/*
state_graph for dead state detection, and associated methods
*/
ptr_addr_map<expr, unsigned> m_expr_to_state;
expr_ref_vector m_state_to_expr;
state_graph m_state_graph;
seq::live_states m_live_states;
/* map from uninterpreted regex constants to assigned regex expressions by EQ */
// expr_map m_const_to_expr;
unsigned m_max_state_graph_size { 10000 };
// Convert between expressions and states (IDs)
unsigned get_state_id(expr* e);
expr* get_expr_from_id(unsigned id);
// Cycle-detection heuristic
// Note: Doesn't need to be sound or complete (doesn't affect soundness)
bool can_be_in_cycle(expr* r1, expr* r2);
// Update the graph
bool update_state_graph(expr* r);
// Printing expressions for seq_regex_brief
std::string state_str(expr* e);
@ -239,17 +209,6 @@ namespace smt {
seq_regex_ptr must be a pointer to seq_regex and the
id must be a valid state id or else nothing is printed.
*/
static void pp_state(void* seq_regex_ptr, std::ostream& out, unsigned id, bool html_encode) {
seq_regex* sr = (seq_regex*)seq_regex_ptr;
if (sr) {
seq_util::rex re_util(sr->re());
if (1 <= id && id <= sr->m_state_to_expr.size()) {
expr* r = sr->get_expr_from_id(id);
seq_util::rex::pp(re_util, r, html_encode).display(out);
}
}
}
bool block_if_empty(expr* r, literal lit);
void add_monadic_membership(literal lit, expr* s, expr* r);
// Expand a term through theory_seq's solution map, but substitute a sub-term only