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

Build the seq_monadic product from interval refinement instead of a cartesian product (#10384)

Browse source 
Stacked on #10381 (base is `seq-live-states-early-exit`, so the diff
here is a single commit).

## What

Over the character sort every derivative cofactor guard denotes a union
of ranges, so a
state's transition relation has a canonical ordered-interval ("t-regex")
form.
`interval_cofactors` builds and caches that form per state: the cofactor
guards are
translated through the existing range-predicate cache, refined into
disjoint ranges in
increasing order, and adjacent ranges carrying the same target set are
merged.

`product_nonempty` then obtains the joint transitions of `n` components
by a **cursor merge**
over those `n` interval lists, emitting exactly the cells of their
common refinement. The
cartesian enumeration it replaces tried `prod_i(k_i)` combinations and
discarded the
infeasible ones by conjoining `guard_set`s; the merge is linear in the
number of intervals
and never constructs an empty guard.

For interval partitions of a linearly ordered alphabet the common
refinement has at most
`sum_i(I_i) + 1` cells, so this is a **product-to-sum** change in the
size of the enumerated
space.

## Why: measured on the 1545-file regex corpus, both transition modes

A temporary probe recorded, per expanded product state, `prod_i(k_i)`
against the true
refinement cell count:

| | brz (full corpus) | light-ant (ClemensRegex/generated) |
|---|---|---|
| product states | 15,353,241 | 12,575,058 |
| cartesian combinations tried | **518,144,218** | 422,362,794 |
| feasible cells | **62,846,910** | 49,683,996 |
| **ratio** | **8.24x** | **8.13x** |
| intervals per state | 10.8 | 11.0 |
| guards outside the range algebra | **0** | **0** |

Individual files reach **91.7x** (`split_membership_medium_unsat_0029`:
64.1M tried, 699K
feasible) — and those are the slowest files in the corpus.

Two measurements shaped the implementation:

* **Cofactors overlap in the antimirov-style modes** (~8% of product
states in light-ant);
they only partition in brz. Picking "the" applicable cofactor per
component would silently
drop successors, so every combination of the targets active on a cell is
emitted.
* **Caching the per-state interval form is what makes this pay off.** An
earlier version that
translated guards and sorted boundaries at each *product* state was
correct but **2.2x
slower** than the cartesian code. States are shared across enormously
many product states,
  so the interval form must be built once per state.

## Results

vs this PR's base (#10381) — identical verdict on every one of the 1545
files, 0 mismatches:

| mode | decided | solve time on decided files | speedup |
|---|---|---|---|
| brz | 1472 -> 1472 | 42,573 ms -> 20,811 ms | **2.05x** |
| light-ant | 1469 -> 1469 | 31,836 ms -> 13,491 ms | **2.36x** |

vs `master` (baseline rebuilt and re-run from scratch for this
comparison), the two stacked
changes contribute along different axes:

| step | brz decided | brz speed | light-ant decided | light-ant speed |
|---|---|---|---|---|
| master | 1467 | 1.00x | 1465 | 1.00x |
| + #10381 | 1472 | 1.12x | 1469 | 1.28x |
| + this PR | 1472 | **4.27x** | 1469 | **4.77x** |

Speedups are over the files decided by both; aggregate totals are
meaningless here because 73
files sit pinned at the harness timeout and contribute a constant
regardless of solver speed.

`seq_monadic`, `seq_rewriter`, `seq_regex`, `seq_range_predicate` and
`seq_regex_live` unit
tests all pass.

## Scope

The cartesian path is kept unchanged for non-character element sorts and
as a fallback for
guards outside the range algebra, so `guard_set`'s generic
candidate-basis path and
`bail_reason::guard` still apply there.

## Follow-up, not included here

The DFS budget (200,000 product-state pops) is a hard cap, and each pop
is now ~8x cheaper.
Raising it to 1,000,000 decides **1477 brz / 1475 light-ant** (+5 / +6,
0 lost, 0 mismatch) at
comparable wall time; head-to-head at that budget the merge is **4.64x**
faster than the
cartesian enumeration and decides 2 more files. That is a policy change
affecting all users,
so it belongs in its own PR.

---------

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-04 15:00:21 -07:00 • committed by Margus Veanes
parent 56d89a998a
commit 57ddf8e7bf
2 changed files with 197 additions and 4 deletions
Download patch file Download diff file Expand all files Collapse all files

183
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>
@ -101,6 +102,93 @@ expr_ref_pair_vector const& seq_monadic::derivative_cofactors(expr* r) {
return m_rw.get_derive().get_cached_cofactors(m_config.m_mode, r);
}
void seq_monadic::reset_ivl_cache() {
for (auto& kv : m_ivl_cache)
dealloc(kv.m_value);
m_ivl_cache.reset();
m_ivl_pin.reset();
}
// 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;
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) {
unsigned n = comps.size();
if (n == 0) {
@ -190,6 +278,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;
@ -252,13 +426,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)
@ -510,6 +688,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;

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

@ -114,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
@ -236,10 +250,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_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() = default;
~seq_monadic() { reset_ivl_cache(); }
void collect_statistics(::statistics &st) const;