--- a/CONTRIBUTORS Mon Sep 12 12:33:37 2011 +0200
+++ b/CONTRIBUTORS Mon Sep 12 13:35:35 2011 +0200
@@ -16,6 +16,11 @@
Various building blocks for Isabelle/Scala layer and Isabelle/jEdit
Prover IDE.
+* 2011: Jasmin Blanchette, TUM
+ Various improvements to Sledgehammer, notably: use of sound translations,
+ support for more provers (Waldmeister, LEO-II, Satallax). Further development
+ of Nitpick and "try".
+
* 2011: Andreas Lochbihler, Karlsruhe Institute of Technology
Theory HOL/Library/Cset_Monad allows do notation for computable
sets (cset) via the generic monad ad-hoc overloading facility.
--- a/NEWS Mon Sep 12 12:33:37 2011 +0200
+++ b/NEWS Mon Sep 12 13:35:35 2011 +0200
@@ -180,10 +180,13 @@
INCOMPATIBILITY.
* Sledgehammer:
+ - Use quasi-sound (and efficient) translations by default.
+ - Added support for the following provers: E-ToFoF, LEO-II, Satallax, SNARK,
+ Waldmeister, and Z3 with TPTP syntax.
+ - Automatically preplay and minimize proofs before showing them if this can be
+ done within reasonable time.
- sledgehammer available_provers ~> sledgehammer supported_provers.
INCOMPATIBILITY.
- - Added support for SNARK and ToFoF-E on SystemOnTPTP and for simply typed
- TPTP problems (TFF).
- Added "preplay_timeout", "slicing", "type_enc", "sound", "max_mono_iters",
and "max_new_mono_instances" options.
- Removed "explicit_apply" and "full_types" options as well as "Full Types"
--- a/src/HOL/Tools/ATP/atp_util.ML Mon Sep 12 12:33:37 2011 +0200
+++ b/src/HOL/Tools/ATP/atp_util.ML Mon Sep 12 13:35:35 2011 +0200
@@ -123,7 +123,9 @@
Sign.typ_instance (Proof_Context.theory_of ctxt) (T, T')
fun type_generalization ctxt T T' = type_instance ctxt T' T
fun type_intersect ctxt T T' =
- can (Sign.typ_unify (Proof_Context.theory_of ctxt) (T, T')) (Vartab.empty, 0)
+ can (Sign.typ_unify (Proof_Context.theory_of ctxt)
+ (T, Logic.incr_tvar (maxidx_of_typ T + 1) T'))
+ (Vartab.empty, 0)
val type_equiv = Sign.typ_equiv o Proof_Context.theory_of
fun varify_type ctxt T =
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_run.ML Mon Sep 12 12:33:37 2011 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_run.ML Mon Sep 12 13:35:35 2011 +0200
@@ -18,8 +18,8 @@
val noneN : string
val timeoutN : string
val unknownN : string
- val auto_min_min_facts : int Config.T
- val auto_min_max_time : real Config.T
+ val auto_minimize_min_facts : int Config.T
+ val auto_minimize_max_time : real Config.T
val get_minimizing_prover : Proof.context -> mode -> string -> prover
val run_sledgehammer :
params -> mode -> int -> relevance_override -> (string -> minimize_command)
@@ -66,11 +66,12 @@
else
"\n" ^ Syntax.string_of_term ctxt (Thm.term_of (Thm.cprem_of goal i))))
-val auto_min_min_facts =
- Attrib.setup_config_int @{binding sledgehammer_auto_min_min_facts}
+val auto_minimize_min_facts =
+ Attrib.setup_config_int @{binding sledgehammer_auto_minimize_min_facts}
(fn generic => Config.get_generic generic binary_min_facts)
-val auto_min_max_time =
- Attrib.setup_config_real @{binding sledgehammer_auto_min_max_time} (K 5.0)
+val auto_minimize_max_time =
+ Attrib.setup_config_real @{binding sledgehammer_auto_minimize_max_time}
+ (K 5.0)
fun minimize ctxt mode name (params as {debug, verbose, isar_proof, ...})
({state, subgoal, subgoal_count, facts, ...} : prover_problem)
@@ -83,13 +84,13 @@
val num_facts = length used_facts
val ((minimize, minimize_name), preplay) =
if mode = Normal then
- if num_facts >= Config.get ctxt auto_min_min_facts then
+ if num_facts >= Config.get ctxt auto_minimize_min_facts then
((true, name), preplay)
else
let
fun can_min_fast_enough msecs =
0.001 * Real.fromInt ((num_facts + 2) * msecs)
- <= Config.get ctxt auto_min_max_time
+ <= Config.get ctxt auto_minimize_max_time
val prover_fast_enough =
run_time_in_msecs |> Option.map can_min_fast_enough
|> the_default false