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: model length bounds, report dropped assertions (#10365)

Browse source 
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
This commit is contained in:
Margus Veanes 2026-08-02 12:20:42 -07:00 • committed by GitHub
parent c9a480cb37
commit 11c969d31d
No known key found for this signature in database
GPG key ID: B5690EEEBB952194
2 changed files with 226 additions and 22 deletions
Download patch file Download diff file Expand all files Collapse all files

93
src/test/seq_monadic.cpp
View file

@ -511,6 +511,99 @@ public:
std::cout << (zero_lo_ok ? " OK " : " FAIL ")
<< "|x| >= 0 is a no-op\n";
// Length bounds on COMPOUND terms and on several variables at once: the shape the
// SMT-LIB regex benchmarks use (e.g. `x.y.x in R /\ |x|>0 /\ |y|>0`). A bound on
// a concatenation constrains the term as a whole; bounds on the individual
// variables have to be intersected with the split induced by the membership.
std::cout << "=== seq_monadic: length bounds on compound terms ===\n";
auto check_bounded = [&](char const* name,
auto&& assert_all, lbool expected) {
m_trail.push_scope();
assert_all();
lbool got = m_mon.check();
m_trail.pop_scope(1);
bool ok = got == expected;
if (!ok) ++m_fail;
std::cout << (ok ? " OK " : " FAIL ") << name
<< " got=" << s(got) << " expected=" << s(expected) << "\n";
};
expr_ref t_xyx(xyx(x, y), m);
expr_ref t_xax(xwx(x, "a"), m);
// |x.y.x| is odd-free: x.y.x in (ab)* with |x.y.x| = 2 forces x.y.x = "ab"
check_bounded("x.y.x in (ab)*, |x.y.x| = 2", [&] {
m_mon.add(t_xyx, abS, nullptr);
m_mon.add_len(t_xyx, 2, nullptr);
}, l_true);
check_bounded("x.y.x in (ab)*, |x.y.x| = 3", [&] {
m_mon.add(t_xyx, abS, nullptr);
m_mon.add_len(t_xyx, 3, nullptr); // (ab)* has only even lengths
}, l_false);
// bounds on the individual variables of a compound membership
check_bounded("x.a.x in Sigma*, |x| >= 2, |x.a.x| <= 5", [&] {
m_mon.add(t_xax, sig2, nullptr);
m_mon.add_lo(x, 2, nullptr);
m_mon.add_hi(t_xax, 5, nullptr);
}, l_true);
check_bounded("x.a.x in Sigma*, |x| >= 3, |x.a.x| <= 5", [&] {
m_mon.add(t_xax, sig2, nullptr);
m_mon.add_lo(x, 3, nullptr); // |x.a.x| = 2|x|+1 >= 7 > 5
m_mon.add_hi(t_xax, 5, nullptr);
}, l_false);
// two variables bounded independently under one membership
check_bounded("x.y.x in (a|b)*, |x| = 1, |y| = 2", [&] {
m_mon.add(t_xyx, abStar, nullptr);
m_mon.add_len(x, 1, nullptr);
m_mon.add_len(y, 2, nullptr);
}, l_true);
check_bounded("x.y.x in a*, |x| >= 1, y in b*", [&] {
m_mon.add(t_xyx, star(a), nullptr);
m_mon.add(y, star(b), nullptr); // y must be both a* and b* -> y = eps
m_mon.add_lo(x, 1, nullptr);
m_mon.add_lo(y, 1, nullptr); // ... but |y| >= 1
}, l_false);
// the bound is the ONLY reason for unsat: without it the membership is satisfiable
check_bounded("x in a(aa)* (no bound)", [&] {
m_mon.add(x, a_aaS, nullptr);
}, l_true);
check_bounded("x in a(aa)*, |x| = 2", [&] {
m_mon.add(x, a_aaS, nullptr); // only odd lengths
m_mon.add_len(x, 2, nullptr);
}, l_false);
// upper and lower bounds that cross
check_bounded("x in Sigma*, |x| >= 3, |x| <= 2", [&] {
m_mon.add(x, sig2, nullptr);
m_mon.add_lo(x, 3, nullptr);
m_mon.add_hi(x, 2, nullptr);
}, l_false);
// The IPv6 abbreviation benchmark shape: an intersection of a positive "contains"
// and a complement, restricted to a character range, over x.y.x with both
// variables non-empty. Without the length bounds the answer is trivially sat via
// x = y = epsilon, so the bounds are what make the test meaningful.
{
expr_ref cc(word("::"), m);
expr_ref sig_plus(cat(dot(), dotstar()), m);
expr_ref has_cc(cat(dotstar(), cat(cc, dotstar())), m);
expr_ref two_cc(cat(dotstar(), cat(cc, cat(sig_plus, cat(cc, dotstar())))), m);
expr_ref hexcol(star(alt(rng('0', '9'),
alt(rng('A', 'F'),
alt(rng('a', 'f'), word(":"))))), m);
expr_ref R6(inter(has_cc, inter(comp(two_cc), hexcol)), m);
check_bounded("ipv6: x.y.x in R, |x|>=1, |y|>=1", [&] {
m_mon.add(t_xyx, R6, nullptr);
m_mon.add_lo(x, 1, nullptr);
m_mon.add_lo(y, 1, nullptr);
}, l_true);
// "::" cannot be split across a repeated x without creating a second group,
// and hexcol forbids everything outside [0-9A-Fa-f:], so a long x is hopeless
check_bounded("ipv6: x.y.x in R, |x|>=1, |y|>=1, |x.y.x|<=2", [&] {
m_mon.add(t_xyx, R6, nullptr);
m_mon.add_lo(x, 1, nullptr);
m_mon.add_lo(y, 1, nullptr);
m_mon.add_hi(t_xyx, 2, nullptr); // needs >= 3 chars to hold "::" plus x twice
}, l_false);
}
std::cout << "=== seq_monadic: SMT regex end-game ===\n";
{
expr_ref_vector assertions(m);

155
src/test/seq_monadic_bench.cpp
View file

@ -8,14 +8,21 @@ Module Name:
Abstract:
Opt-in benchmark harness for seq_monadic. Reads every *.smt2 under
Z3_SEQ_BENCH_DIR, extracts regex memberships, and reports CSV timing.
Z3_SEQ_MONADIC_MODE selects "brz" or "light-ant" (default).
Z3_SEQ_BENCH_DIR, extracts regex memberships and length bounds, and reports
CSV timing. Z3_SEQ_MONADIC_MODE selects "brz" or "light-ant" (default).
Assertions the harness cannot hand to seq_monadic are DROPPED. The CSV
reports how many were dropped ("dropped") and whether the benchmark was
modelled in full ("complete"). On an incomplete benchmark only an `unsat`
verdict carries over to the original problem: dropping conjuncts weakens it,
so `sat` there says nothing about the benchmark's real status.
--*/
#define _CRT_SECURE_NO_WARNINGS
#include "ast/ast.h"
#include "ast/arith_decl_plugin.h"
#include "ast/seq_decl_plugin.h"
#include "ast/rewriter/seq_rewriter.h"
#include "ast/rewriter/seq_monadic.h"
@ -75,10 +82,12 @@ lbool run_file(
seq_monadic::transition_mode mode,
double& solve_ms,
bool& parsed,
bool& complete) {
bool& complete,
unsigned& dropped) {
solve_ms = 0;
parsed = false;
complete = false;
dropped = 0;
cmd_context ctx(false);
ctx.set_ignore_check(true);
{
@ -89,6 +98,7 @@ lbool run_file(
parsed = true;
ast_manager& m = ctx.m();
seq_util u(m);
arith_util a(m);
seq_rewriter rw(m);
trail_stack undo_trail;
seq_monadic mon(rw, undo_trail, mode);
@ -98,19 +108,94 @@ lbool run_file(
ptr_vector<expr> terms;
expr_ref_vector pin(m);
std::function<bool(expr*)> collect = [&](expr* a) {
// Length bounds accumulated per term; lo/hi are the tightest bounds seen.
struct len_bounds { unsigned lo = 0; unsigned hi = UINT_MAX; };
obj_map<expr, len_bounds> bounds;
ptr_vector<expr> bounded;
// seq_monadic models |t| <= hi as a bounded loop, so a huge hi is not usable.
const int64_t MAX_LEN_BOUND = 1 << 16;
const int64_t NO_UPPER = INT64_MAX;
auto tighten = [&](expr* t, int64_t lo, int64_t hi) {
if (!is_seq_var(t) && !u.str.is_concat(t))
return false;
if (lo > MAX_LEN_BOUND)
return false; // cannot build Sigma^lo
if (hi != NO_UPPER && hi > MAX_LEN_BOUND)
return false; // dropping it would be unsound
len_bounds b;
if (!bounds.find(t, b))
bounded.push_back(t);
if (lo > 0)
b.lo = std::max(b.lo, static_cast<unsigned>(lo));
if (hi < 0) // |t| < 0: record a contradiction
b.lo = std::max(b.lo, 1u), b.hi = 0;
else if (hi != NO_UPPER)
b.hi = std::min(b.hi, static_cast<unsigned>(hi));
bounds.insert(t, b);
return true;
};
// Recognize a linear length constraint (str.len t) <op> k (either argument
// order, optionally negated) and record it as a bound on t.
std::function<bool(expr*, bool)> collect_len = [&](expr* e, bool sign) {
expr* arg = nullptr;
if (m.is_not(e, arg))
return collect_len(arg, !sign);
// normalize to lhs <op> rhs with op in {<=, <, =}
expr* lhs = nullptr, * rhs = nullptr;
bool le = false, lt = false, eq = false;
if (a.is_le(e, lhs, rhs)) le = true;
else if (a.is_lt(e, lhs, rhs)) lt = true;
else if (a.is_ge(e, rhs, lhs)) le = true; // k >= |t| == |t| <= k
else if (a.is_gt(e, rhs, lhs)) lt = true;
else if (m.is_eq(e, lhs, rhs) && a.is_int(lhs)) eq = true;
else return false;
expr* t = nullptr;
rational k;
bool len_left; // true: |t| <op> k, else k <op> |t|
if (u.str.is_length(lhs, t) && a.is_numeral(rhs, k))
len_left = true;
else if (u.str.is_length(rhs, t) && a.is_numeral(lhs, k))
len_left = false;
else
return false;
if (!k.is_int() || !k.is_int64())
return false;
int64_t n = k.get_int64();
if (eq)
return !sign && tighten(t, n, n); // |t| != k is not a bound
int64_t s = lt ? 1 : 0; // strict?
if (len_left)
return sign ? tighten(t, n + 1 - s, INT64_MAX) // !(|t| <= k) == |t| >= k+1
: tighten(t, 0, n - s); // |t| <= k
return sign ? tighten(t, 0, n - 1 + s) // !(k <= |t|) == |t| <= k-1
: tighten(t, n + s, INT64_MAX); // k <= |t|
};
// 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
// an unsat verdict still transfers to the benchmark while a sat verdict does not.
std::function<void(expr*)> collect = [&](expr* e) {
expr* s = nullptr, * r = nullptr;
if (m.is_and(a)) {
for (expr* arg : *to_app(a))
if (!collect(arg))
return false;
return true;
if (m.is_and(e)) {
for (expr* arg : *to_app(e))
collect(arg);
return;
}
if (!u.str.is_in_re(e, s, r)) {
if (!collect_len(e, false))
complete = false, ++dropped;
return;
}
if (!u.str.is_in_re(a, s, r))
return false;
bool is_var = is_seq_var(s);
if (!is_var && !u.str.is_concat(s))
return false;
if (!is_var && !u.str.is_concat(s)) {
complete = false, ++dropped;
return;
}
obj_map<expr, expr*>& map = is_var ? var_re : term_re;
expr* previous = nullptr;
if (map.find(s, previous)) {
@ -123,11 +208,10 @@ lbool run_file(
if (!is_var)
terms.push_back(s);
}
return true;
};
complete = true;
for (expr* assertion : ctx.assertions())
complete = collect(assertion) && complete;
collect(assertion);
unsigned n_added = 0;
for (expr* term : terms) {
@ -140,6 +224,20 @@ lbool run_file(
mon.add(k, v, nullptr);
++n_added;
}
for (expr* t : bounded) {
len_bounds b;
bounds.find(t, b);
if (b.lo == b.hi)
mon.add_len(t, b.lo, nullptr);
else {
if (b.lo > 0)
mon.add_lo(t, b.lo, nullptr);
if (b.hi != UINT_MAX)
mon.add_hi(t, b.hi, nullptr);
}
if (b.lo > 0 || b.hi != UINT_MAX)
++n_added;
}
auto start = std::chrono::high_resolution_clock::now();
mon.set_gen_model(false); // benchmark only needs the verdict
@ -158,10 +256,12 @@ void display_row(
bool complete,
seq_monadic::transition_mode mode,
lbool verdict,
double solve_ms) {
double solve_ms,
unsigned dropped) {
std::cout << file << "," << tier << "," << status << ","
<< (complete ? "yes" : "no") << "," << mode_str(mode)
<< "," << verdict_str(verdict) << "," << solve_ms
<< "," << dropped
<< "\n";
}
@ -175,8 +275,12 @@ void tst_seq_monadic_bench() {
if (char const* file = getenv("Z3_SEQ_BENCH_FILE")) {
double ms = 0;
bool parsed = false, complete = false;
lbool verdict = run_file(file, mode, ms, parsed, complete);
display_row(file, "", read_status(file), complete, mode, verdict, ms);
unsigned dropped = 0;
lbool verdict = run_file(file, mode, ms, parsed, complete, dropped);
display_row(file, "", read_status(file), complete, mode, verdict, ms, dropped);
if (!complete)
std::cerr << "INCOMPLETE: " << dropped << " assertion(s) not modelled; "
<< "only an unsat verdict transfers to the benchmark\n";
return;
}
@ -197,8 +301,9 @@ void tst_seq_monadic_bench() {
files.push_back(entry.path().string());
std::sort(files.begin(), files.end());
std::cout << "file,tier,status,complete,mode,verdict,solve_ms\n";
std::cout << "file,tier,status,complete,mode,verdict,solve_ms,dropped\n";
unsigned agree = 0, mismatch = 0, undef = 0, unparsed = 0, incomplete = 0;
unsigned incomplete_sat = 0;
double total_ms = 0;
for (unsigned i = 0; i < files.size(); ++i) {
std::string const& file = files[i];
@ -209,11 +314,16 @@ void tst_seq_monadic_bench() {
<< relative << std::endl;
double ms = 0;
bool parsed = false, complete = false;
lbool verdict = run_file(file, mode, ms, parsed, complete);
display_row(relative, tier, status, complete, mode, verdict, ms);
unsigned dropped = 0;
lbool verdict = run_file(file, mode, ms, parsed, complete, dropped);
display_row(relative, tier, status, complete, mode, verdict, ms, dropped);
total_ms += ms;
if (!parsed) ++unparsed;
if (!complete) ++incomplete;
if (!complete) {
++incomplete;
// constraints were dropped, so a sat verdict does not transfer
if (verdict == l_true) ++incomplete_sat;
}
if (verdict == l_undef) ++undef;
else if (complete && (status == "sat" || status == "unsat")) {
if (status == verdict_str(verdict)) ++agree;
@ -227,5 +337,6 @@ void tst_seq_monadic_bench() {
<< " undef=" << undef
<< " unparsed=" << unparsed
<< " incomplete=" << incomplete
<< " incomplete_sat=" << incomplete_sat
<< " total_solve_ms=" << total_ms << "\n";
}