src/HOL/Mirabelle/Tools/mirabelle_sledgehammer_filter.ML
2012-04-24 sultana 2012-04-24 reversed Tools to Actions Mirabelle renaming;
2011-12-01 blanchet 2011-12-01 renamed "slicing" to "slice"
2011-08-31 blanchet 2011-08-31 more tuning
2011-08-30 nik 2011-08-30 improved handling of induction rules in Sledgehammer
2011-07-08 wenzelm 2011-07-08 discontinued odd Position.column -- left-over from attempts at PGIP implementation; Position.offset discriminates postions precisely, now also available for Position.line/line_file;
2011-06-10 blanchet 2011-06-10 compute the set of base facts only once (instead of three times in parallel) -- this saves about .5 s of CPU time, albeit much less clock wall time
2011-05-31 blanchet 2011-05-31 compile
2011-05-27 blanchet 2011-05-27 fix soundness bug in Sledgehammer: distinguish params in goals from fixed variables in context
2011-05-24 blanchet 2011-05-24 tuning -- the "appropriate" terminology is inspired from TPTP
2011-05-22 blanchet 2011-05-22 improved Waldmeister support -- even run it by default on unit equational goals
2011-05-12 blanchet 2011-05-12 remove unused parameter
2011-05-12 blanchet 2011-05-12 fine-tuned the relevance filter, so that equations of the form "c = (%x. _)" and constants occurring in chained facts are not unduely penalized
2011-05-02 blanchet 2011-05-02 tuning
2011-05-02 blanchet 2011-05-02 have each ATP filter out dangerous facts for themselves, based on their type system
2011-05-01 blanchet 2011-05-01 restructured type systems some more -- the old naming schemes had "argshg diff |less" and "tagshg diff |less" as equivalent and didn't support a monomorphic version of "tags"
2011-05-01 blanchet 2011-05-01 implement the new ATP type system in Sledgehammer
2011-04-21 blanchet 2011-04-21 detect some unsound proofs before showing them to the user
2011-04-21 blanchet 2011-04-21 implemented general slicing for ATPs, especially E 1.2w and above
2011-02-21 blanchet 2011-02-21 give more weight to Frees than to Consts in relevance filter
2011-01-07 wenzelm 2011-01-07 tuned;
2010-12-29 wenzelm 2010-12-29 made SML/NJ happy; more accurate dependencies;
2010-12-15 blanchet 2010-12-15 honor "overlord" option for SMT solvers as well and don't pass "ext" to them
2010-12-15 blanchet 2010-12-15 implemented partially-typed "tags" type encoding
2010-12-08 blanchet 2010-12-08 split "Sledgehammer" module into two parts, to resolve forthcoming dependency problems
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-04 blanchet 2010-11-04 use the SMT integration's official list of built-ins
2010-10-27 blanchet 2010-10-27 generalize to handle any prover (not just E)
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)
2010-10-22 blanchet 2010-10-22 replaced references with proper record that's threaded through
2010-10-22 blanchet 2010-10-22 fixed signature of "is_smt_solver_installed"; renaming
2010-09-01 blanchet 2010-09-01 got rid of the "theory_relevant" option; instead, have fudge factors that behave more smoothly for all provers
2010-09-01 blanchet 2010-09-01 support new option in Mirabelle
2010-09-01 blanchet 2010-09-01 introduce fudge factors to deal with "theory const"
2010-08-31 blanchet 2010-08-31 finished renaming
2010-08-31 blanchet 2010-08-31 add one option to Mirabelle
2010-08-31 blanchet 2010-08-31 improve weighting of irrelevant constants, based on Mirabelle experiments
2010-08-31 blanchet 2010-08-31 take into consideration whether a fact is an "intro"/"elim"/"simp" rule as an additional factor influencing the relevance filter
2010-08-30 blanchet 2010-08-30 adjust Mirabelle
2010-08-30 blanchet 2010-08-30 move imperative code to where it belongs
2010-08-30 blanchet 2010-08-30 allow configuration of fact filter fudge factors
2010-08-30 blanchet 2010-08-30 show index in fact list of all found facts
2010-08-30 blanchet 2010-08-30 allow multiple invocations of "mirabele_sledgehammer_filter", by multiplexing on ID
2010-08-30 blanchet 2010-08-30 improve new "sledgehammer_filter" action
2010-08-30 blanchet 2010-08-30 added evaluation method for relevance filter