Mercurial Mercurial > repos > isabelle / file revisions
summary | shortlog | changelog | graph | tags | bookmarks | branches | file | revisions | annotate | diff | comparison | rss | help
(0) -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
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
Tue, 26 Jun 2012 11:14:40 +0200 blanchet renamed experimental option file | diff | annotate
Tue, 26 Jun 2012 11:14:39 +0200 blanchet started adding polymophic SPASS output file | diff | annotate
Tue, 26 Jun 2012 11:14:39 +0200 blanchet tuning file | diff | annotate
Mon, 18 Jun 2012 17:50:06 +0200 blanchet less confusing error message file | diff | annotate
Wed, 06 Jun 2012 10:35:05 +0200 blanchet killed most unsound encodings file | diff | annotate
Wed, 23 May 2012 21:19:48 +0200 blanchet tuned names file | diff | annotate
Wed, 23 May 2012 13:28:20 +0200 blanchet lower the monomorphization thresholds for less scalable provers file | diff | annotate
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" file | diff | annotate
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 file | diff | annotate
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 file | diff | annotate
Tue, 24 Apr 2012 20:55:09 +0200 blanchet made "split_last" more robust in the face of obscure low-level errors file | diff | annotate
Thu, 19 Apr 2012 17:49:08 +0200 blanchet true delayed evaluation of "SPASS_VERSION" environment variable 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
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 file | diff | annotate
Tue, 20 Mar 2012 00:44:30 +0100 blanchet continued implementation of term ordering attributes file | diff | annotate
Tue, 20 Mar 2012 00:44:30 +0100 blanchet implement term order attribute (for experiments) file | diff | annotate
Tue, 20 Mar 2012 00:44:30 +0100 blanchet internal renamings file | diff | annotate
Thu, 09 Feb 2012 12:57:59 +0100 blanchet added possibility of generating KBO weights to DFG problems file | diff | annotate
Sun, 05 Feb 2012 12:27:10 +0100 blanchet cleaned up new SPASS parsing file | diff | annotate
Sat, 04 Feb 2012 12:08:18 +0100 blanchet made option available to users (mostly for experiments) file | diff | annotate
Fri, 03 Feb 2012 18:00:55 +0100 blanchet optimization: slice caching in case two consecutive slices are nearly identical file | diff | annotate
Fri, 03 Feb 2012 18:00:55 +0100 blanchet try to pass fewer options to Metis 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, 19 Jan 2012 21:37:12 +0100 blanchet renamed "sound" option to "strict" file | diff | annotate
Thu, 19 Jan 2012 21:37:12 +0100 blanchet cleanly separate each Metis encoding file | diff | annotate
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 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
Sat, 19 Nov 2011 12:42:21 +0100 blanchet made SML/NJ happy file | diff | annotate
Fri, 18 Nov 2011 11:47:12 +0100 blanchet be more silent when auto minimizing file | diff | annotate
Fri, 18 Nov 2011 11:47:12 +0100 blanchet better threading of type encodings between Sledgehammer and "metis" file | diff | annotate
Fri, 18 Nov 2011 11:47:12 +0100 blanchet don't propagate user-set "type_enc" or "lam_trans" to Metis calls file | diff | annotate
Fri, 18 Nov 2011 11:47:12 +0100 blanchet don't needlessly pass "lam_lifted" option to "metis" call for SMT proof file | diff | annotate
Fri, 18 Nov 2011 11:47:12 +0100 blanchet quiet down SMT file | diff | annotate
Fri, 18 Nov 2011 11:47:12 +0100 blanchet more aggressive lambda hiding (if we anyway need to pass an option to Metis) file | diff | annotate
Fri, 18 Nov 2011 11:47:12 +0100 blanchet don't pass "lam_lifted" option to "metis" unless there's a good reason file | diff | annotate
Fri, 18 Nov 2011 11:47:12 +0100 blanchet no needless reconstructors file | diff | annotate
Fri, 18 Nov 2011 11:47:12 +0100 blanchet removed more clutter file | diff | annotate
Fri, 18 Nov 2011 11:47:12 +0100 blanchet removed needless baggage file | diff | annotate
Wed, 16 Nov 2011 17:06:14 +0100 blanchet give each time slice its own lambda translation 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
Tue, 15 Nov 2011 22:13:39 +0100 blanchet started implementing lambda-lifting in Metis file | diff | annotate
less more (0) -100 -60 tip
isabelle