diff options
author | Gerard Basler <gerard.basler@gmail.com> | 2014-10-26 23:41:28 +0100 |
---|---|---|
committer | Gerard Basler <gerard.basler@gmail.com> | 2014-10-27 00:03:30 +0100 |
commit | 654912f5020d4f42dff8e2f5a17bdfa5d37befa5 (patch) | |
tree | 71054711f816ab3ca608b73250e4b66c38ba18b0 /src/intellij/test/files/pos | |
parent | 06ae047811d37a8ea6eef2bd92247c0dd5ceb289 (diff) | |
download | scala-654912f5020d4f42dff8e2f5a17bdfa5d37befa5.tar.gz scala-654912f5020d4f42dff8e2f5a17bdfa5d37befa5.tar.bz2 scala-654912f5020d4f42dff8e2f5a17bdfa5d37befa5.zip |
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)
Diffstat (limited to 'src/intellij/test/files/pos')
-rw-r--r-- | src/intellij/test/files/pos/virtpatmat_exhaust_big.scala | 34 |
1 files changed, 34 insertions, 0 deletions
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() + => + } +} +- |