From c78b3d872df88a38747c700ec7bbd3cd6a8bcc0b Mon Sep 17 00:00:00 2001
From: "copilot-swe-agent[bot]" <198982749+Copilot@users.noreply.github.com>
Date: Sat, 21 Feb 2026 23:49:05 +0000
Subject: [PATCH] Convert der tactic to simplifier: add der_simplifier.h and
 update der_tactic.h

Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
---
 src/ast/simplifiers/der_simplifier.h | 42 ++++++++++++++++++++++++++++
 src/tactic/core/der_tactic.h         | 12 ++++++++
 2 files changed, 54 insertions(+)
 create mode 100644 src/ast/simplifiers/der_simplifier.h

diff --git a/src/ast/simplifiers/der_simplifier.h b/src/ast/simplifiers/der_simplifier.h
new file mode 100644
index 000000000..7c2c5703b
--- /dev/null
+++ b/src/ast/simplifiers/der_simplifier.h
@@ -0,0 +1,42 @@
+/*++
+Copyright (c) 2022 Microsoft Corporation
+
+Module Name:
+
+    der_simplifier.h
+
+Abstract:
+
+    Dependent expression simplifier for destructive equality resolution (DER).
+
+Author:
+
+    Nikolaj Bjorner (nbjorner) 2022-11-24
+
+--*/
+
+#pragma once
+
+#include "ast/simplifiers/dependent_expr_state.h"
+#include "ast/rewriter/der.h"
+
+class der_simplifier : public dependent_expr_simplifier {
+    der_rewriter m_r;
+public:
+    der_simplifier(ast_manager& m, params_ref const& p, dependent_expr_state& fmls)
+        : dependent_expr_simplifier(m, fmls), m_r(m) {}
+
+    char const* name() const override { return "der"; }
+
+    void reduce() override {
+        expr_ref  new_curr(m);
+        proof_ref new_pr(m);
+        for (unsigned idx : indices()) {
+            auto d = m_fmls[idx];
+            m_r(d.fml(), new_curr, new_pr);
+            m_fmls.update(idx, dependent_expr(m, new_curr, mp(d.pr(), new_pr), d.dep()));
+        }
+    }
+
+    bool supports_proofs() const override { return true; }
+};
diff --git a/src/tactic/core/der_tactic.h b/src/tactic/core/der_tactic.h
index 555d3108d..36c375124 100644
--- a/src/tactic/core/der_tactic.h
+++ b/src/tactic/core/der_tactic.h
@@ -49,12 +49,24 @@ equality resolution rule takes the form:
 --*/
 #pragma once
 
+#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()) {
+    return alloc(dependent_expr_state_tactic, m, p,
+        [](auto& m, auto& p, auto& s) -> dependent_expr_simplifier* {
+            return alloc(der_simplifier, m, p, s);
+        });
+}
+
 /*
   ADD_TACTIC("der", "destructive equality resolution.", "mk_der_tactic(m)")
+  ADD_TACTIC("der2", "destructive equality resolution.", "mk_der2_tactic(m, p)")
+  ADD_SIMPLIFIER("der", "destructive equality resolution.", "alloc(der_simplifier, m, p, s)")
 */