Merge pull request #8726 from Z3Prover/copilot/convert-cofactor-term-ite-to-simplifier

Convert `cofactor-term-ite` tactic to a simplifier

src/tactic/core/CMakeLists.txt

@@ -2,7 +2,6 @@ z3_add_component(core_tactics
   SOURCES
     blast_term_ite_tactic.cpp
     cofactor_elim_term_ite.cpp
-    cofactor_term_ite_tactic.cpp
     collect_statistics_tactic.cpp
     ctx_simplify_tactic.cpp
     elim_term_ite_tactic.cpp

src/tactic/core/cofactor_term_ite_tactic.cpp

@@ -1,71 +0,0 @@
-/*++
-Copyright (c) 2012 Microsoft Corporation
-
-Module Name:
-
-    cofactor_term_ite_tactic.cpp
-
-Abstract:
-
-    Wrap cofactor_elim_term_ite as a tactic.
-    Eliminate (ground) term if-then-else's using cofactors.
-
-Author:
-
-    Leonardo de Moura (leonardo) 2012-02-20.
-
-Revision History:
-
---*/
-#include "tactic/tactical.h"
-#include "tactic/core/cofactor_elim_term_ite.h"
-
-/**
-   \brief Wrapper for applying cofactor_elim_term_ite in an assertion set.
- */
-class cofactor_term_ite_tactic : public tactic {
-    params_ref             m_params;
-    cofactor_elim_term_ite m_elim_ite;
-
-    void process(goal & g) {
-        ast_manager & m = g.m();
-        unsigned idx = 0;
-        for (const auto& [f, dep, pr] : g) {
-            if (g.inconsistent())
-                break;
-            expr_ref new_f(m);
-            m_elim_ite(f, new_f);
-            g.update(idx++, new_f, nullptr, dep);            
-        }
-    }
-
-public:
-    cofactor_term_ite_tactic(ast_manager & m, params_ref const & p):
-        m_params(p),
-        m_elim_ite(m, p) {
-    }
-
-    tactic * translate(ast_manager & m) override {
-        return alloc(cofactor_term_ite_tactic, m, m_params);
-    }
-
-    char const* name() const override { return "cofactor"; }
-    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); }
-    
-    void  operator()(goal_ref const & g, goal_ref_buffer& result) override {
-        fail_if_proof_generation("cofactor-term-ite", g);
-        fail_if_unsat_core_generation("cofactor-term-ite", g);
-        tactic_report report("cofactor-term-ite", *g);
-        process(*(g.get()));
-        g->inc_depth();
-        result.push_back(g.get());
-    }
-    
-    void cleanup() override { return m_elim_ite.cleanup(); }
-
-};
-
-tactic * mk_cofactor_term_ite_tactic(ast_manager & m, params_ref const & p) {
-    return clean(alloc(cofactor_term_ite_tactic, m, p));
-}

src/tactic/core/cofactor_term_ite_tactic.h

@@ -29,11 +29,54 @@ 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_ite_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_SIMPLIFIER("cofactor-term-ite", "eliminate term if-then-else using cofactors.", "mk_cofactor_term_ite_simplifier(m, p, s)")
 */