Cleanup LinkedHashSet fixes and replace them with Set (i.e., back

to initial implementation).

Assuming that the DPLL procedure does not run into max recursion
depth, that workaround is not needed anymore, since the non-
determinism has been fixed.

Author: gbasler

src/compiler/scala/tools/nsc/transform/patmat/Logic.scala

@@ -87,7 +87,7 @@ trait Logic extends Debugging  {
       def mayBeNull: Boolean
 
       // compute the domain and return it (call registerNull first!)
-      def domainSyms: Option[mutable.LinkedHashSet[Sym]]
+      def domainSyms: Option[Set[Sym]]
 
       // the symbol for this variable being equal to its statically known type
       // (only available if registerEquality has been called for that type before)
@@ -205,7 +205,7 @@ trait Logic extends Debugging  {
     def removeVarEq(props: List[Prop], modelNull: Boolean = false): (Formula, List[Formula]) = {
       val start = if (Statistics.canEnable) Statistics.startTimer(patmatAnaVarEq) else null
 
-      val vars = mutable.LinkedHashSet[Var]()
+      val vars = new mutable.HashSet[Var]
 
       object gatherEqualities extends PropTraverser {
         override def apply(p: Prop) = p match {
@@ -292,7 +292,7 @@ trait Logic extends Debugging  {
     def eqFreePropToSolvable(p: Prop): Formula
     def cnfString(f: Formula): String
 
-    type Model = collection.immutable.SortedMap[Sym, Boolean]
+    type Model = Map[Sym, Boolean]
     val EmptyModel: Model
     val NoModel: Model
 
@@ -342,9 +342,9 @@ trait ScalaLogic extends Interface with Logic with TreeAndTypeAnalysis {
       // we enumerate the subtypes of the full type, as that allows us to filter out more types statically,
       // once we go to run-time checks (on Const's), convert them to checkable types
       // TODO: there seems to be bug for singleton domains (variable does not show up in model)
-      lazy val domain: Option[mutable.LinkedHashSet[Const]] = {
-        val subConsts: Option[mutable.LinkedHashSet[Const]] = enumerateSubtypes(staticTp).map { tps =>
-          mutable.LinkedHashSet(tps: _*).map{ tp =>
+      lazy val domain: Option[Set[Const]] = {
+        val subConsts = enumerateSubtypes(staticTp).map{ tps =>
+          tps.toSet[Type].map{ tp =>
             val domainC = TypeConst(tp)
             registerEquality(domainC)
             domainC
@@ -487,7 +487,7 @@ trait ScalaLogic extends Interface with Logic with TreeAndTypeAnalysis {
       }
 
       // accessing after calling registerNull will result in inconsistencies
-      lazy val domainSyms: Option[collection.mutable.LinkedHashSet[Sym]] = domain map { _ map symForEqualsTo }
+      lazy val domainSyms: Option[Set[Sym]] = domain map { _ map symForEqualsTo }
 
       lazy val symForStaticTp: Option[Sym]  = symForEqualsTo.get(TypeConst(staticTpCheckable))
 

src/compiler/scala/tools/nsc/transform/patmat/Solving.scala

@@ -26,16 +26,9 @@ trait Solving extends Logic {
     type Formula = FormulaBuilder
     def formula(c: Clause*): Formula = ArrayBuffer(c: _*)
 
-    type Clause  = collection.Set[Lit]
+    type Clause  = Set[Lit]
     // a clause is a disjunction of distinct literals
-    def clause(l: Lit*): Clause = (
-      if (l.lengthCompare(1) <= 0) {
-        l.toSet // SI-8531 Avoid LinkedHashSet's bulk for 0 and 1 element clauses
-      } else {
-        // neg/t7020.scala changes output 1% of the time, the non-determinism is quelled with this linked set
-        mutable.LinkedHashSet(l: _*)
-      }
-    )
+    def clause(l: Lit*): Clause = l.toSet
 
     type Lit
     def Lit(sym: Sym, pos: Boolean = true): Lit
@@ -140,7 +133,7 @@ trait Solving extends Logic {
     def cnfString(f: Formula) = alignAcrossRows(f map (_.toList) toList, "\\/", " /\\\n")
 
     // adapted from http://lara.epfl.ch/w/sav10:simple_sat_solver (original by Hossein Hojjat)
-    val EmptyModel = collection.immutable.SortedMap.empty[Sym, Boolean]
+    val EmptyModel = Map.empty[Sym, Boolean]
     val NoModel: Model = null
 
     // returns all solutions, if any (TODO: better infinite recursion backstop -- detect fixpoint??)
@@ -256,15 +249,14 @@ trait Solving extends Logic {
             withLit(findModelFor(dropUnit(f, unitLit)), unitLit)
           case _ =>
             // partition symbols according to whether they appear in positive and/or negative literals
-            // SI-7020 Linked- for deterministic counter examples.
-            val pos = new mutable.LinkedHashSet[Sym]()
-            val neg = new mutable.LinkedHashSet[Sym]()
+            val pos = new mutable.HashSet[Sym]()
+            val neg = new mutable.HashSet[Sym]()
             mforeach(f)(lit => if (lit.pos) pos += lit.sym else neg += lit.sym)
 
             // appearing in both positive and negative
-            val impures: mutable.LinkedHashSet[Sym] = pos intersect neg
+            val impures = pos intersect neg
             // appearing only in either positive/negative positions
-            val pures: mutable.LinkedHashSet[Sym] = (pos ++ neg) -- impures
+            val pures = (pos ++ neg) -- impures
 
             if (pures nonEmpty) {
               val pureSym = pures.head