diff options
author | Lachnitt <lachnitt@stanford.edu> | 2021-09-17 14:03:01 -0700 |
---|---|---|
committer | GitHub <noreply@github.com> | 2021-09-17 21:03:01 +0000 |
commit | 1704b74ffa93b36a2e08e42ca21aad0991ad4d70 (patch) | |
tree | fd6f603b1668b1e35a3c5b8c379c1e7a38202bf5 | |
parent | 03b640fb95528063772c80555d7f06a9884cd870 (diff) |
[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>
-rw-r--r-- | src/proof/alethe/alethe_post_processor.h | 23 |
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 |