projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 8c04f16) | patch
Foreign theory rewrite option (#5763)
authoryoni206 <yoni206@users.noreply.github.com>
Tue, 12 Jan 2021 15:42:37 +0000 (07:42 -0800)
committerGitHub <noreply@github.com>
Tue, 12 Jan 2021 15:42:37 +0000 (09:42 -0600)
commita38a642eab886d298ea3b658c9823544c3a35f27
treeca0769ce5cad74fbff11e4dea6a5288a0be4ddd0tree
parent8c04f1639607b34b56e3eaa8d3188b27e1454b41commit | diff
Foreign theory rewrite option (#5763)

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 third and final step. It adds the user-facing option that turn this feature on, as well as regression tests.
src/options/smt_options.toml diff | blob | history
src/smt/process_assertions.cpp diff | blob | history
test/regress/CMakeLists.txt diff | blob | history
test/regress/regress0/seq/len_simplify.smt2 [new file with mode: 0644] blob