Add arithmetic preprocess module (#5188)
authorAndrew Reynolds <andrew.j.reynolds@gmail.com>
Tue, 6 Oct 2020 12:00:22 +0000 (07:00 -0500)
committerGitHub <noreply@github.com>
Tue, 6 Oct 2020 12:00:22 +0000 (07:00 -0500)
commitcb54d547b2a0e99258cb4c754bc4d979abee93f8
tree679f1e91069e17ce0a6bfacd4fbe9d2ffe5ce1c3
parentcd7680c5a23ade0bd8d7f0dfac4623ed318639bb
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.
src/CMakeLists.txt
src/theory/arith/arith_preprocess.cpp [new file with mode: 0644]
src/theory/arith/arith_preprocess.h [new file with mode: 0644]
src/theory/arith/theory_arith.cpp
src/theory/arith/theory_arith.h