projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: c137366) | patch
(proof-new) Make CombinationEngine proof producing (#4955)
authorAndrew Reynolds <andrew.j.reynolds@gmail.com>
Fri, 28 Aug 2020 20:40:16 +0000 (15:40 -0500)
committerGitHub <noreply@github.com>
Fri, 28 Aug 2020 20:40:16 +0000 (15:40 -0500)
commitf51d3e353fe8e50e5e73c37c17229e603a56ecdd
treed3a00e94d2850aaac623d81df04a0bfc7f762087tree
parentc137366e668aff70b1739a1f2c5cf8e6e2e28a72commit | diff
(proof-new) Make CombinationEngine proof producing (#4955)

Makes combination engine proof producing (for Boolean splits). Followup PRs will start to add proof production in TheoryEngine.
src/theory/combination_care_graph.cpp diff | blob | history
src/theory/combination_care_graph.h diff | blob | history
src/theory/combination_engine.cpp diff | blob | history
src/theory/combination_engine.h diff | blob | history
src/theory/theory_engine.cpp diff | blob | history
src/theory/theory_engine.h diff | blob | history