scala/scala — pull request #3954 by gbasler (2014-09-01 05:16:25+00:00)
Title: SI-7746 fix unspecifc non-exhaustiveness warnings and non-determinism in pattern matcher (2.11)

This pull request should resolve all remaining non-determinisms regarding exhaustiveness warnings in the pattern matcher. It was buried deep in the machinery and thus not easy to find. The non-determinism is also the reason behind SI-7746.

Review by @adriaanm or @retronym

1) The implementation of the DPLL algorithm was flawed and did not return all solutions. Depending on the ordering of the symbols, more or less solutions were found.
You can find a test project that compares the results of the implementation with Sat4j here:
https://github.com/gbasler/dpll
2) The formulas that were passed to the solver resulted in counter examples that were invalid and removed in a following filtering step. That led to the weird situation where the fixed algorithm returned less counter examples than the buggy one. The recursion goes now deeper than before and also this led to less counter examples reported, since it was stopped too early before.
3) I also cleaned up the `LinkedHashSet` workarounds. They should not be needed anymore. I've repeated Jason's checks (see below) and could not find any problems.

I'm working on another PR that will get rid of the "analysis budget" error but this one is a prerequisite to make it work.

Check 1:

```
~/Documents/scala-fix-nondet-patmat:ticket/7746$ (f=test/files/neg/t8430.scala; (for i in {1..20}; do echo $f; done; printf "\n") | qbin/scalac -Xresident) 2>&1 | grep "fail" | sort | uniq | wc -l
1
```
Check 2:

```
for i in {1..100}; do cp test/files/neg/t7020.scala test/files/neg/t7020-$i.scala; cp test/files/neg/t7020.flags test/files/neg/t7020-$i.flags; cat test/files/neg/t7020.check | sed "s/t7020/t7020-$i/" > test/files/neg/t7020-$i.check; done

~/Documents/scala-fix-nondet-patmat:ticket/7746$ test/partest --terse --srcpath disabled test/files/neg/t7020*.scala

Selected 101 tests drawn from specified tests

# starting 101 tests in neg

........................................................................

.............................

101/101 passed (elapsed time: 00:00:32)

Test Run PASSED
```