diff options
author | Gerard Basler <gerard.basler@gmail.com> | 2015-03-12 01:47:47 +0100 |
---|---|---|
committer | Adriaan Moors <adriaan.moors@typesafe.com> | 2015-04-06 14:58:46 -0700 |
commit | d44a86f432a7f9ca250b014acdeab02ac9f2c304 (patch) | |
tree | 3014edc291460cfe0dec4b5f7345a0ff1d174313 /test/junit | |
parent | 214d79841970be29bac126eb48f955c8f082e1bc (diff) | |
download | scala-d44a86f432a7f9ca250b014acdeab02ac9f2c304.tar.gz scala-d44a86f432a7f9ca250b014acdeab02ac9f2c304.tar.bz2 scala-d44a86f432a7f9ca250b014acdeab02ac9f2c304.zip |
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
Diffstat (limited to 'test/junit')
-rw-r--r-- | test/junit/scala/tools/nsc/transform/patmat/SolvingTest.scala | 58 |
1 files changed, 55 insertions, 3 deletions
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) + } } |