Merge pull request #1915 from adriaanm/ticket-6942

SI-6942 more efficient CNF conversion in patmat analysis

1 files changed, 49 insertions, 25 deletions

diff --git a/src/compiler/scala/tools/nsc/typechecker/PatternMatching.scala b/src/compiler/scala/tools/nsc/typechecker/PatternMatching.scala
index f1c70f46d8..cdceb2d992 100644
--- a/src/compiler/scala/tools/nsc/typechecker/PatternMatching.scala
+++ b/src/compiler/scala/tools/nsc/typechecker/PatternMatching.scala
@@ -1954,7 +1954,8 @@ trait PatternMatching extends Transform with TypingTransformers with ast.TreeDSL
     //
     // TODO: for V1 representing x1 and V2 standing for x1.head, encode that
     //       V1 = Nil implies -(V2 = Ci) for all Ci in V2's domain (i.e., it is unassignable)
-    def removeVarEq(props: List[Prop], modelNull: Boolean = false): (Prop, List[Prop]) = {
+    // may throw an AnalysisBudget.Exception
+    def removeVarEq(props: List[Prop], modelNull: Boolean = false): (Formula, List[Formula]) = {
       val start = if (Statistics.canEnable) Statistics.startTimer(patmatAnaVarEq) else null
 
       val vars = new scala.collection.mutable.HashSet[Var]
@@ -1978,10 +1979,10 @@ trait PatternMatching extends Transform with TypingTransformers with ast.TreeDSL
       props foreach gatherEqualities.apply
       if (modelNull) vars foreach (_.registerNull)
 
-      val pure = props map rewriteEqualsToProp.apply
+      val pure = props map (p => eqFreePropToSolvable(rewriteEqualsToProp(p)))
 
-      var eqAxioms: Prop = True
-      def addAxiom(p: Prop) = eqAxioms = And(eqAxioms, p)
+      val eqAxioms = formulaBuilder
+      @inline def addAxiom(p: Prop) = addFormula(eqAxioms, eqFreePropToSolvable(p))
 
       patmatDebug("removeVarEq vars: "+ vars)
       vars.foreach { v =>
@@ -2007,23 +2008,37 @@ trait PatternMatching extends Transform with TypingTransformers with ast.TreeDSL
         }
       }
 
-      patmatDebug("eqAxioms:\n"+ cnfString(eqFreePropToSolvable(eqAxioms)))
-      patmatDebug("pure:"+ pure.map(p => cnfString(eqFreePropToSolvable(p))).mkString("\n"))
+      patmatDebug("eqAxioms:\n"+ cnfString(toFormula(eqAxioms)))
+      patmatDebug("pure:"+ pure.map(p => cnfString(p)).mkString("\n"))
 
       if (Statistics.canEnable) Statistics.stopTimer(patmatAnaVarEq, start)
 
-      (eqAxioms, pure)
+      (toFormula(eqAxioms), pure)
     }
 
 
+    // an interface that should be suitable for feeding a SAT solver when the time comes
     type Formula
+    type FormulaBuilder
+
+    // creates an empty formula builder to which more formulae can be added
+    def formulaBuilder: FormulaBuilder
+
+    // val f = formulaBuilder; addFormula(f, f1); ... addFormula(f, fN)
+    // toFormula(f) == andFormula(f1, andFormula(..., fN))
+    def addFormula(buff: FormulaBuilder, f: Formula): Unit
+    def toFormula(buff: FormulaBuilder): Formula
+
+    // the conjunction of formulae `a` and `b`
     def andFormula(a: Formula, b: Formula): Formula
 
+    // equivalent formula to `a`, but simplified in a lightweight way (drop duplicate clauses)
+    def simplifyFormula(a: Formula): Formula
 
     // may throw an AnalysisBudget.Exception
     def propToSolvable(p: Prop): Formula = {
       val (eqAxioms, pure :: Nil) = removeVarEq(List(p), modelNull = false)
-      eqFreePropToSolvable(And(eqAxioms, pure))
+      andFormula(eqAxioms, pure)
     }
 
     // may throw an AnalysisBudget.Exception
@@ -2039,24 +2054,34 @@ trait PatternMatching extends Transform with TypingTransformers with ast.TreeDSL
   }
 
   trait CNF extends Logic {
-    // CNF: a formula is a conjunction of clauses
-    type Formula = Array[Clause]
     /** 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)
     }
-    def formula(c: Clause*): Formula = c.toArray
-    def andFormula(a: Formula, b: Formula): Formula = a ++ b
 
+    import scala.collection.mutable.ArrayBuffer
+    type FormulaBuilder = ArrayBuffer[Clause]
+    def formulaBuilder  = ArrayBuffer[Clause]()
+    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
-    type Clause = Set[Lit]
     def clause(l: Lit*): Clause = l.toSet
-    private def merge(a: Clause, b: Clause) = a ++ b
 
     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 = {
@@ -2621,23 +2646,22 @@ trait PatternMatching extends Transform with TypingTransformers with ast.TreeDSL
 
       val propsCasesOk   = testCasesOk   map (t => symbolicCase(t, modelNull = true))
       val propsCasesFail = testCasesFail map (t => Not(symbolicCase(t, modelNull = true)))
-      val (eqAxiomsFail, symbolicCasesFail) = removeVarEq(propsCasesFail, modelNull = true)
-      val (eqAxiomsOk, symbolicCasesOk)     = removeVarEq(propsCasesOk,   modelNull = 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))
+        val (eqAxiomsFail, symbolicCasesFail) = removeVarEq(propsCasesFail, modelNull = true)
+        val (eqAxiomsOk, symbolicCasesOk)     = removeVarEq(propsCasesOk,   modelNull = true)
+        val eqAxioms = simplifyFormula(andFormula(eqAxiomsOk, eqAxiomsFail)) // I'm pretty sure eqAxiomsOk == eqAxiomsFail, but not 100% sure.
+
+        val prefix   = formulaBuilder
+        addFormula(prefix, eqAxioms)
 
-        var prefix     = eqAxiomsCNF
         var prefixRest = symbolicCasesFail
         var current    = symbolicCasesOk
         var reachable  = true
         var caseIndex  = 0
 
         patmatDebug("reachability, vars:\n"+ ((propsCasesFail flatMap gatherVariables).distinct map (_.describe) mkString ("\n")))
-        patmatDebug("equality axioms:\n"+ cnfString(eqAxiomsCNF))
+        patmatDebug("equality axioms:\n"+ cnfString(eqAxiomsOk))
 
         // invariant (prefixRest.length == current.length) && (prefix.reverse ++ prefixRest == symbolicCasesFail)
         // termination: prefixRest.length decreases by 1
@@ -2647,11 +2671,11 @@ trait PatternMatching extends Transform with TypingTransformers with ast.TreeDSL
           prefixRest = prefixRest.tail
           if (prefixRest.isEmpty) reachable = true
           else {
-            prefix = andFormula(eqFreePropToSolvable(prefHead), prefix)
+            addFormula(prefix, prefHead)
             current = current.tail
-            val model = findModelFor(andFormula(eqFreePropToSolvable(current.head), prefix))
+            val model = findModelFor(andFormula(current.head, toFormula(prefix)))
 
-            // patmatDebug("trying to reach:\n"+ cnfString(eqFreePropToSolvable(current.head)) +"\nunder prefix:\n"+ cnfString(prefix))
+            // patmatDebug("trying to reach:\n"+ cnfString(current.head) +"\nunder prefix:\n"+ cnfString(prefix))
             // if (NoModel ne model) patmatDebug("reached: "+ modelString(model))
 
             reachable = NoModel ne model