diff options
author | Adriaan Moors <adriaan.moors@typesafe.com> | 2015-04-13 09:37:12 -0700 |
---|---|---|
committer | Adriaan Moors <adriaan.moors@typesafe.com> | 2015-04-13 09:37:12 -0700 |
commit | 8623c2be74f8de0c400dcc04eb6f83168c6272c0 (patch) | |
tree | a40b71e4d6df2f81ecc479b7b9ff9b775e42e32a /test/junit | |
parent | 6e7b32649b041a001fdb61ca184c57e4c8228056 (diff) | |
parent | d44a86f432a7f9ca250b014acdeab02ac9f2c304 (diff) | |
download | scala-8623c2be74f8de0c400dcc04eb6f83168c6272c0.tar.gz scala-8623c2be74f8de0c400dcc04eb6f83168c6272c0.tar.bz2 scala-8623c2be74f8de0c400dcc04eb6f83168c6272c0.zip |
Merge pull request #4431 from adriaanm/rebase-4379
Patmat: efficient reasoning about mutual exclusion
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) + } } |