From 2eebe57467eb9bb34fbf40c9b1c3ad30ce3fe972 Mon Sep 17 00:00:00 2001
From: "copilot-swe-agent[bot]" <198982749+Copilot@users.noreply.github.com>
Date: Thu, 5 Mar 2026 03:21:02 +0000
Subject: [PATCH] Extract handle_empty_side helper in seq_nielsen to eliminate
 duplicate code

Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
---
 src/smt/seq/seq_nielsen.cpp | 71 +++++++++++++++----------------------
 src/smt/seq/seq_nielsen.h   |  9 +++++
 2 files changed, 38 insertions(+), 42 deletions(-)

diff --git a/src/smt/seq/seq_nielsen.cpp b/src/smt/seq/seq_nielsen.cpp
index d812e1eab..714ea061a 100644
--- a/src/smt/seq/seq_nielsen.cpp
+++ b/src/smt/seq/seq_nielsen.cpp
@@ -514,6 +514,33 @@ namespace seq {
     // nielsen_node: simplify_and_init
     // -----------------------------------------------------------------------
 
+    bool nielsen_node::handle_empty_side(euf::sgraph& sg, euf::snode* non_empty_side,
+                                         dep_tracker const& dep, bool& changed) {
+        euf::snode_vector tokens;
+        non_empty_side->collect_tokens(tokens);
+        bool all_vars_or_opaque = true;
+        bool has_char = false;
+        for (euf::snode* t : tokens) {
+            if (t->is_char()) has_char = true;
+            else if (!t->is_var() && t->kind() != euf::snode_kind::s_other) {
+                all_vars_or_opaque = false; break;
+            }
+        }
+        if (has_char || !all_vars_or_opaque) {
+            m_is_general_conflict = true;
+            m_reason = backtrack_reason::symbol_clash;
+            return true;
+        }
+        for (euf::snode* t : tokens) {
+            if (t->is_var()) {
+                nielsen_subst s(t, sg.mk_empty(), dep);
+                apply_subst(sg, s);
+                changed = true;
+            }
+        }
+        return false;
+    }
+
     simplify_result nielsen_node::simplify_and_init(nielsen_graph& g) {
         euf::sgraph& sg = g.sg();
         bool changed = true;
@@ -556,53 +583,13 @@ namespace seq {
 
                 // one side empty, the other not empty => conflict or substitution
                 if (eq.m_lhs->is_empty() && !eq.m_rhs->is_empty()) {
-                    euf::snode_vector tokens;
-                    eq.m_rhs->collect_tokens(tokens);
-                    bool all_vars_or_opaque = true;
-                    bool has_char = false;
-                    for (euf::snode* t : tokens) {
-                        if (t->is_char()) has_char = true;
-                        else if (!t->is_var() && t->kind() != euf::snode_kind::s_other) {
-                            all_vars_or_opaque = false; break;
-                        }
-                    }
-                    if (has_char || !all_vars_or_opaque) {
-                        m_is_general_conflict = true;
-                        m_reason = backtrack_reason::symbol_clash;
+                    if (handle_empty_side(sg, eq.m_rhs, eq.m_dep, changed))
                         return simplify_result::conflict;
-                    }
-                    for (euf::snode* t : tokens) {
-                        if (t->is_var()) {
-                            nielsen_subst s(t, sg.mk_empty(), eq.m_dep);
-                            apply_subst(sg, s);
-                            changed = true;
-                        }
-                    }
                     continue;
                 }
                 if (eq.m_rhs->is_empty() && !eq.m_lhs->is_empty()) {
-                    euf::snode_vector tokens;
-                    eq.m_lhs->collect_tokens(tokens);
-                    bool all_vars_or_opaque = true;
-                    bool has_char = false;
-                    for (euf::snode* t : tokens) {
-                        if (t->is_char()) has_char = true;
-                        else if (!t->is_var() && t->kind() != euf::snode_kind::s_other) {
-                            all_vars_or_opaque = false; break;
-                        }
-                    }
-                    if (has_char || !all_vars_or_opaque) {
-                        m_is_general_conflict = true;
-                        m_reason = backtrack_reason::symbol_clash;
+                    if (handle_empty_side(sg, eq.m_lhs, eq.m_dep, changed))
                         return simplify_result::conflict;
-                    }
-                    for (euf::snode* t : tokens) {
-                        if (t->is_var()) {
-                            nielsen_subst s(t, sg.mk_empty(), eq.m_dep);
-                            apply_subst(sg, s);
-                            changed = true;
-                        }
-                    }
                     continue;
                 }
 
diff --git a/src/smt/seq/seq_nielsen.h b/src/smt/seq/seq_nielsen.h
index 149fce993..9f7735699 100644
--- a/src/smt/seq/seq_nielsen.h
+++ b/src/smt/seq/seq_nielsen.h
@@ -502,6 +502,15 @@ namespace seq {
         // render constraint set as an HTML fragment for DOT node labels.
         // mirrors ZIPT's NielsenNode.ToHtmlString()
         std::ostream& display_html(std::ostream& out, ast_manager& m) const;
+
+    private:
+        // Helper: handle one empty vs one non-empty side of a string equality.
+        // Collects tokens from non_empty_side; if any token causes a conflict
+        // (is a concrete character or an unexpected kind), sets conflict flags
+        // and returns true. Otherwise substitutes all variables to empty,
+        // sets changed=true, and returns false.
+        bool handle_empty_side(euf::sgraph& sg, euf::snode* non_empty_side,
+                               dep_tracker const& dep, bool& changed);
     };
 
     // search statistics collected during Nielsen graph solving