From 02e2d681da77f67ef3a0baf5b8b58485e4f7d714 Mon Sep 17 00:00:00 2001 From: CEisenhofer Date: Tue, 21 Jul 2026 11:09:01 +0200 Subject: [PATCH] Fixed intersect_product --- src/ast/rewriter/seq_monadic.cpp | 148 +++++++++++++++---------------- src/ast/rewriter/seq_monadic.h | 8 +- 2 files changed, 77 insertions(+), 79 deletions(-) diff --git a/src/ast/rewriter/seq_monadic.cpp b/src/ast/rewriter/seq_monadic.cpp index 7987407047..05dca9b4bf 100644 --- a/src/ast/rewriter/seq_monadic.cpp +++ b/src/ast/rewriter/seq_monadic.cpp @@ -53,6 +53,7 @@ Shady parts: --*/ #include "ast/rewriter/seq_monadic.h" +#include "ast/ast_util.h" #include #include #include @@ -194,17 +195,6 @@ namespace seq { return N == nullptr || re.is_epsilon(N); } - // Flatten the operands of a (possibly nested) re.inter into `out`. - static void flatten_inter(seq_util::rex& re, expr* e, ptr_vector& out) { - expr* a = nullptr, * b = nullptr; - if (re.is_intersection(e, a, b)) { - flatten_inter(re, a, out); - flatten_inter(re, b, out); - } - else - out.push_back(e); - } - // Beyond `depth_cap` elements the length no longer changes acceptance, so the // BFS caps the depth component of its visited key there to stay finite. static unsigned depth_cap(unsigned lo, unsigned hi) { return hi == UINT_MAX ? lo : hi; } @@ -323,16 +313,17 @@ namespace seq { unsigned hi, expr_ref_vector& seq) { unsigned n = crs.size(); - bool_vector memb; // per component: membership (nullable) vs reach - ptr_vector tgt; // per component: reach target (or null) - svector start; // start tuple + bool_vector mem; + ptr_vector tgt; + svector start; for (auto const& cr : crs) { bool mb = is_membership(re(), cr); - memb.push_back(mb); + mem.push_back(mb); tgt.push_back(mb ? nullptr : cr.second.get()); start.push_back(cr.first.get()); m_pin.push_back(cr.first.get()); - if (!mb) m_pin.push_back(cr.second.get()); + if (!mb) + m_pin.push_back(cr.second.get()); } // Search state is the product tuple; acceptance is per-component (nullable @@ -341,12 +332,14 @@ namespace seq { auto key_of = [](svector const& st) { std::vector k; k.reserve(st.size()); - for (expr* e : st) k.push_back(e->get_id()); + for (const expr * e : st) { + k.push_back(e->get_id()); + } return k; }; auto accept = [&](svector const& st) -> lbool { for (unsigned i = 0; i < n; ++i) { - if (!memb[i]) { + if (!mem[i]) { if (st[i] != tgt[i]) return l_false; // reach: structural target continue; } @@ -358,71 +351,78 @@ namespace seq { } return l_true; }; - // The engine prunes infeasible joint guards and yields the product successor - // as the re.inter of the per-component derivatives -- but we must NOT assume - // it keeps them in source order (mk_inter subset-collapses, De-Morgan-merges, - // and may reorder operands). So we recover the correspondence by IDENTITY: - // each operand of the joint target is matched to the component whose own - // derivative-target set contains it. A cofactor whose operands cannot be - // assigned bijectively (a merge dropped one, or the match is ambiguous) sets - // `collapsed`, softening a final l_false to l_undef -- we cannot certify - // emptiness through an edge we could not decompose. - bool collapsed = false; + sort* seq_sort = nullptr, * ele_sort = nullptr; + VERIFY(u().is_re(crs[0].first.get(), seq_sort)); + VERIFY(u().is_seq(seq_sort, ele_sort)); + expr_ref ele(m.mk_var(0, ele_sort), m); + expr_ref eps_re(re().mk_epsilon(seq_sort), m); + expr_ref empty_re(re().mk_empty(crs[0].first.get()->get_sort()), m); + + auto feasible = [&](expr* cond) -> bool { + if (m.is_true(cond)) + return true; + const expr_ref tr(m.mk_ite(cond, eps_re, empty_re), m); + expr_ref_pair_vector res(m); + m_rw.get_cofactors(ele, tr, res); + for (auto const& [g, t] : res) { + if (!re().is_empty(t)) + return true; + } + return false; + }; auto expand = [&](svector const& st, std::vector, expr*>>& out) { - // Per-component derivative targets (order-independent recovery dictionary). std::vector> comp_succ(n); + vector> cg, ct; + cg.resize(n); + ct.resize(n); for (unsigned i = 0; i < n; ++i) { expr_ref_pair_vector ci(m); m_rw.brz_derivative_cofactors(st[i], ci); - for (auto const& [gi, ti] : ci) - if (!re().is_empty(ti)) - comp_succ[i].push_back(ti); - } - // The unique operand of `ops` that is a derivative target of component i, - // or null if none / more than one (ambiguous). - auto derivative_of = [&](unsigned i, ptr_vector const& ops) -> expr* { - expr* hit = nullptr; - for (expr* op : ops) - for (expr* ti : comp_succ[i]) - if (op == ti) { - if (hit && hit != op) return nullptr; // ambiguous - hit = op; - break; - } - return hit; - }; - - expr_ref P(st[0], m); - for (unsigned i = 1; i < n; ++i) - P = re().mk_inter(P, st[i]); - expr_ref_pair_vector cof(m); - m_rw.brz_derivative_cofactors(P, cof); - for (auto const& [g, t] : cof) { - if (re().is_empty(t)) continue; - svector nst; - if (n == 1) - nst.push_back(t); - else { - ptr_vector ops; - flatten_inter(re(), t, ops); - nst.resize(n, nullptr); - bool ok_assign = (ops.size() == n); - for (unsigned i = 0; ok_assign && i < n; ++i) - if (!(nst[i] = derivative_of(i, ops))) - ok_assign = false; - for (unsigned i = 0; ok_assign && i < n; ++i) // require a bijection - for (unsigned j = i + 1; j < n; ++j) - if (nst[i] == nst[j]) ok_assign = false; - if (!ok_assign) { collapsed = true; continue; } + for (auto const& [gi, ti] : ci) { + if (re().is_empty(ti)) + continue; + cg[i].push_back(gi); + ct[i].push_back(ti); + m_pin.push_back(gi); + m_pin.push_back(ti); } - for (expr* s : nst) m_pin.push_back(s); - m_pin.push_back(g); - out.push_back({ nst, g }); + if (ct[i].empty()) + return true; + } + + svector idx; + idx.resize(n, 0); + svector tuple; + tuple.resize(n, nullptr); + while (true) { + expr_ref_vector gs(m); + for (unsigned i = 0; i < n; ++i) { + tuple[i] = ct[i][idx[i]]; + gs.push_back(cg[i][idx[i]]); + } + expr_ref g = mk_and(gs); + if (n == 1 || feasible(g)) { + for (expr* s : tuple) { + m_pin.push_back(s); + } + m_pin.push_back(g); + out.push_back({ tuple, g }); + } + unsigned k = 0; + for (; k < n; ++k) { + idx[k]++; + if (idx[k] < ct[k].size()) + break; + idx[k] = 0; + } + if (k == n) + break; + if (!m.inc()) + return false; } return true; }; - lbool r = bounded_search>(m, start, lo, hi, key_of, accept, expand, seq); - return (r == l_false && collapsed) ? l_undef : r; + return bounded_search>(m, start, lo, hi, key_of, accept, expand, seq); } bool split_manager::test_intersect(vector const& crs) { diff --git a/src/ast/rewriter/seq_monadic.h b/src/ast/rewriter/seq_monadic.h index 45dfc5ff0b..b4eaee85ba 100644 --- a/src/ast/rewriter/seq_monadic.h +++ b/src/ast/rewriter/seq_monadic.h @@ -33,8 +33,7 @@ Abstract: The module is element-sort agnostic: it does NOT hard-code any character reasoning. Guard feasibility and successor computation are delegated entirely to the symbolic derivative engine (seq_rewriter::brz_derivative_cofactors, which - prunes infeasible guards internally and, on an re.inter, yields the product - successor in source order) and to th_rewriter for normalization. + prunes infeasible guards internally). Author: @@ -159,7 +158,7 @@ namespace seq { expr_ref_vector& seq); // Product-reachability of a tuple of continuation regexes (handles general N, - // i.e. reach targets N != epsilon), decomposing the engine's product successor. + // i.e. reach targets N != epsilon). lbool intersect_product(vector const& crs, unsigned lo, unsigned hi, expr_ref_vector& seq); @@ -192,8 +191,7 @@ namespace seq { // is decided by the derivative engine (element-sort agnostic). On l_true a // witness is returned in `seq`: one guard predicate over (:var 0) per position. // l_false = empty, l_true = non-empty, l_undef = gave up - // (cap overrun, undecidable nullability, or a product target that could not - // be decomposed). + // (cap overrun or undecidable nullability). lbool intersect(vector const& crs, unsigned lo, unsigned hi, expr_ref_vector& seq); // Cheap, sound one-sided partial check: false only when the intersection is