src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML
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
Fri, 20 Jul 2012 22:19:45 +0200 blanchet use "eproof_ram" script if available (plug-in replacement for "eproof", but faster)
Wed, 18 Jul 2012 08:44:04 +0200 blanchet make the monomorphizer more predictable by making the cutoff independent on the number of facts
Wed, 18 Jul 2012 08:44:04 +0200 blanchet learn from minimized ATP proofs
Wed, 18 Jul 2012 08:44:04 +0200 blanchet use async manager to manage MaSh learners to make sure they get killed cleanly
Wed, 18 Jul 2012 08:44:04 +0200 blanchet added option to control which fact filter is used
Wed, 18 Jul 2012 08:44:03 +0200 blanchet renamed Sledgehammer options
Wed, 18 Jul 2012 08:44:03 +0200 blanchet rationalize relevance filter, slowing moving code from Iter to MaSh
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)
Tue, 26 Jun 2012 11:14:40 +0200 blanchet renamed experimental option
Tue, 26 Jun 2012 11:14:39 +0200 blanchet started adding polymophic SPASS output
Tue, 26 Jun 2012 11:14:39 +0200 blanchet tuning
Mon, 18 Jun 2012 17:50:06 +0200 blanchet less confusing error message
Wed, 06 Jun 2012 10:35:05 +0200 blanchet killed most unsound encodings
Wed, 23 May 2012 21:19:48 +0200 blanchet tuned names
Wed, 23 May 2012 13:28:20 +0200 blanchet lower the monomorphization thresholds for less scalable provers
Mon, 21 May 2012 10:39:32 +0200 blanchet add an experimental "aggressive" mode to Sledgehammer, to experiment with more complete translations of higher-order features without breaking "metis"
Wed, 16 May 2012 18:16:51 +0200 blanchet lower skolem penalty to ensure that some useful facts with existentials, e.g. congruence of "setsum", eventually get picked up
Sun, 13 May 2012 16:31:01 +0200 blanchet get rid of "conj_sym_kind" -- most interesting provers now have built-in sorts, and for the others (e.g. E) "Hypothesis" isn't too bad a default
Tue, 24 Apr 2012 20:55:09 +0200 blanchet made "split_last" more robust in the face of obscure low-level errors
Thu, 19 Apr 2012 17:49:08 +0200 blanchet true delayed evaluation of "SPASS_VERSION" environment variable
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)
Tue, 20 Mar 2012 18:42:45 +0100 blanchet made "spass" a "metaprover" that uses either the new SPASS or the old SPASS, to preserve backward compatibility and prepare for the upcoming release
Tue, 20 Mar 2012 00:44:30 +0100 blanchet continued implementation of term ordering attributes
Tue, 20 Mar 2012 00:44:30 +0100 blanchet implement term order attribute (for experiments)
Tue, 20 Mar 2012 00:44:30 +0100 blanchet internal renamings
Thu, 09 Feb 2012 12:57:59 +0100 blanchet added possibility of generating KBO weights to DFG problems
Sun, 05 Feb 2012 12:27:10 +0100 blanchet cleaned up new SPASS parsing
Sat, 04 Feb 2012 12:08:18 +0100 blanchet made option available to users (mostly for experiments)
Fri, 03 Feb 2012 18:00:55 +0100 blanchet optimization: slice caching in case two consecutive slices are nearly identical
Fri, 03 Feb 2012 18:00:55 +0100 blanchet try to pass fewer options to Metis
Mon, 30 Jan 2012 17:15:59 +0100 blanchet rename lambda translation schemes
Thu, 26 Jan 2012 20:49:54 +0100 blanchet separate orthogonal components
Mon, 23 Jan 2012 17:40:32 +0100 blanchet renamed two files to make room for a new file
Thu, 19 Jan 2012 21:37:12 +0100 blanchet renamed "sound" option to "strict"
Thu, 19 Jan 2012 21:37:12 +0100 blanchet cleanly separate each Metis encoding
Wed, 07 Dec 2011 16:03:05 +0100 blanchet use same order of facts for preplay as for actual reconstruction -- Metis sometimes exhibits very different timings depending on the order of the facts
Thu, 01 Dec 2011 13:34:14 +0100 blanchet added "minimize" option for more control over automatic minimization
Thu, 01 Dec 2011 13:34:13 +0100 blanchet renamed "slicing" to "slice"
Sat, 19 Nov 2011 12:42:21 +0100 blanchet made SML/NJ happy
Fri, 18 Nov 2011 11:47:12 +0100 blanchet be more silent when auto minimizing
Fri, 18 Nov 2011 11:47:12 +0100 blanchet better threading of type encodings between Sledgehammer and "metis"
Fri, 18 Nov 2011 11:47:12 +0100 blanchet don't propagate user-set "type_enc" or "lam_trans" to Metis calls
Fri, 18 Nov 2011 11:47:12 +0100 blanchet don't needlessly pass "lam_lifted" option to "metis" call for SMT proof
Fri, 18 Nov 2011 11:47:12 +0100 blanchet quiet down SMT
Fri, 18 Nov 2011 11:47:12 +0100 blanchet more aggressive lambda hiding (if we anyway need to pass an option to Metis)
Fri, 18 Nov 2011 11:47:12 +0100 blanchet don't pass "lam_lifted" option to "metis" unless there's a good reason
Fri, 18 Nov 2011 11:47:12 +0100 blanchet no needless reconstructors
less more (0) -300 -100 -60 tip