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
Materializing the monadic decomposition as a DNF is the dominant cost in
the
solver. The product over per-position split degrees (and, for a
conjunction of
memberships, over memberships) is exponential, and the `DNF_CAP` of 2^14
disjuncts meant the solver mostly gave up *structurally* rather than
because the
problem was hard — it paid the full product cost before testing
anything.
This decides the same disjunction by depth-first search, without ever
materializing it.
## How it works
`decide()` -> `prepare()` -> `dfs_membership(0)`.
`prepare()` parses each membership into atoms and records every
variable's
**last occurrence** as a packed `(membership_idx << 32) | atom_idx`.
Positions
compare lexicographically in exactly the order the search visits them,
so
"have I seen this variable for the last time?" is an integer equality.
`dfs_atoms(mi, i, R)` walks one membership:
- end of atoms: the remainder is epsilon, so the branch survives iff `R`
is
nullable (an undecidable nullability propagates as `l_undef` rather than
being
guessed);
- constant element: consumed by a derivative, `re.empty` prunes
immediately;
- variable: the last atom is a plain membership, otherwise the variable
drives
the derivative automaton from `R` to some live state `q`, one child per
target.
Components are accumulated per variable in `m_groups[vi]` along the
current
branch — pushed on entry, popped on backtracking. The per-variable
emptiness
test runs as soon as the group is complete (the search just passed the
variable's last occurrence) or holds more than one component, which is
the
earliest point an inconsistency can exist. That test has to happen
anyway;
running it there prunes the whole remaining subtree instead of after the
product
has been built. The search stops at the first satisfying leaf.
A variable shared by several memberships accumulates several components
in the
same branch and they are intersected, so the joint solve falls out of
the search
rather than needing the DNF multiplication.
## Supporting changes
- `group_nonempty` memoizes on the sorted, deduplicated `(state,
target)`
signature of the group, and collapses duplicated components before the
product
search (which is exponential in component count);
- memoize live split states per regex, and `der_elem` per `(regex,
element)`;
- memoize nullability locally — `seq_rewriter`'s own cache is capped at
10000 and
`cleanup()` flushes the entire table;
- hoist the cofactor vectors out of the product loop and reference them
instead
of re-materializing `expr_ref` pairs on every pop;
- `m_budget` becomes a global node budget, and `m_giveup` unwinds the
whole
search instead of letting sibling branches keep expanding.
Removed: `build_membership_dnf`, `decide_dnf`, `simplify_dnf`, the
`disjunct`
type and `DNF_CAP`. The persistent cofactor cache and the separate
`guard_set::cache` are kept as-is; both own their pins, so they survive
the
per-`decide` `m_pin` reset.
## Results
Measured against master (4b2e69c66), same bench harness.
**regexes (1545 files), light-antimirov:** 41 benchmarks newly decided
(22 sat, 19 unsat), **no verdict regressions**, and 8.8s -> 2.2s on the
1421
files both versions decide. Unchanged: 2 timeouts, 0 crashes, 0
mismatches
against declared status. Brzozowski mode agrees: 0 mismatches, 0
disagreements
with light-antimirov.
**QF_S (22172 files):** 0 crashes, 0 timeouts, 0 mismatches on the 4089
benchmarks that are complete and have a declared status. Verdicts are
identical
to master.
Unit tests pass in both transition modes.
## Caveat
On the 81 files neither version decides, DFS costs more (62s -> 149s):
it
explores until the 200000-node budget is exhausted, whereas the DNF path
bailed
immediately at its structural 2^14 cap. `m_budget` has not been retuned
since
the per-node cost dropped, so there is likely room to recover most of
that
without losing the 41 newly decided benchmarks.
---------
Co-authored-by: Margus Veanes <margus@microsoft.com>
Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
Copilot-Session: a2ce3573-4e15-4a4a-afb5-21e3cb04e4a2
The cofactor cache is a pure function of the regex (and the fixed transition
mode), independent of the membership set, so tearing it down on every solve()/
decide() call forced it to be recomputed n+1 times during minimize_core()'s n
deletion trials. Keep it instead, resetting only when it grows past a size cap.
Encapsulate the cofactor memo, its pinned-key trail, and the coupled range-
predicate (guard_set_cache) into a self-contained cofactor_cache class with
find/insert/reset/maybe_reset, so the three reset in lockstep (the range
predicates' guards are owned by the cofactor vectors).
Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
Copilot-Session: 57b9b87e-950a-49ea-bbb3-ed585646a5a9
Addresses code review feedback on PR #10361: the raw `obj_map` typedef +
static `dealloc_cache` helper is replaced by a proper `guard_set_cache`
class that owns its memory and adds a recycling optimization.
## Changes
- **New `guard_set_cache` class** (`guard_set.h` / `.cpp`):
- `m_cache` — `obj_map<expr, seq::range_predicate*>` (null value =
unsupported guard, avoids retranslation)
- `m_fresh` — pre-allocated `range_predicate*` recycled across failed
translations; when `guard_to_range_predicate` rejects a guard, the heap
object is retained in `m_fresh` instead of deallocated, so the next miss
reuses it without an alloc/dealloc round-trip
- Public API: `reset()`, `find(expr*, seq::range_predicate*&) → bool`,
`fresh(unsigned max_char) → seq::range_predicate*`, `insert(expr*,
seq::range_predicate*)`
- **`guard_set`**: removed `rp_cache` typedef and `dealloc_cache`
static; constructor parameter updated to `guard_set_cache*`; `conjoin`
updated to use `fresh()` + `insert()` for the recycling path
- **`seq_monadic`**: field type `guard_set::rp_cache` →
`guard_set_cache`; reset call updated to `m_rp_cache.reset()`
---------
Co-authored-by: copilot-swe-agent[bot] <198982749+Copilot@users.noreply.github.com>
Co-authored-by: Nikolaj Bjorner <nikolaj@cs.stanford.edu>
`guard_set::conjoin` re-translated its guard expression into a
`seq::range_predicate` on every call. It sits in the innermost loop of
`seq_monadic::product_nonempty`'s product-transition enumeration, where
the same handful of cofactor guards recurs on every branch of the
product search — a single regex benchmark was measured at **4.4M
translations of a few dozen distinct guards**.
## Change
Add an optional `guard -> range_predicate` cache to `guard_set`. It is
owned by the caller so its lifetime can be tied to the lifetime of the
guard expressions themselves; `seq_monadic` keys it off
`m_cofactor_cache` (which owns the guards) and resets both together. A
null cache entry records an unsupported guard, preserving the `m_ok =
false` behaviour without retranslating.
The cache is used only on the character-sort path, and is valid only
while every `guard_set` sharing it uses the same element variable `v0`.
That holds in `seq_monadic`: `v0` is `m.mk_var(0, m_elem_sort)`, which
is hash-consed, and the element sort is fixed for the duration of a
solve. The parameter defaults to `nullptr`, so any other caller keeps
the previous behaviour unchanged.
No behavioural change.
## Validation
`test-z3 seq_monadic`: ALL PASS (0 fail) in both `brz` and `light-ant`
modes.
1545-file regex corpus (`light-ant`, 20s timeout per file):
| | master | this PR |
|---|---|---|
| sat / unsat / undef | 1166 / 255 / 121 | 1166 / 255 / 121 |
| timeouts | 3 | 2 |
| solve time, 1421 files decided by both | 74.7 s | **8.4 s (~9x)** |
Verdicts are identical to master on every file; one benchmark that
previously hit the 20s timeout now terminates.
Full QF_S corpus (22,172 files) on the follow-up branch that builds on
this one: 0 crashes, 0 timeouts, and on the 4,089 benchmarks where the
monadic solver is complete and the expected status is known, 0
mismatches against the declared status.
Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
Copilot-Session: a2ce3573-4e15-4a4a-afb5-21e3cb04e4a2
check() now records the dependencies of an unsat subset in m_core, exposed via
ptr_vector<u_dependency> const& core(). On l_false it calls minimize_core:
with the new m_min_core flag (set_min_core, default true) it deletion-minimizes
to a minimal unsat subset containing only constraints that participate in the
contradiction; with the flag off it returns all membership dependencies.
Add unit tests asserting the core omits irrelevant constraints (e.g. x in a*,
x in ~a*, y in b* has core {x-constraints} only), exercising both flag states.
The test harness runs with minimization disabled by default.
Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
Copilot-Session: 57b9b87e-950a-49ea-bbb3-ed585646a5a9
Replace the batch solve_and(mems) with an incremental interface:
void add(expr* term, expr* regex, u_dependency* d);
lbool check();
add() stores each (term, regex, dependency) triple in
m_memberships (vector<tuple<expr_ref, expr_ref, u_dependency*>>); the
dependency is retained for future unsat-core tracking and may be nullptr.
check() decides the accumulated conjunction (the former solve_and body) and
consumes the memberships; an empty conjunction is sat. Update the unit tests
and benchmark to the add()/check() API.
Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
Copilot-Session: 57b9b87e-950a-49ea-bbb3-ed585646a5a9
Remove the obj_map<expr,expr*>* model out-parameter from solve/solve_and/
decide_dnf. Add an m_gen_model flag (default true) with set_gen_model(bool),
store the extracted model in m_model (reset at the top of decide_dnf), and
expose get_model(). Switch live_states out to expr_ref_vector and the
product_nonempty state vectors to ptr_vector<expr>. Simplify the concat case
of parse_term with all_of. Disable model generation in the sat-only unit
tests and the benchmark.
Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
Copilot-Session: 57b9b87e-950a-49ea-bbb3-ed585646a5a9
- decompose and live_states now return bool instead of a bool& ok out-param.
- Use is_uninterp_const(t) in parse_term.
- Use braced pair init and structured bindings over obj_map iteration.
Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
Copilot-Session: 57b9b87e-950a-49ea-bbb3-ed585646a5a9
Memoize derivative_cofactors per regex in an owning cache so each regex's
cofactors are computed once per top-level solve. The cache is reset at the
start of solve()/solve_and() and freed in the destructor.
Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
Copilot-Session: 57b9b87e-950a-49ea-bbb3-ed585646a5a9
Per-variable extra constraints are now expressed as additional (var in R')
memberships passed to solve_and, so the var_extra parameter is dropped from
solve/solve_and and the internal decide_dnf. Tests updated to route extra
constraints through solve_and.
Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
Copilot-Session: 57b9b87e-950a-49ea-bbb3-ed585646a5a9
Extract the guard_set class (element-value set over derivative cofactor
guards) from the anonymous namespace in seq_monadic.cpp into a
self-contained guard_set.h / guard_set.cpp pair.
Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
Copilot-Session: 57b9b87e-950a-49ea-bbb3-ed585646a5a9
## Summary
Pin constant elements extracted while parsing sequence terms so they
remain alive throughout monadic decomposition.
Without these references, character ASTs could be reclaimed while still
stored as raw pointers in decomposition atoms, causing assertion
failures, fast-fail exits, and access violations during derivative
construction.
The fix eliminates 26 previously observed process failures in the regex
benchmark corpus. No stack-depth bailout is needed for these failures.
Light-weight Antimirov cofactors for seq_monadic
================================================
Overview
--------
The seq_monadic solver explores symbolic regex derivatives when
computing live
states and product transitions. Its original transition representation
used
Brzozowski cofactors.
This change adds a light-weight Antimirov representation. It first
computes the
existing Brzozowski cofactors and then decomposes targets whose outer
shape is
s1 | ... | sn
or
(s1 | ... | sn) . tail
into separate transitions. Concatenations are maintained in
right-associative
form, so a distributable union occurs as the head of the concatenation.
Targets are reconstructed with mk_regex_concat to preserve
normalization.
After decomposition, transitions with the same target are merged by
disjoining
their guards. The existing path-aware cofactor traversal and range
predicates
are therefore retained.
Example
-------
For
r = .* a .{k}
the Brzozowski cofactors have the shape
[a, r | .{k}]
[^a, r]
The light-weight Antimirov transformation produces
[., r]
[a, .{k}]
This preserves the language while avoiding the deterministic subset
states
that grow exponentially on this family.
Modes
-----
seq_monadic exposes two transition modes:
light_antimirov default
brzozowski retained as an explicit option
The implementation is seq_rewriter::light_ant_derivative_cofactors.
Correctness
-----------
The seq_monadic unit tests run in both modes. They cover character and
generic
element sequences, multiple and repeated variables, variable
constraints,
bounded loops, conjunctions of memberships, and witness construction. A
focused test checks the cofactor transformation above. The complete
94-test
unit suite used during evaluation passed. The benchmark harness is not
registered as a normal unit test; after detaching it, all 93 registered
tests
pass.
Benchmark evaluation
--------------------
The final optimized comparison used all 1,545 SMT2 files under
C:\git\bench\inputs\regexes. Each file was run in a separate process
with a
15-second timeout. There were 1,513 cases where both modes completed
without a
process failure or timeout.
Brzozowski Light-Ant
paired solver time 94.98 s 63.26 s
median solver time 1.734 ms 0.710 ms
derivative calls 5.70 M 3.39 M
cofactors 13.33 M 6.99 M
live states 2.74 M 0.44 M
product states 652.8 K 642.8 K
Light-Ant reduced paired solver time by 33.4%, derivative calls by
40.5%,
cofactors by 47.5%, and live states by 84.0%. It was faster on 1,091
cases;
Brzozowski was faster on 421 cases.
Light-Ant changed 131 Brzozowski undef results to sat. There were no
reverse
verdict changes and no mismatches against known sat/unsat statuses. Both
modes
had two timeouts. Process failures decreased from 30 to 27.
By corpus, paired solver time improved by 39.1% on ClemensRegex and by
11.9% on
MargusRegex.
Alternatives considered
-----------------------
Direct use of full Antimirov derivatives was also evaluated. It
introduced
large performance outliers, particularly around intersections, and
produced
additional undef results and timeouts. Disabling intersection-over-union
distribution improved some of these cases but remained slower and less
robust
than the light-weight transformation. The direct full-Ant mode was
therefore
removed from this change.
Copilot-Session: a2ce3573-4e15-4a4a-afb5-21e3cb04e4a2
## Summary
Adds `seq_monadic` (`src/ast/rewriter/seq_monadic.{h,cpp}`), a
self-contained,
rewriter-level decision procedure for regex membership of a term that is
a
concatenation of sequence variables and constant elements — e.g. `x·a·x
∈ R`,
including repeated and multiple variables. It uses a whole-language
*monadic
decomposition* plus automaton product-reachability; it is minterm-free
and does
**not** use Nielsen word-equation splitting or `seq_split`.
The component is **purely additive**: it is not wired into any solver
path, so
default behavior is unchanged. It ships with a unit test and an opt-in
benchmark
harness that is inert unless `Z3_SEQ_BENCH_DIR` is set.
## What it does
- `x·u ∈ R ⇔ ⋁_q ( x reaches q in A_R ∧ u ∈ q )` over the derivative
automaton; `reach(q)` is never materialized as a regex (avoids the
state-elimination blowup). A variable's constraint is decided by a lazy
product-reachability search over tuples of derivative states, with
transitions
= the product of `brz_derivative_cofactors` branches and
pairwise-conjoined
`seq::range_predicate` guards.
- **Generic in the element sort**: characters use the exact
`range_predicate`
algebra; any other element sort uses a candidate-basis over the element
values
the guards mention (sound and complete for the
`{true,false,=,<=,and,or,not}`
guard grammar the derivatives emit).
- **Concrete witnesses**: on sat it reconstructs a witness value (a
sequence of
concrete elements, not predicates) per variable from the accepting
product path.
- **Boolean combinations**: `solve_and` decides a conjunction of
memberships
jointly, so a variable shared across memberships is constrained
consistently.
This is the natural extension since `¬(t∈R) ≡ t∈~R`, `∨` = union of
DNFs, and
`∧` = product of DNFs.
Also de-duplicates the char-guard → `range_predicate` translator into a
single
public `seq::guard_to_range_predicate` in `seq_range_collapse` (it was
previously
duplicated there and in `seq_monadic`).
## Testing
- `tst_seq_monadic`: single / multiple / repeated variables, nested
complement,
bounded loops, per-variable constraints, a generic `(Seq Int)` section,
witness
verification (substitute the model back and re-decide membership), and
`solve_and` cases that are individually sat but jointly unsat.
- Full unit suite `test-z3 /a` passes (93/93).
## Evaluation (offline harness, not part of CI)
On a regex-membership benchmark corpus, restricted to files carrying a
genuine
`(set-info :status)`, the solver decides 318 and 316 are correct
(99.4%); the
only 2 disagreements are a length limitation (`|x|=2k`) that is outside
the
membership fragment.
## Known limitations / follow-ups
- Pathological deeply-nested, high-multiplicity regexes can overflow the
recursive derivative stack; a recursion-depth guard to degrade to
`unknown` is
a natural follow-up.
- Out-of-fragment constraints (word equations, length / Parikh) are not
handled,
by design — this decides regex membership only.
---------
Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
Co-authored-by: Nikolaj Bjorner <nikolaj@cs.stanford.edu>
Copilot-Session: 916db256-43c6-4067-b6f4-fa8d2cf2f37f
