From 07c797c32be68ce678e71cc0f6a8ebdfd9d1b829 Mon Sep 17 00:00:00 2001 From: Margus Veanes Date: Fri, 3 Jul 2026 19:40:26 +0300 Subject: [PATCH] seq_split: dedup identical pairs in intersect (sound, memory-only) A split-set denotes the UNION of its pairs, so identical (hash-consed) pairs are redundant; skipping them in the De Morgan cross-product cuts the materialized split-set ~7x on L15 negcount (65536 -> 9216) with no behaviour change (verified L11 sat / L14 unsat). NOTE: memory-only -- it does not fix the underlying combinatorial blow-up of complement()'s structural De Morgan on a concatenation of predicates (root cause; see spec analysis). Adds nseq-split-dedup-drops counter. Easily reverted if a derivative/minterm-based complement supersedes the cross-product. Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com> --- src/ast/rewriter/seq_split.cpp | 11 +++++++++++ src/ast/rewriter/seq_split.h | 1 + src/smt/seq/seq_nielsen.cpp | 1 + 3 files changed, 13 insertions(+) diff --git a/src/ast/rewriter/seq_split.cpp b/src/ast/rewriter/seq_split.cpp index 43f61f26a8..c2984e905b 100644 --- a/src/ast/rewriter/seq_split.cpp +++ b/src/ast/rewriter/seq_split.cpp @@ -20,6 +20,7 @@ Author: #include "ast/rewriter/seq_rewriter.h" #include "ast/ast_pp.h" #include "util/obj_hashtable.h" +#include "util/obj_pair_hashtable.h" #include "util/stack.h" seq_split::seq_split(seq_rewriter& rw) : @@ -191,6 +192,10 @@ bool seq_split::intersect(split_set const& s1, split_set const& s2, split_set& r unsigned threshold, split_oracle const& oracle) const { ++m_stats.m_intersect; const seq_util::rex& r = re(); + // Dedup the cross-product: a split-set denotes the UNION of its pairs, + // so identical (perfectly-shared) pairs are redundant. Skipping them keeps + // the De Morgan fold from accumulating exponentially many equal splits. + obj_pair_hashtable seen; for (auto const& p1 : s1) { for (auto const& p2 : s2) { if (r.is_empty(p1.m_d) || r.is_empty(p2.m_d) || @@ -199,6 +204,12 @@ bool seq_split::intersect(split_set const& s1, split_set const& s2, split_set& r const expr_ref di(m_rw.mk_regex_inter_normalize(p1.m_d, p2.m_d), m); const expr_ref ni(m_rw.mk_regex_inter_normalize(p1.m_n, p2.m_n), m); ++m_stats.m_intersect_pairs; + std::pair key(di.get(), ni.get()); + if (seen.contains(key)) { + ++m_stats.m_dedup_drops; + continue; + } + seen.insert(key); push(result, oracle, di, ni); if (result.size() > threshold) { ++m_stats.m_threshold_overruns; diff --git a/src/ast/rewriter/seq_split.h b/src/ast/rewriter/seq_split.h index 86953a250f..046bde3c15 100644 --- a/src/ast/rewriter/seq_split.h +++ b/src/ast/rewriter/seq_split.h @@ -72,6 +72,7 @@ struct split_stats { unsigned m_giveups = 0; // iterator give-ups (unsupported/weak/overrun) unsigned m_threshold_overruns = 0; // threshold hits (intersect/complement/iterator) unsigned m_max_split_set = 0; // largest materialized split-set seen + unsigned m_dedup_drops = 0; // duplicate pairs skipped in intersect unsigned m_simplify = 0; // simplify() calls void reset() { *this = split_stats(); } }; diff --git a/src/smt/seq/seq_nielsen.cpp b/src/smt/seq/seq_nielsen.cpp index e36a01326f..55c14f280a 100644 --- a/src/smt/seq/seq_nielsen.cpp +++ b/src/smt/seq/seq_nielsen.cpp @@ -6019,6 +6019,7 @@ namespace seq { st.update("nseq split giveups", sp.m_giveups); st.update("nseq split threshold-overruns", sp.m_threshold_overruns); st.update("nseq split max-split-set", sp.m_max_split_set); + st.update("nseq split dedup-drops", sp.m_dedup_drops); st.update("nseq split simplify", sp.m_simplify); }