projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 2edc04b) | patch
(proof-new) Theory engine proof producing (#5195)
authorAndrew Reynolds <andrew.j.reynolds@gmail.com>
Fri, 9 Oct 2020 00:07:52 +0000 (19:07 -0500)
committerGitHub <noreply@github.com>
Fri, 9 Oct 2020 00:07:52 +0000 (19:07 -0500)
commitbc5056c8927e8fbffbe9e9d103f0a81f8ab49480
treeb600bdc0b38cd59bc08e248c265ad0e77af2c82ctree
parent2edc04bdfdac32ce899c98c4a8887c037b1f6a3fcommit | diff
(proof-new) Theory engine proof producing (#5195)

This completes proof support in TheoryEngine.

The main addition in this PR is to make its getExplanation method proof producing.
src/smt/smt_solver.cpp diff | blob | history
src/theory/theory_engine.cpp diff | blob | history
src/theory/theory_engine.h diff | blob | history