From 683cb4ec03bf1284cdccf2eb5352fbeb296e30ef Mon Sep 17 00:00:00 2001 From: Margus Veanes Date: Fri, 31 Jul 2026 10:34:34 -0700 Subject: [PATCH] seq_monadic: add light Antimirov cofactor mode (#10323) 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 --- src/ast/rewriter/seq_monadic.cpp | 13 +++++-- src/ast/rewriter/seq_monadic.h | 22 +++++++++-- src/ast/rewriter/seq_rewriter.cpp | 60 ++++++++++++++++++++++++++++++ src/ast/rewriter/seq_rewriter.h | 7 ++++ src/test/seq_monadic.cpp | 61 +++++++++++++++++++++++++++++-- 5 files changed, 152 insertions(+), 11 deletions(-) diff --git a/src/ast/rewriter/seq_monadic.cpp b/src/ast/rewriter/seq_monadic.cpp index f9ba950b07..3d9b11c014 100644 --- a/src/ast/rewriter/seq_monadic.cpp +++ b/src/ast/rewriter/seq_monadic.cpp @@ -22,8 +22,6 @@ TODOs: - track unsat cores and expose them as explain functionality - if perf suffers: use DFS backtracking search instead of DNF expansion (space overhead) - create a validation harness: expose certificates for correctness that can be checked. -- handle transitions into unions and concatenations over unions -- establish a perf harness - extend with lower and upper bound constraints - encapsulate within general interface: create: undo_trail x dependency_manager x ast_manager -> regex_membership @@ -229,6 +227,13 @@ expr_ref seq_monadic::der_elem(expr* r, expr* elem) { return d2; } +void seq_monadic::derivative_cofactors(expr* r, expr_ref_pair_vector& result) { + if (m_mode == transition_mode::light_antimirov) + m_rw.light_ant_derivative_cofactors(r, result); + else + m_rw.brz_derivative_cofactors(r, result); +} + void seq_monadic::live_states(expr* R, ptr_vector& out, bool& ok) { ok = true; obj_map id; @@ -251,7 +256,7 @@ void seq_monadic::live_states(expr* R, ptr_vector& out, bool& ok) { for (unsigned i = 0; i < states.size(); ++i) { if (states.size() > STATE_CAP || !m.inc()) { ok = false; return; } expr_ref_pair_vector cof(m); - m_rw.brz_derivative_cofactors(states.get(i), cof); + derivative_cofactors(states.get(i), cof); for (auto const& [g, t] : cof) { if (re().is_empty(t)) continue; unsigned k = intern(t); // MUST precede succ[i] indexing: intern may @@ -357,7 +362,7 @@ lbool seq_monadic::product_nonempty(svector const& comps, expr_ref* w std::vector>> branches(n); for (unsigned i = 0; i < n; ++i) { expr_ref_pair_vector cof(m); - m_rw.brz_derivative_cofactors(st[i], cof); + derivative_cofactors(st[i], cof); for (auto const& [g, t] : cof) { if (re().is_empty(t)) continue; m_pin.push_back(t); diff --git a/src/ast/rewriter/seq_monadic.h b/src/ast/rewriter/seq_monadic.h index d979134e47..63de75cc5d 100644 --- a/src/ast/rewriter/seq_monadic.h +++ b/src/ast/rewriter/seq_monadic.h @@ -15,9 +15,9 @@ Abstract: derivatives). Self-contained decision procedure: NO Nielsen splitting (seq_split), NO minterms, - and NO materialization of reach(q) as a regex. It relies only on the symbolic - Brzozowski derivative (brz_derivative_cofactors as a transition regex) and on - automaton product-reachability for emptiness. + and NO materialization of reach(q) as a regex. It uses symbolic derivative + cofactors as Brzozowski states or Brzozowski states post-processed into + light-weight Antimirov states, and automaton product-reachability for emptiness. Method. For a term x.u in R and the whole-language split, x drives the derivative automaton of R from R to some live state q, and the rest u must be accepted from q: @@ -59,10 +59,18 @@ Author: #include class seq_monadic { +public: + enum class transition_mode { + brzozowski, + light_antimirov + }; + +private: ast_manager& m; seq_rewriter& m_rw; th_rewriter m_thrw; // normalizes constant-element derivatives (folds // ground guards so dead states become re.empty) + transition_mode m_mode; sort* m_seq_sort = nullptr; // sequence sort of the regex under analysis sort* m_elem_sort = nullptr; // element sort of that sequence sort expr_ref_vector m_pin; // pins derivative states / witnesses referenced later @@ -86,6 +94,9 @@ class seq_monadic { // Brzozowski derivative of regex `r` by the concrete element `elem`. expr_ref der_elem(expr* r, expr* elem); + // Symbolic transition cofactors in the selected mode. + void derivative_cofactors(expr* r, expr_ref_pair_vector& result); + // Live reachable derivative states of R (BFS over cofactor targets + liveness // least-fixpoint). These are the split states q. Sets `ok` false on a cap overrun. void live_states(expr* R, ptr_vector& out, bool& ok); @@ -119,7 +130,10 @@ class seq_monadic { obj_map* model); public: - seq_monadic(seq_rewriter& rw) : m(rw.m()), m_rw(rw), m_thrw(rw.m()), m_pin(rw.m()) {} + seq_monadic(seq_rewriter& rw, transition_mode mode = transition_mode::light_antimirov) : + m(rw.m()), m_rw(rw), m_thrw(rw.m()), m_mode(mode), m_pin(rw.m()) {} + + transition_mode mode() const { return m_mode; } // Decide (str.in_re term R) for a term that is a concatenation of string variables // (possibly repeated / several distinct) and constant characters. diff --git a/src/ast/rewriter/seq_rewriter.cpp b/src/ast/rewriter/seq_rewriter.cpp index 8aed5bf43a..d5f42cbbe9 100644 --- a/src/ast/rewriter/seq_rewriter.cpp +++ b/src/ast/rewriter/seq_rewriter.cpp @@ -2931,6 +2931,66 @@ expr_ref seq_rewriter::mk_derivative(expr* ele, expr* r) { return result; } +void seq_rewriter::light_ant_derivative_cofactors(expr* r, expr_ref_pair_vector& result) { + expr_ref_pair_vector brz(m()); + m_derive.derivative_cofactors(r, brz); + + obj_map target_index; + expr_ref_vector guards(m()); + expr_ref_vector targets(m()); + + auto add = [&](expr* guard, expr* target) { + unsigned index = 0; + if (target_index.find(target, index)) { + expr_ref merged(m()); + m_br.mk_or(guards.get(index), guard, merged); + guards.set(index, merged); + } + else { + target_index.insert(target, targets.size()); + targets.push_back(target); + guards.push_back(guard); + } + }; + + for (auto const& [guard, target] : brz) { + ptr_vector pending; + pending.push_back(target); + while (!pending.empty()) { + expr* t = pending.back(); + pending.pop_back(); + expr* left = nullptr, * right = nullptr; + if (re().is_union(t, left, right)) { + pending.push_back(right); + pending.push_back(left); + } + else if (re().is_concat(t, left, right) && re().is_union(left)) { + ptr_vector heads; + heads.push_back(left); + while (!heads.empty()) { + expr* head = heads.back(); + heads.pop_back(); + expr* a = nullptr, * b = nullptr; + if (re().is_union(head, a, b)) { + heads.push_back(b); + heads.push_back(a); + } + else { + expr_ref split = mk_regex_concat(head, right); + add(guard, split); + } + } + } + else { + add(guard, t); + } + } + } + + result.reset(); + for (unsigned i = 0; i < targets.size(); ++i) + result.push_back(guards.get(i), targets.get(i)); +} expr_ref seq_rewriter::mk_regex_union_normalize(expr* r1, expr* r2) { expr_ref _r1(r1, m()), _r2(r2, m()); diff --git a/src/ast/rewriter/seq_rewriter.h b/src/ast/rewriter/seq_rewriter.h index ed84b2dbaf..c9c5ea989f 100644 --- a/src/ast/rewriter/seq_rewriter.h +++ b/src/ast/rewriter/seq_rewriter.h @@ -475,6 +475,13 @@ public: m_derive.derivative_cofactors(r, result); } + /* + Compute Brzozowski cofactors, then expose nondeterminism in targets of the + form (s1 | ... | sn) or (s1 | ... | sn) . tail. Cofactors with the same + resulting target are merged by disjoining their guards. + */ + void light_ant_derivative_cofactors(expr* r, expr_ref_pair_vector& result); + // heuristic elimination of element from condition that comes form a derivative. // special case optimization for conjunctions of equalities, disequalities and ranges. void elim_condition(expr* elem, expr_ref& cond); diff --git a/src/test/seq_monadic.cpp b/src/test/seq_monadic.cpp index 5377aac1a3..b1587d77ce 100644 --- a/src/test/seq_monadic.cpp +++ b/src/test/seq_monadic.cpp @@ -40,6 +40,7 @@ class seq_monadic_test { seq_util u; sort_ref m_str; // String sort sort_ref m_re; // RegEx sort over m_str + seq_monadic::transition_mode m_mode; unsigned m_fail = 0; seq_util::rex& re() { return u.re; } @@ -51,6 +52,7 @@ class seq_monadic_test { expr_ref star(expr* a) { return expr_ref(re().mk_star(a), m); } expr_ref inter(expr* a, expr* b) { return expr_ref(re().mk_inter(a, b), m); } expr_ref comp(expr* a) { return expr_ref(re().mk_complement(a), m); } + expr_ref dot() { return expr_ref(re().mk_full_char(m_re), m); } expr_ref dotstar() { return expr_ref(re().mk_full_seq(m_re), m); } expr_ref rng(char lo, char hi) { char sl[2] = { lo, 0 }, sh[2] = { hi, 0 }; @@ -70,6 +72,53 @@ class seq_monadic_test { expr_ref xyx(expr* x, expr* y) { return sconcat(x, sconcat(y, x)); } static char const* s(lbool l) { return l == l_true ? "sat" : l == l_false ? "unsat" : "undef"; } + char const* mode_name() const { + switch (m_mode) { + case seq_monadic::transition_mode::brzozowski: return "brz"; + case seq_monadic::transition_mode::light_antimirov: return "light-ant"; + } + UNREACHABLE(); + return ""; + } + + bool eval_guard(expr* guard, unsigned ch) { + sort* elem_sort = nullptr; + VERIFY(u.is_seq(m_str, elem_sort)); + expr_ref v0(m.mk_var(0, elem_sort), m); + expr_safe_replace rep(m); + rep.insert(v0, u.str.mk_char(ch)); + expr_ref instantiated(m), simplified(m); + rep(guard, instantiated); + th_rewriter rw(m); + rw(instantiated, simplified); + return m.is_true(simplified); + } + + void check_ant_cofactors() { + expr_ref a = word("a"); + expr_ref any = dotstar(); + expr_ref dot3 = loop(dot(), 3, 3); + expr_ref R = cat(any, cat(a, dot3)); + expr_ref_pair_vector cof(m); + m_rw.light_ant_derivative_cofactors(R, cof); + + bool found_R = false, found_dot3 = false, ok = cof.size() == 2; + for (auto const& [guard, target] : cof) { + if (target == R) { + found_R = eval_guard(guard, 'a') && eval_guard(guard, 'b'); + } + else if (target == dot3) { + found_dot3 = eval_guard(guard, 'a') && !eval_guard(guard, 'b'); + } + else { + ok = false; + } + } + ok = ok && found_R && found_dot3; + if (!ok) ++m_fail; + std::cout << (ok ? " OK " : " FAIL ") + << mode_name() << " cofactor construction\n"; + } void check(char const* name, expr* term, expr* R, lbool expected) { lbool got = m_mon.solve(term, R); @@ -145,12 +194,16 @@ class seq_monadic_test { } public: - seq_monadic_test() : m_reg(m), m_rw(m), m_mon(m_rw), u(m), m_str(m), m_re(m) { + seq_monadic_test(seq_monadic::transition_mode mode) : + m_reg(m), m_rw(m), m_mon(m_rw, mode), u(m), m_str(m), m_re(m), m_mode(mode) { m_str = u.str.mk_string_sort(); m_re = re().mk_re(m_str); } void run() { + std::cout << "=== seq_monadic mode: " << mode_name() << " ===\n"; + if (m_mode == seq_monadic::transition_mode::light_antimirov) + check_ant_cofactors(); expr_ref x = var("x"); expr_ref a = word("a"); expr_ref b = word("b"); @@ -309,6 +362,8 @@ public: } void tst_seq_monadic() { - seq_monadic_test t; - t.run(); + seq_monadic_test brz(seq_monadic::transition_mode::brzozowski); + brz.run(); + seq_monadic_test light_ant(seq_monadic::transition_mode::light_antimirov); + light_ant.run(); }