diff options
| author | Gereon Kremer <gkremer@stanford.edu> | 2021-02-19 09:34:36 +0100 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2021-02-19 09:34:36 +0100 |
| commit | ce58453982ddd53a5fc08d9db4c6c3f49b852838 (patch) | |
| tree | e77cb66ff4d5bca985524d3c2befd33d580916af /src/CMakeLists.txt | |
| parent | 6ae21de6f85d9629018c1b6bf912ef39f3e169fb (diff) | |
Cleanup of inferences in arithmetic theory (#5927)
This PR cleans up several issues in the arithmetic theory mostly related to its usage of InferenceId and the TheoryInferenceManager:
remove the ArithLemma class and uses SimpleTheoryLemma instead
only use NlLemma if we actually need it
use proper InferenceIds everywhere
remove unused code in the nonlinear extension
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 96f98bd4c..3bfb248a4 100644 --- a/src/CMakeLists.txt +++ b/src/CMakeLists.txt @@ -291,8 +291,6 @@ libcvc4_add_sources( theory/arith/approx_simplex.h theory/arith/arith_ite_utils.cpp theory/arith/arith_ite_utils.h - theory/arith/arith_lemma.cpp - theory/arith/arith_lemma.h theory/arith/arith_msum.cpp theory/arith/arith_msum.h theory/arith/arith_preprocess.cpp |