diff options
| author | yoni206 <yoni206@users.noreply.github.com> | 2021-01-09 06:35:18 -0800 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2021-01-09 08:35:18 -0600 |
| commit | fcac065b47ea73aecb90f019c07dc6fa09cd914f (patch) | |
| tree | e8ec67725927e7e6a1a88cdda9ec91877f232fff /test/regress/CMakeLists.txt | |
| parent | 907437b1aba221181cd7817b18f103902d18770c (diff) | |
Strings arith checks preprocessing pass: step 2 (#5750)
We are adding a preprocessing pass that simplifies arithmetic constraints related to strings.
For example, len(s) >= 0 would be replaced by true.
This will make use of CVC4::theory::strings::ArithEntail::check.
This PR is the second step. It includes the implementation of the main function, as well as unit tests for it.
A subsequent PR will add a user-level option that will turn on this preprocessing pass, as well as regression tests.
Diffstat (limited to 'test/regress/CMakeLists.txt')
0 files changed, 0 insertions, 0 deletions