SI-6942 more efficient unreachability analysis

Avoid blowing the stack/the analysis budget by more eagerly translating
the propositions that model matches to CNF.
First building a large proposition that represents the match,
and then converting to CNF tends to blow the stack.
Luckily, it's easy to convert to CNF as we go.

The optimization relies on `CNF(P1 /\ ... /\ PN) == CNF(P1) ++ CNF(...) ++ CNF(PN)`:

Normalizing a conjunction of propositions
    yields the same formula as
concatenating the normalized conjuncts.

CNF conversion is expensive for large propositions,
so we push it down into the conjunction and
then concatenate the resulting arrays of clauses (which is cheap).

(CNF converts a free-form proposition into an `Array[Set[Lit]]`, where:
 - the Array's elements are /\'ed together;
 - and the Set's elements are \/'ed;
 - a Lit is a possibly negated variable.)

NOTE:
 - removeVarEq may throw an AnalysisBudget.Exception
 - also reworked the interface used to build formula,
   so that we can more easily plug in SAT4J when the time comes
use ArrayBuffer instead of Array to build Formulae
Merge pull request #1915 from adriaanm/ticket-6942

SI-6942 more efficient CNF conversion in patmat analysis
SI-6968 Simple Tuple patterns aren't irrefutable

Reverts part of c82ecab. The parser can't assume that
a pattern `(a, b)` will match, as results of
`.isInstanceOf[Tuple2]` can't be statically known until
after the typer.

The reopens SI-1336, SI-5589 and SI-4574, in exchange for fixing
this regression SI-6968. Keeping all of those fixed will require
a better definition of irrefutability, and some acrobatics to
ensure safe passage to the ambiguous trees through typechecking.
SI-4574 Leverage patmat for irrefutable filter elision

For-comprehension desugaring is spefified to elide the
`withFilter` call in `for (<pattern> <- xs)` if `pattern`
is irrefutable. But translating this corner of the spec
into a working compiler implementation has long been a
source of frustration and missteps.

The parser is able to detect irrefutability in trivial
cases, and elide the filtering. But for anything non-trivial,
(including, importantly, `for ((a, b) <- xs))`, it assumes
the filtering is required. The utility phase, `RefChecks`
attempts to find these calls, checks refutability (which
unlike it's myriad other tasks sort of matches its moniker!)
and elimiates the call if possible.

This is already problematic, because that possibly/maybe
call to `withFilter` can interfere with type checking
and inference. Tempting as it seemed, SI-6968 showed us
that we can't sidestep these by performing more pre-checks in
the parser.

The analysis in `RefChecks` has not been working at all
since the introduction of the new pattern matcher in Scala
2.10, as it is looking for a `Match` node that is now
translated earlier. Furthermore, it was making a common
mistake when on applications, forgetting to handle type
arguments.

So, history lesson over. Let's talk about the future.
Which is actually pretty simple.

We can exploit the fact that the pattern matcher runs
earlier by performing the refutability analysis
during match translation, and attaching the result to the
translated tree. `RefChecks` can now look for this attachment,
and eliminate the filtering.

I've also cleaned up the legacy code path, but while
the enclosed test now at least calls `isIrrefutable`
under `-Xoldpatmat`, it doesn't come up with the
right answer. I don't think its worthwhile to investigate
that further.