SI-6582 Use Tseitin's algorithm for CNF.

This resolves the `AnalysisBudgetException` problem for big pattern matches. Initial experiments indicate that the problem is even simpler than initially thought: all formulae I got from the exhaustiveness check could be transformed directly into CNF. Thus the framework introduced here might be overkill and a much simpler implementation could work as well. For Scala 2.11 I'd suggest to replace the DPLL procedure with Sat4j.
scala · adriaanm · Aug 5, 2013 · Aug 5, 2013 · Aug 5, 2013 · Aug 6, 2013
commit d50cada25aa52a2e0aa242a7c78f3ca5cf1048e5
diff --git a/src/compiler/scala/tools/nsc/transform/patmat/CNFBuilder.scala b/src/compiler/scala/tools/nsc/transform/patmat/CNFBuilder.scala
@@ -0,0 +1,96 @@
+/* NSC -- new Scala compiler
+ *
+ * @author Gerard Basler
+ */
+
+package scala.tools.nsc.transform.patmat
+
+/** A literal.
+ */
+class Lit(val v: Int) extends AnyVal {
+  def unary_- : Lit = Lit(-v)
+  def variable: Int = Math.abs(v)
+  def positive = v >= 0
+}
+
+object Lit {
+  def apply(v: Int): Lit = new Lit(v)
+}
+
+/** Conjunctive normal form (of a Boolean formula).
+ *  A formula in this form is amenable to a SAT solver
+ *  (i.e., solver that decides satisfiability of a formula).
+ */
+class CNFBuilder {
+
+  import scala.collection.mutable.ArrayBuffer
+
+  // a clause is a disjunction of distinct literals
+  type Clause = Set[Lit]
+  type ClauseBuilder = ArrayBuffer[Clause]
+  private[this] val buff = ArrayBuffer[Clause]()
+  def clauses: Array[Clause] = buff.toArray
+
+  private[this] var myLiteralCount = 0
+  def allLiterals: Set[Lit] = (1 to myLiteralCount).map(Lit(_)).toSet
+  def newLiteral(): Lit = {
+    myLiteralCount += 1
+    Lit(myLiteralCount)
+  }
+
+  lazy val constTrue: Lit = {
+    val constTrue = newLiteral()
+    addClauseProcessed(constTrue)
+    constTrue
+  }
+
+  lazy val constFalse: Lit = -constTrue
+
+  def isConst(l: Lit): Boolean = l == constTrue || l == constFalse
+
+  def addClauseRaw(clause: Clause): Unit = buff += clause
+
+  /** Add literals vector, ignores clauses that are trivially satisfied
+   *
+   *  @param bv
+   */
+  def addClauseProcessed(bv: Lit*) {
+    val clause = processClause(bv: _*)
+    if (clause.nonEmpty)
+      addClauseRaw(clause)
+  }
+
+  /** @return empty clause, if clause trivially satisfied
+   */
+  private def processClause(bv: Lit*): Clause = {
+    val clause = bv.distinct
+
+    val isTautology = clause.combinations(2).exists {
+      case Seq(a, b) => a == -b
+    }
+
+    if (isTautology)
+      Set()
+    else
+      clause.toSet
+  }
+
+  override def toString: String = {
+    for {
+      clause <- buff
+    } yield {
+      clause.mkString("(", " ", ")")
+    }
+  }.mkString("\n")
+
+  def dimacs: String = {
+    val header = s"p cnf ${myLiteralCount} ${buff.length}\n"
+    header + {
+      for {
+        clause <- buff
+      } yield {
+        clause.toSeq.sortBy(_.variable) mkString ("", " ", " 0")
+      }
+    }.mkString("\n")
+  }
+}
diff --git a/src/compiler/scala/tools/nsc/transform/patmat/Logic.scala b/src/compiler/scala/tools/nsc/transform/patmat/Logic.scala
@@ -12,6 +12,7 @@ import scala.collection.mutable
 import scala.reflect.internal.util.Statistics
 import scala.reflect.internal.util.Position
 import scala.reflect.internal.util.HashSet
+import scala.collection.mutable.ArrayBuffer
 import scala.annotation.tailrec
 
 
