| Fri, 21 Nov 2014 22:59:32 +0100 |
wenzelm |
tuned;
|
changeset |
files
|
| Fri, 21 Nov 2014 18:14:39 +0100 |
wenzelm |
removed some add-ons from modules that are relevant for the inference kernel;
|
changeset |
files
|
| Fri, 21 Nov 2014 13:18:56 +0100 |
Andreas Lochbihler |
add lemma following a proof suggestion by Joachim Breitner
|
changeset |
files
|
| Fri, 21 Nov 2014 12:24:59 +0100 |
Andreas Lochbihler |
add lemma
|
changeset |
files
|
| Fri, 21 Nov 2014 12:11:44 +0100 |
Andreas Lochbihler |
register pmf as BNF
|
changeset |
files
|
| Thu, 20 Nov 2014 17:29:18 +0100 |
blanchet |
added CVC4 option that helps on JD
|
changeset |
files
|
| Thu, 20 Nov 2014 17:29:18 +0100 |
blanchet |
always generate patterns as lists of lists, to avoid confusing CVC4 (and stick to what SMT-LIB 2 actually says)
|
changeset |
files
|
| Thu, 20 Nov 2014 17:29:18 +0100 |
blanchet |
work around bug in CVC4, with boolean arguments to (co)datatypes
|
changeset |
files
|
| Thu, 20 Nov 2014 17:29:18 +0100 |
blanchet |
other way of crashing (with CVC4)
|
changeset |
files
|
| Thu, 20 Nov 2014 17:29:18 +0100 |
blanchet |
set right logic for CVC4 with (co)datatypes
|
changeset |
files
|
| Thu, 20 Nov 2014 17:29:18 +0100 |
blanchet |
removed explicit '--quant-cf' option to CVC4, now that it's the default
|
changeset |
files
|
| Wed, 19 Nov 2014 19:12:14 +0100 |
traytel |
more accurate lemma name
|
changeset |
files
|
| Wed, 19 Nov 2014 10:31:15 +0100 |
blanchet |
parse CVC4 unsat cores
|
changeset |
files
|
| Wed, 19 Nov 2014 10:31:15 +0100 |
blanchet |
tuning
|
changeset |
files
|
| Wed, 19 Nov 2014 10:31:15 +0100 |
blanchet |
removed redundant code line
|
changeset |
files
|