projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 3f77b4a) | patch
(proof-new) Witness form proof generator (#4782)
authorAndrew Reynolds <andrew.j.reynolds@gmail.com>
Wed, 12 Aug 2020 16:41:26 +0000 (11:41 -0500)
committerGitHub <noreply@github.com>
Wed, 12 Aug 2020 16:41:26 +0000 (09:41 -0700)
commit9d1ce085de6df543d9d9a2fa9b8fa9001feb4b6b
tree023474f131ee9f21e829fc623e31de808b9235d5tree
parent3f77b4ac0d4ff8ab69e2f2932e9ced088bd339edcommit | diff
(proof-new) Witness form proof generator (#4782)

This class is responsible for the connection between terms and their witness form in the final proof.
src/CMakeLists.txt diff | blob | history
src/expr/lazy_proof.cpp diff | blob | history
src/expr/lazy_proof.h diff | blob | history
src/expr/proof_rule.cpp diff | blob | history
src/expr/proof_rule.h diff | blob | history
src/smt/witness_form.cpp [new file with mode: 0644] blob
src/smt/witness_form.h [new file with mode: 0644] blob
src/theory/builtin/proof_checker.cpp diff | blob | history