strings arith checks preprocessing pass: step 1 (#5747)
authoryoni206 <yoni206@users.noreply.github.com>
Wed, 6 Jan 2021 22:41:13 +0000 (14:41 -0800)
committerGitHub <noreply@github.com>
Wed, 6 Jan 2021 22:41:13 +0000 (16:41 -0600)
commit3b0b4f554841847aa529a1d95585aedcba5b0fee
tree8e870a8dc0398f85d0c6799e3c9a26cf96bd4d40
parentc32c2c5f5203fff6d4982755e3784f6f2f315b3b
strings arith checks preprocessing pass: step 1 (#5747)

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 first step. It only includes the preprocessing pass infrastructure, with an empty implementation of the main function StrLenSimplify::simplify. It also adds the pass to the registry.
The implementation of this function is not complicated, but is left for a future PR in order to keep the PR short.

Future PRs will include an implementation of the main function, tests, and a command line option to turn on the pass.
src/CMakeLists.txt
src/preprocessing/passes/foreign_theory_rewrite.cpp [new file with mode: 0644]
src/preprocessing/passes/foreign_theory_rewrite.h [new file with mode: 0644]
src/preprocessing/preprocessing_pass_registry.cpp