src/HOL/Tools/Sledgehammer/sledgehammer.ML
Mon, 15 Nov 2010 18:58:30 +0100 blanchet cosmetics
Mon, 15 Nov 2010 18:56:31 +0100 blanchet interpret SMT_Failure.Solver_Crashed correctly
Mon, 15 Nov 2010 18:56:29 +0100 blanchet pick up SMT solver crashes and report them to the user/Mirabelle if desired
Wed, 10 Nov 2010 09:03:07 +0100 blanchet make SML/NJ happy
Mon, 08 Nov 2010 14:33:30 +0100 blanchet reduce the number of monomorphization iterations from 10 (the default) to 4, in the interest of faster SMT solving
Mon, 08 Nov 2010 13:53:18 +0100 blanchet compile -- 7550b2cba1cb broke the build
Mon, 08 Nov 2010 12:13:44 +0100 boehmes better modularization: moved SMT configuration options and diagnostics as well as SMT failure and exception into separate structures (both of which are loaded first and consequently are available to other SMT structures)
Mon, 08 Nov 2010 02:33:48 +0100 blanchet make sure the SMT solver runs several iterations by lowering the timeout at each iteration -- yields better results in practice
Sun, 07 Nov 2010 18:19:04 +0100 blanchet always use a hard timeout in Mirabelle
Sun, 07 Nov 2010 18:03:24 +0100 blanchet don't pass too many facts on the first iteration of the SMT solver
Sun, 07 Nov 2010 18:02:02 +0100 blanchet catch TimeOut exception
Sun, 07 Nov 2010 17:56:07 +0100 blanchet ensure the SMT solver respects the timeout -- Mirabelle revealed cases where "smt_filter" apparently never returns
Sun, 07 Nov 2010 17:51:25 +0100 blanchet if SMT used as a filter in a loop fails at each iteration, returns the first error, not the last, since it is more informative -- the first error typically says "out of memory", whereas the last might well be "the SMT problem is unprovable", which should be no surprise if too many facts were removed
Sat, 06 Nov 2010 10:25:08 +0100 blanchet invoke SMT solver in a loop, with fewer and fewer facts, in case of error
Thu, 04 Nov 2010 14:59:44 +0100 blanchet cosmetics
Thu, 04 Nov 2010 14:59:44 +0100 blanchet use the SMT integration's official list of built-ins
Wed, 03 Nov 2010 22:26:53 +0100 blanchet standardize on seconds for Nitpick and Sledgehammer timeouts
Thu, 28 Oct 2010 09:36:51 +0200 blanchet clear identification;
Tue, 26 Oct 2010 21:51:04 +0200 blanchet adapted SMT solver error handling to reflect latest changes in "SMT_Solver"
Tue, 26 Oct 2010 21:43:50 +0200 blanchet better list of irrelevant SMT constants
Tue, 26 Oct 2010 21:34:01 +0200 blanchet if "debug" is on, print list of relevant facts (poweruser request);
Tue, 26 Oct 2010 21:01:28 +0200 blanchet standardize on "fact" terminology (vs. "axiom" or "theorem") in Sledgehammer -- but keep "Axiom" in the lower-level "ATP_Problem" module
Tue, 26 Oct 2010 20:09:38 +0200 blanchet merge
Tue, 26 Oct 2010 16:56:54 +0200 blanchet remove needless context argument;
Tue, 26 Oct 2010 17:35:51 +0200 boehmes capture out-of-memory warnings of Z3 and turn them into proper exceptions; be more precise about SMT solver run-time: return NONE instead of ~1
Tue, 26 Oct 2010 14:48:55 +0200 blanchet tuning
Tue, 26 Oct 2010 13:50:57 +0200 blanchet proper error handling for SMT solvers in Sledgehammer
Tue, 26 Oct 2010 13:16:43 +0200 blanchet integrated "smt" proof method with Sledgehammer
Mon, 25 Oct 2010 21:06:56 +0200 wenzelm renamed Output.priority to Output.urgent_message to emphasize its special role more clearly;
Fri, 22 Oct 2010 18:31:45 +0200 blanchet tuning
Fri, 22 Oct 2010 16:11:43 +0200 blanchet more robust handling of "remote_" vs. non-"remote_" provers
Fri, 22 Oct 2010 15:02:27 +0200 blanchet generalized the relevance filter so that it takes the list of "irrelevant constants" as argument (since the ATP and SMT preprocessing are different)
Fri, 22 Oct 2010 14:47:43 +0200 blanchet replaced references with proper record that's threaded through
Fri, 22 Oct 2010 14:10:32 +0200 blanchet fixed signature of "is_smt_solver_installed";
Fri, 22 Oct 2010 13:57:54 +0200 blanchet renamed modules
Fri, 22 Oct 2010 13:48:21 +0200 blanchet remove more needless code ("run_smt_solvers");
Fri, 22 Oct 2010 12:15:31 +0200 blanchet got rid of duplicate functionality ("run_smt_solver_somehow");
Fri, 22 Oct 2010 11:58:33 +0200 blanchet bring ATPs and SMT solvers more in line with each other
Fri, 22 Oct 2010 11:11:34 +0200 blanchet make Sledgehammer minimizer fully work with SMT
Fri, 22 Oct 2010 09:50:18 +0200 blanchet generalization of the Sledgehammer minimizer, to make it possible to handle SMT solvers as well
Thu, 21 Oct 2010 16:25:40 +0200 blanchet first step in adding support for an SMT backend to Sledgehammer
Thu, 21 Oct 2010 14:55:09 +0200 blanchet use consistent terminology in Sledgehammer: "prover = ATP or SMT solver or ..."
Thu, 16 Sep 2010 16:12:02 +0200 blanchet rename "Metis_Clauses" to "Metis_Translate" for consistency with "Sledgehammer_Translate"
Thu, 16 Sep 2010 15:38:46 +0200 blanchet move SPASS's Flotter hack to "Sledgehammer_Reconstruct"
Thu, 16 Sep 2010 15:28:16 +0200 blanchet skip some "important" messages
Thu, 16 Sep 2010 15:16:08 +0200 blanchet refactoring: move ATP proof and error extraction code to "ATP_Proof" module
Thu, 16 Sep 2010 11:59:45 +0200 blanchet use the same TSTP/Vampire/SPASS parser for one-liners as for Isar proofs
Thu, 16 Sep 2010 11:12:08 +0200 blanchet factored out TSTP/SPASS/Vampire proof parsing;
Tue, 14 Sep 2010 23:01:29 +0200 blanchet finish support for E 1.2 proof reconstruction;
Tue, 14 Sep 2010 19:40:19 +0200 blanchet clarify message
Tue, 14 Sep 2010 19:38:44 +0200 blanchet use same hack as in "Async_Manager" to work around Proof General bug
Tue, 14 Sep 2010 16:34:26 +0200 blanchet handle relevance filter corner cases more gracefully;
Tue, 14 Sep 2010 15:39:57 +0200 blanchet Sledgehammer should be called in "prove" mode;
Mon, 13 Sep 2010 14:29:53 +0200 blanchet tuning
Sat, 11 Sep 2010 12:31:42 +0200 blanchet tuning
Sat, 11 Sep 2010 10:21:52 +0200 blanchet implemented Auto Sledgehammer
Thu, 09 Sep 2010 16:27:36 +0200 blanchet more precise error messages when Vampire is interrupted or SPASS runs into an internal bug
Thu, 09 Sep 2010 16:06:11 +0200 blanchet better error reporting when the Sledgehammer minimizer is interrupted
Wed, 08 Sep 2010 16:01:06 +0200 blanchet merge
Mon, 06 Sep 2010 16:50:29 +0200 blanchet use Future.fork rather than Thread.fork, so that the thread is part of the global thread management
less more (0) -100 -60 tip