using NOT_NOT_ELIM rather than macros to do double-neg elimination (#5261)

diff --git a/src/prop/proof_cnf_stream.cpp b/src/prop/proof_cnf_stream.cpp
index 92212ded0a2f41f2c30d6bb80e2b327042b29f3e..c7dd288afdb4473bd45510fccc592a5f340220b8 100644 (file)
--- 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 5aa909a375c3a907dba0602e03a69c6d1636bc5b..a08b159011fcd76c496852cf511ea2a5742a839f 100644 (file)
--- 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;