From 1704b74ffa93b36a2e08e42ca21aad0991ad4d70 Mon Sep 17 00:00:00 2001 From: Lachnitt Date: Fri, 17 Sep 2021 14:03:01 -0700 Subject: [PATCH] [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 --- src/proof/alethe/alethe_post_processor.h | 23 ++++++++++++++++++++++- 1 file changed, 22 insertions(+), 1 deletion(-) 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 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 -- 2.30.2