projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: aa8da1f) | patch
(proof-new) Theory preprocessor proof producing (#4807)
authorAndrew Reynolds <andrew.j.reynolds@gmail.com>
Tue, 18 Aug 2020 21:42:22 +0000 (16:42 -0500)
committerGitHub <noreply@github.com>
Tue, 18 Aug 2020 21:42:22 +0000 (16:42 -0500)
commit77fdb2327ae969a7d97b6eb67ad3526d78867b3a
tree8a16e05c53feca4085254566e7a15e1b14310704tree
parentaa8da1ff4e7f119408dbf14074b9a5efcb06618bcommit | diff
(proof-new) Theory preprocessor proof producing (#4807)

This makes the theory preprocessor proof producing in the new infrastructure, which involves updating its interfaces to TrustNode in a few places.
src/expr/proof_rule.cpp diff | blob | history
src/expr/proof_rule.h diff | blob | history
src/theory/builtin/proof_checker.cpp diff | blob | history
src/theory/theory_engine.cpp diff | blob | history
src/theory/theory_preprocessor.cpp diff | blob | history
src/theory/theory_preprocessor.h diff | blob | history