From 3a390dda1867c069a5e829d4344edeb09f2da3b2 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Sun, 14 Jun 2026 15:05:25 -0700
Subject: [PATCH] add membership elimination to legacy elim_uncnstr
 pre-processor. Detect xor encodings

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
 src/ast/rewriter/seq_rewriter.cpp       | 18 ++++++++++++++++++
 src/tactic/core/elim_uncnstr_tactic.cpp | 23 ++++++++++++++++++++++-
 2 files changed, 40 insertions(+), 1 deletion(-)

diff --git a/src/ast/rewriter/seq_rewriter.cpp b/src/ast/rewriter/seq_rewriter.cpp
index 1654c5777..abf5809cb 100644
--- a/src/ast/rewriter/seq_rewriter.cpp
+++ b/src/ast/rewriter/seq_rewriter.cpp
@@ -3314,11 +3314,20 @@ expr_ref seq_rewriter::mk_antimirov_deriv_restrict(expr* e, expr* d, expr* cond)
 
 expr_ref seq_rewriter::mk_regex_union_normalize(expr* r1, expr* r2) {
     expr_ref _r1(r1, m()), _r2(r2, m());
+    expr *a1, *b1, *a2, *b2;
     SASSERT(m_util.is_re(r1));
     SASSERT(m_util.is_re(r2));
     expr_ref result(m());
     std::function<bool(expr*, expr*&, expr*&)> test = [&](expr* t, expr*& a, expr*& b) { return re().is_union(t, a, b); };
     std::function<expr* (expr*, expr*)> compose = [&](expr* r1, expr* r2) { return (is_subset(r1, r2) ? r2 : (is_subset(r2, r1) ? r1 : re().mk_union(r1, r2))); };
+    std::function<bool(expr *, expr *)> is_complement = [&](expr *a, expr *b) {
+        expr *s;
+        if (re().is_complement(a, s) && s == b)
+            return true;
+        if (re().is_complement(b, s) && s == a)
+            return true;
+        return false;
+    };    
     if (r1 == r2 || re().is_empty(r2) || re().is_full_seq(r1))
         result = r1;
     else if (re().is_empty(r1) || re().is_full_seq(r2))
@@ -3327,6 +3336,15 @@ expr_ref seq_rewriter::mk_regex_union_normalize(expr* r1, expr* r2) {
         result = r1;
     else if (re().is_dot_plus(r2) && re().get_info(r1).min_length > 0)
         result = r2;
+    // (R1 \ R2) U (R2 \ R1) = R1 xor R2
+    else if (re().is_intersection(r1, a1, a2) && re().is_intersection(r2, b1, b2) && 
+        is_complement(a1, b2) && is_complement(a2, b1)) {
+        result = re().mk_xor(a1, re().mk_complement(a2));
+    }   
+    else if (re().is_intersection(r1, a1, a2) && re().is_intersection(r2, b1, b2) && 
+        is_complement(a1, b1) && is_complement(a2, b2)) {
+        result = re().mk_xor(a1, re().mk_complement(a2));
+    } 
     else
         result = merge_regex_sets(r1, r2, re().mk_full_seq(r1->get_sort()), test, compose);
     return result;
diff --git a/src/tactic/core/elim_uncnstr_tactic.cpp b/src/tactic/core/elim_uncnstr_tactic.cpp
index 9caf76c4a..69e5465c1 100644
--- a/src/tactic/core/elim_uncnstr_tactic.cpp
+++ b/src/tactic/core/elim_uncnstr_tactic.cpp
@@ -19,6 +19,7 @@ Notes:
 #include "tactic/tactical.h"
 #include "ast/converters/generic_model_converter.h"
 #include "ast/rewriter/rewriter_def.h"
+#include "ast/rewriter/seq_rewriter.h"
 #include "ast/arith_decl_plugin.h"
 #include "ast/bv_decl_plugin.h"
 #include "ast/recfun_decl_plugin.h"
@@ -803,10 +804,10 @@ class elim_uncnstr_tactic : public tactic {
 
         // x ++ y -> z, x -> z, y -> eps
         app * process_seq_app(func_decl * f, unsigned num, expr * const * args) {
+            app *r = nullptr;
             switch (f->get_decl_kind()) {
             case _OP_STRING_CONCAT:
             case OP_SEQ_CONCAT: {
-                app * r = nullptr;
                 expr* x, *y;
                 if (uncnstr(args[0]) && num == 2 &&
                     args[1]->get_ref_count() == 1 && 
@@ -833,6 +834,26 @@ class elim_uncnstr_tactic : public tactic {
                 
                 return r;
             }
+            case OP_SEQ_IN_RE:
+                if (uncnstr(args[0]) && m_seq_util.re.is_ground(args[1]) && m_seq_util.is_string(args[0]->get_sort())) {
+                    zstring s1;
+                    expr *re = args[1];
+                    seq_rewriter rw(m());
+                    if (l_true != rw.some_string_in_re(re, s1))
+                        return nullptr;
+                    zstring s2;
+                    expr_ref not_re(m_seq_util.re.mk_complement(re), m());
+                    if (l_true != rw.some_string_in_re(not_re, s2))
+                        return nullptr;
+
+                    mk_fresh_uncnstr_var_for(f, num, args, r);
+                    expr_ref witness1 = expr_ref(m_seq_util.str.mk_string(s1), m());
+                    expr_ref witness2 = expr_ref(m_seq_util.str.mk_string(s2), m());
+                    if (m_mc)
+                        add_def(args[0], m().mk_ite(r, witness1, witness2));
+                    return r;
+                }
+                return nullptr;
             default:
                 return nullptr;
             }