Mercurial Mercurial > repos > isabelle / file revisions
summary | shortlog | changelog | graph | tags | bookmarks | branches | file | revisions | annotate | diff | comparison | rss | help
(0) tip
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/HOL/Tools/Sledgehammer/sledgehammer_run.ML
Tue, 24 May 2011 00:01:33 +0200 blanchet tuning -- the "appropriate" terminology is inspired from TPTP file | diff | annotate
Sun, 22 May 2011 14:51:42 +0200 blanchet added message when Waldmeister isn't run file | diff | annotate
Sun, 22 May 2011 14:51:42 +0200 blanchet improved Waldmeister support -- even run it by default on unit equational goals file | diff | annotate
Thu, 19 May 2011 10:24:13 +0200 blanchet distinguish between a soft timeout (30 s by defalt) and a hard timeout (60 s), to let minimization-based provers (such as CVC3, Yices, and occasionally the other provers) do their job file | diff | annotate
Tue, 03 May 2011 00:10:22 +0200 blanchet replaced some Unsynchronized.refs with Config.Ts file | diff | annotate
Mon, 02 May 2011 22:52:15 +0200 blanchet tuning file | diff | annotate
Mon, 02 May 2011 22:52:15 +0200 blanchet have each ATP filter out dangerous facts for themselves, based on their type system file | diff | annotate
Mon, 02 May 2011 14:40:57 +0200 blanchet use strings to encode type systems in ATP module, to reduce the amount of out-of-place information and also to make it easier to print the type system used file | diff | annotate
Sun, 01 May 2011 18:37:25 +0200 blanchet restructured type systems some more -- the old naming schemes had "argshg diff |less" and "tagshg diff |less" as equivalent and didn't support a monomorphic version of "tags" file | diff | annotate
Sun, 01 May 2011 18:37:25 +0200 blanchet implement the new ATP type system in Sledgehammer file | diff | annotate
Sun, 01 May 2011 18:37:24 +0200 blanchet reimplemented the hAPP introduction code so that it's done earlier, when the types are still available file | diff | annotate
Sun, 01 May 2011 18:37:24 +0200 blanchet perform constant mangling and/or removal of its type args in an earlier phase, so that the rest of the code doesn't need to worry about it file | diff | annotate
Thu, 21 Apr 2011 22:18:28 +0200 blanchet detect some unsound proofs before showing them to the user file | diff | annotate
Thu, 21 Apr 2011 18:39:22 +0200 blanchet cleanup: get rid of "may_slice" arguments without changing semantics file | diff | annotate
Thu, 21 Apr 2011 18:39:22 +0200 blanchet implemented general slicing for ATPs, especially E 1.2w and above file | diff | annotate
Sat, 16 Apr 2011 16:15:37 +0200 wenzelm modernized structure Proof_Context; file | diff | annotate
Thu, 31 Mar 2011 11:16:52 +0200 blanchet added monomorphization option to Sledgehammer ATPs -- this looks promising but is still off by default file | diff | annotate
Thu, 17 Mar 2011 11:18:31 +0100 blanchet add option to function to keep trivial ATP formulas, needed for some experiments file | diff | annotate
Mon, 21 Feb 2011 10:29:00 +0100 blanchet added a timeout around SMT preprocessing (notably monomorphization) file | diff | annotate
Fri, 18 Feb 2011 16:30:44 +0100 blanchet gracious timeout in "blocking" mode file | diff | annotate
Thu, 10 Feb 2011 16:15:43 +0100 blanchet run all provers in blocking mode, even if a proof was already found -- this behavior is less confusing to the user file | diff | annotate
Wed, 09 Feb 2011 17:18:58 +0100 blanchet tuning file | diff | annotate
Wed, 09 Feb 2011 17:18:58 +0100 blanchet automatically minimize Z3-as-an-ATP proofs (cf. CVC3 and Yices) file | diff | annotate
Wed, 09 Feb 2011 17:18:58 +0100 blanchet renamed field file | diff | annotate
Tue, 08 Feb 2011 16:10:10 +0100 blanchet available_provers ~> supported_provers (for clarity) file | diff | annotate
Thu, 06 Jan 2011 17:51:56 +0100 boehmes differentiate between local and remote SMT solvers (e.g., "z3" vs. "remote_z3"); file | diff | annotate
Tue, 21 Dec 2010 03:56:51 +0100 blanchet added "smt_triggers" option to experiment with triggers in Sledgehammer; file | diff | annotate
Mon, 20 Dec 2010 14:10:40 +0100 blanchet make exceptions more transparent in "debug" mode file | diff | annotate
Sat, 18 Dec 2010 14:02:14 +0100 blanchet tuning file | diff | annotate
Sat, 18 Dec 2010 13:43:46 +0100 blanchet lower threshold where the binary algorithm kick in and use the same value for automatic minimization file | diff | annotate
Sat, 18 Dec 2010 13:34:32 +0100 blanchet let each prover minimizes its own stuff (rather than taking the first prover of the list to minimize every prover's stuff) file | diff | annotate
Sat, 18 Dec 2010 12:53:56 +0100 blanchet renamed function to run prover with minimizer and changed signature to clarify its semantics and make it a drop in replacement for "get_prover" file | diff | annotate
Sat, 18 Dec 2010 12:46:58 +0100 blanchet factored out running a prover with (optionally) an implicit minimizer phrase file | diff | annotate
Fri, 17 Dec 2010 23:09:53 +0100 blanchet remove option that doesn't work in Mirabelle anyway (Mirabelle uses Sledgehammer_Provers, not Sledgehammer_Run) file | diff | annotate
Fri, 17 Dec 2010 21:31:19 +0100 blanchet put the SMT weights back where they belong, so that they're also used by Mirabelle file | diff | annotate
Fri, 17 Dec 2010 18:23:56 +0100 blanchet added debugging option to find out how good the relevance filter was at identifying relevant facts file | diff | annotate
Fri, 17 Dec 2010 16:55:27 +0100 blanchet export experimental options file | diff | annotate
Fri, 17 Dec 2010 15:30:43 +0100 blanchet run the SMT relevance filter only once, then run the normalization/monomorphization code once _per class_ of SMT solvers file | diff | annotate
Thu, 16 Dec 2010 15:12:17 +0100 blanchet make "debug" imply "blocking", since in blocking mode the exceptions flow through and are more instructive file | diff | annotate
Wed, 15 Dec 2010 19:41:24 +0100 blanchet make sure errors generated in a thread don't vanish in cyberspace (e.g., when invoking Sledgehammer with unknown facts) file | diff | annotate
Wed, 15 Dec 2010 18:10:32 +0100 blanchet facilitate debugging file | diff | annotate
Wed, 15 Dec 2010 11:26:28 +0100 blanchet weaken the "expect" flag so that it doesn't trigger errors if a prover is not installed file | diff | annotate
Wed, 15 Dec 2010 11:26:28 +0100 blanchet implemented partially-typed "tags" type encoding file | diff | annotate
Wed, 08 Dec 2010 22:17:53 +0100 blanchet implicitly call the minimizer for SMT solvers that don't return an unsat core file | diff | annotate
Wed, 08 Dec 2010 22:17:52 +0100 blanchet renamings file | diff | annotate
Wed, 08 Dec 2010 22:17:52 +0100 blanchet moved function to later module file | diff | annotate
Wed, 08 Dec 2010 22:17:52 +0100 blanchet clarified terminology file | diff | annotate
Wed, 08 Dec 2010 22:17:52 +0100 blanchet split "Sledgehammer" module into two parts, to resolve forthcoming dependency problems file | diff | annotate | base
less more (0) tip
isabelle