Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Simplify n-ary and/or with duplicate operands like and(x, y, x) #161

Open
wants to merge 1 commit into
base: master
Choose a base branch
from

Conversation

PhilippWendler
Copy link
Member

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), 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 true and false operands 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

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
@kfriedberger
Copy link
Member

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.
Additionally, this might even replace and simplify user code that does the same filtering on its own.

@PhilippWendler
Copy link
Member Author

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.

@PhilippWendler
Copy link
Member Author

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
Development

Successfully merging this pull request may close these issues.

2 participants