diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2021-07-12 13:55:13 -0500 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2021-07-12 18:55:13 +0000 |
| commit | b35641f1a4ac8d70cf868b273971ee7c5e3b35f0 (patch) | |
| tree | e05ba328b28ed05a11756712a9303ac05cefdd1d /src/CMakeLists.txt | |
| parent | e01ae3a87f4e1dc4b4511e8bd028d5c0838ccedc (diff) | |
Add arithmetic preprocess rewrite equality module (#6860)
This is the first part of a refactoring which will ensure that the linear arithmetic solver does not violate integer type constraints in its model.
This PR moves the method https://github.com/ajreynol/CVC4/blob/master/src/theory/arith/theory_arith.cpp#L129 to its own module / file.
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 811f1c5ae..9fce77c80 100644 --- a/src/CMakeLists.txt +++ b/src/CMakeLists.txt @@ -467,6 +467,8 @@ libcvc5_add_sources( theory/arith/operator_elim.h theory/arith/partial_model.cpp theory/arith/partial_model.h + theory/arith/pp_rewrite_eq.cpp + theory/arith/pp_rewrite_eq.h theory/arith/proof_checker.cpp theory/arith/proof_checker.h theory/arith/proof_macros.h |