| Tue, 21 Dec 2010 01:12:17 +0100 |
blanchet |
enable E weight generation with unofficial latest version of E (tentatively called E 1.2B) -- backed by Judgment Day
|
file |
diff |
annotate
|
| Sat, 18 Dec 2010 13:34:32 +0100 |
blanchet |
let each prover minimizes its own stuff (rather than taking the first prover of the list to minimize every prover's stuff)
|
file |
diff |
annotate
|
| Fri, 17 Dec 2010 22:15:08 +0100 |
blanchet |
more precise error messages in "verbose" (or "debug") mode, following this morning's permission debacle
|
file |
diff |
annotate
|
| Fri, 17 Dec 2010 00:27:40 +0100 |
blanchet |
more precise/correct SMT error handling
|
file |
diff |
annotate
|
| Thu, 16 Dec 2010 15:12:17 +0100 |
blanchet |
fixed more issues with the Vampire output parser, and added support for Vampire's TSTP output (--proof tptp)
|
file |
diff |
annotate
|
| Thu, 16 Dec 2010 15:12:17 +0100 |
blanchet |
generalize the Vampire parser some more to cope with things like "{2, 3\}" seen in some proofs
|
file |
diff |
annotate
|
| Wed, 15 Dec 2010 11:26:28 +0100 |
blanchet |
fix Vampire parsing problem
|
file |
diff |
annotate
|
| Wed, 08 Dec 2010 22:17:53 +0100 |
blanchet |
reword error message
|
file |
diff |
annotate
|
| Wed, 24 Nov 2010 16:15:15 +0100 |
blanchet |
more precise error handling in Sledgehammer/SMT for Z3 and remote SMT provers
|
file |
diff |
annotate
|
| Tue, 23 Nov 2010 22:37:16 +0100 |
blanchet |
more precise error handling for Z3;
|
file |
diff |
annotate
|
| Sat, 20 Nov 2010 00:53:26 +0100 |
wenzelm |
renamed raw "explode" function to "raw_explode" to emphasize its meaning;
|
file |
diff |
annotate
|
| Mon, 15 Nov 2010 18:56:29 +0100 |
blanchet |
pick up SMT solver crashes and report them to the user/Mirabelle if desired
|
file |
diff |
annotate
|
| Thu, 23 Sep 2010 10:34:01 +0200 |
blanchet |
make SML/NJ happy
|
file |
diff |
annotate
|
| Wed, 22 Sep 2010 10:02:39 +0200 |
blanchet |
make SML/NJ happier
|
file |
diff |
annotate
|
| Tue, 21 Sep 2010 10:02:50 +0200 |
blanchet |
make SML/NJ happier
|
file |
diff |
annotate
|
| Thu, 16 Sep 2010 15:16:08 +0200 |
blanchet |
refactoring: move ATP proof and error extraction code to "ATP_Proof" module
|
file |
diff |
annotate
|
| Thu, 16 Sep 2010 14:24:48 +0200 |
blanchet |
avoid code duplication
|
file |
diff |
annotate
|
| Thu, 16 Sep 2010 13:52:17 +0200 |
blanchet |
merge constructors
|
file |
diff |
annotate
|
| Thu, 16 Sep 2010 13:44:41 +0200 |
blanchet |
factor out the inverse of "nice_atp_problem"
|
file |
diff |
annotate
|
| Thu, 16 Sep 2010 11:59:45 +0200 |
blanchet |
use the same TSTP/Vampire/SPASS parser for one-liners as for Isar proofs
|
file |
diff |
annotate
|
| Thu, 16 Sep 2010 11:12:08 +0200 |
blanchet |
factored out TSTP/SPASS/Vampire proof parsing;
|
file |
diff |
annotate
|