From: Lachnitt <lachnitt@stanford.edu>
Date: Fri, 17 Sep 2021 21:03:01 +0000 (-0700)
Subject: [proofs] Alethe: Added Proof Postprocessor to alethe_proof_processor (#7202)
X-Git-Tag: cvc5-1.0.0~1200
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=1704b74ffa93b36a2e08e42ca21aad0991ad4d70;p=cvc5.git

[proofs] Alethe: Added Proof Postprocessor to alethe_proof_processor (#7202)

Added proof postprocessor 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 323f8767a..a19903f12 100644
--- a/src/proof/alethe/alethe_post_processor.h
+++ b/src/proof/alethe/alethe_post_processor.h
@@ -140,11 +140,32 @@ class AletheProofPostprocessFinalCallback : public ProofNodeUpdaterCallback
   /** The proof node manager */
   ProofNodeManager* d_pnm;
   /** The cl operator is defined as described in the
-    * AletheProofPostprocessCallback class above
+   * AletheProofPostprocessCallback class above
    **/
   Node d_cl;
 };
 
+/**
+ * The proof postprocessor module. This postprocesses a proof node into one
+ * using the rules from the Alethe calculus.
+ */
+class AletheProofPostprocess
+{
+ public:
+  AletheProofPostprocess(ProofNodeManager* pnm);
+  ~AletheProofPostprocess();
+  /** post-process */
+  void process(std::shared_ptr<ProofNode> pf);
+
+ private:
+  /** The proof node manager */
+  ProofNodeManager* d_pnm;
+  /** The post process callback */
+  AletheProofPostprocessCallback d_cb;
+  /** The final post process callback */
+  AletheProofPostprocessFinalCallback d_fcb;
+};
+
 }  // namespace proof
 
 }  // namespace cvc5