From d44a86f432a7f9ca250b014acdeab02ac9f2c304 Mon Sep 17 00:00:00 2001
From: Gerard Basler <gerard.basler@gmail.com>
Date: Thu, 12 Mar 2015 01:47:47 +0100
Subject: Patmat: efficient reasoning about mutual exclusion

Faster analysis of wide (but relatively flat) class hierarchies
by using a more efficient encoding of mutual exclusion.

The old CNF encoding for mutually exclusive symbols of a domain
added a quadratic number of clauses to the formula to satisfy.

E.g. if a domain has the symbols `a`, `b` and `c` then
the clauses
```
!a \/ !b  /\
!a \/ !c  /\
!b \/ !c
```
were added.

The first line prevents that `a` and `b` are both true at the same time, etc.

There's a simple, more efficient encoding that can be used instead: consider a
comparator circuit in hardware, that checks that out of `n` signals, at most 1
is true. Such a circuit can be built in the form of a sequential counter and
thus requires only 3n-4 additional clauses [1]. A comprehensible comparison of
different encodings can be found in [2].

[1]: http://www.carstensinz.de/papers/CP-2005.pdf
[2]: http://www.wv.inf.tu-dresden.de/Publications/2013/report-13-04.pdf
---
 .../tools/nsc/transform/patmat/SolvingTest.scala   | 58 ++++++++++++++++++++--
 1 file changed, 55 insertions(+), 3 deletions(-)

(limited to 'test/junit')

diff --git a/test/junit/scala/tools/nsc/transform/patmat/SolvingTest.scala b/test/junit/scala/tools/nsc/transform/patmat/SolvingTest.scala
index 1fe7b19056..7bcb90a2ee 100644
--- a/test/junit/scala/tools/nsc/transform/patmat/SolvingTest.scala
+++ b/test/junit/scala/tools/nsc/transform/patmat/SolvingTest.scala
@@ -52,6 +52,8 @@ object TestSolver extends Logic with Solving {
 
       def domainSyms = None
 
+      def groupedDomains: List[Set[TestSolver.Sym]] = Nil
+
       def implications = Nil
 
       def mayBeNull = false
@@ -207,11 +209,44 @@ class SolvingTest {
 
   import scala.tools.nsc.transform.patmat.TestSolver.TestSolver._
 
-  implicit val Ord: Ordering[TestSolver.TestSolver.Model] = Ordering.by {
-    _.toSeq.sortBy(_.toString()).toIterable
+  object SymName {
+    def unapply(s: Sym): Option[String] = {
+      val Var(Tree(name)) = s.variable
+      Some(name)
+    }
+  }
+
+  implicit val ModelOrd: Ordering[TestSolver.TestSolver.Model] = Ordering.by {
+    _.toSeq.sortWith {
+      case ((sym1, v1), (sym2, v2)) =>
+        val SymName(name1) = sym1
+        val SymName(name2) = sym2
+        if (name1 < name2)
+          true
+        else if (name1 > name2)
+          false
+        else
+          v1 < v2
+    }.toIterable
+  }
+
+  implicit val SolutionOrd: Ordering[TestSolver.TestSolver.Solution] =
+    Ordering.by(_.model)
+
+  def formatSolution(solution: Solution): String = {
+    formatModel(solution.model)
   }
 
-  private def sym(name: String) = Sym(Var(Tree(name)), NullConst)
+  def formatModel(model: Model): String = {
+    (for {
+      (SymName(name), value) <- model
+    } yield {
+      val v = if (value) "T" else "F"
+      s"$name -> $v"
+    }).mkString(", ")
+  }
+
+  def sym(name: String) = Sym(Var(Tree(name)), NullConst)
 
   @Test
   def testSymCreation() {
@@ -553,6 +588,23 @@ class SolvingTest {
         assertEquals(tseitinNoUnassigned, expansionNoUnassigned)
     }
   }
+
+  def pairWiseEncoding(ops: List[Sym]) = {
+    And(ops.combinations(2).collect {
+      case a :: b :: Nil => Or(Not(a), Not(b))
+    }.toSet[TestSolver.TestSolver.Prop])
+  }
+
+  @Test
+  def testAtMostOne() {
+    val dummySym = sym("dummy")
+    val syms = "pqrstu".map(c => sym(c.toString)).toList
+    // expand unassigned variables
+    // (otherwise solutions can not be compared)
+    val expected = TestSolver.TestSolver.findAllModelsFor(propToSolvable(And(dummySym, pairWiseEncoding(syms)))).flatMap(expandUnassigned)
+    val actual = TestSolver.TestSolver.findAllModelsFor(propToSolvable(And(dummySym, AtMostOne(syms)))).flatMap(expandUnassigned)
+    assertEquals(expected.toSet, actual.toSet)
+  }
 }
 
 
-- 
cgit v1.2.3