Delete nnf_tactic.cpp, subsume into cnf_nnf_simplifier

Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>

src/ast/simplifiers/cnf_nnf.h

@@ -26,18 +26,24 @@ class cnf_nnf_simplifier : public dependent_expr_simplifier {
 
     defined_names m_defined_names;
     th_rewriter   m_rewriter;
+    params_ref    m_params;
     
 public:
     cnf_nnf_simplifier(ast_manager& m, params_ref const& p, dependent_expr_state& fmls):
         dependent_expr_simplifier(m, fmls),
         m_defined_names(m),
-        m_rewriter(m, p){
+        m_rewriter(m, p),
+        m_params(p) {
     }
 
     char const* name() const override { return "cnf-nnf"; }
+
+    void updt_params(params_ref const& p) override { m_params.append(p); m_rewriter.updt_params(p); }
+
+    void collect_param_descrs(param_descrs& r) override { nnf::get_param_descrs(r); }
     
     void reduce() override {
-        nnf apply_nnf(m, m_defined_names);
+        nnf apply_nnf(m, m_defined_names, m_params);
         expr_ref_vector  push_todo(m);
         proof_ref_vector push_todo_prs(m);
         proof_ref pr(m);

src/tactic/core/CMakeLists.txt

@@ -9,7 +9,6 @@ z3_add_component(core_tactics
     elim_term_ite_tactic.cpp
     elim_uncnstr_tactic.cpp
     injectivity_tactic.cpp
-    nnf_tactic.cpp
     occf_tactic.cpp
     pb_preprocess_tactic.cpp
     propagate_values_tactic.cpp

src/tactic/core/nnf_tactic.cpp

@@ -1,106 +0,0 @@
-/*++
-Copyright (c) 2011 Microsoft Corporation
-
-Module Name:
-
-    nnf_tactic.cpp
-
-Abstract:
-
-    NNF tactic
-
-Author:
-
-    Leonardo de Moura (leonardo) 2011-12-28.
-
-Revision History:
-
---*/
-#include "ast/normal_forms/nnf.h"
-#include "tactic/tactical.h"
-#include "ast/converters/generic_model_converter.h"
-
-class nnf_tactic : public tactic {
-    params_ref    m_params;
-    nnf *         m_nnf;
-
-    struct set_nnf {
-        nnf_tactic & m_owner;
-        
-        set_nnf(nnf_tactic & owner, nnf & n):
-            m_owner(owner) {
-            m_owner.m_nnf = &n;            
-        }
-        
-        ~set_nnf() {
-            m_owner.m_nnf = nullptr;
-        }
-    };
-public:
-    nnf_tactic(params_ref const & p):
-        m_params(p),
-        m_nnf(nullptr) {
-        TRACE(nnf, tout << "nnf_tactic constructor: " << p << "\n";);
-    }
-
-    tactic * translate(ast_manager & m) override {
-        return alloc(nnf_tactic, m_params);
-    }
-
-    char const* name() const override { return "nnf"; }
-
-    void updt_params(params_ref const & p) override { m_params.append(p); }
-
-    void collect_param_descrs(param_descrs & r) override { nnf::get_param_descrs(r); }
-
-    void operator()(goal_ref const & g, goal_ref_buffer & result) override {
-        TRACE(nnf, tout << "params: " << m_params << "\n"; g->display(tout););
-        tactic_report report("nnf", *g);
-        bool produce_proofs = g->proofs_enabled();
-
-        ast_manager & m = g->m();
-        defined_names dnames(m);
-        nnf local_nnf(m, dnames, m_params);
-        set_nnf setter(*this, local_nnf);
-        
-        expr_ref_vector defs(m);
-        proof_ref_vector def_prs(m);
-        
-        expr_ref   new_curr(m);
-        proof_ref  new_pr(m);
-        
-        unsigned sz = g->size();
-        for (unsigned i = 0; !g->inconsistent() && i < sz; ++i) {
-            expr * curr = g->form(i);
-            local_nnf(curr, defs, def_prs, new_curr, new_pr);
-            if (produce_proofs) {
-                proof * pr = g->pr(i);
-                new_pr     = m.mk_modus_ponens(pr, new_pr);
-            }
-            g->update(i, new_curr, new_pr, g->dep(i));
-        }
-        
-        sz = defs.size();
-        for (unsigned i = 0; !g->inconsistent() && i < sz; ++i) {
-            if (produce_proofs)
-                g->assert_expr(defs.get(i), def_prs.get(i), nullptr);
-            else
-                g->assert_expr(defs.get(i), nullptr, nullptr);
-        }
-        g->inc_depth();
-        result.push_back(g.get());
-        unsigned num_extra_names = dnames.get_num_names();
-        if (num_extra_names > 0 && !g->inconsistent()) {
-            generic_model_converter * fmc = alloc(generic_model_converter, m, "nnf");
-            g->add(fmc);
-            for (unsigned i = 0; i < num_extra_names; ++i)
-                fmc->hide(dnames.get_name_decl(i));
-        }
-    }
-    
-    void cleanup() override {}
-};
-
-tactic * mk_snf_tactic(ast_manager & m, params_ref const & p) {
-    return alloc(nnf_tactic, p);
-}

src/tactic/core/nnf_tactic.h

@@ -64,7 +64,12 @@ Once all negations are pushed inside, the resulting formula is in NNF.
 class ast_manager;
 class tactic;
 
-tactic * mk_snf_tactic(ast_manager & m, params_ref const & p = params_ref());
+inline tactic * mk_snf_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(cnf_nnf_simplifier, m, p, s);
+        });
+}
 
 inline tactic * mk_nnf_tactic(ast_manager & m, params_ref const & p = params_ref()) {
     return alloc(dependent_expr_state_tactic, m, p,