Improve reachability / exhaustive checks for pattern matches for class#4379
Closed
gbasler wants to merge 1 commit intoscala:2.11.xfrom
Closed
Improve reachability / exhaustive checks for pattern matches for class#4379gbasler wants to merge 1 commit intoscala:2.11.xfrom
gbasler wants to merge 1 commit intoscala:2.11.xfrom
Conversation
Member
|
👏 |
3b6f1e1 to
eb80879
Compare
Contributor
|
Super! Very elegant. |
Member
There was a problem hiding this comment.
ops.lengthCompare(5) > 0 is a little more efficient here.
Contributor
Author
|
I've changed a few things due to the review, can squash it, when you are fine with the changes. I'll also have a quick look with the profiler and check how the extreme cases perform... |
Member
|
/rebuild |
hierarchies (relatively flat) with a lot of children. The CNF encoding for mutually exclusive symbols of a domain that was used so far, adds a quadratic number of clauses to the formula to check. E.g. if a domain has the symbols `a`, `b` and `c` then the clauses ``` !a \/ !b /\ !a \/ !c /\ !b \/ !c ``` are added. The first line prevents that `a` and `b` are both true at the same time and so on. There's a simple, more efficient encoding that can be used instead: consider a comparator circuit in hardware, that checks that out of `n` signals, at most 1 is true. Such a circuit can be built in the form of a sequential counter and thus requires only 3n-4 additional clauses [1]. A comprehensible comparison of different encodings can be found in [2]. [1]: http://www.carstensinz.de/papers/CP-2005.pdf [2]: http://www.wv.inf.tu-dresden.de/Publications/2013/report-13-04.pdf
cbc52ce to
2822f5c
Compare
Contributor
|
I think this can be merged as is, with potential performance tuning in a later PR. I dropped the ball on getting this merged in a timely fashion (in my defense, we had a pretty packed end of the quarter). Thanks again! |
Contributor
|
Rebasing this. |
This was referenced Apr 7, 2017
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
5 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.
hierarchies (relatively flat) with a lot of children.
The CNF encoding for mutually exclusive symbols of a domain that was used so
far, adds a quadratic number of clauses to the formula to check.
E.g. if a domain has the symbols
a,bandcthenthe clauses
are added.
The first line prevents that
aandbare both true at the same time and soon.
There's a simple, more efficient encoding that can be used instead: consider a
comparator circuit in hardware, that checks that out of
nsignals, at most 1is true. Such a circuit can be built in the form of a sequential counter and
thus requires only 3n-4 additional clauses 1. A comprehensible comparison of
different encodings can be found in 2.
Review by @adriaanm or @retronym