[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>

1 files changed, 22 insertions, 1 deletions

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