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)

4 files changed, 74 insertions, 0 deletions

diff --git a/src/intellij/test/files/neg/virtpatmat_exhaust_big.check b/src/intellij/test/files/neg/virtpatmat_exhaust_big.check
new file mode 100644
index 0000000000..fddc85a362
--- /dev/null
+++ b/src/intellij/test/files/neg/virtpatmat_exhaust_big.check
@@ -0,0 +1,7 @@
+virtpatmat_exhaust_big.scala:27: warning: match may not be exhaustive.
+It would fail on the following input: Z11()
+  def foo(z: Z) = z match {
+                  ^
+error: No warnings can be incurred under -Xfatal-warnings.
+one warning found
+one error found
diff --git a/src/intellij/test/files/neg/virtpatmat_exhaust_big.flags b/src/intellij/test/files/neg/virtpatmat_exhaust_big.flags
new file mode 100644
index 0000000000..b5a8748652
--- /dev/null
+++ b/src/intellij/test/files/neg/virtpatmat_exhaust_big.flags
@@ -0,0 +1 @@
+-Xfatal-warnings -unchecked
diff --git a/src/intellij/test/files/neg/virtpatmat_exhaust_big.scala b/src/intellij/test/files/neg/virtpatmat_exhaust_big.scala
new file mode 100644
index 0000000000..dd639eb56e
--- /dev/null
+++ b/src/intellij/test/files/neg/virtpatmat_exhaust_big.scala
@@ -0,0 +1,32 @@
+sealed abstract class Z
+object Z {
+   object     Z0    extends Z
+   case class Z1()  extends Z
+   object     Z2    extends Z
+   case class Z3()  extends Z
+   object     Z4    extends Z
+   case class Z5()  extends Z
+   object     Z6    extends Z
+   case class Z7()  extends Z
+   object     Z8    extends Z
+   case class Z9()  extends Z
+   object     Z10   extends Z
+   case class Z11() extends Z
+   object     Z12   extends Z
+   case class Z13() extends Z
+   object     Z14   extends Z
+   case class Z15() extends Z
+   object     Z16   extends Z
+   case class Z17() extends Z
+   object     Z18   extends Z
+   case class Z19() extends Z
+}
+
+object Test {
+  import Z._
+  def foo(z: Z) = z match {
+    case Z0  | Z1()  | Z2  | Z3()  | Z4  | Z5()  | Z6  | Z7()  | Z8  | Z9() |
+         Z10 | Z12 | Z13() | Z14 | Z15() | Z16 | Z17() | Z18 | Z19()
+         =>
+  }
+}
diff --git a/src/intellij/test/files/pos/virtpatmat_exhaust_big.scala b/src/intellij/test/files/pos/virtpatmat_exhaust_big.scala
new file mode 100644
index 0000000000..41aef3226e
--- /dev/null
+++ b/src/intellij/test/files/pos/virtpatmat_exhaust_big.scala
@@ -0,0 +1,34 @@
+sealed abstract class Z
+object Z {
+   object     Z0    extends Z
+   case class Z1()  extends Z
+   object     Z2    extends Z
+   case class Z3()  extends Z
+   object     Z4    extends Z
+   case class Z5()  extends Z
+   object     Z6    extends Z
+   case class Z7()  extends Z
+   object     Z8    extends Z
+   case class Z9()  extends Z
+   object     Z10   extends Z
+   case class Z11() extends Z
+   object     Z12   extends Z
+   case class Z13() extends Z
+   object     Z14   extends Z
+   case class Z15() extends Z
+   object     Z16   extends Z
+   case class Z17() extends Z
+   object     Z18   extends Z
+   case class Z19() extends Z
+}
+
+// drop any case and it will report an error
+object Test {
+  import Z._
+  def foo(z: Z) = z match {
+    case Z0  | Z1()  | Z2  | Z3()  | Z4  | Z5()  | Z6  | Z7()  | Z8  | Z9() |
+         Z10 | Z11() | Z12 | Z13() | Z14 | Z15() | Z16 | Z17() | Z18 | Z19()
+         =>
+  }
+}
+-