Mercurial Mercurial > wneuper > isa / file revisions
summary | shortlog | changelog | graph | tags | bookmarks | branches | file | revisions | annotate | diff | comparison | rss | help
(0) -100 -60 tip
src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML
Sat, 04 Feb 2012 12:08:18 +0100 made option available to users (mostly for experiments) file | diff | annotate
Fri, 03 Feb 2012 18:00:55 +0100 optimization: slice caching in case two consecutive slices are nearly identical file | diff | annotate
Fri, 03 Feb 2012 18:00:55 +0100 try to pass fewer options to Metis file | diff | annotate
Mon, 30 Jan 2012 17:15:59 +0100 rename lambda translation schemes file | diff | annotate
Thu, 26 Jan 2012 20:49:54 +0100 separate orthogonal components file | diff | annotate
Mon, 23 Jan 2012 17:40:32 +0100 renamed two files to make room for a new file file | diff | annotate
Thu, 19 Jan 2012 21:37:12 +0100 renamed "sound" option to "strict" file | diff | annotate
Thu, 19 Jan 2012 21:37:12 +0100 cleanly separate each Metis encoding file | diff | annotate
Wed, 07 Dec 2011 16:03:05 +0100 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 added "minimize" option for more control over automatic minimization file | diff | annotate
Thu, 01 Dec 2011 13:34:13 +0100 renamed "slicing" to "slice" file | diff | annotate
Sat, 19 Nov 2011 12:42:21 +0100 made SML/NJ happy file | diff | annotate
Fri, 18 Nov 2011 11:47:12 +0100 be more silent when auto minimizing file | diff | annotate
Fri, 18 Nov 2011 11:47:12 +0100 better threading of type encodings between Sledgehammer and "metis" file | diff | annotate
Fri, 18 Nov 2011 11:47:12 +0100 don't propagate user-set "type_enc" or "lam_trans" to Metis calls file | diff | annotate
Fri, 18 Nov 2011 11:47:12 +0100 don't needlessly pass "lam_lifted" option to "metis" call for SMT proof file | diff | annotate
Fri, 18 Nov 2011 11:47:12 +0100 quiet down SMT file | diff | annotate
Fri, 18 Nov 2011 11:47:12 +0100 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 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 no needless reconstructors file | diff | annotate
Fri, 18 Nov 2011 11:47:12 +0100 removed more clutter file | diff | annotate
Fri, 18 Nov 2011 11:47:12 +0100 removed needless baggage file | diff | annotate
Wed, 16 Nov 2011 17:06:14 +0100 give each time slice its own lambda translation file | diff | annotate
Wed, 16 Nov 2011 16:35:19 +0100 thread in additional options to minimizer file | diff | annotate
Wed, 16 Nov 2011 13:22:36 +0100 make metis reconstruction handling more flexible file | diff | annotate
Wed, 16 Nov 2011 09:42:27 +0100 parse lambda translation option in Metis file | diff | annotate
Tue, 15 Nov 2011 22:15:51 +0100 rename configuration option to more reasonable length file | diff | annotate
Tue, 15 Nov 2011 22:13:39 +0100 started implementing lambda-lifting in Metis file | diff | annotate
Sun, 06 Nov 2011 22:18:54 +0100 more millisecond cleanup file | diff | annotate
Sun, 06 Nov 2011 22:18:54 +0100 try "smt" as a fallback for ATPs if "metis" fails/times out file | diff | annotate
Sun, 06 Nov 2011 22:18:54 +0100 more detailed preplay output file | diff | annotate
Sun, 06 Nov 2011 22:18:54 +0100 tuning file | diff | annotate
Sun, 06 Nov 2011 13:57:17 +0100 use "Time.time" rather than milliseconds internally file | diff | annotate
Sun, 06 Nov 2011 13:46:26 +0100 tune: no need for option file | diff | annotate
Sat, 29 Oct 2011 13:15:58 +0200 added DFG unsorted support (like in the old days) file | diff | annotate
Sat, 29 Oct 2011 13:15:58 +0200 added sorted DFG output for coming version of SPASS file | diff | annotate
Sat, 29 Oct 2011 13:15:58 +0200 check "sound" flag before doing something unsound... file | diff | annotate
Tue, 13 Sep 2011 11:24:58 +0200 simplified unsound proof detection by removing impossible case file | diff | annotate
Sat, 10 Sep 2011 00:44:25 +0200 continue with minimization in debug mode in spite of unsoundness file | diff | annotate
Fri, 02 Sep 2011 14:43:20 +0200 renamed "Metis_Tactics" to "Metis_Tactic", now that there is only one Metis tactic ("metisFT" is legacy) file | diff | annotate
Fri, 02 Sep 2011 14:43:20 +0200 fewer TPTP important messages file | diff | annotate
Thu, 01 Sep 2011 13:18:27 +0200 always measure time for ATPs -- auto minimization relies on it file | diff | annotate
Thu, 01 Sep 2011 13:18:27 +0200 make "sound" sound and "unsound" more sound, based on evaluation file | diff | annotate
Tue, 30 Aug 2011 16:25:10 +0200 fixed just introduced silly bug file | diff | annotate
Tue, 30 Aug 2011 16:11:42 +0200 tuning file | diff | annotate
Tue, 30 Aug 2011 16:07:45 +0200 flip logic of boolean option so it's off by default file | diff | annotate
Tue, 30 Aug 2011 14:12:55 +0200 improved handling of induction rules in Sledgehammer file | diff | annotate
Tue, 30 Aug 2011 14:12:55 +0200 added generation of induction rules file | diff | annotate
Fri, 26 Aug 2011 10:25:13 +0200 added a component in generated file names reflecting whether the minimizer is used -- needed for evaluation to keep these files separated from the main problem files file | diff | annotate
Tue, 23 Aug 2011 16:07:01 +0200 exploit TFF format in Z3 used as ATP, and renamed it "z3_tptp" file | diff | annotate
Tue, 23 Aug 2011 14:44:19 +0200 added formats to the slice and use TFF for remote Vampire file | diff | annotate
Mon, 22 Aug 2011 15:02:45 +0200 cleaner handling of polymorphic monotonicity inference file | diff | annotate
Mon, 22 Aug 2011 15:02:45 +0200 added option to control soundness of encodings more precisely, for evaluation purposes file | diff | annotate
Mon, 22 Aug 2011 15:02:45 +0200 make sound mode more sound (and clean up code) file | diff | annotate
Tue, 09 Aug 2011 09:05:22 +0200 move lambda-lifting code to ATP encoding, so it can be used by Metis file | diff | annotate
Thu, 28 Jul 2011 11:43:45 +0200 tuning file | diff | annotate
Tue, 26 Jul 2011 14:53:00 +0200 remove spurious message file | diff | annotate
Mon, 25 Jul 2011 14:10:12 +0200 introduced hybrid lambda translation file | diff | annotate
Mon, 25 Jul 2011 14:10:12 +0200 avoid needless type args for lifted-lambdas file | diff | annotate
Thu, 21 Jul 2011 21:29:10 +0200 make "concealed" lambda translation sound file | diff | annotate
(0) -100 -60 tip
wneuper/isa