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