From 78b77b9d1ef35fc087230e045c0cce09d24728c3 Mon Sep 17 00:00:00 2001 From: CEisenhofer Date: Mon, 20 Jan 2025 16:51:34 +0100 Subject: [PATCH] Special case regex membership with constant string --- src/ast/rewriter/seq_rewriter.cpp | 21 +++++++++++++++++++++ 1 file changed, 21 insertions(+) diff --git a/src/ast/rewriter/seq_rewriter.cpp b/src/ast/rewriter/seq_rewriter.cpp index b117e02e1..4c4cc900f 100644 --- a/src/ast/rewriter/seq_rewriter.cpp +++ b/src/ast/rewriter/seq_rewriter.cpp @@ -4545,6 +4545,27 @@ br_status seq_rewriter::mk_str_in_regexp(expr* a, expr* b, expr_ref& result) { result = m().mk_true(); return BR_DONE; } + + zstring s; + if (str().is_string(a, s) && re().is_ground(b)) { + // Just check membership and replace by true/false + expr_ref r(b, m()); + for (unsigned i = 0; i < s.length(); i++) { + if (re().is_empty(r)) { + result = m().mk_false(); + return BR_DONE; + } + unsigned ch = s[i]; + expr_ref new_r = mk_derivative(m_util.mk_char(ch), r); + r = new_r; + } + if (re().get_info(r).nullable) + result = m().mk_true(); + else + result = m().mk_false(); + return BR_DONE; + } + expr_ref b_s(m()); if (lift_str_from_to_re(b, b_s)) { result = m_br.mk_eq_rw(a, b_s);