Merge 2.10.x into master.

Conflicts:
	src/compiler/scala/tools/nsc/transform/patmat/Logic.scala

6 files changed, 305 insertions, 283 deletions

diff --git a/src/compiler/scala/tools/nsc/transform/patmat/Logic.scala b/src/compiler/scala/tools/nsc/transform/patmat/Logic.scala
index 4be84d8ca5..69d9987b05 100644
--- a/src/compiler/scala/tools/nsc/transform/patmat/Logic.scala
+++ b/src/compiler/scala/tools/nsc/transform/patmat/Logic.scala
@@ -289,238 +289,6 @@ trait Logic extends Debugging  {
   }
 }
 
-// naive CNF translation and simple DPLL solver
-trait SimpleSolver extends Logic {
-  import PatternMatchingStats._
-  trait CNF extends PropositionalLogic {
-
-    /** Override Array creation for efficiency (to not go through reflection). */
-    private implicit val clauseTag: scala.reflect.ClassTag[Clause] = new scala.reflect.ClassTag[Clause] {
-      def runtimeClass: java.lang.Class[Clause] = classOf[Clause]
-      final override def newArray(len: Int): Array[Clause] = new Array[Clause](len)
-    }
-
-    import scala.collection.mutable.ArrayBuffer
-    type FormulaBuilder = ArrayBuffer[Clause]
-    def formulaBuilder  = ArrayBuffer[Clause]()
-    def formulaBuilderSized(init: Int)  = new ArrayBuffer[Clause](init)
-    def addFormula(buff: FormulaBuilder, f: Formula): Unit = buff ++= f
-    def toFormula(buff: FormulaBuilder): Formula = buff
-
-    // CNF: a formula is a conjunction of clauses
-    type Formula = FormulaBuilder
-    def formula(c: Clause*): Formula = ArrayBuffer(c: _*)
-
-    type Clause  = Set[Lit]
-    // a clause is a disjunction of distinct literals
-    def clause(l: Lit*): Clause = l.toSet
-
-    type Lit
-    def Lit(sym: Sym, pos: Boolean = true): Lit
-
-    def andFormula(a: Formula, b: Formula): Formula = a ++ b
-    def simplifyFormula(a: Formula): Formula = a.distinct
-
-    private def merge(a: Clause, b: Clause) = a ++ b
-
-    // throws an AnalysisBudget.Exception when the prop results in a CNF that's too big
-    // TODO: be smarter/more efficient about this (http://lara.epfl.ch/w/sav09:tseitin_s_encoding)
-    def eqFreePropToSolvable(p: Prop): Formula = {
-      def negationNormalFormNot(p: Prop, budget: Int): Prop =
-        if (budget <= 0) throw AnalysisBudget.exceeded
-        else p match {
-          case And(a, b) =>  Or(negationNormalFormNot(a, budget - 1), negationNormalFormNot(b, budget - 1))
-          case Or(a, b)  => And(negationNormalFormNot(a, budget - 1), negationNormalFormNot(b, budget - 1))
-          case Not(p)    => negationNormalForm(p, budget - 1)
-          case True      => False
-          case False     => True
-          case s: Sym    => Not(s)
-        }
-
-      def negationNormalForm(p: Prop, budget: Int = AnalysisBudget.max): Prop =
-        if (budget <= 0) throw AnalysisBudget.exceeded
-        else p match {
-          case And(a, b)      => And(negationNormalForm(a, budget - 1), negationNormalForm(b, budget - 1))
-          case Or(a, b)       =>  Or(negationNormalForm(a, budget - 1), negationNormalForm(b, budget - 1))
-          case Not(negated)   => negationNormalFormNot(negated, budget - 1)
-          case True
-             | False
-             | (_ : 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, pos = false)))
-
-      def conjunctiveNormalForm(p: Prop, budget: Int = AnalysisBudget.max): Formula = {
-        def distribute(a: Formula, b: Formula, budget: Int): Formula =
-          if (budget <= 0) throw AnalysisBudget.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)))
-            }
-
-        if (budget <= 0) throw AnalysisBudget.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 = if (Statistics.canEnable) Statistics.startTimer(patmatCNF) else null
-      val res   = conjunctiveNormalForm(negationNormalForm(p))
-
-      if (Statistics.canEnable) Statistics.stopTimer(patmatCNF, start)
-
-      //
-      if (Statistics.canEnable) patmatCNFSizes(res.size).value += 1
-
-//      debug.patmat("cnf for\n"+ p +"\nis:\n"+cnfString(res))
-      res
-    }
-  }
-
-  // simple solver using DPLL
-  trait Solver 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 eq sym) && (o.pos == pos)
-        case _ => false
-      }
-      override def hashCode = sym.hashCode + pos.hashCode
-
-      def unary_- = Lit(sym, !pos)
-    }
-
-    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)
-    val EmptyModel = Map.empty[Sym, Boolean]
-    val NoModel: Model = null
-
-    // returns all solutions, if any (TODO: better infinite recursion backstop -- detect fixpoint??)
-    def findAllModelsFor(f: Formula): List[Model] = {
-      val vars: Set[Sym] = f.flatMap(_ collect {case l: Lit => l.sym}).toSet
-      // debug.patmat("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 = 10): List[Model]=
-        if (recursionDepthAllowed == 0) models
-        else {
-          debug.patmat("find all models for\n"+ cnfString(f))
-          val model = findModelFor(f)
-          // if we found a solution, conjunct the formula with the model's negation and recurse
-          if (model ne NoModel) {
-            val unassigned = (vars -- model.keySet).toList
-            debug.patmat("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, pos = true)) ++ force(Lit(s, pos = false))
-            }
-            debug.patmat("forced "+ forced)
-            val negated = negateModel(model)
-            findAllModels(f :+ negated, model :: (forced ++ models), recursionDepthAllowed - 1)
-          }
-          else models
-        }
-
-      findAllModels(f, Nil)
-    }
-
-    private def withLit(res: Model, l: Lit): Model = if (res eq NoModel) NoModel else res + (l.sym -> l.pos)
-    private def dropUnit(f: Formula, unitLit: Lit): Formula = {
-      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 dropped = formulaBuilderSized(f.size)
-      for {
-        clause <- f
-        if !(clause contains unitLit)
-      } dropped += (clause - negated)
-      dropped
-    }
-
-    def findModelFor(f: Formula): Model = {
-      @inline def orElse(a: Model, b: => Model) = if (a ne NoModel) a else b
-
-      debug.patmat("DPLL\n"+ cnfString(f))
-
-      val start = if (Statistics.canEnable) Statistics.startTimer(patmatAnaDPLL) else null
-
-      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
-            // debug.patmat("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 mutable.HashSet[Sym]()
-            val neg = new mutable.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))
-              // debug.patmat("pure: "+ pureLit +" pures: "+ pures +" impures: "+ impures)
-              val simplified = f.filterNot(_.contains(pureLit))
-              withLit(findModelFor(simplified), pureLit)
-            } else {
-              val split = f.head.head
-              // debug.patmat("split: "+ split)
-              orElse(findModelFor(f :+ clause(split)), findModelFor(f :+ clause(-split)))
-            }
-        }
-
-        if (Statistics.canEnable) Statistics.stopTimer(patmatAnaDPLL, start)
-
-        satisfiableWithModel
-    }
-  }
-}
-
 trait ScalaLogic extends Interface with Logic with TreeAndTypeAnalysis {
   trait TreesAndTypesDomain extends PropositionalLogic with CheckableTreeAndTypeAnalysis {
     type Type = global.Type
diff --git a/src/compiler/scala/tools/nsc/transform/patmat/MatchAnalysis.scala b/src/compiler/scala/tools/nsc/transform/patmat/MatchAnalysis.scala
index ceb4d26a0b..3ee75df6c4 100644
--- a/src/compiler/scala/tools/nsc/transform/patmat/MatchAnalysis.scala
+++ b/src/compiler/scala/tools/nsc/transform/patmat/MatchAnalysis.scala
@@ -125,23 +125,15 @@ trait TreeAndTypeAnalysis extends Debugging {
   }
 }
 
-trait MatchAnalysis extends TreeAndTypeAnalysis with ScalaLogic with MatchTreeMaking {
-  import PatternMatchingStats._
-  import global.{Tree, Type, Symbol, CaseDef, atPos,
-    Select, Block, ThisType, SingleType, NoPrefix, NoType, definitions, needsOuterTest,
-    ConstantType, Literal, Constant, gen, This, analyzer, EmptyTree, map2, NoSymbol, Traverser,
-    Function, Typed, treeInfo, DefTree, ValDef, nme, appliedType, Name, WildcardType, Ident, TypeRef,
-    UniqueType, RefinedType, currentUnit, SingletonType, singleType, ModuleClassSymbol,
-    nestedMemberType, TypeMap, EmptyScope, Apply, If, Bind, lub, Alternative, deriveCaseDef, Match, MethodType, LabelDef, TypeTree, Throw, newTermName}
-
-  import definitions._
-  import analyzer.{Typer, ErrorUtils, formalTypes}
+trait MatchApproximation extends TreeAndTypeAnalysis with ScalaLogic with MatchTreeMaking {
+  import global.{Tree, Type, NoType, Symbol, NoSymbol, ConstantType, Literal, Constant, Ident, UniqueType, RefinedType, EmptyScope}
+  import global.definitions.{ListClass, NilModule}
 
   /**
    * Represent a match as a formula in propositional logic that encodes whether the match matches (abstractly: we only consider types)
    *
    */
-  trait TreeMakerApproximation extends TreeMakers with TreesAndTypesDomain {
+  trait MatchApproximator extends TreeMakers with TreesAndTypesDomain {
     object Test {
       var currId = 0
     }
@@ -348,7 +340,14 @@ trait MatchAnalysis extends TreeAndTypeAnalysis with ScalaLogic with MatchTreeMa
     }
   }
 
-  trait MatchAnalyses extends TreeMakerApproximation  {
+}
+
+trait MatchAnalysis extends MatchApproximation {
+  import PatternMatchingStats._
+  import global.{Tree, Type, Symbol, NoSymbol, Ident, Select}
+  import global.definitions.{isPrimitiveValueClass, ConsClass, isTupleSymbol}
+
+  trait MatchAnalyzer extends MatchApproximator  {
     def uncheckedWarning(pos: Position, msg: String) = global.currentUnit.uncheckedWarning(pos, msg)
     def warn(pos: Position, ex: AnalysisBudget.Exception, kind: String) = uncheckedWarning(pos, s"Cannot check match for $kind.\n${ex.advice}")
 
@@ -498,7 +497,7 @@ trait MatchAnalysis extends TreeAndTypeAnalysis with ScalaLogic with MatchTreeMa
 
     // a way to construct a value that will make the match fail: a constructor invocation, a constant, an object of some type)
     class CounterExample {
-      protected[MatchAnalyses] def flattenConsArgs: List[CounterExample] = Nil
+      protected[MatchAnalyzer] def flattenConsArgs: List[CounterExample] = Nil
       def coveredBy(other: CounterExample): Boolean = this == other || other == WildcardExample
     }
     case class ValueExample(c: ValueConst) extends CounterExample { override def toString = c.toString }
@@ -513,11 +512,11 @@ trait MatchAnalysis extends TreeAndTypeAnalysis with ScalaLogic with MatchTreeMa
       }
     }
     case class ListExample(ctorArgs: List[CounterExample]) extends CounterExample {
-      protected[MatchAnalyses] override def flattenConsArgs: List[CounterExample] = ctorArgs match {
+      protected[MatchAnalyzer] override def flattenConsArgs: List[CounterExample] = ctorArgs match {
         case hd :: tl :: Nil => hd :: tl.flattenConsArgs
         case _ => Nil
       }
-      protected[MatchAnalyses] lazy val elems = flattenConsArgs
+      protected[MatchAnalyzer] lazy val elems = flattenConsArgs
 
       override def coveredBy(other: CounterExample): Boolean =
         other match {
@@ -692,11 +691,13 @@ trait MatchAnalysis extends TreeAndTypeAnalysis with ScalaLogic with MatchTreeMa
       VariableAssignment(scrutVar).toCounterExample()
     }
 
-    def analyzeCases(prevBinder: Symbol, cases: List[List[TreeMaker]], pt: Type, unchecked: Boolean): Unit = {
-      unreachableCase(prevBinder, cases, pt) foreach { caseIndex =>
-        reportUnreachable(cases(caseIndex).last.pos)
+    def analyzeCases(prevBinder: Symbol, cases: List[List[TreeMaker]], pt: Type, suppression: Suppression): Unit = {
+      if (!suppression.unreachable) {
+        unreachableCase(prevBinder, cases, pt) foreach { caseIndex =>
+          reportUnreachable(cases(caseIndex).last.pos)
+        }
       }
-      if (!unchecked) {
+      if (!suppression.exhaustive) {
         val counterExamples = exhaustive(prevBinder, cases, pt)
         if (counterExamples.nonEmpty)
           reportMissingCases(prevBinder.pos, counterExamples)
diff --git a/src/compiler/scala/tools/nsc/transform/patmat/MatchOptimization.scala b/src/compiler/scala/tools/nsc/transform/patmat/MatchOptimization.scala
index ebc2750a4d..dcf2413b15 100644
--- a/src/compiler/scala/tools/nsc/transform/patmat/MatchOptimization.scala
+++ b/src/compiler/scala/tools/nsc/transform/patmat/MatchOptimization.scala
@@ -30,7 +30,7 @@ trait MatchOptimization extends MatchTreeMaking with MatchAnalysis {
 
 
   ////
-  trait CommonSubconditionElimination extends TreeMakerApproximation { self: OptimizedCodegen =>
+  trait CommonSubconditionElimination extends OptimizedCodegen with MatchApproximator {
     /** a flow-sensitive, generalised, common sub-expression elimination
      * reuse knowledge from performed tests
      * the only sub-expressions we consider are the conditions and results of the three tests (type, type&equality, equality)
@@ -205,16 +205,16 @@ trait MatchOptimization extends MatchTreeMaking with MatchAnalysis {
 
 
   //// DCE
-  trait DeadCodeElimination extends TreeMakers {
-    // TODO: non-trivial dead-code elimination
-    // e.g., the following match should compile to a simple instanceof:
-    //   case class Ident(name: String)
-    //   for (Ident(name) <- ts) println(name)
-    def doDCE(prevBinder: Symbol, cases: List[List[TreeMaker]], pt: Type): List[List[TreeMaker]] = {
-      // do minimal DCE
-      cases
-    }
-  }
+//  trait DeadCodeElimination extends TreeMakers {
+//    // TODO: non-trivial dead-code elimination
+//    // e.g., the following match should compile to a simple instanceof:
+//    //   case class Ident(name: String)
+//    //   for (Ident(name) <- ts) println(name)
+//    def doDCE(prevBinder: Symbol, cases: List[List[TreeMaker]], pt: Type): List[List[TreeMaker]] = {
+//      // do minimal DCE
+//      cases
+//    }
+//  }
 
   //// SWITCHES -- TODO: operate on Tests rather than TreeMakers
   trait SwitchEmission extends TreeMakers with OptimizedMatchMonadInterface {
@@ -589,12 +589,12 @@ trait MatchOptimization extends MatchTreeMaking with MatchAnalysis {
     }
   }
 
-  trait MatchOptimizations extends CommonSubconditionElimination
-                              with DeadCodeElimination
-                              with SwitchEmission
-                              with OptimizedCodegen {
+  trait MatchOptimizer extends OptimizedCodegen
+                          with SwitchEmission
+                          with CommonSubconditionElimination {
     override def optimizeCases(prevBinder: Symbol, cases: List[List[TreeMaker]], pt: Type): (List[List[TreeMaker]], List[Tree]) = {
-      val optCases = doCSE(prevBinder, doDCE(prevBinder, cases, pt), pt)
+      // TODO: do CSE on result of doDCE(prevBinder, cases, pt)
+      val optCases = doCSE(prevBinder, cases, pt)
       val toHoist = (
         for (treeMakers <- optCases)
           yield treeMakers.collect{case tm: ReusedCondTreeMaker => tm.treesToHoist}
diff --git a/src/compiler/scala/tools/nsc/transform/patmat/MatchTreeMaking.scala b/src/compiler/scala/tools/nsc/transform/patmat/MatchTreeMaking.scala
index 51f21780b5..202f3444f8 100644
--- a/src/compiler/scala/tools/nsc/transform/patmat/MatchTreeMaking.scala
+++ b/src/compiler/scala/tools/nsc/transform/patmat/MatchTreeMaking.scala
@@ -23,16 +23,21 @@ trait MatchTreeMaking extends MatchCodeGen with Debugging {
   import global.{Tree, Type, Symbol, CaseDef, atPos, settings,
     Select, Block, ThisType, SingleType, NoPrefix, NoType, needsOuterTest,
     ConstantType, Literal, Constant, gen, This, EmptyTree, map2, NoSymbol, Traverser,
-    Function, Typed, treeInfo, TypeRef, DefTree}
+    Function, Typed, treeInfo, TypeRef, DefTree, Ident, nme}
 
   import global.definitions.{SomeClass, AnyRefClass, UncheckedClass, BooleanClass}
 
+  final case class Suppression(exhaustive: Boolean, unreachable: Boolean)
+  object Suppression {
+    val NoSuppression = Suppression(false, false)
+  }
+
 ///////////////////////////////////////////////////////////////////////////////////////////////////////////////////////////////////////////////////////////////
 // the making of the trees
 ///////////////////////////////////////////////////////////////////////////////////////////////////////////////////////////////////////////////////////////////
   trait TreeMakers extends TypedSubstitution with CodegenCore {
     def optimizeCases(prevBinder: Symbol, cases: List[List[TreeMaker]], pt: Type): (List[List[TreeMaker]], List[Tree])
-    def analyzeCases(prevBinder: Symbol, cases: List[List[TreeMaker]], pt: Type, unchecked: Boolean): Unit
+    def analyzeCases(prevBinder: Symbol, cases: List[List[TreeMaker]], pt: Type, suppression: Suppression): Unit
 
     def emitSwitch(scrut: Tree, scrutSym: Symbol, cases: List[List[TreeMaker]], pt: Type, matchFailGenOverride: Option[Tree => Tree], unchecked: Boolean): Option[Tree] =
       None
@@ -522,18 +527,24 @@ trait MatchTreeMaking extends MatchCodeGen with Debugging {
         def matchFailGen = (matchFailGenOverride orElse Some(CODE.MATCHERROR(_: Tree)))
         debug.patmat("combining cases: "+ (casesNoSubstOnly.map(_.mkString(" >> ")).mkString("{", "\n", "}")))
 
-        val (unchecked, requireSwitch) =
-          if (settings.XnoPatmatAnalysis.value) (true, false)
+        val (suppression, requireSwitch): (Suppression, Boolean) =
+          if (settings.XnoPatmatAnalysis.value) (Suppression.NoSuppression, false)
           else scrut match {
-            case Typed(_, tpt) =>
-              (tpt.tpe hasAnnotation UncheckedClass,
-               // matches with two or fewer cases need not apply for switchiness (if-then-else will do)
-               treeInfo.isSwitchAnnotation(tpt.tpe) && casesNoSubstOnly.lengthCompare(2) > 0)
+            case Typed(tree, tpt) =>
+              val suppressExhaustive = tpt.tpe hasAnnotation UncheckedClass
+              val supressUnreachable = tree match {
+                case Ident(name) if name startsWith nme.CHECK_IF_REFUTABLE_STRING => true // SI-7183 don't warn for withFilter's that turn out to be irrefutable.
+                case _ => false
+              }
+              val suppression = Suppression(suppressExhaustive, supressUnreachable)
+              // matches with two or fewer cases need not apply for switchiness (if-then-else will do)
+              val requireSwitch = treeInfo.isSwitchAnnotation(tpt.tpe) && casesNoSubstOnly.lengthCompare(2) > 0
+              (suppression, requireSwitch)
             case _ =>
-              (false, false)
+              (Suppression.NoSuppression, false)
           }
 
-        emitSwitch(scrut, scrutSym, casesNoSubstOnly, pt, matchFailGenOverride, unchecked).getOrElse{
+        emitSwitch(scrut, scrutSym, casesNoSubstOnly, pt, matchFailGenOverride, suppression.exhaustive).getOrElse{
           if (requireSwitch) typer.context.unit.warning(scrut.pos, "could not emit switch for @switch annotated match")
 
           if (casesNoSubstOnly nonEmpty) {
@@ -550,7 +561,7 @@ trait MatchTreeMaking extends MatchCodeGen with Debugging {
                   }) None
               else matchFailGen
 
-            analyzeCases(scrutSym, casesNoSubstOnly, pt, unchecked)
+            analyzeCases(scrutSym, casesNoSubstOnly, pt, suppression)
 
             val (cases, toHoist) = optimizeCases(scrutSym, casesNoSubstOnly, pt)
 
diff --git a/src/compiler/scala/tools/nsc/transform/patmat/PatternMatching.scala b/src/compiler/scala/tools/nsc/transform/patmat/PatternMatching.scala
index 0e5d3f4ea5..8be8b72130 100644
--- a/src/compiler/scala/tools/nsc/transform/patmat/PatternMatching.scala
+++ b/src/compiler/scala/tools/nsc/transform/patmat/PatternMatching.scala
@@ -41,7 +41,7 @@ trait PatternMatching extends Transform with TypingTransformers
                       with MatchTreeMaking
                       with MatchCodeGen
                       with ScalaLogic
-                      with SimpleSolver
+                      with Solving
                       with MatchAnalysis
                       with MatchOptimization {
   import global._
@@ -79,12 +79,12 @@ trait PatternMatching extends Transform with TypingTransformers
 
   class PureMatchTranslator(val typer: analyzer.Typer, val matchStrategy: Tree) extends MatchTranslator with PureCodegen {
     def optimizeCases(prevBinder: Symbol, cases: List[List[TreeMaker]], pt: Type) = (cases, Nil)
-    def analyzeCases(prevBinder: Symbol, cases: List[List[TreeMaker]], pt: Type, unchecked: Boolean): Unit = {}
+    def analyzeCases(prevBinder: Symbol, cases: List[List[TreeMaker]], pt: Type, suppression: Suppression): Unit = {}
   }
 
   class OptimizingMatchTranslator(val typer: analyzer.Typer) extends MatchTranslator
-                                                             with MatchOptimizations
-                                                             with MatchAnalyses
+                                                             with MatchOptimizer
+                                                             with MatchAnalyzer
                                                              with Solver
 }
 
diff --git a/src/compiler/scala/tools/nsc/transform/patmat/Solving.scala b/src/compiler/scala/tools/nsc/transform/patmat/Solving.scala
new file mode 100644
index 0000000000..34cdbeba8e
--- /dev/null
+++ b/src/compiler/scala/tools/nsc/transform/patmat/Solving.scala
@@ -0,0 +1,242 @@
+/* NSC -- new Scala compiler
+ *
+ * Copyright 2011-2013 LAMP/EPFL
+ * @author Adriaan Moors
+ */
+
+package scala.tools.nsc.transform.patmat
+
+import scala.collection.mutable
+import scala.reflect.internal.util.Statistics
+
+// naive CNF translation and simple DPLL solver
+trait Solving extends Logic {
+  import PatternMatchingStats._
+  trait CNF extends PropositionalLogic {
+
+    /** Override Array creation for efficiency (to not go through reflection). */
+    private implicit val clauseTag: scala.reflect.ClassTag[Clause] = new scala.reflect.ClassTag[Clause] {
+      def runtimeClass: java.lang.Class[Clause] = classOf[Clause]
+      final override def newArray(len: Int): Array[Clause] = new Array[Clause](len)
+    }
+
+    import scala.collection.mutable.ArrayBuffer
+    type FormulaBuilder = ArrayBuffer[Clause]
+    def formulaBuilder  = ArrayBuffer[Clause]()
+    def formulaBuilderSized(init: Int)  = new ArrayBuffer[Clause](init)
+    def addFormula(buff: FormulaBuilder, f: Formula): Unit = buff ++= f
+    def toFormula(buff: FormulaBuilder): Formula = buff
+
+    // CNF: a formula is a conjunction of clauses
+    type Formula = FormulaBuilder
+    def formula(c: Clause*): Formula = ArrayBuffer(c: _*)
+
+    type Clause  = Set[Lit]
+    // a clause is a disjunction of distinct literals
+    def clause(l: Lit*): Clause = l.toSet
+
+    type Lit
+    def Lit(sym: Sym, pos: Boolean = true): Lit
+
+    def andFormula(a: Formula, b: Formula): Formula = a ++ b
+    def simplifyFormula(a: Formula): Formula = a.distinct
+
+    private def merge(a: Clause, b: Clause) = a ++ b
+
+    // throws an AnalysisBudget.Exception when the prop results in a CNF that's too big
+    // TODO: be smarter/more efficient about this (http://lara.epfl.ch/w/sav09:tseitin_s_encoding)
+    def eqFreePropToSolvable(p: Prop): Formula = {
+      def negationNormalFormNot(p: Prop, budget: Int): Prop =
+        if (budget <= 0) throw AnalysisBudget.exceeded
+        else p match {
+          case And(a, b) =>  Or(negationNormalFormNot(a, budget - 1), negationNormalFormNot(b, budget - 1))
+          case Or(a, b)  => And(negationNormalFormNot(a, budget - 1), negationNormalFormNot(b, budget - 1))
+          case Not(p)    => negationNormalForm(p, budget - 1)
+          case True      => False
+          case False     => True
+          case s: Sym    => Not(s)
+        }
+
+      def negationNormalForm(p: Prop, budget: Int = AnalysisBudget.max): Prop =
+        if (budget <= 0) throw AnalysisBudget.exceeded
+        else p match {
+          case And(a, b)      => And(negationNormalForm(a, budget - 1), negationNormalForm(b, budget - 1))
+          case Or(a, b)       =>  Or(negationNormalForm(a, budget - 1), negationNormalForm(b, budget - 1))
+          case Not(negated)   => negationNormalFormNot(negated, budget - 1)
+          case True
+             | False
+             | (_ : 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, pos = false)))
+
+      def conjunctiveNormalForm(p: Prop, budget: Int = AnalysisBudget.max): Formula = {
+        def distribute(a: Formula, b: Formula, budget: Int): Formula =
+          if (budget <= 0) throw AnalysisBudget.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)))
+            }
+
+        if (budget <= 0) throw AnalysisBudget.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 = if (Statistics.canEnable) Statistics.startTimer(patmatCNF) else null
+      val res   = conjunctiveNormalForm(negationNormalForm(p))
+
+      if (Statistics.canEnable) Statistics.stopTimer(patmatCNF, start)
+
+      //
+      if (Statistics.canEnable) patmatCNFSizes(res.size).value += 1
+
+//      debug.patmat("cnf for\n"+ p +"\nis:\n"+cnfString(res))
+      res
+    }
+  }
+
+  // simple solver using DPLL
+  trait Solver 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 eq sym) && (o.pos == pos)
+        case _ => false
+      }
+      override def hashCode = sym.hashCode + pos.hashCode
+
+      def unary_- = Lit(sym, !pos)
+    }
+
+    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)
+    val EmptyModel = Map.empty[Sym, Boolean]
+    val NoModel: Model = null
+
+    // returns all solutions, if any (TODO: better infinite recursion backstop -- detect fixpoint??)
+    def findAllModelsFor(f: Formula): List[Model] = {
+      val vars: Set[Sym] = f.flatMap(_ collect {case l: Lit => l.sym}).toSet
+      // debug.patmat("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 = 10): List[Model]=
+        if (recursionDepthAllowed == 0) models
+        else {
+          debug.patmat("find all models for\n"+ cnfString(f))
+          val model = findModelFor(f)
+          // if we found a solution, conjunct the formula with the model's negation and recurse
+          if (model ne NoModel) {
+            val unassigned = (vars -- model.keySet).toList
+            debug.patmat("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, pos = true)) ++ force(Lit(s, pos = false))
+            }
+            debug.patmat("forced "+ forced)
+            val negated = negateModel(model)
+            findAllModels(f :+ negated, model :: (forced ++ models), recursionDepthAllowed - 1)
+          }
+          else models
+        }
+
+      findAllModels(f, Nil)
+    }
+
+    private def withLit(res: Model, l: Lit): Model = if (res eq NoModel) NoModel else res + (l.sym -> l.pos)
+    private def dropUnit(f: Formula, unitLit: Lit): Formula = {
+      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 dropped = formulaBuilderSized(f.size)
+      for {
+        clause <- f
+        if !(clause contains unitLit)
+      } dropped += (clause - negated)
+      dropped
+    }
+
+    def findModelFor(f: Formula): Model = {
+      @inline def orElse(a: Model, b: => Model) = if (a ne NoModel) a else b
+
+      debug.patmat("DPLL\n"+ cnfString(f))
+
+      val start = if (Statistics.canEnable) Statistics.startTimer(patmatAnaDPLL) else null
+
+      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
+            // debug.patmat("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 mutable.HashSet[Sym]()
+            val neg = new mutable.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))
+              // debug.patmat("pure: "+ pureLit +" pures: "+ pures +" impures: "+ impures)
+              val simplified = f.filterNot(_.contains(pureLit))
+              withLit(findModelFor(simplified), pureLit)
+            } else {
+              val split = f.head.head
+              // debug.patmat("split: "+ split)
+              orElse(findModelFor(f :+ clause(split)), findModelFor(f :+ clause(-split)))
+            }
+        }
+
+        if (Statistics.canEnable) Statistics.stopTimer(patmatAnaDPLL, start)
+
+        satisfiableWithModel
+    }
+  }
+}