From: Haniel Barbosa <hanielbbarbosa@gmail.com>
Date: Tue, 22 Mar 2022 19:53:42 +0000 (-0300)
Subject: [proofs] Alethe: fixing formatting and adding missing comment (#7779)
X-Git-Tag: cvc5-1.0.0~209
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=0b2506b8db508f6fa1320e7534cd1b74cebffb22;p=cvc5.git

[proofs] Alethe: fixing formatting and adding missing comment (#7779)
---

diff --git a/src/proof/alethe/alethe_post_processor.cpp b/src/proof/alethe/alethe_post_processor.cpp
index 24d17676f..f698a5fbd 100644
--- a/src/proof/alethe/alethe_post_processor.cpp
+++ b/src/proof/alethe/alethe_post_processor.cpp
@@ -201,10 +201,9 @@ bool AletheProofPostprocessCallback::update(Node res,
     // -------------------------------------------- RESOLUTION
     //          (cl (not (and F1 ... Fn)))*
     //
-    // VP8: (cl (=> (and F1 ... Fn))) (cl (not (=> (and F1 ... Fn) false))
-    //      (not (and F1 ... Fn)))
+    // VP8: (cl (=> (and F1 ... Fn) false))
     // VP9: (cl (= (=> (and F1 ... Fn) false) (not (and F1 ... Fn))))
-    //
+    // VP10: (cl (not (=> (and F1 ... Fn) false)) (not (and F1 ... Fn)))
     //
     // Otherwise,
     //                T1
@@ -447,13 +446,14 @@ bool AletheProofPostprocessCallback::update(Node res,
       Node vp1 = nm->mkNode(
           kind::SEXPR, d_cl, args[0].notNode().notNode().notNode(), args[0]);
       Node vp2 = nm->mkNode(kind::SEXPR,
-                              d_cl,
-                              args[0].notNode().notNode().notNode().notNode(),
-                              args[0].notNode());
+                            d_cl,
+                            args[0].notNode().notNode().notNode().notNode(),
+                            args[0].notNode());
 
       return addAletheStep(AletheRule::NOT_NOT, vp2, vp2, {}, {}, *cdp)
-          && addAletheStep(AletheRule::NOT_NOT, vp1, vp1, {}, {}, *cdp)
-          && addAletheStepFromOr(AletheRule::RESOLUTION, res, {vp1, vp2}, {}, *cdp);
+             && addAletheStep(AletheRule::NOT_NOT, vp1, vp1, {}, {}, *cdp)
+             && addAletheStepFromOr(
+                 AletheRule::RESOLUTION, res, {vp1, vp2}, {}, *cdp);
     }
     // ======== Equality resolution
     // See proof_rule.h for documentation on the EQ_RESOLVE rule. This
@@ -644,7 +644,7 @@ bool AletheProofPostprocessCallback::update(Node res,
     // * the corresponding proof node is (and F1 ... Fn)
     case PfRule::AND_INTRO:
     {
-      std::vector<Node> neg_Nodes = {d_cl,res};
+      std::vector<Node> neg_Nodes = {d_cl, res};
       for (size_t i = 0, size = children.size(); i < size; i++)
       {
         neg_Nodes.push_back(children[i].notNode());
@@ -1813,9 +1813,10 @@ AletheProofPostprocess::AletheProofPostprocess(ProofNodeManager* pnm,
 
 AletheProofPostprocess::~AletheProofPostprocess() {}
 
-void AletheProofPostprocess::process(std::shared_ptr<ProofNode> pf) {
+void AletheProofPostprocess::process(std::shared_ptr<ProofNode> pf)
+{
   // Translate proof node
-  ProofNodeUpdater updater(d_pnm, d_cb,true,false);
+  ProofNodeUpdater updater(d_pnm, d_cb, true, false);
   updater.process(pf->getChildren()[0]);
 
   // In the Alethe proof format the final step has to be (cl). However, after