Permalink
Browse files

SI-7020 Determinism for pattern matcher warnings

Use LinkedHashSet for the DPLL algorithm for determistic
counter example generation.

Before, the test compiled with:

    [info] v2.10.2 => /Users/jason/usr/scala-v2.10.2-0-g60d462e
    test/files/neg/t7020.scala:3: warning: match may not be exhaustive.
    It would fail on the following inputs: List((x: Int forSome x not in (1, 2, 4, 5, 6, 7))), List(_, _)
      List(5) match {
          ^
    test/files/neg/t7020.scala:10: warning: match may not be exhaustive.
    It would fail on the following inputs: List((x: Int forSome x not in (1, 2, 4, 5, 6, 7))), List(_, _)
      List(5) match {
          ^
    test/files/neg/t7020.scala:17: warning: match may not be exhaustive.
    It would fail on the following inputs: List((x: Int forSome x not in (1, 2, 4, 6, 7)), _), List(1, _), List(2, _), List(4, _), List(5, _), List(6, _), List(7, _), List(??, _)
      List(5) match {
          ^
    test/files/neg/t7020.scala:24: warning: match may not be exhaustive.
    It would fail on the following input: List(_, _)
      List(5) match {
          ^
  • Loading branch information...
1 parent 1a03184 commit ebb01e05cbe4541838efa189196fe7a49ddb82cf @retronym retronym committed Aug 11, 2013
@@ -208,15 +208,16 @@ trait Solving extends Logic {
withLit(findModelFor(dropUnit(f, unitLit)), unitLit)
case _ =>
// partition symbols according to whether they appear in positive and/or negative literals
- val pos = new mutable.HashSet[Sym]()
- val neg = new mutable.HashSet[Sym]()
+ // SI-7020 Linked- for deterministic counter examples.
+ val pos = new mutable.LinkedHashSet[Sym]()
+ val neg = new mutable.LinkedHashSet[Sym]()
f.foreach{_.foreach{ lit =>
if (lit.pos) pos += lit.sym else neg += lit.sym
}}
// appearing in both positive and negative
- val impures = pos intersect neg
+ val impures: mutable.LinkedHashSet[Sym] = pos intersect neg
// appearing only in either positive/negative positions
- val pures = (pos ++ neg) -- impures
+ val pures: mutable.LinkedHashSet[Sym] = (pos ++ neg) -- impures
if (pures nonEmpty) {
val pureSym = pures.head
View
@@ -0,0 +1,17 @@
+t7020.scala:3: error: match may not be exhaustive.
+It would fail on the following inputs: List((x: Int forSome x not in (1, 2, 4, 5, 6, 7))), List(_, _)
+ List(5) match {
+ ^
+t7020.scala:10: error: match may not be exhaustive.
+It would fail on the following inputs: List((x: Int forSome x not in (1, 2, 4, 5, 6, 7))), List(_, _)
+ List(5) match {
+ ^
+t7020.scala:17: error: match may not be exhaustive.
+It would fail on the following inputs: List((x: Int forSome x not in (1, 2, 4, 5, 6, 7))), List(_, _)
+ List(5) match {
+ ^
+t7020.scala:24: error: match may not be exhaustive.
+It would fail on the following inputs: List((x: Int forSome x not in (1, 2, 4, 5, 6, 7))), List(_, _)
+ List(5) match {
+ ^
+four errors found
@@ -0,0 +1 @@
+-Xfatal-warnings
View
@@ -0,0 +1,30 @@
+object Test {
+ // warning was non-deterministic
+ List(5) match {
+ case 1 :: Nil | 2 :: Nil =>
+ case (x@(4 | 5 | 6)) :: Nil =>
+ case 7 :: Nil =>
+ case Nil =>
+ }
+
+ List(5) match {
+ case 1 :: Nil | 2 :: Nil =>
+ case (x@(4 | 5 | 6)) :: Nil =>
+ case 7 :: Nil =>
+ case Nil =>
+ }
+
+ List(5) match {
+ case 1 :: Nil | 2 :: Nil =>
+ case (x@(4 | 5 | 6)) :: Nil =>
+ case 7 :: Nil =>
+ case Nil =>
+ }
+
+ List(5) match {
+ case 1 :: Nil | 2 :: Nil =>
+ case (x@(4 | 5 | 6)) :: Nil =>
+ case 7 :: Nil =>
+ case Nil =>
+ }
+}

0 comments on commit ebb01e0

Please sign in to comment.