Thu, 19 Dec 2013 09:28:20 +0100 |
blanchet |
tuning
|
file |
diff |
annotate
|
Tue, 19 Nov 2013 18:34:04 +0100 |
blanchet |
tuning
|
file |
diff |
annotate
|
Thu, 17 Oct 2013 20:49:19 +0200 |
blanchet |
generate a comment storing the goal nickname in "learn_prover"
|
file |
diff |
annotate
|
Thu, 17 Oct 2013 02:22:54 +0200 |
blanchet |
thread the goal through instead of relying on unreliable (possibly fake) state
|
file |
diff |
annotate
|
Thu, 17 Oct 2013 01:20:40 +0200 |
blanchet |
verbose minimization when learning from ATP proofs
|
file |
diff |
annotate
|
Wed, 16 Oct 2013 19:55:23 +0200 |
blanchet |
have MaSh minimize
|
file |
diff |
annotate
|
Mon, 23 Sep 2013 14:53:43 +0200 |
blanchet |
added "spy" option to Sledgehammer
|
file |
diff |
annotate
|
Fri, 20 Sep 2013 22:39:30 +0200 |
blanchet |
merged "isar_try0" and "isar_minimize" options
|
file |
diff |
annotate
|
Fri, 20 Sep 2013 22:39:30 +0200 |
blanchet |
hardcoded obscure option
|
file |
diff |
annotate
|
Fri, 20 Sep 2013 22:39:30 +0200 |
blanchet |
hard-coded an obscure option
|
file |
diff |
annotate
|
Fri, 20 Sep 2013 22:39:30 +0200 |
blanchet |
use configuration mechanism for low-level tracing
|
file |
diff |
annotate
|
Thu, 12 Sep 2013 22:10:57 +0200 |
blanchet |
prefixed types and some functions with "atp_" for disambiguation
|
file |
diff |
annotate
|
Fri, 12 Jul 2013 22:41:25 +0200 |
smolkas |
added sledgehammer parameters isar_try0 and isar_minimize and their negative aliases
|
file |
diff |
annotate
|
Tue, 09 Jul 2013 18:45:06 +0200 |
smolkas |
completely rewrote SH compress; added two parameters for experimentation/fine grained control
|
file |
diff |
annotate
|
Tue, 09 Jul 2013 18:44:59 +0200 |
smolkas |
moved code -> easier debugging
|
file |
diff |
annotate
|
Thu, 16 May 2013 13:34:13 +0200 |
blanchet |
tuning -- renamed '_from_' to '_of_' in Sledgehammer
|
file |
diff |
annotate
|
Wed, 15 May 2013 17:43:42 +0200 |
blanchet |
renamed Sledgehammer functions with 'for' in their names to 'of'
|
file |
diff |
annotate
|
Mon, 06 May 2013 11:03:08 +0200 |
smolkas |
added preplay tracing
|
file |
diff |
annotate
|
Wed, 20 Feb 2013 14:10:51 +0100 |
blanchet |
minimize SMT proofs with E if Isar proofs are desired and Metis managed to preplay
|
file |
diff |
annotate
|
Wed, 20 Feb 2013 08:44:24 +0100 |
blanchet |
auto-minimizer should respect "isar_proofs = true"
|
file |
diff |
annotate
|
Wed, 20 Feb 2013 08:44:24 +0100 |
blanchet |
made "isar_proofs" a 3-way option, to provide a way to totally disable isar_proofs if desired
|
file |
diff |
annotate
|
Tue, 19 Feb 2013 17:01:06 +0100 |
blanchet |
avoid using "smt" for minimization -- better use the prover itself, since then Sledgehammer gets to try metis again and gives the opportunity to output an Isar proof -- and show Isar proof as fallback for SMT proofs
|
file |
diff |
annotate
|
Thu, 14 Feb 2013 22:49:22 +0100 |
smolkas |
renamed sledgehammer_shrink to sledgehammer_compress
|
file |
diff |
annotate
|
Thu, 31 Jan 2013 17:54:05 +0100 |
blanchet |
tuned data structure
|
file |
diff |
annotate
|
Thu, 31 Jan 2013 17:54:05 +0100 |
blanchet |
thread through fact triple component from which used facts come, for accurate index output
|
file |
diff |
annotate
|
Thu, 31 Jan 2013 17:54:05 +0100 |
blanchet |
thread fact triple (MeSh, MePo, MaSh) to allow different filters in different slices
|
file |
diff |
annotate
|
Thu, 31 Jan 2013 17:54:05 +0100 |
blanchet |
eliminated needless speed optimization -- and simplified code quite a bit
|
file |
diff |
annotate
|
Wed, 02 Jan 2013 10:54:36 +0100 |
blanchet |
use "Lazy" to simplify control flow a bit and guarantee single evaluation (at most)
|
file |
diff |
annotate
|
Wed, 02 Jan 2013 10:41:53 +0100 |
blanchet |
tuning
|
file |
diff |
annotate
|
Sat, 15 Dec 2012 19:57:12 +0100 |
blanchet |
thread no timeout properly
|
file |
diff |
annotate
|
Tue, 06 Nov 2012 15:15:33 +0100 |
blanchet |
renamed Sledgehammer option
|
file |
diff |
annotate
|
Thu, 18 Oct 2012 15:05:17 +0200 |
blanchet |
renamed Isar-proof related options + changed semantics of Isar shrinking
|
file |
diff |
annotate
|
Thu, 18 Oct 2012 13:19:44 +0200 |
blanchet |
refactor code
|
file |
diff |
annotate
|
Tue, 14 Aug 2012 14:07:53 +0200 |
blanchet |
warn users about unused "using" facts
|
file |
diff |
annotate
|
Tue, 14 Aug 2012 13:20:59 +0200 |
blanchet |
be less aggressive at kicking out chained facts
|
file |
diff |
annotate
|
Tue, 14 Aug 2012 12:49:42 +0200 |
blanchet |
consider removing chained facts last, so that they're more likely to be kept
|
file |
diff |
annotate
|
Fri, 20 Jul 2012 22:19:46 +0200 |
blanchet |
learn from SMT proofs when they can be minimized by Metis
|
file |
diff |
annotate
|
Fri, 20 Jul 2012 22:19:46 +0200 |
blanchet |
name tuning
|
file |
diff |
annotate
|
Fri, 20 Jul 2012 22:19:46 +0200 |
blanchet |
fixed various issues with MaSh's file handling + tune output + generate local facts again + handle nameless facts gracefully
|
file |
diff |
annotate
|
Fri, 20 Jul 2012 22:19:46 +0200 |
blanchet |
added "learn_from_atp" command to MaSh, for patient users
|
file |
diff |
annotate
|
Fri, 20 Jul 2012 22:19:46 +0200 |
blanchet |
learn on explicit "min" command but do the learning in a thread, since it may take a couple of seconds
|
file |
diff |
annotate
|
Wed, 18 Jul 2012 08:44:04 +0200 |
blanchet |
learn from minimized ATP proofs
|
file |
diff |
annotate
|
Wed, 18 Jul 2012 08:44:04 +0200 |
blanchet |
added option to control which fact filter is used
|
file |
diff |
annotate
|
Wed, 18 Jul 2012 08:44:03 +0200 |
blanchet |
renamed Sledgehammer options
|
file |
diff |
annotate
|
Wed, 18 Jul 2012 08:44:03 +0200 |
blanchet |
more code rationalization in relevance filter
|
file |
diff |
annotate
|
Wed, 11 Jul 2012 21:43:19 +0200 |
blanchet |
further ML structure split to permit finer-grained loading/reordering (problem to solve: MaSh needs most of Sledgehammer)
|
file |
diff |
annotate
|
Wed, 06 Jun 2012 10:35:05 +0200 |
blanchet |
avoid dumping definitions several times in LEO-II proofs
|
file |
diff |
annotate
|
Wed, 18 Apr 2012 10:53:28 +0200 |
blanchet |
get rid of minor optimization that caused strange problems and was hard to debug (and apparently saved less than 100 ms on a 30 s run)
|
file |
diff |
annotate
|
Sat, 04 Feb 2012 12:08:18 +0100 |
blanchet |
made option available to users (mostly for experiments)
|
file |
diff |
annotate
|
Wed, 01 Feb 2012 12:47:43 +0100 |
blanchet |
proper statuses for "fact_from_ref"
|
file |
diff |
annotate
|
Thu, 26 Jan 2012 20:49:54 +0100 |
blanchet |
separate orthogonal components
|
file |
diff |
annotate
|
Mon, 23 Jan 2012 17:40:32 +0100 |
blanchet |
renamed two files to make room for a new file
|
file |
diff |
annotate
|
Thu, 19 Jan 2012 21:37:12 +0100 |
blanchet |
renamed "sound" option to "strict"
|
file |
diff |
annotate
|
Thu, 01 Dec 2011 13:34:14 +0100 |
blanchet |
added "minimize" option for more control over automatic minimization
|
file |
diff |
annotate
|
Thu, 01 Dec 2011 13:34:13 +0100 |
blanchet |
renamed "slicing" to "slice"
|
file |
diff |
annotate
|
Fri, 18 Nov 2011 11:47:12 +0100 |
blanchet |
be more silent when auto minimizing
|
file |
diff |
annotate
|
Wed, 16 Nov 2011 16:35:19 +0100 |
blanchet |
thread in additional options to minimizer
|
file |
diff |
annotate
|
Wed, 16 Nov 2011 13:22:36 +0100 |
blanchet |
make metis reconstruction handling more flexible
|
file |
diff |
annotate
|
Wed, 16 Nov 2011 09:42:27 +0100 |
blanchet |
parse lambda translation option in Metis
|
file |
diff |
annotate
|
Sun, 06 Nov 2011 14:23:04 +0100 |
blanchet |
cascading timeouts in minimizer, part 2
|
file |
diff |
annotate
|