diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2021-08-05 10:21:48 -0500 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2021-08-05 10:21:48 -0500 |
| commit | 48a1854491c99d61d21482115e18399195d4d365 (patch) | |
| tree | 47b933d38ac7577dba75dee11d19925bec6a50f8 /src/theory/strings/theory_strings.cpp | |
| parent | 183808b608071890b4d8a05d51233fe37a133873 (diff) | |
Fix policy for rewriting string equalities (#6916)
This PR simplifies our rewriter for string equalities. We do not try to rewrite equalities to true/false by default.
This prevents cases where lemmas may contain vacuous premises that rewrite to false, hence making a lemma rewrite to true.
This PR reorganizes the interplay between the rewrite and the post-processing of rewrites via extended equality rewriting.
Fixes #6913. Also adds benchmarks from #6101 which appear related but were fixed in previous commits, thus fixes #6101 as well.
Diffstat (limited to 'src/theory/strings/theory_strings.cpp')
| -rw-r--r-- | src/theory/strings/theory_strings.cpp | 9 |
1 files changed, 9 insertions, 0 deletions
diff --git a/src/theory/strings/theory_strings.cpp b/src/theory/strings/theory_strings.cpp index 8912bad3b..c526decf1 100644 --- a/src/theory/strings/theory_strings.cpp +++ b/src/theory/strings/theory_strings.cpp @@ -993,6 +993,15 @@ void TheoryStrings::checkRegisterTermsNormalForms() TrustNode TheoryStrings::ppRewrite(TNode atom, std::vector<SkolemLemma>& lems) { Trace("strings-ppr") << "TheoryStrings::ppRewrite " << atom << std::endl; + if (atom.getKind() == EQUAL) + { + // always apply aggressive equality rewrites here + Node ret = d_rewriter.rewriteEqualityExt(atom); + if (ret != atom) + { + return TrustNode::mkTrustRewrite(atom, ret, nullptr); + } + } if (atom.getKind() == STRING_FROM_CODE) { // str.from_code(t) ---> |