projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 776ee02) | patch
(proof-new) Make arrays proof producing (#5112)
authorAndrew Reynolds <andrew.j.reynolds@gmail.com>
Thu, 1 Oct 2020 22:19:08 +0000 (17:19 -0500)
committerGitHub <noreply@github.com>
Thu, 1 Oct 2020 22:19:08 +0000 (17:19 -0500)
commit75d47fd5b65c3fe6dff3ef591d8331f737ca1cea
treef8b5d619f3cfe0b9d3f1e9e22c9209606b2c53e3tree
parent776ee02237b06eb3130e56af4d98d9ff36667d8bcommit | diff
(proof-new) Make arrays proof producing (#5112)

This includes adding a basic inference manager to arrays that ensures that the correct applications of PfRule are given to the inference manager.

Note that some calls to lemma are yet to be converted. Also note that some minor simplifications were made for unnecessary parts of the code.
src/CMakeLists.txt diff | blob | history
src/theory/arrays/inference_manager.cpp [new file with mode: 0644] blob
src/theory/arrays/inference_manager.h [new file with mode: 0644] blob
src/theory/arrays/theory_arrays.cpp diff | blob | history
src/theory/arrays/theory_arrays.h diff | blob | history