diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2020-09-02 10:56:53 -0500 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2020-09-02 10:56:53 -0500 |
| commit | 8d10d1053a0616d8e791219f651b22c10f9039bf (patch) | |
| tree | 4d145eebdc3687a2200a6334f84c65c800a99577 /src/CMakeLists.txt | |
| parent | 1e93736643667d7b8e4ff9fa5f86596ce1ec31d3 (diff) | |
(new theory) Update TheoryArrays to the new standard (#5000)
This includes using the standard d_conflict flag in TheoryState and splitting its check into 3 callbacks.
It also deletes some unused code and eliminates an assertion (line 791 of theory_arrays.cpp) which doesn't hold in a central architecture.
Further work on standardization for arrays will add an InferenceManager to guard its uses of asserting facts to equality engine (both for proofs and configurable theory combination).
FYI @barrettcw
Diffstat (limited to 'src/CMakeLists.txt')
| -rw-r--r-- | src/CMakeLists.txt | 2 |
1 files changed, 0 insertions, 2 deletions
diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt index 2da04ce66..0ad9526a5 100644 --- a/src/CMakeLists.txt +++ b/src/CMakeLists.txt @@ -354,8 +354,6 @@ libcvc4_add_sources( theory/arith/type_enumerator.h theory/arrays/array_info.cpp theory/arrays/array_info.h - theory/arrays/static_fact_manager.cpp - theory/arrays/static_fact_manager.h theory/arrays/theory_arrays.cpp theory/arrays/theory_arrays.h theory/arrays/theory_arrays_rewriter.cpp |