projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 0f9ae46) | patch
(proof-new) CDProof inherits from ProofGenerator (#4622)
authorAndrew Reynolds <andrew.j.reynolds@gmail.com>
Fri, 19 Jun 2020 23:55:19 +0000 (18:55 -0500)
committerGitHub <noreply@github.com>
Fri, 19 Jun 2020 23:55:19 +0000 (18:55 -0500)
commite8000a4693ecc1f8418c80726032ef6937e36241
treeb6869ef2f8da60f76d6f946f38fb885f1d817d33tree
parent0f9ae462a99f04607c6406afb129fa1393f1ce33commit | diff
(proof-new) CDProof inherits from ProofGenerator (#4622)

This design simplifies a number of issues and makes the PRefProofGenerator class obsolete.
src/expr/lazy_proof.cpp diff | blob | history
src/expr/lazy_proof.h diff | blob | history
src/expr/proof.cpp diff | blob | history
src/expr/proof.h diff | blob | history
src/expr/proof_generator.cpp diff | blob | history
src/expr/proof_generator.h diff | blob | history
src/expr/term_conversion_proof_generator.cpp diff | blob | history