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: using NOT_NOT_ELIM rather than macros to do double-neg elimination
 (#5261)

---
 src/prop/proof_cnf_stream.cpp | 22 +++++++++-------------
 1 file changed, 9 insertions(+), 13 deletions(-)

(limited to 'src/prop')

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)
       {
-- 
cgit v1.2.3