From: Lachnitt <lachnitt@stanford.edu>
Date: Fri, 17 Sep 2021 20:37:53 +0000 (-0700)
Subject: [proofs] Alethe: Added Final Callback Function to alethe_proof_processor (#7200)
X-Git-Tag: cvc5-1.0.0~1201
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=03b640fb95528063772c80555d7f06a9884cd870;p=cvc5.git

[proofs] Alethe: Added Final Callback Function to alethe_proof_processor (#7200)

Added final callback class to alethe_proof_processor header file.

Co-authored-by: Haniel Barbosa <hanielbbarbosa@gmail.com>
---

diff --git a/src/proof/alethe/alethe_post_processor.h b/src/proof/alethe/alethe_post_processor.h
index 6b5ab04d7..323f8767a 100644
--- a/src/proof/alethe/alethe_post_processor.h
+++ b/src/proof/alethe/alethe_post_processor.h
@@ -99,6 +99,52 @@ class AletheProofPostprocessCallback : public ProofNodeUpdaterCallback
                            CDProof& cdp);
 };
 
+/**
+ * Final callback class used by the Alethe converter to add the last step to a
+ * proof in the following two cases. The last step should always be printed as
+ * (cl).
+ *
+ * 1. If the last step of a proof which is false is reached it is printed as (cl
+ *    false).
+ * 2. If one of the assumptions is false it is printed as false.
+ *
+ * Thus, an additional resolution step with (cl (not true)) has to be added to
+ * transfer (cl false) into (cl).
+ */
+class AletheProofPostprocessFinalCallback : public ProofNodeUpdaterCallback
+{
+ public:
+  AletheProofPostprocessFinalCallback(ProofNodeManager* pnm);
+  ~AletheProofPostprocessFinalCallback() {}
+  /** Should proof pn be updated? It should, if the last step is printed as (cl
+   * false) or if it is an assumption (in that case it is printed as false).
+   * Since the proof node should not be traversed, this method will always set
+   * continueUpdate to false.
+   */
+  bool shouldUpdate(std::shared_ptr<ProofNode> pn,
+                    const std::vector<Node>& fa,
+                    bool& continueUpdate) override;
+  /**
+   * This method gets a proof node pn. If the last step of the proof is false
+   * which is printed as (cl false) it updates the proof for false such that
+   * (cl) is printed instead.
+   */
+  bool update(Node res,
+              PfRule id,
+              const std::vector<Node>& children,
+              const std::vector<Node>& args,
+              CDProof* cdp,
+              bool& continueUpdate) override;
+
+ private:
+  /** The proof node manager */
+  ProofNodeManager* d_pnm;
+  /** The cl operator is defined as described in the
+    * AletheProofPostprocessCallback class above
+   **/
+  Node d_cl;
+};
+
 }  // namespace proof
 
 }  // namespace cvc5