From c18db6080a8e62800aab17f163957822c8007010 Mon Sep 17 00:00:00 2001
From: "copilot-swe-agent[bot]" <198982749+Copilot@users.noreply.github.com>
Date: Sat, 21 Feb 2026 23:52:01 +0000
Subject: [PATCH] Convert cofactor-term-ite tactic to also expose as a
 simplifier

Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
---
 src/tactic/core/cofactor_term_ite_tactic.h | 52 ++++++++++++++++++++--
 1 file changed, 49 insertions(+), 3 deletions(-)

diff --git a/src/tactic/core/cofactor_term_ite_tactic.h b/src/tactic/core/cofactor_term_ite_tactic.h
index 68568c8ce..0cb9f9142 100644
--- a/src/tactic/core/cofactor_term_ite_tactic.h
+++ b/src/tactic/core/cofactor_term_ite_tactic.h
@@ -29,11 +29,57 @@ It hoists nested if-then-else expressions inside terms into the top level of the
 #pragma once
 
 #include "util/params.h"
-class ast_manager;
-class tactic;
+#include "tactic/tactic.h"
+#include "tactic/dependent_expr_state_tactic.h"
+#include "ast/simplifiers/dependent_expr_state.h"
+#include "tactic/core/cofactor_elim_term_ite.h"
+
+class cofactor_term_ite_simplifier : public dependent_expr_simplifier {
+    params_ref             m_params;
+    cofactor_elim_term_ite m_elim_ite;
+
+public:
+    cofactor_term_ite_simplifier(ast_manager& m, params_ref const& p, dependent_expr_state& s)
+        : dependent_expr_simplifier(m, s), m_params(p), m_elim_ite(m, p) {}
+
+    char const* name() const override { return "cofactor-term-ite"; }
+
+    void updt_params(params_ref const& p) override {
+        m_params.append(p);
+        m_elim_ite.updt_params(m_params);
+    }
+
+    void collect_param_descrs(param_descrs& r) override {
+        m_elim_ite.collect_param_descrs(r);
+    }
+
+    bool supports_proofs() const override { return false; }
+
+    void reduce() override {
+        expr_ref new_fml(m);
+        for (unsigned idx : indices()) {
+            auto const& d = m_fmls[idx];
+            m_elim_ite(d.fml(), new_fml);
+            if (new_fml != d.fml())
+                m_fmls.update(idx, dependent_expr(m, new_fml, nullptr, d.dep()));
+        }
+    }
+};
+
+inline dependent_expr_simplifier* mk_cofactor_term_ite_simplifier(
+        ast_manager& m, params_ref const& p, dependent_expr_state& s) {
+    return alloc(cofactor_term_ite_simplifier, m, p, s);
+}
+
+inline tactic* mk_cofactor_term_ite2_tactic(ast_manager& m, params_ref const& p = params_ref()) {
+    return alloc(dependent_expr_state_tactic, m, p, mk_cofactor_term_ite_simplifier);
+}
 
 tactic * mk_cofactor_term_ite_tactic(ast_manager & m, params_ref const & p = params_ref());
+
 /*
-  ADD_TACTIC("cofactor-term-ite", "eliminate term if-the-else using cofactors.", "mk_cofactor_term_ite_tactic(m, p)")
+  ADD_TACTIC("cofactor-term-ite", "eliminate term if-then-else using cofactors.", "mk_cofactor_term_ite_tactic(m, p)")
+  ADD_TACTIC("cofactor-term-ite2", "eliminate term if-then-else using cofactors.", "mk_cofactor_term_ite2_tactic(m, p)")
+  ADD_SIMPLIFIER("cofactor-term-ite", "eliminate term if-then-else using cofactors.", "mk_cofactor_term_ite_simplifier(m, p, s)")
 */