From 549e5c5d9c89bda1235b8f305ce3cd0157cfd778 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Tue, 30 Jun 2026 20:51:36 -0700 Subject: [PATCH 01/24] add signature Signed-off-by: Nikolaj Bjorner --- src/ast/rewriter/seq_split.h | 25 +++++++++++++++++++++++++ 1 file changed, 25 insertions(+) diff --git a/src/ast/rewriter/seq_split.h b/src/ast/rewriter/seq_split.h index f3b7a57675..03b2eb9bf5 100644 --- a/src/ast/rewriter/seq_split.h +++ b/src/ast/rewriter/seq_split.h @@ -31,6 +31,31 @@ Author: class seq_rewriter; +class split_set2 { + struct imp; + imp *m_imp; + +public: + split_set2(seq_rewriter &rw, expr *r); + + ~split_set2(); + + class iterator { + struct imp; + imp *m_imp; + public: + iterator(split_set2& s, bool end = false); + ~iterator(); + iterator &operator++(); + std::pair operator*() const; + bool operator==(iterator const &other) const; + bool operator!=(iterator const &other) const; + }; + + iterator begin() const; + iterator end() const; +}; + // An individual split : the left (prefix) regex D and right (suffix) // regex N. u.v in L(r) for this split iff u in L(D) and v in L(N). struct split_pair { From 1f3b053f9e12624b44b650a5f81d3710390fbfb4 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Wed, 1 Jul 2026 07:46:16 -0700 Subject: [PATCH 02/24] outline opaque splitter Signed-off-by: Nikolaj Bjorner --- src/ast/rewriter/seq_split.cpp | 351 ++++++++++++++++++++++++++++----- src/ast/rewriter/seq_split.h | 51 +++-- 2 files changed, 341 insertions(+), 61 deletions(-) diff --git a/src/ast/rewriter/seq_split.cpp b/src/ast/rewriter/seq_split.cpp index 8977065fc0..08fd6bfb90 100644 --- a/src/ast/rewriter/seq_split.cpp +++ b/src/ast/rewriter/seq_split.cpp @@ -19,7 +19,295 @@ Author: #include "ast/rewriter/seq_rewriter.h" #include "ast/ast_pp.h" #include "util/obj_hashtable.h" -#include "util/stack.h" + +struct split_set2::imp { + ast_manager &m; + seq_rewriter &rw; + seq_util &seq; + seq_util::rex &re; + expr_ref r; + unsigned m_threshold = UINT_MAX; + split_oracle m_filter; + sort *m_seq_sort = nullptr; // sequence sort the decls are built for + + imp(seq_rewriter &rw, expr *r, unsigned threshold, split_oracle const &filter) : m(rw.m()), rw(rw), + seq(rw.u()), re(rw.u().re), r(r, m), m_threshold(threshold), m_filter(filter) { + VERIFY(seq.is_re(r, m_seq_sort)); + } + +}; + +struct split_set2::iterator::imp { + struct cartesian_product { + split_set2::imp &s; + imp &i; + split_set2 a_s, b_s; + split_set2::iterator a_it; + split_set2::iterator b_it; + cartesian_product(imp &i, expr *a, expr *b) + : s(i.i), i(i), a_s(s.rw, a, {}), b_s(s.rw, b, {}), a_it(a_s.begin()), b_it(b_s.begin()) {} + bool at_end() const { + return a_it == a_s.end() && b_it == b_s.end(); + } + void next() { + SASSERT(!at_end()); + if (b_it != b_s.end()) + ++b_it; + + if (b_it == b_s.end()) { + ++a_it; + if (a_it != a_s.end()) + b_it.m_imp->rewind(); + } + } + void consume() { + while (!at_end() && !i.has_split()) { + auto [a1, a2] = *a_it; + auto [b1, b2] = *b_it; + expr_ref a(s.rw.mk_regex_inter_normalize(a1, b1), s.m); + expr_ref b(s.rw.mk_regex_inter_normalize(a2, b2), s.m); + i.push_split(a, b); + next(); + } + if (b_it.failed() || a_it.failed()) + i.m_failure = true; + } + }; + + // Complement of a split-set via De Morgan: ~S = cap_{s in S} ~s with + // ~ = { <~D, .*>, <.*, ~N> } and ~{} = { <.*, .*> }. + // May produce up to 2^|sp| pairs (bounded by the threshold). A threshold + // overrun must abort entirely: a partial fold is a strictly weaker (unsound) + // split-set, since each ~sp[i] further constrains ~S. + + struct complement { + split_set2::imp &s; + imp &i; + split_set2 a; + split_set2::iterator it; + + complement(imp &i, expr *r) : s(i.i), i(i), a(s.rw, r, {}), it(a.begin()) {} + + void consume() { + while (it != a.end() && !i.has_split()) { + auto [a, b] = *it; + NOT_IMPLEMENTED_YET(); + // create a cascade of cross-products. + // empty set as a base case. + ++it; + } + } + }; + split_set2 &s; + split_set2::imp &i; + ast_manager &m; + seq_util &seq; + seq_util::rex &re; + expr_ref_vector m_cont; + vector> m_splits; + unsigned m_qhead = 0; + scoped_ptr m_cartesian; + scoped_ptr m_complement; + bool m_at_end; + bool m_failure = false; + imp(split_set2 &s, bool at_end) : s(s), i(*s.m_imp), m(i.m), seq(i.seq), re(i.re), m_cont(m), m_at_end(at_end) { + m_cont.push_back(i.r); + } + + bool has_split() { + return m_qhead < m_splits.size(); + } + + void rewind() { + m_qhead = 0; + m_at_end = m_qhead < m_splits.size(); + SASSERT(m_cont.empty()); + SASSERT(!m_cartesian); + SASSERT(!m_complement); + } + + void next() { + while (!at_end()) { + m_qhead++; + if (has_split()) + return; + if (m_cartesian) { + m_cartesian->consume(); + if (!m_splits.empty()) + return; + m_cartesian = nullptr; + } + + if (m_complement) { + m_complement->consume(); + if (!m_splits.empty()) + return; + m_complement = nullptr; + } + + if (m_cont.empty()) { + m_at_end = true; + return; + } + + // TODO: we can be strategic about choosing what to unfold, + // and perform early subsumption check + expr_ref last(m_cont.back(), m); + m_cont.pop_back(); + unfold(last); + } + } + + void push_split(expr *a, expr *b) { + if (m_failure) + return; + if (i.m_filter && !i.m_filter(a, b)) + return; + if (re.get_info(a).min_length == UINT_MAX) + return; + if (re.get_info(b).min_length == UINT_MAX) + return; + // subsumption checking + m_splits.push_back({expr_ref(a, m), expr_ref(b, m)}); + if (m_splits.size() > i.m_threshold) { + TRACE(seq, tout << "size of split set exceeds threshold"); + m_failure = true; + } + } + + void unfold(expr* r) { + SASSERT(seq.is_re(r)); + if (re.is_empty(r)) + return; + + expr *a, *b; + if (re.is_union(r, a, b)) { + m_cont.push_back(a); + m_cont.push_back(b); + return; + } + + if (re.is_intersection(r, a, b)) { + m_cartesian = alloc(cartesian_product, *this, a, b); + return; + } + + if (re.is_complement(r, a)) { + m_complement = alloc(complement, *this, a); + return; + } + + if (re.is_concat(r, a, b)) { + NOT_IMPLEMENTED_YET(); + } + + if (re.is_to_re(r, a)) { + if (seq.str.is_concat(a, a, b)) { + m_cont.push_back(re.mk_concat(re.mk_to_re(a), re.mk_to_re(b))); + return; + } + if (seq.str.is_unit(a, b)) { + expr_ref eps(nullptr, m); // TODO + push_split(eps, a); + push_split(a, eps); + return; + } + zstring zs; + if (seq.str.is_string(a, zs)) { + // TODO + NOT_IMPLEMENTED_YET(); + } + set_failure(r); + return; + } + + if (re.is_epsilon(r)) { + push_split(r, r); + return; + } + + if (re.is_star(r, a)) { + NOT_IMPLEMENTED_YET(); + } + + if (re.is_plus(r, a)) { + NOT_IMPLEMENTED_YET(); + } + + if (re.is_diff(r, a, b)) { + NOT_IMPLEMENTED_YET(); + } + + if (re.is_full_char(r) || re.is_range(r) || re.is_of_pred(r)) { + expr_ref eps(re.mk_epsilon(i.m_seq_sort), m); + push_split(r, eps); + push_split(eps, r); + return; + } + + // .* : sigma(.*) = { <.*, .*> } + if (re.is_full_seq(r)) { + push_split(r, r); + return; + } + + set_failure(r); + } + + void set_failure(expr* r) { + TRACE(seq, tout << "split_set2::iterator::unfold: unhandled regex: " << mk_pp(r, m) << "\n"); + m_failure = true; + m_at_end = true; + } + + bool at_end() const { + return m_failure || m_at_end; + } +}; + +split_set2::split_set2(seq_rewriter &rw, expr *r, unsigned threshold, split_oracle const &oracle) { + m_imp = alloc(imp, rw, r, threshold, oracle); +} + +split_set2::~split_set2() { + dealloc(m_imp); +} + +split_set2::iterator::iterator(split_set2 const &s, bool at_end) { + m_imp = alloc(imp, const_cast(s), at_end); +} + +split_set2::iterator::~iterator() { + dealloc(m_imp); +} + + +split_set2::iterator split_set2::begin() const { + return iterator(*this, false); +} + +split_set2::iterator split_set2::end() const { + return iterator(*this, true); +} + +split_set2::iterator& split_set2::iterator::operator++() { + m_imp->next(); + return *this; +} + +std::pair split_set2::iterator::operator*() const { + SASSERT(m_imp->has_split()); + return m_imp->m_splits[m_imp->m_qhead]; +} + +bool split_set2::iterator::operator==(split_set2::iterator const &other) const { + SASSERT(m_imp->at_end() || other.m_imp->at_end()); + return m_imp->at_end() && other.m_imp->at_end(); +} + +bool split_set2::iterator::failed() const { + return m_imp->m_failure; +} seq_split::seq_split(seq_rewriter& rw) : m(rw.m()), m_rw(rw), m_subset(rw.u().re), @@ -119,53 +407,24 @@ expr_ref seq_split::mk_rcat(expr* s, expr* r) { bool seq_split::is_empty_ss(expr* e) const { return is_app(e) && to_app(e)->get_decl() == m_d_empty; } -bool seq_split::is_single(expr* e, expr*& d, expr*& n) const { - if (!is_app(e) || to_app(e)->get_decl() != m_d_single) - return false; - d = to_app(e)->get_arg(0); - n = to_app(e)->get_arg(1); - return true; + +bool seq_split::is_app1(expr* e, func_decl* d, expr*& a) const { + if (is_app(e) && to_app(e)->get_decl() == d) { + a = to_app(e)->get_arg(0); + return true; + } + return false; } -bool seq_split::is_fromre(expr* e, expr*& r) const { - if (!is_app(e) || to_app(e)->get_decl() != m_d_fromre) - return false; - r = to_app(e)->get_arg(0); - return true; -} -bool seq_split::is_union(expr* e, expr*& a, expr*& b) const { - if (!is_app(e) || to_app(e)->get_decl() != m_d_union) - return false; - a = to_app(e)->get_arg(0); - b = to_app(e)->get_arg(1); - return true; -} -bool seq_split::is_inter(expr* e, expr*& a, expr*& b) const { - if (!is_app(e) || to_app(e)->get_decl() != m_d_inter) - return false; - a = to_app(e)->get_arg(0); - b = to_app(e)->get_arg(1); - return true; -} -bool seq_split::is_compl(expr* e, expr*& a) const { - if (!is_app(e) || to_app(e)->get_decl() != m_d_compl) - return false; - a = to_app(e)->get_arg(0); - return true; -} -bool seq_split::is_lcat(expr* e, expr*& r, expr*& s) const { - if (!is_app(e) || to_app(e)->get_decl() != m_d_lcat) - return false; - r = to_app(e)->get_arg(0); - s = to_app(e)->get_arg(1); - return true; -} -bool seq_split::is_rcat(expr* e, expr*& s, expr*& r) const { - if (!is_app(e) || to_app(e)->get_decl() != m_d_rcat) - return false; - s = to_app(e)->get_arg(0); - r = to_app(e)->get_arg(1); - return true; + +bool seq_split::is_app2(expr *e, func_decl *d, expr *&a, expr *&b) const { + if (is_app(e) && to_app(e)->get_decl() == d) { + a = to_app(e)->get_arg(0); + b = to_app(e)->get_arg(1); + return true; + } + return false; } + bool seq_split::is_frontier(expr* e) const { expr *a = nullptr, *b = nullptr; return is_empty_ss(e) || is_single(e, a, b) || is_union(e, a, b); diff --git a/src/ast/rewriter/seq_split.h b/src/ast/rewriter/seq_split.h index 03b2eb9bf5..34f8ed8359 100644 --- a/src/ast/rewriter/seq_split.h +++ b/src/ast/rewriter/seq_split.h @@ -31,12 +31,17 @@ Author: class seq_rewriter; +// Optional lookahead oracle. Called for each candidate split as it is +// generated; returns true to keep it, false to prune it. An empty oracle (the +// default) keeps everything, so sigma is unchanged. See seq_split::compute. +typedef std::function split_oracle; + class split_set2 { struct imp; imp *m_imp; public: - split_set2(seq_rewriter &rw, expr *r); + split_set2(seq_rewriter &rw, expr *r, unsigned threshold, split_oracle const& oracle = split_oracle()); ~split_set2(); @@ -44,12 +49,15 @@ public: struct imp; imp *m_imp; public: - iterator(split_set2& s, bool end = false); + iterator(split_set2 const& s, bool end = false); ~iterator(); iterator &operator++(); - std::pair operator*() const; + std::pair operator*() const; + bool failed() const; bool operator==(iterator const &other) const; - bool operator!=(iterator const &other) const; + bool operator!=(iterator const &other) const { + return !(*this == other); + } }; iterator begin() const; @@ -77,10 +85,7 @@ typedef vector split_set; // give up (return false) on complement / intersection instead. enum class split_mode { weak, strong }; -// Optional lookahead oracle. Called for each candidate split as it is -// generated; returns true to keep it, false to prune it. An empty oracle (the -// default) keeps everything, so sigma is unchanged. See seq_split::compute. -typedef std::function split_oracle; + class seq_split { ast_manager& m; @@ -126,13 +131,29 @@ class seq_split { // Recognizers over the local decls. bool is_empty_ss(expr* e) const; - bool is_single(expr* e, expr*& d, expr*& n) const; - bool is_fromre(expr* e, expr*& r) const; - bool is_union (expr* e, expr*& a, expr*& b) const; - bool is_inter (expr* e, expr*& a, expr*& b) const; - bool is_compl (expr* e, expr*& a) const; - bool is_lcat (expr* e, expr*& r, expr*& s) const; - bool is_rcat (expr* e, expr*& s, expr*& r) const; + bool is_app1(expr *e, func_decl *d, expr *&a) const; + bool is_app2(expr *e, func_decl *d, expr*& a, expr*& b) const; + bool is_single(expr *e, expr *&d, expr *&n) const { + return is_app2(e, m_d_single, d, n); + } + bool is_fromre(expr* e, expr*& r) const { + return is_app1(e, m_d_fromre, r); + } + bool is_union (expr* e, expr*& a, expr*& b) const { + return is_app2(e, m_d_union, a, b); + } + bool is_inter (expr* e, expr*& a, expr*& b) const { + return is_app2(e, m_d_inter, a, b); + } + bool is_compl (expr* e, expr*& a) const { + return is_app1(e, m_d_compl, a); + } + bool is_lcat (expr* e, expr*& r, expr*& s) const { + return is_app2(e, m_d_lcat, r, s); + } + bool is_rcat (expr* e, expr*& s, expr*& r) const { + return is_app2(e, m_d_rcat, s, r); + } // A term whose head is empty | single | union (ready for the worklist loop). bool is_frontier(expr* e) const; From 052e1a54a679f10a10305c2ad75c1979db0be006 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Wed, 1 Jul 2026 07:52:52 -0700 Subject: [PATCH 03/24] outline opaque splitter Signed-off-by: Nikolaj Bjorner --- src/ast/rewriter/seq_split.cpp | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/src/ast/rewriter/seq_split.cpp b/src/ast/rewriter/seq_split.cpp index 08fd6bfb90..5db1de81c5 100644 --- a/src/ast/rewriter/seq_split.cpp +++ b/src/ast/rewriter/seq_split.cpp @@ -127,20 +127,20 @@ struct split_set2::iterator::imp { } void next() { + m_qhead++; while (!at_end()) { - m_qhead++; if (has_split()) return; if (m_cartesian) { m_cartesian->consume(); - if (!m_splits.empty()) + if (has_split()) return; m_cartesian = nullptr; } if (m_complement) { m_complement->consume(); - if (!m_splits.empty()) + if (has_split()) return; m_complement = nullptr; } From 2e5f1b1d69ca5e979216e24e360e4b22fdb30c52 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Wed, 1 Jul 2026 16:25:25 -0700 Subject: [PATCH 04/24] updates to split_set Signed-off-by: Nikolaj Bjorner --- src/ast/rewriter/seq_rewriter.h | 4 +- src/ast/rewriter/seq_split.cpp | 349 +++++++++++++++++++++++------- src/ast/rewriter/seq_split.h | 5 + src/cmd_context/tptp_frontend.cpp | 23 +- 4 files changed, 303 insertions(+), 78 deletions(-) diff --git a/src/ast/rewriter/seq_rewriter.h b/src/ast/rewriter/seq_rewriter.h index 7cd5bf7153..1781ef6f23 100644 --- a/src/ast/rewriter/seq_rewriter.h +++ b/src/ast/rewriter/seq_rewriter.h @@ -198,7 +198,7 @@ class seq_rewriter { bool neq_char(expr* ch1, expr* ch2); bool le_char(expr* ch1, expr* ch2); bool are_complements(expr* r1, expr* r2) const; - bool is_subset(expr* r1, expr* r2) const; + br_status mk_seq_unit(expr* e, expr_ref& result); br_status mk_seq_concat(expr* a, expr* b, expr_ref& result); @@ -422,6 +422,8 @@ public: void simplify_split(split_set& s) { m_split.simplify(s); } + bool is_subset(expr *r1, expr *r2) const; + // decompose a membership constraint into a set of pairs of regex splits std::pair split_membership(expr* str, expr* regex, unsigned threshold, split_set& result) const { return m_split.split_membership(str, regex, threshold, result); diff --git a/src/ast/rewriter/seq_split.cpp b/src/ast/rewriter/seq_split.cpp index 5db1de81c5..a39a14e50a 100644 --- a/src/ast/rewriter/seq_split.cpp +++ b/src/ast/rewriter/seq_split.cpp @@ -19,6 +19,7 @@ Author: #include "ast/rewriter/seq_rewriter.h" #include "ast/ast_pp.h" #include "util/obj_hashtable.h" +#include "util/scoped_ptr_vector.h" struct split_set2::imp { ast_manager &m; @@ -28,49 +29,66 @@ struct split_set2::imp { expr_ref r; unsigned m_threshold = UINT_MAX; split_oracle m_filter; + sort *m_re_sort = nullptr; sort *m_seq_sort = nullptr; // sequence sort the decls are built for imp(seq_rewriter &rw, expr *r, unsigned threshold, split_oracle const &filter) : m(rw.m()), rw(rw), seq(rw.u()), re(rw.u().re), r(r, m), m_threshold(threshold), m_filter(filter) { - VERIFY(seq.is_re(r, m_seq_sort)); + if (r) { + VERIFY(seq.is_re(r, m_seq_sort)); + m_re_sort = r->get_sort(); + } } +}; +class split_set2::consumer { +protected: + split_set2::iterator::imp *ip = nullptr; +public: + virtual void consume() = 0; + void set_parent(split_set2::iterator::imp &i) { + ip = &i; + } + split_set2::iterator::imp &parent() { + return *ip; + } }; struct split_set2::iterator::imp { - struct cartesian_product { - split_set2::imp &s; - imp &i; + struct intersection : public split_set2::consumer { + split_set2 a_s, b_s; - split_set2::iterator a_it; - split_set2::iterator b_it; - cartesian_product(imp &i, expr *a, expr *b) - : s(i.i), i(i), a_s(s.rw, a, {}), b_s(s.rw, b, {}), a_it(a_s.begin()), b_it(b_s.begin()) {} + split_set2::iterator a_it, a_end; + split_set2::iterator b_it, b_end; + intersection(seq_rewriter& rw, split_set2 const& a_s, split_set2 const& b_s) + : a_s(a_s), b_s(b_s), + a_it(a_s.begin()), a_end(a_s.end()), + b_it(b_s.begin()), b_end(b_s.end()) {} bool at_end() const { - return a_it == a_s.end() && b_it == b_s.end(); + return (a_it == a_end && b_it == b_end) || a_it.failed() || b_it.failed(); } void next() { SASSERT(!at_end()); - if (b_it != b_s.end()) + if (b_it != b_end) ++b_it; - - if (b_it == b_s.end()) { + + if (b_it == b_end) { ++a_it; - if (a_it != a_s.end()) + if (a_it != a_end) b_it.m_imp->rewind(); } } - void consume() { - while (!at_end() && !i.has_split()) { + void consume() override { + while (!at_end() && !parent().has_split()) { auto [a1, a2] = *a_it; auto [b1, b2] = *b_it; - expr_ref a(s.rw.mk_regex_inter_normalize(a1, b1), s.m); - expr_ref b(s.rw.mk_regex_inter_normalize(a2, b2), s.m); - i.push_split(a, b); - next(); + auto a = parent().i.rw.mk_regex_inter_normalize(a1, b1); + auto b = parent().i.rw.mk_regex_inter_normalize(a2, b2); + parent().push_split(a, b); + next(); } if (b_it.failed() || a_it.failed()) - i.m_failure = true; + parent().m_failure = true; } }; @@ -80,23 +98,147 @@ struct split_set2::iterator::imp { // overrun must abort entirely: a partial fold is a strictly weaker (unsound) // split-set, since each ~sp[i] further constrains ~S. - struct complement { - split_set2::imp &s; - imp &i; - split_set2 a; - split_set2::iterator it; + struct complement : public split_set2::consumer { - complement(imp &i, expr *r) : s(i.i), i(i), a(s.rw, r, {}), it(a.begin()) {} + split_set2 a_s; + split_set2::iterator it, end; + bool m_init = false; + scoped_ptr m_intersection; + - void consume() { - while (it != a.end() && !i.has_split()) { - auto [a, b] = *it; - NOT_IMPLEMENTED_YET(); - // create a cascade of cross-products. - // empty set as a base case. - ++it; - } + complement(split_set2 const &a) : a_s(a), it(a_s.begin()), end(a_s.end()) + { } + + void init() { + if (m_init) + return; + m_init = true; + expr_ref full(parent().seq.re.mk_full_seq(parent().i.m_re_sort), parent().m); + m_intersection = nullptr; + auto &p = parent(); + while (it != end && !it.failed()) { + auto [a, b] = *it; + split_set2 A(p.i.rw, nullptr, p.i.m_threshold, p.i.m_filter); + split_set2 B(p.i.rw, nullptr, p.i.m_threshold, p.i.m_filter); + auto inter = alloc(intersection, p.i.rw, A, B); + if (m_intersection) { + m_intersection->set_parent(*inter->a_it.m_imp); + inter->a_it.m_imp->m_consumer = m_intersection.detach(); + } + else + inter->a_it.m_imp->push_split(full, full); + inter->b_it.m_imp->push_split(full, p.i.re.mk_complement(b)); + inter->b_it.m_imp->push_split(p.i.re.mk_complement(a), full); + inter->a_it.m_imp->init(); + inter->b_it.m_imp->init(); + m_intersection = inter; + ++it; + } + if (m_intersection) + m_intersection->set_parent(p); + else + p.push_split(full, full); + if (it.failed()) + p.m_failure = true; + } + + void consume() override { + init(); + if (m_intersection) + m_intersection->consume(); + } + }; + + struct non_eps : public split_set2::consumer { + ast_manager &m; + split_set2 a_s; + split_set2::iterator a_it; + non_eps(ast_manager& m, split_set2 const &a_s) : m(m), a_s(a_s), a_it(a_s.begin()) {} + + void consume() override { + while (a_it != a_s.end() && !parent().has_split()) { + auto [p, q] = *a_it; + if (parent().re.is_epsilon(q)) + continue; + parent().push_split(p, q); + } + if (a_it.failed()) + parent().m_failure = true; + } + }; + + struct concat_left : public split_set2::consumer { + split_set2 a_s; + split_set2::iterator a_it; + split_set2::iterator a_end; + expr_ref b; + concat_left(split_set2 const &a_s, expr *b) + : a_s(a_s), a_it(a_s.begin()), a_end(a_s.end()), b(b, a_s.m_imp->m) {} + + void consume() override { + while (a_it != a_end && !parent().has_split()) { + auto [p, q] = *a_it; + parent().push_split(p, parent().re.mk_concat(q, b)); + } + if (a_it.failed()) + parent().m_failure = true; + } + }; + + struct concat_right : public split_set2::consumer { + expr_ref a; + split_set2 b_s; + split_set2::iterator b_it; + split_set2::iterator b_end; + concat_right(expr* a, split_set2 const &b_s) : a(a, b_s.m_imp->m), b_s(b_s), b_it(b_s.begin()), b_end(b_s.end()) {} + + void consume() override { + while (b_it != b_end && !parent().has_split()) { + auto [p, q] = *b_it; + parent().push_split(parent().re.mk_concat(a, p), q); + } + if (b_it.failed()) + parent().m_failure = true; + } + }; + + + // TODO: can be written as a.sigma(b) u sigma(a).b filtering out eps on one union. + struct concat : split_set2::consumer { + expr_ref a, b; + split_set2 a_s, b_s; + split_set2::iterator a_it, a_end; + split_set2::iterator b_it, b_end; + concat(seq_rewriter& rw, expr *a, expr *b) + : a(a, rw.m()), b(b, rw.m()), + a_s(rw, a, {}), b_s(rw, b, {}), + a_it(a_s.begin()), a_end(a_s.end()), b_it(b_s.begin()), b_end(b_s.end()) {} + + bool at_end() const { + return a_it == a_end && b_it == b_end; + } + + void consume() override { + if (at_end()) + return; + while (!parent().has_split() && !at_end() && !a_it.failed() && !b_it.failed()) { + if (a_it == a_end) { + auto [p, q] = *b_it; + parent().push_split(parent().re.mk_concat(a, p), q); + ++b_it; + } + else { + auto [p, q] = *a_it; + if (!parent().re.is_epsilon(q)) + parent().push_split(p, parent().re.mk_concat(q, b)); + ++a_it; + } + } + if (a_it.failed() || b_it.failed()) + parent().m_failure = true; + } + }; split_set2 &s; split_set2::imp &i; @@ -105,51 +247,51 @@ struct split_set2::iterator::imp { seq_util::rex &re; expr_ref_vector m_cont; vector> m_splits; + bool m_init = false; unsigned m_qhead = 0; - scoped_ptr m_cartesian; - scoped_ptr m_complement; + scoped_ptr m_consumer; bool m_at_end; bool m_failure = false; imp(split_set2 &s, bool at_end) : s(s), i(*s.m_imp), m(i.m), seq(i.seq), re(i.re), m_cont(m), m_at_end(at_end) { - m_cont.push_back(i.r); + if (i.r) { + m_cont.push_back(i.r); + init(); + } } bool has_split() { + SASSERT(m_init); return m_qhead < m_splits.size(); } void rewind() { m_qhead = 0; - m_at_end = m_qhead < m_splits.size(); + m_at_end = m_qhead == m_splits.size(); SASSERT(m_cont.empty()); - SASSERT(!m_cartesian); - SASSERT(!m_complement); + SASSERT(!m_consumer); + } + + void init() { + if (!m_init) + next(); + m_init = true; } void next() { - m_qhead++; + m_init = true; while (!at_end()) { if (has_split()) return; - if (m_cartesian) { - m_cartesian->consume(); + if (m_consumer) { + m_consumer->consume(); if (has_split()) return; - m_cartesian = nullptr; + m_consumer = nullptr; } - - if (m_complement) { - m_complement->consume(); - if (has_split()) - return; - m_complement = nullptr; - } - if (m_cont.empty()) { m_at_end = true; return; } - // TODO: we can be strategic about choosing what to unfold, // and perform early subsumption check expr_ref last(m_cont.back(), m); @@ -159,6 +301,7 @@ struct split_set2::iterator::imp { } void push_split(expr *a, expr *b) { + expr_ref _a(a, m), _b(b, m); if (m_failure) return; if (i.m_filter && !i.m_filter(a, b)) @@ -168,7 +311,28 @@ struct split_set2::iterator::imp { if (re.get_info(b).min_length == UINT_MAX) return; // subsumption checking - m_splits.push_back({expr_ref(a, m), expr_ref(b, m)}); + for (auto const &[p, q] : m_splits) { + if (i.rw.is_subset(a, p) && i.rw.is_subset(b, q)) + return; + } + for (unsigned j = m_qhead; j < m_splits.size(); ++j) { + auto const &[p, q] = m_splits[j]; + if (i.rw.is_subset(p, a) && i.rw.is_subset(q, b)) { + m_splits[j] = {_a, _b}; + return; + } + if (a == p) { + _b = i.re.mk_union(q, _b); + m_splits[j] = {_a, _b}; + return; + } + if (b == q) { + _a = i.re.mk_union(p, _a); + m_splits[j] = {_a, _b}; + return; + } + } + m_splits.push_back({_a, _b}); if (m_splits.size() > i.m_threshold) { TRACE(seq, tout << "size of split set exceeds threshold"); m_failure = true; @@ -180,6 +344,8 @@ struct split_set2::iterator::imp { if (re.is_empty(r)) return; + SASSERT(!m_consumer); + auto mk_eps = [&]() { return expr_ref(re.mk_epsilon(i.m_seq_sort), m); }; expr *a, *b; if (re.is_union(r, a, b)) { m_cont.push_back(a); @@ -188,36 +354,45 @@ struct split_set2::iterator::imp { } if (re.is_intersection(r, a, b)) { - m_cartesian = alloc(cartesian_product, *this, a, b); + split_set2 a_s(i.rw, a, i.m_threshold, {}); + split_set2 b_s(i.rw, b, i.m_threshold, {}); + m_consumer = alloc(intersection, i.rw, a_s, b_s); + m_consumer->set_parent(*this); return; } if (re.is_complement(r, a)) { - m_complement = alloc(complement, *this, a); + split_set2 sigma_a(i.rw, a, i.m_threshold, {}); + m_consumer = alloc(complement, sigma_a); + m_consumer->set_parent(*this); return; } if (re.is_concat(r, a, b)) { - NOT_IMPLEMENTED_YET(); + m_consumer = alloc(concat, i.rw, a, b); + m_consumer->set_parent(*this); + return; } if (re.is_to_re(r, a)) { + zstring str; if (seq.str.is_concat(a, a, b)) { m_cont.push_back(re.mk_concat(re.mk_to_re(a), re.mk_to_re(b))); - return; } - if (seq.str.is_unit(a, b)) { - expr_ref eps(nullptr, m); // TODO + else if (seq.str.is_unit(a, b)) { + auto eps = mk_eps(); push_split(eps, a); push_split(a, eps); - return; } - zstring zs; - if (seq.str.is_string(a, zs)) { - // TODO - NOT_IMPLEMENTED_YET(); + else if (seq.str.is_string(a, str)) { + for (unsigned i = 0; i <= str.length(); ++i) { + const expr_ref p(re.mk_to_re(seq.str.mk_string(str.extract(0, i))), m); + const expr_ref q(re.mk_to_re(seq.str.mk_string(str.extract(i, str.length() - i))), m); + push_split(p, q); + } } - set_failure(r); + else + set_failure(r); return; } @@ -226,20 +401,40 @@ struct split_set2::iterator::imp { return; } + // star: sigma(a*) = { } cup a*.sigma(a).a* + auto add_star = [&](expr *r, expr* a) { + split_set2 sigma_a(i.rw, a, i.m_threshold, {}); + auto *c_left = alloc(concat_left, sigma_a, r); + split_set2 sigma_aa(i.rw, nullptr, i.m_threshold, {}); + auto *c_right = alloc(concat_right, r, sigma_aa); + auto &parent = *c_right->b_it.m_imp; + parent.m_consumer = c_left; + c_left->set_parent(parent); + m_consumer = c_right; + m_consumer->set_parent(*this); + }; + if (re.is_star(r, a)) { - NOT_IMPLEMENTED_YET(); + auto eps = mk_eps(); + push_split(eps, eps); + add_star(r, a); + return; } + // plus: a+ = a.a* ; sigma(a+) = a*.sigma(a).a* (star rule without ) if (re.is_plus(r, a)) { - NOT_IMPLEMENTED_YET(); + const expr_ref star(re.mk_star(a), m); // a* + add_star(star, a); + return; } if (re.is_diff(r, a, b)) { - NOT_IMPLEMENTED_YET(); + m_cont.push_back(re.mk_inter(a, re.mk_complement(b))); + return; } if (re.is_full_char(r) || re.is_range(r) || re.is_of_pred(r)) { - expr_ref eps(re.mk_epsilon(i.m_seq_sort), m); + auto eps = mk_eps(); push_split(r, eps); push_split(eps, r); return; @@ -255,7 +450,7 @@ struct split_set2::iterator::imp { } void set_failure(expr* r) { - TRACE(seq, tout << "split_set2::iterator::unfold: unhandled regex: " << mk_pp(r, m) << "\n"); + TRACE(seq, tout << "split_set::iterator::unfold: unhandled regex: " << mk_pp(r, m) << "\n"); m_failure = true; m_at_end = true; } @@ -273,6 +468,10 @@ split_set2::~split_set2() { dealloc(m_imp); } +split_set2::split_set2(split_set2 const& other) { + m_imp = alloc(imp, other.m_imp->rw, other.m_imp->r, other.m_imp->m_threshold, other.m_imp->m_filter); +} + split_set2::iterator::iterator(split_set2 const &s, bool at_end) { m_imp = alloc(imp, const_cast(s), at_end); } @@ -281,7 +480,6 @@ split_set2::iterator::~iterator() { dealloc(m_imp); } - split_set2::iterator split_set2::begin() const { return iterator(*this, false); } @@ -291,17 +489,18 @@ split_set2::iterator split_set2::end() const { } split_set2::iterator& split_set2::iterator::operator++() { + SASSERT(m_imp->m_init); + m_imp->m_qhead++; m_imp->next(); return *this; } -std::pair split_set2::iterator::operator*() const { - SASSERT(m_imp->has_split()); +std::pair split_set2::iterator::operator*() const { + SASSERT(m_imp->m_init); return m_imp->m_splits[m_imp->m_qhead]; } bool split_set2::iterator::operator==(split_set2::iterator const &other) const { - SASSERT(m_imp->at_end() || other.m_imp->at_end()); return m_imp->at_end() && other.m_imp->at_end(); } diff --git a/src/ast/rewriter/seq_split.h b/src/ast/rewriter/seq_split.h index 34f8ed8359..4df5e49014 100644 --- a/src/ast/rewriter/seq_split.h +++ b/src/ast/rewriter/seq_split.h @@ -40,14 +40,19 @@ class split_set2 { struct imp; imp *m_imp; + class consumer; + public: split_set2(seq_rewriter &rw, expr *r, unsigned threshold, split_oracle const& oracle = split_oracle()); ~split_set2(); + split_set2(split_set2 const& other); + class iterator { struct imp; imp *m_imp; + friend class consumer; public: iterator(split_set2 const& s, bool end = false); ~iterator(); diff --git a/src/cmd_context/tptp_frontend.cpp b/src/cmd_context/tptp_frontend.cpp index 0f2e686696..4dd535b765 100644 --- a/src/cmd_context/tptp_frontend.cpp +++ b/src/cmd_context/tptp_frontend.cpp @@ -1011,6 +1011,10 @@ class tptp_parser { // Table-driven prefix operator dispatch auto op_it = m_ops.find(n); if (op_it != m_ops.end() && !op_it->second.is_infix) { + if (args.empty()) { + while (accept(token_kind::at_tok)) + args.push_back(parse_at_arg()); + } return op_it->second.builder(args); } @@ -1491,6 +1495,10 @@ class tptp_parser { // Table-driven prefix operator dispatch auto op_it = m_ops.find(n); if (op_it != m_ops.end() && !op_it->second.is_infix) { + if (args.empty()) { + while (accept(token_kind::at_tok)) + args.push_back(parse_at_arg()); + } return op_it->second.builder(args); } @@ -1808,8 +1816,19 @@ class tptp_parser { expect(token_kind::rparen, "')'"); if (t.domain.empty() && is_ttype(t.range)) { - // Sort declaration: monomorphize to m_univ - m_sorts.insert_or_assign(name, m_univ); + // Sort declaration: give every declared type its own distinct uninterpreted + // sort. Collapsing all declared $tType sorts onto a single m_univ is unsound: + // a per-type constraint such as "![H:human]:H=jon" would then also constrain + // unrelated sorts (e.g. cats), turning satisfiable axiom sets into a spurious + // contradiction and reporting Theorem where the conjecture is CounterSatisfiable. + if (m_sorts.find(name) == m_sorts.end()) { + sort* s = m.mk_uninterpreted_sort(symbol(name)); + m_pinned_sorts.push_back(s); + m_sorts.emplace(name, s); + } + // A prior *use* of the name (before its declaration) already created a fresh + // sort via parse_defined_sort; keep that same sort so uses and the declaration + // agree. return; } From 361e0fba757f90377273856978130af36428b26d Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Thu, 2 Jul 2026 11:14:05 -0700 Subject: [PATCH 05/24] split-set checkpoint Signed-off-by: Nikolaj Bjorner --- src/ast/rewriter/seq_rewriter.h | 16 +- src/ast/rewriter/seq_split.cpp | 948 +++----------------------------- src/ast/rewriter/seq_split.h | 216 +------- src/smt/seq_regex.cpp | 3 + src/test/seq_split.cpp | 607 +++++++++----------- 5 files changed, 367 insertions(+), 1423 deletions(-) diff --git a/src/ast/rewriter/seq_rewriter.h b/src/ast/rewriter/seq_rewriter.h index 1781ef6f23..f83f35d1ea 100644 --- a/src/ast/rewriter/seq_rewriter.h +++ b/src/ast/rewriter/seq_rewriter.h @@ -134,7 +134,6 @@ class seq_rewriter { seq_util m_util; seq_subset m_subset; - seq_split m_split; arith_util m_autil; bool_rewriter m_br; seq::derive m_derive; @@ -334,7 +333,7 @@ class seq_rewriter { public: seq_rewriter(ast_manager & m, params_ref const & p = params_ref()): - m_util(m), m_subset(m_util.re), m_split(*this), m_autil(m), m_br(m, p), m_derive(m, *this), // m_re2aut(m), + m_util(m), m_subset(m_util.re), m_autil(m), m_br(m, p), m_derive(m, *this), // m_re2aut(m), m_op_cache(m), m_es(m), m_lhs(m), m_rhs(m) { } @@ -413,22 +412,9 @@ public: return result; } - // Split decomposition (sigma) of a regex; see seq_split.h. `oracle` (optional) - // prunes non-viable splits during generation. - bool split(expr* r, split_set& out, unsigned threshold, - const split_mode mode = split_mode::strong, split_oracle const& oracle = {}) { - return m_split.compute(r, out, threshold, mode, oracle); - } - - void simplify_split(split_set& s) { m_split.simplify(s); } bool is_subset(expr *r1, expr *r2) const; - // decompose a membership constraint into a set of pairs of regex splits - std::pair split_membership(expr* str, expr* regex, unsigned threshold, split_set& result) const { - return m_split.split_membership(str, regex, threshold, result); - } - /** * check if regular expression is of the form all ++ s ++ all ++ t + u ++ all, where, s, t, u are sequences */ diff --git a/src/ast/rewriter/seq_split.cpp b/src/ast/rewriter/seq_split.cpp index a39a14e50a..7fe237b060 100644 --- a/src/ast/rewriter/seq_split.cpp +++ b/src/ast/rewriter/seq_split.cpp @@ -18,10 +18,8 @@ Author: #include "ast/rewriter/seq_split.h" #include "ast/rewriter/seq_rewriter.h" #include "ast/ast_pp.h" -#include "util/obj_hashtable.h" -#include "util/scoped_ptr_vector.h" -struct split_set2::imp { +struct split_set::imp { ast_manager &m; seq_rewriter &rw; seq_util &seq; @@ -38,30 +36,33 @@ struct split_set2::imp { VERIFY(seq.is_re(r, m_seq_sort)); m_re_sort = r->get_sort(); } + if (m_threshold == 0) + m_threshold = UINT_MAX; } }; -class split_set2::consumer { +class split_set::consumer { protected: - split_set2::iterator::imp *ip = nullptr; + split_set::iterator::imp *ip = nullptr; public: + virtual ~consumer() = default; virtual void consume() = 0; - void set_parent(split_set2::iterator::imp &i) { + void set_parent(split_set::iterator::imp &i) { ip = &i; } - split_set2::iterator::imp &parent() { + split_set::iterator::imp &parent() { return *ip; } }; -struct split_set2::iterator::imp { - struct intersection : public split_set2::consumer { +struct split_set::iterator::imp { + struct intersection : public split_set::consumer { - split_set2 a_s, b_s; - split_set2::iterator a_it, a_end; - split_set2::iterator b_it, b_end; - intersection(seq_rewriter& rw, split_set2 const& a_s, split_set2 const& b_s) - : a_s(a_s), b_s(b_s), + split_set a_s, b_s; + split_set::iterator a_it, a_end; + split_set::iterator b_it, b_end; + intersection(seq_rewriter& rw, split_set const& a_src, split_set const& b_src) + : a_s(a_src), b_s(b_src), a_it(a_s.begin()), a_end(a_s.end()), b_it(b_s.begin()), b_end(b_s.end()) {} bool at_end() const { @@ -98,17 +99,16 @@ struct split_set2::iterator::imp { // overrun must abort entirely: a partial fold is a strictly weaker (unsound) // split-set, since each ~sp[i] further constrains ~S. - struct complement : public split_set2::consumer { + struct complement : public split_set::consumer { - split_set2 a_s; - split_set2::iterator it, end; + split_set a_s; + split_set::iterator it, end; bool m_init = false; scoped_ptr m_intersection; - complement(split_set2 const &a) : a_s(a), it(a_s.begin()), end(a_s.end()) - { - } + complement(split_set const &a) : a_s(a), it(a_s.begin()), end(a_s.end()) + { } void init() { if (m_init) @@ -119,8 +119,8 @@ struct split_set2::iterator::imp { auto &p = parent(); while (it != end && !it.failed()) { auto [a, b] = *it; - split_set2 A(p.i.rw, nullptr, p.i.m_threshold, p.i.m_filter); - split_set2 B(p.i.rw, nullptr, p.i.m_threshold, p.i.m_filter); + split_set A(p.i.rw, nullptr, p.i.m_threshold, p.i.m_filter); + split_set B(p.i.rw, nullptr, p.i.m_threshold, p.i.m_filter); auto inter = alloc(intersection, p.i.rw, A, B); if (m_intersection) { m_intersection->set_parent(*inter->a_it.m_imp); @@ -128,8 +128,8 @@ struct split_set2::iterator::imp { } else inter->a_it.m_imp->push_split(full, full); - inter->b_it.m_imp->push_split(full, p.i.re.mk_complement(b)); - inter->b_it.m_imp->push_split(p.i.re.mk_complement(a), full); + inter->b_it.m_imp->push_split(full, p.i.rw.mk_complement(b)); + inter->b_it.m_imp->push_split(p.i.rw.mk_complement(a), full); inter->a_it.m_imp->init(); inter->b_it.m_imp->init(); m_intersection = inter; @@ -150,53 +150,37 @@ struct split_set2::iterator::imp { } }; - struct non_eps : public split_set2::consumer { - ast_manager &m; - split_set2 a_s; - split_set2::iterator a_it; - non_eps(ast_manager& m, split_set2 const &a_s) : m(m), a_s(a_s), a_it(a_s.begin()) {} - - void consume() override { - while (a_it != a_s.end() && !parent().has_split()) { - auto [p, q] = *a_it; - if (parent().re.is_epsilon(q)) - continue; - parent().push_split(p, q); - } - if (a_it.failed()) - parent().m_failure = true; - } - }; - - struct concat_left : public split_set2::consumer { - split_set2 a_s; - split_set2::iterator a_it; - split_set2::iterator a_end; + struct concat_left : public split_set::consumer { + split_set a_s; + split_set::iterator a_it; + split_set::iterator a_end; expr_ref b; - concat_left(split_set2 const &a_s, expr *b) - : a_s(a_s), a_it(a_s.begin()), a_end(a_s.end()), b(b, a_s.m_imp->m) {} + concat_left(split_set const &a_src, expr *b) + : a_s(a_src), a_it(a_s.begin()), a_end(a_s.end()), b(b, a_s.m_imp->m) {} void consume() override { while (a_it != a_end && !parent().has_split()) { auto [p, q] = *a_it; - parent().push_split(p, parent().re.mk_concat(q, b)); + parent().push_split(p, parent().i.rw.mk_re_append(q, b)); + ++a_it; } if (a_it.failed()) parent().m_failure = true; } }; - struct concat_right : public split_set2::consumer { + struct concat_right : public split_set::consumer { expr_ref a; - split_set2 b_s; - split_set2::iterator b_it; - split_set2::iterator b_end; - concat_right(expr* a, split_set2 const &b_s) : a(a, b_s.m_imp->m), b_s(b_s), b_it(b_s.begin()), b_end(b_s.end()) {} + split_set b_s; + split_set::iterator b_it; + split_set::iterator b_end; + concat_right(expr* a, split_set const &b_src) : a(a, b_src.m_imp->m), b_s(b_src), b_it(b_s.begin()), b_end(b_s.end()) {} void consume() override { while (b_it != b_end && !parent().has_split()) { auto [p, q] = *b_it; - parent().push_split(parent().re.mk_concat(a, p), q); + parent().push_split(parent().i.rw.mk_re_append(a, p), q); + ++b_it; } if (b_it.failed()) parent().m_failure = true; @@ -205,14 +189,14 @@ struct split_set2::iterator::imp { // TODO: can be written as a.sigma(b) u sigma(a).b filtering out eps on one union. - struct concat : split_set2::consumer { + struct concat : split_set::consumer { expr_ref a, b; - split_set2 a_s, b_s; - split_set2::iterator a_it, a_end; - split_set2::iterator b_it, b_end; - concat(seq_rewriter& rw, expr *a, expr *b) + split_set a_s, b_s; + split_set::iterator a_it, a_end; + split_set::iterator b_it, b_end; + concat(seq_rewriter& rw, expr *a, expr *b, unsigned threshold) : a(a, rw.m()), b(b, rw.m()), - a_s(rw, a, {}), b_s(rw, b, {}), + a_s(rw, a, threshold, {}), b_s(rw, b, threshold, {}), a_it(a_s.begin()), a_end(a_s.end()), b_it(b_s.begin()), b_end(b_s.end()) {} bool at_end() const { @@ -225,13 +209,13 @@ struct split_set2::iterator::imp { while (!parent().has_split() && !at_end() && !a_it.failed() && !b_it.failed()) { if (a_it == a_end) { auto [p, q] = *b_it; - parent().push_split(parent().re.mk_concat(a, p), q); + parent().push_split(parent().i.rw.mk_re_append(a, p), q); ++b_it; } else { auto [p, q] = *a_it; if (!parent().re.is_epsilon(q)) - parent().push_split(p, parent().re.mk_concat(q, b)); + parent().push_split(p, parent().i.rw.mk_re_append(q, b)); ++a_it; } } @@ -240,8 +224,8 @@ struct split_set2::iterator::imp { } }; - split_set2 &s; - split_set2::imp &i; + split_set &s; + split_set::imp &i; ast_manager &m; seq_util &seq; seq_util::rex &re; @@ -249,10 +233,10 @@ struct split_set2::iterator::imp { vector> m_splits; bool m_init = false; unsigned m_qhead = 0; - scoped_ptr m_consumer; + scoped_ptr m_consumer; bool m_at_end; bool m_failure = false; - imp(split_set2 &s, bool at_end) : s(s), i(*s.m_imp), m(i.m), seq(i.seq), re(i.re), m_cont(m), m_at_end(at_end) { + imp(split_set &s, bool at_end) : s(s), i(*s.m_imp), m(i.m), seq(i.seq), re(i.re), m_cont(m), m_at_end(at_end) { if (i.r) { m_cont.push_back(i.r); init(); @@ -300,12 +284,15 @@ struct split_set2::iterator::imp { } } - void push_split(expr *a, expr *b) { - expr_ref _a(a, m), _b(b, m); + void push_split(expr *_a, expr *_b) { + expr_ref a(_a, m), b(_b, m); + if (m_failure) return; if (i.m_filter && !i.m_filter(a, b)) return; + if (re.is_empty(a) || re.is_empty(b)) + return; if (re.get_info(a).min_length == UINT_MAX) return; if (re.get_info(b).min_length == UINT_MAX) @@ -318,21 +305,22 @@ struct split_set2::iterator::imp { for (unsigned j = m_qhead; j < m_splits.size(); ++j) { auto const &[p, q] = m_splits[j]; if (i.rw.is_subset(p, a) && i.rw.is_subset(q, b)) { - m_splits[j] = {_a, _b}; + m_splits[j] = {a, b}; return; } if (a == p) { - _b = i.re.mk_union(q, _b); - m_splits[j] = {_a, _b}; + b = i.rw.mk_union(q, b); + m_splits[j] = {a, b}; return; } if (b == q) { - _a = i.re.mk_union(p, _a); - m_splits[j] = {_a, _b}; + a = i.rw.mk_union(p, a); + m_splits[j] = {a, b}; return; } } - m_splits.push_back({_a, _b}); + TRACE(seq, tout << "push <" << a << ", " << b << ">\n"); + m_splits.push_back({a, b}); if (m_splits.size() > i.m_threshold) { TRACE(seq, tout << "size of split set exceeds threshold"); m_failure = true; @@ -354,22 +342,22 @@ struct split_set2::iterator::imp { } if (re.is_intersection(r, a, b)) { - split_set2 a_s(i.rw, a, i.m_threshold, {}); - split_set2 b_s(i.rw, b, i.m_threshold, {}); + split_set a_s(i.rw, a, i.m_threshold, {}); + split_set b_s(i.rw, b, i.m_threshold, {}); m_consumer = alloc(intersection, i.rw, a_s, b_s); m_consumer->set_parent(*this); return; } if (re.is_complement(r, a)) { - split_set2 sigma_a(i.rw, a, i.m_threshold, {}); + split_set sigma_a(i.rw, a, i.m_threshold, {}); m_consumer = alloc(complement, sigma_a); m_consumer->set_parent(*this); return; } if (re.is_concat(r, a, b)) { - m_consumer = alloc(concat, i.rw, a, b); + m_consumer = alloc(concat, i.rw, a, b, i.m_threshold); m_consumer->set_parent(*this); return; } @@ -403,13 +391,14 @@ struct split_set2::iterator::imp { // star: sigma(a*) = { } cup a*.sigma(a).a* auto add_star = [&](expr *r, expr* a) { - split_set2 sigma_a(i.rw, a, i.m_threshold, {}); + split_set sigma_a(i.rw, a, i.m_threshold, {}); auto *c_left = alloc(concat_left, sigma_a, r); - split_set2 sigma_aa(i.rw, nullptr, i.m_threshold, {}); + split_set sigma_aa(i.rw, nullptr, i.m_threshold, {}); auto *c_right = alloc(concat_right, r, sigma_aa); auto &parent = *c_right->b_it.m_imp; parent.m_consumer = c_left; - c_left->set_parent(parent); + c_left->set_parent(parent); + parent.init(); m_consumer = c_right; m_consumer->set_parent(*this); }; @@ -429,7 +418,7 @@ struct split_set2::iterator::imp { } if (re.is_diff(r, a, b)) { - m_cont.push_back(re.mk_inter(a, re.mk_complement(b))); + m_cont.push_back(i.rw.mk_inter(a, i.rw.mk_complement(b))); return; } @@ -460,819 +449,50 @@ struct split_set2::iterator::imp { } }; -split_set2::split_set2(seq_rewriter &rw, expr *r, unsigned threshold, split_oracle const &oracle) { +split_set::split_set(seq_rewriter &rw, expr *r, unsigned threshold, split_oracle const &oracle) { m_imp = alloc(imp, rw, r, threshold, oracle); } -split_set2::~split_set2() { +split_set::~split_set() { dealloc(m_imp); } -split_set2::split_set2(split_set2 const& other) { +split_set::split_set(split_set const& other) { m_imp = alloc(imp, other.m_imp->rw, other.m_imp->r, other.m_imp->m_threshold, other.m_imp->m_filter); } -split_set2::iterator::iterator(split_set2 const &s, bool at_end) { - m_imp = alloc(imp, const_cast(s), at_end); +split_set::iterator::iterator(split_set const &s, bool at_end) { + m_imp = alloc(imp, const_cast(s), at_end); } -split_set2::iterator::~iterator() { +split_set::iterator::~iterator() { dealloc(m_imp); } -split_set2::iterator split_set2::begin() const { +split_set::iterator split_set::begin() const { return iterator(*this, false); } -split_set2::iterator split_set2::end() const { +split_set::iterator split_set::end() const { return iterator(*this, true); } -split_set2::iterator& split_set2::iterator::operator++() { +split_set::iterator& split_set::iterator::operator++() { SASSERT(m_imp->m_init); m_imp->m_qhead++; m_imp->next(); return *this; } -std::pair split_set2::iterator::operator*() const { +std::pair split_set::iterator::operator*() const { SASSERT(m_imp->m_init); return m_imp->m_splits[m_imp->m_qhead]; } -bool split_set2::iterator::operator==(split_set2::iterator const &other) const { +bool split_set::iterator::operator==(split_set::iterator const &other) const { return m_imp->at_end() && other.m_imp->at_end(); } -bool split_set2::iterator::failed() const { +bool split_set::iterator::failed() const { return m_imp->m_failure; } - -seq_split::seq_split(seq_rewriter& rw) : - m(rw.m()), m_rw(rw), m_subset(rw.u().re), - m_set_sort(m), - m_d_empty(m), m_d_single(m), m_d_fromre(m), m_d_union(m), - m_d_inter(m), m_d_compl(m), m_d_lcat(m), m_d_rcat(m), - m_empty_app(m) {} - -// --------------------------------------------------------------------------- -// Suspended split-set representation (split algebra over `expr`). -// --------------------------------------------------------------------------- - -void seq_split::ensure_decls(sort* seq_sort) { - SASSERT(seq_sort); - if (m_seq_sort == seq_sort) - return; - sort* re_sort = re().mk_re(seq_sort); - m_set_sort = m.mk_uninterpreted_sort(symbol("seq.split.set")); - sort* ss = m_set_sort; - m_d_empty = m.mk_func_decl(symbol("seq.split.empty"), 0u, nullptr, ss); - m_d_single = m.mk_func_decl(symbol("seq.split.single"), re_sort, re_sort, ss); - m_d_fromre = m.mk_func_decl(symbol("seq.split.from_re"), re_sort, ss); - m_d_union = m.mk_func_decl(symbol("seq.split.union"), ss, ss, ss); - m_d_inter = m.mk_func_decl(symbol("seq.split.inter"), ss, ss, ss); - m_d_compl = m.mk_func_decl(symbol("seq.split.compl"), ss, ss); - m_d_lcat = m.mk_func_decl(symbol("seq.split.lcat"), re_sort, ss, ss); - m_d_rcat = m.mk_func_decl(symbol("seq.split.rcat"), ss, re_sort, ss); - m_empty_app = m.mk_const(m_d_empty); - m_seq_sort = seq_sort; -} - -// --- smart constructors ---------------------------------------------------- - -expr_ref seq_split::mk_empty() { - SASSERT(m_empty_app); - return m_empty_app; -} - -expr_ref seq_split::mk_single(expr* d, expr* n) { - SASSERT(d && n); - if (re().is_empty(d) || re().is_empty(n)) - return mk_empty(); - return expr_ref(m.mk_app(m_d_single, d, n), m); -} - -expr_ref seq_split::mk_fromre(expr* r) { - SASSERT(r); - sort* seq_sort = nullptr; - VERIFY(seq().is_re(r, seq_sort)); - ensure_decls(seq_sort); - if (re().is_empty(r)) - return mk_empty(); - return expr_ref(m.mk_app(m_d_fromre, r), m); -} - -expr_ref seq_split::mk_union(expr* a, expr* b) { - SASSERT(a && b); - if (is_empty_ss(a)) - return expr_ref(b, m); - if (is_empty_ss(b)) - return expr_ref(a, m); - return expr_ref(m.mk_app(m_d_union, a, b), m); -} - -expr_ref seq_split::mk_inter(expr* a, expr* b) { - SASSERT(a && b); - if (is_empty_ss(a) || is_empty_ss(b)) - return mk_empty(); - return expr_ref(m.mk_app(m_d_inter, a, b), m); -} - -expr_ref seq_split::mk_compl(expr* a) { - SASSERT(a); - return expr_ref(m.mk_app(m_d_compl, a), m); -} - -expr_ref seq_split::mk_lcat(expr* r, expr* s) { - SASSERT(r && s); - if (is_empty_ss(s)) - return mk_empty(); - if (re().is_epsilon(r)) // eps . S = S - return expr_ref(s, m); - return expr_ref(m.mk_app(m_d_lcat, r, s), m); -} - -expr_ref seq_split::mk_rcat(expr* s, expr* r) { - SASSERT(r && s); - if (is_empty_ss(s)) - return mk_empty(); - if (re().is_epsilon(r)) // S . eps = S - return expr_ref(s, m); - return expr_ref(m.mk_app(m_d_rcat, s, r), m); -} - -// --- recognizers ----------------------------------------------------------- - -bool seq_split::is_empty_ss(expr* e) const { - return is_app(e) && to_app(e)->get_decl() == m_d_empty; -} - -bool seq_split::is_app1(expr* e, func_decl* d, expr*& a) const { - if (is_app(e) && to_app(e)->get_decl() == d) { - a = to_app(e)->get_arg(0); - return true; - } - return false; -} - -bool seq_split::is_app2(expr *e, func_decl *d, expr *&a, expr *&b) const { - if (is_app(e) && to_app(e)->get_decl() == d) { - a = to_app(e)->get_arg(0); - b = to_app(e)->get_arg(1); - return true; - } - return false; -} - -bool seq_split::is_frontier(expr* e) const { - expr *a = nullptr, *b = nullptr; - return is_empty_ss(e) || is_single(e, a, b) || is_union(e, a, b); -} - -seq_util& seq_split::seq() const { return m_rw.u(); } -seq_util::rex& seq_split::re() const { return m_rw.u().re; } - -// Add unless the (optional) lookahead oracle prunes it. -void seq_split::push(split_set& out, split_oracle const& oracle, expr* d, expr* n) const { - if (!oracle || oracle(d, n)) - out.push_back(split_pair(d, n, m)); -} - -// Cross-product intersection of two split-sets (split algebra): -// S1 cap S2 = { | in S1, in S2 }. -// Pairs where any component is bottom (the empty regex) are dropped. -bool seq_split::intersect(split_set const& s1, split_set const& s2, split_set& result, - unsigned threshold, split_oracle const& oracle) const { - const seq_util::rex& r = re(); - for (auto const& p1 : s1) { - for (auto const& p2 : s2) { - if (r.is_empty(p1.m_d) || r.is_empty(p2.m_d) || - r.is_empty(p1.m_n) || r.is_empty(p2.m_n)) - continue; - 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); - push(result, oracle, di, ni); - if (result.size() > threshold) - return false; - } - } - return true; -} - -// Complement of a split-set via De Morgan: ~S = cap_{s in S} ~s with -// ~ = { <~D, .*>, <.*, ~N> } and ~{} = { <.*, .*> }. -// May produce up to 2^|sp| pairs (bounded by the threshold). A threshold -// overrun must abort entirely: a partial fold is a strictly weaker (unsound) -// split-set, since each ~sp[i] further constrains ~S. -bool seq_split::complement(sort* seq_sort, split_set const& sp, split_set& result, - const unsigned threshold, split_oracle const& oracle) const { - - seq_util::rex& r = re(); - sort* re_sort = r.mk_re(seq_sort); - const expr_ref full(r.mk_full_seq(re_sort), m); // .* - if (sp.empty()) { // ~{} = <.*, .*> - push(result, oracle, full, full); - return true; - } - // The acc/next pairs carry genuine output-orientation N components (the De - // Morgan ~ = {<~D,.*>, <.*,~N>}), so the oracle prunes them soundly and - // keeps the 2^|sp| fold from blowing up. - split_set acc; - push(acc, oracle, r.mk_complement(sp[0].m_d), full); - push(acc, oracle, full, r.mk_complement(sp[0].m_n)); - for (unsigned i = 1; i < sp.size(); ++i) { - split_set next; - push(next, oracle, r.mk_complement(sp[i].m_d), full); - push(next, oracle, full, r.mk_complement(sp[i].m_n)); - split_set tmp; - if (!intersect(acc, next, tmp, threshold, oracle)) - return false; - acc = std::move(tmp); - if (acc.empty()) // intersection empty => ~S is empty - break; - if (acc.size() > threshold) - return false; - } - result.append(acc); - return true; -} - -// One level of the sigma rules. Mirrors the historic eager `compute`, except it -// emits *suspended* split-algebra terms (from_re / lcat / rcat / inter / compl) for -// the subterms instead of recursing. `mode` is irrelevant here: weak vs. strong is -// decided when `head_normalize` reaches an inter / compl node. -expr_ref seq_split::expand_fromre(expr* r, bool& ok) { - ok = true; - seq_util& sq = seq(); - seq_util::rex& rex = re(); - - sort* seq_sort = nullptr; - if (!sq.is_re(r, seq_sort)) { - ok = false; - return expr_ref(m); - } - ensure_decls(seq_sort); - - // bottom: sigma(empty) = {} - if (rex.is_empty(r)) - return mk_empty(); - - // epsilon: sigma(eps) = { } - if (rex.is_epsilon(r)) { - const expr_ref eps(rex.mk_epsilon(seq_sort), m); - return mk_single(eps, eps); - } - - expr* a = nullptr, *b = nullptr; - - // to_re(s): split the literal word s at every position. - expr* s = nullptr; - if (rex.is_to_re(r, s)) { - zstring str; - vector stack; - stack.push_back(s); - - while (!stack.empty()) { - expr* cur = stack.back(); - stack.pop_back(); - if (seq().str.is_concat(cur, a, b)) { - stack.push_back(b); - stack.push_back(a); - } - else { - expr* ch; - unsigned cv; - if (seq().str.is_unit(cur, ch) && seq().is_const_char(ch, cv)) { - str += zstring(cv); - continue; - } - zstring str2; - if (sq.str.is_string(s, str2)) { - str = str2; - continue; - } - // not a constant string; unsupported for now - ok = false; - return expr_ref(m); - } - } - expr_ref acc = mk_empty(); - for (unsigned i = 0; i <= str.length(); ++i) { - const expr_ref p(rex.mk_to_re(sq.str.mk_string(str.extract(0, i))), m); - const expr_ref q(rex.mk_to_re(sq.str.mk_string(str.extract(i, str.length() - i))), m); - acc = mk_union(acc, mk_single(p, q)); - } - return acc; - } - - // single-character class alpha (., [lo-hi], of_pred): - // sigma(alpha) = { , } - if (rex.is_full_char(r) || rex.is_range(r) || rex.is_of_pred(r)) { - const expr_ref ex(r, m); - const expr_ref eps(rex.mk_epsilon(seq_sort), m); - return mk_union(mk_single(eps, ex), mk_single(ex, eps)); - } - - // .* : sigma(.*) = { <.*, .*> } - if (rex.is_full_seq(r)) { - const expr_ref ex(r, m); - return mk_single(ex, ex); - } - - // union: sigma(r0 | ... | r_{n-1}) = U from_re(ri) (re.union may be n-ary) - if (rex.is_union(r)) { - app* ap = to_app(r); - expr_ref acc = mk_empty(); - for (expr* arg : *ap) { - acc = mk_union(acc, mk_fromre(arg)); - } - return acc; - } - - // concat: sigma(r0...r_{n-1}) = U_i (r0...r_{i-1}) . sigma(ri) . (r_{i+1}...r_{n-1}) - // emitted as U_i lcat(left, rcat(from_re(ri), right)) (re.++ may be n-ary) - if (rex.is_concat(r)) { - app* ap = to_app(r); - const unsigned n = ap->get_num_args(); - expr_ref acc = mk_empty(); - for (unsigned i = 0; i < n; ++i) { - expr_ref left(m), right(m); - if (i == 0) - left = rex.mk_epsilon(seq_sort); - else { - for (unsigned j = 0; j < i; ++j) { - expr* arg = ap->get_arg(j); - left = left ? expr_ref(rex.mk_concat(left, arg), m) : expr_ref(arg, m); - } - } - if (i == n - 1) - right = rex.mk_epsilon(seq_sort); - else { - right = ap->get_arg(i + 1); - for (unsigned j = i + 2; j < n; ++j) { - expr* arg = ap->get_arg(j); - right = rex.mk_concat(right, arg); - } - } - expr_ref term = mk_lcat(left, mk_rcat(mk_fromre(ap->get_arg(i)), right)); - acc = mk_union(acc, term); - } - return acc; - } - - // star: sigma(a*) = { } cup a*.sigma(a).a* - if (rex.is_star(r, a)) { - const expr_ref eps(rex.mk_epsilon(seq_sort), m); - expr_ref body = mk_lcat(r, mk_rcat(mk_fromre(a), r)); // a*.from_re(a).a* - return mk_union(mk_single(eps, eps), body); - } - - // plus: a+ = a.a* ; sigma(a+) = a*.sigma(a).a* (star rule without ) - if (rex.is_plus(r, a)) { - const expr_ref star(rex.mk_star(a), m); // a* - return mk_lcat(star, mk_rcat(mk_fromre(a), star)); - } - - // intersection: sigma(r0 & ... & r_{n-1}) = cap from_re(ri) (re.inter may be n-ary) - if (rex.is_intersection(r)) { - app* ap = to_app(r); - const unsigned n = ap->get_num_args(); - expr_ref acc = mk_fromre(ap->get_arg(0)); - for (unsigned i = 1; i < n; ++i) - acc = mk_inter(acc, mk_fromre(ap->get_arg(i))); - return acc; - } - - // complement: sigma(~a) = ~sigma(a). - if (rex.is_complement(r, a)) - return mk_compl(mk_fromre(a)); - - // difference: a \ b = a & ~b ; sigma(a \ b) = sigma(a) cap ~sigma(b). - if (rex.is_diff(r, a, b)) - return mk_inter(mk_fromre(a), mk_compl(mk_fromre(b))); - - // bounded loop / ite / other: not handled (paper "v1: bail"). - TRACE(seq, tout << "seq_split: unsupported regex " << mk_pp(r, m) << "\n";); - ok = false; - return expr_ref(m); -} - -// r . hs : push the left regex onto the D component of a head-normal split-set. -expr_ref seq_split::distribute_lcat(expr* r, expr* hs) { - expr *a = nullptr, *b = nullptr, *d = nullptr, *n = nullptr; - if (is_empty_ss(hs)) - return mk_empty(); - if (is_single(hs, d, n)) - return mk_single(m_rw.mk_re_append(r, d), n); // r.D - if (is_union(hs, a, b)) - return mk_union(mk_lcat(r, a), mk_lcat(r, b)); - UNREACHABLE(); - return expr_ref(hs, m); -} - -// hs . r : push the right regex onto the N component of a head-normal split-set. -expr_ref seq_split::distribute_rcat(expr* hs, expr* r) { - expr *a = nullptr, *b = nullptr, *d = nullptr, *n = nullptr; - if (is_empty_ss(hs)) - return mk_empty(); - if (is_single(hs, d, n)) - return mk_single(d, m_rw.mk_re_append(n, r)); // N.r - if (is_union(hs, a, b)) - return mk_union(mk_rcat(a, r), mk_rcat(b, r)); - UNREACHABLE(); - return expr_ref(hs, m); -} - -expr_ref seq_split::from_split_set(split_set const& s) { - expr_ref acc = mk_empty(); - for (auto const& p : s) - acc = mk_union(acc, mk_single(p.m_d, p.m_n)); - return acc; -} - -expr_ref seq_split::head_normalize(expr* t, split_mode mode, unsigned threshold, - split_oracle const& oracle, bool& ok) { - ok = true; - expr *a = nullptr, *b = nullptr, *r = nullptr, *s = nullptr; - - // already a frontier node - if (is_frontier(t)) - return expr_ref(t, m); - - // from_re(r): one level of sigma; recurse to settle a non-frontier head - // (plus / inter / compl / diff expand to lcat / inter / compl nodes). - if (is_fromre(t, r)) { - expr_ref e = expand_fromre(r, ok); - if (!ok) - return expr_ref(m); - if (is_frontier(e)) - return e; - return head_normalize(e, mode, threshold, oracle, ok); - } - - // r.S : head-normalize S, then distribute r over the frontier. - if (is_lcat(t, r, s)) { - expr_ref hs = head_normalize(s, mode, threshold, oracle, ok); - if (!ok) - return expr_ref(m); - return distribute_lcat(r, hs); - } - if (is_rcat(t, s, r)) { - expr_ref hs = head_normalize(s, mode, threshold, oracle, ok); - if (!ok) - return expr_ref(m); - return distribute_rcat(hs, r); - } - - // inter / compl are eager by nature: a single split of S1 cap S2 (or ~S) - // cannot be produced without materializing the operand split-sets. - if (is_inter(t, a, b)) { - if (mode == split_mode::weak) { - ok = false; - return expr_ref(m); - } - split_set sa, sb, tmp; - if (!materialize(a, mode, threshold, oracle, sa) || - !materialize(b, mode, threshold, oracle, sb) || - !intersect(sa, sb, tmp, threshold, oracle)) { - ok = false; - return expr_ref(m); - } - return from_split_set(tmp); - } - if (is_compl(t, a)) { - if (mode == split_mode::weak) { - ok = false; - return expr_ref(m); - } - // The body is materialized WITHOUT the oracle (its pairs are inverted, so - // their N is unrelated to the output N); the oracle is re-applied in - // complement(). - split_set sa, res; - if (!materialize(a, mode, threshold, split_oracle{}, sa) || - !complement(m_seq_sort, sa, res, threshold, oracle)) { - ok = false; - return expr_ref(m); - } - return from_split_set(res); - } - - UNREACHABLE(); - ok = false; - return expr_ref(m); -} - -bool seq_split::materialize(expr* node, split_mode mode, unsigned threshold, - split_oracle const& oracle, split_set& out) { - iterator it(*this, node, mode, threshold, oracle); - expr_ref d(m), n(m); - while (it.next(d, n)) - out.push_back(split_pair(d, n, m)); - return !it.gave_up(); -} - -expr_ref seq_split::make(expr* r) { - SASSERT(r); - sort* seq_sort = nullptr; - if (!seq().is_re(r, seq_sort)) - return expr_ref(m); - return mk_fromre(r); -} - -// --- Lazy enumerator -------------------------------------------------------- -// The worklist holds suspended split-sets. Each next() pops a node, head- -// normalizes it to a frontier (empty | single | union), and either returns the -// single split, pushes the two union branches back, or skips an empty. All the -// expansion work happens lazily, one split per next() call. - -seq_split::iterator::iterator(seq_split& engine, expr* node, split_mode mode, - unsigned threshold, split_oracle oracle) : - m_engine(engine), m(engine.m), m_mode(mode), m_threshold(threshold), - m_oracle(std::move(oracle)), m_work(engine.m) { - SASSERT(node); - m_work.push_back(node); -} - -bool seq_split::iterator::next(expr_ref& out_d, expr_ref& out_n) { - if (m_giveup) - return false; // a prior give-up is sticky - while (!m_work.empty()) { - expr_ref t(m_work.back(), m); - m_work.pop_back(); - - bool ok = true; - expr_ref hn = m_engine.head_normalize(t, m_mode, m_threshold, m_oracle, ok); - if (!ok) { - m_giveup = true; // unsupported / weak Boolean / overrun - return false; - } - - expr *a = nullptr, *b = nullptr, *d = nullptr, *n = nullptr; - if (m_engine.is_empty_ss(hn)) - continue; - if (m_engine.is_single(hn, d, n)) { - if (m_oracle && !m_oracle(d, n)) - continue; // pruned by lookahead - if (++m_count > m_threshold) { - m_giveup = true; // safety cap against space bloat - return false; - } - out_d = d; - out_n = n; - return true; - } - if (m_engine.is_union(hn, a, b)) { - m_work.push_back(a); - m_work.push_back(b); - continue; - } - UNREACHABLE(); - } - return false; // exhausted (m_giveup stays false) -} - -seq_split::iterator seq_split::iterate(expr* node, split_mode mode, unsigned threshold, - split_oracle const& oracle) { - return iterator(*this, node, mode, threshold, oracle); -} - -// Eager wrapper: drain the lazy enumeration into `out`. Semantics (give-up cases, -// oracle discipline) match the historic engine. -bool seq_split::compute(expr* r, split_set& result, unsigned threshold, split_mode mode, - split_oracle const& oracle) { - SASSERT(r); - sort* seq_sort = nullptr; - if (!seq().is_re(r, seq_sort)) - return false; - expr_ref node = mk_fromre(r); - return materialize(node, mode, threshold, oracle, result); -} - -// same-D / same-N merge (paper eqs. 1 & 2): -// { , } -> (by_left = true, group by D) -// { , } -> (by_left = false, group by N) -// Only fires on syntactically-identical (perfectly-shared) key components, so -// it is a conservative instance of the rule. -void seq_split::merge_by(split_set& pairs, const bool by_left) const { - obj_map idx; // key component -> position in `out` - split_set out; - for (auto const& p : pairs) { - expr* key = by_left ? p.m_d.get() : p.m_n.get(); - expr* other = by_left ? p.m_n.get() : p.m_d.get(); - unsigned pos; - if (idx.find(key, pos)) { - expr* prev = by_left ? out[pos].m_n.get() : out[pos].m_d.get(); - const expr_ref u(m_rw.mk_regex_union_normalize(prev, other), m); - if (by_left) - out[pos].m_n = u; - else - out[pos].m_d = u; - } - else { - idx.insert(key, out.size()); - out.push_back(p); - } - } - pairs.swap(out); -} - -void seq_split::simplify(split_set& pairs) const { - seq_util::rex& r = re(); - - // 1. drop pairs with a bottom (empty-language) component. - unsigned w = 0; - for (unsigned i = 0; i < pairs.size(); ++i) { - if (r.is_empty(pairs[i].m_d) || r.is_empty(pairs[i].m_n)) - continue; - if (w != i) - pairs[w] = pairs[i]; - ++w; - } - pairs.shrink(w); - if (pairs.size() <= 1) - return; - - // 2. same-D / same-N merge rules. - merge_by(pairs, true); - merge_by(pairs, false); - if (pairs.size() <= 1) - return; - - // 3. subsumption: drop when L(D_i) subseteq L(D_j) and - // L(N_i) subseteq L(N_j) for some kept j. seq_subset is conservative - // (returns true only for definite containment), so we never drop a - // needed split. - //if (pairs.size() > 64) - // return; - - struct row { expr* d; expr* n; unsigned idx; }; - vector rows; - for (unsigned i = 0; i < pairs.size(); ++i) - rows.push_back({ pairs[i].m_d.get(), pairs[i].m_n.get(), i }); - - auto subsumes = [&](row const& a, row const& b) { - return m_subset.is_subset(b.d, a.d) && m_subset.is_subset(b.n, a.n); - }; - - vector kept; - for (row const& row_r : rows) { - bool redundant = false; - for (row const& k : kept) - if (subsumes(k, row_r)) { redundant = true; break; } - if (redundant) - continue; - // drop already-kept rows strictly subsumed by row_r - unsigned kw = 0; - for (unsigned t = 0; t < kept.size(); ++t) { - if (subsumes(row_r, kept[t])) - continue; - kept[kw++] = kept[t]; - } - kept.shrink(kw); - kept.push_back(row_r); - } - - split_set result; - for (row const& k : kept) - result.push_back(pairs[k.idx]); - pairs.swap(result); -} - -std::pair seq_split::split_membership(expr* str, expr* regex, unsigned threshold, split_set& result) const { - expr_ref_vector tokens(m); - vector stack; - stack.push_back(str); - - while (!stack.empty()) { - expr* cur = stack.back(); - stack.pop_back(); - expr* l, *r; - if (seq().str.is_concat(cur, l, r)) { - stack.push_back(r); - stack.push_back(l); - } - else - tokens.push_back(expr_ref(cur, m)); - } - - expr* ch; - unsigned i = 0; - - while (i < tokens.size() && (seq().str.is_string(tokens.get(i)) || (seq().str.is_unit(tokens.get(i), ch) && seq().is_const_char(ch)))) { - zstring s; - if (seq().str.is_string(tokens.get(i), s)) { - if (s.empty()) { - i++; - continue; - } - ch = seq().mk_char(s[0]); - tokens[i] = seq().str.mk_string(s.extract(1, s.length() - 1)); - } - else - i++; - regex = m_rw.mk_derivative(ch, regex); - } - - if (i > 0) { - unsigned j = 0; - for (; i < tokens.size(); i++, j++) { - tokens[j] = tokens.get(i); - } - tokens.shrink(j); - } - - // TODO: Do this for the back as well (also, why did no rule before do that?) - - if (tokens.empty()) - return { expr_ref(m), expr_ref(m) }; - - // Choose the factorization boundary so the tail starts with the - // longest run of concrete characters c. - // This gives the split-engine lookahead oracle the most pruning information. - // head = u' (tokens before the run), tail = c · u''' (tokens from the run onward). - const unsigned total = tokens.size(); - unsigned run_start = 0, run_len = 0; - for (i = 1; i < total; ) { - if (!(seq().str.is_unit(tokens.get(i), ch) && seq().is_const_char(ch))) { - i++; - continue; - } - unsigned j = i; - while (j < total && seq().str.is_unit(tokens.get(j), ch) && seq().is_const_char(ch)) { - j++; - } - if (j - i > run_len) { - run_len = j - i; - run_start = i; - } - i = j; - } - // No constant run => fall back to splitting off the first token. - const unsigned p = run_len == 0 ? 1 : run_start; - SASSERT(p >= 1); - expr* head = tokens.get(0); - for (i = 1; i < p; i++) { - head = seq().str.mk_concat(head, tokens.get(i)); - } - expr* tail = seq().str.mk_empty(head->get_sort()); - if (tokens.size() > p + run_len) { - tail = tokens.get(p + run_len); - for (i = p + run_len + 1; i < tokens.size(); i++) { - tail = seq().str.mk_concat(tail, tokens.get(i)); - } - } - SASSERT(head && tail); - - // Build the constant lookahead c and (if non-empty) an oracle that - // prunes splits whose postfix cannot match c. - zstring c; - for (i = 0; i < run_len; ++i) { - unsigned cv; - VERIFY(seq().str.is_unit(tokens.get(run_start + i), ch)); - VERIFY(seq().is_const_char(ch, cv)); - c = c + zstring(cv); - } - split_oracle oracle; - if (!c.empty()) - oracle = [this, &c](expr*, expr* n) { return split_lookahead_viable(n, c); }; - - // Decompose the regex into a split-set via the shared seq_split engine - if (!m_rw.split(regex, result, threshold, split_mode::strong, oracle)) { - result.clear(); - return { expr_ref(m), expr_ref(m) }; - } - - simplify(result); - - // Eagerly consume the constant run c from the tail by taking the c-derivative - // of each postfix - if (!c.empty()) { - unsigned w = 0; - for (i = 0; i < result.size(); ++i) { - expr* d = result[i].m_n; - for (unsigned k = 0; d && !seq().re.is_empty(d) && k < c.length(); ++k) { - d = m_rw.mk_derivative(seq().mk_char(c[k]), d); - } - SASSERT(d); - if (re().is_empty(d)) - continue; // postfix can't start with c => infeasible split, drop - result[w++] = split_pair(result[i].m_d, d, m); - } - result.shrink(w); - } - - return { expr_ref(head, m), expr_ref(tail, m) }; -} - -bool seq_split::split_lookahead_viable(expr* regex, zstring const& c) const { - SASSERT(regex); - for (unsigned i = 0; i < c.length(); i++) { - if (m.is_true(m_rw.is_nullable(regex))) - return true; // N accepts the prefix c[0..i) => a suffix completes it - regex = m_rw.mk_derivative(seq().mk_char(c[i]), regex); - SASSERT(regex); - if (re().is_empty(regex)) - return false; // N went (syntactically) dead before reaching c - } - return !re().is_empty(regex); -} \ No newline at end of file diff --git a/src/ast/rewriter/seq_split.h b/src/ast/rewriter/seq_split.h index 4df5e49014..18469c26fa 100644 --- a/src/ast/rewriter/seq_split.h +++ b/src/ast/rewriter/seq_split.h @@ -36,25 +36,25 @@ class seq_rewriter; // default) keeps everything, so sigma is unchanged. See seq_split::compute. typedef std::function split_oracle; -class split_set2 { +class split_set { struct imp; imp *m_imp; class consumer; public: - split_set2(seq_rewriter &rw, expr *r, unsigned threshold, split_oracle const& oracle = split_oracle()); + split_set(seq_rewriter &rw, expr *r, unsigned threshold, split_oracle const& filter); - ~split_set2(); + ~split_set(); - split_set2(split_set2 const& other); + split_set(split_set const& other); class iterator { struct imp; imp *m_imp; friend class consumer; public: - iterator(split_set2 const& s, bool end = false); + iterator(split_set const& s, bool end = false); ~iterator(); iterator &operator++(); std::pair operator*() const; @@ -68,209 +68,3 @@ public: iterator begin() const; iterator end() const; }; - -// An individual split : the left (prefix) regex D and right (suffix) -// regex N. u.v in L(r) for this split iff u in L(D) and v in L(N). -struct split_pair { - expr_ref m_d; - expr_ref m_n; - split_pair(expr* d, expr* n, ast_manager& m) : m_d(d, m), m_n(n, m) { - SASSERT(d && n); - } -}; - -// A split-set is a union of individual splits. -typedef vector split_set; - -// Controls how aggressively sigma expands the Boolean-closure cases: -// strong - fully expand complement / intersection via the split algebra -// (De Morgan / cross product). This is the behaviour the nseq -// solver relies on. -// weak - do not perform the (potentially 2^k) Boolean-closure expansion; -// give up (return false) on complement / intersection instead. -enum class split_mode { weak, strong }; - - - -class seq_split { - ast_manager& m; - seq_rewriter& m_rw; // for mk_re_append + manager / seq_util access - seq_subset m_subset; // language-subset checks for subsumption - - // --- Suspended split-set representation ------------------------------- - // A split-set computation is kept as an `expr` term over a small family of - // locally-declared, uninterpreted function symbols (the split algebra of the - // paper / split-algebra.md). Nothing here is ever asserted to the solver; - // the terms are only used as scratch structure to drive lazy expansion. - // - // empty : SplitSet -- {} (bottom) - // single : Re x Re -> SplitSet -- a single split - // from_re : Re -> SplitSet -- the *suspended* sigma(r) - // union : SplitSet x SplitSet -> SplitSet - // inter : SplitSet x SplitSet -> SplitSet - // compl : SplitSet -> SplitSet - // lcat : Re x SplitSet -> SplitSet -- r . S (left-concat onto D) - // rcat : SplitSet x Re -> SplitSet -- S . r (right-concat onto N) - sort* m_seq_sort = nullptr; // sequence sort the decls are built for - sort_ref m_set_sort; // the uninterpreted SplitSet sort - func_decl_ref m_d_empty, m_d_single, m_d_fromre, m_d_union, - m_d_inter, m_d_compl, m_d_lcat, m_d_rcat; - expr_ref m_empty_app; // cached nullary `empty` term - - seq_util& seq() const; - seq_util::rex& re() const; - - // (Re)build the local declarations for `seq_sort` if not already current. - void ensure_decls(sort* seq_sort); - - // Smart constructors: apply the cheap normalizations the eager engine relies - // on (drop-bottom, eps cancellation, union absorption of empty). - expr_ref mk_empty(); - expr_ref mk_single(expr* d, expr* n); - expr_ref mk_fromre(expr* r); - expr_ref mk_union(expr* a, expr* b); - expr_ref mk_inter(expr* a, expr* b); - expr_ref mk_compl(expr* a); - expr_ref mk_lcat(expr* r, expr* s); - expr_ref mk_rcat(expr* s, expr* r); - - // Recognizers over the local decls. - bool is_empty_ss(expr* e) const; - bool is_app1(expr *e, func_decl *d, expr *&a) const; - bool is_app2(expr *e, func_decl *d, expr*& a, expr*& b) const; - bool is_single(expr *e, expr *&d, expr *&n) const { - return is_app2(e, m_d_single, d, n); - } - bool is_fromre(expr* e, expr*& r) const { - return is_app1(e, m_d_fromre, r); - } - bool is_union (expr* e, expr*& a, expr*& b) const { - return is_app2(e, m_d_union, a, b); - } - bool is_inter (expr* e, expr*& a, expr*& b) const { - return is_app2(e, m_d_inter, a, b); - } - bool is_compl (expr* e, expr*& a) const { - return is_app1(e, m_d_compl, a); - } - bool is_lcat (expr* e, expr*& r, expr*& s) const { - return is_app2(e, m_d_lcat, r, s); - } - bool is_rcat (expr* e, expr*& s, expr*& r) const { - return is_app2(e, m_d_rcat, s, r); - } - // A term whose head is empty | single | union (ready for the worklist loop). - bool is_frontier(expr* e) const; - - // One level of the sigma rules: from_re(r) -> a SplitSet term built from the - // immediate subterms. `ok` is set false on an unsupported shape. - expr_ref expand_fromre(expr* r, bool& ok); - // Distribute a left/right concatenation over a head-normal split-set. - expr_ref distribute_lcat(expr* r, expr* hs); - expr_ref distribute_rcat(expr* hs, expr* r); - // Materialized split-set -> a `union` of `single`s. - expr_ref from_split_set(split_set const& s); - // Reduce `t` until its head is empty | single | union (one outermost level - // for the lazy nodes; inter/compl are expanded eagerly via `materialize`, - // since the paper's De Morgan / cross-product cannot yield a split lazily). - // `ok` is set false on a give-up (unsupported shape, weak-mode Boolean, or - // threshold overrun). - expr_ref head_normalize(expr* t, split_mode mode, unsigned threshold, - split_oracle const& oracle, bool& ok); - // Fully drain a suspended split-set into `out` (used for inter/compl bodies). - // Runs an `iterator` to exhaustion; returns false on a give-up. - bool materialize(expr* node, split_mode mode, unsigned threshold, - split_oracle const& oracle, split_set& out); - - // Push onto `out`, unless `oracle` rejects it. - void push(split_set& out, split_oracle const& oracle, expr* d, expr* n) const; - - // S1 cap S2 = { } dropping any pair with a bottom - // component (and any rejected by `oracle`). Returns false on threshold overrun. - bool intersect(split_set const& s1, split_set const& s2, split_set& result, - unsigned threshold, split_oracle const& oracle) const; - - // De Morgan complement of a split-set: ~S = cap_{s in S} ~s with - // ~ = { <~D, .*>, <.*, ~N> } and ~{} = { <.*, .*> }. - bool complement(sort* seq_sort, split_set const& sp, split_set& result, - unsigned threshold, split_oracle const& oracle) const; - - // same-D / same-N merge: groups pairs that share a (syntactically identical) - // left (resp. right) component and unions the other component. - void merge_by(split_set& pairs, bool by_left) const; - -public: - explicit seq_split(seq_rewriter& rw); - - // Lazy split enumerator. Holds the suspended split-set worklist and produces - // the concrete splits one at a time, on demand, instead of computing - // them all up front. Obtain one from seq_split::iterate (or construct it - // directly) and pull splits with next() until it returns false; gave_up() then - // tells a normal exhaustion (false) apart from a give-up (true). - // - // The threshold is supplied by the caller and serves only as a safety cap - // against space bloat (lazy expansion still has to materialize the operands of - // intersection / complement). A threshold overrun, an unsupported regex shape, - // or a Boolean-closure case in weak mode aborts the enumeration: next() returns - // false and gave_up() returns true. To stop early, simply stop calling next(). - // - // `oracle` (optional) prunes non-viable splits as they are produced. It must - // be sound to apply per split: a candidate N can still gain a prefix from a - // factor appended to its right later (concat/star), so the oracle must use a - // "prefix-compatible" test (prune only when N can never match the lookahead, - // even partially), NOT a strict "starts-with" test. The complement body is - // expanded WITHOUT the oracle (inverted orientation); the oracle is re-applied - // to the complement's output fold. - class iterator { - seq_split& m_engine; - ast_manager& m; - split_mode m_mode; - unsigned m_threshold; - split_oracle m_oracle; - expr_ref_vector m_work; // GC-safe worklist of suspended split-sets - unsigned m_count = 0; // splits produced so far (vs. threshold) - bool m_giveup = false; - public: - iterator(seq_split& engine, expr* node, split_mode mode, - unsigned threshold, split_oracle oracle); - // Compute the next split. On success returns true and sets ; on - // exhaustion or give-up returns false (see gave_up()). Calling next() - // again after it has returned false keeps returning false. - bool next(expr_ref& d, expr_ref& n); - // Valid after next() has returned false: true iff the enumeration aborted - // (unsupported regex / weak-mode Boolean / threshold overrun) rather than - // running out of splits. - bool gave_up() const { return m_giveup; } - }; - - // Build the *suspended* sigma(r) as a split-algebra term (no expansion). - // Returns null on a non-regex argument. Drive it with `iterate`. - expr_ref make(expr* r); - - // Create a lazy enumerator over a suspended split-set `node` (typically the - // result of make()). See `iterator` for the meaning of the arguments. - iterator iterate(expr* node, split_mode mode, unsigned threshold, - split_oracle const& oracle = {}); - - // Compute sigma(r), appending to `out` (does not clear it). Thin eager - // wrapper that drains an `iterator` to exhaustion; semantics match the historic - // engine. See `iterator` for the meaning of `threshold`, `mode`, and `oracle`. - bool compute(expr* r, split_set& out, unsigned threshold, - split_mode mode = split_mode::strong, split_oracle const& oracle = {}); - - // In-place simplification of a split-set: drop bottom components, apply the - // same-D / same-N merge rules, and drop splits subsumed by another (using - // seq_subset). Size-capped to keep the O(n^2) subsumption affordable. - void simplify(split_set& s) const; - - // decompose a membership constraint into a set of pairs of regex splits - std::pair split_membership(expr* str, expr* regex, unsigned threshold, split_set& result) const; - - // Lookahead oracle for the split engine: is the split's right component - // `n_regex` prefix-compatible with the constant character sequence `c`? - // This is sound to apply during split generation — it never drops a viable split. - // Thus, it might not eliminate all cases in order to stay sound - bool split_lookahead_viable(expr* regex, zstring const& c) const; - - -}; diff --git a/src/smt/seq_regex.cpp b/src/smt/seq_regex.cpp index e0423599dc..b6cc2f941d 100644 --- a/src/smt/seq_regex.cpp +++ b/src/smt/seq_regex.cpp @@ -128,6 +128,8 @@ namespace smt { return; } + #if 0 + // TODO - review if (th.get_fparams().m_seq_regex_factorization_enabled) { unsigned threshold = th.get_fparams().m_seq_regex_factorization_threshold; if (threshold == 0) @@ -151,6 +153,7 @@ namespace smt { } // fallthrough; decomposition failed } + #endif // Convert a non-ground sequence into an additional regex and // strengthen the original regex constraint into an intersection diff --git a/src/test/seq_split.cpp b/src/test/seq_split.cpp index 29df0545c7..1347bdd401 100644 --- a/src/test/seq_split.cpp +++ b/src/test/seq_split.cpp @@ -7,7 +7,10 @@ Module Name: Abstract: - Unit tests for the regex split engine (the split function sigma) in ast/rewriter/seq_split.cpp. + Unit tests for the regex split engine (the split function sigma) in + ast/rewriter/seq_split.cpp. The engine is exposed through split_set: a + lazily-iterated split-set constructed from a regex, a size threshold, and an + optional lookahead oracle. Author: @@ -20,6 +23,7 @@ Author: #include "ast/seq_decl_plugin.h" #include "ast/rewriter/seq_rewriter.h" #include "ast/rewriter/seq_split.h" +#include "ast/rewriter/th_rewriter.h" #include #include @@ -29,181 +33,305 @@ struct plugin_registrar { }; class seq_split_test { - ast_manager m; + ast_manager m; plugin_registrar m_reg; - seq_rewriter m_rw; - seq_split m_split; - seq_util u; - sort_ref m_str; // the sequence (String) sort - sort_ref m_re; // the RegEx sort over m_str + seq_rewriter m_rw; + seq_util u; + sort_ref m_str; // the sequence (String) sort + sort_ref m_re; // the RegEx sort over m_str + expr_ref_vector m_pin; // keeps collected/expected AST nodes alive so that + // pointer identity (hash-consing) is stable across + // the lifetime of a single check. seq_util::rex& re() { return u.re; } + // pin an expr so its address stays valid for later hash-cons lookups, and + // return the raw pointer used as a set key. + expr* pin(expr* e) { m_pin.push_back(e); return e; } + expr_ref eps() { return expr_ref(re().mk_epsilon(m_str), m); } // mk_epsilon takes the seq sort expr_ref dot() { return expr_ref(re().mk_full_char(m_re), m); } // mk_full_char takes the RegEx sort expr_ref dotstar() { return expr_ref(re().mk_full_seq(m_re), m); } // .* expr_ref empty_re() { return expr_ref(re().mk_empty(m_re), m); } // the bottom regex - expr_ref rappend(expr* a, expr* b) { return m_rw.mk_re_append(a, b); } // the engine's regex concat + expr_ref rcat(expr* a, expr* b) { return m_rw.mk_re_append(a, b); } // the engine's raw regex concat expr_ref word(char const* s) { return expr_ref(re().mk_to_re(u.str.mk_string(zstring(s))), m); } expr_ref rng(char lo, char hi) { - return expr_ref(re().mk_range(u.str.mk_string(zstring(std::string(1, lo).c_str())), - u.str.mk_string(zstring(std::string(1, hi).c_str()))), m); + return expr_ref(re().mk_range(m_re, static_cast(lo), static_cast(hi)), m); } typedef std::set> pair_set; - pair_set as_set(split_set const& s) { - pair_set out; - for (auto const& p : s) - out.insert({ p.m_d.get(), p.m_n.get() }); - return out; + // Drain sigma(r) into a set of pairs. Returns true when the engine + // ran to a clean exhaustion, false when it gave up (threshold overrun or an + // unsupported regex). Collected nodes are pinned so that the raw pointers + // used as set keys stay valid after the split_set is destroyed. + bool collect(expr* r, pair_set& out, unsigned threshold = UINT_MAX, + split_oracle const& oracle = split_oracle()) { + split_set s(m_rw, r, threshold, oracle); + split_set::iterator it = s.begin(), end = s.end(); + for (; it != end; ++it) { + auto const [d, n] = *it; + out.insert({ pin(d), pin(n) }); + } + return !it.failed(); } - bool eager(expr* r, split_set& out, unsigned threshold = UINT_MAX, - split_mode mode = split_mode::strong, split_oracle const& oracle = {}) { - return m_split.compute(r, out, threshold, mode, oracle); - } - - bool lazy(expr* r, split_set& out, unsigned threshold = UINT_MAX, - split_mode mode = split_mode::strong, split_oracle const& oracle = {}) { - expr_ref node = m_split.make(r); - ENSURE(node); - seq_split::iterator it = m_split.iterate(node, mode, threshold, oracle); - expr_ref d(m), n(m); - while (it.next(d, n)) - out.push_back(split_pair(d, n, m)); - return !it.gave_up(); - } - - // assert that the eager and lazy engines agree on sigma(r) as a *set* of - // splits, and report the common cardinality. - unsigned check_agree(expr* r) { - split_set se, sl; - bool oke = eager(r, se); - bool okl = lazy(r, sl); - ENSURE(oke == okl); - if (!oke) - return 0; - ENSURE(as_set(se) == as_set(sl)); - return (unsigned)as_set(se).size(); + // Cardinality of sigma(r); requires a clean exhaustion. + unsigned count(expr* r) { + pair_set s; + ENSURE(collect(r, s)); + return (unsigned)s.size(); } public: - seq_split_test() : m_reg(m), m_rw(m), m_split(m_rw), u(m), m_str(m), m_re(m) { + seq_split_test() : m_reg(m), m_rw(m), u(m), m_str(m), m_re(m), m_pin(m) { m_str = u.str.mk_string_sort(); m_re = re().mk_re(m_str); } - void test_eager_epsilon() { - split_set s; - ENSURE(eager(eps(), s)); - ENSURE(as_set(s) == pair_set({ { eps().get(), eps().get() } })); + void test_epsilon() { + // sigma(eps) = { } + pair_set s; + ENSURE(collect(eps(), s)); + ENSURE(s == pair_set({ { eps().get(), eps().get() } })); } - void test_eager_char() { + void test_char() { // sigma(.) = { , <., eps> } expr_ref a = dot(); - split_set s; - ENSURE(eager(a, s)); + pair_set s; + ENSURE(collect(a, s)); pair_set expected({ { eps().get(), a.get() }, { a.get(), eps().get() } }); - ENSURE(as_set(s) == expected); + ENSURE(s == expected); } - void test_eager_word() { + void test_word() { // sigma("ab") = { <"", "ab">, <"a","b">, <"ab",""> } - split_set s; - ENSURE(eager(word("ab"), s)); + pair_set s; + ENSURE(collect(word("ab"), s)); pair_set expected({ - { word("").get(), word("ab").get() }, - { word("a").get(), word("b").get() }, - { word("ab").get(), word("").get() }, + { word("").get(), word("ab").get() }, + { word("a").get(), word("b").get() }, + { word("ab").get(), word("").get() }, }); - ENSURE(as_set(s) == expected); + ENSURE(s == expected); } - void test_eager_union() { + void test_empty_word() { + // sigma(to_re("")) = { <"", ""> } (a single, trivial split) + pair_set s; + ENSURE(collect(word(""), s)); + ENSURE(s == pair_set({ { word("").get(), word("").get() } })); + } + + void test_union() { // sigma(a | b) = sigma(a) cup sigma(b) expr_ref a = rng('a', 'a'), b = rng('b', 'b'); expr_ref u_re(re().mk_union(a, b), m); - split_set s; - ENSURE(eager(u_re, s)); + pair_set s; + ENSURE(collect(u_re, s)); pair_set expected({ { eps().get(), a.get() }, { a.get(), eps().get() }, { eps().get(), b.get() }, { b.get(), eps().get() }, }); - ENSURE(as_set(s) == expected); + ENSURE(s == expected); } - void test_agree_all() { + void test_full_seq() { + // sigma(.*) = { <.*, .*> } + expr_ref ds = dotstar(); + pair_set s; + ENSURE(collect(ds, s)); + ENSURE(s == pair_set({ { ds.get(), ds.get() } })); + } + + void test_bottom() { + // sigma(empty) = {} + pair_set s; + ENSURE(collect(empty_re(), s)); + ENSURE(s.empty()); + } + + void test_star_content() { + // sigma(a*) = { , , } + expr_ref a = rng('a', 'a'); + expr_ref as(re().mk_star(a), m); + pair_set s; + ENSURE(collect(as, s)); + pair_set expected({ + { eps().get(), eps().get() }, + { rcat(as, eps()).get(), rcat(a, as).get() }, + { rcat(as, a).get(), rcat(eps(), as).get() }, + }); + ENSURE(s == expected); + } + + void test_plus_content() { + // sigma(a+) = a*.sigma(a).a* (the star rule without ) + expr_ref a = rng('a', 'a'); + expr_ref as(re().mk_star(a), m); + expr_ref ap(re().mk_plus(a), m); + pair_set s; + ENSURE(collect(ap, s)); + pair_set expected({ + { rcat(as, eps()).get(), rcat(a, as).get() }, + { rcat(as, a).get(), rcat(eps(), as).get() }, + }); + ENSURE(s == expected); + } + + void test_concat_content() { + // sigma(a.b): the engine drops the epsilon-suffix split from the left + // side (it is language-equivalent to a right-side split), giving + // { , , } expr_ref a = rng('a', 'a'), b = rng('b', 'b'); - expr_ref star(re().mk_star(a), m); - expr_ref plus(re().mk_plus(a), m); - expr_ref concat(re().mk_concat(a, b), m); - expr_ref uni(re().mk_union(a, b), m); - expr_ref inter(re().mk_inter(re().mk_star(a), re().mk_star(b)), m); - expr_ref compl_(re().mk_complement(re().mk_star(a)), m); - expr_ref diff(re().mk_diff(re().mk_star(a), re().mk_star(b)), m); - - ENSURE(check_agree(eps()) == 1); - ENSURE(check_agree(a) == 2); - ENSURE(check_agree(word("ab")) == 3); - ENSURE(check_agree(uni) == 4); - ENSURE(check_agree(star) == 3); // { , , } - (void)check_agree(plus); - (void)check_agree(concat); - (void)check_agree(inter); // strong-mode intersection - (void)check_agree(compl_); // strong-mode De Morgan complement - (void)check_agree(diff); + expr_ref ab(re().mk_concat(a, b), m); + pair_set s; + ENSURE(collect(ab, s)); + pair_set expected({ + { eps().get(), rcat(a, b).get() }, // + { rcat(a, eps()).get(), b.get() }, // + { rcat(a, b).get(), eps().get() }, // + }); + ENSURE(s == expected); } - void test_lazy_early_stop() { - // a* has 3 splits; pull just the first one and then stop. (Note .* is the - // full_seq special case with a single split, so use a proper char-class body.) - expr_ref star(re().mk_star(rng('a', 'a')), m); - expr_ref node = m_split.make(star); - ENSURE(node); - seq_split::iterator it = m_split.iterate(node, split_mode::strong, UINT_MAX, {}); - expr_ref d(m), n(m); - unsigned seen = 0; - if (it.next(d, n)) // pull exactly one split, then walk away - ++seen; - ENSURE(!it.gave_up()); // stopping early is not a give-up - ENSURE(seen == 1); + void test_nary_union() { + // sigma(a|b|c) has 2 splits per char-class + expr_ref a = rng('a', 'a'), b = rng('b', 'b'), c = rng('c', 'c'); + expr_ref u3(re().mk_union(a, re().mk_union(b, c)), m); + ENSURE(count(u3) == 6); + } + + void test_nary_concat() { + // sigma(a.b.c) + expr_ref a = rng('a', 'a'), b = rng('b', 'b'), c = rng('c', 'c'); + expr_ref c3(re().mk_concat(a, re().mk_concat(b, c)), m); + ENSURE(count(c3) >= 4); + } + + void test_intersection() { + // The engine handles intersection via the split algebra (De Morgan-free + // product). It must run to completion and produce a non-empty set. + expr_ref inter(re().mk_inter(re().mk_star(rng('a', 'a')), + re().mk_star(rng('b', 'b'))), m); + pair_set s; + ENSURE(collect(inter, s)); + ENSURE(!s.empty()); + } + + void test_complement() { + // strong-mode De Morgan complement + expr_ref compl_(re().mk_complement(re().mk_star(rng('a', 'a'))), m); + pair_set s; + ENSURE(collect(compl_, s)); + ENSURE(!s.empty()); + } + + void test_diff() { + // sigma(a* \ b*) via intersection with the complement + expr_ref diff(re().mk_diff(re().mk_star(rng('a', 'a')), + re().mk_star(rng('b', 'b'))), m); + pair_set s; + ENSURE(collect(diff, s)); + ENSURE(!s.empty()); + } + + void test_nested_complement() { + // sigma(~~(a*)) must still terminate cleanly + expr_ref cc(re().mk_complement(re().mk_complement(re().mk_star(rng('a', 'a')))), m); + pair_set s; + ENSURE(collect(cc, s)); + } + + void test_determinism() { + // Two independent runs over the same regex yield the identical set. + expr_ref r(re().mk_concat(rng('a', 'a'), re().mk_star(rng('b', 'b'))), m); + pair_set s1, s2; + ENSURE(collect(r, s1)); + ENSURE(collect(r, s2)); + ENSURE(s1 == s2); + } + + void test_threshold_boundary() { + expr_ref as(re().mk_star(rng('a', 'a')), m); // exactly 3 splits + unsigned k = count(as); + ENSURE(k == 3); + + pair_set ok; + ENSURE(collect(as, ok, k)); // at threshold: fine + + pair_set bad; + ENSURE(!collect(as, bad, k - 1)); // one below threshold: give up } void test_threshold_giveup() { - expr_ref star(re().mk_star(rng('a', 'a')), m); // 3 splits - split_set s; - ENSURE(!lazy(star, s, /*threshold*/ 1)); - // the eager wrapper honours the same cap - split_set s2; - ENSURE(!eager(star, s2, /*threshold*/ 1)); + // a* has 3 splits; capping at 1 forces a give-up. + expr_ref as(re().mk_star(rng('a', 'a')), m); + pair_set s; + ENSURE(!collect(as, s, /*threshold*/ 1)); } - void test_weak_vs_strong() { - expr_ref inter(re().mk_inter(re().mk_star(rng('a', 'a')), re().mk_star(rng('b', 'b'))), m); - expr_ref compl_(re().mk_complement(re().mk_star(dot())), m); - - split_set s; - ENSURE(!eager(inter, s, UINT_MAX, split_mode::weak)); - s.reset(); - ENSURE(!lazy(inter, s, UINT_MAX, split_mode::weak)); - s.reset(); - ENSURE(!eager(compl_, s, UINT_MAX, split_mode::weak)); - s.reset(); - ENSURE(!lazy(compl_, s, UINT_MAX, split_mode::weak)); - - // strong mode succeeds for both - s.reset(); - ENSURE(eager(inter, s, UINT_MAX, split_mode::strong)); - s.reset(); - ENSURE(eager(compl_, s, UINT_MAX, split_mode::strong)); + void test_early_stop() { + // Pull exactly one split on demand, then walk away. Stopping early is + // not a give-up, even when the full set is larger. + expr_ref as(re().mk_star(rng('a', 'a')), m); // 3 splits + split_set s(m_rw, as, UINT_MAX, {}); + split_set::iterator it = s.begin(), end = s.end(); + unsigned seen = 0; + if (it != end) { + (void)*it; + ++seen; + } + ENSURE(seen == 1); + ENSURE(!it.failed()); // early stop is not a failure } - void test_make_non_regex() { - expr_ref not_a_regex(u.str.mk_string(zstring("a")), m); // String, not RegEx - expr_ref node = m_split.make(not_a_regex); - ENSURE(!node); + void test_early_stop_after_two() { + // Pull two splits on demand, then stop. + expr_ref as(re().mk_star(rng('a', 'a')), m); // 3 splits + split_set s(m_rw, as, UINT_MAX, {}); + split_set::iterator it = s.begin(), end = s.end(); + unsigned seen = 0; + while (seen < 2 && it != end) { + (void)*it; + ++it; + ++seen; + } + ENSURE(seen == 2); + ENSURE(!it.failed()); + } + + void test_iterator_exhaustion() { + // Pull every split on demand; failed() must stay false on a clean + // exhaustion, and end() must remain end() once drained. + expr_ref as(re().mk_star(rng('a', 'a')), m); // 3 splits + split_set s(m_rw, as, UINT_MAX, {}); + split_set::iterator it = s.begin(), end = s.end(); + unsigned seen = 0; + for (; it != end; ++it) { + (void)*it; + ++seen; + } + ENSURE(seen == 3); + ENSURE(!it.failed()); + // idempotent past the end + ENSURE(it == end); + ENSURE(!it.failed()); + } + + void test_iterator_giveup() { + // A threshold overrun aborts: the iterator reaches end() with failed(). + expr_ref as(re().mk_star(rng('a', 'a')), m); // 3 splits, cap at 1 + split_set s(m_rw, as, 1, {}); + split_set::iterator it = s.begin(), end = s.end(); + unsigned seen = 0; + for (; it != end; ++it) { + (void)*it; + ++seen; + } + ENSURE(it.failed()); // aborted, not a clean exhaustion + ENSURE(seen <= 1); // produced at most the capped number } void test_oracle_prunes() { @@ -213,233 +341,46 @@ public: expr_ref e = eps(); split_oracle keep_eps_suffix = [&](expr*, expr* n) { return n == e.get(); }; - split_set se, sl; - ENSURE(eager(a, se, UINT_MAX, split_mode::strong, keep_eps_suffix)); - ENSURE(lazy(a, sl, UINT_MAX, split_mode::strong, keep_eps_suffix)); - pair_set expected({ { a.get(), e.get() } }); - ENSURE(as_set(se) == expected); - ENSURE(as_set(sl) == expected); - } - - void test_eager_full_seq() { - // sigma(.*) = { <.*, .*> } - expr_ref ds = dotstar(); - split_set s; - ENSURE(eager(ds, s)); - ENSURE(as_set(s) == pair_set({ { ds.get(), ds.get() } })); - } - - void test_eager_bottom() { - // sigma(empty) = {} - split_set s; - ENSURE(eager(empty_re(), s)); - ENSURE(s.empty()); - - split_set sl; - ENSURE(lazy(empty_re(), sl)); - ENSURE(sl.empty()); - } - - void test_eager_empty_word() { - // sigma(to_re("")) = { <"", ""> } (a single, trivial split) - split_set s; - ENSURE(eager(word(""), s)); - ENSURE(as_set(s) == pair_set({ { word("").get(), word("").get() } })); - } - - void test_eager_star_content() { - // sigma(a*) = { , , } - expr_ref a = rng('a', 'a'); - expr_ref as(re().mk_star(a), m); - split_set s; - ENSURE(eager(as, s)); - pair_set expected({ - { eps().get(), eps().get() }, - { rappend(as, eps()).get(), rappend(a, as).get() }, - { rappend(as, a).get(), rappend(eps(), as).get() }, - }); - ENSURE(as_set(s) == expected); - } - - void test_eager_plus_content() { - // sigma(a+) = a*.sigma(a).a* (the star rule without ) - expr_ref a = rng('a', 'a'); - expr_ref as(re().mk_star(a), m); - expr_ref ap(re().mk_plus(a), m); - split_set s; - ENSURE(eager(ap, s)); - pair_set expected({ - { rappend(as, eps()).get(), rappend(a, as).get() }, - { rappend(as, a).get(), rappend(eps(), as).get() }, - }); - ENSURE(as_set(s) == expected); - } - - void test_eager_concat_content() { - // sigma(a.b) = sigma(a).b cup a.sigma(b) - expr_ref a = rng('a', 'a'), b = rng('b', 'b'); - expr_ref ab(re().mk_concat(a, b), m); - split_set s; - ENSURE(eager(ab, s)); - pair_set expected({ - { eps().get(), rappend(a, b).get() }, // - { a.get(), rappend(eps(), b).get() }, // - { rappend(a, eps()).get(), b.get() }, // - { rappend(a, b).get(), eps().get() }, // - }); - ENSURE(as_set(s) == expected); - } - - void test_nary_union() { - // sigma(a|b|c) has 2 splits per char-class - expr_ref a = rng('a', 'a'), b = rng('b', 'b'), c = rng('c', 'c'); - expr_ref u3(re().mk_union(a, re().mk_union(b, c)), m); - ENSURE(check_agree(u3) == 6); - } - - void test_nary_concat() { - // sigma(a.b.c) - expr_ref a = rng('a', 'a'), b = rng('b', 'b'), c = rng('c', 'c'); - expr_ref c3(re().mk_concat(a, re().mk_concat(b, c)), m); - ENSURE(check_agree(c3) >= 4); - } - - void test_nested_complement() { - // sigma(~~(a*)) - expr_ref cc(re().mk_complement(re().mk_complement(re().mk_star(rng('a', 'a')))), m); - (void)check_agree(cc); - } - - void test_determinism() { - expr_ref r(re().mk_concat(rng('a', 'a'), re().mk_star(rng('b', 'b'))), m); - split_set s1, s2; - ENSURE(lazy(r, s1)); - ENSURE(lazy(r, s2)); - ENSURE(as_set(s1) == as_set(s2)); - } - - void test_threshold_boundary() { - expr_ref as(re().mk_star(rng('a', 'a')), m); // exactly 3 splits - split_set s; - ENSURE(eager(as, s)); - unsigned k = (unsigned)as_set(s).size(); - ENSURE(k == 3); - - split_set ok_e, ok_l, bad_e, bad_l; - ENSURE(eager(as, ok_e, k)); - ENSURE(lazy(as, ok_l, k)); - ENSURE(!eager(as, bad_e, k - 1)); // one below threshold; give up - ENSURE(!lazy(as, bad_l, k - 1)); - } - - void test_early_stop_after_two() { - expr_ref as(re().mk_star(rng('a', 'a')), m); // 3 splits - expr_ref node = m_split.make(as); - ENSURE(node); - seq_split::iterator it = m_split.iterate(node, split_mode::strong, UINT_MAX, {}); - expr_ref d(m), n(m); - unsigned seen = 0; - while (seen < 2 && it.next(d, n)) // pull two splits on demand, then stop - ++seen; - ENSURE(!it.gave_up()); - ENSURE(seen == 2); - } - - void test_iterator_exhaustion() { - // Pull every split on demand; gave_up() must stay false on a clean - // exhaustion, and next() must keep returning false once drained. - expr_ref as(re().mk_star(rng('a', 'a')), m); // 3 splits - expr_ref node = m_split.make(as); - ENSURE(node); - seq_split::iterator it = m_split.iterate(node, split_mode::strong, UINT_MAX, {}); - expr_ref d(m), n(m); - unsigned seen = 0; - while (it.next(d, n)) - ++seen; - ENSURE(seen == 3); - ENSURE(!it.gave_up()); - // idempotent past the end - ENSURE(!it.next(d, n)); - ENSURE(!it.gave_up()); - } - - void test_iterator_giveup() { - // A threshold overrun aborts: next() returns false and gave_up() is true. - expr_ref as(re().mk_star(rng('a', 'a')), m); // 3 splits, cap at 1 - expr_ref node = m_split.make(as); - ENSURE(node); - seq_split::iterator it = m_split.iterate(node, split_mode::strong, /*threshold*/ 1, {}); - expr_ref d(m), n(m); - unsigned seen = 0; - while (it.next(d, n)) - ++seen; - ENSURE(it.gave_up()); // aborted, not a clean exhaustion - ENSURE(seen <= 1); // produced at most the capped number - - // A weak-mode Boolean closure is likewise a give-up. - expr_ref inter(re().mk_inter(re().mk_star(rng('a', 'a')), re().mk_star(rng('b', 'b'))), m); - expr_ref inode = m_split.make(inter); - ENSURE(inode); - seq_split::iterator wit = m_split.iterate(inode, split_mode::weak, UINT_MAX, {}); - ENSURE(!wit.next(d, n)); - ENSURE(wit.gave_up()); - } - - void test_simplify() { - expr_ref regs[] = { - expr_ref(re().mk_star(rng('a', 'a')), m), - expr_ref(re().mk_complement(re().mk_star(rng('a', 'a'))), m), - expr_ref(re().mk_concat(rng('a', 'a'), rng('b', 'b')), m), - }; - for (auto& r : regs) { - split_set s; - ENSURE(eager(r, s)); - unsigned before = (unsigned)s.size(); - m_split.simplify(s); - ENSURE(s.size() <= before); - ENSURE(!s.empty()); - // idempotent - split_set s2(s); - m_split.simplify(s2); - ENSURE(as_set(s) == as_set(s2)); - } + pair_set s; + ENSURE(collect(a, s, UINT_MAX, keep_eps_suffix)); + ENSURE(s == pair_set({ { a.get(), e.get() } })); } void test_trivial_oracle() { + // An oracle that keeps everything leaves sigma unchanged. expr_ref r(re().mk_star(rng('a', 'a')), m); split_oracle keep_all = [](expr*, expr*) { return true; }; - split_set s_no, s_yes; - ENSURE(eager(r, s_no)); - ENSURE(eager(r, s_yes, UINT_MAX, split_mode::strong, keep_all)); - ENSURE(as_set(s_no) == as_set(s_yes)); + pair_set s_no, s_yes; + ENSURE(collect(r, s_no)); + ENSURE(collect(r, s_yes, UINT_MAX, keep_all)); + ENSURE(s_no == s_yes); } void run() { - test_eager_epsilon(); - test_eager_char(); - test_eager_word(); - test_eager_union(); - test_agree_all(); - test_lazy_early_stop(); - test_threshold_giveup(); - test_weak_vs_strong(); - test_make_non_regex(); - test_oracle_prunes(); - test_eager_full_seq(); - test_eager_bottom(); - test_eager_empty_word(); - test_eager_star_content(); - test_eager_plus_content(); - test_eager_concat_content(); + test_epsilon(); + test_char(); + test_word(); + test_empty_word(); + test_union(); + test_full_seq(); + test_bottom(); + test_star_content(); + test_plus_content(); + test_concat_content(); test_nary_union(); test_nary_concat(); + test_intersection(); + test_complement(); + test_diff(); test_nested_complement(); test_determinism(); test_threshold_boundary(); + test_threshold_giveup(); + test_early_stop(); test_early_stop_after_two(); test_iterator_exhaustion(); test_iterator_giveup(); - test_simplify(); + test_oracle_prunes(); test_trivial_oracle(); } }; From 2b4a473334e4d1f13b720fcb9908c0ea5ebdbda7 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Thu, 2 Jul 2026 18:42:56 -0700 Subject: [PATCH 06/24] use move constructor, re-enable split_set in seq_regex --- src/ast/rewriter/seq_split.cpp | 121 +++++++++++++++++++++++++++------ src/ast/rewriter/seq_split.h | 7 +- src/smt/seq_regex.cpp | 91 +++++++++++++++++++++---- src/smt/seq_regex.h | 2 + 4 files changed, 185 insertions(+), 36 deletions(-) diff --git a/src/ast/rewriter/seq_split.cpp b/src/ast/rewriter/seq_split.cpp index 7fe237b060..df97e43aa8 100644 --- a/src/ast/rewriter/seq_split.cpp +++ b/src/ast/rewriter/seq_split.cpp @@ -29,6 +29,7 @@ struct split_set::imp { split_oracle m_filter; sort *m_re_sort = nullptr; sort *m_seq_sort = nullptr; // sequence sort the decls are built for + bool m_failure = false; imp(seq_rewriter &rw, expr *r, unsigned threshold, split_oracle const &filter) : m(rw.m()), rw(rw), seq(rw.u()), re(rw.u().re), r(r, m), m_threshold(threshold), m_filter(filter) { @@ -61,8 +62,8 @@ struct split_set::iterator::imp { split_set a_s, b_s; split_set::iterator a_it, a_end; split_set::iterator b_it, b_end; - intersection(seq_rewriter& rw, split_set const& a_src, split_set const& b_src) - : a_s(a_src), b_s(b_src), + intersection(seq_rewriter& rw, split_set&& a_src, split_set&& b_src) + : a_s(std::move(a_src)), b_s(std::move(b_src)), a_it(a_s.begin()), a_end(a_s.end()), b_it(b_s.begin()), b_end(b_s.end()) {} bool at_end() const { @@ -107,21 +108,22 @@ struct split_set::iterator::imp { scoped_ptr m_intersection; - complement(split_set const &a) : a_s(a), it(a_s.begin()), end(a_s.end()) + complement(split_set&& a) : a_s(std::move(a)), it(a_s.begin()), end(a_s.end()) { } void init() { if (m_init) return; - m_init = true; - expr_ref full(parent().seq.re.mk_full_seq(parent().i.m_re_sort), parent().m); - m_intersection = nullptr; + m_init = true; auto &p = parent(); + expr_ref full(p.seq.re.mk_full_seq(p.i.m_re_sort), p.m); + m_intersection = nullptr; + while (it != end && !it.failed()) { auto [a, b] = *it; split_set A(p.i.rw, nullptr, p.i.m_threshold, p.i.m_filter); split_set B(p.i.rw, nullptr, p.i.m_threshold, p.i.m_filter); - auto inter = alloc(intersection, p.i.rw, A, B); + auto inter = alloc(intersection, p.i.rw, std::move(A), std::move(B)); if (m_intersection) { m_intersection->set_parent(*inter->a_it.m_imp); inter->a_it.m_imp->m_consumer = m_intersection.detach(); @@ -140,7 +142,7 @@ struct split_set::iterator::imp { else p.push_split(full, full); if (it.failed()) - p.m_failure = true; + p.set_failure(); } void consume() override { @@ -155,8 +157,8 @@ struct split_set::iterator::imp { split_set::iterator a_it; split_set::iterator a_end; expr_ref b; - concat_left(split_set const &a_src, expr *b) - : a_s(a_src), a_it(a_s.begin()), a_end(a_s.end()), b(b, a_s.m_imp->m) {} + concat_left(split_set&& a_src, expr *b) + : a_s(std::move(a_src)), a_it(a_s.begin()), a_end(a_s.end()), b(b, a_s.m_imp->m) {} void consume() override { while (a_it != a_end && !parent().has_split()) { @@ -165,7 +167,7 @@ struct split_set::iterator::imp { ++a_it; } if (a_it.failed()) - parent().m_failure = true; + parent().set_failure(); } }; @@ -174,7 +176,7 @@ struct split_set::iterator::imp { split_set b_s; split_set::iterator b_it; split_set::iterator b_end; - concat_right(expr* a, split_set const &b_src) : a(a, b_src.m_imp->m), b_s(b_src), b_it(b_s.begin()), b_end(b_s.end()) {} + concat_right(expr* a, split_set&& b_src) : a(a, b_src.m_imp->m), b_s(std::move(b_src)), b_it(b_s.begin()), b_end(b_s.end()) {} void consume() override { while (b_it != b_end && !parent().has_split()) { @@ -183,7 +185,7 @@ struct split_set::iterator::imp { ++b_it; } if (b_it.failed()) - parent().m_failure = true; + parent().set_failure(); } }; @@ -220,7 +222,7 @@ struct split_set::iterator::imp { } } if (a_it.failed() || b_it.failed()) - parent().m_failure = true; + parent().set_failure(); } }; @@ -243,6 +245,11 @@ struct split_set::iterator::imp { } } + void set_failure() { + m_failure = true; + s.m_imp->m_failure = true; + } + bool has_split() { SASSERT(m_init); return m_qhead < m_splits.size(); @@ -323,7 +330,7 @@ struct split_set::iterator::imp { m_splits.push_back({a, b}); if (m_splits.size() > i.m_threshold) { TRACE(seq, tout << "size of split set exceeds threshold"); - m_failure = true; + set_failure(); } } @@ -344,14 +351,14 @@ struct split_set::iterator::imp { if (re.is_intersection(r, a, b)) { split_set a_s(i.rw, a, i.m_threshold, {}); split_set b_s(i.rw, b, i.m_threshold, {}); - m_consumer = alloc(intersection, i.rw, a_s, b_s); + m_consumer = alloc(intersection, i.rw, std::move(a_s), std::move(b_s)); m_consumer->set_parent(*this); return; } if (re.is_complement(r, a)) { split_set sigma_a(i.rw, a, i.m_threshold, {}); - m_consumer = alloc(complement, sigma_a); + m_consumer = alloc(complement, std::move(sigma_a)); m_consumer->set_parent(*this); return; } @@ -392,9 +399,9 @@ struct split_set::iterator::imp { // star: sigma(a*) = { } cup a*.sigma(a).a* auto add_star = [&](expr *r, expr* a) { split_set sigma_a(i.rw, a, i.m_threshold, {}); - auto *c_left = alloc(concat_left, sigma_a, r); + auto *c_left = alloc(concat_left, std::move(sigma_a), r); split_set sigma_aa(i.rw, nullptr, i.m_threshold, {}); - auto *c_right = alloc(concat_right, r, sigma_aa); + auto *c_right = alloc(concat_right, r, std::move(sigma_aa)); auto &parent = *c_right->b_it.m_imp; parent.m_consumer = c_left; c_left->set_parent(parent); @@ -440,7 +447,7 @@ struct split_set::iterator::imp { void set_failure(expr* r) { TRACE(seq, tout << "split_set::iterator::unfold: unhandled regex: " << mk_pp(r, m) << "\n"); - m_failure = true; + set_failure(); m_at_end = true; } @@ -457,8 +464,8 @@ split_set::~split_set() { dealloc(m_imp); } -split_set::split_set(split_set const& other) { - m_imp = alloc(imp, other.m_imp->rw, other.m_imp->r, other.m_imp->m_threshold, other.m_imp->m_filter); +split_set::split_set(split_set&& other) noexcept : m_imp(other.m_imp) { + other.m_imp = nullptr; } split_set::iterator::iterator(split_set const &s, bool at_end) { @@ -496,3 +503,73 @@ bool split_set::iterator::operator==(split_set::iterator const &other) const { bool split_set::iterator::failed() const { return m_imp->m_failure; } + +bool split_set::failed() const { + return m_imp->m_failure; +} + +std::pair split_set::try_split_sequence(expr *str) { + ast_manager &m = m_imp->m; + auto &seq = m_imp->seq; + + expr_ref_vector tokens(m); + vector stack; + stack.push_back(str); + + while (!stack.empty()) { + expr *cur = stack.back(); + stack.pop_back(); + expr *l, *r; + if (seq.str.is_concat(cur, l, r)) { + stack.push_back(r); + stack.push_back(l); + } + else + tokens.push_back(expr_ref(cur, m)); + } + + expr *ch; + unsigned i = 0; + + // TODO: Do this for the back as well (also, why did no rule before do that?) + + if (tokens.empty()) + return {expr_ref(m), expr_ref(m)}; + + // Choose the factorization boundary so the tail starts with the + // longest run of concrete characters c. + // This gives the split-engine lookahead oracle the most pruning information. + // head = u' (tokens before the run), tail = c � u''' (tokens from the run onward). + const unsigned total = tokens.size(); + unsigned run_start = 0, run_len = 0; + for (i = 1; i < total;) { + if (!(seq.str.is_unit(tokens.get(i), ch) && seq.is_const_char(ch))) { + i++; + continue; + } + unsigned j = i; + while (j < total && seq.str.is_unit(tokens.get(j), ch) && seq.is_const_char(ch)) { + j++; + } + if (j - i > run_len) { + run_len = j - i; + run_start = i; + } + i = j; + } + // No constant run => fall back to splitting off the first token. + const unsigned p = run_len == 0 ? 1 : run_start; + SASSERT(p >= 1); + expr *head = tokens.get(0); + for (i = 1; i < p; i++) { + head = seq.str.mk_concat(head, tokens.get(i)); + } + expr *tail = seq.str.mk_empty(head->get_sort()); + if (tokens.size() > p + run_len) { + tail = tokens.get(p + run_len); + for (i = p + run_len + 1; i < tokens.size(); i++) { + tail = seq.str.mk_concat(tail, tokens.get(i)); + } + } + return {expr_ref(head, m), expr_ref(tail, m)}; +} diff --git a/src/ast/rewriter/seq_split.h b/src/ast/rewriter/seq_split.h index 18469c26fa..9746b07dc7 100644 --- a/src/ast/rewriter/seq_split.h +++ b/src/ast/rewriter/seq_split.h @@ -47,7 +47,9 @@ public: ~split_set(); - split_set(split_set const& other); + split_set(split_set const& other) = delete; + + split_set(split_set&& other) noexcept; class iterator { struct imp; @@ -67,4 +69,7 @@ public: iterator begin() const; iterator end() const; + bool failed() const; + + std::pair try_split_sequence(expr *s); }; diff --git a/src/smt/seq_regex.cpp b/src/smt/seq_regex.cpp index b6cc2f941d..be75641269 100644 --- a/src/smt/seq_regex.cpp +++ b/src/smt/seq_regex.cpp @@ -114,6 +114,12 @@ namespace smt { return; } + if (unfold_prefix(lit)) { + TRACE(seq_regex, tout << "unfolded prefix" << std::endl;); + STRACE(seq_regex_brief, tout << "unfold_prefix ";); + return; + } + if (coallesce_in_re(lit)) { TRACE(seq_regex, tout << "simplified conjunctions to an intersection" << std::endl;); @@ -121,6 +127,7 @@ namespace smt { return; } + if (is_string_equality(lit)) { TRACE(seq_regex, tout << "simplified regex using string equality" << std::endl;); @@ -128,16 +135,43 @@ namespace smt { return; } - #if 0 - // TODO - review + // TODO - replace this with a propagator closure that gets invoked and removed on backtracking. + // it tracks + // an in_re2 literal is of the form in_re2(u, R1, v, R2) + // Assert in_re2(u, R1, v, R2) => u in R1 and v in R2 + // forward on split_set until there is a new in_re2 literal that is not already false. + // If there was an already created in_re2 literal that is true, + // then check that the propagation axiom is true + // if it isn't true, then assert it. + // if it is true, we are done + // If split_set is done and all in_re2 literals are false, there is a conflict. + // Assert the conflict clause lit => (or in_re2 literals) + // Final check also unfolds this axiomatization + // (we have to add a final check to seq_regex for this). + if (th.get_fparams().m_seq_regex_factorization_enabled) { unsigned threshold = th.get_fparams().m_seq_regex_factorization_threshold; - if (threshold == 0) - threshold = UINT_MAX; - split_set result; - auto [head, tail] = seq_rw().split_membership(s, r, threshold, result); - if (head) { - SASSERT(tail); + expr_ref_vector prefix(m); + expr *hd, *tl, *v; + auto filter = [&](expr* p, expr* _q) -> bool { + expr_ref q(_q, m); + for (expr* v : prefix) { + q = seq_rw().mk_derivative(v, q); + if (re().is_empty(q)) + return false; + } + return re().is_empty(q); + }; + + split_set result(seq_rw(), r, threshold, filter); + + auto [head, tail] = result.try_split_sequence(s); + if (head && tail) { + tl = tail; + while (str().is_concat(tl, hd, tl) && str().is_unit(hd, v) && m.is_value(v)) { + prefix.push_back(v); + } + // propagate all cases expr_ref_vector cases(m); expr_ref_vector branches(m); @@ -146,14 +180,15 @@ namespace smt { expr_ref mem_tail(re().mk_in_re(tail, post), m); cases.push_back(m.mk_and(mem_head, mem_tail)); } - const expr_ref cases_expr(m.mk_or(cases), m); - ctx.internalize(cases_expr, false); - th.propagate_lit(nullptr, 1, &lit, ctx.get_literal(cases_expr)); - return; + if (!result.failed()) { + const expr_ref cases_expr(m.mk_or(cases), m); + ctx.internalize(cases_expr, false); + th.propagate_lit(nullptr, 1, &lit, ctx.get_literal(cases_expr)); + return; + } } // fallthrough; decomposition failed } - #endif // Convert a non-ground sequence into an additional regex and // strengthen the original regex constraint into an intersection @@ -384,6 +419,36 @@ namespace smt { true); } + bool seq_regex::unfold_prefix(literal lit) { + expr *s = nullptr, *r = nullptr; + expr *e = ctx.bool_var2expr(lit.var()); + VERIFY(str().is_in_re(e, s, r)); + expr_ref_vector prefix(m); + expr *hd, *v, *tl = s; + while (str().is_concat(tl, hd, tl) && str().is_unit(hd, v) && m.is_value(v)) + prefix.push_back(v); + + if (prefix.empty()) + return false; + + expr_ref q(r, m); + for (expr *v : prefix) { + q = seq_rw().mk_derivative(v, q); + if (re().is_empty(q)) { + enode_pair_vector eqs; + literal_vector lits; + lits.push_back(~lit); + th.set_conflict(eqs, lits); + return true; + } + } + expr_ref fml(re().mk_in_re(tl, q), m); + rewrite(fml); + literal nlit = th.mk_literal(fml); + th.propagate_lit(nullptr, 1, &lit, nlit); + return true; + } + /** * Combine a conjunction of membership relations for the same string * within the same Regex. diff --git a/src/smt/seq_regex.h b/src/smt/seq_regex.h index dd1c474b31..ff7b601b44 100644 --- a/src/smt/seq_regex.h +++ b/src/smt/seq_regex.h @@ -151,6 +151,8 @@ namespace smt { bool block_unfolding(literal lit, unsigned i); + bool unfold_prefix(literal lit); + expr_ref mk_first(expr* r, expr* n); bool is_member(expr* r, expr* u); From d43d61a4bff1475d96b9c84a518b3f4b046a8ac3 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Thu, 2 Jul 2026 19:32:09 -0700 Subject: [PATCH 07/24] cleanup and add comments --- src/smt/seq_regex.cpp | 120 ++++++++++++++++++++++-------------------- src/smt/seq_regex.h | 25 +++++++++ 2 files changed, 89 insertions(+), 56 deletions(-) diff --git a/src/smt/seq_regex.cpp b/src/smt/seq_regex.cpp index be75641269..497000d461 100644 --- a/src/smt/seq_regex.cpp +++ b/src/smt/seq_regex.cpp @@ -127,7 +127,6 @@ namespace smt { return; } - if (is_string_equality(lit)) { TRACE(seq_regex, tout << "simplified regex using string equality" << std::endl;); @@ -135,60 +134,10 @@ namespace smt { return; } - // TODO - replace this with a propagator closure that gets invoked and removed on backtracking. - // it tracks - // an in_re2 literal is of the form in_re2(u, R1, v, R2) - // Assert in_re2(u, R1, v, R2) => u in R1 and v in R2 - // forward on split_set until there is a new in_re2 literal that is not already false. - // If there was an already created in_re2 literal that is true, - // then check that the propagation axiom is true - // if it isn't true, then assert it. - // if it is true, we are done - // If split_set is done and all in_re2 literals are false, there is a conflict. - // Assert the conflict clause lit => (or in_re2 literals) - // Final check also unfolds this axiomatization - // (we have to add a final check to seq_regex for this). - - if (th.get_fparams().m_seq_regex_factorization_enabled) { - unsigned threshold = th.get_fparams().m_seq_regex_factorization_threshold; - expr_ref_vector prefix(m); - expr *hd, *tl, *v; - auto filter = [&](expr* p, expr* _q) -> bool { - expr_ref q(_q, m); - for (expr* v : prefix) { - q = seq_rw().mk_derivative(v, q); - if (re().is_empty(q)) - return false; - } - return re().is_empty(q); - }; - - split_set result(seq_rw(), r, threshold, filter); - - auto [head, tail] = result.try_split_sequence(s); - if (head && tail) { - tl = tail; - while (str().is_concat(tl, hd, tl) && str().is_unit(hd, v) && m.is_value(v)) { - prefix.push_back(v); - } - - // propagate all cases - expr_ref_vector cases(m); - expr_ref_vector branches(m); - for (auto [pre, post] : result) { - expr_ref mem_head(re().mk_in_re(head, pre), m); - expr_ref mem_tail(re().mk_in_re(tail, post), m); - cases.push_back(m.mk_and(mem_head, mem_tail)); - } - if (!result.failed()) { - const expr_ref cases_expr(m.mk_or(cases), m); - ctx.internalize(cases_expr, false); - th.propagate_lit(nullptr, 1, &lit, ctx.get_literal(cases_expr)); - return; - } - } - // fallthrough; decomposition failed - } + if (factor_membership(lit)) { + TRACE(seq_regex, tout << "factor membership\n"); + return; + } // Convert a non-ground sequence into an additional regex and // strengthen the original regex constraint into an intersection @@ -216,7 +165,6 @@ namespace smt { TRACE(seq, tout << "propagate " << acc << "\n";); - //th.propagate_lit(nullptr, 1, &lit, acc_lit); th.add_axiom(~lit, acc_lit); } @@ -419,6 +367,66 @@ namespace smt { true); } + bool seq_regex::factor_membership(literal lit) { + expr *s = nullptr, *r = nullptr; + expr *e = ctx.bool_var2expr(lit.var()); + VERIFY(str().is_in_re(e, s, r)); + // TODO - replace this with a propagator closure that gets invoked and removed on backtracking. + // it tracks + // an in_re2 literal is of the form in_re2(u, R1, v, R2) + // Assert in_re2(u, R1, v, R2) => u in R1 and v in R2 + // forward on split_set until there is a new in_re2 literal that is not already false. + // If there was an already created in_re2 literal that is true, + // then check that the propagation axiom is true + // if it isn't true, then assert it. + // if it is true, we are done + // If split_set is done and all in_re2 literals are false, there is a conflict. + // Assert the conflict clause lit => (or in_re2 literals) + // Final check also unfolds this axiomatization + // (we have to add a final check to seq_regex for this). + + if (!th.get_fparams().m_seq_regex_factorization_enabled) + return false; + + unsigned threshold = th.get_fparams().m_seq_regex_factorization_threshold; + expr_ref_vector prefix(m); + expr *hd, *tl, *v; + auto filter = [&](expr *p, expr *_q) -> bool { + expr_ref q(_q, m); + for (expr *v : prefix) { + q = seq_rw().mk_derivative(v, q); + if (re().is_empty(q)) + return false; + } + return re().is_empty(q); + }; + + split_set result(seq_rw(), r, threshold, filter); + + auto [head, tail] = result.try_split_sequence(s); + if (head && tail) { + tl = tail; + while (str().is_concat(tl, hd, tl) && str().is_unit(hd, v) && m.is_value(v)) + prefix.push_back(v); + + // propagate all cases + expr_ref_vector cases(m); + expr_ref_vector branches(m); + for (auto [pre, post] : result) { + expr_ref mem_head(re().mk_in_re(head, pre), m); + expr_ref mem_tail(re().mk_in_re(tail, post), m); + cases.push_back(m.mk_and(mem_head, mem_tail)); + } + if (!result.failed()) { + const expr_ref cases_expr(m.mk_or(cases), m); + ctx.internalize(cases_expr, false); + th.propagate_lit(nullptr, 1, &lit, ctx.get_literal(cases_expr)); + return true; + } + } + return false; + } + bool seq_regex::unfold_prefix(literal lit) { expr *s = nullptr, *r = nullptr; expr *e = ctx.bool_var2expr(lit.var()); diff --git a/src/smt/seq_regex.h b/src/smt/seq_regex.h index ff7b601b44..376c19a50d 100644 --- a/src/smt/seq_regex.h +++ b/src/smt/seq_regex.h @@ -21,6 +21,7 @@ Author: #include "ast/seq_decl_plugin.h" #include "ast/rewriter/seq_rewriter.h" #include "ast/rewriter/seq_skolem.h" +#include "ast/rewriter/seq_split.h" #include "smt/smt_context.h" /* @@ -91,6 +92,28 @@ Author: namespace smt { class theory_seq; + class seq_regex; + + // a split continuation is a closure that contains a split set + // and in_re2 literals that were extracted from a partial split. + // there are the following outcomes: + // 1. it was not possible to split:failed() + // 2. one of the in_re2 literals is true: in_re2(u, r1, v, r2) and in_re(u, r1), in_re(v, r2) are true + // 3. one of in_re2(u, r1, v, r2) is true: but in_re(u, r1) or in_re(v, r2) is undef or false. + // 4. all in_re2(u, r1, v, r2) are false: there is a next split from m_split -> add propagation axioms and set phase of in_re2. + // 5. all in_re2(u, r1, v, r2) are false: there is no next split from m_split -> conflict + // split continuations are assigned at scope level and map propagation literal lit to a split continuation. + // they are checked during propagation and during final check. + class split_cont { + split_set m_split; + expr_ref_vector m_in_re2; + public: + split_cont(seq_regex &r, literal lit); + bool failed() const; + bool is_sat(); + bool is_unsat(); + literal next_split(); + }; class seq_regex { // Data about a constraint of the form (str.in_re s R) @@ -153,6 +176,8 @@ namespace smt { bool unfold_prefix(literal lit); + bool factor_membership(literal lit); + expr_ref mk_first(expr* r, expr* n); bool is_member(expr* r, expr* u); From f30650b4b4910eda1333e36ccb160ecdcc6860f6 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Fri, 3 Jul 2026 11:21:38 -0700 Subject: [PATCH 08/24] bug fix Signed-off-by: Nikolaj Bjorner --- src/ast/rewriter/seq_split.cpp | 4 +- src/smt/seq_regex.cpp | 82 +++++++++++++++++++++++++++++++++- src/smt/seq_regex.h | 47 ++++++++++--------- 3 files changed, 108 insertions(+), 25 deletions(-) diff --git a/src/ast/rewriter/seq_split.cpp b/src/ast/rewriter/seq_split.cpp index df97e43aa8..d8963ce838 100644 --- a/src/ast/rewriter/seq_split.cpp +++ b/src/ast/rewriter/seq_split.cpp @@ -376,8 +376,8 @@ struct split_set::iterator::imp { } else if (seq.str.is_unit(a, b)) { auto eps = mk_eps(); - push_split(eps, a); - push_split(a, eps); + push_split(eps, r); + push_split(r, eps); } else if (seq.str.is_string(a, str)) { for (unsigned i = 0; i <= str.length(); ++i) { diff --git a/src/smt/seq_regex.cpp b/src/smt/seq_regex.cpp index 497000d461..d9844b31a0 100644 --- a/src/smt/seq_regex.cpp +++ b/src/smt/seq_regex.cpp @@ -26,6 +26,83 @@ Author: namespace smt { + seq_regex::split_cont::split_cont(seq_regex &sr, split_set &&ss, literal lit, expr *u, expr *v, expr *r) + : m_regex(sr), m_u(u), m_v(v), m_split(std::move(ss)), m_it(m_split.begin()), m_end(m_split.end()), + m_in_re2(sr.m), m_lit(lit) {} + + bool seq_regex::split_cont::failed() const { + return m_split.failed(); + } + bool seq_regex::split_cont::next_split() { + if (m_split.failed()) + return false; + auto &ctx = m_regex.ctx; + auto &re = m_regex.re(); + auto &m = m_regex.m; + literal lit_undef = null_literal; + for (auto e : m_in_re2) { + auto lit = m_regex.th.mk_literal(e); + auto rel = ctx.is_relevant(lit); + switch (ctx.get_assignment(lit)) { + case l_undef: + lit_undef = lit; + break; + case l_true: + if (!rel) + ctx.mark_as_relevant(lit); + return rel; + case l_false: + break; + } + if (lit_undef != null_literal) + break; + } + + if (lit_undef == null_literal) { + while (m_it != m_end) { + auto [pre, post] = *m_it; + auto a = re.mk_in_re(m_u, pre); + auto b = re.mk_in_re(m_v, post); + auto e = m.mk_and(a, b); + m_in_re2.push_back(e); + auto lit = m_regex.th.mk_literal(e); + auto rel = ctx.is_relevant(lit); + switch (ctx.get_assignment(lit)) { + case l_undef: lit_undef = lit; break; + case l_true: + if (!rel) + ctx.mark_as_relevant(lit); + return rel; + case l_false: break; + } + ++m_it; + if (lit_undef != null_literal) + break; + } + } + + if (m_split.failed()) + return false; + + if (lit_undef != null_literal) { + ctx.mark_as_relevant(lit_undef); + ctx.force_phase(lit_undef); + return true; + } + // all literals are false: + enode_pair_vector eqs; + literal_vector lits; + lits.push_back(m_lit); + for (auto e : m_in_re2) { + auto lit = m_regex.th.mk_literal(e); + SASSERT(ctx.get_assignment(lit) == l_false); + lits.push_back(~lit); + } + m_regex.th.set_conflict(eqs, lits); + return true; + } + + seq_regex::seq_regex(theory_seq& th): th(th), ctx(th.get_context()), @@ -368,6 +445,8 @@ namespace smt { } bool seq_regex::factor_membership(literal lit) { + if (!th.get_fparams().m_seq_regex_factorization_enabled) + return false; expr *s = nullptr, *r = nullptr; expr *e = ctx.bool_var2expr(lit.var()); VERIFY(str().is_in_re(e, s, r)); @@ -385,8 +464,7 @@ namespace smt { // Final check also unfolds this axiomatization // (we have to add a final check to seq_regex for this). - if (!th.get_fparams().m_seq_regex_factorization_enabled) - return false; + unsigned threshold = th.get_fparams().m_seq_regex_factorization_threshold; expr_ref_vector prefix(m); diff --git a/src/smt/seq_regex.h b/src/smt/seq_regex.h index 376c19a50d..2cb4db4d4c 100644 --- a/src/smt/seq_regex.h +++ b/src/smt/seq_regex.h @@ -94,27 +94,6 @@ namespace smt { class theory_seq; class seq_regex; - // a split continuation is a closure that contains a split set - // and in_re2 literals that were extracted from a partial split. - // there are the following outcomes: - // 1. it was not possible to split:failed() - // 2. one of the in_re2 literals is true: in_re2(u, r1, v, r2) and in_re(u, r1), in_re(v, r2) are true - // 3. one of in_re2(u, r1, v, r2) is true: but in_re(u, r1) or in_re(v, r2) is undef or false. - // 4. all in_re2(u, r1, v, r2) are false: there is a next split from m_split -> add propagation axioms and set phase of in_re2. - // 5. all in_re2(u, r1, v, r2) are false: there is no next split from m_split -> conflict - // split continuations are assigned at scope level and map propagation literal lit to a split continuation. - // they are checked during propagation and during final check. - class split_cont { - split_set m_split; - expr_ref_vector m_in_re2; - public: - split_cont(seq_regex &r, literal lit); - bool failed() const; - bool is_sat(); - bool is_unsat(); - literal next_split(); - }; - class seq_regex { // Data about a constraint of the form (str.in_re s R) struct s_in_re { @@ -126,6 +105,32 @@ namespace smt { m_lit(l), m_s(s), m_re(r), m_active(true) {} }; + // a split continuation is a closure that contains a split set + // and in_re2 literals that were extracted from a partial split. + // there are the following outcomes: + // 1. it was not possible to split:failed() + // 2. one of the in_re2 literals is true: in_re2(u, r1, v, r2) and in_re(u, r1), in_re(v, r2) are true + // 3. one of in_re2(u, r1, v, r2) is true: but in_re(u, r1) or in_re(v, r2) is undef or false. + // 4. all in_re2(u, r1, v, r2) are false: there is a next split from m_split -> add propagation axioms and set + // phase of in_re2. + // 5. all in_re2(u, r1, v, r2) are false: there is no next split from m_split -> conflict + // split continuations are assigned at scope level and map propagation literal lit to a split continuation. + // they are checked during propagation and during final check. + class split_cont { + seq_regex &m_regex; + split_set m_split; + expr *m_u, *m_v, *m_r; + split_set::iterator m_it; + split_set::iterator m_end; + expr_ref_vector m_in_re2; + literal m_lit; + + public: + split_cont(seq_regex &sr, split_set&& ss, literal lit, expr* u, expr* v, expr* r); + bool failed() const; + bool next_split(); + }; + theory_seq& th; context& ctx; ast_manager& m; From 1c11526d640773dd43780966a4bcd449d1af9365 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Fri, 3 Jul 2026 11:41:37 -0700 Subject: [PATCH 09/24] fix propagation of failure Signed-off-by: Nikolaj Bjorner --- src/ast/rewriter/seq_split.cpp | 5 ++--- src/smt/seq_regex.cpp | 2 +- 2 files changed, 3 insertions(+), 4 deletions(-) diff --git a/src/ast/rewriter/seq_split.cpp b/src/ast/rewriter/seq_split.cpp index d8963ce838..452bdc420e 100644 --- a/src/ast/rewriter/seq_split.cpp +++ b/src/ast/rewriter/seq_split.cpp @@ -90,7 +90,7 @@ struct split_set::iterator::imp { next(); } if (b_it.failed() || a_it.failed()) - parent().m_failure = true; + parent().set_failure(); } }; @@ -206,8 +206,6 @@ struct split_set::iterator::imp { } void consume() override { - if (at_end()) - return; while (!parent().has_split() && !at_end() && !a_it.failed() && !b_it.failed()) { if (a_it == a_end) { auto [p, q] = *b_it; @@ -335,6 +333,7 @@ struct split_set::iterator::imp { } void unfold(expr* r) { + TRACE(seq, tout << "unfold " << mk_pp(r, m) << "\n"); SASSERT(seq.is_re(r)); if (re.is_empty(r)) return; diff --git a/src/smt/seq_regex.cpp b/src/smt/seq_regex.cpp index d9844b31a0..9f2dbd32c9 100644 --- a/src/smt/seq_regex.cpp +++ b/src/smt/seq_regex.cpp @@ -523,7 +523,7 @@ namespace smt { if (re().is_empty(q)) { enode_pair_vector eqs; literal_vector lits; - lits.push_back(~lit); + lits.push_back(lit); th.set_conflict(eqs, lits); return true; } From 4a52f32c6b01c571f2dbbc8a7cdba1380e283bcc Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Fri, 3 Jul 2026 11:58:22 -0700 Subject: [PATCH 10/24] update Signed-off-by: Nikolaj Bjorner --- src/smt/seq_regex.h | 7 +++---- src/smt/theory_seq.cpp | 10 +++------- 2 files changed, 6 insertions(+), 11 deletions(-) diff --git a/src/smt/seq_regex.h b/src/smt/seq_regex.h index 2cb4db4d4c..1ac21e37ef 100644 --- a/src/smt/seq_regex.h +++ b/src/smt/seq_regex.h @@ -225,10 +225,9 @@ namespace smt { seq_regex(theory_seq& th); - void push_scope() {} - void pop_scope(unsigned num_scopes) {} - bool can_propagate() const { return false; } - bool propagate() const { return false; } + bool final_check() { + return true; + } void propagate_in_re(literal lit); diff --git a/src/smt/theory_seq.cpp b/src/smt/theory_seq.cpp index 5357814d34..69e625093a 100644 --- a/src/smt/theory_seq.cpp +++ b/src/smt/theory_seq.cpp @@ -341,8 +341,8 @@ final_check_status theory_seq::final_check_eh(unsigned level) { TRACEFIN("solve_nqs"); return FC_CONTINUE; } - if (m_regex.propagate()) { - TRACEFIN("regex propagate"); + if (!m_regex.final_check()) { + TRACEFIN("regex final check"); return FC_CONTINUE; } if (check_fixed_length(true, false)) { @@ -2473,7 +2473,7 @@ theory_var theory_seq::mk_var(enode* n) { } bool theory_seq::can_propagate() { - return m_axioms_head < m_axioms.size() || !m_replay.empty() || m_new_solution || m_regex.can_propagate(); + return m_axioms_head < m_axioms.size() || !m_replay.empty() || m_new_solution; } bool theory_seq::canonize(expr* e, dependency*& eqs, expr_ref& result) { @@ -2689,8 +2689,6 @@ void theory_seq::add_dependency(dependency*& dep, enode* a, enode* b) { void theory_seq::propagate() { - if (m_regex.can_propagate()) - m_regex.propagate(); while (m_axioms_head < m_axioms.size() && !ctx.inconsistent()) { expr_ref e(m); e = m_axioms.get(m_axioms_head); @@ -3261,7 +3259,6 @@ void theory_seq::push_scope_eh() { m_ncs.push_scope(); m_lts.push_scope(); m_recfuns.push_scope(); - m_regex.push_scope(); } void theory_seq::pop_scope_eh(unsigned num_scopes) { @@ -3275,7 +3272,6 @@ void theory_seq::pop_scope_eh(unsigned num_scopes) { m_ncs.pop_scope(num_scopes); m_lts.pop_scope(num_scopes); m_recfuns.pop_scope(num_scopes); - m_regex.pop_scope(num_scopes); m_rewrite.reset(); if (ctx.get_base_level() > ctx.get_scope_level() - num_scopes) { m_replay.reset(); From 3abdf5928a5b071ce1592313263fe1bca1d9c324 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Fri, 3 Jul 2026 12:23:20 -0700 Subject: [PATCH 11/24] fixing unsoundness in concat rule Signed-off-by: Nikolaj Bjorner --- src/ast/rewriter/seq_split.cpp | 15 +++++++++------ 1 file changed, 9 insertions(+), 6 deletions(-) diff --git a/src/ast/rewriter/seq_split.cpp b/src/ast/rewriter/seq_split.cpp index 452bdc420e..92fa5f3747 100644 --- a/src/ast/rewriter/seq_split.cpp +++ b/src/ast/rewriter/seq_split.cpp @@ -36,6 +36,7 @@ struct split_set::imp { if (r) { VERIFY(seq.is_re(r, m_seq_sort)); m_re_sort = r->get_sort(); + TRACE(seq, tout << "split_set::imp: " << this << " " << mk_pp(r, m) << " threshold: " << m_threshold << "\n"); } if (m_threshold == 0) m_threshold = UINT_MAX; @@ -214,8 +215,7 @@ struct split_set::iterator::imp { } else { auto [p, q] = *a_it; - if (!parent().re.is_epsilon(q)) - parent().push_split(p, parent().i.rw.mk_re_append(q, b)); + parent().push_split(p, parent().i.rw.mk_re_append(q, b)); ++a_it; } } @@ -237,10 +237,12 @@ struct split_set::iterator::imp { bool m_at_end; bool m_failure = false; imp(split_set &s, bool at_end) : s(s), i(*s.m_imp), m(i.m), seq(i.seq), re(i.re), m_cont(m), m_at_end(at_end) { - if (i.r) { + if (at_end) + m_init = true; + else if (i.r) { m_cont.push_back(i.r); init(); - } + } } void set_failure() { @@ -268,7 +270,7 @@ struct split_set::iterator::imp { void next() { m_init = true; - while (!at_end()) { + while (!m_failure && !m_at_end) { if (has_split()) return; if (m_consumer) { @@ -451,7 +453,8 @@ struct split_set::iterator::imp { } bool at_end() const { - return m_failure || m_at_end; + TRACE(seq, tout << "split_set::iterator::at_end: " << this << " " << m_at_end << " " << m_qhead << "/" << m_splits.size() << "\n"); + return m_failure || (m_at_end && m_qhead == m_splits.size()); } }; From b095adfa815fd69e14195431b738b553a3901e96 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Fri, 3 Jul 2026 12:24:06 -0700 Subject: [PATCH 12/24] fixing unsoundness in concat rule Signed-off-by: Nikolaj Bjorner --- src/ast/rewriter/seq_split.cpp | 2 -- 1 file changed, 2 deletions(-) diff --git a/src/ast/rewriter/seq_split.cpp b/src/ast/rewriter/seq_split.cpp index 92fa5f3747..63cad62564 100644 --- a/src/ast/rewriter/seq_split.cpp +++ b/src/ast/rewriter/seq_split.cpp @@ -36,7 +36,6 @@ struct split_set::imp { if (r) { VERIFY(seq.is_re(r, m_seq_sort)); m_re_sort = r->get_sort(); - TRACE(seq, tout << "split_set::imp: " << this << " " << mk_pp(r, m) << " threshold: " << m_threshold << "\n"); } if (m_threshold == 0) m_threshold = UINT_MAX; @@ -453,7 +452,6 @@ struct split_set::iterator::imp { } bool at_end() const { - TRACE(seq, tout << "split_set::iterator::at_end: " << this << " " << m_at_end << " " << m_qhead << "/" << m_splits.size() << "\n"); return m_failure || (m_at_end && m_qhead == m_splits.size()); } }; From 52e6f885b933c9a1fcf4a059b2cef4361aeb33c5 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Fri, 3 Jul 2026 19:31:29 -0700 Subject: [PATCH 13/24] bug fixes to split-set Signed-off-by: Nikolaj Bjorner --- src/ast/rewriter/seq_split.cpp | 66 ++++++++++++++++------------------ src/ast/rewriter/seq_split.h | 2 ++ src/smt/seq_regex.cpp | 4 +-- src/smt/seq_regex.h | 2 +- 4 files changed, 35 insertions(+), 39 deletions(-) diff --git a/src/ast/rewriter/seq_split.cpp b/src/ast/rewriter/seq_split.cpp index 63cad62564..eba15111c9 100644 --- a/src/ast/rewriter/seq_split.cpp +++ b/src/ast/rewriter/seq_split.cpp @@ -81,6 +81,7 @@ struct split_set::iterator::imp { } } void consume() override { + TRACE(seq, tout << "intersection consume\n"); while (!at_end() && !parent().has_split()) { auto [a1, a2] = *a_it; auto [b1, b2] = *b_it; @@ -146,6 +147,7 @@ struct split_set::iterator::imp { } void consume() override { + TRACE(seq, tout << "complement consume\n"); init(); if (m_intersection) m_intersection->consume(); @@ -161,6 +163,7 @@ struct split_set::iterator::imp { : a_s(std::move(a_src)), a_it(a_s.begin()), a_end(a_s.end()), b(b, a_s.m_imp->m) {} void consume() override { + TRACE(seq, tout << "concat_left consume\n"); while (a_it != a_end && !parent().has_split()) { auto [p, q] = *a_it; parent().push_split(p, parent().i.rw.mk_re_append(q, b)); @@ -179,6 +182,7 @@ struct split_set::iterator::imp { concat_right(expr* a, split_set&& b_src) : a(a, b_src.m_imp->m), b_s(std::move(b_src)), b_it(b_s.begin()), b_end(b_s.end()) {} void consume() override { + TRACE(seq, tout << "concat_right consume\n"); while (b_it != b_end && !parent().has_split()) { auto [p, q] = *b_it; parent().push_split(parent().i.rw.mk_re_append(a, p), q); @@ -206,7 +210,9 @@ struct split_set::iterator::imp { } void consume() override { + TRACE(seq, tout << "concat-start: " << mk_pp(a, parent().i.m) << " " << mk_pp(b, parent().i.m) << "\n"); while (!parent().has_split() && !at_end() && !a_it.failed() && !b_it.failed()) { + TRACE(seq, tout << "concat: " << mk_pp(a, parent().i.m) << " " << mk_pp(b, parent().i.m) << "\n"); if (a_it == a_end) { auto [p, q] = *b_it; parent().push_split(parent().i.rw.mk_re_append(a, p), q); @@ -233,9 +239,10 @@ struct split_set::iterator::imp { bool m_init = false; unsigned m_qhead = 0; scoped_ptr m_consumer; - bool m_at_end; + bool m_end_marker; + bool m_at_end = false; bool m_failure = false; - imp(split_set &s, bool at_end) : s(s), i(*s.m_imp), m(i.m), seq(i.seq), re(i.re), m_cont(m), m_at_end(at_end) { + imp(split_set &s, bool at_end) : s(s), i(*s.m_imp), m(i.m), seq(i.seq), re(i.re), m_cont(m), m_end_marker(at_end) { if (at_end) m_init = true; else if (i.r) { @@ -255,6 +262,7 @@ struct split_set::iterator::imp { } void rewind() { + TRACE(seq, tout << "rewind: " << m_splits.size() << "\n";); m_qhead = 0; m_at_end = m_qhead == m_splits.size(); SASSERT(m_cont.empty()); @@ -292,7 +300,6 @@ struct split_set::iterator::imp { void push_split(expr *_a, expr *_b) { expr_ref a(_a, m), b(_b, m); - if (m_failure) return; if (i.m_filter && !i.m_filter(a, b)) @@ -364,6 +371,7 @@ struct split_set::iterator::imp { } if (re.is_concat(r, a, b)) { + TRACE(seq, tout << "concat-start: " << mk_pp(a, i.m) << " " << mk_pp(b, i.m) << "\n"); m_consumer = alloc(concat, i.rw, a, b, i.m_threshold); m_consumer->set_parent(*this); return; @@ -452,7 +460,7 @@ struct split_set::iterator::imp { } bool at_end() const { - return m_failure || (m_at_end && m_qhead == m_splits.size()); + return m_failure || m_end_marker || (m_at_end && m_qhead == m_splits.size()); } }; @@ -512,29 +520,15 @@ std::pair split_set::try_split_sequence(expr *str) { ast_manager &m = m_imp->m; auto &seq = m_imp->seq; + if (!seq.str.is_concat(str)) + return {expr_ref(m), expr_ref(m)}; expr_ref_vector tokens(m); - vector stack; - stack.push_back(str); - - while (!stack.empty()) { - expr *cur = stack.back(); - stack.pop_back(); - expr *l, *r; - if (seq.str.is_concat(cur, l, r)) { - stack.push_back(r); - stack.push_back(l); - } - else - tokens.push_back(expr_ref(cur, m)); - } + seq.str.get_concat(str, tokens); + SASSERT(tokens.size() > 1); expr *ch; unsigned i = 0; - // TODO: Do this for the back as well (also, why did no rule before do that?) - - if (tokens.empty()) - return {expr_ref(m), expr_ref(m)}; // Choose the factorization boundary so the tail starts with the // longest run of concrete characters c. @@ -543,12 +537,12 @@ std::pair split_set::try_split_sequence(expr *str) { const unsigned total = tokens.size(); unsigned run_start = 0, run_len = 0; for (i = 1; i < total;) { - if (!(seq.str.is_unit(tokens.get(i), ch) && seq.is_const_char(ch))) { + if (!(seq.str.is_unit(tokens.get(i), ch) && m.is_value(ch))) { i++; continue; } unsigned j = i; - while (j < total && seq.str.is_unit(tokens.get(j), ch) && seq.is_const_char(ch)) { + while (j < total && seq.str.is_unit(tokens.get(j), ch) && m.is_value(ch)) { j++; } if (j - i > run_len) { @@ -560,16 +554,16 @@ std::pair split_set::try_split_sequence(expr *str) { // No constant run => fall back to splitting off the first token. const unsigned p = run_len == 0 ? 1 : run_start; SASSERT(p >= 1); - expr *head = tokens.get(0); - for (i = 1; i < p; i++) { - head = seq.str.mk_concat(head, tokens.get(i)); - } - expr *tail = seq.str.mk_empty(head->get_sort()); - if (tokens.size() > p + run_len) { - tail = tokens.get(p + run_len); - for (i = p + run_len + 1; i < tokens.size(); i++) { - tail = seq.str.mk_concat(tail, tokens.get(i)); - } - } - return {expr_ref(head, m), expr_ref(tail, m)}; + SASSERT(p < total); + expr_ref head(tokens.get(p - 1), m); + for (unsigned i = p - 1; i-- > 0;) + head = seq.str.mk_concat(tokens.get(i), head); + + expr_ref tail(tokens.back(), m); + for (unsigned i = tokens.size() - 1; i-- > p;) + tail = seq.str.mk_concat(tokens.get(i), tail); + + TRACE(seq, tout << "split_set::try_split_sequence: " << mk_pp(str, m) << " -> " << head << " | " + << tail << "\n"); + return { head, tail }; } diff --git a/src/ast/rewriter/seq_split.h b/src/ast/rewriter/seq_split.h index 9746b07dc7..20ad0a452b 100644 --- a/src/ast/rewriter/seq_split.h +++ b/src/ast/rewriter/seq_split.h @@ -51,6 +51,8 @@ public: split_set(split_set&& other) noexcept; + split_set &operator=(split_set const &other) = delete; + class iterator { struct imp; imp *m_imp; diff --git a/src/smt/seq_regex.cpp b/src/smt/seq_regex.cpp index 9f2dbd32c9..b2f038bbcf 100644 --- a/src/smt/seq_regex.cpp +++ b/src/smt/seq_regex.cpp @@ -27,7 +27,7 @@ Author: namespace smt { seq_regex::split_cont::split_cont(seq_regex &sr, split_set &&ss, literal lit, expr *u, expr *v, expr *r) - : m_regex(sr), m_u(u), m_v(v), m_split(std::move(ss)), m_it(m_split.begin()), m_end(m_split.end()), + : m_regex(sr), m_u(u, sr.m), m_v(v, sr.m), m_r(r, sr.m), m_split(std::move(ss)), m_it(m_split.begin()), m_end(m_split.end()), m_in_re2(sr.m), m_lit(lit) {} bool seq_regex::split_cont::failed() const { @@ -476,7 +476,7 @@ namespace smt { if (re().is_empty(q)) return false; } - return re().is_empty(q); + return !re().is_empty(q); }; split_set result(seq_rw(), r, threshold, filter); diff --git a/src/smt/seq_regex.h b/src/smt/seq_regex.h index 1ac21e37ef..016c8da813 100644 --- a/src/smt/seq_regex.h +++ b/src/smt/seq_regex.h @@ -119,7 +119,7 @@ namespace smt { class split_cont { seq_regex &m_regex; split_set m_split; - expr *m_u, *m_v, *m_r; + expr_ref m_u, m_v, m_r; split_set::iterator m_it; split_set::iterator m_end; expr_ref_vector m_in_re2; From d19f19c5d657fa663e7490861e59cf5f16f9a96b Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Fri, 3 Jul 2026 19:50:19 -0700 Subject: [PATCH 14/24] bug fix Signed-off-by: Nikolaj Bjorner --- src/smt/seq_regex.cpp | 7 ++++--- 1 file changed, 4 insertions(+), 3 deletions(-) diff --git a/src/smt/seq_regex.cpp b/src/smt/seq_regex.cpp index b2f038bbcf..c4005f9857 100644 --- a/src/smt/seq_regex.cpp +++ b/src/smt/seq_regex.cpp @@ -510,9 +510,10 @@ namespace smt { expr *e = ctx.bool_var2expr(lit.var()); VERIFY(str().is_in_re(e, s, r)); expr_ref_vector prefix(m); - expr *hd, *v, *tl = s; - while (str().is_concat(tl, hd, tl) && str().is_unit(hd, v) && m.is_value(v)) - prefix.push_back(v); + expr *hd, *v, *tl = s, *tl1; + while (str().is_concat(tl, hd, tl1) && str().is_unit(hd, v) && m.is_value(v)) + prefix.push_back(v), + tl = tl1; if (prefix.empty()) return false; From 7d75e6f40a21d3fe5170e74a072e2acf7f1666d8 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Fri, 3 Jul 2026 22:53:38 -0700 Subject: [PATCH 15/24] hunt for non-constants Signed-off-by: Nikolaj Bjorner --- src/smt/seq_regex.cpp | 2 ++ 1 file changed, 2 insertions(+) diff --git a/src/smt/seq_regex.cpp b/src/smt/seq_regex.cpp index c4005f9857..166f12096a 100644 --- a/src/smt/seq_regex.cpp +++ b/src/smt/seq_regex.cpp @@ -515,6 +515,8 @@ namespace smt { prefix.push_back(v), tl = tl1; + VERIFY(!(str().is_concat(tl, hd, tl1) && str().is_unit(hd))); + if (prefix.empty()) return false; From 00ee1ca75c4c6acb92c09d3c47e83033acdfd4cd Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Fri, 3 Jul 2026 23:24:58 -0700 Subject: [PATCH 16/24] restructure Signed-off-by: Nikolaj Bjorner --- src/smt/seq_regex.cpp | 126 +++++++++++++++++------------------------- src/smt/seq_regex.h | 12 ++-- 2 files changed, 58 insertions(+), 80 deletions(-) diff --git a/src/smt/seq_regex.cpp b/src/smt/seq_regex.cpp index 166f12096a..e466e56178 100644 --- a/src/smt/seq_regex.cpp +++ b/src/smt/seq_regex.cpp @@ -132,11 +132,9 @@ namespace smt { * s = x ++ y and x in R and y in Q */ - bool seq_regex::is_string_equality(literal lit) { - expr* s = nullptr, *r = nullptr; + bool seq_regex::is_string_equality(literal lit, expr* s, expr* r) { expr* e = ctx.bool_var2expr(lit.var()); expr_ref id(a().mk_int(e->get_id()), m); - VERIFY(str().is_in_re(e, s, r)); sort* seq_sort = s->get_sort(); vector patterns; auto mk_cont = [&](unsigned idx) { @@ -191,31 +189,34 @@ namespace smt { return; } - if (unfold_prefix(lit)) { + if (unfold_prefix(lit, s, r)) { TRACE(seq_regex, tout << "unfolded prefix" << std::endl;); STRACE(seq_regex_brief, tout << "unfold_prefix ";); return; } - if (coallesce_in_re(lit)) { - TRACE(seq_regex, tout - << "simplified conjunctions to an intersection" << std::endl;); - STRACE(seq_regex_brief, tout << "coallesce_in_re ";); - return; - } - - if (is_string_equality(lit)) { + if (is_string_equality(lit, s, r)) { TRACE(seq_regex, tout << "simplified regex using string equality" << std::endl;); STRACE(seq_regex_brief, tout << "string_eq ";); return; } - if (factor_membership(lit)) { + if (factor_ite(lit, s, r)) { + TRACE(seq_regex, tout << "factored ite in regex" << std::endl;); + STRACE(seq_regex_brief, tout << "factor_ite ";); + return; + } + + if (factor_membership(lit, s, r)) { TRACE(seq_regex, tout << "factor membership\n"); return; } + initialize_accept(lit, s, r); + } + + void seq_regex::initialize_accept(literal lit, expr *s, expr *r) { // Convert a non-ground sequence into an additional regex and // strengthen the original regex constraint into an intersection // for example: @@ -228,11 +229,9 @@ namespace smt { if (!re().is_full_seq(s_approx)) { r = re().mk_inter(r, s_approx); _r_temp_owner = r; - TRACE(seq_regex, tout - << "get_overapprox_regex(" << mk_pp(s, m) - << ") = " << mk_pp(s_approx, m) << std::endl;); - STRACE(seq_regex_brief, tout - << "overapprox=" << state_str(r) << " ";); + TRACE(seq_regex, + tout << "get_overapprox_regex(" << mk_pp(s, m) << ") = " << mk_pp(s_approx, m) << std::endl;); + STRACE(seq_regex_brief, tout << "overapprox=" << state_str(r) << " ";); } } @@ -444,12 +443,10 @@ namespace smt { true); } - bool seq_regex::factor_membership(literal lit) { + bool seq_regex::factor_membership(literal lit, expr* s, expr* r) { if (!th.get_fparams().m_seq_regex_factorization_enabled) return false; - expr *s = nullptr, *r = nullptr; - expr *e = ctx.bool_var2expr(lit.var()); - VERIFY(str().is_in_re(e, s, r)); + // TODO - replace this with a propagator closure that gets invoked and removed on backtracking. // it tracks // an in_re2 literal is of the form in_re2(u, R1, v, R2) @@ -505,18 +502,39 @@ namespace smt { return false; } - bool seq_regex::unfold_prefix(literal lit) { - expr *s = nullptr, *r = nullptr; - expr *e = ctx.bool_var2expr(lit.var()); - VERIFY(str().is_in_re(e, s, r)); + + bool seq_regex::factor_ite(literal lit, expr* s, expr* r) { + bool_rewriter br(m); + expr_ref c(m), t(m), e(m); + if (!br.decompose_ite(r, c, t, e)) + return false; + auto c_lit = th.mk_literal(c); + switch (ctx.get_assignment(c_lit)) { + case l_true: { + literal lits[2] = {lit, c_lit}; + th.propagate_lit(nullptr, 2, lits, th.mk_literal(re().mk_in_re(s, t))); + break; + } + case l_false: { + literal lits[2] = {lit, ~c_lit}; + th.propagate_lit(nullptr, 2, lits, th.mk_literal(re().mk_in_re(s, e))); + break; + } + case l_undef: { + ctx.mark_as_relevant(c_lit); + break; + } + } + return true; + } + + bool seq_regex::unfold_prefix(literal lit, expr* s, expr* r) { expr_ref_vector prefix(m); expr *hd, *v, *tl = s, *tl1; - while (str().is_concat(tl, hd, tl1) && str().is_unit(hd, v) && m.is_value(v)) + while (str().is_concat(tl, hd, tl1) && str().is_unit(hd, v)) prefix.push_back(v), tl = tl1; - VERIFY(!(str().is_concat(tl, hd, tl1) && str().is_unit(hd))); - if (prefix.empty()) return false; @@ -538,58 +556,16 @@ namespace smt { return true; } - /** - * Combine a conjunction of membership relations for the same string - * within the same Regex. - */ - bool seq_regex::coallesce_in_re(literal lit) { - return false; // disabled - expr* s = nullptr, *r = nullptr; - expr* e = ctx.bool_var2expr(lit.var()); - VERIFY(str().is_in_re(e, s, r)); - expr_ref regex(r, m); - literal_vector lits; - for (unsigned i = 0; i < m_s_in_re.size(); ++i) { - auto const& entry = m_s_in_re[i]; - if (!entry.m_active) - continue; - enode* n1 = th.ensure_enode(entry.m_s); - enode* n2 = th.ensure_enode(s); - if (n1->get_root() != n2->get_root()) - continue; - if (entry.m_re == regex) - continue; - - th.m_trail_stack.push(vector_value_trail(m_s_in_re, i)); - m_s_in_re[i].m_active = false; - IF_VERBOSE(11, verbose_stream() << "Intersect " << regex << " " << - mk_pp(entry.m_re, m) << " " << mk_pp(s, m) << " " << mk_pp(entry.m_s, m) << std::endl;); - regex = re().mk_inter(entry.m_re, regex); - rewrite(regex); - lits.push_back(~entry.m_lit); - if (n1 != n2) - lits.push_back(~th.mk_eq(n1->get_expr(), n2->get_expr(), false)); - } - m_s_in_re.push_back(s_in_re(lit, s, regex)); - th.get_trail_stack().push(push_back_vector>(m_s_in_re)); - if (lits.empty()) - return false; - lits.push_back(~lit); - lits.push_back(th.mk_literal(re().mk_in_re(s, regex))); - th.add_axiom(lits); - return true; - } - expr_ref seq_regex::symmetric_diff(expr* r1, expr* r2) { expr_ref r(m); if (r1 == r2) r = re().mk_empty(r1->get_sort()); - else if (re().is_empty(r1)) + else if (re().is_empty(r1)) r = r2; else if (re().is_empty(r2)) r = r1; - else - r = re().mk_union(re().mk_diff(r1, r2), re().mk_diff(r2, r1)); + else + r = re().mk_xor(r1, r2); rewrite(r); return r; } @@ -705,7 +681,6 @@ namespace smt { STRACE(seq_regex_brief, tout << "PNEQ ";); sort* seq_sort = nullptr; VERIFY(u().is_re(r1, seq_sort)); - expr_ref r = symmetric_diff(r1, r2); if (is_ground(r1) && is_ground(r2)) { seq::regex_bisim bisim(seq_rw()); switch (bisim.are_equivalent(r1, r2)) { @@ -720,6 +695,7 @@ namespace smt { break; } } + auto r = symmetric_diff(r1, r2); expr_ref emp(re().mk_empty(r->get_sort()), m); expr_ref n(m.mk_fresh_const("re.char", seq_sort), m); expr_ref is_non_empty = sk().mk_is_non_empty(r, r, n); diff --git a/src/smt/seq_regex.h b/src/smt/seq_regex.h index 016c8da813..914a21d0a3 100644 --- a/src/smt/seq_regex.h +++ b/src/smt/seq_regex.h @@ -168,20 +168,22 @@ namespace smt { seq::skolem& sk(); arith_util& a(); - bool is_string_equality(literal lit); + bool is_string_equality(literal lit, expr* s, expr* r); // Get a regex which overapproximates a given string expr_ref get_overapprox_regex(expr* s); void rewrite(expr_ref& e); - bool coallesce_in_re(literal lit); - bool block_unfolding(literal lit, unsigned i); - bool unfold_prefix(literal lit); + bool unfold_prefix(literal lit, expr* s, expr* r); - bool factor_membership(literal lit); + bool factor_membership(literal lit, expr* s, expr* r); + + bool factor_ite(literal lit, expr* s, expr* r); + + void initialize_accept(literal lit, expr *s, expr *r); expr_ref mk_first(expr* r, expr* n); From 71f30149572f6ad0c0f4173163564dcd580f22b3 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Fri, 3 Jul 2026 23:58:13 -0700 Subject: [PATCH 17/24] na Signed-off-by: Nikolaj Bjorner --- src/ast/rewriter/seq_split.cpp | 2 - src/smt/seq_regex.cpp | 83 +++++++++++++++++++++++++--------- src/smt/seq_regex.h | 21 +++------ 3 files changed, 69 insertions(+), 37 deletions(-) diff --git a/src/ast/rewriter/seq_split.cpp b/src/ast/rewriter/seq_split.cpp index eba15111c9..be320cb74d 100644 --- a/src/ast/rewriter/seq_split.cpp +++ b/src/ast/rewriter/seq_split.cpp @@ -210,9 +210,7 @@ struct split_set::iterator::imp { } void consume() override { - TRACE(seq, tout << "concat-start: " << mk_pp(a, parent().i.m) << " " << mk_pp(b, parent().i.m) << "\n"); while (!parent().has_split() && !at_end() && !a_it.failed() && !b_it.failed()) { - TRACE(seq, tout << "concat: " << mk_pp(a, parent().i.m) << " " << mk_pp(b, parent().i.m) << "\n"); if (a_it == a_end) { auto [p, q] = *b_it; parent().push_split(parent().i.rw.mk_re_append(a, p), q); diff --git a/src/smt/seq_regex.cpp b/src/smt/seq_regex.cpp index e466e56178..289ca5e0f8 100644 --- a/src/smt/seq_regex.cpp +++ b/src/smt/seq_regex.cpp @@ -172,39 +172,22 @@ namespace smt { VERIFY(str().is_in_re(e, s, r)); TRACE(seq_regex, tout << "propagate in RE: " << lit.sign() << " " << mk_pp(e, m) << std::endl;); - STRACE(seq_regex_brief, tout << "PIR(" << mk_pp(s, m) << "," - << state_str(r) << ") ";); - // convert negative negative membership literals to positive - // ~(s in R) => s in C(R) - if (lit.sign()) { - expr_ref fml(re().mk_in_re(s, re().mk_complement(r)), m); - rewrite(fml); - literal nlit = th.mk_literal(fml); - if (lit == nlit) { - // is-nullable doesn't simplify for regexes with uninterpreted subterms - th.add_unhandled_expr(fml); - } - th.propagate_lit(nullptr, 1, &lit, nlit); + if (unfold_complement(lit, s, r)) return; - } if (unfold_prefix(lit, s, r)) { - TRACE(seq_regex, tout << "unfolded prefix" << std::endl;); - STRACE(seq_regex_brief, tout << "unfold_prefix ";); + TRACE(seq_regex, tout << "unfolded prefix\n"); return; } if (is_string_equality(lit, s, r)) { - TRACE(seq_regex, tout - << "simplified regex using string equality" << std::endl;); - STRACE(seq_regex_brief, tout << "string_eq ";); + TRACE(seq_regex, tout << "simplified regex using string equality\n"); return; } if (factor_ite(lit, s, r)) { - TRACE(seq_regex, tout << "factored ite in regex" << std::endl;); - STRACE(seq_regex_brief, tout << "factor_ite ";); + TRACE(seq_regex, tout << "factored ite in regex\n"); return; } @@ -502,6 +485,64 @@ namespace smt { return false; } + bool seq_regex::final_check() { + + return true; + + // sketch: + // + // check registered seq_cont if more case splits are needed. + // check registered atomic regex membership for membership + // fallback to initialize_accept? + + expr *x = nullptr, *r = nullptr; + bool done = true; + for (auto s : m_split_conts) { + if (s->failed()) + ; + else if (s->next_split()) + done = false; + else if (s->failed()) { + done = false; + + expr *e = ctx.bool_var2expr(s->lit().var()); + VERIFY(str().is_in_re(e, x, r)); + initialize_accept(s->lit(), x, r); + } + else + ; // some split literal is true + } + obj_map> var2regex; + for (auto lit : m_atomic_memberships) { + expr *e = ctx.bool_var2expr(lit.var()); + VERIFY(str().is_in_re(e, x, r)); + var2regex.insert_if_not_there(x, ptr_vector()).push_back(r); + } + for (auto const &[x, regexes] : var2regex) { + // synthesize a solution within intersection of regexes. + // if intersection is empty, report conflict. + // add guardrails for solution satisfying current length assignment to x + // if solution does not satisfy length constraints initialize_accept instead of retaining atomic + + } + return done; + } + + bool seq_regex::unfold_complement(literal lit, expr *s, expr *r) { + if (!lit.sign()) + return false; + // convert negative negative membership literals to positive + // ~(s in R) => s in C(R) + expr_ref fml(re().mk_in_re(s, re().mk_complement(r)), m); + rewrite(fml); + literal nlit = th.mk_literal(fml); + if (lit == nlit) { + // is-nullable doesn't simplify for regexes with uninterpreted subterms + th.add_unhandled_expr(fml); + } + th.propagate_lit(nullptr, 1, &lit, nlit); + return true; + } bool seq_regex::factor_ite(literal lit, expr* s, expr* r) { bool_rewriter br(m); diff --git a/src/smt/seq_regex.h b/src/smt/seq_regex.h index 914a21d0a3..43320fab7c 100644 --- a/src/smt/seq_regex.h +++ b/src/smt/seq_regex.h @@ -95,17 +95,8 @@ namespace smt { class seq_regex; class seq_regex { - // Data about a constraint of the form (str.in_re s R) - struct s_in_re { - literal m_lit; - expr* m_s; - expr* m_re; - bool m_active; - s_in_re(literal l, expr* s, expr* r): - m_lit(l), m_s(s), m_re(r), m_active(true) {} - }; - // a split continuation is a closure that contains a split set + // a split continuation is a closure that contains a split set // and in_re2 literals that were extracted from a partial split. // there are the following outcomes: // 1. it was not possible to split:failed() @@ -129,13 +120,15 @@ namespace smt { split_cont(seq_regex &sr, split_set&& ss, literal lit, expr* u, expr* v, expr* r); bool failed() const; bool next_split(); + literal lit() const { return m_lit; } }; theory_seq& th; context& ctx; ast_manager& m; - vector m_s_in_re; + ptr_vector m_split_conts; // split continuations + literal_vector m_atomic_memberships; // str.in_re X r, where X is a variable /* state_graph for dead state detection, and associated methods */ @@ -179,6 +172,8 @@ namespace smt { bool unfold_prefix(literal lit, expr* s, expr* r); + bool unfold_complement(literal lit, expr *s, expr *r); + bool factor_membership(literal lit, expr* s, expr* r); bool factor_ite(literal lit, expr* s, expr* r); @@ -227,9 +222,7 @@ namespace smt { seq_regex(theory_seq& th); - bool final_check() { - return true; - } + bool final_check(); void propagate_in_re(literal lit); From 5fe6236e9e07d1190c4a659185ac56f45a1f323b Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sat, 4 Jul 2026 11:12:24 -0700 Subject: [PATCH 18/24] add outline of Margus's lookahead optimization Signed-off-by: Nikolaj Bjorner --- src/ast/rewriter/seq_split.cpp | 236 +++++++++++++++++++++++++++------ 1 file changed, 192 insertions(+), 44 deletions(-) diff --git a/src/ast/rewriter/seq_split.cpp b/src/ast/rewriter/seq_split.cpp index be320cb74d..c1b1b6463d 100644 --- a/src/ast/rewriter/seq_split.cpp +++ b/src/ast/rewriter/seq_split.cpp @@ -154,38 +154,19 @@ struct split_set::iterator::imp { } }; - struct concat_left : public split_set::consumer { - split_set a_s; - split_set::iterator a_it; - split_set::iterator a_end; - expr_ref b; - concat_left(split_set&& a_src, expr *b) - : a_s(std::move(a_src)), a_it(a_s.begin()), a_end(a_s.end()), b(b, a_s.m_imp->m) {} - - void consume() override { - TRACE(seq, tout << "concat_left consume\n"); - while (a_it != a_end && !parent().has_split()) { - auto [p, q] = *a_it; - parent().push_split(p, parent().i.rw.mk_re_append(q, b)); - ++a_it; - } - if (a_it.failed()) - parent().set_failure(); - } - }; - - struct concat_right : public split_set::consumer { + struct concat_sandwitch : public split_set::consumer { expr_ref a; split_set b_s; + expr_ref c; split_set::iterator b_it; split_set::iterator b_end; - concat_right(expr* a, split_set&& b_src) : a(a, b_src.m_imp->m), b_s(std::move(b_src)), b_it(b_s.begin()), b_end(b_s.end()) {} + concat_sandwitch(expr* a, split_set&& b_src, expr* c) : + a(a, b_src.m_imp->m), b_s(std::move(b_src)), c(c, b_s.m_imp->m), b_it(b_s.begin()), b_end(b_s.end()) {} void consume() override { - TRACE(seq, tout << "concat_right consume\n"); while (b_it != b_end && !parent().has_split()) { auto [p, q] = *b_it; - parent().push_split(parent().i.rw.mk_re_append(a, p), q); + parent().push_split(parent().i.rw.mk_re_append(a, p), parent().i.rw.mk_re_append(q, c)); ++b_it; } if (b_it.failed()) @@ -193,8 +174,6 @@ struct split_set::iterator::imp { } }; - - // TODO: can be written as a.sigma(b) u sigma(a).b filtering out eps on one union. struct concat : split_set::consumer { expr_ref a, b; split_set a_s, b_s; @@ -288,8 +267,6 @@ struct split_set::iterator::imp { m_at_end = true; return; } - // TODO: we can be strategic about choosing what to unfold, - // and perform early subsumption check expr_ref last(m_cont.back(), m); m_cont.pop_back(); unfold(last); @@ -338,7 +315,29 @@ struct split_set::iterator::imp { } } - void unfold(expr* r) { + bool is_cheap(expr* r) { + if (re.is_empty(r)) + return true; + if (re.is_union(r)) + return true; + if (re.is_to_re(r)) + return true; + if (re.is_full_char(r) || re.is_range(r) || re.is_of_pred(r)) + return true; + if (re.is_full_seq(r)) + return true; + + return false; + } + + void push_cont(expr* r) { + if (is_cheap(r)) + unfold(r); + else + m_cont.push_back(r); + } + + void unfold(expr* r) { TRACE(seq, tout << "unfold " << mk_pp(r, m) << "\n"); SASSERT(seq.is_re(r)); if (re.is_empty(r)) @@ -348,8 +347,8 @@ struct split_set::iterator::imp { auto mk_eps = [&]() { return expr_ref(re.mk_epsilon(i.m_seq_sort), m); }; expr *a, *b; if (re.is_union(r, a, b)) { - m_cont.push_back(a); - m_cont.push_back(b); + push_cont(a); + push_cont(b); return; } @@ -402,31 +401,25 @@ struct split_set::iterator::imp { return; } - // star: sigma(a*) = { } cup a*.sigma(a).a* - auto add_star = [&](expr *r, expr* a) { + // left . sigma(a) . right + auto add_sandwitch = [&](expr *left, expr *a, expr *right) { split_set sigma_a(i.rw, a, i.m_threshold, {}); - auto *c_left = alloc(concat_left, std::move(sigma_a), r); - split_set sigma_aa(i.rw, nullptr, i.m_threshold, {}); - auto *c_right = alloc(concat_right, r, std::move(sigma_aa)); - auto &parent = *c_right->b_it.m_imp; - parent.m_consumer = c_left; - c_left->set_parent(parent); - parent.init(); - m_consumer = c_right; + m_consumer = alloc(concat_sandwitch, left, std::move(sigma_a), right); m_consumer->set_parent(*this); }; + // star: sigma(a*) = { } cup a*.sigma(a).a* if (re.is_star(r, a)) { auto eps = mk_eps(); push_split(eps, eps); - add_star(r, a); + add_sandwitch(r, a, r); return; } // plus: a+ = a.a* ; sigma(a+) = a*.sigma(a).a* (star rule without ) if (re.is_plus(r, a)) { const expr_ref star(re.mk_star(a), m); // a* - add_star(star, a); + add_sandwitch(star, a, star); return; } @@ -448,6 +441,36 @@ struct split_set::iterator::imp { return; } + // abbreviation + // optional: a? = eps | a ; sigma(a?) = sigma(eps | a) = eps cup sigma(a) + if (re.is_opt(r, a)) { + auto eps = mk_eps(); + push_split(eps, eps); + push_cont(a); + return; + } + + // loop: r{l,h} = \bigcup_{l <= j <= h} r^j. + // A split either singles out the i-th copy of a (0 <= i < h) as + // for in sigma(a), + // where r{lo_i,hi_i} folds the tail counts j-i-1, over every remaining + // j in [l,h] with j > i, into a single loop [ when l == 0] + unsigned l, h; + if (re.is_loop(r, a, l, h)) { + if (l == 0) { + auto eps = mk_eps(); + push_split(eps, eps); + } + for (unsigned i = 0; i < h; i++) { + const expr_ref pre(re.mk_loop_proper(a, i, i), m); + const unsigned lo_i = l > i + 1 ? l - i - 1 : 0; + const unsigned hi_i = h - i - 1; + const expr_ref post(re.mk_loop_proper(a, lo_i, hi_i), m); + add_sandwitch(pre, a, post); + } + return; + } + set_failure(r); } @@ -458,7 +481,7 @@ struct split_set::iterator::imp { } bool at_end() const { - return m_failure || m_end_marker || (m_at_end && m_qhead == m_splits.size()); + return m_end_marker || ((m_failure || m_at_end) && m_qhead == m_splits.size()); } }; @@ -565,3 +588,128 @@ std::pair split_set::try_split_sequence(expr *str) { << tail << "\n"); return { head, tail }; } + +#if 0 +// One level of the sigma rules. Mirrors the historic eager `compute`, except it +// emits *suspended* split-algebra terms (from_re / lcat / rcat / inter / compl) for +// the subterms instead of recursing. `mode` is irrelevant here: weak vs. strong is +// decided when `head_normalize` reaches an inter / compl node. +namespace { + // Cofactor path condition `pred` (a Boolean over x = (:var 0)) -> the canonical + // range_predicate (union of ranges) of the characters satisfying it. Returns + // false on a construct outside {true,false,and,or,not,=,char.<=} over x. + static bool pred_to_rp(ast_manager &m, seq_util &sq, expr *x, expr *pred, unsigned maxc, + seq::range_predicate &out) { + expr *a = nullptr, *b = nullptr; + unsigned c = 0; + if (m.is_true(pred)) { + out = seq::range_predicate::top(maxc); + return true; + } + if (m.is_false(pred)) { + out = seq::range_predicate::empty(maxc); + return true; + } + if (m.is_eq(pred, a, b)) { + if (a == x && sq.is_const_char(b, c)) { + out = seq::range_predicate::singleton(c, maxc); + return true; + } + if (b == x && sq.is_const_char(a, c)) { + out = seq::range_predicate::singleton(c, maxc); + return true; + } + return false; + } + if (sq.is_char_le(pred, a, b)) { + if (b == x && sq.is_const_char(a, c)) { + out = seq::range_predicate::range(c, maxc, maxc); + return true; + } + if (a == x && sq.is_const_char(b, c)) { + out = seq::range_predicate::range(0, c, maxc); + return true; + } + return false; + } + if (m.is_not(pred, a)) { + seq::range_predicate s(maxc); + if (!pred_to_rp(m, sq, x, a, maxc, s)) + return false; + out = ~s; + return true; + } + if (m.is_and(pred)) { + out = seq::range_predicate::top(maxc); + for (expr *arg : *to_app(pred)) { + seq::range_predicate s(maxc); + if (!pred_to_rp(m, sq, x, arg, maxc, s)) + return false; + out = out & s; + } + return true; + } + if (m.is_or(pred)) { + out = seq::range_predicate::empty(maxc); + for (expr *arg : *to_app(pred)) { + seq::range_predicate s(maxc); + if (!pred_to_rp(m, sq, x, arg, maxc, s)) + return false; + out = out | s; + } + return true; + } + return false; + } +} // namespace + +// Single-character regex for a cofactor path condition `pred` (a Boolean over the +// character (:var 0)). Materialized via the canonical seq::range_predicate as a +// union-of-ranges regex (fully supported by the derivative / emptiness / primitive +// path, and canonical so equivalent classes share AST identity). Falls back to +// of_pred(lambda) only for predicates outside the recognized range fragment. +expr_ref seq_split::mk_charclass_re(expr *pred, sort *seq_sort) { + seq_util &sq = seq(); + sort *cs = sq.mk_char_sort(); + expr_ref var0(m.mk_var(0, cs), m); + seq::range_predicate rp(sq.max_char()); + // NSB: can we be lazy about expanding to range predicate normal form, just use lambdas as defalt + // and use general purpose processing to handle of_pred? + if (pred_to_rp(m, sq, var0, pred, sq.max_char(), rp)) + return seq::range_predicate_to_regex(sq, rp, seq_sort); + symbol nm("c"); + expr_ref lam(m.mk_lambda(1, &cs, &nm, pred), m); + return expr_ref(re().mk_of_pred(lam), m); +} + +// r == E(r) | RE(LF(delta(r))): peel one character through the symbolic derivative +// (Brzozowski cofactors) and recurse. Shared by the complement and intersection +// cases to avoid the De Morgan / cross-product blow-up. delta distributes over +// both ~ and &, so LF(delta(r)) = { (alpha_i, tgt_i) } with tgt_i the (complement / +// intersection of) character-derivatives. Records `r` in `deriv_memo` as a cycle +// guard. Returns a null expr_ref when nullability of `r` is not statically +// decidable (the caller then falls back to its structural rule). +bool seq_split::iterator::imp::try_derivative_split(expr *r, sort *seq_sort, obj_hashtable &deriv_memo) { + seq_util::rex &rex = re(); + expr_ref nb = m_rw.is_nullable(r); + if (!m.is_true(nb) && !m.is_false(nb)) + return false; // undecidable -> fall back + deriv_memo.insert(r); + // NSB: take a reference count on r here for the table? + sort *re_sort = rex.mk_re(seq_sort); + expr_ref unfolded(m); + if (m.is_true(nb)) { + auto eps = re.mk_epsilon(seq_sort); + push_split(eps, eps); + } + expr_ref_pair_vector cofs(m); + m_rw.brz_derivative_cofactors(r, cofs); // { (alpha_i, tgt_i) } = LF(delta(r)) + for (auto const &[cond, tgt] : cofs) { + expr_ref alpha = mk_charclass_re(cond, seq_sort); // single-char regex + expr_ref term(rex.mk_concat(alpha, tgt), m); // alpha_i . tgt_i + push_cont(term); + } + return true; +} + +#endif \ No newline at end of file From 3a4cdfdc269e5f5d252cbea57a5f453516cb74a4 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sat, 4 Jul 2026 14:29:10 -0700 Subject: [PATCH 19/24] stop complaining abot Char in QF_S benchmarks Signed-off-by: Nikolaj Bjorner --- src/solver/check_logic.cpp | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/solver/check_logic.cpp b/src/solver/check_logic.cpp index bc92c8a30a..e81167f677 100644 --- a/src/solver/check_logic.cpp +++ b/src/solver/check_logic.cpp @@ -469,7 +469,7 @@ struct check_logic::imp { else if (m.is_builtin_family_id(fid)) { // nothing to check } - else if (fid == m_seq_util.get_family_id()) { + else if (fid == m_seq_util.get_family_id() || m_seq_util.is_char(s)) { // nothing to check } else if (fid == m_dt_util.get_family_id() && m_dt) { From 3f62cb9932dfbf84222a5dcbfe96a409b1d56016 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sat, 4 Jul 2026 16:26:51 -0700 Subject: [PATCH 20/24] fix bug in intersection iterator Signed-off-by: Nikolaj Bjorner --- src/ast/rewriter/seq_split.cpp | 10 ++++++---- 1 file changed, 6 insertions(+), 4 deletions(-) diff --git a/src/ast/rewriter/seq_split.cpp b/src/ast/rewriter/seq_split.cpp index c1b1b6463d..394edfb334 100644 --- a/src/ast/rewriter/seq_split.cpp +++ b/src/ast/rewriter/seq_split.cpp @@ -67,17 +67,19 @@ struct split_set::iterator::imp { a_it(a_s.begin()), a_end(a_s.end()), b_it(b_s.begin()), b_end(b_s.end()) {} bool at_end() const { - return (a_it == a_end && b_it == b_end) || a_it.failed() || b_it.failed(); + return b_it == b_end || a_it == a_end || a_it.failed() || b_it.failed(); } void next() { SASSERT(!at_end()); - if (b_it != b_end) - ++b_it; + SASSERT(b_it != b_end); + ++b_it; if (b_it == b_end) { ++a_it; - if (a_it != a_end) + if (a_it != a_end) { b_it.m_imp->rewind(); + SASSERT(b_it != b_end); + } } } void consume() override { From 6610545c0893400fbb73bffb4e39000463f7123f Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sun, 5 Jul 2026 12:03:27 -0700 Subject: [PATCH 21/24] disable loop split set Signed-off-by: Nikolaj Bjorner --- src/ast/rewriter/seq_split.cpp | 2 +- src/smt/seq_regex.cpp | 5 +---- 2 files changed, 2 insertions(+), 5 deletions(-) diff --git a/src/ast/rewriter/seq_split.cpp b/src/ast/rewriter/seq_split.cpp index 394edfb334..69f5dea165 100644 --- a/src/ast/rewriter/seq_split.cpp +++ b/src/ast/rewriter/seq_split.cpp @@ -458,7 +458,7 @@ struct split_set::iterator::imp { // where r{lo_i,hi_i} folds the tail counts j-i-1, over every remaining // j in [l,h] with j > i, into a single loop [ when l == 0] unsigned l, h; - if (re.is_loop(r, a, l, h)) { + if (false && re.is_loop(r, a, l, h)) { if (l == 0) { auto eps = mk_eps(); push_split(eps, eps); diff --git a/src/smt/seq_regex.cpp b/src/smt/seq_regex.cpp index 289ca5e0f8..6f3c8609c3 100644 --- a/src/smt/seq_regex.cpp +++ b/src/smt/seq_regex.cpp @@ -444,8 +444,6 @@ namespace smt { // Final check also unfolds this axiomatization // (we have to add a final check to seq_regex for this). - - unsigned threshold = th.get_fparams().m_seq_regex_factorization_threshold; expr_ref_vector prefix(m); expr *hd, *tl, *v; @@ -477,8 +475,7 @@ namespace smt { } if (!result.failed()) { const expr_ref cases_expr(m.mk_or(cases), m); - ctx.internalize(cases_expr, false); - th.propagate_lit(nullptr, 1, &lit, ctx.get_literal(cases_expr)); + th.propagate_lit(nullptr, 1, &lit, th.mk_literal(cases_expr)); return true; } } From b616f714add439e7b881216c32bfea8aabbda267 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sun, 19 Jul 2026 12:08:35 -0700 Subject: [PATCH 22/24] Add continuation-regex split service (seq_monadic) Port seq_monadic to the split_set branch, reimplemented against the cont_regex / split / split_manager API. Element-sort agnostic: relies on the derivative engine and th_rewriter, no character-specific reasoning. - Global derivative-transition graph reused across regexes (intern_state / expand_state / build_graph) so states, nullability and cofactor successors are computed once. - embed(r) = ; the epsilon accept-state marks the membership (nullable) case uniformly. - intersect handles general cont_regex, including non-epsilon reach targets N (membership BFS + product-reachability paths). - No budget / reset_pin. Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com> Copilot-Session: 34aa9af0-4977-411d-aaa7-7cb81cc4e9f8 --- src/ast/rewriter/CMakeLists.txt | 1 + src/ast/rewriter/seq_monadic.cpp | 425 +++++++++++++++++++++++++++++++ src/ast/rewriter/seq_monadic.h | 199 +++++++++++++++ src/test/CMakeLists.txt | 1 + src/test/main.cpp | 1 + src/test/seq_monadic.cpp | 174 +++++++++++++ 6 files changed, 801 insertions(+) create mode 100644 src/ast/rewriter/seq_monadic.cpp create mode 100644 src/ast/rewriter/seq_monadic.h create mode 100644 src/test/seq_monadic.cpp diff --git a/src/ast/rewriter/CMakeLists.txt b/src/ast/rewriter/CMakeLists.txt index df06cedfe3..9f4d7fe436 100644 --- a/src/ast/rewriter/CMakeLists.txt +++ b/src/ast/rewriter/CMakeLists.txt @@ -40,6 +40,7 @@ z3_add_component(rewriter seq_axioms.cpp seq_eq_solver.cpp seq_derive.cpp + seq_monadic.cpp seq_subset.cpp seq_split.cpp seq_derive.cpp diff --git a/src/ast/rewriter/seq_monadic.cpp b/src/ast/rewriter/seq_monadic.cpp new file mode 100644 index 0000000000..4af73793eb --- /dev/null +++ b/src/ast/rewriter/seq_monadic.cpp @@ -0,0 +1,425 @@ +/*++ +Copyright (c) 2026 Microsoft Corporation + +Module Name: + + seq_monadic.cpp + +Abstract: + + Continuation-regex split service and intersection non-emptiness. See + seq_monadic.h. + + Automaton-based (product/derivative reachability) and element-sort agnostic: + guard feasibility and successor states are computed entirely by the symbolic + derivative engine (seq_rewriter::brz_derivative_cofactors, which prunes + infeasible guards internally), so there is no character-specific reasoning in + this module. A single global derivative-transition graph is grown lazily and + recycled across every regex, so no derivative is computed twice. th_rewriter is + used to normalize the intersection regex. + +Author: + + Nikolaj Bjorner / Margus Veanes 2026 + +--*/ + +#include "ast/rewriter/seq_monadic.h" +#include +#include +#include + +namespace seq { + + // ------------------------------------------------------------------ + // global derivative-transition graph (shared / recycled across regexes) + // ------------------------------------------------------------------ + + unsigned split_manager::intern_state(expr* s) { + unsigned id; + if (m_state_id.find(s, id)) + return id; // recycle the global state + id = m_gstate.size(); + m_state_id.insert(s, id); + m_gstate.push_back(s); + m_pin.push_back(s); + expr_ref nb = m_rw.is_nullable(s); + m_gmaybe_null.push_back(!m.is_false(nb)); // unknown nullability => keep (conservative) + m_gexpanded.push_back(false); + m_gsucc.push_back(svector()); + return id; + } + + void split_manager::expand_state(unsigned i, bool& ok) { + ok = true; + if (m_gexpanded[i]) + return; // successors already computed once + if (!m.inc()) { ok = false; return; } + expr* s = m_gstate[i]; // captured before any interning realloc + expr_ref_pair_vector cof(m); + m_rw.brz_derivative_cofactors(s, cof); + svector edges; + for (auto const& [g, t] : cof) { + if (re().is_empty(t)) continue; // engine already pruned infeasible guards + unsigned k = intern_state(t); // may realloc m_gsucc: collect edges first + m_pin.push_back(g); + edges.push_back(gedge{ g, k }); + } + for (gedge const& e : edges) // m_gsucc stable now (no more interning) + m_gsucc[i].push_back(e); + m_gexpanded[i] = true; + } + + // ------------------------------------------------------------------ + // live-state / reachability machinery (projected out of the global graph) + // ------------------------------------------------------------------ + + void split_manager::build_graph(expr* R, ptr_vector& states, + vector>& succ, + bool_vector& maybe_null, bool& ok) { + ok = true; + states.reset(); + succ.reset(); + maybe_null.reset(); + obj_map local; // state expr -> local index + svector l2g; // local index -> global id + auto local_of = [&](expr* s) -> unsigned { + unsigned li; + if (local.find(s, li)) return li; + unsigned gid = intern_state(s); + li = states.size(); + local.insert(s, li); + l2g.push_back(gid); + states.push_back(s); + maybe_null.push_back(m_gmaybe_null[gid]); + succ.push_back(svector()); + return li; + }; + local_of(R); + const unsigned STATE_CAP = 1u << 12; + for (unsigned i = 0; i < states.size(); ++i) { + if (states.size() > STATE_CAP || !m.inc()) { ok = false; return; } + unsigned gid = l2g[i]; + expand_state(gid, ok); + if (!ok) return; + svector tgts; // snapshot: local_of may realloc m_gsucc + for (edge const& e : m_gsucc[gid]) + tgts.push_back(e.target); + for (unsigned t : tgts) + succ[i].push_back(local_of(m_gstate[t])); + } + } + + void split_manager::live_states(expr* R, ptr_vector& out, bool& ok) { + ptr_vector states; + vector> succ; + bool_vector maybe_null; + build_graph(R, states, succ, maybe_null, ok); + if (!ok) return; + unsigned n = states.size(); + bool_vector live; + live.resize(n, false); + for (unsigned i = 0; i < n; ++i) + live[i] = maybe_null[i]; + for (bool ch = true; ch; ) { + ch = false; + for (unsigned i = 0; i < n; ++i) + if (!live[i]) + for (unsigned j : succ[i]) + if (live[j]) { live[i] = true; ch = true; break; } + } + for (unsigned i = 0; i < n; ++i) + if (live[i]) out.push_back(states.get(i)); + } + + void split_manager::reaching_states(expr* R, expr* N, ptr_vector& out, bool& ok) { + ptr_vector states; + vector> succ; + bool_vector maybe_null; + build_graph(R, states, succ, maybe_null, ok); + if (!ok) return; + unsigned n = states.size(); + unsigned tgt = UINT_MAX; + for (unsigned i = 0; i < n; ++i) + if (states.get(i) == N) { tgt = i; break; } + if (tgt == UINT_MAX) return; // N unreachable => no midpoints + bool_vector reach; + reach.resize(n, false); + reach[tgt] = true; + for (bool ch = true; ch; ) { + ch = false; + for (unsigned i = 0; i < n; ++i) + if (!reach[i]) + for (unsigned j : succ[i]) + if (reach[j]) { reach[i] = true; ch = true; break; } + } + for (unsigned i = 0; i < n; ++i) + if (reach[i]) out.push_back(states.get(i)); + } + + // ------------------------------------------------------------------ + // intersection non-emptiness + // ------------------------------------------------------------------ + + // A component is a membership (nullable) component when N_i is null or + // the epsilon regex; otherwise it is a reach component with structural target N_i. + static bool is_membership(seq_util::rex& re, cont_regex const& cr) { + expr* N = cr.second.get(); + 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); + } + + lbool split_manager::intersect(vector const& crs, unsigned lo, unsigned hi, + expr_ref_vector& seq) { + seq.reset(); + unsigned n = crs.size(); + if (n == 0) { + // universal language: contains a word of every length; non-empty iff lo <= hi + if (lo > hi) return l_false; + for (unsigned k = 0; k < lo; ++k) + seq.push_back(m.mk_true()); // trivial guard: any element admissible + return l_true; + } + // Fast, robust path when every component is a membership (nullable) component: + // the intersection is non-empty iff some reachable product state is nullable. + bool all_memb = true; + for (auto const& cr : crs) + if (!is_membership(re(), cr)) { all_memb = false; break; } + if (all_memb) + return intersect_membership(crs, lo, hi, seq); + + // General case: a tuple product search that also handles reach targets + // N != epsilon via structural target matching. + return intersect_product(crs, lo, hi, seq); + } + + lbool split_manager::intersect_membership(vector const& crs, unsigned lo, + unsigned hi, expr_ref_vector& seq) { + unsigned n = crs.size(); + // The normalized intersection regex; the derivative engine handles guard + // feasibility and successor computation internally. + expr_ref P(crs[0].first.get(), m); + for (unsigned i = 1; i < n; ++i) + P = re().mk_inter(P, crs[i].first.get()); + m_th(P); + unsigned r0 = intern_state(P.get()); + + // Search node with witness reconstruction: `guard` is the derivative path + // condition on the incoming edge (a predicate over the element (:var 0)). + struct node { unsigned st; unsigned depth; int parent; expr* guard; }; + std::vector nodes; + + // Beyond `cap` elements the length no longer changes acceptance, so we cap + // the depth in the visited key to keep the state space finite. + unsigned cap = (hi == UINT_MAX) ? lo : hi; + auto key = [&](unsigned st, unsigned depth) { + return std::make_pair(st, depth < cap ? depth : cap); + }; + + std::set> visited; + nodes.push_back(node{ r0, 0, -1, nullptr }); + visited.insert(key(r0, 0)); + + bool undecided = false; + for (size_t head = 0; head < nodes.size(); ++head) { + if (!m.inc()) return l_undef; + int cur = (int) head; + unsigned st = nodes[cur].st; // note: `nodes` may grow below + unsigned depth = nodes[cur].depth; + + if (depth >= lo && depth <= hi && m_gmaybe_null[st]) { + expr_ref nb = m_rw.is_nullable(m_gstate[st]); + if (m.is_true(nb)) { + ptr_vector gs; + for (int j = cur; j >= 0 && nodes[j].parent >= 0; j = nodes[j].parent) + gs.push_back(nodes[j].guard); + for (unsigned k = gs.size(); k-- > 0; ) + seq.push_back(gs[k]); + return l_true; + } + if (!m.is_false(nb)) + undecided = true; // undecidable nullability => cannot claim l_false + } + if (depth >= hi) + continue; // cannot extend further + bool ok = true; + expand_state(st, ok); + if (!ok) return l_undef; + for (edge const& e : m_gsucc[st]) // no interning here => m_gsucc stable + if (visited.insert(key(e.target, depth + 1)).second) + nodes.push_back(node{ e.target, depth + 1, cur, e.guard }); + } + return undecided ? l_undef : l_false; + } + + lbool split_manager::intersect_product(vector const& crs, unsigned lo, + 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 + for (auto const& cr : crs) { + bool mb = is_membership(re(), cr); + memb.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()); + } + + // Search node: a product tuple, its depth, its parent, and the joint guard on + // the incoming edge (a predicate over the element variable (:var 0)). + struct node { svector st; unsigned depth; int parent; expr* guard; }; + std::vector nodes; + + // Beyond `cap` elements the length no longer changes acceptance, so we cap the + // depth in the visited key to keep the state space finite. + unsigned cap = (hi == UINT_MAX) ? lo : hi; + auto key = [&](svector const& st, unsigned depth) { + std::vector k; + k.reserve(st.size() + 1); + for (expr* e : st) k.push_back(e->get_id()); + k.push_back(depth < cap ? depth : cap); + return k; + }; + + auto is_accept = [&](svector const& st, bool& undecided) -> bool { + for (unsigned i = 0; i < n; ++i) { + if (memb[i]) { + expr_ref nb = m_rw.is_nullable(st[i]); + if (m.is_true(nb)) continue; + if (m.is_false(nb)) return false; + undecided = true; return false; + } + else if (st[i] != tgt[i]) + return false; // reach component: structural target match + } + return true; + }; + + std::set> visited; + nodes.push_back(node{ start, 0, -1, nullptr }); + visited.insert(key(start, 0)); + + bool undecided = false; + for (size_t head = 0; head < nodes.size(); ++head) { + if (!m.inc()) return l_undef; + int cur = (int) head; + svector st = nodes[cur].st; // copy: `nodes` may grow below + unsigned depth = nodes[cur].depth; + + if (depth >= lo && depth <= hi) { + bool u2 = false; + if (is_accept(st, u2)) { + ptr_vector gs; // reconstruct the per-position guards + for (int j = cur; j >= 0 && nodes[j].parent >= 0; j = nodes[j].parent) + gs.push_back(nodes[j].guard); + for (unsigned k = gs.size(); k-- > 0; ) + seq.push_back(gs[k]); + return l_true; + } + if (u2) undecided = true; + } + if (depth >= hi) + continue; // cannot extend further + + // Joint transitions: cofactors of inter(st_0,...,st_{n-1}). The engine + // prunes infeasible joint guards and yields the product successor as an + // re.inter in source order, which we decompose positionally. + 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); + if (ops.size() != n) { // engine collapsed the product: give up soundly + undecided = true; + continue; + } + for (unsigned i = 0; i < n; ++i) nst.push_back(ops[i]); + } + for (expr* s : nst) m_pin.push_back(s); + m_pin.push_back(g); + if (visited.insert(key(nst, depth + 1)).second) + nodes.push_back(node{ nst, depth + 1, cur, g }); + } + } + return undecided ? l_undef : l_false; + } + + bool split_manager::test_intersect(vector const& crs) { + // one-sided cheap check: an obviously-empty start (or reach target) state + // certainly makes the intersection empty. Normalize via th_rewriter first so + // that e.g. concat(empty, epsilon) collapses to the empty regex. + expr_ref tmp(m); + for (auto const& cr : crs) { + m_th(cr.first, tmp); + if (re().is_empty(tmp)) + return false; + if (cr.second.get()) { + m_th(cr.second, tmp); + if (re().is_empty(tmp)) + return false; + } + } + return true; + } + + // ------------------------------------------------------------------ + // seq::split / seq::split_iterator + // ------------------------------------------------------------------ + + split_iterator::split_iterator(split_manager& sm, cont_regex const& cr) { + m_sm = &sm; + m_R = cr.first.get(); + m_N = cr.second.get(); + bool ok = true; + bool membership = (m_N == nullptr) || sm.re().is_epsilon(m_N); + if (membership) + sm.live_states(m_R, m_mids, ok); + else + sm.reaching_states(m_R, m_N, m_mids, ok); + if (!ok) { m_failed = true; m_mids.reset(); } + } + + split_pair split_iterator::operator*() const { + ast_manager& m = m_sm->mgr(); + expr* mid = m_mids[m_pos]; + cont_regex left(expr_ref(m_R, m), expr_ref(mid, m)); + cont_regex right(expr_ref(mid, m), m_N ? expr_ref(m_N, m) : expr_ref(m)); + return split_pair(left, right); + } + + split_iterator& split_iterator::operator++() { + if (m_pos < m_mids.size()) ++m_pos; + return *this; + } + + split::split(split_manager& sm, expr* r) + : m_sm(sm), m_R(r, sm.mgr()), m_N(sm.mgr()) {} + + split::split(split_manager& sm, cont_regex const& cr) + : m_sm(sm), m_R(cr.first), m_N(cr.second) {} + + split_iterator split::begin() { + return split_iterator(m_sm, cont_regex(m_R, m_N)); + } +} diff --git a/src/ast/rewriter/seq_monadic.h b/src/ast/rewriter/seq_monadic.h new file mode 100644 index 0000000000..9875e2a077 --- /dev/null +++ b/src/ast/rewriter/seq_monadic.h @@ -0,0 +1,199 @@ +/*++ +Copyright (c) 2026 Microsoft Corporation + +Module Name: + + seq_monadic.h + +Abstract: + + Continuation-regex split service and intersection non-emptiness for regular + expressions, following the design sketched in + paper/bench/eval/monadic-vs-nielsen-eval.md. + + * A continuation regex (seq::cont_regex) is a pair of regexes. R is + the start state and N is the accept state. A word w is accepted iff + delta_w(R) == N, with one distinguished case: when N is the epsilon regex + (the regex accepting the empty sequence) acceptance is ordinary membership + w in L(R), i.e. delta_w(R) is nullable. This is because the Brzozowski + derivative folds the epsilon tail into nullability (the epsilon state is not + structurally reachable for looping nullable regexes). Every regex R is + embedded as the continuation regex . + + * seq::split exposes, for a continuation regex, an (opaque) iterator of + seq::split_pair splits: uv in ==> u in /\ v in , + where R' ranges over the live cofactors of R that can still reach N. + + * seq::split_manager owns the live-state / reachability machinery shared across + regexes, and decides emptiness of an intersection of continuation regexes. + It maintains one global derivative-transition graph and recycles the states + (and their computed nullability / cofactor successors) across every regex it + processes, so the same derivative is never recomputed. + + 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. + +Author: + + Nikolaj Bjorner / Margus Veanes 2026 + +--*/ +#pragma once + +#include "ast/rewriter/seq_rewriter.h" +#include "ast/rewriter/th_rewriter.h" +#include "util/lbool.h" +#include "util/obj_hashtable.h" +#include "util/vector.h" +#include + +namespace seq { + + // A continuation regex : start state R, accept state N. A word w is + // accepted iff delta_w(R) == N. When N is the epsilon regex (or null), the + // accept condition is ordinary membership (delta_w(R) is nullable). + typedef std::pair cont_regex; + + // A split of uv in into u in and v in . + typedef std::pair split_pair; + + class split_manager; + + // Opaque, lazy iterator over the splits of a continuation regex. The internal + // state (the enumerated midpoints R') is computed on construction. `failed()` + // reports a non-ground regex or a resource limit reached while computing + // derivatives. + class split_iterator { + friend class split; + split_manager* m_sm = nullptr; + expr* m_R = nullptr; // start state of the continuation regex + expr* m_N = nullptr; // accept state (epsilon/null => membership) + ptr_vector m_mids; // enumerated live midpoints R' + unsigned m_pos = 0; // current midpoint index + bool m_failed = false; // non-ground regex / resource limit + + split_iterator(split_manager& sm, cont_regex const& cr); // begin + + bool at_end() const { return m_failed || m_pos >= m_mids.size(); } + + public: + split_iterator() = default; // end sentinel + + split_pair operator*() const; + split_iterator& operator++(); + bool operator==(split_iterator const& other) const { return at_end() && other.at_end(); } + bool operator!=(split_iterator const& other) const { return !(*this == other); } + bool failed() const { return m_failed; } + }; + + // A continuation regex together with the manager that can split it. + class split { + split_manager& m_sm; + expr_ref m_R; + expr_ref m_N; + public: + split(split_manager& sm, expr* r); + split(split_manager& sm, cont_regex const& cr); + split_iterator begin(); + split_iterator end() { return split_iterator(); } + }; + + // Manages live states / abstract reachability across the regexes it processes, + // and decides emptiness of intersections of continuation regexes. One global + // derivative-transition graph is grown lazily and shared across every regex, so + // states, their nullability and their cofactor successors are computed once. + class split_manager { + friend class split; + friend class split_iterator; + + // A cofactor transition of the global graph: on a guard (a predicate over the + // element variable (:var 0)) the derivative moves to the target state. + struct gedge { expr* guard; unsigned target; }; + + ast_manager& m; + seq_rewriter& m_rw; + th_rewriter m_th; // regex normalization (element-sort agnostic) + expr_ref_vector m_pin; // keeps interned states / guards alive + + // Global reachability graph, reused across every processed regex. + obj_map m_state_id; // regex state -> global id + ptr_vector m_gstate; // global id -> state + bool_vector m_gmaybe_null; // per state: !is_false(is_nullable) + bool_vector m_gexpanded; // per state: cofactor successors computed + vector> m_gsucc; // per state: (guard, target) edges + + seq_util& u() const { return m_rw.u(); } + seq_util::rex& re() const { return m_rw.u().re; } + + // Intern a state into the global graph (recycles an existing global state), + // computing its nullability lazily. Returns its global id. + unsigned intern_state(expr* s); + + // Compute (once) the cofactor successors of the global state `i`, recycling + // any target states already present in the graph. Sets `ok` false on a + // resource limit. + void expand_state(unsigned i, bool& ok); + + // Reachable derivative states of R with their transition graph and per-state + // (possible) nullability, projected out of the global graph. Sets `ok` false + // on cap overrun / resource limit. + void build_graph(expr* R, ptr_vector& states, + vector>& succ, bool_vector& maybe_null, bool& ok); + + // Live reachable derivative states of R (can reach a nullable state). + void live_states(expr* R, ptr_vector& out, bool& ok); + + // Reachable derivative states of R from which the state N is reachable. + void reaching_states(expr* R, expr* N, ptr_vector& out, bool& ok); + + // Non-emptiness of an all-membership intersection: BFS over the normalized + // product state inter(R_0,...,R_{n-1}) with an is_nullable acceptance test. + lbool intersect_membership(vector const& crs, unsigned lo, unsigned hi, + 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. + lbool intersect_product(vector const& crs, unsigned lo, unsigned hi, + expr_ref_vector& seq); + + public: + split_manager(seq_rewriter& rw) + : m(rw.m()), m_rw(rw), m_th(rw.m()), m_pin(rw.m()) {} + + ast_manager& mgr() const { return m; } + seq_rewriter& rw() const { return m_rw; } + + void pin(expr* e) { m_pin.push_back(e); } + + // Embed a regex R as the continuation regex . The + // epsilon accept-state marks the membership (nullable) case uniformly. + cont_regex embed(expr* r) { + sort* ss = nullptr; + VERIFY(u().is_re(r, ss)); + expr_ref eps(re().mk_epsilon(ss), m); + expr_ref start(re().mk_concat(r, eps), m); + return cont_regex(start, eps); + } + + split mk_split(expr* r) { return split(*this, r); } + split mk_split(cont_regex const& cr) { return split(*this, cr); } + + // Emptiness of the intersection of the continuation regexes `crs`, restricted + // to words of at least `lo` and at most `hi` elements (hi == UINT_MAX for no + // upper bound). A component accepts a word w iff delta_w(R_i) == N_i, + // where an epsilon (or null) N_i means the nullable/membership case. Feasibility + // 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). + 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 + // certainly empty; true otherwise (may be a false positive). + bool test_intersect(vector const& crs); + }; +} diff --git a/src/test/CMakeLists.txt b/src/test/CMakeLists.txt index 4563752812..ce93b91339 100644 --- a/src/test/CMakeLists.txt +++ b/src/test/CMakeLists.txt @@ -25,6 +25,7 @@ add_executable(test-z3 parametric_datatype.cpp arith_rewriter.cpp seq_rewriter.cpp + seq_monadic.cpp arith_simplifier_plugin.cpp ast.cpp bdd.cpp diff --git a/src/test/main.cpp b/src/test/main.cpp index 3a3cab41db..8f55cdbb1a 100644 --- a/src/test/main.cpp +++ b/src/test/main.cpp @@ -116,6 +116,7 @@ X(range_predicate) \ X(regex_range_collapse) \ X(seq_rewriter) \ + X(seq_monadic) \ X(check_assumptions) \ X(smt_context) \ X(theory_dl) \ diff --git a/src/test/seq_monadic.cpp b/src/test/seq_monadic.cpp new file mode 100644 index 0000000000..2161ed79b5 --- /dev/null +++ b/src/test/seq_monadic.cpp @@ -0,0 +1,174 @@ +/*++ +Copyright (c) 2026 Microsoft Corporation + +Module Name: + + seq_monadic.cpp + +Abstract: + + Unit tests for the continuation-regex split service in + ast/rewriter/seq_monadic.{h,cpp}: seq::split_manager::intersect (element-sort + agnostic intersection non-emptiness, decided by the derivative engine) and the + seq::split midpoint iterator. + +Author: + + Nikolaj Bjorner / Margus Veanes 2026 + +--*/ + +#include "ast/ast.h" +#include "ast/reg_decl_plugins.h" +#include "ast/seq_decl_plugin.h" +#include "ast/rewriter/seq_rewriter.h" +#include "ast/rewriter/seq_monadic.h" +#include +#include + +namespace { + +struct plugin_registrar { + plugin_registrar(ast_manager& m) { reg_decl_plugins(m); } +}; + +class seq_monadic_test { + ast_manager m; + plugin_registrar m_reg; + seq_rewriter m_rw; + seq::split_manager m_sm; + seq_util u; + sort_ref m_str; // String sort + sort_ref m_re; // RegEx sort over m_str + unsigned m_fail = 0; + + seq_util::rex& re() { return u.re; } + + // regex builders + expr_ref word(char const* s) { return expr_ref(re().mk_to_re(u.str.mk_string(zstring(s))), m); } + expr_ref cat(expr* a, expr* b) { return expr_ref(re().mk_concat(a, b), m); } + expr_ref alt(expr* a, expr* b) { return expr_ref(re().mk_union(a, b), m); } + expr_ref star(expr* a) { return expr_ref(re().mk_star(a), m); } + expr_ref comp(expr* a) { return expr_ref(re().mk_complement(a), m); } + expr_ref dotstar() { return expr_ref(re().mk_full_seq(m_re), m); } + expr_ref none() { return expr_ref(re().mk_empty(m_re), m); } + expr_ref rng(char lo, char hi) { + char sl[2] = { lo, 0 }, sh[2] = { hi, 0 }; + return expr_ref(re().mk_range(u.str.mk_string(zstring(sl)), u.str.mk_string(zstring(sh))), m); + } + expr_ref loop(expr* r, unsigned lo, unsigned hi) { return expr_ref(re().mk_loop(r, lo, hi), m); } + + static char const* s(lbool l) { return l == l_true ? "sat" : l == l_false ? "unsat" : "undef"; } + + // intersection non-emptiness of the given membership regexes, words of length in [lo,hi] + lbool inter(std::initializer_list rs, unsigned lo, unsigned hi) { + vector crs; + for (expr* r : rs) crs.push_back(m_sm.embed(r)); + expr_ref_vector wit(m); + return m_sm.intersect(crs, lo, hi, wit); + } + + // intersection non-emptiness of a single reach continuation regex + lbool reach(expr* R, expr* N, unsigned lo, unsigned hi) { + vector crs; + crs.push_back(seq::cont_regex(expr_ref(R, m), expr_ref(N, m))); + expr_ref_vector wit(m); + return m_sm.intersect(crs, lo, hi, wit); + } + + void check(char const* name, lbool got, lbool expected) { + bool ok = (got == expected); + if (!ok) ++m_fail; + std::cout << (ok ? " OK " : " FAIL ") << name + << " got=" << s(got) << " expected=" << s(expected) << "\n"; + } + +public: + seq_monadic_test() : m_reg(m), m_rw(m), m_sm(m_rw), u(m), m_str(m), m_re(m) { + m_str = u.str.mk_string_sort(); + m_re = re().mk_re(m_str); + } + + void run() { + expr_ref a = word("a"); + expr_ref b = word("b"); + expr_ref ab = cat(a, b); + expr_ref sig = dotstar(); // Sigma* + expr_ref saas = cat(sig, cat(cat(a, a), sig)); // Sigma* a a Sigma* + expr_ref sbbs = cat(sig, cat(cat(b, b), sig)); // Sigma* b b Sigma* + expr_ref digitp = cat(rng('0', '9'), star(rng('0', '9'))); // [0-9]+ + + std::cout << "=== split_manager::intersect (membership) ===\n"; + + check("Sigma* ", inter({ sig }, 0, UINT_MAX), l_true); + check("empty regex ", inter({ none() }, 0, UINT_MAX), l_false); + check("~Sigma* ", inter({ comp(sig) }, 0, UINT_MAX), l_false); + // a* & b* = { epsilon } + check("a* & b* (any length) ", inter({ star(a), star(b) }, 0, UINT_MAX), l_true); + check("a* & b* (>= 1 char) ", inter({ star(a), star(b) }, 1, UINT_MAX), l_false); + // Sigma*aaSigma* & Sigma*bbSigma* has a common word (e.g. aabb) + check("SaaS & SbbS ", inter({ saas, sbbs }, 0, UINT_MAX), l_true); + // (a|b)* intersect ~(SaaS) intersect ~(SbbS) is non-empty (alternating words) + check("(a|b)* & ~SaaS & ~SbbS ", + inter({ star(alt(a, b)), comp(saas), comp(sbbs) }, 0, UINT_MAX), l_true); + // nested complement (L3-03) non-empty + check("L3-03 nested complement ", + inter({ comp(cat(star(a), comp(cat(star(b), comp(star(ab)))))) }, 0, UINT_MAX), l_true); + + std::cout << "=== split_manager::intersect (length bounds) ===\n"; + check("[0-9]+ length 0..0 ", inter({ digitp }, 0, 0), l_false); + check("[0-9]+ length 1..1 ", inter({ digitp }, 1, 1), l_true); + check("a* length 2..2 ", inter({ star(a) }, 2, 2), l_true); + check("a* & b* length 3..3 ", inter({ star(a), star(b) }, 3, 3), l_false); + check("[0-9]{2} & [0-9]+ len 2 ", inter({ loop(rng('0','9'), 2, 2), digitp }, 2, 2), l_true); + check("[0-9]{2} len 3 ", inter({ loop(rng('0','9'), 2, 2) }, 3, 3), l_false); + + std::cout << "=== split_manager::intersect (reach, general N) ===\n"; + { + expr_ref aSig = cat(a, sig); // a . Sigma* + // : delta_epsilon(Sigma*) == Sigma* already at depth 0 + check(" len0 ", reach(sig, sig, 0, UINT_MAX), l_true); + // : Sigma* never derives to the empty regex + check(" ", reach(sig, none(), 0, UINT_MAX), l_false); + // : reached exactly after consuming one element + check(" len1 ", reach(aSig, sig, 1, 1), l_true); + check(" len0 ", reach(aSig, sig, 0, 0), l_false); + } + + std::cout << "=== split_manager::test_intersect ===\n"; + { + vector good, bad; + good.push_back(m_sm.embed(sig)); + bad.push_back(m_sm.embed(none())); + check("test_intersect Sigma* ", m_sm.test_intersect(good) ? l_true : l_false, l_true); + check("test_intersect empty ", m_sm.test_intersect(bad) ? l_true : l_false, l_false); + } + + std::cout << "=== split midpoint iterator ===\n"; + { + seq::split sp = m_sm.mk_split(star(alt(a, b))); + seq::split_iterator it = sp.begin(); + bool failed = it.failed(); + unsigned count = 0; + for (; it != sp.end(); ++it) { + seq::split_pair pr = *it; + // left = , right = : the shared midpoint agrees + if (pr.first.second.get() != pr.second.first.get()) ++m_fail; + ++count; + } + check("(a|b)* split not failed ", failed ? l_true : l_false, l_false); + check("(a|b)* has >=1 midpoint ", count > 0 ? l_true : l_false, l_true); + } + + std::cout << "=== seq_monadic: " << (m_fail == 0 ? "ALL PASS" : "FAILURES") << " (" + << m_fail << " fail) ===\n"; + ENSURE(m_fail == 0); + } +}; + +} + +void tst_seq_monadic() { + seq_monadic_test t; + t.run(); +} From e17fba7e393fe2dbff4f328f7afdef28e493ce0f Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sun, 19 Jul 2026 12:20:00 -0700 Subject: [PATCH 23/24] Document known shady parts in seq_monadic (witness extraction, epsilon/N handling) Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com> Copilot-Session: 34aa9af0-4977-411d-aaa7-7cb81cc4e9f8 --- src/ast/rewriter/seq_monadic.cpp | 14 ++++++++++++++ 1 file changed, 14 insertions(+) diff --git a/src/ast/rewriter/seq_monadic.cpp b/src/ast/rewriter/seq_monadic.cpp index 4af73793eb..49144bcb56 100644 --- a/src/ast/rewriter/seq_monadic.cpp +++ b/src/ast/rewriter/seq_monadic.cpp @@ -22,6 +22,20 @@ Author: Nikolaj Bjorner / Margus Veanes 2026 +Shady parts: + +- witness extraction is buggy. It should generally rely on a choice function that takes a + Boolean expression F[(:var 0)] with a single free variable and synthesize a value for the free + variable such that the expression is true. + For character predicates we can assume that the Boolean expressions are range predicates and we can + use utilities for range predicates. For other types use some best effort, say F is of the form (= (:var 0) value). + Expose the witness function in a self-contained module outside of this file. + +- checking intersections with continuation regexes is shady. The nullability check is now really about + whether there is an epsilon transition to the accepting state N. The copilot-generated code ignores this. + Generally, dealing with epsilon state is shady. There are many equivalent ways a state can be epsilon, such + as epsilon*, or comp(.+), etc. + --*/ #include "ast/rewriter/seq_monadic.h" From 9c21f9e184eea0ed195d7954196b8bc5b1b01eab Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sun, 19 Jul 2026 12:30:30 -0700 Subject: [PATCH 24/24] Expand shady-parts notes in seq_monadic (N-relative nullability, epsilon handling, STATE_CAP) Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com> Copilot-Session: 34aa9af0-4977-411d-aaa7-7cb81cc4e9f8 --- src/ast/rewriter/seq_monadic.cpp | 16 +++++++++++++++- 1 file changed, 15 insertions(+), 1 deletion(-) diff --git a/src/ast/rewriter/seq_monadic.cpp b/src/ast/rewriter/seq_monadic.cpp index 49144bcb56..be05dce203 100644 --- a/src/ast/rewriter/seq_monadic.cpp +++ b/src/ast/rewriter/seq_monadic.cpp @@ -24,7 +24,12 @@ Author: Shady parts: -- witness extraction is buggy. It should generally rely on a choice function that takes a +- epsilon transitions appear not accounted for when computing reaching states. + If a regex R contains N by taking a set of epsilon transitions, then it is nullable relative + to N. It suggests a use for a version of nullability that is relative to N. + Deal also with when N itself has epsilon transitions to N1, .., Nk. + +- witness extraction is plain wrong. It should generally rely on a choice function that takes a Boolean expression F[(:var 0)] with a single free variable and synthesize a value for the free variable such that the expression is true. For character predicates we can assume that the Boolean expressions are range predicates and we can @@ -36,6 +41,15 @@ Shady parts: Generally, dealing with epsilon state is shady. There are many equivalent ways a state can be epsilon, such as epsilon*, or comp(.+), etc. +- I don't think there should be a special case for when N is epsilon and having N being nullptr + is uneven. + The code uses "live_states" and "reaching_states" for two cases. + +- The code in test_intersect shouldn't be relying on a rewriter. Anything that can be rewritten + could be done prior. + +- Remove hard-wired constants such as STATE_CAP. + --*/ #include "ast/rewriter/seq_monadic.h"