| Wed, 07 Mar 2012 13:00:30 +0000 |
sultana |
added max_new_mono_instances, max_mono_iters, to Mirabelle-Sledgehammer; changed sh_minimize to avoid setting Mirabelle-level defaults;
|
file |
diff |
annotate
|
| Wed, 07 Mar 2012 13:00:30 +0000 |
sultana |
added sh_minimize and preplay_timeout options to Mirabelle's Sledgehammer action;
|
file |
diff |
annotate
|
| Fri, 24 Feb 2012 11:23:34 +0100 |
blanchet |
renamed 'try_methods' to 'try0'
|
file |
diff |
annotate
|
| Mon, 06 Feb 2012 23:01:01 +0100 |
blanchet |
renamed type encoding
|
file |
diff |
annotate
|
| Sun, 05 Feb 2012 12:27:10 +0100 |
blanchet |
tuning
|
file |
diff |
annotate
|
| Sat, 04 Feb 2012 17:01:25 +0100 |
blanchet |
added option to Mirabelle/Sledgehammer
|
file |
diff |
annotate
|
| Tue, 31 Jan 2012 18:46:31 +0100 |
blanchet |
renamed Sledgehammer option
|
file |
diff |
annotate
|
| Mon, 30 Jan 2012 17:15:59 +0100 |
blanchet |
rename lambda translation schemes
|
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, 01 Dec 2011 13:34:13 +0100 |
blanchet |
renamed "slicing" to "slice"
|
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
|
| Tue, 15 Nov 2011 22:15:51 +0100 |
blanchet |
rename configuration option to more reasonable length
|
file |
diff |
annotate
|
| Sun, 06 Nov 2011 14:05:57 +0100 |
blanchet |
tuning
|
file |
diff |
annotate
|
| Wed, 07 Sep 2011 09:10:41 +0200 |
blanchet |
rationalize uniform encodings
|
file |
diff |
annotate
|
| Fri, 02 Sep 2011 14:43:20 +0200 |
blanchet |
renamed "Metis_Tactics" to "Metis_Tactic", now that there is only one Metis tactic ("metisFT" is legacy)
|
file |
diff |
annotate
|
| Thu, 01 Sep 2011 13:18:27 +0200 |
blanchet |
always measure time for ATPs -- auto minimization relies on it
|
file |
diff |
annotate
|
| Thu, 01 Sep 2011 13:18:27 +0200 |
blanchet |
make "sound" sound and "unsound" more sound, based on evaluation
|
file |
diff |
annotate
|
| Wed, 31 Aug 2011 11:52:03 +0200 |
blanchet |
more tuning
|
file |
diff |
annotate
|
| Tue, 30 Aug 2011 16:07:45 +0200 |
blanchet |
extended simple types with polymorphism -- the implementation still needs some work though
|
file |
diff |
annotate
|
| Tue, 30 Aug 2011 14:12:55 +0200 |
nik |
improved handling of induction rules in Sledgehammer
|
file |
diff |
annotate
|
| Sun, 28 Aug 2011 13:13:27 +0200 |
blanchet |
split timeout among ATPs in and add Metis to the mix as backup
|
file |
diff |
annotate
|
| Sat, 27 Aug 2011 11:22:21 +0200 |
blanchet |
beef up sledgehammer_tac in Mirabelle some more
|
file |
diff |
annotate
|
| Thu, 25 Aug 2011 00:00:36 +0200 |
blanchet |
include chained facts for minimizer, otherwise it won't work
|
file |
diff |
annotate
|
| Wed, 24 Aug 2011 11:17:33 +0200 |
blanchet |
more reliable "sledgehammer\_tac" reconstruction, by avoiding "insert_tac"
|
file |
diff |
annotate
|
| Wed, 24 Aug 2011 11:17:33 +0200 |
blanchet |
specify timeout for "sledgehammer_tac"
|
file |
diff |
annotate
|
| Tue, 23 Aug 2011 22:44:08 +0200 |
blanchet |
don't select facts when using sledgehammer_tac for reconstruction
|
file |
diff |
annotate
|
| Tue, 23 Aug 2011 20:35:41 +0200 |
blanchet |
don't perform a triviality check if the goal is skipped anyway
|
file |
diff |
annotate
|