diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2021-02-10 09:11:02 -0600 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2021-02-10 09:11:02 -0600 |
| commit | e9408ca21267616bb799ef5f7fda85a1fee9c07c (patch) | |
| tree | c1abfe14a791ed162e91e31e595a19d818294079 /src/theory/strings/word.cpp | |
| parent | 261886a6ddc7fb93afcb7492a7e22884d6f75c96 (diff) | |
Simplify method for inferring proxy lemmas in strings (#5789)
This PR simplifies our heuristic for inferring when an explanation for a strings lemma can be minimized based on proxy variable definitions. In particular, we do not turn solved equalities for proxy variables into substitutions. This aspect of the heuristic is incompatible with the new eager solver work, and moreover is buggy since substitutions should not be applied within string terms. The latter was leading the incorrect models on the 2 issues fixed by this PR.
Current results on the eager solver on SMT-LIB shows this change has very little performance impact.
Fixes #5692, fixes #5610.
Diffstat (limited to 'src/theory/strings/word.cpp')
0 files changed, 0 insertions, 0 deletions