mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-08-07 06:28:18 +00:00
Code Activity

seq_monadic_bench: encode modular length constraints as regex loops (#10402)

Browse source 
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
This commit is contained in:
Margus Veanes 2026-08-04 20:10:00 -07:00 • committed by GitHub
parent ae29ceb6a8
commit 4af3410d10
No known key found for this signature in database
GPG key ID: B5690EEEBB952194
1 changed files with 178 additions and 1 deletions
Download patch file Download diff file Expand all files Collapse all files

179
src/test/seq_monadic_bench.cpp
View file

@ -177,6 +177,179 @@ lbool run_file(
: tighten(t, n + s, INT64_MAX); // k <= |t|
};
// A length equation |t| = c*k + d, where k is an integer variable occurring in no
// other assertion than its own bounds, describes exactly the lengths congruent to d
// modulo c that those bounds allow -- that is, t in .{base}(.{c})*. seq_monadic has
// no integer reasoning, so without this rewrite both the equation and its guard are
// dropped and the benchmark measures a strictly weaker problem.
obj_map<expr, expr*> modular_re; // the equation -> regex encoding it
obj_map<expr, expr*> modular_term; // the equation -> the string term
obj_hashtable<expr> consumed; // guards fully accounted for by the encoding
{
ptr_vector<expr> conjuncts;
std::function<void(expr*)> flatten = [&](expr* e) {
if (m.is_and(e))
for (expr* arg : *to_app(e))
flatten(arg);
else
conjuncts.push_back(e);
};
for (expr* assertion : ctx.assertions())
flatten(assertion);
auto is_int_var = [&](expr* e) { return is_uninterp_const(e) && a.is_int(e); };
auto occurs = [&](expr* e, expr* k) {
obj_hashtable<expr> seen;
ptr_vector<expr> todo;
todo.push_back(e);
while (!todo.empty()) {
expr* t = todo.back();
todo.pop_back();
if (t == k)
return true;
if (!is_app(t) || seen.contains(t))
continue;
seen.insert(t);
for (expr* arg : *to_app(t))
todo.push_back(arg);
}
return false;
};
// c*k + d, with a single integer variable k and c > 0
auto parse_linear = [&](expr* e, expr*& k, rational& c, rational& d) {
k = nullptr;
c.reset();
d.reset();
ptr_vector<expr> todo;
todo.push_back(e);
rational v;
while (!todo.empty()) {
expr* t = todo.back();
todo.pop_back();
expr* x = nullptr, * y = nullptr;
if (a.is_add(t))
for (expr* arg : *to_app(t))
todo.push_back(arg);
else if (a.is_numeral(t, v))
d += v;
else if (a.is_mul(t, x, y) && a.is_numeral(x, v) && is_int_var(y)) {
if (k && k != y)
return false;
k = y, c += v;
}
else if (is_int_var(t)) {
if (k && k != t)
return false;
k = t, c += rational(1);
}
else
return false;
}
return k != nullptr && c.is_pos();
};
// k <= v / v <= k, including the strict and reversed spellings
auto parse_guard = [&](expr* e, expr*& k, bool& is_lower, rational& bound) {
expr* lhs = nullptr, * rhs = nullptr;
bool strict = false;
if (a.is_le(e, lhs, rhs)) {}
else if (a.is_lt(e, lhs, rhs)) strict = true;
else if (a.is_ge(e, rhs, lhs)) {}
else if (a.is_gt(e, rhs, lhs)) strict = true;
else return false;
rational v;
if (is_int_var(lhs) && a.is_numeral(rhs, v))
return k = lhs, is_lower = false, bound = strict ? v - 1 : v, true;
if (a.is_numeral(lhs, v) && is_int_var(rhs))
return k = rhs, is_lower = true, bound = strict ? v + 1 : v, true;
return false;
};
auto fits = [&](rational const& r) {
if (!r.is_int() || !r.is_int64())
return false;
int64_t v = r.get_int64();
return -(int64_t)MAX_LEN_BOUND <= v && v <= (int64_t)MAX_LEN_BOUND;
};
for (expr* eq : conjuncts) {
expr* lhs = nullptr, * rhs = nullptr, * t = nullptr, * k = nullptr;
rational c, d;
if (!m.is_eq(eq, lhs, rhs) || !a.is_int(lhs))
continue;
if (!(u.str.is_length(lhs, t) && parse_linear(rhs, k, c, d)) &&
!(u.str.is_length(rhs, t) && parse_linear(lhs, k, c, d)))
continue;
if (!is_seq_var(t) && !u.str.is_concat(t))
continue;
if (!fits(c) || !fits(d))
continue;
// Every other assertion mentioning k has to be a bound on k alone, otherwise
// eliminating k would lose information.
ptr_vector<expr> guards;
bool has_lo = false, has_hi = false, ok = true;
rational lo, hi;
for (expr* other : conjuncts) {
if (other == eq || !occurs(other, k))
continue;
expr* gk = nullptr;
bool is_lower = false;
rational bound;
if (!parse_guard(other, gk, is_lower, bound) || gk != k || !fits(bound)) {
ok = false;
break;
}
if (is_lower)
lo = has_lo ? std::max(lo, bound) : bound, has_lo = true;
else
hi = has_hi ? std::min(hi, bound) : bound, has_hi = true;
guards.push_back(other);
}
if (!ok)
continue;
int64_t ci = c.get_int64(), di = d.get_int64();
int64_t base = ((di % ci) + ci) % ci; // least non-negative length = d (mod c)
if (has_lo) {
// c*lo + d is congruent to base modulo c, so it is reached exactly.
int64_t lowest = ci * lo.get_int64() + di;
if (lowest > base)
base = lowest;
}
int64_t periods = -1; // -1: unbounded, i.e. a star
if (has_hi) {
int64_t highest = ci * hi.get_int64() + di;
if (highest < base)
continue; // empty; not worth encoding
periods = (highest - base) / ci;
}
if (base > MAX_LEN_BOUND || periods > MAX_LEN_BOUND)
continue;
sort* re_sort = u.re.mk_re(t->get_sort());
expr_ref all_char(u.re.mk_full_char(re_sort), m);
expr_ref period(u.re.mk_loop_proper(all_char, (unsigned)ci, (unsigned)ci), m);
expr_ref rep(m);
if (periods < 0)
rep = u.re.mk_star(period);
else
rep = u.re.mk_loop_proper(period, 0, (unsigned)periods);
expr_ref regex(rep, m);
if (base > 0) {
expr_ref prefix(u.re.mk_loop_proper(all_char, (unsigned)base, (unsigned)base), m);
regex = u.re.mk_concat(prefix, rep);
}
pin.push_back(regex);
modular_re.insert(eq, regex);
modular_term.insert(eq, t);
for (expr* g : guards)
consumed.insert(g);
}
}
// Collect what seq_monadic can model. Conjunctions are traversed so that an
// unsupported conjunct does not discard its siblings; every conjunct that cannot be
// modelled is counted in `dropped`. Dropping conjuncts only weakens the problem, so
@ -194,7 +367,11 @@ lbool run_file(
// benchmark faithful to what the solver actually sees.
bool negated = false;
expr* arg = nullptr;
if (m.is_not(e, arg) && u.str.is_in_re(arg, s, r))
if (consumed.contains(e))
return; // a guard the modular encoding folded in
if (modular_re.find(e, r))
modular_term.find(e, s);
else if (m.is_not(e, arg) && u.str.is_in_re(arg, s, r))
negated = true;
else if (!u.str.is_in_re(e, s, r)) {
if (!collect_len(e, false))