diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2020-10-01 17:19:08 -0500 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2020-10-01 17:19:08 -0500 |
| commit | 75d47fd5b65c3fe6dff3ef591d8331f737ca1cea (patch) | |
| tree | f8b5d619f3cfe0b9d3f1e9e22c9209606b2c53e3 /src/CMakeLists.txt | |
| parent | 776ee02237b06eb3130e56af4d98d9ff36667d8b (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.
Diffstat (limited to 'src/CMakeLists.txt')
| -rw-r--r-- | src/CMakeLists.txt | 2 |
1 files changed, 2 insertions, 0 deletions
diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt index c0f53e455..7c22b880a 100644 --- a/src/CMakeLists.txt +++ b/src/CMakeLists.txt @@ -400,6 +400,8 @@ libcvc4_add_sources( theory/arith/type_enumerator.h theory/arrays/array_info.cpp theory/arrays/array_info.h + theory/arrays/inference_manager.cpp + theory/arrays/inference_manager.h theory/arrays/proof_checker.cpp theory/arrays/proof_checker.h theory/arrays/skolem_cache.cpp |