src/HOL/Tools/Sledgehammer/sledgehammer_run.ML
2011-05-01 blanchet 2011-05-01 reimplemented the hAPP introduction code so that it's done earlier, when the types are still available
2011-05-01 blanchet 2011-05-01 perform constant mangling and/or removal of its type args in an earlier phase, so that the rest of the code doesn't need to worry about it
2011-04-21 blanchet 2011-04-21 detect some unsound proofs before showing them to the user
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-04-16 wenzelm 2011-04-16 modernized structure Proof_Context;
2011-03-31 blanchet 2011-03-31 added monomorphization option to Sledgehammer ATPs -- this looks promising but is still off by default
2011-03-17 blanchet 2011-03-17 add option to function to keep trivial ATP formulas, needed for some experiments
2011-02-21 blanchet 2011-02-21 added a timeout around SMT preprocessing (notably monomorphization)
2011-02-18 blanchet 2011-02-18 gracious timeout in "blocking" mode
2011-02-10 blanchet 2011-02-10 run all provers in blocking mode, even if a proof was already found -- this behavior is less confusing to the user
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-02-08 blanchet 2011-02-08 available_provers ~> supported_provers (for clarity)
2011-01-06 boehmes 2011-01-06 differentiate between local and remote SMT solvers (e.g., "z3" vs. "remote_z3"); turned individual SMT solvers into components; made CVC3 the default SMT solver (Z3 is licensed as "non-commercial only"); tuned smt_filter interface
2010-12-21 blanchet 2010-12-21 added "smt_triggers" option to experiment with triggers in Sledgehammer; renamings (for consistency)
2010-12-20 blanchet 2010-12-20 make exceptions more transparent in "debug" mode
2010-12-18 blanchet 2010-12-18 tuning
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-18 blanchet 2010-12-18 renamed function to run prover with minimizer and changed signature to clarify its semantics and make it a drop in replacement for "get_prover"
2010-12-18 blanchet 2010-12-18 factored out running a prover with (optionally) an implicit minimizer phrase
2010-12-17 blanchet 2010-12-17 remove option that doesn't work in Mirabelle anyway (Mirabelle uses Sledgehammer_Provers, not Sledgehammer_Run)
2010-12-17 blanchet 2010-12-17 put the SMT weights back where they belong, so that they're also used by Mirabelle
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 export experimental options
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 make sure errors generated in a thread don't vanish in cyberspace (e.g., when invoking Sledgehammer with unknown facts)
2010-12-15 blanchet 2010-12-15 facilitate debugging
2010-12-15 blanchet 2010-12-15 weaken the "expect" flag so that it doesn't trigger errors if a prover is not installed
2010-12-15 blanchet 2010-12-15 implemented partially-typed "tags" type encoding
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 moved function to later module
2010-12-08 blanchet 2010-12-08 clarified terminology
2010-12-08 blanchet 2010-12-08 split "Sledgehammer" module into two parts, to resolve forthcoming dependency problems