diff options
| author | Gerard Basler <gerard.basler@gmail.com> | 2015-03-12 01:47:47 +0100 |
|---|---|---|
| committer | Adriaan Moors <adriaan.moors@typesafe.com> | 2015-04-06 14:58:46 -0700 |
| commit | d44a86f432a7f9ca250b014acdeab02ac9f2c304 (patch) | |
| tree | 3014edc291460cfe0dec4b5f7345a0ff1d174313 /test/files/neg/patmatexhaust-huge.flags | |
| parent | 214d79841970be29bac126eb48f955c8f082e1bc (diff) | |
| download | scala-d44a86f432a7f9ca250b014acdeab02ac9f2c304.tar.gz scala-d44a86f432a7f9ca250b014acdeab02ac9f2c304.tar.bz2 scala-d44a86f432a7f9ca250b014acdeab02ac9f2c304.zip | |
Patmat: efficient reasoning about mutual exclusion
Faster analysis of wide (but relatively flat) class hierarchies
by using a more efficient encoding of mutual exclusion.
The old CNF encoding for mutually exclusive symbols of a domain
added a quadratic number of clauses to the formula to satisfy.
E.g. if a domain has the symbols `a`, `b` and `c` then
the clauses
```
!a \/ !b /\
!a \/ !c /\
!b \/ !c
```
were added.
The first line prevents that `a` and `b` are both true at the same time, etc.
There's a simple, more efficient encoding that can be used instead: consider a
comparator circuit in hardware, that checks that out of `n` signals, at most 1
is true. Such a circuit can be built in the form of a sequential counter and
thus requires only 3n-4 additional clauses [1]. A comprehensible comparison of
different encodings can be found in [2].
[1]: http://www.carstensinz.de/papers/CP-2005.pdf
[2]: http://www.wv.inf.tu-dresden.de/Publications/2013/report-13-04.pdf
Diffstat (limited to 'test/files/neg/patmatexhaust-huge.flags')
| -rw-r--r-- | test/files/neg/patmatexhaust-huge.flags | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/test/files/neg/patmatexhaust-huge.flags b/test/files/neg/patmatexhaust-huge.flags new file mode 100644 index 0000000000..591a950f83 --- /dev/null +++ b/test/files/neg/patmatexhaust-huge.flags @@ -0,0 +1 @@ +-Xfatal-warnings -unchecked -Ypatmat-exhaust-depth off
\ No newline at end of file |