From 292cf76b2cd8476ce08120c15cda8840b8fbd605 Mon Sep 17 00:00:00 2001
From: "copilot-swe-agent[bot]" <198982749+Copilot@users.noreply.github.com>
Date: Sat, 21 Feb 2026 23:27:28 +0000
Subject: [PATCH] Register cnf_nnf_simplifier and add nnf2 tactic wrapper

Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
---
 src/ast/simplifiers/cnf_nnf.h |  4 ++++
 src/tactic/core/nnf_tactic.h  | 11 +++++++++++
 2 files changed, 15 insertions(+)

diff --git a/src/ast/simplifiers/cnf_nnf.h b/src/ast/simplifiers/cnf_nnf.h
index 6cb1c346e..8d388f9c3 100644
--- a/src/ast/simplifiers/cnf_nnf.h
+++ b/src/ast/simplifiers/cnf_nnf.h
@@ -63,3 +63,7 @@ public:
 
     void pop(unsigned n) override { dependent_expr_simplifier::pop(n); m_defined_names.pop(n); }
 };
+
+/*
+  ADD_SIMPLIFIER("nnf", "put goal in negation normal form.", "alloc(cnf_nnf_simplifier, m, p, s)")
+*/
diff --git a/src/tactic/core/nnf_tactic.h b/src/tactic/core/nnf_tactic.h
index 083380be8..781212ed9 100644
--- a/src/tactic/core/nnf_tactic.h
+++ b/src/tactic/core/nnf_tactic.h
@@ -58,15 +58,26 @@ Once all negations are pushed inside, the resulting formula is in NNF.
 #pragma once
 
 #include "util/params.h"
+#include "tactic/dependent_expr_state_tactic.h"
+#include "ast/simplifiers/cnf_nnf.h"
+
 class ast_manager;
 class tactic;
 
 tactic * mk_snf_tactic(ast_manager & m, params_ref const & p = params_ref());
 tactic * mk_nnf_tactic(ast_manager & m, params_ref const & p = params_ref());
 
+inline tactic * mk_nnf2_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);
+        });
+}
+
 /*
   ADD_TACTIC("snf", "put goal in skolem normal form.", "mk_snf_tactic(m, p)")
   ADD_TACTIC("nnf", "put goal in negation normal form.", "mk_nnf_tactic(m, p)")
+  ADD_TACTIC("nnf2", "put goal in negation normal form.", "mk_nnf2_tactic(m, p)")
 */