From 7c4a3b2c1b6667e4953865a2333c0036d80be44c Mon Sep 17 00:00:00 2001
From: "copilot-swe-agent[bot]" <198982749+Copilot@users.noreply.github.com>
Date: Sun, 22 Feb 2026 00:40:49 +0000
Subject: [PATCH] Remove old der_tactic implementation; rename mk_der2_tactic
 to mk_der_tactic

Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
---
 src/tactic/core/der_tactic.cpp | 72 +---------------------------------
 src/tactic/core/der_tactic.h   | 10 +----
 2 files changed, 3 insertions(+), 79 deletions(-)

diff --git a/src/tactic/core/der_tactic.cpp b/src/tactic/core/der_tactic.cpp
index 4df46e19e..47c23e036 100644
--- a/src/tactic/core/der_tactic.cpp
+++ b/src/tactic/core/der_tactic.cpp
@@ -14,74 +14,4 @@ Author:
     Leonardo de Moura (leonardo) 2012-10-20
 
 --*/
-#include "ast/rewriter/der.h"
-#include "tactic/tactical.h"
-
-class der_tactic : public tactic {
-    struct imp {
-        ast_manager &   m_manager;
-        der_rewriter    m_r;
-        
-        imp(ast_manager & m):
-            m_manager(m),
-            m_r(m) {
-        }
-        
-        ast_manager & m() const { return m_manager; }
-                
-        void reset() {
-            m_r.reset();
-        }
-        
-        void operator()(goal & g) {
-            tactic_report report("der", g);
-            expr_ref   new_curr(m());
-            proof_ref  new_pr(m());
-            unsigned idx = 0;
-            for (auto [curr, dep, pr] : g) {
-                if (g.inconsistent())
-                    break;
-                m_r(curr, new_curr, new_pr);
-                new_pr = m().mk_modus_ponens(pr, new_pr);                
-                g.update(idx++, new_curr, new_pr, dep);
-            }
-            g.elim_redundancies();
-        }
-    };
-
-    imp *      m_imp;
-
-public:
-    der_tactic(ast_manager & m) {
-        m_imp = alloc(imp, m);
-    }
-
-    tactic * translate(ast_manager & m) override {
-        return alloc(der_tactic, m);
-    }
-
-    ~der_tactic() override {
-        dealloc(m_imp);
-    }
-
-    char const* name() const override { return "der"; }
-    
-    void operator()(goal_ref const & in, 
-                    goal_ref_buffer & result) override {
-        (*m_imp)(*(in.get()));
-        in->inc_depth();
-        result.push_back(in.get());
-    }
-
-    void cleanup() override {
-        ast_manager & m = m_imp->m();
-        imp * d = alloc(imp, m);
-        std::swap(d, m_imp);        
-        dealloc(d);
-    }
-    
-};
-
-tactic * mk_der_tactic(ast_manager & m) {
-    return alloc(der_tactic, m);
-}
+#include "tactic/core/der_tactic.h"
diff --git a/src/tactic/core/der_tactic.h b/src/tactic/core/der_tactic.h
index 36c375124..2fe82cf3b 100644
--- a/src/tactic/core/der_tactic.h
+++ b/src/tactic/core/der_tactic.h
@@ -52,12 +52,7 @@ equality resolution rule takes the form:
 #include "tactic/dependent_expr_state_tactic.h"
 #include "ast/simplifiers/der_simplifier.h"
 
-class ast_manager;
-class tactic;
-
-tactic * mk_der_tactic(ast_manager & m);
-
-inline tactic * mk_der2_tactic(ast_manager & m, params_ref const & p = params_ref()) {
+inline tactic * mk_der_tactic(ast_manager & m, params_ref const & p = params_ref()) {
     return alloc(dependent_expr_state_tactic, m, p,
         [](auto& m, auto& p, auto& s) -> dependent_expr_simplifier* {
             return alloc(der_simplifier, m, p, s);
@@ -65,8 +60,7 @@ inline tactic * mk_der2_tactic(ast_manager & m, params_ref const & p = params_re
 }
 
 /*
-  ADD_TACTIC("der", "destructive equality resolution.", "mk_der_tactic(m)")
-  ADD_TACTIC("der2", "destructive equality resolution.", "mk_der2_tactic(m, p)")
+  ADD_TACTIC("der", "destructive equality resolution.", "mk_der_tactic(m, p)")
   ADD_SIMPLIFIER("der", "destructive equality resolution.", "alloc(der_simplifier, m, p, s)")
 */