Unreachability analysis for pattern matches

Analyze matches for unreachable cases.

A case is unreachable if it implies its preceding cases.
Call `C` the formula that is satisfiable if the considered case matches.
Call `P` the formula that is satisfiable if the cases preceding it match.
The case is reachable if there is a model for `-P /\ C`.
Thus, the case is unreachable if there is no model for `-(-P /\ C)`,
or, equivalently, `P \/ -C`, or `C => P`.

Unreachability needs a more precise model for type and value tests than exhaustivity.
Before, `{case _: Int => case 1 =>}` would be modeled as `X = Int \/ X = 1.type`,
and thus, the second case would be reachable if we can satisfy `X != Int /\ X = 1.type`.
Of course, the case isn't reachable, yet the formula is satisfiable, so we must augment
our model to take into account that `X = 1.type => X = Int`.

This is done by `removeVarEq`, which models the following axioms about equality.
It does so to retain the meaning of equality after replacing `V = C` (variable = constant)
by a literal (fresh symbol). For each variable:
 1. a sealed type test must result in exactly one of its partitions being chosen
    (the core of exhaustivity)
 2. when a type test is true, tests of super types must also be true,
    and unrelated type tests must be false

For example, `V : X ::= A | B | C`, and `A => B` (since `A extends B`).
Coverage (1) is formulated as: `A \/ B \/ C`, and the implications of (2) are simply
`V=A => V=B /\ V=X`, `V=B => V=X`, `V=C => V=X`.

Exclusion for unrelated types typically results from matches such as `{case SomeConst =>
case OtherConst => }`. Here, `V=SomeConst.type => !V=OtherConst.type`. This is a
conservative approximation. If these constants happen to be the same value dynamically
(but the types don't tell us this), the last case is actually unreachable. Of course we
must err on the safe side.

We simplify the equality axioms as follows (in principle this could be done by the
solver, but it's easy to do before solving). If we've already excluded a pair of
assignments of constants to a certain variable at some point, say `(-A \/ -B)`, then
don't exclude the symmetric one `(-B \/ -A)`. (Nor the positive implications `-B \/ A`,
or `-A \/ B`, which would entail the equality axioms falsifying the whole formula.)

TODO: We should also model dependencies between variables: if `V1` corresponds to
`x: List[_]` and `V2` is `x.hd`, `V2` cannot be assigned at all when `V1 = null` or
`V1 = Nil`. Right now this is implemented hackily by pruning counter-examples in exhaustivity.
Unreachability would also benefit from a more faithful representation.

I had to refactor some of the framework, but most of it is shared with exhaustivity. We
must allow approximating tree makers twice, sharing variables, but using different
approximations for values not statically known. When considering reachability of a case,
we must assume, for example, that its unknown guard succeeds (otherwise it would wrongly
be considered unreachable), whereas unknown guards in the preceding cases must be
considered to fail (otherwise we could never get to those case, and again, it would
falsely be considered unreachable).

Since this analysis is relatively expensive, you may opt-out using `-Xno-patmat-analysis`
(or annotating the selector with @unchecked). We hope to improve the performance in the
near future. -Ystatistics has also been extended to provide some numbers on time spent in
the equality-rewrite, solving and analyzing.

2 files changed, 732 insertions, 248 deletions

diff --git a/src/compiler/scala/tools/nsc/typechecker/PatternMatching.scala b/src/compiler/scala/tools/nsc/typechecker/PatternMatching.scala
index 830e7db8ca..21b80df735 100644
--- a/src/compiler/scala/tools/nsc/typechecker/PatternMatching.scala
+++ b/src/compiler/scala/tools/nsc/typechecker/PatternMatching.scala
@@ -14,6 +14,7 @@ import scala.tools.nsc.transform.TypingTransformers
 import scala.tools.nsc.transform.Transform
 import scala.collection.mutable.HashSet
 import scala.collection.mutable.HashMap
+import scala.tools.nsc.util.Statistics
 
 /** Translate pattern matching.
   *
@@ -38,6 +39,8 @@ import scala.collection.mutable.HashMap
   *  - recover exhaustivity and unreachability checking using a variation on the type-safe builder pattern
   */
 trait PatternMatching extends Transform with TypingTransformers with ast.TreeDSL {   // self: Analyzer =>
+  import Statistics._
+
   val global: Global               // need to repeat here because otherwise last mixin defines global as
                                    // SymbolTable. If we had DOT this would not be an issue
   import global._                  // the global environment
@@ -182,6 +185,8 @@ trait PatternMatching extends Transform with TypingTransformers with ast.TreeDSL
         case _                                          => tp
       }
 
+      val start = startTimer(patmatNanos)
+
       val selectorTp = repeatedToSeq(elimAnonymousClass(selector.tpe.widen.withoutAnnotations))
 
       val origPt  = match_.tpe
@@ -205,7 +210,10 @@ trait PatternMatching extends Transform with TypingTransformers with ast.TreeDSL
 
       val selectorSym  = freshSym(selector.pos, pureType(selectorTp)) setFlag SYNTH_CASE
       // pt = Any* occurs when compiling test/files/pos/annotDepMethType.scala  with -Xexperimental
-      combineCases(selector, selectorSym, cases map translateCase(selectorSym, pt), pt, matchOwner, matchFailGenOverride)
+      val combined = combineCases(selector, selectorSym, cases map translateCase(selectorSym, pt), pt, matchOwner, matchFailGenOverride)
+
+      stopTimer(patmatNanos, start)
+      combined
     }
 
     // return list of typed CaseDefs that are supported by the backend (typed/bind/wildcard)
@@ -1328,11 +1336,11 @@ trait PatternMatching extends Transform with TypingTransformers with ast.TreeDSL
       // def andThen_: (prev: List[Test]): List[Test] =
       //   prev.filterNot(this <:< _) :+ this
 
-      private val reusedBy = new collection.mutable.HashSet[Test]
+      // private val reusedBy = new collection.mutable.HashSet[Test]
       var reuses: Option[Test] = None
       def registerReuseBy(later: Test): Unit = {
         assert(later.reuses.isEmpty, later.reuses)
-        reusedBy += later
+        // reusedBy += later
         later.reuses = Some(this)
       }
 
@@ -1427,9 +1435,16 @@ trait PatternMatching extends Transform with TypingTransformers with ast.TreeDSL
 
 
     // returns (tree, tests), where `tree` will be used to refer to `root` in `tests`
