SI-7020 Determinism for pattern matcher warnings #2826
Conversation
ghost
assigned 
|
A few more runs before the patch: |
| // appearing only in either positive/negative positions | ||
| val pures = (pos ++ neg) -- impures | ||
| val pures: mutable.LinkedHashSet[Sym] = (pos ++ neg) -- impures | ||
|
|
||
| if (pures nonEmpty) { | ||
| val pureSym = pures.head |
There was a problem hiding this comment.
The LinkedHashSet affects mainly what literal is choosen here (aka branching literal). I'm wondering if there's a good heuristic on what literal to choose. Also Sat4J might have a different heuristic...
There was a problem hiding this comment.
I forgot to push the checkfile update. At least for this case, picking the first in the set gives the shortest error messages, but I don't know why that is or if it holds in general.
There was a problem hiding this comment.
Some more explanation:
If the pattern match is not exhaustive, the DPLL procedure provides a counter example. There could be more than one and it just reports the first one it finds, so depending on what direction in the search it took, the counter example will look different. And the choice of the literal determines exactly that.
I'm not sure now, if it searches for all models or just for one in this case.
Another possibility would be to always search for all models, and then sort them according to some preference.
Use LinkedHashSet for the DPLL algorithm for determistic
counter example generation.
Before, the test compiled with:
[info] v2.10.2 => /Users/jason/usr/scala-v2.10.2-0-g60d462e
test/files/neg/t7020.scala:3: warning: match may not be exhaustive.
It would fail on the following inputs: List((x: Int forSome x not in (1, 2, 4, 5, 6, 7))), List(_, _)
List(5) match {
^
test/files/neg/t7020.scala:10: warning: match may not be exhaustive.
It would fail on the following inputs: List((x: Int forSome x not in (1, 2, 4, 5, 6, 7))), List(_, _)
List(5) match {
^
test/files/neg/t7020.scala:17: warning: match may not be exhaustive.
It would fail on the following inputs: List((x: Int forSome x not in (1, 2, 4, 6, 7)), _), List(1, _), List(2, _), List(4, _), List(5, _), List(6, _), List(7, _), List(??, _)
List(5) match {
^
test/files/neg/t7020.scala:24: warning: match may not be exhaustive.
It would fail on the following input: List(_, _)
List(5) match {
^
|
With RC1 approaching we need to decide whether this is in 2.10.3 or deferred to 2.10.4 @adriaanm do you want to review? |
|
Happy to review. If this resolves the issue in the Tseitin PR, I think they both should go in. |
|
LGTM -- it's a good point that we'll need to fix this again when switching to sat4j in 2.11, though. |
SI-7020 Determinism for pattern matcher warnings
|
I should mention that there are quite a few more non-linked maps and sets in the pattern matcher. I just changed the ones that triggered this non-determinism. I suppose we don't depend on iteration order for the others, or we haven't found tests that show that yet. |
Use LinkedHashSet for the DPLL algorithm for determistic
counter example generation.
Before, the test compiled with:
Review by @adriaanm, /cc @gbasler