projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: eed1028) | patch
(proof-new) Make theory preprocessor proofs self contained (#5642)
authorAndrew Reynolds <andrew.j.reynolds@gmail.com>
Wed, 9 Dec 2020 21:00:13 +0000 (15:00 -0600)
committerGitHub <noreply@github.com>
Wed, 9 Dec 2020 21:00:13 +0000 (15:00 -0600)
commitb060a8e0d55b870aa1abfde34cb7df560bf9fefc
tree75dcde4de5f241a3988966f0a0ad219bccb54c26tree
parenteed1028716c90df8f26aa1afa948f2deeb1cbdb7commit | diff
(proof-new) Make theory preprocessor proofs self contained (#5642)

Previously, there was a block of code in TheoryEngine::lemma for processing the proofs from theory preprocessing.

It is much cleaner if this block was self contained in TheoryPreprocessor.

This is required for the planned move of TheoryPreprocessor from TheoryEngine -> PropEngine.
src/theory/theory_engine.cpp diff | blob | history
src/theory/theory_preprocessor.cpp diff | blob | history
src/theory/theory_preprocessor.h diff | blob | history