[backport] SI-7746 patmat: fix non-determinism, infeasible counter examples
Fixes non-determinism within the DPLL algorithm and disallows
infeasible counter examples directly in the formula.

The function to compute all solutions was flawed and thus only
returned a subset of the solutions. The algorithm would stop too soon
and thus depending on the ordering of the symbols return more or less
solutions. I also added printing a warning when the search was stopped
because the max recursion depth was reached. This is very useful as an
explanation of spuriously failing regression tests, since less counter
examples might be reported. In such a case the recursion depth should
be set to infinite by adding `-Ypatmat-exhaust-depth off`.

The mapping of the solutions of the DPLL algorithm to counter examples
has been adapted to take the additional solutions from the
solver into account:

Consider for example `t8430.scala`:

```Scala
sealed trait CL3Literal
case object IntLit extends CL3Literal
case object CharLit extends CL3Literal
case object BooleanLit extends CL3Literal
case object UnitLit extends CL3Literal

sealed trait Tree
case class LetL(value: CL3Literal) extends Tree
case object LetP extends Tree
case object LetC extends Tree
case object LetF extends Tree

object Test {
  (tree: Tree) => tree match {case LetL(CharLit) => ??? }
}
```

This test contains 2 domains,  `IntLit, CharLit, ...` and `LetL, LetP, ...`,
the corresponding formula to check exhaustivity looks like:

```
    V1=LetC.type#13    \/ V1=LetF.type#14 \/    V1=LetL#11     \/  V1=LetP.type#15    /\
 V2=BooleanLit.type#16 \/  V2=CharLit#12  \/ V2=IntLit.type#17 \/ V2=UnitLit.type#18  /\
      -V1=LetL#11      \/ -V2=CharLit#12  \/                   \/
```

The first two lines assign a value of the domain to the scrutinee (and
the correponding member in case of `LetL`) and prohibit the counter
example `LetL(CharLit)` since it's covered by the pattern match. The
used Boolean encoding allows that scrutinee `V1` can be equal to
`LetC` and `LetF` at the same time and thus, during enumeration of all
possible solutions of the formula, such a solution will be found,
since only one literal needs to be set to true, to  satisfy that
clause. That means, if at least one of the literals of such a clause
was in the `unassigned` list of the DPLL procedure, we will get
solutions where the scrutinee is equal to more than one element of the
domain.

A remedy would be to add constraints that forbid both literals
to be true at the same time. His is infeasible for big domains (see
`pos/t8531.scala`), since we would have to add a quadratic number of
clauses (one clause for each pair in the domain). A much simpler
solution is to just filter the invalid results. Since both values for
`unassigned` literals are explored, we will eventually find a valid
counter example.

Conflicts:
	src/compiler/scala/tools/nsc/settings/ScalaSettings.scala
	src/compiler/scala/tools/nsc/transform/patmat/MatchAnalysis.scala
	src/compiler/scala/tools/nsc/transform/patmat/Solving.scala
	test/files/neg/patmatexhaust.scala
	test/files/neg/t8430.check
	test/files/neg/t8430.flags
	test/files/run/virtpatmat_nested_lists.flags
	test/files/run/virtpatmat_opt_sharing.flags

ifxes
screw the proxy
[backport] 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.
And, Or take sets of Props
Remove redundant UniqueSym class.
Debug printing for Any, not AnyRef, to include primitives

Signed-off-by: Gerard Basler <gerard.basler@gmail.com>
[backport] Avoid the `CNF budget exceeded` exception via smarter translation into CNF.

The exhaustivity checks in the pattern matcher build a propositional
formula that must be converted into conjunctive normal form (CNF) in
order to be amenable to the following DPLL decision procedure.
However, the simple conversion into CNF via negation normal form and
Shannon expansion that was used has exponential worst-case complexity
and thus even simple problems could become untractable.

A better approach is to use a transformation into an _equisatisfiable_
CNF-formula (by generating auxiliary variables) that runs with linear
complexity. The commonly known Tseitin transformation uses bi-
implication. I have choosen for an enhancement: the Plaisted
transformation which uses implication only, thus the resulting CNF
formula has (on average) only half of the clauses of a Tseitin
transformation.

The Plaisted transformation uses the polarities of sub-expressions to
figure out which part of the bi-implication can be omitted. However,
if all sub-expressions have positive polarity (e.g., after
transformation into negation normal form) then the conversion is
rather simple and the pseudo-normalization via NNF increases chances
only one side of the bi-implication is needed.

I implemented only optimizations that had a substantial
effect on formula size:
- formula simplification, extraction of multi argument operands
- if a formula is already in CNF then the Tseitin/Plaisted
  transformation is omitted
- Plaisted via NNF
- omitted: (sharing of sub-formulas is also not implemented)
- omitted: (clause subsumption)

Conflicts:
	src/compiler/scala/tools/nsc/transform/patmat/Logic.scala
	src/compiler/scala/tools/nsc/transform/patmat/MatchAnalysis.scala
	src/compiler/scala/tools/nsc/transform/patmat/Solving.scala