From 8e11ae58e9dcf41450fbb8d133675fcffd853263 Mon Sep 17 00:00:00 2001 From: Margus Veanes Date: Mon, 3 Aug 2026 10:06:26 -0700 Subject: [PATCH] move light_ant_derivative_cofactors into the derivative engine (#10371) MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit 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 --- src/ast/rewriter/seq_derive.cpp | 61 +++++++++++++++++++++++++++++++ src/ast/rewriter/seq_derive.h | 19 ++++++++++ src/ast/rewriter/seq_rewriter.cpp | 61 ------------------------------- src/ast/rewriter/seq_rewriter.h | 4 +- 4 files changed, 83 insertions(+), 62 deletions(-) diff --git a/src/ast/rewriter/seq_derive.cpp b/src/ast/rewriter/seq_derive.cpp index 9892ffd35c..8bfe4bf96b 100644 --- a/src/ast/rewriter/seq_derive.cpp +++ b/src/ast/rewriter/seq_derive.cpp @@ -1567,5 +1567,66 @@ namespace seq { get_cofactors(m_ele, d, result); } + void derive::light_ant_derivative_cofactors(expr* r, expr_ref_pair_vector& result) { + expr_ref_pair_vector brz(m); + 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 = m_re.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)); + } + } diff --git a/src/ast/rewriter/seq_derive.h b/src/ast/rewriter/seq_derive.h index e0559bdf1d..08e8631315 100644 --- a/src/ast/rewriter/seq_derive.h +++ b/src/ast/rewriter/seq_derive.h @@ -261,6 +261,25 @@ namespace seq { */ void derivative_cofactors(expr* r, expr_ref_pair_vector& result); + /** + * Compute the Brzozowski cofactors of r (derivative_cofactors above), + * then expose the nondeterminism that a union leaf hides: a target of + * the form (s1 | ... | sn), or (s1 | ... | sn) . tail, is split into + * one cofactor per alternative si (resp. si . tail). Splitting is + * applied recursively, so nested unions are flattened as well. + * + * Splitting can make two originally distinct cofactors reach the same + * target; such cofactors are merged back into a single pair whose + * guard is the disjunction of the original guards. The result is + * therefore still a list of distinct targets, but each one is a + * single Antimirov-style alternative rather than a union state. + * + * The guards are not required to be mutually exclusive after merging, + * and the transition relation is genuinely nondeterministic: a + * character may be accepted by several of the returned guards. + */ + void light_ant_derivative_cofactors(expr* r, expr_ref_pair_vector& result); + }; } diff --git a/src/ast/rewriter/seq_rewriter.cpp b/src/ast/rewriter/seq_rewriter.cpp index 508e2dea6d..6b71e47db5 100644 --- a/src/ast/rewriter/seq_rewriter.cpp +++ b/src/ast/rewriter/seq_rewriter.cpp @@ -2931,67 +2931,6 @@ 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()); expr *a1, *b1, *a2, *b2; diff --git a/src/ast/rewriter/seq_rewriter.h b/src/ast/rewriter/seq_rewriter.h index c9c5ea989f..5bad5ae3dc 100644 --- a/src/ast/rewriter/seq_rewriter.h +++ b/src/ast/rewriter/seq_rewriter.h @@ -480,7 +480,9 @@ public: 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); + void light_ant_derivative_cofactors(expr* r, expr_ref_pair_vector& result) { + m_derive.light_ant_derivative_cofactors(r, result); + } // heuristic elimination of element from condition that comes form a derivative. // special case optimization for conjunctions of equalities, disequalities and ranges.