src/HOL/Tools/Sledgehammer/sledgehammer.ML
Wed, 21 May 2014 14:09:42 +0200 blanchet avoid markup-generating @{make_string}
Thu, 27 Mar 2014 17:12:40 +0100 wenzelm clarified Isabelle/ML bootstrap, such that Execution does not require ML_Compiler;
Thu, 13 Feb 2014 13:16:17 +0100 blanchet avoid changing the state's context -- this results in transfer problems later with SMT, and hence preplay tactic failures
Mon, 03 Feb 2014 16:53:58 +0100 blanchet renamed ML file
Mon, 03 Feb 2014 15:33:18 +0100 blanchet tuning
Fri, 31 Jan 2014 16:10:39 +0100 blanchet tuning
Fri, 31 Jan 2014 10:23:32 +0100 blanchet renamed many Sledgehammer ML files to clarify structure
Tue, 07 Dec 2010 16:27:07 +0100 blanchet pass constant arguments to the built-in check function, cf. d2b1fc1b8e19
Tue, 07 Dec 2010 14:53:12 +0100 boehmes centralized handling of built-in types and constants;
Mon, 06 Dec 2010 11:41:24 +0100 blanchet handle "max_relevant" uniformly
Mon, 06 Dec 2010 11:26:17 +0100 blanchet honor the default max relevant facts setting from the SMT solvers in Sledgehammer
Mon, 06 Dec 2010 10:31:29 +0100 blanchet trust SMT filter's timeout -- nested timeouts seem to be at the origin of spontaneous Interrupt exceptions in some cases
Mon, 06 Dec 2010 10:23:31 +0100 blanchet reraise interrupt exceptions
Fri, 03 Dec 2010 18:29:14 +0100 blanchet replace "smt" prover with specific SMT solvers, e.g. "z3" -- whatever the SMT module gives us
Fri, 26 Nov 2010 22:22:07 +0100 blanchet put facts found by SMT solver in alphabetical order and omit chained facts, as was done already for ATP proofs
Fri, 26 Nov 2010 09:15:49 +0100 blanchet adjust Sledgehammer/SMT fudge factor
Thu, 25 Nov 2010 14:58:50 +0100 blanchet cosmetics
Thu, 25 Nov 2010 13:26:12 +0100 blanchet set Metis option on correct context, lest it be ignored
Thu, 25 Nov 2010 12:11:12 +0100 blanchet make "debug" mode of Sledgehammer/SMT more liberal
Wed, 24 Nov 2010 16:15:15 +0100 blanchet more precise error handling in Sledgehammer/SMT for Z3 and remote SMT provers
Tue, 23 Nov 2010 22:37:16 +0100 blanchet more precise error handling for Z3;
Tue, 23 Nov 2010 21:54:03 +0100 blanchet use "Thm.transfer" in Sledgehammer to prevent theory merger issues in "SMT_Solver.smt_filter" later on
Tue, 23 Nov 2010 18:28:09 +0100 blanchet try Metis to reconstruct SMT proofs, to increase success rate and reduce dependency on (often remote) SMT solvers or certificates
Sat, 20 Nov 2010 00:53:26 +0100 wenzelm renamed raw "explode" function to "raw_explode" to emphasize its meaning;
Mon, 15 Nov 2010 22:24:08 +0100 boehmes merged
Mon, 15 Nov 2010 22:23:28 +0100 boehmes renamed SMT failure: Abnormal_Termination is indeed more appropriate than Solver_Crashed
Mon, 15 Nov 2010 22:08:01 +0100 blanchet better error message
Mon, 15 Nov 2010 21:08:48 +0100 blanchet better error message
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)
less more (0) -100 -60 tip