## Summary
Fixes a regression detected by the snapshot-regression corpus.
- Originating discussion:
https://github.com/Z3Prover/bench/discussions/3514
- Benchmark ref: `iss-2795/bug-1.smt2`
## Divergence
```diff
--- bug-1.expected.out (expected)
+++ produced (current z3)
@@ -1 +1,2 @@
+(error "line 3 column 23: invalid declaration, builtin symbol 'pi' has the same argument sorts")
unsat
```
The benchmark declares `(declare-fun pi () Real)`. The expected oracle
is `unsat`; current z3 instead errors out before solving.
## Root cause
Commit 2999517d5 (#10411, "Reject declarations that clash with built-in
signatures") added `cmd_context::builtin_signature_collides`, which
rejects any user declaration whose name resolves to a built-in
application. For **nullary** symbols there are no argument sorts to
distinguish an overload, so this also rejected declarations of
Z3-specific arithmetic *extension* constants such as `pi` and `euler`
(registered as `OP_PI` / `OP_E` in `arith_decl_plugin`). These are not
SMT-LIB reserved symbols and were historically allowed to be shadowed by
user declarations, which is what `iss-2795/bug-1.smt2` relies on.
## Fix
In `builtin_signature_collides`, keep rejecting:
- any collision with `arity > 0` (real overload clash), and
- nullary symbols that resolve into the **basic** theory family (genuine
reserved core constants such as `true`/`false`).
Allow nullary symbols that resolve into non-core theory plugins (e.g.
`pi`, `euler`) to be shadowed. The change is confined to
`src/cmd_context/cmd_context.cpp`.
## Validation
Rebuilt z3 (`make -j8` from `scripts/mk_make.py`) and re-ran the
benchmark:
```
$ ./z3 -T:20 inputs/issues/iss-2795/bug-1.smt2
unsat
```
which now matches the recorded oracle. Also confirmed the intended
#10411 rejections still fire:
- `(declare-fun and (Bool Bool) Int)` -> rejected
- `(declare-const true Bool)` -> rejected
- `(define-fun + ((a Int)(b Int)) Int 0)` -> rejected
- `(declare-fun pi () Real)` / `(declare-fun euler () Real)` -> now
accepted
> [!WARNING]
> <details>
> <summary>Firewall blocked 1 domain</summary>
>
> The following domain was blocked by the firewall during workflow
execution:
>
> - `pypi.org`
>> To allow these domains, add them to the `network.allowed` list in
your workflow frontmatter:
>
> ```yaml
> network:
> allowed:
> - defaults
> - "pypi.org"
> ```
>
> See [Network
Configuration](https://github.github.com/gh-aw/reference/network/) for
more information.
>
> </details>
> Generated by [Fix a Z3 snapshot-regression
divergence](https://github.com/Z3Prover/bench/actions/runs/31074578887)
· 190.8 AIC · ⌖ 19.6 AIC · ⊞ 10.7K ·
[◷](https://github.com/search?q=repo%3AZ3Prover%2Fz3+%22gh-aw-workflow-id%3A+snapshot-regression-fixer%22&type=pullrequests)
<!-- gh-aw-agentic-workflow: Fix a Z3 snapshot-regression divergence,
engine: copilot, version: 1.0.65, model: claude-opus-4.8, id:
31074578887, workflow_id: snapshot-regression-fixer, run:
https://github.com/Z3Prover/bench/actions/runs/31074578887 -->
<!-- gh-aw-workflow-id: snapshot-regression-fixer -->
<!-- gh-aw-workflow-call-id: Z3Prover/bench/snapshot-regression-fixer
-->
Co-authored-by: z3prover-ci-bot[bot] <305651407+z3prover-ci-bot[bot]@users.noreply.github.com>
Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
## Problem
`optsmt::geometric_lex` terminates the search when `maximize_objective`
returns the same blocker twice:
```cpp
if (bound == last_bound)
break;
```
That fixed-point test is unreliable for a **delta-rational optimum** `r
+ k*delta` with `k > 0`. `theory_lra::mk_ge` builds the blocker from the
*rational part and a strictness flag only*:
```cpp
rational r = val.get_rational();
bool is_strict = val.get_infinitesimal().is_pos();
...
b = a.mk_le(mk_obj(v), a.mk_numeral(r, is_int)); // k is discarded
```
So two consecutive stalled rounds at `r + k1*delta` and `r + k2*delta`
produce the *identical* literal, the loop breaks, and the stalled value
is reported as the optimum.
Such a value is not a proven optimum — it only records that the
arithmetic solver could not move off the bound it was just given.
## Symptom
```smt2
(declare-const a Real)
(declare-const b Real)
(assert (xor (= 0.0 b) (> (mod (to_int (- a)) 50) 3)))
(minimize a)
(check-sat)
(get-objectives)
```
`a` is unbounded below — `b = 0` with `a = -50k` satisfies the
constraint for every `k`. But master reports a finite value whenever the
integer cut/cube heuristics run less often than the default period:
```
$ z3 lp.int_hammer_period=64 small.smt2
sat
(objectives
(a (+ (/ 1.0 4.0) (* (- 1.0) epsilon)))) ; wrong, should be -oo
```
## Change
When the blocker has collapsed and the objective carries a *positive*
infinitesimal, force a strictly larger rational step instead of giving
up. If that step is infeasible the loop still terminates normally
through the `l_false` branch with the best proven bound, so the change
cannot weaken a genuine optimum.
## Validation
- **Unit tests**: 94/94 pass.
- **New regression coverage**: `tst_scaled_min` now also runs at
`lp.int_hammer_period` 16/32/64/128. It **fails on master** (`infinity
coeff: 0` — a finite value for an unbounded objective) and **passes with
this change**.
- **Differential testing** against master on randomly generated
optimization benchmarks (`-T:10`, no crashes anywhere):
| corpus | files | diffs | crashes |
|---|---|---|---|
| linear, `int_hammer_period=4` | 3000 | 0 | 0 |
| linear, `int_hammer_period=64` | 3000 | 0 | 0 |
| nonlinear / `mod` / `to_int` / box+lex+pareto | 490 | 5 | 0 |
All 5 differences were checked against an independent satisfiability
oracle, and **master is wrong in every one**:
| case | master | this PR | oracle |
|---|---|---|---|
| `maximize (* -5.0 x0)` | `5 + 5ε` | `25` | `= 25` sat, `> 25` unsat →
**25 is optimal** |
| `minimize (+ (* -3.0 x0) (* 3.0 x1))` | `237/5 - ε` | `-oo` | `<
-1000000` sat → **unbounded** |
| `minimize (+ (* -5.0 x2) ...)`, box | `290 - 5ε` | `321/2` | `< 170`
sat → master's value unreachable |
| `minimize (* 5.0 x1)` | `495/4 - 5ε` | `487/4 - 5ε` | `<= 487/4` sat →
strictly better |
| `minimize (+ (* -1.0 x3) (* 4.0 x3) (* 4.0 x2))` | `-4ε` | `-36` | `=
-36` sat, `< -36` unsat → **-36 is optimal** |
Three become exactly optimal and two strictly closer to the true
optimum; no case regressed.
## Note
This addresses the `optsmt` side of the fixed-point test. The underlying
cause — `theory_lra::mk_ge` dropping the infinitesimal coefficient `k`
when building a blocker — is the same root issue that #10269 addresses
in the LRA path, and a complete fix there would make this guard
redundant rather than conflict with it.
Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
Fixes#10375.
## Analysis of [run
30786942559](https://github.com/Z3Prover/z3/actions/runs/30786942559)
The job is green, but `make test` exited 2. Every failing test is an
**expected-output mismatch**, and all 70 of them differ only by the
`--proof_recovery` banner:
```
- The SMT solver could not prove the query.
+ - This query was retried due to the --proof_recovery option, yet it still
+ failed on all attempts.
```
That text comes from `--proof_recovery` in the workflow's own
`fstar_otherflags` default, which F*'s `.expected` files do not carry —
so these are configuration mismatches, not Z3 regressions. There are
also failures that never reach the solver (`hello.__all`, `dune`,
extraction diffs on `RemoveUnusedTypars_B.fs` / `Bug3865.out`).
None of that was reconstructible from the artifact: the run uploaded 526
`.smt2` files, almost all logged failing queries from negative tests
that are *supposed* to fail, and nothing else. No logs, no produced
output, no `.expected` oracle, no diff.
## Changes
* **`Resolve FStar options`** — computes `OTHERFLAGS` once (removing the
duplicated `--z3version` extraction) and enforces
`--log_failing_queries`. Scheduled runs get no `workflow_dispatch`
inputs, so the options that make F* emit `.smt2` files are hard-wired
instead of assumed to come from the inputs. The effective flags are
recorded in the artifact, the job summary and the discussion.
* **`Build FStar`** now tees to a log, as the test step already did.
* **`Collect FStar failure artifacts`** replaces `Collect generated SMT2
files` and produces:
* `logs/` — build log, test log, versions, commit, effective flags, and
a `failing-tests.txt` summary of mismatched outputs plus failed make
targets;
* `smt2/` — the logged failing queries, as before;
* `test-output/` — for every expected-output test whose result differs
from its oracle: `<name>.actual`, `<name>.expected` and a unified
`<name>.diff`.
* **Upload always runs.** Previously, if no `.smt2` file existed the
collect step short-circuited and the upload was skipped, so the hardest
failures produced no artifact at all.
* The failure summary is surfaced in the **job summary** and in the
**discussion**, so a mismatch is visible without downloading anything.
Applied to the run above, `test-output/` would hold the
actual/expected/diff triple for each of the 70 mismatches and
`failing-tests.txt` would list them alongside `hello.__all` and the
other non-SMT failures.
## Validation
The workflow parses as YAML; every `run:` block passes `bash -n` and the
`github-script` body passes `node --check`. The new steps were executed
locally against a fixture reproducing the run's failure shapes:
* mismatched `.output` / `.json_output` / `.ideout` / `.fs` / `.out`
files are collected with correct diffs; the generated diff for
`Basic.fst.output` reproduces the annotation in the run exactly;
* matching outputs, `_output` files with no `.expected`, and files over
4 MB are correctly skipped;
* failed make targets are parsed from both logs;
* with no F* tree at all (build failed before clone) the collector still
exits 0 and the artifact still contains the logs;
* option resolution was checked with the default flags, with
`--log_failing_queries` absent, with empty flags, and with an
unparseable `z3 --version`;
* the rendered discussion body is 53 040 characters in the worst case,
below GitHub's 65 536 limit.
Behaviour deliberately unchanged: the build and test steps keep
`continue-on-error`, so a broken F* master still does not block the
report.
Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
Follow-up to #10399, which promised this as the next step in making the
harness measure the
problem the benchmark actually states.
> Stacked on #10401 (a one-line build fix), so that CI is green. Once
#10401 merges this PR
> reduces to the single `seq_monadic_bench.cpp` commit.
## What
A length equation
```smt2
(assert (= (str.len x) (+ (* 2 k) 1)))
(assert (>= k 0))
```
whose integer variable `k` occurs nowhere else says exactly that `|x|`
is odd — a *regular*
property. In general `|t| = c*k + d` with `lo <= k` is
```
t ∈ .{base}(.{c})*
```
where `base` is the least admissible length congruent to `d` modulo `c`.
A two-sided guard
`lo <= k <= hi` gives the bounded form `.{base}(.{c}){0,periods}`.
`seq_monadic` has no integer reasoning, so previously both the equation
and its guard were
dropped. Dropping *weakens* the problem, so `unsat` still transferred to
the original
benchmark but `sat` did not — on these files the harness was reporting
an answer to a
question nobody asked.
The rewrite fires only when every other conjunct mentioning `k` is a
bound on `k` alone.
Otherwise `k` is load-bearing elsewhere and eliminating it would lose
information. This is
why `hard_len_nonprim_2_cyclic_phase_shift.smt2`, whose equation is
`(= (+ (str.len x) (str.len y)) (+ (* 3 k) 1))`, is correctly left alone
— its left-hand
side couples two variables and is genuinely relational.
## Effect on the regex corpus
1476 files, light-ant mode, 20s budget. Decided count is unchanged at
1396.
| | before | after |
|---|---|---|
| complete | 1411 | **1416** |
| files with drops | 63 | **58** |
| dropped assertions | 107 | **93** |
| MargusRegex complete | 297/298 | **298/298** |
Four files change verdict, all `sat -> unsat`, which is the expected
direction — the problem
is no longer weakened. Each agrees with the answer its own header
documents:
| file | before | after | header says |
|---|---|---|---|
| `MargusRegex/levels/L2-04-alt-even-unsat.smt2` | sat *(wrong)* |
**unsat**, 0.33 ms | `Status unsat is authoritative` |
| `hard_len_nonprim_5_odd_even_boundary_clash.smt2` | sat | **unsat**,
0.17 ms | "The CEGAR length abstraction … declares SAT!" (i.e. that is
the trap) |
| `hard_len_nonprim_6_cegar_interleaved.smt2` | sat | **unsat** |
"fundamentally UNSAT" |
| `hard_length_2_cegar_gradient.smt2` | sat | **unsat**, 0.24 ms | — |
`L2-04-alt-even-unsat.smt2` is the interesting one: it was the *only*
file in the corpus
where the harness contradicted an authoritative status annotation.
Default z3 does not
decide it in 30s.
`hard_len_nonprim_6` remains incomplete — it also carries relational
length constraints
(`|x| = |z| + 2`, `|y| = |z| + 1`) which are out of monadic scope — but
its modular
constraint is now modelled, and `unsat` on a weakened problem still
transfers.
## Validation
- **Encoding correctness.** For each `(c, d, lo, hi)` the two length
sets
`{c·k + d : lo ≤ k (≤ hi)}` and `{base + c·j : 0 ≤ j (≤ periods)}` were
compared over
`n ≥ 0` by asking z3 to refute their equivalence. **4368 combinations**
covering
`c ∈ 1..13`, `d ∈ 0..13`, `lo ∈ -2..3`, and both the unbounded and
bounded forms — all
`unsat`, i.e. all equivalent.
- 94/94 unit tests.
- Identical results in `light-ant` and `brz` modes.
- No verdict change anywhere outside the four files above.
Remaining drops after this change are word equations (86 across 52
files) and relational
length constraints (8 across 6 files), both genuinely outside monadic
scope.
---------
Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
Copilot-Session: a2ce3573-4e15-4a4a-afb5-21e3cb04e4a2
`master` currently does not compile.
The merged version of #10398 replaced the plain loop in
`seq_regex::all_true` with
```cpp
return all_of(lits, [&ctx](literal lit) { return l_true == ctx.get_assignment(lit); });
```
`ctx` is a **data member** of `seq_regex` (`seq_regex.cpp:31`), not a
variable with automatic
storage duration, so naming it in a lambda capture list is ill-formed.
All three major
compilers reject it:
- MSVC: `error C2065: 'ctx': undeclared identifier`
- GCC: `error: capture of non-variable 'smt::seq_regex::ctx'`
- Clang: `error: 'ctx' in capture list does not name a variable`
This changes the capture to `this`, which is what the body actually
needs in order to reach
`ctx`. The predicate itself is untouched, so there is no behavioural
change.
Verified: `z3.exe` builds cleanly, and
`inputs/issues/iss-9928/instance14703.smt2` — the
original soundness reproducer from #10398 — still answers `sat`.
Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
Copilot-Session: a2ce3573-4e15-4a4a-afb5-21e3cb04e4a2
The benchmark harness in `seq_monadic_bench` only recognized positive
`(str.in_re t R)` assertions. Everything else it could not model was
dropped, counted in `dropped`, and cleared the `complete` flag.
A negated membership `(not (str.in_re t R))` is just a membership in the
complement. `seq_monadic` handles `re.comp` natively, and
`seq_regex::unfold_complement` performs exactly this rewrite on the
production path, so dropping it made the benchmark measure a strictly
weaker problem than the solver actually sees. Length constraints already
handled negation through `collect_len`'s `sign` parameter; this closes
the same gap for memberships.
### Effect
Full regex corpus (1476 files, `light-ant` mode, 20s timeout):
| metric | before | after |
|---|---|---|
| decided | 1396 | 1396 |
| **complete (all assertions modelled)** | 1384 | **1411** |
| files with dropped assertions | 90 | 63 |
| dropped assertions | 134 | 107 |
| sum of solve times | 181.3s | 165.6s |
No verdict changes on any of the 1476 files, and no measurable cost.
27 files that previously reported an unfaithful, weakened problem are
now
modelled exactly.
### What is still dropped
For reference, the remaining 107 drops across 63 files are:
| category | drops | files | example |
|---|---|---|---|
| word equations | 86 | 52 | `(= (str.++ x y) (str.++ y x))` |
| integer-variable guards | 8 | 7 | `(>= k 0)` |
| relational length | 8 | 6 | `(= (str.len x) (+ (str.len y) 1))` |
| modular length | 7 | 6 | `(= (str.len x) (* 2 k))` |
Word equations are genuinely outside a monadic decomposition and are
expected to stay dropped. The modular-length group is monadic in
disguise -- `|x| = 2k ∧ k >= 0` is exactly `x in (..)*` -- and encoding
it
as a regex loop would make 5 further files complete. That is left for a
follow-up.
Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
Copilot-Session: a2ce3573-4e15-4a4a-afb5-21e3cb04e4a2
Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
Copilot-Session: a2ce3573-4e15-4a4a-afb5-21e3cb04e4a2
Fixes a soundness bug in the monadic regex solver: it can answer `unsat`
on satisfiable inputs.
Reproducer (annotated `sat`, answered `unsat`):
```
z3 smt.seq.regex_monadic=true QF_S/20230329-automatark-lu/instance14703.smt2
```
The bug is latent on master and is exercised by #10381, which changes
the
search path enough to hit it. It reproduces on master as soon as the
search reaches the same state, so it is fixed here independently of that
stack.
### Root cause
`seq_regex::add_monadic_bounds` asks the arithmetic solver for the bound
it currently derives for `str.len s` and records it as a dependency of
the monadic solver:
```cpp
bool has_lo = th.lower_bound(len, lo) && ...
```
`theory_seq::lower_bound` goes to `arith_value::get_lo`, which reports
the bound the tableau has derived. That bound is justified by whatever
combination of literals the tableau used -- it is *not* justified by the
single atom `len >= lo`.
When such a dependency turns up in an unsat core, `add_core_literal`
fabricates that atom after the fact:
```cpp
lits.push_back(th.m_ax.mk_ge(b.m_len, b.m_value));
```
and the result is handed to `th.set_conflict(nullptr, lits)`.
`theory_seq::set_conflict` builds an
`ext_theory_conflict_justification`,
which requires every antecedent to be assigned true.
`conflict_resolution::process_antecedent` skips an antecedent whose
assign level is not above the base level and never checks its truth
value, so a literal that is *false* is silently dropped from resolution.
The clause that actually gets learned is then strictly stronger than the
valid clause the monadic solver proved.
On the reproducer, at scope 186 `lower_bound(str.len X)` returns 12
while
the atom `(>= (str.len X) 12)` is assigned **false**, so the valid
clause
```
~(X in R1) | ~(X in R2) | ~(|X| >= 12)
```
degenerates to the invalid
```
~(X in R1) | ~(X in R2)
```
which is what produces the wrong `unsat`. 4 of the 15 monadic cores on
this instance contain such a literal.
### Fix
The clause is always valid -- the monadic solver did prove the
conjunction unsat -- it is just not currently *falsified*, so it cannot
be presented as a conflict. So check whether the core is a legitimate
conflict, and if it is not, assert the clause as a theory axiom instead
and hand the memberships to the legacy regex solver.
The fallback is what guarantees progress: the axiom is already satisfied
by the non-true literal's negation, so without it the next `final_check`
would rederive the identical core forever. This reuses the existing
`enable_legacy_fallback()` escape hatch already used for `l_undef`; it
is
backtrackable (`value_trail`) and is re-enabled when a new membership
arrives, so no completeness is lost.
`arith_value` exposes no justification-returning bound API, so recording
the justifying literal up front is not currently an option; the derived
bound remains useful for pruning, it just cannot be replayed as an
antecedent.
### Validation
`test-z3 /a`: 94/94 pass.
A/B over QF_S with `smt.seq.regex_monadic=true model_validate=true`,
5s timeout, comparing this fix against the same build without it:
| family | files | decided before | decided after | unsound before |
unsound after |
|---|---|---|---|---|---|
| `20230329-automatark-lu` (sampled) | 5332 | 5258 | 5250 | **1** |
**0** |
| `2019-Jiang/slog` (sampled) | 988 | 937 | 937 | 0 | 0 |
| `20250411-hornstr-equiv` | 552 | 543 | 543 | 0 | 0 |
| `20250410-matching` | 230 | 84 | 84 | 0 | 0 |
| `20250411-negated-predicates` | 450 | 0 | 0 | 0 | 0 |
Every verdict is identical outside automatark-lu. Within automatark-lu
the only semantic change is the fixed instance; the 8 remaining
differences are load-induced timeouts at the 5s boundary (all had
pre-fix times of 4.7-5.2s) and all 9 solve identically on both builds
when rerun at 20s without contention. Total wall time improved in every
family.
### Note for review
Worth a second opinion: it is not obvious *why*
`theory_arith::get_lower`
reports 12 while the atom `(>= (str.len X) 12)` is assigned false at the
same scope. Either the derived bound was never propagated to that atom,
or it belongs to a different enode in the same equivalence class. It
does
not affect this fix -- the literal is fabricated either way -- but it
may
point at a second issue on the arithmetic side.
---------
Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
Co-authored-by: Nikolaj Bjorner <nikolaj@cs.stanford.edu>
Copilot-Session: a2ce3573-4e15-4a4a-afb5-21e3cb04e4a2
The nightly release failed because the default `GITHUB_TOKEN` is a
GitHub Actions App installation token without permission to create a tag
that includes workflow changes.
- Mint a short-lived installation token for `z3prover-ci-bot`.
- Request only `contents: write` and `workflows: write`.
- Use the App token for checkout credentials, tag deletion/push, and
release deletion/creation.
- Do not use `GH_AW_GITHUB_TOKEN`, a PAT, or another classic token.
Repository setup:
- `Z3_CI_APP_CLIENT_ID` is configured on `Z3Prover/z3`.
- Add `Z3_CI_APP_PRIVATE_KEY` as an Actions repository secret.
- Grant `z3prover-ci-bot` **Workflows: Read and write**, then approve
the updated installation permissions for the Z3Prover organization.
---------
Co-authored-by: copilot-swe-agent[bot] <198982749+Copilot@users.noreply.github.com>
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
Co-authored-by: Lev Nachmanson <levnach@hotmail.com>
Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
`re.loop` has two accepted AST forms: bounds as decl parameters, `((_
re.loop lo hi) r)` (1 argument, 2 parameters), and bounds as arguments,
`(re.loop r lo hi)` (3 arguments, 0 parameters). The plugin accepts
arities 1, 2 and 3, and `is_loop` has separate overloads for each form.
Only the parameter form was recognized downstream.
### The soundness bug
`mk_info_rec`'s `OP_RE_LOOP` case read the bounds solely from
`get_decl()->get_num_parameters()`, which is 0 for the argument form, so
it silently fell back to the locals `lower_bound = 0, upper_bound =
UINT_MAX`. `info::loop` computes
```cpp
loop_nullable = (nullable == l_true || lower == 0) ? l_true : nullable;
```
so `lower == 0` forces nullability, and `min_length` collapses to
`min_length * 0 = 0`.
Net effect: `(re.loop (str.to_re "ab") 1 3)` was reported as `nullable =
l_true, min_length = 0`. At the SMT level
```smt2
(declare-const x String)
(assert (str.in_re x (re.loop (str.to_re "ab") 1 3)))
(assert (= (str.len x) 0))
(check-sat)
```
answered **sat** rather than unsat. The indexed form of the same regex
correctly answers unsat.
`seq_rewriter::mk_re_loop` already normalizes the argument form to
`mk_loop_proper`, which is why this was never observable on the usual
paths — it only surfaces where the rewriter is bypassed, as in
`seq_monadic`. The `info.nullable` fast path added in #10366 didn't
create the bug but widened the path that reaches it.
### The performance bug
`derive_core` had no case for the argument form either, so the
derivative got stuck as an uninterpreted `re.derivative` term.
Instrumenting all three sites that can emit a symbolic `re.derivative`
showed that **every one of the 4171 stuck terms** in the regex corpus
came from this fall-through (the 512-deep recursion cap and the
unnormalizable `re.reverse` site never fired), and 4096 of them came
from a single legacy-form loop, whose search then burned its full budget
before giving up.
### The fix
* `mk_info_rec` branches on `get_num_args()`; for the argument form it
reads the bounds from `get_arg(1)`/`get_arg(2)` when they are unsigned
numerals, and returns `unknown_info` when they are not.
* `derive_core` normalizes the numeral argument forms to
`mk_loop_proper`/`mk_loop` and recurses. The block is gated on the cheap
`re().is_loop(r)` kind check so that regexes falling through to the
later cases don't pay for the `rational` locals.
Arguably the right long-term place to normalize is the parser, so the
legacy form never reaches the AST at all. Keeping the `mk_info_rec` half
is still worthwhile as a guard for API-constructed terms, and the
regression test builds the term directly via `mk_app`, so it stays
meaningful either way.
### Regression test
`src/test/seq_rewriter.cpp` gains a case asserting that `get_info`
agrees on the two forms (`nullable == l_false`, `min_length == 2`).
Verified to actually catch the bug: reverting `seq_decl_plugin.cpp` and
rebuilding gives `ASSERTION VIOLATION` with `nullable=l_true
min_length=0`.
### Evaluation
Full run over 1545 regex benchmarks with declared statuses, in both
transition modes:
| | light-ant | brz |
|---|---|---|
| decided (before → after) | 1462 → **1463** | 1464 → **1465** |
| soundness mismatches | 0 → 0 | 0 → 0 |
| verdict changes | 1 | 1 (same file) |
The one changed file is `L4-01-loop-sat.smt2`: **undef @ 8625 ms → sat @
0.20 ms**. The corpus contains 1 legacy-form file and 236 indexed-form
files, which share the modified `OP_RE_LOOP` path, hence the full A/B
rather than a spot check.
Timing is neutral. Measured with an interleaved base/fix/base/fix
protocol over two saved binaries, since same-binary run-to-run variance
(±8%) turned out to exceed the effect: paired best-of-2 over the 315
files taking >1 ms gives a **median ratio of 0.998** (p25/p75 =
0.889/1.075), overall 0.976.
`tst_seq_rewriter` passes, `seq_monadic` is ALL PASS in both modes, and
the 22172-file QF_S corpus shows no verdict changes and no mismatches.
Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
Co-authored-by: Nikolaj Bjorner <nikolaj@cs.stanford.edu>
Copilot-Session: a2ce3573-4e15-4a4a-afb5-21e3cb04e4a2
Follow-up cleanup requested in review of the seq_monadic work. Based
directly on master, independent of #10370.
`light_ant_derivative_cofactors` was implemented in `seq_rewriter`, even
though it is purely a derivative operation: it post-processes the output
of `derive::derivative_cofactors` and uses no rewriter state beyond the
shared `bool_rewriter`. The two sibling entry points, `get_cofactors`
and `brz_derivative_cofactors`, were already thin forwarders into
`seq::derive`, so this one was the odd one out.
### Change
The body moves to `seq::derive`, next to `get_cofactors` and
`derivative_cofactors`, so all three cofactor entry points live in one
place. `seq_rewriter` keeps `light_ant_derivative_cofactors` as an
inline forwarder in the header, matching how the other two are exposed —
no caller changes anywhere (`seq_monadic`, `smt/seq_regex`,
`seq_range_collapse`, `seq_regex_bisim`, and the unit tests all keep
calling it through the rewriter).
| file | |
|---|---|
| `seq_derive.h` | declaration + doc comment |
| `seq_derive.cpp` | +61, the body |
| `seq_rewriter.cpp` | −61, the body |
| `seq_rewriter.h` | forwarder becomes inline, like its two siblings |
The one non-mechanical detail: the splitting step builds its
concatenation with `seq_rewriter::mk_regex_concat`, which stays in the
rewriter because other rewriter code uses it. `derive` already holds the
`m_re` back-reference and calls through it for `mk_inter`, `mk_xor0` and
`is_subset`, so the moved code does the same rather than duplicating the
constructor. The terms produced are identical.
### Verification
Pure refactoring, so this was checked for exact equivalence rather than
for improvement.
* **0 verdict differences** against master over 1545 regex benchmarks,
in light-ant (the mode that exercises this path) and in brz. Decided
counts unchanged at 1462 / 1464.
* `seq_monadic` ALL PASS in both transition modes; `seq_rewriter`,
`seq_regex_bisim` and `regex_range_collapse` all pass.
Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
Copilot-Session: a2ce3573-4e15-4a4a-afb5-21e3cb04e4a2
## Summary
Two related changes:
1. Rewrite `(Σ*·S)*` to the flat form `() | Σ*·S` in
`seq_rewriter::mk_re_star`.
2. Make `seq_monadic_bench` normalize its inputs, so that rewriter-level
changes are
observable at all.
## The rewrite
`Σ*·S` is idempotent under concatenation. Any word of `(Σ*·S)·(Σ*·S)`
factors as
`(Σ*·S·Σ*)·S`, and the leading `Σ*·S·Σ*` is absorbed by `Σ*`, so the
word is again in
`Σ*·S`. Hence `L·L ⊆ L`, and therefore `L* = () | L`.
This is the same absorption argument the subset checker already
implements — see the
"prefix absorption" rule `P·R' ⊆ Σ*·R'` in `seq_subset.cpp`. It was
simply never applied
to the star.
The two forms denote the same language but are not equally cheap to
determinize. Under
the star, every residual carries a trailing `(Σ*·S)*` factor, so the
derivative automaton
keeps a separate copy of the `S`-tracking states for each unfolding. The
flat form drops
that factor and the copies collapse.
Measured live-state counts of the derivative automaton:
| regex | star form | flat form |
|---|---|---|
| `nonA ∩ (Σ*·b·Σ^5)*` | 904 | **65** |
| `core ∩ (Σ*·b·Σ^5)*` | 1807 | **129** |
roughly a 14x reduction.
The shape is not exotic: it is what a "contains" pattern under a star
looks like, and it
occurs in 27 of the 1545 regex benchmarks I track.
## The bench change
`seq_monadic_bench` handed `seq_monadic` the raw parsed regex, whereas
in the solver
`seq_regex` only ever sees terms that `asserted_formulas` has already
rewritten. The
bench therefore could not observe a rewriter-level change at all — the
rewrite above
measured as *exactly zero* difference across all 1545 benchmarks in both
modes until the
bench was made to normalize.
Each `str.in_re` regex argument now goes through `th_rewriter` before
reaching
`seq_monadic`, placed ahead of the multi-membership merge so that
`mk_regex_inter_normalize` also receives normalized operands.
This is closer to production but not identical to it:
`asserted_formulas` rewrites whole
assertions and can propagate across them, while this rewrites each
membership's regex in
isolation.
## Measurements
Combined effect over 1545 regex benchmarks, against master:
| mode | decided | gained | lost | mismatches | status conflicts |
|---|---|---|---|---|---|
| light-ant | 1464 → **1467** | 4 | 1 | 0 | 0 |
| brz | 1466 → **1469** | 4 | 1 | 0 | 0 |
Gained in both modes:
- `MargusRegex/levels/L4-01-loop-sat`
- `ClemensRegex/generated/split_membership_medium_sat_0012`
- `ClemensRegex/generated/split_membership_medium_sat_0000`
- `ClemensRegex/generated_easy/split_membership_easy_unsat_0009`
The single loss per mode comes from the normalization, not the rewrite,
and is marginal in
both cases: `easy_unsat_0006` (light-ant) took 5.5 s and
`medium_sat_0036` (brz) took
3.9 s on master, and both now trip a cap slightly earlier. Each is
mode-specific —
`easy_unsat_0006` is still decided in `brz`, and `medium_sat_0036` was
already undecided in
`light-ant` on master.
Runtime, paired best-of-2 over two interleaved rounds:
| | outside `ClemensRegex/generated` | `ClemensRegex/generated` |
|---|---|---|
| light-ant | +2.2% | +12.0% |
| brz | −0.2% | +11.3% |
Outside the `generated` family this is inside the ±8% run-to-run noise
of the measurement
machine. Within that family the increase is expected and is what buys
the extra
decisions: those files previously tripped the `state_cap` bail early,
and with the smaller
automaton the search gets further before exhausting the budget. The cost
stays bounded by
the existing budget.
The rule fires only on the `Σ*·S` shape:
```
(simplify (re.* (re.++ re.all (str.to_re "b"))))
→ (re.union (re.++ re.all (str.to_re "b")) (str.to_re ""))
(simplify (re.* (re.++ (str.to_re "a") (str.to_re "b"))))
→ (re.* (str.to_re "ab"))
```
## Tests
Adds case 22 to `src/test/seq_rewriter.cpp`: checks that `(Σ*·b)*` is no
longer a star
after rewriting, and pins the semantics with three solver queries —
`"ab"` and `""` are
members, `"ba"` is not.
`seq_rewriter`, `seq_monadic`, `seq_regex_bisim` and
`regex_range_collapse` all pass in
both `light-ant` and `brz` modes.
Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
Copilot-Session: a2ce3573-4e15-4a4a-afb5-21e3cb04e4a2
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
When smt.seq.regex_monadic is on, keep contains-style memberships
(s in .*P.*) as regex memberships routed to the monadic solver instead
of rewriting them into a word equation s = f1 ++ P ++ f2. The word
equation blows up theory_seq on long concatenations before final_check
(hence monadic) is ever reached.
Evaluated on 1476 regex benchmarks (10s timeout): solved 1160 -> 1341
vs legacy, +193 newly solved, 0 sat<->unsat soundness disagreements.
Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
Copilot-Session: 57b9b87e-950a-49ea-bbb3-ed585646a5a9
Follow-up to the feedback that `seq_monadic_bench` silently drops
non-membership
constraints and therefore reports results that don't correspond to the
benchmark
it claims to be solving. In particular the ipv6 benchmarks are guarded
by
`str.len` bounds, which the monadic solver *can* already express.
Test-only change (`src/test/`), no solver code touched.
## 1. Model length bounds via the existing API
`seq_monadic` already exposes `add_lo` / `add_hi` / `add_len`, which
encode
`t in Σ^lo Σ*`, `t in Σ^{0,hi}` and `t in Σ^{len,len}`. The harness now
extracts
constant length bounds from assertions and feeds them through:
- handles `<=`, `<`, `>=`, `>`, `=` in either argument order, under
arbitrary
`not` nesting;
- applies to any term the solver accepts (a variable, or a
concatenation), so
`(> (str.len x) 0)` alongside `(str.in_re (str.++ x y x) R)` works;
- intersects multiple bounds on the same term, and encodes an
unsatisfiable
bound (`|t| < 0`, or crossing bounds) as `lo=1, hi=0`;
- rejects rather than approximates anything not representable — an
out-of-range
constant, a relational bound `(= (str.len x) (str.len y))`, or a
semilinear
one `(= (str.len x) (* 2 k))` is counted as dropped, not silently
weakened.
`ipv6-exactly-one-cc-sat.smt2` now reports `complete=yes, dropped=0,
verdict=sat`,
matching its declared status.
## 2. Report incompleteness
Dropping conjuncts only weakens the problem, so on an incomplete
benchmark
`unsat` transfers to the original but `sat` says nothing. That was
previously
invisible. Now:
- a `dropped` column counts unmodellable **conjuncts** (not top-level
assertions), so it is a precise "how much of the benchmark is missing";
- single-file mode prints an `INCOMPLETE: ...` warning to stderr;
- the summary line gained `incomplete_sat=`, the count of results that
must not
be trusted;
- the file header documents the semantics.
`collect` also no longer short-circuits on the first unsupported
conjunct of an
`and`, which was discarding modellable siblings. On QF_S this alone
moves 456
files from `undef` to a decided verdict.
## 3. Unit tests
11 tests in a new *length bounds on compound terms* section of
`seq_monadic.cpp`: bounds on concatenations (`x.y.x`, `x.a.x`), several
bounded
variables under one membership, a case where the bound is the only cause
of
unsat, crossing `lo`/`hi`, and two ipv6-shaped tests reconstructing
`R = has_cc ∩ ¬two_cc ∩ hexcol`. All pass in both `brz` and `light-ant`.
## Validation
Both corpora, both transition modes, against master at c9a480cb3.
**regexes (1545 files):** complete 1448 → 1453. Two verdicts change,
both from
`sat` to `unsat` — these were previously *wrong*, caused by dropped
length
constraints; one of the two is declared `unsat` upstream. 0 crashes, 2
timeouts
(unchanged), 0 mismatches against declared status on complete benchmarks
in
either mode, and 0 disagreements between `brz` and `light-ant`.
**QF_S (22172 files):** 0 crashes, 0 timeouts. Of the 4089 files that
are both
complete and have a declared status, 0 mismatches. Of the 4366
incomplete files
that returned `unsat`, 4097 are declared `unsat` and **none** is
declared `sat`,
which is the invariant that matters for the weakening argument above.
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
- Fix angle-bracket include for expr_safe_replace.h to use quotes
(consistent with all other local includes in this file)
- Rewrite block_unfolding using early-return guard clauses instead of a
single boolean expression with a comma-operator side effect, which was
difficult to read and reason about
- Replace while (size() > 0) with idiomatic while (!empty()) in
mk_deriv_accept DFS loop
- Expand nested ternary chains in mk_deriv_accept into explicit if/else
chains for readability (ite-branch and union-branch cases)
No functional change.
Co-authored-by: github-actions[bot] <41898282+github-actions[bot]@users.noreply.github.com>
Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
Feed arithmetic length lower/upper/exact bounds (via theory_seq
lower_bound/upper_bound) into the monadic regex end-game solver using the
existing add_lo/add_hi/add_len helpers, so proposed witnesses respect length
constraints and length-driven cases resolve directly instead of backtracking
over the model.
Dependencies handed to the monadic solver now encode a union of sorts:
2*lit.index() for membership literals (even) and 2*bound_index+1 for length
bounds (odd). On unsat, the core is decoded back into conflict literals,
materializing the justifying arithmetic bound literals (len>=lo, len<=hi) at
that point. Bounds are recorded in m_monadic_bounds and undone via push_trail.
Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
Copilot-Session: 57b9b87e-950a-49ea-bbb3-ed585646a5a9
