From a3f0c83be35703f14db9f93d7876f68adfb7425a Mon Sep 17 00:00:00 2001 From: CEisenhofer Date: Thu, 16 Jul 2026 11:46:41 +0200 Subject: [PATCH] 2 bug fixes for regex monadic decomposition --- src/ast/euf/euf_sgraph.cpp | 36 ++++++++++++++++++++++ src/ast/rewriter/seq_range_collapse.cpp | 40 +++++++++++-------------- src/ast/rewriter/seq_split.cpp | 11 +++++-- src/smt/seq/seq_nielsen.cpp | 32 +++++++++++++++++--- src/smt/seq/seq_regex.cpp | 19 ++++++++++++ src/test/regex_range_collapse.cpp | 32 ++++++++++---------- 6 files changed, 124 insertions(+), 46 deletions(-) diff --git a/src/ast/euf/euf_sgraph.cpp b/src/ast/euf/euf_sgraph.cpp index af6b308557..962cc2cd81 100644 --- a/src/ast/euf/euf_sgraph.cpp +++ b/src/ast/euf/euf_sgraph.cpp @@ -20,6 +20,7 @@ Author: #include "ast/euf/euf_seq_plugin.h" #include "ast/arith_decl_plugin.h" #include "ast/rewriter/th_rewriter.h" +#include "ast/rewriter/seq_range_collapse.h" #include "ast/ast_pp.h" namespace euf { @@ -147,6 +148,23 @@ namespace euf { expr* e = n->m_expr; n->m_rigid = e && (m_seq.str.is_replace(e) || m_seq.str.is_replace_all(e) || m_seq.str.is_replace_re(e) || m_seq.str.is_replace_re_all(e)); + // re.of_pred also has no dedicated snode kind, but over a lambda in + // the recognized range fragment it is just the canonical multi-range + // character class emitted by seq::range_predicate_to_regex. Treat it + // as a settled single-character regex leaf — ground and classical — + // so memberships over it (or regexes containing it) stay primitive + // and the leaf/emptiness machinery engages; collect_re_predicates + // contributes its interval boundaries to the minterm partition. + // A lambda outside the fragment keeps the conservative non-ground + // treatment (nothing can partition on it). + if (e && m_seq.re.is_of_pred(e)) { + n->m_regex_free = false; + seq::range_predicate rp(m_seq.max_char()); + if (seq::regex_to_range_predicate(m_seq, e, rp)) { + n->m_ground = true; + n->m_is_classical = true; + } + } } break; @@ -795,6 +813,24 @@ namespace euf { if (m_seq.re.is_empty(e)) return; + // re.of_pred over a range-fragment lambda: the canonical multi-range + // character class (see seq::range_predicate_to_regex). Contribute one + // single-range regex per interval so the minterm partition sees its + // boundaries. Outside the fragment nothing can be extracted; such an + // snode is non-ground (see compute_metadata), so the is_ground gates in + // front of the minterm consumers keep it out of these paths. + if (m_seq.re.is_of_pred(e)) { + seq::range_predicate rp(m_seq.max_char()); + if (seq::regex_to_range_predicate(m_seq, e, rp)) { + sort* re_sort = e->get_sort(); + for (unsigned i = 0; i < rp.num_ranges(); ++i) { + auto [rlo, rhi] = rp[i]; + preds.push_back(m_seq.re.mk_range(re_sort, rlo, rhi)); + } + } + return; + } + // Expected compound regex operators are handled by recursion below. // If a leaf survives to this point, it is an unhandled regex form. if (re->num_args() == 0) { diff --git a/src/ast/rewriter/seq_range_collapse.cpp b/src/ast/rewriter/seq_range_collapse.cpp index d2af71f6b3..7f072a6458 100644 --- a/src/ast/rewriter/seq_range_collapse.cpp +++ b/src/ast/rewriter/seq_range_collapse.cpp @@ -25,51 +25,51 @@ namespace seq { // 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, - seq::range_predicate &out) { + range_predicate &out) { unsigned maxc = sq.max_char(); expr *a = nullptr, *b = nullptr; unsigned c = 0; if (m.is_true(pred)) { - out = seq::range_predicate::top(maxc); + out = range_predicate::top(maxc); return true; } if (m.is_false(pred)) { - out = seq::range_predicate::empty(maxc); + out = 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); + out = range_predicate::singleton(c, maxc); return true; } if (b == x && sq.is_const_char(a, c)) { - out = seq::range_predicate::singleton(c, maxc); + out = 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); + out = 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); + out = range_predicate::range(0, c, maxc); return true; } return false; } if (m.is_not(pred, a)) { - seq::range_predicate s(maxc); + range_predicate s(maxc); if (!pred_to_rp(m, sq, x, a, s)) return false; out = ~s; return true; } if (m.is_and(pred)) { - out = seq::range_predicate::top(maxc); + out = range_predicate::top(maxc); for (expr *arg : *to_app(pred)) { - seq::range_predicate s(maxc); + range_predicate s(maxc); if (!pred_to_rp(m, sq, x, arg, s)) return false; out = out & s; @@ -77,9 +77,9 @@ namespace seq { return true; } if (m.is_or(pred)) { - out = seq::range_predicate::empty(maxc); + out = range_predicate::empty(maxc); for (expr *arg : *to_app(pred)) { - seq::range_predicate s(maxc); + range_predicate s(maxc); if (!pred_to_rp(m, sq, x, arg, s)) return false; out = out | s; @@ -202,10 +202,6 @@ namespace seq { return false; } - static expr_ref mk_unit_string_from_char(seq_util& u, unsigned c) { - return expr_ref(u.str.mk_string(zstring(c)), u.get_manager()); - } - static expr_ref mk_single_range_regex(seq_util& u, unsigned lo, unsigned hi, sort* re_sort) { ast_manager& m = u.get_manager(); return expr_ref(u.re.mk_range(re_sort, lo, hi), m); @@ -224,12 +220,10 @@ namespace seq { auto [lo, hi] = p[0]; return mk_single_range_regex(u, lo, hi, re_sort); } - // Build single-range AST nodes first, then sort by expression id - // so the resulting right-associated union matches the canonical - // id-sorted shape that seq_rewriter::merge_regex_sets expects. - // Without this the merge algorithm produces incorrect unions - // when it has to combine our materialized output with another - // (id-sorted) regex set. + // Fold a multi-range class into a single re.of_pred predicate + // (lambda ch. \/_i lo_i <= ch <= hi_i). The body stays inside the + // fragment recognized by pred_to_rp, so regex_to_range_predicate + // round-trips it back to the same range_predicate. expr_ref_vector ranges(m); expr_ref bound(m.mk_var(0, char_sort), m); symbol char_sym("ch"); @@ -239,7 +233,7 @@ namespace seq { ranges.push_back(m.mk_and(ch.mk_le(ch.mk_char(lo), bound), ch.mk_le(bound, ch.mk_char(hi)))); } expr_ref body(m.mk_or(ranges), m); - return expr_ref(m.mk_lambda(1, &char_sort, &char_sym, body), m); + return expr_ref(u.re.mk_of_pred(m.mk_lambda(1, &char_sort, &char_sym, body)), m); } expr_ref unfold_fold(seq_rewriter &rw, expr *r) { diff --git a/src/ast/rewriter/seq_split.cpp b/src/ast/rewriter/seq_split.cpp index 68a0e6af23..f12032bb77 100644 --- a/src/ast/rewriter/seq_split.cpp +++ b/src/ast/rewriter/seq_split.cpp @@ -344,8 +344,10 @@ expr_ref seq_split::try_derivative_split(expr* r, sort* seq_sort, obj_hashtable< deriv_memo.insert(r); sort* re_sort = rex.mk_re(seq_sort); expr_ref unfolded(m); - if (m.is_true(nb)) unfolded = rex.mk_epsilon(seq_sort); // E(r) = eps - else unfolded = rex.mk_empty(re_sort); // E(r) = bot + if (m.is_true(nb)) + unfolded = rex.mk_epsilon(seq_sort); // E(r) = eps + else + unfolded = rex.mk_empty(re_sort); // E(r) = bot 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) { @@ -614,12 +616,17 @@ expr_ref seq_split::from_split_set(split_set const& s) { return acc; } +static unsigned cnt = 0; + expr_ref seq_split::head_normalize(expr* t, split_mode mode, unsigned threshold, split_oracle const& oracle, bool& ok, obj_hashtable& deriv_memo) { ok = true; expr *a = nullptr, *b = nullptr, *r = nullptr, *s = nullptr; + cnt++; + // std::cout << cnt << std::endl; + // already a frontier node if (is_frontier(t)) return expr_ref(t, m); diff --git a/src/smt/seq/seq_nielsen.cpp b/src/smt/seq/seq_nielsen.cpp index 083ec4cee4..5e3e17c022 100644 --- a/src/smt/seq/seq_nielsen.cpp +++ b/src/smt/seq/seq_nielsen.cpp @@ -2448,6 +2448,14 @@ namespace seq { // rule to identify and compare ancestors. node->m_dfs_path_pos = cur_path.size(); + // Cut bookkeeping is per-visit: values left over from an earlier traversal + // (hot-restart) describe a different path. Reset them so the early unsat + // returns below (sticky general conflict, cache hit, simplify/arith + // conflict) report a clean, cut-free closure to the parent's fold instead + // of leaking a stale cut. + node->m_subtree_lowlink = UINT_MAX; + node->m_subtree_has_cut = false; + if (node->is_general_conflict()) { ++m_stats.m_num_simplify_conflict; return search_result::unsat; @@ -2797,6 +2805,17 @@ namespace seq { // node's string signature alone. Make it sticky (survives // hot-restart) and memoize it in the transposition table. node->set_general_conflict(); + // The internal cuts (if any) deferred to this node or its + // descendants and are DISCHARGED by this closure — nothing + // escapes, so report a clean closure to the parent's fold. + // Leaking the internal cut upward lets an ancestor with a + // mixed closure (this child string-only + another child + // arithmetic) mark itself general_conflict (all children + // are) and THEN take the "cut may hide a model" unknown + // exit — the sticky mark reads as unsat on the next + // traversal: a spurious UNSAT. + node->m_subtree_has_cut = false; + node->m_subtree_lowlink = UINT_MAX; // EXCEPTION: a lazy-factorization continuation (is_rf_cont) // aliases its parent's — and ultimately the original, undivided // membership's — string signature, yet its subtree only explored @@ -4697,11 +4716,16 @@ namespace seq { } } // Self-concatenation (e.g. x++x): the tail collapses back onto the - // exact same token as the head, so Δ and ∇ constrain the same - // variable simultaneously and must be checked jointly -- otherwise + // exact same SEQUENCE as the head, so Δ and ∇ constrain the same + // word simultaneously and must be checked jointly -- otherwise // a Δ/∇ pair that is only individually non-empty (e.g. ) - // is wrongly treated as feasible. - if (st->m_tail == first) + // is wrongly treated as feasible. The joint check is only sound + // when head and tail are the SAME sequence: comparing the tail + // against `first` alone (the first token of the whole membership + // string) also matches e.g. x·y·c·x, where head = x·y is a + // DIFFERENT word than the tail x — intersecting Δ with ∇ there + // over-prunes feasible splits (a spurious UNSAT). + if (st->m_head == st->m_tail) regexes_p.push_back(sn_q); if (m_seq_regex->check_intersection_emptiness(regexes_p, 100) == l_true) { eliminated_dep = m_dep_mgr.mk_join(eliminated_dep, first_filter_dep); diff --git a/src/smt/seq/seq_regex.cpp b/src/smt/seq/seq_regex.cpp index ef3e8af2aa..cc88f0a363 100644 --- a/src/smt/seq/seq_regex.cpp +++ b/src/smt/seq/seq_regex.cpp @@ -16,6 +16,7 @@ Author: --*/ #include "smt/seq/seq_regex.h" +#include "ast/rewriter/seq_range_collapse.h" namespace seq { @@ -193,6 +194,24 @@ namespace seq { if (re->is_fail() || re->is_full_char() || re->is_full_seq()) return; + // re.of_pred over a range-fragment lambda: the canonical multi-range + // character class (see seq::range_predicate_to_regex). Boundaries at + // every interval edge. Outside the fragment the snode is non-ground + // (see sgraph::compute_metadata) and is_empty_bfs's ground gate keeps + // it away from this partition. + if (seq.re.is_of_pred(e)) { + range_predicate rp(seq.max_char()); + if (regex_to_range_predicate(seq, e, rp)) { + for (unsigned i = 0; i < rp.num_ranges(); ++i) { + auto [rlo, rhi] = rp[i]; + bounds.push_back(rlo); + if (rhi < zstring::max_char()) + bounds.push_back(rhi + 1); + } + } + return; + } + // If we reached a leaf and none of the expected leaf forms matched, // this is a regex constructor we did not account for in boundary // extraction and should fail loudly in debug builds. diff --git a/src/test/regex_range_collapse.cpp b/src/test/regex_range_collapse.cpp index 1c81a424ae..3b3eb5b260 100644 --- a/src/test/regex_range_collapse.cpp +++ b/src/test/regex_range_collapse.cpp @@ -212,33 +212,31 @@ namespace { check(extract_range_chars(u, e, lo, hi) && lo == 'A' && hi == 'A', "{A} -> re.range A A"); } - // 2 ranges -> re.union(range_0, range_1) in canonical order + // 2 ranges -> re.of_pred(lambda) with a RegEx(String) sort, round-tripping + // back to the same range set { range_predicate p = range_predicate::range('0', '9', M) | range_predicate::range('a', 'z', M); expr_ref e = range_predicate_to_regex(u, p, str_sort); - expr* a = nullptr; expr* b = nullptr; - check(u.re.is_union(e, a, b), "2-range -> union"); - unsigned lo0 = 0, hi0 = 0, lo1 = 0, hi1 = 0; - check(extract_range_chars(u, a, lo0, hi0) && lo0 == '0' && hi0 == '9', - "union arg0 = (0-9) (canonical: lower lo first)"); - check(extract_range_chars(u, b, lo1, hi1) && lo1 == 'a' && hi1 == 'z', - "union arg1 = (a-z)"); + expr* lam = nullptr; + check(u.re.is_of_pred(e, lam) && is_lambda(lam), "2-range -> of_pred(lambda)"); + sort* elem = nullptr; + check(u.is_re(e, elem) && u.is_string(elem), "of_pred regex is RegEx(String)"); + range_predicate p_out(M); + check(regex_to_range_predicate(u, e, p_out), "2-range of_pred translatable"); + check(p == p_out, "2-range of_pred round-trip equal"); } - // 3 ranges -> right-associated union + // 3 ranges -> re.of_pred(lambda), round-tripping back to the same range set { range_predicate p = range_predicate::range(0, 5, M) | range_predicate::range(10, 15, M) | range_predicate::range(20, 25, M); expr_ref e = range_predicate_to_regex(u, p, str_sort); - expr* a = nullptr; expr* rest = nullptr; - check(u.re.is_union(e, a, rest), "3-range -> union(...)"); - unsigned lo = 0, hi = 0; - check(extract_range_chars(u, a, lo, hi) && lo == 0 && hi == 5, "first arg = (0-5)"); - expr* b = nullptr; expr* c = nullptr; - check(u.re.is_union(rest, b, c), "rest is union(...,...)"); - check(extract_range_chars(u, b, lo, hi) && lo == 10 && hi == 15, "second range"); - check(extract_range_chars(u, c, lo, hi) && lo == 20 && hi == 25, "third range"); + expr* lam = nullptr; + check(u.re.is_of_pred(e, lam) && is_lambda(lam), "3-range -> of_pred(lambda)"); + range_predicate p_out(M); + check(regex_to_range_predicate(u, e, p_out), "3-range of_pred translatable"); + check(p == p_out, "3-range of_pred round-trip equal"); } // Round-trip identity for an arbitrary range-set {