diff options
| author | Haniel Barbosa <hanielbbarbosa@gmail.com> | 2020-10-14 01:43:14 -0300 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2020-10-13 23:43:14 -0500 |
| commit | 0ddae476216452696dbb809173afc2fb440a7c57 (patch) | |
| tree | bbf443f354b7b72b6a7b47a905788f32203111a1 /src/prop | |
| parent | 9be90e37556d0654d7b7565ba6a62ba46eb44ccd (diff) | |
using NOT_NOT_ELIM rather than macros to do double-neg elimination (#5261)
Diffstat (limited to 'src/prop')
| -rw-r--r-- | src/prop/proof_cnf_stream.cpp | 22 |
1 files changed, 9 insertions, 13 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) { |