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/theory/strings/extf_solver.cpp | |
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/theory/strings/extf_solver.cpp')
-rw-r--r-- | src/theory/strings/extf_solver.cpp | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/src/theory/strings/extf_solver.cpp b/src/theory/strings/extf_solver.cpp index 7e416d132..352da5ac8 100644 --- a/src/theory/strings/extf_solver.cpp +++ b/src/theory/strings/extf_solver.cpp @@ -43,7 +43,7 @@ ExtfSolver::ExtfSolver(SolverState& s, d_csolver(cs), d_extt(et), d_statistics(statistics), - d_preproc(d_termReg.getSkolemCache(), s.getUserContext(), statistics), + d_preproc(d_termReg.getSkolemCache(), &statistics.d_reductions), d_hasExtf(s.getSatContext(), false), d_extfInferCache(s.getSatContext()), d_reduced(s.getUserContext()) |