projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 944cb8e) | patch
(proof-new) SMT proof postprocess callback (#4883)
authorAndrew Reynolds <andrew.j.reynolds@gmail.com>
Tue, 18 Aug 2020 18:47:57 +0000 (13:47 -0500)
committerGitHub <noreply@github.com>
Tue, 18 Aug 2020 18:47:57 +0000 (13:47 -0500)
commit50b0f20be87cd82f464d3f8fc15a5fa2f0a47556
tree5340e7ff62e17a9954e3ab931f5edd4d1e4ba995tree
parent944cb8e5381c47ccc49955a19609921399bb9437commit | diff
(proof-new) SMT proof postprocess callback (#4883)

This is the callback class for processing the final proof, which connects proofs of preprocessing and expands unwanted macro steps based on proof granularity mode.

The next step will be to add the ProofNodeUpdater that uses this callback and runs final sanity checks for checking proofs.
src/smt/proof_post_processor.cpp [new file with mode: 0644] blob
src/smt/proof_post_processor.h [new file with mode: 0644] blob