Patmat: efficient reasoning about mutual exclusion#4431
Patmat: efficient reasoning about mutual exclusion#4431adriaanm merged 1 commit intoscala:2.11.xfrom
Conversation
Faster analysis of wide (but relatively flat) class hierarchies by using a more efficient encoding of mutual exclusion. The old CNF encoding for mutually exclusive symbols of a domain added a quadratic number of clauses to the formula to satisfy. E.g. if a domain has the symbols `a`, `b` and `c` then the clauses ``` !a \/ !b /\ !a \/ !c /\ !b \/ !c ``` were added. The first line prevents that `a` and `b` are both true at the same time, etc. 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
|
/rebuild |
There was a problem hiding this comment.
Doesn't going to flatMap change the semantics of the isDefined/nonEmpty check below?
There was a problem hiding this comment.
I think the outcome is the same if you have List(None, ...) or just List(...) after the switch to flatMap.
However, for the other case you could before have a List(Some(Nil)), which will just reduce to Nil using flatMap.
You could enter the true branch below but the final outcome should be the same, shouldn't it?
There was a problem hiding this comment.
True, thanks for explaining.
|
I'm sorry it took so long to digest this. In addition to my comments above, I think it could help my understanding to see how the change can be broken down into:
Can they be understood in isolation? |
|
The grouping is a prerequisite to be able to use the mutual exclusion logic. The approach that I have taken should be conservative though: a quadratic number of implications is still generated but if the algorithm manages to isolate the groups, these implications are removed and replaced with the mutual exclusion logic. |
|
LGTM |
Patmat: efficient reasoning about mutual exclusion
|
Hey, @gbasler, it looks like this caused a regression in unreachability checking: https://issues.scala-lang.org/browse/SI-9369 |
[Rebase of #4379]
Faster analysis of wide (but relatively flat) class hierarchies
by using a more efficient encoding of mutual exclusion.