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
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
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
less more (0) -300 -100 -60 tip
isabelle