@@ -139,6 +140,90 @@ trait Logic extends Debugging  {
     def /\(props: Iterable[Prop]) = if (props.isEmpty) True else And(props.toSet)
     def \/(props: Iterable[Prop]) = if (props.isEmpty) False else Or(props.toSet)
 
+    /**
+     * Simplifies propositional formula according to the following rules:
+     * - eliminate double negation (avoids unnecessary Tseitin variables)
+     * - flatten trees of same connectives (avoids unnecessary Tseitin variables)
+     * - removes constants and connectives that are in fact constant because of their operands
+     * - eliminates duplicate operands
+     *
+     * Complexity: DFS over formula tree
+     */
+    def simplify(f: Prop): Prop = {
+      // limit size to avoid blow up
+      def hasImpureAtom(ops: Seq[Prop]): Boolean = ops.size < 10 &&
+        ops.combinations(2).exists {
+        case Seq(a, Not(b)) if a == b => true
+        case Seq(Not(a), b) if a == b => true
+        case _                        => false
+      }
+
+      @tailrec
+      def isAtom(f: Prop): Boolean = f match {
+        case _: Sym | True | False => true
+        case Not(a)                   => isAtom(a)
+        case _                        => false
+      }
+
+      f match {
+        case And(fv)     =>
+          // recurse for nested And (pulls all Ands up)
+          val ops = fv.map(simplify) - True // ignore `True`
+
+          // build up Set in order to remove duplicates
+          val opsFlattened = (ops.flatMap {
+            case And(fv) => fv
+            case f       => Set(f)
+          }).toSeq
+
+          if (hasImpureAtom(opsFlattened) || opsFlattened.contains(False)) {
+            False
+          } else {
+            opsFlattened match {
+              case Seq()  => True
+              case Seq(f) => f
+              case ops    => And(ops.toSet)
+            }
+          }
+        case Or(fv)      =>
+          // recurse for nested Or (pulls all Ors up)
+          val ops = fv.map(simplify) - False // ignore `False`
+
+          val opsFlattened = (ops.flatMap {
+            case Or(fv) => fv
+            case f      => Set(f)
+          }).toSeq
+
+          if (hasImpureAtom(opsFlattened) || opsFlattened.contains(True)) {
+            True
+          } else {
+            opsFlattened match {
+              case Seq()  => False
+              case Seq(f) => f
+              case ops    => Or(ops.toSet)
+            }
+          }
+        case Not(Not(a)) =>
+          simplify(a)
+        case Not(True)   =>
+          False
+        case Not(False)  =>
+          True
+        case Not(p)      =>
+          Not(simplify(p)) match {
+            case Not(And(ops)) if ops.forall(isAtom) =>
+              // use De Morgan's rule to push negation into operands
+              // (might allow flattening of tree of connectives closer to root)
+              new Or(ops.map(p => simplify(Not(p)))) // call simplify again to remove redundant Not(s)
+            case Not(Or(ops)) if ops.forall(isAtom)  =>
+              // De Morgan (see above)
+              new And(ops.map(p => simplify(Not(p))))
+            case s                                   =>
+              s
+          }
+        case p => p
+      }
+    }
 
     trait PropTraverser {
       def apply(x: Prop): Unit = x match {
@@ -172,12 +257,13 @@ trait Logic extends Debugging  {
     // to govern how much time we spend analyzing matches for unreachability/exhaustivity
     object AnalysisBudget {
       import scala.tools.cmd.FromString.IntFromString
-      val max = sys.props.get("scalac.patmat.analysisBudget").collect(IntFromString.orElse{case "off" => Integer.MAX_VALUE}).getOrElse(256)
+      val TimeoutProperty = "scalac.patmat.analysisTimeOut"
+      val defaultTimeoutMillis = sys.props.get(TimeoutProperty).collect(IntFromString.orElse{case "off" => 0}).getOrElse(10 * 1000)
 
-      abstract class Exception(val advice: String) extends RuntimeException("CNF budget exceeded")
+      abstract class Exception(val advice: String) extends RuntimeException("SAT solver time budget exceeded")
 
-      object exceeded extends Exception(
-          s"(The analysis required more space than allowed. Please try with scalac -Dscalac.patmat.analysisBudget=${AnalysisBudget.max*2} or -Dscalac.patmat.analysisBudget=off.)")
+      object timeout extends Exception(
+          s"(The analysis required more time than allowed. Please try with scalac -D${TimeoutProperty}=${AnalysisBudget.defaultTimeoutMillis*2} or -D${TimeoutProperty}=off.)")
 
     }
 
@@ -199,7 +285,7 @@ trait Logic extends Debugging  {
     // 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)
     // may throw an AnalysisBudget.Exception
-    def removeVarEq(props: List[Prop], modelNull: Boolean = false): (Formula, List[Formula]) = {
+    def removeVarEq(props: List[Prop], modelNull: Boolean = false): (Prop, List[Prop]) = {
       val start = if (Statistics.canEnable) Statistics.startTimer(patmatAnaVarEq) else null
 
       val vars = new scala.collection.mutable.HashSet[Var]
@@ -223,10 +309,10 @@ trait Logic extends Debugging  {
       props foreach gatherEqualities.apply
       if (modelNull) vars foreach (_.registerNull)
 
-      val pure = props map (p => eqFreePropToSolvable(rewriteEqualsToProp(p)))
+      val pure = props map (p => rewriteEqualsToProp(p))
 
-      val eqAxioms = formulaBuilder
-      @inline def addAxiom(p: Prop) = addFormula(eqAxioms, eqFreePropToSolvable(p))
+      val eqAxioms = mutable.ArrayBuffer[Prop]()
+      @inline def addAxiom(p: Prop) = eqAxioms += p
 
       debug.patmat("removeVarEq vars: "+ vars)
       vars.foreach { v =>
@@ -252,49 +338,30 @@ trait Logic extends Debugging  {
         }
       }
 
      debug.patmat(s"eqAxioms:\n$eqAxioms")
+      debug.patmat(s"eqAxioms:\n${eqAxioms.mkString("\n")}")
       debug.patmat(s"pure:${pure.mkString("\n")}")
 
       if (Statistics.canEnable) Statistics.stopTimer(patmatAnaVarEq, start)
 
-      (toFormula(eqAxioms), pure)
+      (And(eqAxioms.toSet), pure)
     }
 
+    case class Solvable(cnf: CNFBuilder, symForVar: Map[Int, Sym])
 
-    // 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)
-      andFormula(eqAxioms, pure)
+    def propToSolvable(p: Prop): Solvable = {
+      val (eqAxiom, pure :: Nil) = removeVarEq(List(p), modelNull = false)
+      eqFreePropToSolvable(And(eqAxiom, pure))
     }
 
-    // may throw an AnalysisBudget.Exception
-    def eqFreePropToSolvable(p: Prop): Formula
-    def cnfString(f: Formula): String
+    def eqFreePropToSolvable(f: Prop): Solvable
 
     type Model = Map[Sym, Boolean]
     val EmptyModel: Model
     val NoModel: Model
 
-    def findModelFor(f: Formula): Model
-    def findAllModelsFor(f: Formula): List[Model]
+    def findModelFor(solvable: Solvable): Model
+
+    def findAllModelsFor(solvable: Solvable): List[Model]
   }
 }
 

diff --git a/src/compiler/scala/tools/nsc/transform/patmat/MatchAnalysis.scala b/src/compiler/scala/tools/nsc/transform/patmat/MatchAnalysis.scala
@@ -384,18 +384,19 @@ trait MatchAnalysis extends MatchApproximation {
       try {
         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.
+        // TODO: obsolete
+        val eqAxioms = simplify(And(eqAxiomsOk, eqAxiomsFail)) // I'm pretty sure eqAxiomsOk == eqAxiomsFail, but not 100% sure.
 
-        val prefix   = formulaBuilder
-        addFormula(prefix, eqAxioms)
+        val prefix = mutable.ArrayBuffer[Prop]()
+        prefix += eqAxioms
 
         var prefixRest = symbolicCasesFail
         var current    = symbolicCasesOk
         var reachable  = true
         var caseIndex  = 0
 
         debug.patmat("reachability, vars:\n"+ ((propsCasesFail flatMap gatherVariables).distinct map (_.describe) mkString ("\n")))
-        debug.patmat("equality axioms:\n"+ cnfString(eqAxiomsOk))
+        debug.patmat(s"equality axioms:\n$eqAxiomsOk")
 
         // invariant (prefixRest.length == current.length) && (prefix.reverse ++ prefixRest == symbolicCasesFail)
         // termination: prefixRest.length decreases by 1
@@ -405,9 +406,9 @@ trait MatchAnalysis extends MatchApproximation {
           prefixRest = prefixRest.tail
           if (prefixRest.isEmpty) reachable = true
           else {
-            addFormula(prefix, prefHead)
+            prefix += prefHead
             current = current.tail
-            val model = findModelFor(andFormula(current.head, toFormula(prefix)))
+            val model    = findModelFor(eqFreePropToSolvable(And((current.head +: prefix) : _*)))
 
             // debug.patmat("trying to reach:\n"+ cnfString(current.head) +"\nunder prefix:\n"+ cnfString(prefix))
             // if (NoModel ne model) debug.patmat("reached: "+ modelString(model))
@@ -485,7 +486,7 @@ trait MatchAnalysis extends MatchApproximation {
         } catch {
           case ex : AnalysisBudget.Exception =>
             warn(prevBinder.pos, ex, "exhaustivity")
-            Nil // CNF budget exceeded
+            Nil // SAT solver timeout
         }
       }
     }