From 4af3410d104ad291437275ad1553d2b82b152727 Mon Sep 17 00:00:00 2001 From: Margus Veanes Date: Tue, 4 Aug 2026 20:10:00 -0700 Subject: [PATCH] seq_monadic_bench: encode modular length constraints as regex loops (#10402) MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit 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 --- src/test/seq_monadic_bench.cpp | 179 ++++++++++++++++++++++++++++++++- 1 file changed, 178 insertions(+), 1 deletion(-) diff --git a/src/test/seq_monadic_bench.cpp b/src/test/seq_monadic_bench.cpp index 25baa11525..1c28e81ec8 100644 --- a/src/test/seq_monadic_bench.cpp +++ b/src/test/seq_monadic_bench.cpp @@ -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 modular_re; // the equation -> regex encoding it + obj_map modular_term; // the equation -> the string term + obj_hashtable consumed; // guards fully accounted for by the encoding + { + ptr_vector conjuncts; + std::function 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 seen; + ptr_vector 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 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 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))