-    abstract class TreeMakersToConds(val root: Symbol, val cases: List[List[TreeMaker]]) {
+    abstract class TreeMakersToConds(val root: Symbol) {
+      def discard() = {
+        pointsToBound.clear()
+        trees.clear()
+        normalize  = EmptySubstitution
+        accumSubst = EmptySubstitution
+      }
       // a variable in this set should never be replaced by a tree that "does not consist of a selection on a variable in this set" (intuitively)
-      private val pointsToBound            = collection.mutable.HashSet(root)
+      private val pointsToBound = collection.mutable.HashSet(root)
+      private val trees         = collection.mutable.HashSet.empty[Tree]
 
       // the substitution that renames variables to variables in pointsToBound
       private var normalize: Substitution  = EmptySubstitution
@@ -1462,7 +1477,6 @@ trait PatternMatching extends Transform with TypingTransformers with ast.TreeDSL
         // patmatDebug("accumSubst: "+ accumSubst)
       }
 
-      private val trees = new collection.mutable.HashSet[Tree]
 
       // TODO: improve, e.g., for constants
       def sameValue(a: Tree, b: Tree): Boolean = (a eq b) || ((a, b) match {
@@ -1533,14 +1547,14 @@ trait PatternMatching extends Transform with TypingTransformers with ast.TreeDSL
         }
       }
 
-      final def approximateMatch(condMaker: CondMaker = makeCond): List[List[Test]] = cases.map { _ map (tm => Test(treeMakerToCond(tm, condMaker), tm)) }
+      final def approximateMatch(cases: List[List[TreeMaker]], condMaker: CondMaker = makeCond): List[List[Test]] = cases.map { _ map (tm => Test(treeMakerToCond(tm, condMaker), tm)) }
 
-      final def approximateMatchAgain(condMaker: CondMaker = makeCond): List[List[Test]] = cases.map { _ map (tm => Test(treeMakerToCondNoSubst(tm, condMaker), tm)) }
+      final def approximateMatchAgain(cases: List[List[TreeMaker]], condMaker: CondMaker = makeCond): List[List[Test]] = cases.map { _ map (tm => Test(treeMakerToCondNoSubst(tm, condMaker), tm)) }
     }
 
     def approximateMatch(root: Symbol, cases: List[List[TreeMaker]]): List[List[Test]] = {
-      object approximator extends TreeMakersToConds(root, cases)
-      approximator.approximateMatch()
+      object approximator extends TreeMakersToConds(root)
+      approximator.approximateMatch(cases)
     }
 
     def showTreeMakers(cases: List[List[TreeMaker]]) = {
@@ -1585,18 +1599,36 @@ trait PatternMatching extends Transform with TypingTransformers with ast.TreeDSL
     class Prop
     case class Eq(p: Var, q: Const) extends Prop
 
-    type Const
+    type Const <: AbsConst
+
+    trait AbsConst {
+      def implies(other: Const): Boolean
+      def excludes(other: Const): Boolean
+    }
+
     type Var <: AbsVar
 
     trait AbsVar {
-      // if the domain is enumerable, at least one assignment must be true
-      def domainEnumerable: Boolean
-      def domain: Option[Set[Const]]
+      // indicate we may later require a prop for V = C
+      def registerEquality(c: Const): Unit
+
+      // indicates null is part of the domain
+      def considerNull: Unit
+
+      // compute the domain and return it (call considerNull first!)
+      def domainSyms: Option[Set[Sym]]
 
       // for this var, call it V, turn V = C into the equivalent proposition in boolean logic
+      // registerEquality(c) must have been called prior to this call
+      // in fact, all equalities relevant to this variable must have been registered
       def propForEqualsTo(c: Const): Prop
 
-      def equalitySyms: Set[Sym]
+//      // describe the equality axioms related to this variable being equal to this constant
+//      def impliedProp(c: Const): Prop
+
+      // populated by registerEquality
+      // once equalitySyms has been called, registerEquality has no effect
+      def equalitySyms: List[Sym]
     }
 
     // would be nice to statically check whether a prop is equational or pure,
@@ -1608,12 +1640,17 @@ trait PatternMatching extends Transform with TypingTransformers with ast.TreeDSL
     case object True extends Prop
     case object False extends Prop
 
-    private def nextSymId = {_symId += 1; _symId}; private var _symId = 0
-
     // symbols are propositions
     case class Sym(val variable: Var, val const: Const) extends Prop {
-      override val toString = variable +"="+ const +"#"+ nextSymId
+      private[this] val id = nextSymId
+      override def toString = variable +"="+ const +"#"+ id
     }
+    private def nextSymId = {_symId += 1; _symId}; private var _symId = 0
+
+
+    @inline def /\(props: Iterable[Prop]) = if (props.isEmpty) True else props.reduceLeft(And(_, _))
+    @inline def \/(props: Iterable[Prop]) = if (props.isEmpty) False else props.reduceLeft(Or(_, _))
+
 
     trait PropTraverser {
       def apply(x: Prop): Unit = x match {
@@ -1627,6 +1664,14 @@ trait PatternMatching extends Transform with TypingTransformers with ast.TreeDSL
       def applyConst(x: Const): Unit = {}
     }
 
+    def gatherVariables(p: Prop): Set[Var] = {
+      val vars = new HashSet[Var]()
+      (new PropTraverser {
+        override def applyVar(v: Var) = vars += v
+      })(p)
+      vars.toSet
+    }
+
     trait PropMap {
       def apply(x: Prop): Prop = x match { // TODO: mapConserve
         case And(a, b) => And(apply(a), apply(b))
@@ -1636,278 +1681,687 @@ trait PatternMatching extends Transform with TypingTransformers with ast.TreeDSL
       }
     }
 
-    // plan: (aka TODO)
-
     // convert finite domain propositional logic to boolean propositional logic
     // for all c in C, there is a corresponding (meta-indexed) proposition Qv(c) that represents V = c,
     // the only property of equality that is encoded is that a variable can at most be equal to one of the c in C:
     // thus, for each distinct c, c', c'',... in C, a clause `not (Qv(c) /\ (Qv(c') \/ ... \/ Qv(c'')))` is added
-    def removeVarEq(prop: Prop): Prop = {
+    def removeVarEq(props: List[Prop], considerNull: Boolean = false): (Prop, List[Prop]) = {
+      val start = startTimer(patmatAnaVarEq)
+
       val vars = new collection.mutable.HashSet[Var]
 
-      object dropEquational extends PropMap {
+      object gatherEqualities extends PropTraverser {
         override def apply(p: Prop) = p match {
-          case Eq(v, c) => vars += v; v.propForEqualsTo(c)
+          case Eq(v, c) =>
+            vars += v
+            v.registerEquality(c)
           case _ => super.apply(p)
         }
       }
 
-      // dropEquational populates vars, and for each var in vars. var.equalitySyms
-      val pure = dropEquational(prop)
+      object rewriteEqualsToProp extends PropMap {
+        override def apply(p: Prop) = p match {
+          case Eq(v, c) => v.propForEqualsTo(c)
+          case _ => super.apply(p)
+        }
+      }
+
+      props foreach gatherEqualities.apply
+      if (considerNull) vars foreach (_.considerNull)
 
-      // X = C is translated to P_X=C
-      // X = C' is translated to P_X=C'
-      // need to enforce X cannot simultaneously equal C and C'
-      // thus, all equality syms are mutually exclusive
-      // X = A, B, C, D --> Not(And(A, B)) /\ Not(And(A, C)) /\ Not(And(A, D))
-      //                 /\ Not(And(B, C)) /\ Not(And(B, D))
-      //                 /\ Not(And(C, D))
-      // equivalently Or(Not(A), Not(B)) /\ Or(...)
+      val pure = props map rewriteEqualsToProp.apply
 
       var eqAxioms: Prop = True
-      def mutex(a: Sym)(b: Sym) =
-        eqAxioms = And(eqAxioms, Or(Not(a), Not(b)))
+      @inline def addAxiom(p: Prop) = eqAxioms = And(eqAxioms, p)
 
-      // at least one assignment from the domain must be true
-      def assigned(dom: Set[Sym]) =
-        eqAxioms = And(eqAxioms, dom.reduceLeft(Or))
+      case class ExcludedPair(a: Const, b: Const) {
+        override def equals(o: Any) = o match {
+          case ExcludedPair(aa, bb) => (a == aa && b == bb) || (a == bb && b == aa)
+          case _ => false
+        }
+      }
 
       // patmatDebug("vars: "+ vars)
       vars.foreach { v =>
-        // is the domain enumerable? then create equality syms for all elements in the domain and
-        // assert at least one of them must be selected
-        // if v.domain.isEmpty, we must consider the domain to be infinite
-        v.domain foreach { dom =>
-          // get the Syms for the constants in the domain (making fresh ones for those not encountered in the formula)
-          val domProps = dom map {c => v.propForEqualsTo(c)}
-          val domSyms  = new collection.mutable.HashSet[Sym]()
-          object collectSyms extends PropTraverser {
-            override def apply(p: Prop) = p match {
-              case domSym: Sym => domSyms += domSym
-              case _ => super.apply(p)
-            }
+        val excludedPair = new collection.mutable.HashSet[ExcludedPair]
+
+        // if v.domainSyms.isEmpty, we must consider the domain to be infinite
+        // otherwise, since the domain fully partitions the type of the value,
+        // exactly one of the types (and whatever it implies, imposed separately) must be chosen
+        // consider X ::= A | B | C, and A => B
+        // coverage is formulated as: A \/ B \/ C and the implications are
+        v.domainSyms foreach { dsyms => addAxiom(\/(dsyms)) }
+
+        val syms = v.equalitySyms
+        // patmatDebug("eqSyms "+(v, syms))
+        syms foreach { sym =>
+          // don't relate V = C to V = C -- `b.const == sym.const`
+          // if we've already excluded the pair at some point (-A \/ -B), then don't exclude the symmetric one (-B \/ -A)
+          // (nor the positive implications -B \/ A, or -A \/ B, which would entail the equality axioms falsifying the whole formula)
+          val todo = syms filterNot (b => (b.const == sym.const) || excludedPair(ExcludedPair(b.const, sym.const)))
+          val (excluded, notExcluded) = todo partition (b => sym.const.excludes(b.const))
+          val implied = notExcluded filter (b => sym.const.implies(b.const))
+          // patmatDebug("implications: "+ (sym.const, excluded, implied, syms))
+
+          // when this symbol is true, what must hold...
+          implied  foreach (impliedSym => addAxiom(Or(Not(sym), impliedSym)))
+
+          // ... and what must not?
+          excluded foreach {excludedSym =>
+            excludedPair += ExcludedPair(sym.const, excludedSym.const)
+            addAxiom(Or(Not(sym), Not(excludedSym)))
           }
-          domProps foreach collectSyms.apply
-
-          // TODO: an empty domain means involved type tests can never be true --> always non-exhaustive?
-          if (domSyms.nonEmpty) assigned(domSyms.toSet)
-        }
-
-        // recover mutual-exclusivity (a variable can never be assigned two different constants)
-        var syms = v.equalitySyms.toList
-        while (syms.nonEmpty) {
-          syms.tail.foreach(mutex(syms.head))
-          syms = syms.tail
         }
       }
 
-      // patmatDebug("eqAxioms:\n"+ cnfString(conjunctiveNormalForm(negationNormalForm(eqAxioms))))
-      // patmatDebug("pure:\n"+ cnfString(conjunctiveNormalForm(negationNormalForm(pure))))
+      // patmatDebug("eqAxioms:\n"+ cnfString(eqFreePropToSolvable(eqAxioms)))
+      // patmatDebug("pure:\n"+ cnfString(eqFreePropToSolvable(pure)))
+
+      stopTimer(patmatAnaVarEq, start)
 
-      And(eqAxioms, pure)
+      (eqAxioms, pure)
     }
 
-    // convert propositional logic formula to CNF
-    // http://www.dcs.warwick.ac.uk/people/academic/Ranko.Lazic/fsv/fsv6.pdf
-    def negationNormalForm(p: Prop): Prop = p match {
-      case And(a, b)      => And(negationNormalForm(a), negationNormalForm(b))
-      case Or(a, b)       => Or(negationNormalForm(a), negationNormalForm(b))
-      case Not(And(a, b)) => negationNormalForm(Or(Not(a), Not(b)))
-      case Not(Or(a, b))  => negationNormalForm(And(Not(a), Not(b)))
-      case Not(Not(p))    => negationNormalForm(p)
-      case Not(True)      => False
-      case Not(False)     => True
-      case True
-         | False
-         | (_ : Sym)
-         | Not(_ : Sym)   => p
+
+    type Formula
+    def andFormula(a: Formula, b: Formula): Formula
+
+    // may throw an IllegalArgumentException
+    def propToSolvable(p: Prop) = {
+      val (eqAxioms, pure :: Nil) = removeVarEq(List(p), considerNull = false)
+      eqFreePropToSolvable(And(eqAxioms, pure))
     }
 
+    def eqFreePropToSolvable(p: Prop): Formula
+    def cnfString(f: Formula): String
+
+    type Model = Map[Sym, Boolean]
+    val EmptyModel: Model
+    val NoModel: Model
+
+    def findModelFor(f: Formula): Model
+    def findAllModelsFor(f: Formula): List[Model]
+  }
+
+  trait CNF extends Logic {
     // CNF: a formula is a conjunction of clauses
-    type Formula = List[Clause] ; def formula(c: Clause*): Formula = c.toList
+    type Formula = Array[Clause]
+    def formula(c: Clause*): Formula = c.toArray
+    def andFormula(a: Formula, b: Formula): Formula = a ++ b
 
     // a clause is a disjunction of distinct literals
-    type Clause  = Set[Lit]     ; def clause(l: Lit*): Clause = l.toSet
+    type Clause = Set[Lit]
+    def clause(l: Lit*): Clause = l.toSet
+    @inline private def merge(a: Clause, b: Clause) = a ++ b
+
+    type Lit
+    def Lit(sym: Sym, pos: Boolean = true): Lit
+
+    // throws an IllegalArgumentException when the prop results in a CNF that's too big
+    def eqFreePropToSolvable(p: Prop): Formula = {
+      // TODO: for now, reusing the normalization from DPLL
+      def negationNormalForm(p: Prop): Prop = p match {
+        case And(a, b)      => And(negationNormalForm(a), negationNormalForm(b))
+        case Or(a, b)       => Or(negationNormalForm(a), negationNormalForm(b))
+        case Not(And(a, b)) => negationNormalForm(Or(Not(a), Not(b)))
+        case Not(Or(a, b))  => negationNormalForm(And(Not(a), Not(b)))
+        case Not(Not(p))    => negationNormalForm(p)
+        case Not(True)      => False
+        case Not(False)     => True
+        case True
+           | False
+           | (_ : Sym)
+           | Not(_ : Sym)   => p
+      }
+
+      val TrueF          = formula()
+      val FalseF         = formula(clause())
+      def lit(s: Sym)    = formula(clause(Lit(s)))
+      def negLit(s: Sym) = formula(clause(Lit(s, false)))
+
+      def conjunctiveNormalForm(p: Prop, budget: Int = 256): Formula = {
+        def distribute(a: Formula, b: Formula, budget: Int): Formula =
+          if (budget <= 0) throw new IllegalArgumentException("CNF budget exceeded")
+          else
+            (a, b) match {
+              // true \/ _ = true
+              // _ \/ true = true
+              case (trueA, trueB) if trueA.size == 0 || trueB.size == 0 => TrueF
+              // lit \/ lit
+              case (a, b) if a.size == 1 && b.size == 1 => formula(merge(a(0), b(0)))
+              // (c1 /\ ... /\ cn) \/ d = ((c1 \/ d) /\ ... /\ (cn \/ d))
+              // d \/ (c1 /\ ... /\ cn) = ((d \/ c1) /\ ... /\ (d \/ cn))
+              case (cs, ds) =>
+                val (big, small) = if (cs.size > ds.size) (cs, ds) else (ds, cs)
+                big flatMap (c => distribute(formula(c), small, budget - (big.size*small.size)))
+            }
 
-    // a literal is a (possibly negated) variable
-    case class Lit(sym: Sym, pos: Boolean = true) {
-      override def toString = if (!pos) "-"+ sym.toString else sym.toString
-      def unary_- = Lit(sym, !pos)
+        if (budget <= 0) throw new IllegalArgumentException("CNF budget exceeded")
+
+        p match {
+          case True        => TrueF
+          case False       => FalseF
+          case s: Sym      => lit(s)
+          case Not(s: Sym) => negLit(s)
+          case And(a, b)   =>
+            val cnfA = conjunctiveNormalForm(a, budget - 1)
+            val cnfB = conjunctiveNormalForm(b, budget - cnfA.size)
+            cnfA ++ cnfB
+          case Or(a, b)    =>
+            val cnfA = conjunctiveNormalForm(a)
+            val cnfB = conjunctiveNormalForm(b)
+            distribute(cnfA, cnfB, budget - (cnfA.size + cnfB.size))
+        }
+      }
+
+      val start = startTimer(patmatCNF)
+      val res = conjunctiveNormalForm(negationNormalForm(p))
+      stopTimer(patmatCNF, start)
+      patmatCNFSizes(res.size) += 1
+
+//      patmatDebug("cnf for\n"+ p +"\nis:\n"+cnfString(res))
+      res
     }
 
-    val TrueF          = formula()
-    val FalseF         = formula(clause())
-    def lit(s: Sym)    = formula(clause(Lit(s)))
-    def negLit(s: Sym) = formula(clause(Lit(s, false)))
+  }
 
-    def conjunctiveNormalForm(p: Prop): Formula = {
-      def distribute(a: Formula, b: Formula): Formula = (a, b) match {
-        // true \/ _ = true
-        case (TrueF, _) => TrueF
-        // _ \/ true = true
-        case (_, TrueF) => TrueF
-        // lit \/ lit
-        case (List(a), List(b)) => formula(a ++ b)
-        // (c1 /\ ... /\ cn) \/ d = ((c1 \/ d) /\ ... /\ (cn \/ d))
-        case (cs, d) if cs.tail nonEmpty => cs flatMap (c => distribute(formula(c), d))
-        // d \/ (c1 /\ ... /\ cn) = ((d \/ c1) /\ ... /\ (d \/ cn))
-        case (d, cs) if cs.tail nonEmpty => cs flatMap (c => distribute(d, formula(c)))
+  trait DPLLSolver extends CNF {
+    // a literal is a (possibly negated) variable
+    def Lit(sym: Sym, pos: Boolean = true) = new Lit(sym, pos)
+    class Lit(val sym: Sym, val pos: Boolean) {
+      override def toString = if (!pos) "-"+ sym.toString else sym.toString
+      override def equals(o: Any) = o match {
+        case o: Lit => (o.sym == sym) && (o.pos == pos)
+        case _ => false
       }
+      override def hashCode = sym.hashCode + pos.hashCode
 
-      p match {
-        case True        => TrueF
-        case False       => FalseF
-        case s: Sym      => lit(s)
-        case Not(s: Sym) => negLit(s)
-        case And(a, b)   => conjunctiveNormalForm(a) ++ conjunctiveNormalForm(b)
-        case Or(a, b)    => distribute(conjunctiveNormalForm(a), conjunctiveNormalForm(b))
-      }
+      def unary_- = Lit(sym, !pos)
     }
 
-    def normalize(p: Prop) = conjunctiveNormalForm(negationNormalForm(removeVarEq(p)))
     def cnfString(f: Formula) = alignAcrossRows(f map (_.toList) toList, "\\/", " /\\\n")
 
     // adapted from http://lara.epfl.ch/w/sav10:simple_sat_solver (original by Hossein Hojjat)
-    type Model = Map[Sym, Boolean]
+//    type Model = Map[Sym, Boolean]
     val EmptyModel = Map.empty[Sym, Boolean]
+    val NoModel: Model = null
 
     // returns all solutions, if any (TODO: better infinite recursion backstop -- detect fixpoint??)
-    def fullDPLL(f: Formula): List[Model] = {
+    def findAllModelsFor(f: Formula): List[Model] = {
+      val vars: Set[Sym] = f.flatMap(_ collect {case l: Lit => l.sym}).toSet
+      // patmatDebug("vars "+ vars)
       // the negation of a model -(S1=True/False /\ ... /\ SN=True/False) = clause(S1=False/True, ...., SN=False/True)
       def negateModel(m: Model) = clause(m.toSeq.map{ case (sym, pos) => Lit(sym, !pos) } : _*)
 
-      def findAllModels(f: Formula, models: List[Model], recursionDepthAllowed: Int = 20): List[Model]=
+      def findAllModels(f: Formula, models: List[Model], recursionDepthAllowed: Int = 10): List[Model]=
         if (recursionDepthAllowed == 0) models
         else {
-          val (ok, model) = DPLL(f)
+          // patmatDebug("solving\n"+ cnfString(f))
+          val model = findModelFor(f)
           // if we found a solution, conjunct the formula with the model's negation and recurse
-          if (ok) findAllModels(f :+ negateModel(model), model :: models, recursionDepthAllowed - 1)
+          if (model ne NoModel) {
+            val unassigned = (vars -- model.keySet).toList
+            // patmatDebug("unassigned "+ unassigned +" in "+ model)
+            def force(lit: Lit) = {
+              val model = withLit(findModelFor(dropUnit(f, lit)), lit)
+              if (model ne NoModel) List(model)
+              else Nil
+            }
+            val forced = unassigned flatMap { s =>
+              force(Lit(s, true)) ++ force(Lit(s, false))
+            }
+            // patmatDebug("forced "+ forced)
+            val negated = negateModel(model)
+            findAllModels(f :+ negated, model :: (forced ++ models), recursionDepthAllowed - 1)
+          }
           else models
         }
 
       findAllModels(f, Nil)
     }
 
-    def DPLL(f: Formula): (Boolean, Model) = {
-      @inline def withLit(res: (Boolean, Model), l: Lit) = (res._1, res._2 + (l.sym -> l.pos))
-      @inline def orElse(a: (Boolean, Model), b: => (Boolean, Model)) = if (a._1) a else b
+    @inline private def withLit(res: Model, l: Lit): Model = if (res eq NoModel) NoModel else res + (l.sym -> l.pos)
+    @inline private def dropUnit(f: Formula, unitLit: Lit) = {
+      val negated = -unitLit
+      // drop entire clauses that are trivially true
+      // (i.e., disjunctions that contain the literal we're making true in the returned model),
+      // and simplify clauses by dropping the negation of the literal we're making true
+      // (since False \/ X == X)
+      f.filterNot(_.contains(unitLit)).map(_ - negated)
+    }
+
+    def findModelFor(f: Formula): Model = {
+      @inline def orElse(a: Model, b: => Model) = if (a ne NoModel) a else b
 
       // patmatDebug("dpll\n"+ cnfString(f))
 
-      if (f isEmpty) (true, EmptyModel)
-      else if(f exists (_.isEmpty)) (false, EmptyModel)
-      else f.find(_.size == 1) map { unitClause =>
-        val unitLit = unitClause.head
-        // patmatDebug("unit: "+ unitLit)
-        val negated = -unitLit
-        // drop entire clauses that are trivially true
-        // (i.e., disjunctions that contain the literal we're making true in the returned model),
-        // and simplify clauses by dropping the negation of the literal we're making true
-        // (since False \/ X == X)
-        val simplified = f.filterNot(_.contains(unitLit)).map(_ - negated)
-        withLit(DPLL(simplified), unitLit)
-      } getOrElse {
-        // partition symbols according to whether they appear in positive and/or negative literals
-        val pos = new HashSet[Sym]()
-        val neg = new HashSet[Sym]()
-        f.foreach{_.foreach{ lit =>
-          if (lit.pos) pos += lit.sym else neg += lit.sym
-        }}
-        // appearing in both positive and negative
-        val impures = pos intersect neg
-        // appearing only in either positive/negative positions
-        val pures = (pos ++ neg) -- impures
-
-        if (pures nonEmpty) {
-          val pureSym = pures.head
-          // turn it back into a literal
-          // (since equality on literals is in terms of equality
-          //  of the underlying symbol and its positivity, simply construct a new Lit)
-          val pureLit = Lit(pureSym, pos(pureSym))
-          // patmatDebug("pure: "+ pureLit +" pures: "+ pures +" impures: "+ impures)
-          val simplified = f.filterNot(_.contains(pureLit))
-          withLit(DPLL(simplified), pureLit)
-        } else {
-          val split = f.head.head
-          // patmatDebug("split: "+ split)
-          orElse(DPLL(f :+ clause(split)), DPLL(f :+ clause(-split)))
+      val start = startTimer(patmatAnaDPLL)
+
+      val satisfiableWithModel: Model =
+        if (f isEmpty) EmptyModel
+        else if(f exists (_.isEmpty)) NoModel
+        else f.find(_.size == 1) match {
+          case Some(unitClause) =>
+            val unitLit = unitClause.head
+            // patmatDebug("unit: "+ unitLit)
+            withLit(findModelFor(dropUnit(f, unitLit)), unitLit)
+          case _ =>
+            // partition symbols according to whether they appear in positive and/or negative literals
+            val pos = new HashSet[Sym]()
+            val neg = new HashSet[Sym]()
+            f.foreach{_.foreach{ lit =>
+              if (lit.pos) pos += lit.sym else neg += lit.sym
+            }}
+            // appearing in both positive and negative
+            val impures = pos intersect neg
+            // appearing only in either positive/negative positions
+            val pures = (pos ++ neg) -- impures
+
+            if (pures nonEmpty) {
+              val pureSym = pures.head
+              // turn it back into a literal
+              // (since equality on literals is in terms of equality
+              //  of the underlying symbol and its positivity, simply construct a new Lit)
+              val pureLit = Lit(pureSym, pos(pureSym))
+              // patmatDebug("pure: "+ pureLit +" pures: "+ pures +" impures: "+ impures)
+              val simplified = f.filterNot(_.contains(pureLit))
+              withLit(findModelFor(simplified), pureLit)
+            } else {
+              val split = f.head.head
+              // patmatDebug("split: "+ split)
+              orElse(findModelFor(f :+ clause(split)), findModelFor(f :+ clause(-split)))
+            }
         }
-      }
+
+        stopTimer(patmatAnaDPLL, start)
+
+        satisfiableWithModel
     }
   }
 
+
   /**
    * Represent a match as a formula in propositional logic that encodes whether the match matches (abstractly: we only consider types)
    *
    */
   trait SymbolicMatchAnalysis extends TreeMakerApproximation with Logic { self: CodegenCore =>
+    def prepareNewAnalysis() = { Var.resetUniques(); Const.resetUniques() }
+
     object Var {
       private var _nextId = 0
       def nextId = {_nextId += 1; _nextId}
 
+      def resetUniques() = {_nextId = 0; uniques.clear()}
       private val uniques = new collection.mutable.HashMap[Tree, Var]
       def apply(x: Tree): Var = uniques getOrElseUpdate(x, new Var(x, x.tpe))
     }
     class Var(val path: Tree, fullTp: Type, checked: Boolean = true) extends AbsVar {
+      private[this] val id: Int = Var.nextId
+
+      // private[this] var canModify: Option[Array[StackTraceElement]] = None
+      @inline private[this] def ensureCanModify = {} //if (canModify.nonEmpty) patmatDebug("BUG!"+ this +" modified after having been observed: "+ canModify.get.mkString("\n"))
+
+      @inline private[this] def observed = {} //canModify = Some(Thread.currentThread.getStackTrace)
+
+      // don't access until all potential equalities have been registered using registerEquality
+      private[this] val symForEqualsTo = new collection.mutable.HashMap[Const, Sym]
+
       // when looking at the domain, we only care about types we can check at run time
       val domainTp: Type = checkableType(fullTp)
 
+      private[this] var _considerNull = false
+      def considerNull: Unit = { ensureCanModify; if (NullTp <:< domainTp) _considerNull = true }
+
       // case None => domain is unknown,
       // case Some(List(tps: _*)) => domain is exactly tps
       // we enumerate the subtypes of the full type, as that allows us to filter out more types statically,
       // once we go to run-time checks (on Const's), convert them to checkable types
       // TODO: there seems to be bug for singleton domains (variable does not show up in model)
-      val domain = if (checked) enumerateSubtypes(fullTp).map(_.map(Const).toSet) else None
-
-      def describe = toString + ": "+ fullTp + domain.map(_.map(_.tp).mkString(" ::= ", " | ", "")).getOrElse(" ::= ??") +" // = "+ path
-      def domainEnumerable = domain.nonEmpty
+      lazy val domain: Option[Set[Const]] =
+        if (!checked) None
+        else {
+          val subConsts = enumerateSubtypes(fullTp).map{ tps =>
+            tps.toSet[Type].map{ tp =>
+              val domainC = TypeConst(tp)
+              registerEquality(domainC)
+              domainC
+            }
+          }
 
-      private val domMap = new collection.mutable.HashMap[Const, Sym]
-      private def symForEqualsTo(c: Const) = {
-        domMap getOrElseUpdate(c, {
-            // println("creating symbol for equality "+ this +" = "+ c)
-            Sym(this, c)
-          })
-      }
+          val allConsts =
+            if (! _considerNull) subConsts
+            else {
+              registerEquality(NullConst)
+              subConsts map (_ + NullConst)
+            }
 
-      // for this var, call it V, turn V = C into the equivalent proposition in boolean logic
-      // over all executions of this method on the same Var object,
-      def propForEqualsTo(c: Const): Prop = {
-        domain match {
-          case None => symForEqualsTo(c)
-          case Some(domainConsts) =>
-            val domainTps = domainConsts map (_.tp)
-            val checkedTp = c.tp
-            // find all the domain types that could make the type test true
-            // if the checked type is a supertype of the lub of the domain,
-            // we'll end up \/'ing the whole domain together,
-            // but must not simplify to True, as the type test may also fail...
-            val matches = domainTps.filter(_ <:< checkedTp).map{ tp => symForEqualsTo(Const(tp)) }
-            // println("type-equals-prop for "+ this +" = "+ c +": "+ (checkedTp, domainTp, domainTps) +" matches: "+ matches)
-
-            if (matches isEmpty) False else matches.reduceLeft(Or)
+          observed; allConsts
         }
-      }
 
-      def equalitySyms: Set[Sym] = domMap.values.toSet
+      // accessing after calling considerNull will result in inconsistencies
+      lazy val domainSyms: Option[Set[Sym]] = domain map { _ map symForEqualsTo }
 
-      private[this] val id: Int = Var.nextId
+
+      // populate equalitySyms
+      // don't care about the result, but want only one fresh symbol per distinct constant c
+      def registerEquality(c: Const): Unit = {ensureCanModify; symForEqualsTo getOrElseUpdate(c, Sym(this, c))}
+
+      // don't access until all potential equalities have been registered using registerEquality
+      lazy val equalitySyms = {observed; symForEqualsTo.values.toList}
+
+      // return the symbol that represents this variable being equal to the constant `c`, if it exists, otherwise False (for robustness)
+      // (registerEquality(c) must have been called prior, either when constructing the domain or from outside)
+      def propForEqualsTo(c: Const): Prop = {observed; symForEqualsTo.getOrElse(c, False)}
+
+
+      // don't call until all equalities have been registered and considerNull has been called (if needed)
+      def describe = toString + ": " + fullTp + domain.map(_.mkString(" ::= ", " | ", "// "+ symForEqualsTo.keys)).getOrElse(symForEqualsTo.keys.mkString(" ::= ", " | ", " | ...")) + " // = " + path
       override def toString = "V"+ id
+
+
+
+      // when V = C, which other V = Ci are implied?
+      //   V = null is an exclusive assignment, since null precludes any type test being true
+      //   V = Any does not imply anything (except non-nullness)
+      // consider:
+      //  when V's domain is closed, say V : X ::= A | B | C, and we have some value constants, say U and V, of type X:
+      //  (x: X) match { case U => case V => case _ : X => }
+      //
+      // V's equalityConsts (for the above match): TC(X), TC(A), TC(B), TC(C), VC(U), VC(V)
+      // Set(TC(X), VC(U), VC(V)).forall(c => Set(TC(A), TC(B), TC(C)).forall(_.covers(c)))
+      // Set(VC(U), VC(V), TC(A), TC(B), TC(C)).forall(_.implies(TC(X))
+      // impliedSuper for TC(X) is empty (since it's at the top of the lattice),
+      // but since we have a closed domain, we know that also one of the partitions must hold
+      // thus, TC(X) implies TC(A) \/ TC(B) \/ TC(C),
+      // we only need to add this implication when impliedSuper is empty,
+      // since that'll eventually be the case (transitive closure & acyclic graphs ftw)
+//      def impliedProp(c: Const): Prop = if (c eq NullConst) True else {
+//        val impliedSuper     =  /\((equalityConsts filter { other => (c != other) && c.implies(other) && !other.implies(c) } map symForEqualsTo))
+//
+//        val implied =
+//          if (impliedSuper == True) domain match { case None => True
+//            case Some(domCs) => \/(domCs filter { _.covers(c) } map symForEqualsTo)
+//          } else impliedSuper
+//
+//        // patmatDebug("impliedProp: "+(this, c, impliedSuper, implied))
+//        implied
+//      }
+//      private lazy val equalityConsts = symForEqualsTo.keySet
     }
 
 
     // all our variables range over types
     // a literal constant becomes ConstantType(Constant(v)) when the type allows it (roughly, anyval + string + null)
     // equality between variables: SingleType(x) (note that pattern variables cannot relate to each other -- it's always patternVar == nonPatternVar)
-    case class Const(tp: Type) {
-      override def toString = tp.toString
+    object Const {
+      def resetUniques() = {_nextTypeId = 0; _nextValueId = 0; uniques.clear()} // patmatDebug("RESET")
+
+      private var _nextTypeId = 0
+      def nextTypeId = {_nextTypeId += 1; _nextTypeId}
+
+      private var _nextValueId = 0
+      def nextValueId = {_nextValueId += 1; _nextValueId}
+
+      private val uniques = new collection.mutable.HashMap[Type, Const]
+      private[SymbolicMatchAnalysis] def unique(tp: Type, mkFresh: => Const): Const =
+        uniques.get(tp).getOrElse(
+          uniques.find {case (oldTp, oldC) => oldTp =:= tp} match {
+            case Some((_, c)) => c
+            case _ =>
+              val fresh = mkFresh
+              uniques(tp) = fresh
+              fresh
+          })
+    }
 
-      def toValueString = tp match {
-        case ConstantType(c) => c.escapedStringValue
-        case _ => tp.toString
+    sealed abstract class Const extends AbsConst {
+      protected def tp: Type
+      protected def wideTp: Type
+
+      def isAny = wideTp.typeSymbol == AnyClass
+
+//      final def covers(other: Const): Boolean = {
+//        val r = (this, other) match {
+//          case (_: ValueConst, _: ValueConst) => this == other // hashconsed
+//          case (TypeConst(a) , _: ValueConst) => a <:< other.wideTp
+//          case (_            , _: TypeConst)  => tp <:< other.tp
+//          case _                              => false
+//        }
+//        // if(r) patmatDebug("covers    : "+(this, other))
+//        // else  patmatDebug("NOT covers: "+(this, other))
+//        r
+//      }
+
+      final def implies(other: Const): Boolean = {
+        val r = (this, other) match {
+          case (_: ValueConst, _: ValueConst) => this == other // hashconsed
+          case (_: ValueConst, _: TypeConst)  => tp <:< other.tp
+          case (_: TypeConst,  _)             => tp <:< other.tp
+          case _                              => false
+        }
+        // if(r) patmatDebug("implies    : "+(this, other))
+        // else  patmatDebug("NOT implies: "+(this, other))
+        r
+      }
+
+      // does V = C preclude V having value `other`?  V = null is an exclusive assignment,
+      // but V = 1 does not preclude V = Int, or V = Any
+      final def excludes(other: Const): Boolean = {
+        val r = (this, other) match {
+          case (_, NullConst)                 => true
+          case (NullConst, _)                 => true
+          // this causes false negative for unreachability, but that's ok:
+          // example: val X = 1; val Y = 1; (2: Int) match { case X => case Y => /* considered reachable */ }
+          case (_: ValueConst, _: ValueConst) => this != other
+          case (_: ValueConst, _: TypeConst)  => !((tp <:< other.tp) || (other.tp <:< wideTp))
+          case (_: TypeConst,  _: ValueConst) => !((other.tp <:< tp) || (tp <:< other.wideTp))
+          case (_: TypeConst,  _: TypeConst)  => !((tp <:< other.tp) || (other.tp <:< tp))
+          case _                              => false
+        }
+        // if(r) patmatDebug("excludes    : "+(this, other))
+        // else  patmatDebug("NOT excludes: "+(this, other))
+        r
+      }
+
+      // the equality symbol for V = C is looked up by C
+      final override def equals(other: Any): Boolean = other match { case o: Const => this eq o case _ => false }
+    }
+
+
+    object TypeConst {
+      def apply(tp: Type) = {
+        if (tp =:= NullTp) NullConst
+        else if (tp.isInstanceOf[SingletonType]) ValueConst.fromType(tp)
+        else Const.unique(tp, new TypeConst(tp))
+      }
+      def unapply(c: TypeConst): Some[Type] = Some(c.tp)
+    }
+
+    // corresponds to a type test that does not imply any value-equality (well, except for outer checks, which we don't model yet)
+    sealed class TypeConst(val tp: Type) extends Const {
+      assert(!(tp =:= NullTp))
+      private[this] val id: Int = Const.nextTypeId
+
+      val wideTp = tp.widen
+
+      override def toString = tp.toString //+"#"+ id
+    }
+
+    // p is a unique type or a constant value
+    object ValueConst {
+      def fromType(tp: Type) = {
+        assert(tp.isInstanceOf[SingletonType])
+        val toString = tp match {
+          case ConstantType(c) => c.escapedStringValue
+          case _ => tp.toString
+        }
+        Const.unique(tp, new ValueConst(tp, tp.widen, toString))
+      }
+      def apply(p: Tree) = {
+        val tp = p.tpe.normalize
+        if (tp =:= NullTp) NullConst
+        else {
+          val wideTp = {
+            if (p.hasSymbol && p.symbol.isStable) tp.asSeenFrom(tp.prefix, p.symbol.owner).widen
+            else tp.widen
+          }
+
+          val narrowTp =
+            if (tp.isInstanceOf[SingletonType]) tp
+            else p match {
+              case Literal(c) =>
+                if (c.tpe.typeSymbol == UnitClass) c.tpe
+                else ConstantType(c)
+              case p if p.symbol.isStable =>
+                singleType(tp.prefix, p.symbol)
+              case x =>
+                // TODO: better type
+                x.tpe.narrow
+            }
+
+          val toString =
+            if (p.hasSymbol && p.symbol.isStable) p.symbol.name.toString // tp.toString
+            else p.toString //+"#"+ id
+
+          Const.unique(narrowTp, new ValueConst(narrowTp, checkableType(wideTp), toString)) // must make wide type checkable so that it is comparable to types from TypeConst
+        }
+      }
+    }
+    sealed class ValueConst(val tp: Type, val wideTp: Type, override val toString: String) extends Const {
+      // patmatDebug("VC"+(tp, wideTp, toString))
+      assert(!(tp =:= NullTp))
+      private[this] val id: Int = Const.nextValueId
+    }
+
+    lazy val NullTp = ConstantType(Constant(null))
+    case object NullConst extends Const {
+      protected def tp     = NullTp
+      protected def wideTp = NullTp
+
+      def isValue = true
+      override def toString = "null"
+    }
+
+
+    // turns a case (represented as a list of abstract tests)
+    // into a proposition that is satisfiable if the case may match
+    def symbolicCase(tests: List[Test], modelNull: Boolean = false): Prop = {
+      def symbolic(t: Cond): Prop = t match {
+        case AndCond(a, b) => And(symbolic(a), symbolic(b))
+        case OrCond(a, b) => Or(symbolic(a), symbolic(b))
+        case Top => True
+        case Havoc => False
+        case TypeCond(p, pt) => Eq(Var(p), TypeConst(checkableType(pt)))
+        case EqualityCond(p, q) => Eq(Var(p), ValueConst(q))
+        case NonNullCond(p) => if (!modelNull) True else Not(Eq(Var(p), NullConst))
+      }
+
+      val testsBeforeBody = tests.takeWhile(t => !t.treeMaker.isInstanceOf[BodyTreeMaker])
+      /\(testsBeforeBody.map(t => symbolic(t.cond)))
+    }
+
+    // TODO: model dependencies between variables: if V1 corresponds to (x: List[_]) and V2 is (x.hd), V2 cannot be assigned when V1 = null or V1 = Nil
+    // right now hackily implement this by pruning counter-examples
+    // unreachability would also benefit from a more faithful representation
+
+    // reachability (dead code)
+
+    // computes the first 0-based case index that is unreachable (if any)
+    // a case is unreachable if it implies its preceding cases
+    // call C the formula that is satisfiable if the considered case matches
+    // call P the formula that is satisfiable if the cases preceding it match
+    // the case is reachable if there is a model for -P /\ C,
+    // thus, the case is unreachable if there is no model for -(-P /\ C),
+    // or, equivalently, P \/ -C, or C => P
+    def unreachableCase(prevBinder: Symbol, cases: List[List[TreeMaker]], pt: Type): Option[Int] = {
+      // customize TreeMakersToConds (which turns a tree of tree makers into a more abstract DAG of tests)
+      // when approximating the current case (which we hope is reachable), be optimistic about the unknowns
+      object reachabilityApproximation extends TreeMakersToConds(prevBinder) {
+        def makeCondOptimistic(tm: TreeMaker)(recurse: TreeMaker => Cond): Cond = tm match {
+          // for unreachability, let's assume a guard always matches (unless we statically determined otherwise)
+          // otherwise, a guarded case would be considered unreachable
+          case GuardTreeMaker(guard) =>
+            guard.tpe match {
+              case ConstantType(Constant(false)) => Havoc // not the best name; however, symbolically, 'Havoc' becomes 'False'
+              case _ => Top
+            }
+          // similar to a guard, user-defined extractors should not cause us to freak out
+          // if we're not 100% sure it does not match (i.e., its result type is None or Constant(false) -- TODO),
+          // let's stay optimistic and assume it does
+          case ExtractorTreeMaker(_, _, _, _)
+             | ProductExtractorTreeMaker(_, Some(_), _)  => Top
+          // TODO: consider length-checks
+          case _ =>
+            makeCond(tm)(recurse)
+        }
+
+        // be pessimistic when approximating the prefix of the current case
+        // we hope the prefix fails so that we might get to the current case, which we hope is not dead
+        def makeCondPessimistic(tm: TreeMaker)(recurse: TreeMaker => Cond): Cond = makeCond(tm)(recurse)
+      }
+
+      val start = startTimer(patmatAnaReach)
+
+      // use the same approximator so we share variables,
+      // but need different conditions depending on whether we're conservatively looking for failure or success
+      val testCasesOk   = reachabilityApproximation.approximateMatch(cases, reachabilityApproximation.makeCondOptimistic)
+      val testCasesFail = reachabilityApproximation.approximateMatchAgain(cases, reachabilityApproximation.makeCondPessimistic)
+
+      reachabilityApproximation.discard()
+      prepareNewAnalysis()
+
+      val propsCasesOk   = testCasesOk   map (t => symbolicCase(t, modelNull = true))
+      val propsCasesFail = testCasesFail map (t => Not(symbolicCase(t, modelNull = true)))
+      val (eqAxiomsFail, symbolicCasesFail) = removeVarEq(propsCasesFail, considerNull = true)
+      val (eqAxiomsOk, symbolicCasesOk)     = removeVarEq(propsCasesOk,   considerNull = true)
+
+      try {
+        // most of the time eqAxiomsFail == eqAxiomsOk, but the different approximations might cause different variables to disapper in general
+        val eqAxiomsCNF =
+          if (eqAxiomsFail == eqAxiomsOk) eqFreePropToSolvable(eqAxiomsFail)
+          else eqFreePropToSolvable(And(eqAxiomsFail, eqAxiomsOk))
+
+        var prefix     = eqAxiomsCNF
+        var prefixRest = symbolicCasesFail
+        var current    = symbolicCasesOk
+        var reachable  = true
+        var caseIndex  = 0
+
+  //      patmatDebug("reachability, vars:\n"+ ((propsCasesFail flatMap gatherVariables) map (_.describe) mkString ("\n")))
+  //      patmatDebug("equality axioms:\n"+ cnfString(eqAxiomsCNF))
+
+        // invariant (prefixRest.length == current.length) && (prefix.reverse ++ prefixRest == symbolicCasesFail)
+        // termination: prefixRest.length decreases by 1
+        while (prefixRest.nonEmpty && reachable) {
+          val prefHead = prefixRest.head
+          caseIndex += 1
+          prefixRest = prefixRest.tail
+          if (prefixRest.isEmpty) reachable = true
+          else {
+            prefix = andFormula(eqFreePropToSolvable(prefHead), prefix)
+            current = current.tail
+            val model = findModelFor(andFormula(eqFreePropToSolvable(current.head), prefix))
+
+  //          patmatDebug("trying to reach:\n"+ cnfString(current.head) +"\nunder prefix:\n"+ cnfString(prefix))
+  //          if (ok) patmatDebug("reached: "+ modelString(model))
+
+            reachable = model ne NoModel
+          }
+        }
+
+        stopTimer(patmatAnaReach, start)
+
+        if (reachable) None else Some(caseIndex)
+      } catch {
+        case e : IllegalArgumentException =>
+//          patmatDebug(util.Position.formatMessage(prevBinder.pos, "Cannot check match for reachability", false))
+//          e.printStackTrace()
+          None // CNF budget exceeded
       }
     }
 
+    // exhaustivity
+
     // make sure it's not a primitive, else (5: Byte) match { case 5 => ... } sees no Byte
     // TODO: domain of feasibly enumerable built-in types (enums, char?)
     def enumerateSubtypes(tp: Type): Option[List[Type]] =
@@ -1945,12 +2399,6 @@ trait PatternMatching extends Transform with TypingTransformers with ast.TreeDSL
           Some(validSubTypes)
       }
 
-    def narrowTypeOf(p: Tree) = p match {
-      case Literal(c) => ConstantType(c)
-      case Ident(_) if p.symbol.isStable => singleType(p.tpe.prefix, p.symbol)
-      case x => x.tpe.narrow
-    }
-
     // approximate a type to the static type that is fully checkable at run time,
     // hiding statically known but dynamically uncheckable information using existential quantification
     // TODO: this is subject to the availability of TypeTags (since an abstract type with a type tag is checkable at run time)
@@ -1989,8 +2437,9 @@ trait PatternMatching extends Transform with TypingTransformers with ast.TreeDSL
       // - back off (to avoid crying exhaustive too often) when:
       //    - there are guards -->
       //    - there are extractor calls (that we can't secretly/soundly) rewrite
+      val start = startTimer(patmatAnaExhaust)
       var backoff = false
-      object exhaustivityApproximation extends TreeMakersToConds(prevBinder, cases) {
+      object exhaustivityApproximation extends TreeMakersToConds(prevBinder) {
         def makeCondExhaustivity(tm: TreeMaker)(recurse: TreeMaker => Cond): Cond = tm match {
           case p @ ExtractorTreeMaker(extractor, Some(lenCheck), testedBinder, _) =>
             p.checkedLength match {
@@ -2020,27 +2469,16 @@ trait PatternMatching extends Transform with TypingTransformers with ast.TreeDSL
         }
       }
 
-      def symbolic(t: Cond): Prop = t match {
-        case AndCond(a, b) => And(symbolic(a), symbolic(b))
-        case OrCond(a, b) => Or(symbolic(a), symbolic(b))
-        case Top => True
-        case Havoc => False
-        case TypeCond(p, pt) => Eq(Var(p), Const(checkableType(pt)))
-        case EqualityCond(p, q) => Eq(Var(p), Const(narrowTypeOf(q)))
-        case NonNullCond(p) => True // ignoring nullness because it generates too much noise Not(Eq(Var(p), Const(NullClass.tpe)))
-      }
+      val tests = exhaustivityApproximation.approximateMatch(cases, exhaustivityApproximation.makeCondExhaustivity)
 
-      def symbolicCase(tests: List[Test]) = {
-        val testsBeforeBody = tests.takeWhile(t => !t.treeMaker.isInstanceOf[BodyTreeMaker])
-        testsBeforeBody.map(t => symbolic(t.cond)).foldLeft(True: Prop)(And)
-      }
+      if (backoff) Nil else {
+        val prevBinderTree = exhaustivityApproximation.binderToUniqueTree(prevBinder)
 
-      val tests = exhaustivityApproximation.approximateMatch(exhaustivityApproximation.makeCondExhaustivity)
+        exhaustivityApproximation.discard()
+        prepareNewAnalysis()
 
-      if (backoff) Nil else {
-        val symbolicCases = tests map symbolicCase
+        val symbolicCases = tests map (symbolicCase(_, modelNull = false))
 
-        val prevBinderTree = exhaustivityApproximation.binderToUniqueTree(prevBinder)
 
         // TODO: null tests generate too much noise, so disabled them -- is there any way to bring them back?
         // assuming we're matching on a non-null scrutinee (prevBinder), when does the match fail?
@@ -2053,8 +2491,7 @@ trait PatternMatching extends Transform with TypingTransformers with ast.TreeDSL
         // val matchFails = And(symbolic(nonNullScrutineeCond), Not(symbolicCases reduceLeft (Or(_, _))))
 
         // when does the match fail?
-        val matchFails = Not(symbolicCases reduceLeft (Or(_, _)))
-
+        val matchFails = Not(\/(symbolicCases))
 
   // debug output:
         // patmatDebug("analysing:")
@@ -2064,15 +2501,25 @@ trait PatternMatching extends Transform with TypingTransformers with ast.TreeDSL
         // val vars = gatherVariables(matchFails)
         // patmatDebug("\nvars:\n"+ (vars map (_.describe) mkString ("\n")))
         //
-        // patmatDebug("\nmatchFails as CNF:\n"+ cnfString(normalize(matchFails)))
+        // patmatDebug("\nmatchFails as CNF:\n"+ cnfString(propToSolvable(matchFails)))
+
+        try {
+          // find the models (under which the match fails)
+          val matchFailModels = findAllModelsFor(propToSolvable(matchFails))
 
-        // find the models (under which the match fails)
-        val matchFailModels = fullDPLL(normalize(matchFails))
+          val scrutVar = Var(prevBinderTree)
+          val counterExamples = matchFailModels.map(modelToCounterExample(scrutVar))
 
-        val scrutVar = Var(prevBinderTree)
-        val counterExamples = matchFailModels.map(modelToCounterExample(scrutVar))
+          val pruned = CounterExample.prune(counterExamples).map(_.toString).sorted
 
-        CounterExample.prune(counterExamples).map(_.toString).sorted
+          stopTimer(patmatAnaExhaust, start)
+          pruned
+        } catch {
+          case e : IllegalArgumentException =>
+            // patmatDebug(util.Position.formatMessage(prevBinder.pos, "Cannot check match for exhaustivity", false))
+            // e.printStackTrace()
+            Nil // CNF budget exceeded
+        }
       }
     }
 
@@ -2088,13 +2535,13 @@ trait PatternMatching extends Transform with TypingTransformers with ast.TreeDSL
       protected[SymbolicMatchAnalysis] def flattenConsArgs: List[CounterExample] = Nil
       def coveredBy(other: CounterExample): Boolean = this == other || other == WildcardExample
     }
-    case class ValueExample(c: Const) extends CounterExample { override def toString = c.toValueString }
+    case class ValueExample(c: ValueConst) extends CounterExample { override def toString = c.toString }
     case class TypeExample(c: Const)  extends CounterExample { override def toString = "(_ : "+ c +")" }
     case class NegativeExample(nonTrivialNonEqualTo: List[Const]) extends CounterExample {
       override def toString = {
         val negation =
-          if (nonTrivialNonEqualTo.tail.isEmpty) nonTrivialNonEqualTo.head.toValueString
-          else nonTrivialNonEqualTo.map(_.toValueString).sorted.mkString("in (", ", ", ")")
+          if (nonTrivialNonEqualTo.tail.isEmpty) nonTrivialNonEqualTo.head.toString
+          else nonTrivialNonEqualTo.map(_.toString).sorted.mkString("in (", ", ", ")")
         "<not "+ negation +">"
       }
     }
@@ -2131,6 +2578,21 @@ trait PatternMatching extends Transform with TypingTransformers with ast.TreeDSL
     case object WildcardExample extends CounterExample { override def toString = "_" }
     case object NoExample extends CounterExample { override def toString = "??" }
 
+    @inline def modelToVarAssignment(model: Model): Map[Var, (Seq[Const], Seq[Const])] =
+      model.toSeq.groupBy{f => f match {case (sym, value) => sym.variable} }.mapValues{ xs =>
+        val (trues, falses) = xs.partition(_._2)
+        (trues map (_._1.const), falses map (_._1.const))
+        // should never be more than one value in trues...
+      }
+
+    def varAssignmentString(varAssignment: Map[Var, (Seq[Const], Seq[Const])]) =
+      varAssignment.toSeq.sortBy(_._1.toString).map { case (v, (trues, falses)) =>
+         val assignment = "== "+ (trues mkString("(", ", ", ")")) +"  != ("+ (falses mkString(", ")) +")"
+         v +"(="+ v.path +": "+ v.domainTp +") "+ assignment
+       }.mkString("\n")
+
+    def modelString(model: Model) = varAssignmentString(modelToVarAssignment(model))
+
     // return constructor call when the model is a true counter example
     // (the variables don't take into account type information derived from other variables,
     //  so, naively, you might try to construct a counter example like _ :: Nil(_ :: _, _ :: _),
@@ -2141,18 +2603,9 @@ trait PatternMatching extends Transform with TypingTransformers with ast.TreeDSL
       // x1.tl = ...
       // x1.hd.hd = ...
       // ...
-      val varAssignment = model.toSeq.groupBy{f => f match {case (sym, value) => sym.variable} }.mapValues{ xs =>
-        val (trues, falses) = xs.partition(_._2)
-        (trues map (_._1.const), falses map (_._1.const))
-        // should never be more than one value in trues...
-      }
-
-      // patmatDebug("var assignment for model "+ model +":\n"+
-      //   varAssignment.toSeq.sortBy(_._1.toString).map { case (v, (trues, falses)) =>
-      //     val assignment = "== "+ (trues mkString("(", ", ", ")")) +"  != ("+ (falses mkString(", ")) +")"
-      //     v +"(="+ v.path +": "+ v.domainTp +") "+ assignment
-      //   }.mkString("\n"))
+      val varAssignment = modelToVarAssignment(model)
 
+      // patmatDebug("var assignment for model "+ model +":\n"+ varAssignmentString(varAssignment))
 
       // chop a path into a list of symbols
       def chop(path: Tree): List[Symbol] = path match {
@@ -2198,7 +2651,9 @@ trait PatternMatching extends Transform with TypingTransformers with ast.TreeDSL
 
       // node in the tree that describes how to construct a counter-example
       case class VariableAssignment(variable: Var, equalTo: List[Const], notEqualTo: List[Const], fields: collection.mutable.Map[Symbol, VariableAssignment]) {
-        private lazy val ctor       = (equalTo match { case List(Const(tp)) => tp case _ => variable.domainTp }).typeSymbol.primaryConstructor
+        // need to prune since the model now incorporates all super types of a constant (needed for reachability)
+        private lazy val prunedEqualTo = equalTo filterNot (subsumed => equalTo.exists(better => (better ne subsumed) && (better implies subsumed)))
+        private lazy val ctor       = (prunedEqualTo match { case List(TypeConst(tp)) => tp case _ => variable.domainTp }).typeSymbol.primaryConstructor
         private lazy val ctorParams = if (ctor == NoSymbol || ctor.paramss.isEmpty) Nil else ctor.paramss.head
         private lazy val cls        = if (ctor == NoSymbol) NoSymbol else ctor.owner
         private lazy val caseFieldAccs = if (cls == NoSymbol) Nil else cls.caseFieldAccessors
@@ -2207,7 +2662,7 @@ trait PatternMatching extends Transform with TypingTransformers with ast.TreeDSL
         def allFieldAssignmentsLegal: Boolean =
           (fields.keySet subsetOf caseFieldAccs.toSet) && fields.values.forall(_.allFieldAssignmentsLegal)
 
-        private lazy val nonTrivialNonEqualTo = notEqualTo.filterNot{c => val sym = c.tp.typeSymbol; sym == AnyClass } // sym == NullClass ||
+        private lazy val nonTrivialNonEqualTo = notEqualTo.filterNot{c => c.isAny }
 
         // NoExample if the constructor call is ill-typed
         // (thus statically impossible -- can we incorporate this into the formula?)
@@ -2215,17 +2670,17 @@ trait PatternMatching extends Transform with TypingTransformers with ast.TreeDSL
         def toCounterExample(beBrief: Boolean = false): CounterExample =
           if (!allFieldAssignmentsLegal) NoExample
           else {
-//            println("describing "+ (variable, equalTo, notEqualTo, fields, cls, allFieldAssignmentsLegal))
-            val res = equalTo match {
+            // patmatDebug("describing "+ (variable, equalTo, notEqualTo, fields, cls, allFieldAssignmentsLegal))
+            val res = prunedEqualTo match {
               // a definite assignment to a value
-              case List(eq@Const(_: ConstantType)) if fields.isEmpty => ValueExample(eq)
+              case List(eq: ValueConst) if fields.isEmpty => ValueExample(eq)
 
               // constructor call
               // or we did not gather any information about equality but we have information about the fields
               //  --> typical example is when the scrutinee is a tuple and all the cases first unwrap that tuple and only then test something interesting
               case _ if cls != NoSymbol &&
-                        (  equalTo.nonEmpty
-                        || (fields.nonEmpty && !isPrimitiveValueClass(cls) && equalTo.isEmpty && notEqualTo.isEmpty)) =>
+                        (  prunedEqualTo.nonEmpty
+                        || (fields.nonEmpty && !isPrimitiveValueClass(cls) && prunedEqualTo.isEmpty && notEqualTo.isEmpty)) =>
 
                 @inline def args(brevity: Boolean = beBrief) = {
                   // figure out the constructor arguments from the field assignment
@@ -2252,7 +2707,7 @@ trait PatternMatching extends Transform with TypingTransformers with ast.TreeDSL
               // TODO: improve reasoning -- in the mean time, a false negative is better than an annoying false positive
               case _ => NoExample
             }
-// patmatDebug("described as: "+ res)
+            // patmatDebug("described as: "+ res)
             res
           }
 
@@ -2715,8 +3170,14 @@ trait PatternMatching extends Transform with TypingTransformers with ast.TreeDSL
                               with DeadCodeElimination
                               with SwitchEmission
                               with OptimizedCodegen
-                              with SymbolicMatchAnalysis { self: TreeMakers =>
+                              with SymbolicMatchAnalysis
+                              with DPLLSolver { self: TreeMakers =>
     override def optimizeCases(prevBinder: Symbol, cases: List[List[TreeMaker]], pt: Type, unchecked: Boolean): (List[List[TreeMaker]], List[Tree]) = {
+      if (!unchecked) {
+        unreachableCase(prevBinder, cases, pt) foreach { caseIndex =>
+          typer.context.unit.warning(cases(caseIndex).last.pos, "unreachable code")
+        }
+      }
       val counterExamples = if (unchecked) Nil else exhaustive(prevBinder, cases, pt)
       if (counterExamples.nonEmpty) {
         val ceString =
diff --git a/src/compiler/scala/tools/nsc/util/Statistics.scala b/src/compiler/scala/tools/nsc/util/Statistics.scala
index 61c7695911..53ab6654ee 100644
--- a/src/compiler/scala/tools/nsc/util/Statistics.scala
+++ b/src/compiler/scala/tools/nsc/util/Statistics.scala
@@ -60,6 +60,14 @@ class Statistics extends scala.reflect.internal.util.Statistics {
 
   val macroExpandCount = new Counter
   val macroExpandNanos = new Timer
+
+  val patmatNanos      = new Timer
+  val patmatAnaDPLL    = new Timer
+  val patmatAnaVarEq   = new Timer
+  val patmatCNF        = new Timer
+  val patmatAnaExhaust = new Timer
+  val patmatAnaReach   = new Timer
+  val patmatCNFSizes   = new collection.mutable.HashMap[Int, Int] withDefaultValue 0
 }
 
 object Statistics extends Statistics
@@ -71,7 +79,7 @@ abstract class StatisticsInfo {
   val global: Global
   import global._
 
-  var phasesShown = List("parser", "typer", "erasure", "cleanup")
+  var phasesShown = List("parser", "typer", "patmat", "erasure", "cleanup")
 
   def countNodes(tree: Tree, counts: ClassCounts) {
     for (t <- tree) counts(t.getClass) += 1
@@ -83,10 +91,15 @@ abstract class StatisticsInfo {
   def showRelTyper(timer: Timer) =
     timer+showPercent(timer.nanos, typerNanos.nanos)
 
-  def showCounts(counts: ClassCounts) =
+  def showRelPatmat(timer: Timer) =
+    timer+showPercent(timer.nanos, patmatNanos.nanos)
+
+  def showCounts[T](counts: scala.collection.mutable.Map[T, Int]) =
     counts.toSeq.sortWith(_._2 > _._2).map {
-      case (cls, cnt) =>
+      case (cls: Class[_], cnt) =>
         cls.toString.substring(cls.toString.lastIndexOf("$") + 1)+": "+cnt
+      case (o, cnt) =>
+        o.toString +": "+cnt
     }
 
   def print(phase: Phase) = if (phasesShown contains phase.name) {
@@ -169,6 +182,16 @@ abstract class StatisticsInfo {
       if (timer1   != null) inform("#timer1                  : " + timer1)
       if (timer2   != null) inform("#timer2                  : " + timer2)
       //for (t <- uniques.iterator) println("unique: "+t)
+
+      if (phase.name == "patmat") {
+        inform("time spent in patmat       : " + patmatNanos                   )
+        inform("             of which DPLL : " + showRelPatmat(patmatAnaDPLL   ))
+        inform("of which in CNF conversion : " + showRelPatmat(patmatCNF       ))
+        inform("           CNF size counts : " + showCounts(patmatCNFSizes     ))
+        inform("of which variable equality : " + showRelPatmat(patmatAnaVarEq  ))
+        inform("  of which in exhaustivity : " + showRelPatmat(patmatAnaExhaust))
+        inform("of which in unreachability : " + showRelPatmat(patmatAnaReach  ))
+      }
     }
   }
 }