[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 323f8767af3e6aab9e429e8302bdcc276388a45b..a19903f12e9c14c77bee4a3b731d166a401b9bc5 100644 (file)
--- 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