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.

If the search for exhaustivity stops at the max recursion depth, all bets are off since we might not find all possible counter examples. Thus I added a switch `-Ypatmat-exhaust-depth <n> | <off>` that lets the user set the max recursion depth. This is necessary in order to keep the regression tests stable.

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
```
Yes that's easy to construct: just create a symbol with a large domain. So the number of subtype checks is quadratic in the number of symbols in the domain. 

I added now a fast path in case a symbol has no children and avoid the subtype check in that case.

I needed the subtype check to be able to report one (redundant) case for `patmatexhaust.scala`. See also the comments in the code. Maybe it can just be omitted (or omitted if the domain is larger than a specific number)? 

In the end I need this list to add more constraints to the CNF formula that is checked. So the number of clauses is quadratic in the number of symbols as well. I don't think this can be avoided.
However, such a test case would - with the current implementation - most likely run into a `CNF budget exceeded` error anyway.