Fix collectEmptyEqs() in string utils#6562
Merged
ajreynol merged 2 commits intocvc5:masterfrom May 18, 2021
Merged
Conversation
Fixes cvc5#6483. The benchmark in the issue was performing the following incorrect rewrite: ``` Rewrite (str.replace "B" (str.replace (str.++ (str.replace "B" a "B") a) "B" "") "B") to (str.replace "B" a "B") by RPL_X_Y_X_SIMP. ``` The rewrite `RPL_X_Y_X_SIMP` rewrites terms of the form `(str.replace x y x)`, where `x` is of length one and `(= y "")` rewrites to a conjunction of equalities of the form `(= y_i "")` where `y_i` is some term. The function responsible for collecting the terms `y_i` from this conjunction, `collectEmptyEqs()`, returns a `bool` and a vector of `Node`s. The `bool` indicates whether all equalities in the conjunction were of the form `(= y_i "")`. The rewrite `RPL_X_Y_X_SIMP` only applies if this is true. However, `collectEmptyEqs()` had a bug where it would not return false when all of the conjuncts were equalities but not all of them were equalities with the empty string. This commit fixes `collectEmptyEqs()` and adds tests.
Member
|
Does this PR also fix #6101 ? |
Member
Author
Unfortunately, it does not look like it. The rewrite fixed in this PR does not apply very often. |
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
2 participants
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Fixes #6483. The benchmark in the issue was performing the following
incorrect rewrite:
The rewrite
RPL_X_Y_X_SIMPrewrites terms of the form(str.replace x y x), wherexis of length one and(= y "")rewrites to aconjunction of equalities of the form
(= y_i "")wherey_iis someterm. The function responsible for collecting the terms
y_ifrom thisconjunction,
collectEmptyEqs(), returns abooland a vector ofNodes. Theboolindicates whether all equalities in the conjunctionwere of the form
(= y_i ""). The rewriteRPL_X_Y_X_SIMPonly appliesif this is true. However,
collectEmptyEqs()had a bug where it wouldnot return false when all of the conjuncts were equalities but not all
of them were equalities with the empty string. This commit fixes
collectEmptyEqs()and adds tests.