| Wed, 30 Jul 2014 23:52:56 +0200 |
blanchet |
reduced preplay timeout to 1 s
|
file |
diff |
annotate
|
| Fri, 25 Jul 2014 13:15:50 +0200 |
blanchet |
reordered provers
|
file |
diff |
annotate
|
| Sun, 29 Jun 2014 18:28:27 +0200 |
blanchet |
compile
|
file |
diff |
annotate
|
| Tue, 24 Jun 2014 08:19:55 +0200 |
blanchet |
move method silencing code closer to the methods it is trying to silence, to reduce bad side-effects
|
file |
diff |
annotate
|
| Wed, 18 Jun 2014 15:23:40 +0200 |
blanchet |
more generous formula -- there are lots of duplicates out there
|
file |
diff |
annotate
|
| Wed, 18 Jun 2014 14:19:42 +0200 |
blanchet |
automatically learn MaSh facts also in 'blocking' mode
|
file |
diff |
annotate
|
| Thu, 12 Jun 2014 17:10:12 +0200 |
blanchet |
renamed Sledgehammer options
|
file |
diff |
annotate
|
| Thu, 12 Jun 2014 17:02:03 +0200 |
blanchet |
took out broken support for Yices from SMT2 stack -- see 'NEWS' for rationale
|
file |
diff |
annotate
|
| Wed, 11 Jun 2014 11:28:46 +0200 |
blanchet |
removed '_new' sufffix in SMT2 solver names (in some cases)
|
file |
diff |
annotate
|
| Wed, 11 Jun 2014 11:28:46 +0200 |
blanchet |
removed old SMT module from Sledgehammer
|
file |
diff |
annotate
|
| Mon, 02 Jun 2014 15:10:18 +0200 |
fleury |
basic setup for zipperposition prover
|
file |
diff |
annotate
|
| Fri, 16 May 2014 19:13:50 +0200 |
blanchet |
silence methods even better
|
file |
diff |
annotate
|
| Thu, 15 May 2014 20:48:13 +0200 |
blanchet |
new approach to silence proof methods, to avoid weird theory/context mismatches
|
file |
diff |
annotate
|
| Sun, 04 May 2014 18:14:58 +0200 |
blanchet |
improved whitelist (cf. be1874de8344)
|
file |
diff |
annotate
|
| Sat, 19 Apr 2014 19:52:02 +0200 |
wenzelm |
more elementary option sledgehammer_provers, avoiding complications of defaults from ML side (NB: guessing at number of cores does not make sense in PIDE);
|
file |
diff |
annotate
|
| Tue, 08 Apr 2014 14:59:36 +0200 |
wenzelm |
more uniform ML/document antiquotations;
|
file |
diff |
annotate
|
| Mon, 31 Mar 2014 10:28:08 +0200 |
wenzelm |
support bulk messages consisting of small string segments, which are more healthy to the Poly/ML RTS and might prevent spurious GC crashes such as MTGCProcessMarkPointers::ScanAddressesInObject;
|
file |
diff |
annotate
|
| Thu, 13 Mar 2014 13:18:13 +0100 |
blanchet |
integrate SMT2 with Sledgehammer
|
file |
diff |
annotate
|
| Fri, 14 Feb 2014 10:33:57 +0100 |
blanchet |
restored old 'remotify' logic -- too many bugs were introduced when refactoring the code
|
file |
diff |
annotate
|
| Thu, 13 Feb 2014 16:21:43 +0100 |
blanchet |
do the right thing with provers that exist only remotely (e.g. e_sine)
|
file |
diff |
annotate
|
| Mon, 03 Feb 2014 19:32:02 +0100 |
blanchet |
renamed 'smt' option 'smt_proofs' to avoid clash with 'smt' prover
|
file |
diff |
annotate
|
| Mon, 03 Feb 2014 17:13:31 +0100 |
blanchet |
added 'smt' option to control generation of 'by smt' proofs
|
file |
diff |
annotate
|
| Mon, 03 Feb 2014 15:33:18 +0100 |
blanchet |
tuning
|
file |
diff |
annotate
|
| Mon, 03 Feb 2014 10:19:19 +0100 |
blanchet |
reduced preplaying timeout, since (1) Isar proofs are getting better and better as alternatives; (2) the same timeout is used for each step in an Isar proof, where a lower timeout makes more sense
|
file |
diff |
annotate
|
| Fri, 31 Jan 2014 12:30:54 +0100 |
blanchet |
refactor large ML file
|
file |
diff |
annotate
|
| Fri, 31 Jan 2014 10:23:32 +0100 |
blanchet |
renamed many Sledgehammer ML files to clarify structure
|
file |
diff |
annotate
|
| Fri, 31 Jan 2014 10:23:32 +0100 |
blanchet |
renamed ML file
|
file |
diff |
annotate
|
| Fri, 31 Jan 2014 10:23:32 +0100 |
blanchet |
tuned ML file name
|
file |
diff |
annotate
| base
|