| 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
|