Fix normal forms context-dependent simplification for strings (#7090)
authorAndrew Reynolds <andrew.j.reynolds@gmail.com>
Tue, 31 Aug 2021 14:07:48 +0000 (09:07 -0500)
committerGitHub <noreply@github.com>
Tue, 31 Aug 2021 14:07:48 +0000 (09:07 -0500)
commit54991eb9fa2e21c8c4705c5522ad99a9ccd9b41b
tree0794cea225c644f7334e96e9d5b0be96a31081d5
parent1954e0a0bd07ab2236c59bee2bc3da53e2018f23
Fix normal forms context-dependent simplification for strings (#7090)

This corrects an issue in our context-dependent simplification which limited the cases it was applied.

Previously, we were using a best content heuristic when it was applicable to compute the substitution, even if we were in an effort where normal forms had been computed. The latter should always be used if possible, since normal forms always have at least as much or more concrete components.
src/theory/strings/base_solver.cpp
src/theory/strings/extf_solver.cpp