2 bug fixes for regex monadic decomposition

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) {

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) {

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<expr>& 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);

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. <eps, "a">)
-            // 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);

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.

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
         {