From a4c2a2b22c105e1b9045ddc18cbf8ad652cee49d Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Sun, 6 Nov 2022 11:57:46 -0800
Subject: [PATCH] use ast_util::mk_not to avoid redundant double negations
 during nff

---
 src/ast/normal_forms/nnf.cpp | 9 +++++----
 1 file changed, 5 insertions(+), 4 deletions(-)

diff --git a/src/ast/normal_forms/nnf.cpp b/src/ast/normal_forms/nnf.cpp
index d0398543b..a35956454 100644
--- a/src/ast/normal_forms/nnf.cpp
+++ b/src/ast/normal_forms/nnf.cpp
@@ -22,6 +22,7 @@ Notes:
 #include "ast/normal_forms/nnf.h"
 #include "ast/normal_forms/nnf_params.hpp"
 #include "ast/used_vars.h"
+#include "ast/ast_util.h"
 #include "ast/well_sorted.h"
 #include "ast/act_cache.h"
 #include "ast/rewriter/var_subst.h"
@@ -137,7 +138,7 @@ class skolemizer {
                 if (is_sk_hack(p)) {
                     expr * sk_hack = to_app(p)->get_arg(0);
                     if (q->get_kind() == forall_k) // check whether is in negative/positive context.
-                        tmp  = m.mk_or(body, m.mk_not(sk_hack)); // negative context
+                        tmp  = m.mk_or(body, mk_not(m, sk_hack)); // negative context
                     else
                         tmp  = m.mk_and(body, sk_hack); // positive context
                     body = tmp;
@@ -148,7 +149,7 @@ class skolemizer {
         p = nullptr;
         if (m_proofs_enabled) {
             if (q->get_kind() == forall_k) 
-                p = m.mk_skolemization(m.mk_not(q), m.mk_not(r));
+                p = m.mk_skolemization(mk_not(m, q), mk_not(m, r));
             else
                 p = m.mk_skolemization(q, r);
         }
@@ -388,7 +389,7 @@ struct nnf::imp {
     }
 
     void skip(expr * t, bool pol) {
-        expr * r = pol ? t : m.mk_not(t);
+        expr * r = pol ? t : mk_not(m, t);
         m_result_stack.push_back(r);
         if (proofs_enabled()) {
             m_result_pr_stack.push_back(m.mk_oeq_reflexivity(r));
@@ -639,7 +640,7 @@ struct nnf::imp {
                 m_name_quant->operator()(t, m_todo_defs, m_todo_proofs, n2, pr2);
 
             if (!fr.m_pol)
-                n2 = m.mk_not(n2);
+                n2 = mk_not(m, n2);
             m_result_stack.push_back(n2);
             if (proofs_enabled()) {
                 if (!fr.m_pol) {