diff options
| author | yoni206 <yoni206@users.noreply.github.com> | 2021-01-12 07:42:37 -0800 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2021-01-12 09:42:37 -0600 |
| commit | a38a642eab886d298ea3b658c9823544c3a35f27 (patch) | |
| tree | ca0769ce5cad74fbff11e4dea6a5288a0be4ddd0 /src/smt/process_assertions.cpp | |
| parent | 8c04f1639607b34b56e3eaa8d3188b27e1454b41 (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.
Diffstat (limited to 'src/smt/process_assertions.cpp')
| -rw-r--r-- | src/smt/process_assertions.cpp | 4 |
1 files changed, 4 insertions, 0 deletions
diff --git a/src/smt/process_assertions.cpp b/src/smt/process_assertions.cpp index 5faa2a66c..0bbc2eeae 100644 --- a/src/smt/process_assertions.cpp +++ b/src/smt/process_assertions.cpp @@ -204,6 +204,10 @@ bool ProcessAssertions::apply(Assertions& as) { d_passes["bv-to-int"]->apply(&assertions); } + if (options::foreignTheoryRewrite()) + { + d_passes["foreign-theory-rewrite"]->apply(&assertions); + } // Since this pass is not robust for the information tracking necessary for // unsat cores, it's only applied if we are not doing unsat core computation |