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/t7519.check | |
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/t7519.check')
0 files changed, 0 insertions, 0 deletions