From 4f5c19acfaf053c2b89aca8f1f6969ac8f7f07b4 Mon Sep 17 00:00:00 2001
From: "copilot-swe-agent[bot]" <198982749+Copilot@users.noreply.github.com>
Date: Wed, 1 Apr 2026 17:16:12 +0000
Subject: [PATCH] remove unused functions from seq_nielsen

Agent-Logs-Url: https://github.com/Z3Prover/z3/sessions/ebc080bd-ce7f-43cc-8778-0b9b955b39a0

Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
---
 src/smt/seq/seq_nielsen.cpp | 26 --------------------------
 src/smt/seq/seq_nielsen.h   |  7 -------
 2 files changed, 33 deletions(-)

diff --git a/src/smt/seq/seq_nielsen.cpp b/src/smt/seq/seq_nielsen.cpp
index d5f52dfa7..091c02f3a 100644
--- a/src/smt/seq/seq_nielsen.cpp
+++ b/src/smt/seq/seq_nielsen.cpp
@@ -2252,32 +2252,6 @@ namespace seq {
         return false;
     }
 
-    // -----------------------------------------------------------------------
-    // Helper: find a power token in any str_eq
-    // -----------------------------------------------------------------------
-
-    euf::snode* nielsen_graph::find_power_token(nielsen_node* node) const {
-        for (str_eq const& eq : node->str_eqs()) {
-            if (eq.is_trivial())
-                continue;
-            if (!eq.m_lhs || !eq.m_rhs)
-                continue;
-            euf::snode_vector toks;
-            eq.m_lhs->collect_tokens(toks);
-            for (euf::snode* t : toks) {
-                if (t->is_power())
-                    return t;
-            }
-            toks.reset();
-            eq.m_rhs->collect_tokens(toks);
-            for (euf::snode* t : toks) {
-                if (t->is_power())
-                    return t;
-            }
-        }
-        return nullptr;
-    }
-
     // -----------------------------------------------------------------------
     // Helper: find a power token facing a constant (char) head
     // Returns true if found, sets power, other_head, eq_out.
diff --git a/src/smt/seq/seq_nielsen.h b/src/smt/seq/seq_nielsen.h
index 5a522a74a..0cd304a96 100644
--- a/src/smt/seq/seq_nielsen.h
+++ b/src/smt/seq/seq_nielsen.h
@@ -964,10 +964,6 @@ namespace seq {
         // create a fresh variable with a unique name and the given sequence sort
         euf::snode* mk_fresh_var(sort* s);
 
-        // create a fresh symbolic character: seq.unit(fresh_char_const)
-        // analogous to ZIPT's SymCharToken creation
-        euf::snode* mk_fresh_char_var();
-
         // deterministic modifier: var = ε, same-head cancel
         bool apply_det_modifier(nielsen_node* node);
 
@@ -1066,9 +1062,6 @@ namespace seq {
 
         bool apply_var_num_unwinding_mem(nielsen_node* node);
 
-        // find the first power token in any str_eq at this node
-        euf::snode* find_power_token(nielsen_node* node) const;
-
         // find a power token facing a constant (char/non-var) token at either end
         // of an equation; returns orientation via `fwd` (true=head, false=tail).
         bool find_power_vs_non_var(nielsen_node* node, euf::snode*& power, euf::snode*& other_head, str_eq const*& eq_out, bool& fwd) const;