2011-05-22 ago added message when Waldmeister isn't run
2011-05-22 ago improved Waldmeister support -- even run it by default on unit equational goals
2011-05-19 ago distinguish between a soft timeout (30 s by defalt) and a hard timeout (60 s), to let minimization-based provers (such as CVC3, Yices, and occasionally the other provers) do their job
2011-05-03 ago replaced some Unsynchronized.refs with Config.Ts
2011-05-02 ago tuning
2011-05-02 ago have each ATP filter out dangerous facts for themselves, based on their type system
2011-05-02 ago use strings to encode type systems in ATP module, to reduce the amount of out-of-place information and also to make it easier to print the type system used
2011-05-01 ago 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 ago implement the new ATP type system in Sledgehammer
2011-05-01 ago reimplemented the hAPP introduction code so that it's done earlier, when the types are still available
2011-05-01 ago 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 ago detect some unsound proofs before showing them to the user
2011-04-21 ago cleanup: get rid of "may_slice" arguments without changing semantics
2011-04-21 ago implemented general slicing for ATPs, especially E 1.2w and above
2011-04-16 ago modernized structure Proof_Context;
2011-03-31 ago added monomorphization option to Sledgehammer ATPs -- this looks promising but is still off by default
2011-03-17 ago add option to function to keep trivial ATP formulas, needed for some experiments
2011-02-21 ago added a timeout around SMT preprocessing (notably monomorphization)
2011-02-18 ago gracious timeout in "blocking" mode
2011-02-10 ago run all provers in blocking mode, even if a proof was already found -- this behavior is less confusing to the user
2011-02-09 ago tuning
2011-02-09 ago automatically minimize Z3-as-an-ATP proofs (cf. CVC3 and Yices)
2011-02-09 ago renamed field
2011-02-08 ago available_provers ~> supported_provers (for clarity)
2011-01-06 ago differentiate between local and remote SMT solvers (e.g., "z3" vs. "remote_z3");
2010-12-21 ago added "smt_triggers" option to experiment with triggers in Sledgehammer;
2010-12-20 ago make exceptions more transparent in "debug" mode
2010-12-18 ago tuning
2010-12-18 ago lower threshold where the binary algorithm kick in and use the same value for automatic minimization
2010-12-18 ago 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 ago 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 ago factored out running a prover with (optionally) an implicit minimizer phrase
2010-12-17 ago remove option that doesn't work in Mirabelle anyway (Mirabelle uses Sledgehammer_Provers, not Sledgehammer_Run)
2010-12-17 ago put the SMT weights back where they belong, so that they're also used by Mirabelle
2010-12-17 ago added debugging option to find out how good the relevance filter was at identifying relevant facts
2010-12-17 ago export experimental options
2010-12-17 ago run the SMT relevance filter only once, then run the normalization/monomorphization code once _per class_ of SMT solvers
2010-12-16 ago make "debug" imply "blocking", since in blocking mode the exceptions flow through and are more instructive
2010-12-15 ago make sure errors generated in a thread don't vanish in cyberspace (e.g., when invoking Sledgehammer with unknown facts)
2010-12-15 ago facilitate debugging
2010-12-15 ago weaken the "expect" flag so that it doesn't trigger errors if a prover is not installed
2010-12-15 ago implemented partially-typed "tags" type encoding
2010-12-08 ago implicitly call the minimizer for SMT solvers that don't return an unsat core
2010-12-08 ago renamings
2010-12-08 ago moved function to later module
2010-12-08 ago clarified terminology
2010-12-08 ago split "Sledgehammer" module into two parts, to resolve forthcoming dependency problems