Simplify n-ary and/or with duplicate operands like and(x, y, x) #161
Conversation
This file contains 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
SMTInterpol already does this, now we do it for all other solvers as well. This basically re-adds 36e47b5 (which was only for Z3), but in a more memory-efficient way (Stream.distinct() typically uses a regular HashSet, the old commit used a LinkedHashSet). The performance and memory consumption are O(n) (amortized). Cf. #73
|
As we never communicate towards the user, that formulae are structured as how they are build, I do not see a problem with merging this PR. There are more solvers (coming sooner or later) that do not support automatic simplification on that level. |
|
Yes, from a functional point of view there is no problem, there is just the overhead that was the cause for rejection in the past. Not sure how many users actually do filter duplicates themselves, and everything except duplicates is also filtered out without this commit. |
|
Ping? How about deciding on this one? |
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
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.
SMTInterpol already does this, now we do it for all other solvers as well.
This basically re-adds 36e47b5 (which was only for Z3), but in a more memory-efficient way (
Stream.distinct()typically uses a regularHashSet, the old commit used aLinkedHashSet).The performance and memory consumption are O(n) (amortized), just like the existing code. The overhead is basically one additional
HashSet.In the discussion of 36e47b5 it was decided to not do this, and I am also not really convinced this is worth it (we now consistently do simplifications of
trueandfalseoperands including short-circuiting, this PR would only filter out duplicate operands, which are probably rare).But given the new implementation and that this is the first time we have an implementation that would make the behavior across all solvers consistent, I would like to put this up for discussion. At the least we will have this PR as permanent record of this potential solution.
Cf. #73