diff options
| author | Gerard Basler <gerard.basler@gmail.com> | 2014-12-29 21:02:56 +0100 |
|---|---|---|
| committer | Gerard Basler <gerard.basler@gmail.com> | 2014-12-29 21:06:44 +0100 |
| commit | 5c296a419c32d8d76dbfebd091a98e3934da3e89 (patch) | |
| tree | 0c85b6306a44c539f98cae6771fa4b8ab1565ecb /src | |
| parent | cb272fefc6836265ec816508c345780560558fbb (diff) | |
| download | scala-5c296a419c32d8d76dbfebd091a98e3934da3e89.tar.gz scala-5c296a419c32d8d76dbfebd091a98e3934da3e89.tar.bz2 scala-5c296a419c32d8d76dbfebd091a98e3934da3e89.zip | |
Add unit tests for Tseitin CNF conversion.
We compare the results using the Tseitin transformation with the results of a
conversion via expansion of the formula (using distributive laws), e.g.,
```
+-------+
|Formula|
+---+---+
|
+-----------+-----------+
| |
v v
+---------+ +-------+
|Expansion| |Tseitin|
+----+----+ +---+---+
| +-----+ |
+------->| =?= |<-------+
+-----+
```
both methods should deliver the same results (i.e., models).
Diffstat (limited to 'src')
0 files changed, 0 insertions, 0 deletions