From c9cae773043bcfe94efa7b37cba6c3f4aa108abd Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Wed, 25 Dec 2024 10:56:16 -0800
Subject: [PATCH] update regex membership to be slightly better tuned

---
 src/ast/rewriter/seq_rewriter.cpp |  3 ++-
 src/ast/sls/sls_seq_plugin.cpp    | 31 +++++++++++++++----------------
 src/ast/sls/sls_seq_plugin.h      |  3 ++-
 3 files changed, 19 insertions(+), 18 deletions(-)

diff --git a/src/ast/rewriter/seq_rewriter.cpp b/src/ast/rewriter/seq_rewriter.cpp
index 3ce396593..7675e0d23 100644
--- a/src/ast/rewriter/seq_rewriter.cpp
+++ b/src/ast/rewriter/seq_rewriter.cpp
@@ -3790,6 +3790,7 @@ expr_ref  seq_rewriter::simplify_path(expr* elem, expr* path) {
 
 
 expr_ref seq_rewriter::mk_der_antimirov_union(expr* r1, expr* r2) {
+    verbose_stream() << "union " << r1->get_id() << " " << r2->get_id() << "\n";
     return mk_der_op(_OP_RE_ANTIMIROV_UNION, r1, r2);
 }
 
@@ -4584,7 +4585,7 @@ br_status seq_rewriter::mk_str_in_regexp(expr* a, expr* b, expr_ref& result) {
         result = mk_in_antimirov(tl, mk_antimirov_deriv(hd, b, m().mk_true()));
         return BR_REWRITE_FULL;
     }
-
+    
     if (get_head_tail_reversed(a, hd, tl)) {
         result = re().mk_reverse(re().mk_derivative(tl, re().mk_reverse(b)));
         result = re().mk_in_re(hd, result);
diff --git a/src/ast/sls/sls_seq_plugin.cpp b/src/ast/sls/sls_seq_plugin.cpp
index e8cdb7c91..2a5f05c10 100644
--- a/src/ast/sls/sls_seq_plugin.cpp
+++ b/src/ast/sls/sls_seq_plugin.cpp
@@ -96,8 +96,6 @@ Equality solving using stochastic Nelson.
 #include "ast/sls/sls_context.h"
 #include "ast/ast_pp.h"
 
-#include "ast/rewriter/th_rewriter.h"
-
 
 namespace sls {
     
@@ -105,7 +103,8 @@ namespace sls {
         plugin(c),
         seq(c.get_manager()),
         a(c.get_manager()),
-        rw(c.get_manager())
+        rw(c.get_manager()),
+        thrw(c.get_manager())
     {
         m_fid = seq.get_family_id();
     }
@@ -1705,13 +1704,17 @@ namespace sls {
 
     // Regular expressions
 
-    bool seq_plugin::is_in_re(zstring const& s, expr* r) {
-        expr_ref sval(seq.str.mk_string(s), m);
-        th_rewriter rw(m);
-        expr_ref in_re(seq.re.mk_in_re(sval, r), m);
-        rw(in_re);
-        SASSERT(m.limit().is_canceled() || m.is_true(in_re) || m.is_false(in_re));
-        return m.is_true(in_re);
+    bool seq_plugin::is_in_re(zstring const& s, expr* _r) {
+        expr_ref r(_r, m);
+        for (unsigned i = 0; i < s.length(); ++i) {
+            expr_ref ch(seq.str.mk_char(s[i]), m);
+            expr_ref r1 = rw.mk_derivative(ch, r);
+            if (seq.re.is_empty(r1))
+                return false;   
+            r = r1;
+        }
+        auto info = seq.re.get_info(r);
+        return info.nullable == l_true;
     }
 
     bool seq_plugin::repair_down_in_re(app* e) {
@@ -1721,12 +1724,8 @@ namespace sls {
         if (!info.interpreted)
             return false;
         auto s = strval0(x);
-        expr_ref xval(seq.str.mk_string(s), m);
-        expr_ref in_re(seq.re.mk_in_re(xval, y), m);
-        th_rewriter thrw(m);
-        thrw(in_re);
-        SASSERT(m.limit().is_canceled() || m.is_true(in_re) || m.is_false(in_re));
-        if (m.is_true(in_re) == ctx.is_true(e))
+        bool in_re = is_in_re(s, y);
+        if (in_re == ctx.is_true(e))
             return true;
 
         if (is_value(x))
diff --git a/src/ast/sls/sls_seq_plugin.h b/src/ast/sls/sls_seq_plugin.h
index cc36a0f91..cabfa6d9a 100644
--- a/src/ast/sls/sls_seq_plugin.h
+++ b/src/ast/sls/sls_seq_plugin.h
@@ -20,7 +20,7 @@ Author:
 #include "ast/seq_decl_plugin.h"
 #include "ast/arith_decl_plugin.h"
 #include "ast/rewriter/seq_rewriter.h"
-
+#include "ast/rewriter/th_rewriter.h"
 
 namespace sls {
     
@@ -45,6 +45,7 @@ namespace sls {
         seq_util seq;
         arith_util a;
         seq_rewriter rw;
+        th_rewriter thrw;
         scoped_ptr_vector<eval> m_values;
         indexed_uint_set m_chars;
         bool m_initialized = false;