Merge pull request #8730 from Z3Prover/copilot/convert-der-tactic-to-simplifier

Convert `der` tactic to a `dependent_expr_simplifier`

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; }
+};

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

src/tactic/core/der_tactic.cpp

@@ -1,87 +0,0 @@
-/*++
-Copyright (c) 2012 Microsoft Corporation
-
-Module Name:
-
-    der_tactic.cpp
-
-Abstract:
-
-    DER tactic
-
-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);
-}

src/tactic/core/der_tactic.h

@@ -49,12 +49,18 @@ equality resolution rule takes the form:
 --*/
 #pragma once
 
-class ast_manager;
+#include "tactic/dependent_expr_state_tactic.h"
-class tactic;
+#include "ast/simplifiers/der_simplifier.h"
 
-tactic * mk_der_tactic(ast_manager & m);
+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);
+        });
+}
 
 /*
-  ADD_TACTIC("der", "destructive equality resolution.", "mk_der_tactic(m)")
+  ADD_TACTIC("der", "destructive equality resolution.", "mk_der_tactic(m, p)")
+  ADD_SIMPLIFIER("der", "destructive equality resolution.", "alloc(der_simplifier, m, p, s)")
 */