From 0ddae476216452696dbb809173afc2fb440a7c57 Mon Sep 17 00:00:00 2001
From: Haniel Barbosa <hanielbbarbosa@gmail.com>
Date: Wed, 14 Oct 2020 01:43:14 -0300
Subject: [PATCH] using NOT_NOT_ELIM rather than macros to do double-neg
 elimination (#5261)

---
 src/prop/proof_cnf_stream.cpp           | 22 +++++++++-------------
 src/theory/theory_proof_step_buffer.cpp |  2 +-
 2 files changed, 10 insertions(+), 14 deletions(-)

diff --git a/src/prop/proof_cnf_stream.cpp b/src/prop/proof_cnf_stream.cpp
index 92212ded0..c7dd288af 100644
--- a/src/prop/proof_cnf_stream.cpp
+++ b/src/prop/proof_cnf_stream.cpp
@@ -110,13 +110,10 @@ void ProofCnfStream::convertAndAssert(TNode node, bool negated)
       // track double negation elimination
       if (negated)
       {
-        d_proof.addStep(node[0],
-                        PfRule::MACRO_SR_PRED_TRANSFORM,
-                        {node.notNode()},
-                        {node[0]});
-        Trace("cnf") << "ProofCnfStream::convertAndAssert: "
-                        "MACRO_SR_PRED_TRANSFORM added norm "
-                     << node[0] << "\n";
+        d_proof.addStep(node[0], PfRule::NOT_NOT_ELIM, {node.notNode()}, {});
+        Trace("cnf")
+            << "ProofCnfStream::convertAndAssert: NOT_NOT_ELIM added norm "
+            << node[0] << "\n";
       }
       convertAndAssert(node[0], !negated);
       break;
@@ -139,13 +136,12 @@ void ProofCnfStream::convertAndAssert(TNode node, bool negated)
       {
         // track double negation elimination
         //    (not (not n))
-        //   -------------- MACRO_SR_PRED_TRANSFORM
+        //   -------------- NOT_NOT_ELIM
         //        n
-        d_proof.addStep(
-            nnode, PfRule::MACRO_SR_PRED_TRANSFORM, {node.notNode()}, {nnode});
-        Trace("cnf") << "ProofCnfStream::convertAndAssert: "
-                        "MACRO_SR_PRED_TRANSFORM added norm "
-                     << nnode << "\n";
+        d_proof.addStep(nnode, PfRule::NOT_NOT_ELIM, {node.notNode()}, {});
+        Trace("cnf")
+            << "ProofCnfStream::convertAndAssert: NOT_NOT_ELIM added norm "
+            << nnode << "\n";
       }
       if (added)
       {
diff --git a/src/theory/theory_proof_step_buffer.cpp b/src/theory/theory_proof_step_buffer.cpp
index 5aa909a37..a08b15901 100644
--- a/src/theory/theory_proof_step_buffer.cpp
+++ b/src/theory/theory_proof_step_buffer.cpp
@@ -225,7 +225,7 @@ Node TheoryProofStepBuffer::elimDoubleNegLit(Node n)
   // eliminate double neg
   if (n.getKind() == kind::NOT && n[0].getKind() == kind::NOT)
   {
-    addStep(PfRule::MACRO_SR_PRED_TRANSFORM, {n}, {n[0][0]}, n[0][0]);
+    addStep(PfRule::NOT_NOT_ELIM, {n}, {}, n[0][0]);
     return n[0][0];
   }
   return n;
-- 
2.30.2