SI-8999 Fix out of memory error in exhaustivity check in pattern matcher.

[gbasler]

The OOM could occur when all models are forcibly expanded in the DPLL solver.

The simplest solution would be to limit the number of returned models but then
we are back in non-determinism land (since the subset we get back depends on
which models were found first).

A better alternative is to create only the models that have corresponding
counter examples.

If this does not ring a bell, here's a longer explanation:

TThe models we get from the DPLL solver need to be mapped back to counter
examples. However there's no precalculated mapping model -> counter example.
Even worse, not every valid model corresponds to a valid counter example.

The reason is that restricting the valid models further would for example
require a quadratic number of additional clauses. So to keep the optimistic case
fast (i.e., all cases are covered in a pattern match), the infeasible counter
examples are filtered later.

The DPLL procedure keeps the literals that do not contribute to the solution
unassigned, e.g., for (a \/ b) only {a = true} or {b = true} is required and
the other variable can have any value. This function does a smart expansion of
the model and avoids models that have conflicting mappings.

For example for in case of the given set of symbols (taken from t7020.scala):
"V2=2#16"
"V2=6#19"
"V2=5#18"
"V2=4#17"
"V2=7#20"
One possibility would be to group the symbols by domain but
this would only work for equality tests and would not be compatible
with type tests.
Another observation leads to a much simpler algorithm:
Only one of these symbols can be set to true,
since V2 can at most be equal to one of {2,6,5,4,7}.
I tried to come up with an example where this approach fails, so far it always
worked out...

Review by @adriaanm

[adriaanm]

(Was pre-reviewed before it became a PR)

LGTM -- I'm running out of superlatives, @gbasler!

I tried it on the trickiest example I could think of:

➜  scala git:(gbasler-ticket/SI-8999) qs               
Welcome to Scala version 2.11.5-20141208-090512-7282f420e9 (Java HotSpot(TM) 64-Bit Server VM, Java 1.8.0_25).
Type in expressions to have them evaluated.
Type :help for more information.

scala> def xs: List[Any] = Nil
xs: List[Any]

scala> xs match { case (_: Any) :: Nil => case (_: Boolean) :: Nil =>  case true :: _ => } 
<console>:9: warning: unreachable code
              xs match { case (_: Any) :: Nil => case (_: Boolean) :: Nil =>  case true :: _ => }
                                                                          ^
<console>:9: warning: match may not be exhaustive.
It would fail on the following inputs: List((_ : Boolean), _), List((x: Any forSome x not in (Boolean, true)), _), Nil
              xs match { case (_: Any) :: Nil => case (_: Boolean) :: Nil =>  case true :: _ => }
              ^
scala.MatchError: List() (of class scala.collection.immutable.Nil$)
  ... 33 elided

scala> :quit

➜  scala git:(gbasler-ticket/SI-8999) scala            
Welcome to Scala version 2.11.4 (Java HotSpot(TM) 64-Bit Server VM, Java 1.8.0_25).
Type in expressions to have them evaluated.
Type :help for more information.

scala> def xs: List[Any] = Nil
xs: List[Any]

scala> xs match { case (_: Any) :: Nil => case (_: Boolean) :: Nil =>  case true :: _ => } 
<console>:9: warning: unreachable code
              xs match { case (_: Any) :: Nil => case (_: Boolean) :: Nil =>  case true :: _ => }
                                                                          ^
<console>:9: warning: match may not be exhaustive.
It would fail on the following inputs: List((_ : Boolean), _), List((x: Any forSome x not in (Boolean, true)), _), Nil
              xs match { case (_: Any) :: Nil => case (_: Boolean) :: Nil =>  case true :: _ => }
              ^
scala.MatchError: List() (of class scala.collection.immutable.Nil$)
  ... 33 elided

[adriaanm]

My remaining concern from the pre-review was that variable assignments aren't always mutually exclusive, when type tests and value tests are mixed.

[adriaanm]

My example shows we need to improve our reporting a bit, but the PR does not negatively affect this case.

[adriaanm]

I'll rebase on the other PR.

[som-snytt]

From now on, I'll say, Pre-review by @adriaanm