diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2020-10-06 07:00:22 -0500 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2020-10-06 07:00:22 -0500 |
| commit | cb54d547b2a0e99258cb4c754bc4d979abee93f8 (patch) | |
| tree | 679f1e91069e17ce0a6bfacd4fbe9d2ffe5ce1c3 /src/CMakeLists.txt | |
| parent | cd7680c5a23ade0bd8d7f0dfac4623ed318639bb (diff) | |
Add arithmetic preprocess module (#5188)
This class serves a similar purpose to the strings preprocess module (https://github.com/CVC4/CVC4/blob/master/src/theory/strings/theory_strings_preprocess.h).
It can potentially be used for reducing extended arithmetic operators on demand via lemmas.
This PR does not change the current behavior, but generalizes the use of operator elimination in TheoryArith to make this possible.
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 65223f3c5..4ca57effd 100644 --- a/src/CMakeLists.txt +++ b/src/CMakeLists.txt @@ -285,6 +285,8 @@ libcvc4_add_sources( theory/arith/arith_lemma.h theory/arith/arith_msum.cpp theory/arith/arith_msum.h + theory/arith/arith_preprocess.cpp + theory/arith/arith_preprocess.h theory/arith/arith_rewriter.cpp theory/arith/arith_rewriter.h theory/arith/arith_state.cpp |