projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: b4eeffd) | patch
Add (context-dependent) Proof (#4323)
authorAndrew Reynolds <andrew.j.reynolds@gmail.com>
Fri, 17 Apr 2020 16:57:07 +0000 (11:57 -0500)
committerGitHub <noreply@github.com>
Fri, 17 Apr 2020 16:57:07 +0000 (11:57 -0500)
commitc431160c5c9d706cd6424dc6c4b9b316ff8a5941
tree8e4c55f5ffcda6ab373d4c3a0ffb5e296e9f93a1tree
parentb4eeffd63cc00369ec6b47ed4289577af3dec4ebcommit | diff
Add (context-dependent) Proof (#4323)

A (context-dependent) collection of proof steps that are linked to together to form a ProofNode dag.

Note that the name "Proof" is currently taken. I am calling this class "CDProof", although it is optionally context dependent.
src/expr/CMakeLists.txt diff | blob | history
src/expr/proof.cpp [new file with mode: 0644] blob
src/expr/proof.h [new file with mode: 0644] blob