src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML
Tue, 10 Sep 2013 15:56:51 +0200 blanchet don't be so verbose about SMT solver failures
Mon, 09 Sep 2013 23:54:59 +0200 blanchet since "full_proofs" can influence the proof search significantly (e.g. by disabling splitting for SPASS), it shouldn't be affected by the "debug" flag in the interest of minimizing confusion
Mon, 09 Sep 2013 15:22:04 +0200 blanchet limit the number of instances of a single theorem
Mon, 09 Sep 2013 15:22:04 +0200 blanchet use new monomorphizer in Sledgehammer
Thu, 22 Aug 2013 08:42:27 +0200 blanchet tuning
Sat, 17 Aug 2013 19:13:28 +0200 wenzelm sledgehammer sendback always uses Markup.padding_command: sensible default for most practical applications -- old-style in-line replacement is superseded by auto mode or panel;
Sat, 17 Aug 2013 11:34:50 +0200 wenzelm more explicit sendback propertries based on mode;
Tue, 13 Aug 2013 11:34:56 +0200 blanchet added flag for jEdit/PIDE asynchronous mode
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")
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;
Fri, 12 Jul 2013 22:41:25 +0200 smolkas added sledgehammer parameters isar_try0 and isar_minimize and their negative aliases
Tue, 09 Jul 2013 18:45:06 +0200 smolkas completely rewrote SH compress; added two parameters for experimentation/fine grained control
Tue, 09 Jul 2013 18:44:59 +0200 smolkas moved code -> easier debugging
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])
Sun, 26 May 2013 12:56:37 +0200 blanchet handle lambda-lifted problems in Isar construction code
Fri, 24 May 2013 16:43:37 +0200 blanchet improved handling of free variables' types in Isar proofs
Thu, 16 May 2013 14:58:30 +0200 blanchet correctly 'repair' the monomorphization context for SMT solvers from Sledgehammer
Thu, 16 May 2013 13:34:13 +0200 blanchet tuning -- renamed '_from_' to '_of_' in Sledgehammer
Wed, 15 May 2013 17:43:42 +0200 blanchet renamed Sledgehammer functions with 'for' in their names to 'of'
Mon, 06 May 2013 11:03:08 +0200 smolkas added preplay tracing
Thu, 28 Mar 2013 23:44:41 +0100 boehmes new, simpler implementation of monomorphization;
Thu, 21 Feb 2013 16:36:19 +0100 blanchet tuned misleading message
Thu, 21 Feb 2013 12:22:26 +0100 blanchet generate Isar proof if Metis appears to be too slow
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
Wed, 20 Feb 2013 14:10:51 +0100 blanchet minimize SMT proofs with E if Isar proofs are desired and Metis managed to preplay
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
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
Mon, 18 Feb 2013 18:34:55 +0100 blanchet implement (more) accurate computation of parents
Thu, 14 Feb 2013 22:49:22 +0100 smolkas renamed sledgehammer_shrink to sledgehammer_compress
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
Thu, 31 Jan 2013 17:54:05 +0100 blanchet also have SMT solvers alternate fact filter
Thu, 31 Jan 2013 17:54:05 +0100 blanchet use the right filter in each slice
Thu, 31 Jan 2013 17:54:05 +0100 blanchet store fact filter along with ATP slice
Thu, 31 Jan 2013 17:54:05 +0100 blanchet tuned data structure
Thu, 31 Jan 2013 17:54:05 +0100 blanchet thread through fact triple component from which used facts come, for accurate index output
Thu, 31 Jan 2013 17:54:05 +0100 blanchet thread fact triple (MeSh, MePo, MaSh) to allow different filters in different slices
Thu, 31 Jan 2013 17:54:05 +0100 blanchet eliminated needless speed optimization -- and simplified code quite a bit
Thu, 17 Jan 2013 14:01:45 +0100 blanchet added E-Par support
Mon, 07 Jan 2013 19:44:40 +0100 blanchet cleaner context threading
Wed, 02 Jan 2013 10:54:36 +0100 blanchet use "Lazy" to simplify control flow a bit and guarantee single evaluation (at most)
Wed, 02 Jan 2013 09:42:57 +0100 blanchet added 112 to list of known Z3 error codes
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)
Sat, 15 Dec 2012 19:57:12 +0100 blanchet thread no timeout properly
Wed, 12 Dec 2012 13:42:14 +0100 blanchet tuned debugging file names
Wed, 12 Dec 2012 03:47:02 +0100 blanchet made MaSh evaluation driver work with SMT solvers
Tue, 06 Nov 2012 15:15:33 +0100 blanchet renamed Sledgehammer option
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.)
Thu, 18 Oct 2012 15:41:15 +0200 blanchet tuned Isar output
Thu, 18 Oct 2012 15:05:17 +0200 blanchet renamed Isar-proof related options + changed semantics of Isar shrinking
Thu, 18 Oct 2012 13:19:44 +0200 blanchet refactor code
Tue, 16 Oct 2012 18:50:53 +0200 blanchet added proof minimization code from Steffen Smolka
Tue, 14 Aug 2012 15:26:45 +0200 blanchet fixed then-else confusion
Tue, 14 Aug 2012 15:18:11 +0200 blanchet improved set of reconstructor methods
Tue, 14 Aug 2012 14:07:53 +0200 blanchet warn users about unused "using" facts
Tue, 14 Aug 2012 13:20:59 +0200 blanchet be less aggressive at kicking out chained facts
Tue, 14 Aug 2012 12:54:26 +0200 blanchet recognize bus errors as crash
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
Fri, 03 Aug 2012 09:51:28 +0200 blanchet cleaner temporary file cleanup for MaSh, based on tried-and-trusted code
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)
Fri, 20 Jul 2012 22:19:46 +0200 blanchet added "learn_from_atp" command to MaSh, for patient users
less more (0) -300 -100 -60 tip