From 30784ecaa936e4dc417d269096b278eab1931ed9 Mon Sep 17 00:00:00 2001 From: "copilot-swe-agent[bot]" <198982749+Copilot@users.noreply.github.com> Date: Sat, 21 Feb 2026 23:26:04 +0000 Subject: [PATCH 1/5] Initial plan 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 2/5] 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)") */ 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 3/5] 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)") */ From b149f27e82d3370ba3bb4fdc9b0d4df0283835ec Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sun, 22 Feb 2026 00:25:24 -0800 Subject: [PATCH 4/5] Delete src/tactic/core/der_tactic.cpp --- src/tactic/core/der_tactic.cpp | 17 ----------------- 1 file changed, 17 deletions(-) delete mode 100644 src/tactic/core/der_tactic.cpp diff --git a/src/tactic/core/der_tactic.cpp b/src/tactic/core/der_tactic.cpp deleted file mode 100644 index 47c23e036..000000000 --- a/src/tactic/core/der_tactic.cpp +++ /dev/null @@ -1,17 +0,0 @@ -/*++ -Copyright (c) 2012 Microsoft Corporation - -Module Name: - - der_tactic.cpp - -Abstract: - - DER tactic - -Author: - - Leonardo de Moura (leonardo) 2012-10-20 - ---*/ -#include "tactic/core/der_tactic.h" From 57d1667d28d30c36ac6d8684c7660858eb1c6e80 Mon Sep 17 00:00:00 2001 From: "copilot-swe-agent[bot]" <198982749+Copilot@users.noreply.github.com> Date: Sun, 22 Feb 2026 08:47:14 +0000 Subject: [PATCH 5/5] Remove der_tactic.cpp from CMakeLists.txt (file was deleted) Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com> --- src/tactic/core/CMakeLists.txt | 1 - 1 file changed, 1 deletion(-) diff --git a/src/tactic/core/CMakeLists.txt b/src/tactic/core/CMakeLists.txt index a191b6251..9aa3cc2ba 100644 --- a/src/tactic/core/CMakeLists.txt +++ b/src/tactic/core/CMakeLists.txt @@ -5,7 +5,6 @@ z3_add_component(core_tactics cofactor_term_ite_tactic.cpp collect_statistics_tactic.cpp ctx_simplify_tactic.cpp - der_tactic.cpp elim_term_ite_tactic.cpp elim_uncnstr_tactic.cpp injectivity_tactic.cpp