projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 145b936) | patch
(proof-new) Add builtin proof checker (#4537)
authorAndrew Reynolds <andrew.j.reynolds@gmail.com>
Wed, 3 Jun 2020 19:01:13 +0000 (14:01 -0500)
committerGitHub <noreply@github.com>
Wed, 3 Jun 2020 19:01:13 +0000 (14:01 -0500)
commitf70e265cd4e7df46a1b3b7e3cc67fbf9b9b1b528
tree289b34fd775c89b2d44b464b18d40f43d16e0630tree
parent145b9367255d2925b6b4e43818e223b9186bcfadcommit | diff
(proof-new) Add builtin proof checker (#4537)

This adds the proof checker for TheoryBuiltin, which handles the core proof rules (SCOPE and ASSUME) and all proof rules corresponding to generic operations on Node objects. This includes proof rules for rewriting and substitution, which are added in this PR.
src/CMakeLists.txt diff | blob | history
src/expr/proof_rule.cpp diff | blob | history
src/expr/proof_rule.h diff | blob | history
src/theory/builtin/proof_checker.cpp [new file with mode: 0644] blob
src/theory/builtin/proof_checker.h [new file with mode: 0644] blob