projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 0c6249a) | patch
(proof-new) Add the SMT proof post processor (#4913)
authorAndrew Reynolds <andrew.j.reynolds@gmail.com>
Fri, 28 Aug 2020 18:48:40 +0000 (13:48 -0500)
committerGitHub <noreply@github.com>
Fri, 28 Aug 2020 18:48:40 +0000 (13:48 -0500)
commitd1bb100d75aca76fdeb7a18b6c044035029ffe17
tree2ca30cbc452a68503747877c0c216afed2830c8ftree
parent0c6249a1b2177fda94526b66510474f2cb01a411commit | diff
(proof-new) Add the SMT proof post processor (#4913)

This PR adds the proof post-processor, which is the final authority on putting together the overall proof. It additionally implements lazy pedantic failures and statistics.

This PR also corrects a subtle bug in the elimination of SUBS which requires a TRUE_INTRO/FALSE_INTRO in certain cases.
src/smt/proof_post_processor.cpp diff | blob | history
src/smt/proof_post_processor.h diff | blob | history