src/HOL/Tools/Sledgehammer/sledgehammer_minimize.ML
2011-05-12 blanchet 2011-05-12 renamed "max_mono_instances" to "max_new_mono_instances" and changed its semantics accordingly
2011-05-12 blanchet 2011-05-12 added "max_mono_instances" option to Sledgehammer and renamed old "monomorphize_limit" option
2011-05-03 blanchet 2011-05-03 replaced some Unsynchronized.refs with Config.Ts
2011-05-01 blanchet 2011-05-01 implement the new ATP type system in Sledgehammer
2011-04-21 blanchet 2011-04-21 cleanup: get rid of "may_slice" arguments without changing semantics
2011-04-21 blanchet 2011-04-21 implemented general slicing for ATPs, especially E 1.2w and above
2011-03-31 blanchet 2011-03-31 added monomorphization option to Sledgehammer ATPs -- this looks promising but is still off by default
2011-03-22 blanchet 2011-03-22 make Minimizer honor "verbose" and "debug" options better
2011-02-23 blanchet 2011-02-23 remove confusing message
2011-02-10 blanchet 2011-02-10 tuning
2011-02-10 blanchet 2011-02-10 remove pointless clutter
2011-02-10 blanchet 2011-02-10 make minimizer verbose
2011-02-09 blanchet 2011-02-09 tuning
2011-02-09 blanchet 2011-02-09 automatically minimize Z3-as-an-ATP proofs (cf. CVC3 and Yices)
2011-02-09 blanchet 2011-02-09 renamed field
2011-01-10 wenzelm 2011-01-10 eliminated Int.toString;
2010-12-21 blanchet 2010-12-21 added "smt_triggers" option to experiment with triggers in Sledgehammer; renamings (for consistency)
2010-12-19 blanchet 2010-12-19 reduce the minimizer slack and add verbose information
2010-12-18 blanchet 2010-12-18 lower threshold where the binary algorithm kick in and use the same value for automatic minimization
2010-12-18 blanchet 2010-12-18 let each prover minimizes its own stuff (rather than taking the first prover of the list to minimize every prover's stuff)
2010-12-17 blanchet 2010-12-17 more precise error messages in "verbose" (or "debug") mode, following this morning's permission debacle
2010-12-17 blanchet 2010-12-17 added debugging option to find out how good the relevance filter was at identifying relevant facts
2010-12-17 blanchet 2010-12-17 run the SMT relevance filter only once, then run the normalization/monomorphization code once _per class_ of SMT solvers
2010-12-16 blanchet 2010-12-16 make "debug" imply "blocking", since in blocking mode the exceptions flow through and are more instructive
2010-12-15 blanchet 2010-12-15 implemented partially-typed "tags" type encoding
2010-12-15 blanchet 2010-12-15 added "type_sys" option to Sledgehammer
2010-12-08 blanchet 2010-12-08 implicitly call the minimizer for SMT solvers that don't return an unsat core
2010-12-08 blanchet 2010-12-08 renamings
2010-12-08 blanchet 2010-12-08 split "Sledgehammer" module into two parts, to resolve forthcoming dependency problems
2010-12-06 blanchet 2010-12-06 handle "max_relevant" uniformly
2010-12-06 blanchet 2010-12-06 [mq]: sledge_binary_minimizer
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-15 blanchet 2010-11-15 pick up SMT solver crashes and report them to the user/Mirabelle if desired
2010-11-03 blanchet 2010-11-03 don't be overly verbose in Sledgehammer's minimizer
2010-11-03 blanchet 2010-11-03 standardize on seconds for Nitpick and Sledgehammer timeouts
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 remove needless context argument; prefer "Proof.context_of" to "#context o Proof.goal", since it considers any "using [[...]]"
2010-10-26 blanchet 2010-10-26 proper error handling for SMT solvers in 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 fixed signature of "is_smt_solver_installed"; renaming
2010-10-22 blanchet 2010-10-22 renamed modules
2010-10-22 blanchet 2010-10-22 remove more needless code ("run_smt_solvers"); tuning
2010-10-22 blanchet 2010-10-22 bring ATPs and SMT solvers more in line with each other
2010-10-22 blanchet 2010-10-22 make Sledgehammer minimizer fully work with SMT
2010-10-22 blanchet 2010-10-22 generalization of the Sledgehammer minimizer, to make it possible to handle SMT solvers as well
2010-10-21 blanchet 2010-10-21 first step in adding support for an SMT backend to Sledgehammer
2010-10-21 blanchet 2010-10-21 use consistent terminology in Sledgehammer: "prover = ATP or SMT solver or ..."
2010-09-16 blanchet 2010-09-16 got caught once again by SML's pattern maching (ctor vs. var)
2010-09-16 blanchet 2010-09-16 refactoring: move ATP proof and error extraction code to "ATP_Proof" module
2010-09-16 blanchet 2010-09-16 factored out TSTP/SPASS/Vampire proof parsing; from "Sledgehammer_Reconstructo" to a new module "ATP_Proof"
2010-09-14 blanchet 2010-09-14 handle relevance filter corner cases more gracefully; e.g. the minimizer selects 15 facts but "max_relevant = 14"
2010-09-13 blanchet 2010-09-13 tuning
2010-09-11 blanchet 2010-09-11 tuning
2010-09-11 blanchet 2010-09-11 implemented Auto Sledgehammer
2010-09-09 blanchet 2010-09-09 better error reporting when the Sledgehammer minimizer is interrupted
2010-09-01 blanchet 2010-09-01 minor refactoring
2010-09-01 blanchet 2010-09-01 translate the axioms to FOF once and for all ATPs
2010-09-01 blanchet 2010-09-01 share the relevance filter among the provers