src/HOL/Tools/Sledgehammer/sledgehammer.ML
2014-05-21 blanchet 2014-05-21 avoid markup-generating @{make_string}
2014-03-27 wenzelm 2014-03-27 clarified Isabelle/ML bootstrap, such that Execution does not require ML_Compiler;
2014-02-13 blanchet 2014-02-13 avoid changing the state's context -- this results in transfer problems later with SMT, and hence preplay tactic failures
2014-02-03 blanchet 2014-02-03 renamed ML file
2014-02-03 blanchet 2014-02-03 tuning
2014-01-31 blanchet 2014-01-31 tuning
2014-01-31 blanchet 2014-01-31 renamed many Sledgehammer ML files to clarify structure
2010-12-07 blanchet 2010-12-07 pass constant arguments to the built-in check function, cf. d2b1fc1b8e19
2010-12-07 boehmes 2010-12-07 centralized handling of built-in types and constants; also store types and constants which are rewritten during preprocessing; interfaces are identified by classes (supporting inheritance, at least on the level of built-in symbols); removed term_eq in favor of type replacements: term-level occurrences of type bool are replaced by type term_bool (only for the translation)
2010-12-06 blanchet 2010-12-06 handle "max_relevant" uniformly
2010-12-06 blanchet 2010-12-06 honor the default max relevant facts setting from the SMT solvers in Sledgehammer
2010-12-06 blanchet 2010-12-06 trust SMT filter's timeout -- nested timeouts seem to be at the origin of spontaneous Interrupt exceptions in some cases
2010-12-06 blanchet 2010-12-06 reraise interrupt exceptions
2010-12-03 blanchet 2010-12-03 replace "smt" prover with specific SMT solvers, e.g. "z3" -- whatever the SMT module gives us
2010-11-26 blanchet 2010-11-26 put facts found by SMT solver in alphabetical order and omit chained facts, as was done already for ATP proofs
2010-11-26 blanchet 2010-11-26 adjust Sledgehammer/SMT fudge factor
2010-11-25 blanchet 2010-11-25 cosmetics
2010-11-25 blanchet 2010-11-25 set Metis option on correct context, lest it be ignored
2010-11-25 blanchet 2010-11-25 make "debug" mode of Sledgehammer/SMT more liberal
2010-11-24 blanchet 2010-11-24 more precise error handling in Sledgehammer/SMT for Z3 and remote SMT provers
2010-11-23 blanchet 2010-11-23 more precise error handling for Z3; refactored some of the error handling code shared by ATP and SMT
2010-11-23 blanchet 2010-11-23 use "Thm.transfer" in Sledgehammer to prevent theory merger issues in "SMT_Solver.smt_filter" later on
2010-11-23 blanchet 2010-11-23 try Metis to reconstruct SMT proofs, to increase success rate and reduce dependency on (often remote) SMT solvers or certificates
2010-11-20 wenzelm 2010-11-20 renamed raw "explode" function to "raw_explode" to emphasize its meaning;
2010-11-15 boehmes 2010-11-15 merged
2010-11-15 boehmes 2010-11-15 renamed SMT failure: Abnormal_Termination is indeed more appropriate than Solver_Crashed
2010-11-15 blanchet 2010-11-15 better error message
2010-11-15 blanchet 2010-11-15 better error message
2010-11-15 blanchet 2010-11-15 cosmetics
2010-11-15 blanchet 2010-11-15 interpret SMT_Failure.Solver_Crashed correctly
2010-11-15 blanchet 2010-11-15 pick up SMT solver crashes and report them to the user/Mirabelle if desired
2010-11-10 blanchet 2010-11-10 make SML/NJ happy
2010-11-08 blanchet 2010-11-08 reduce the number of monomorphization iterations from 10 (the default) to 4, in the interest of faster SMT solving
2010-11-08 blanchet 2010-11-08 compile -- 7550b2cba1cb broke the build
2010-11-08 boehmes 2010-11-08 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)
2010-11-08 blanchet 2010-11-08 make sure the SMT solver runs several iterations by lowering the timeout at each iteration -- yields better results in practice
2010-11-07 blanchet 2010-11-07 always use a hard timeout in Mirabelle
2010-11-07 blanchet 2010-11-07 don't pass too many facts on the first iteration of the SMT solver
2010-11-07 blanchet 2010-11-07 catch TimeOut exception
2010-11-07 blanchet 2010-11-07 ensure the SMT solver respects the timeout -- Mirabelle revealed cases where "smt_filter" apparently never returns
2010-11-07 blanchet 2010-11-07 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
2010-11-06 blanchet 2010-11-06 invoke SMT solver in a loop, with fewer and fewer facts, in case of error
2010-11-04 blanchet 2010-11-04 cosmetics
2010-11-04 blanchet 2010-11-04 use the SMT integration's official list of built-ins
2010-11-03 blanchet 2010-11-03 standardize on seconds for Nitpick and Sledgehammer timeouts
2010-10-28 blanchet 2010-10-28 clear identification; thread "Auto S/H" (vs. manual S/H) setting through SMT
2010-10-26 blanchet 2010-10-26 adapted SMT solver error handling to reflect latest changes in "SMT_Solver"
2010-10-26 blanchet 2010-10-26 better list of irrelevant SMT constants
2010-10-26 blanchet 2010-10-26 if "debug" is on, print list of relevant facts (poweruser request); internal renaming
2010-10-26 blanchet 2010-10-26 standardize on "fact" terminology (vs. "axiom" or "theorem") in Sledgehammer -- but keep "Axiom" in the lower-level "ATP_Problem" module
2010-10-26 blanchet 2010-10-26 merge
2010-10-26 blanchet 2010-10-26 remove needless context argument; prefer "Proof.context_of" to "#context o Proof.goal", since it considers any "using [[...]]"
2010-10-26 boehmes 2010-10-26 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
2010-10-26 blanchet 2010-10-26 tuning
2010-10-26 blanchet 2010-10-26 proper error handling for SMT solvers in Sledgehammer
2010-10-26 blanchet 2010-10-26 integrated "smt" proof method with Sledgehammer
2010-10-25 wenzelm 2010-10-25 renamed Output.priority to Output.urgent_message to emphasize its special role more clearly;
2010-10-22 blanchet 2010-10-22 tuning
2010-10-22 blanchet 2010-10-22 more robust handling of "remote_" vs. non-"remote_" provers
2010-10-22 blanchet 2010-10-22 generalized the relevance filter so that it takes the list of "irrelevant constants" as argument (since the ATP and SMT preprocessing are different)