diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2021-01-15 15:19:43 -0600 |
---|---|---|
committer | GitHub <noreply@github.com> | 2021-01-15 15:19:43 -0600 |
commit | de79f1ad325036ca90be9144a74606310b5dab9b (patch) | |
tree | ff025f0ccc846073327b1ad823eb9d255f4a8843 /src/CMakeLists.txt | |
parent | eb6155c5f078a26b7cdddddad6e209fad0f825f8 (diff) |
Implement --no-strings-lazy-pp as a preprocessing pass (#5777)
This option eliminates extended functions in strings eagerly. This was incorrectly done at ppRewrite previously, which should not add lemmas. Instead, this makes this technique into a preprocessing pass. To do this, the interface for the strings preprocessor was cleaned to have fewer dependencies, and made to track a cache internally.
Fixes #5608, fixes #5745, fixes #5767, fixes #5771, fixes #5406.
Diffstat (limited to 'src/CMakeLists.txt')
-rw-r--r-- | src/CMakeLists.txt | 6 |
1 files changed, 4 insertions, 2 deletions
diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt index 6f5647e9a..dd944f929 100644 --- a/src/CMakeLists.txt +++ b/src/CMakeLists.txt @@ -68,6 +68,8 @@ libcvc4_add_sources( preprocessing/passes/bv_to_int.h preprocessing/passes/extended_rewriter_pass.cpp preprocessing/passes/extended_rewriter_pass.h + preprocessing/passes/foreign_theory_rewrite.cpp + preprocessing/passes/foreign_theory_rewrite.h preprocessing/passes/fun_def_fmf.cpp preprocessing/passes/fun_def_fmf.h preprocessing/passes/global_negate.cpp @@ -102,8 +104,8 @@ libcvc4_add_sources( preprocessing/passes/sort_infer.h preprocessing/passes/static_learning.cpp preprocessing/passes/static_learning.h - preprocessing/passes/foreign_theory_rewrite.cpp - preprocessing/passes/foreign_theory_rewrite.h + preprocessing/passes/strings_eager_pp.cpp + preprocessing/passes/strings_eager_pp.h preprocessing/passes/sygus_inference.cpp preprocessing/passes/sygus_inference.h preprocessing/passes/synth_rew_rules.cpp |