Mercurial Mercurial > repos > isabelle / file revisions
summary | shortlog | changelog | graph | tags | bookmarks | branches | file | revisions | annotate | diff | comparison | rss | help
(0) -300 -100 -60 tip
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML
Mon, 29 Jul 2013 15:30:31 +0200 blanchet added support for E 1.8's internal proof objects (eliminating the need for "eproof_ram") file | diff | annotate
Thu, 18 Jul 2013 20:53:22 +0200 wenzelm explicit padding on command boundary for "auto" generated sendback -- do not replace the corresponding goal command, but append to it; 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
Tue, 28 May 2013 08:52:41 +0200 blanchet redid rac7830871177 to avoid duplicate fixed variable (e.g. lemma "P (a::nat)" proof - have "!!a::int. Q a" sledgehammer [e]) file | diff | annotate
Sun, 26 May 2013 12:56:37 +0200 blanchet handle lambda-lifted problems in Isar construction code file | diff | annotate
Fri, 24 May 2013 16:43:37 +0200 blanchet improved handling of free variables' types in Isar proofs file | diff | annotate
Thu, 16 May 2013 14:58:30 +0200 blanchet correctly 'repair' the monomorphization context for SMT solvers from Sledgehammer 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
Thu, 28 Mar 2013 23:44:41 +0100 boehmes new, simpler implementation of monomorphization; file | diff | annotate
Thu, 21 Feb 2013 16:36:19 +0100 blanchet tuned misleading message file | diff | annotate
Thu, 21 Feb 2013 12:22:26 +0100 blanchet generate Isar proof if Metis appears to be too slow file | diff | annotate
Wed, 20 Feb 2013 15:12:38 +0100 blanchet don't pass chained facts directly to SMT solvers -- this breaks various invariants and is never necessary 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 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 15:37:42 +0100 blanchet interpret "max_facts" argument in a slice-dependent fashion, instead of forcing the same number of facts to all slices file | diff | annotate
Mon, 18 Feb 2013 18:34:55 +0100 blanchet implement (more) accurate computation of parents file | diff | annotate
Thu, 14 Feb 2013 22:49:22 +0100 smolkas renamed sledgehammer_shrink to sledgehammer_compress file | diff | annotate
Thu, 07 Feb 2013 14:05:32 +0100 blanchet distinguish MeSh and smart -- with smart, allow combinations of MaSh, MeSh, and MePo in different slices -- and use MaSh also with SMT solvers, based on evaluation file | diff | annotate
Thu, 31 Jan 2013 17:54:05 +0100 blanchet also have SMT solvers alternate fact filter file | diff | annotate
Thu, 31 Jan 2013 17:54:05 +0100 blanchet use the right filter in each slice file | diff | annotate
Thu, 31 Jan 2013 17:54:05 +0100 blanchet store fact filter along with ATP slice 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
Thu, 17 Jan 2013 14:01:45 +0100 blanchet added E-Par support file | diff | annotate
Mon, 07 Jan 2013 19:44:40 +0100 blanchet cleaner context threading 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 09:42:57 +0100 blanchet added 112 to list of known Z3 error codes file | diff | annotate
Sat, 15 Dec 2012 21:26:10 +0100 blanchet avoid creating nested threads for MaSh -- this seems to cause thread creation failures for machines with dozens of cores (unclear yet if that's really the issue) file | diff | annotate
Sat, 15 Dec 2012 19:57:12 +0100 blanchet thread no timeout properly file | diff | annotate
Wed, 12 Dec 2012 13:42:14 +0100 blanchet tuned debugging file names file | diff | annotate
Wed, 12 Dec 2012 03:47:02 +0100 blanchet made MaSh evaluation driver work with SMT solvers file | diff | annotate
Tue, 06 Nov 2012 15:15:33 +0100 blanchet renamed Sledgehammer option file | diff | annotate
Fri, 02 Nov 2012 16:16:48 +0100 blanchet several improvements to Isar proof reconstruction, by Steffen Smolka (step merging in case splits, time measurements, etc.) file | diff | annotate
Thu, 18 Oct 2012 15:41:15 +0200 blanchet tuned Isar output 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, 16 Oct 2012 18:50:53 +0200 blanchet added proof minimization code from Steffen Smolka file | diff | annotate
Tue, 14 Aug 2012 15:26:45 +0200 blanchet fixed then-else confusion file | diff | annotate
Tue, 14 Aug 2012 15:18:11 +0200 blanchet improved set of reconstructor methods 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:54:26 +0200 blanchet recognize bus errors as crash file | diff | annotate
Tue, 07 Aug 2012 14:29:18 +0200 blanchet stop distinguishing between complete and incomplete slices, since this is very fragile and has hardly any useful semantics to users file | diff | annotate
Fri, 03 Aug 2012 09:51:28 +0200 blanchet cleaner temporary file cleanup for MaSh, based on tried-and-trusted code file | diff | annotate
Thu, 26 Jul 2012 10:48:03 +0200 blanchet Sledgehammer already has its own ways of reporting and recovering from crashes in external provers -- no need to additionally print scores of warnings (cf. 4b0daca2bf88) 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:45 +0200 blanchet use "eproof_ram" script if available (plug-in replacement for "eproof", but faster) file | diff | annotate
Wed, 18 Jul 2012 08:44:04 +0200 blanchet make the monomorphizer more predictable by making the cutoff independent on the number of facts 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 use async manager to manage MaSh learners to make sure they get killed cleanly 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 rationalize relevance filter, slowing moving code from Iter to MaSh 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
less more (0) -300 -100 -60 tip
isabelle