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/theory/bags/theory_bags.cpp | |
| 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/theory/bags/theory_bags.cpp')
0 files changed, 0 insertions, 0 deletions