--- a/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML Sun Nov 06 18:42:15 2011 +0100
+++ b/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML Sun Nov 06 18:42:17 2011 +0100
@@ -405,11 +405,11 @@
NONE => I
| SOME secs => TimeLimit.timeLimit (Time.fromSeconds secs))
fun failed failure =
- ({outcome = SOME failure, used_facts = [], run_time_in_msecs = NONE,
+ ({outcome = SOME failure, used_facts = [], run_time = Time.zeroTime,
preplay = K (ATP_Reconstruct.Failed_to_Play ATP_Reconstruct.Metis),
message = K "", message_tail = ""}, ~1)
- val ({outcome, used_facts, run_time_in_msecs, preplay, message,
- message_tail} : Sledgehammer_Provers.prover_result,
+ val ({outcome, used_facts, run_time, preplay, message, message_tail}
+ : Sledgehammer_Provers.prover_result,
time_isa) = time_limit (Mirabelle.cpu_time (fn () =>
let
val _ = if is_appropriate_prop concl_t then ()
@@ -431,7 +431,7 @@
in prover params (K (K "")) problem end)) ()
handle TimeLimit.TimeOut => failed ATP_Proof.TimedOut
| Fail "inappropriate" => failed ATP_Proof.Inappropriate
- val time_prover = run_time_in_msecs |> the_default ~1
+ val time_prover = run_time |> Time.toMilliseconds
val msg = message (preplay ()) ^ message_tail
in
case outcome of
--- a/src/HOL/Tools/ATP/atp_systems.ML Sun Nov 06 18:42:15 2011 +0100
+++ b/src/HOL/Tools/ATP/atp_systems.ML Sun Nov 06 18:42:17 2011 +0100
@@ -43,8 +43,8 @@
val iproverN : string
val iprover_eqN : string
val leo2N : string
- val pffN : string
- val phfN : string
+ val dummy_tff1N : string
+ val dummy_thfN : string
val satallaxN : string
val snarkN : string
val spassN : string
@@ -130,12 +130,12 @@
val iproverN = "iprover"
val iprover_eqN = "iprover_eq"
val leo2N = "leo2"
-val pffN = "pff"
-val phfN = "phf"
+val dummy_tff1N = "dummy_tff1" (* experimental *)
+val dummy_thfN = "dummy_thf" (* experimental *)
val satallaxN = "satallax"
val snarkN = "snark"
val spassN = "spass"
-val spass_newN = "spass_new"
+val spass_newN = "spass_new" (* experimental *)
val vampireN = "vampire"
val waldmeisterN = "waldmeister"
val z3_tptpN = "z3_tptp"
@@ -437,13 +437,13 @@
prem_kind = Hypothesis,
best_slices = K [(1.0, (false, (200, format, type_enc, "")))]}
-val pff_format = TFF (TPTP_Polymorphic, TPTP_Explicit)
-val pff_config = dummy_config pff_format "poly_simple"
-val pff = (pffN, pff_config)
+val dummy_tff1_format = TFF (TPTP_Polymorphic, TPTP_Explicit)
+val dummy_tff1_config = dummy_config dummy_tff1_format "poly_simple"
+val dummy_tff1 = (dummy_tff1N, dummy_tff1_config)
-val phf_format = THF (TPTP_Polymorphic, TPTP_Explicit, THF_With_Choice)
-val phf_config = dummy_config phf_format "poly_simple_higher"
-val phf = (phfN, phf_config)
+val dummy_thf_format = THF (TPTP_Polymorphic, TPTP_Explicit, THF_With_Choice)
+val dummy_thf_config = dummy_config dummy_thf_format "poly_simple_higher"
+val dummy_thf = (dummy_thfN, dummy_thf_config)
(* Remote ATP invocation via SystemOnTPTP *)
@@ -574,8 +574,8 @@
Synchronized.change systems (fn _ => get_systems ())
val atps =
- [e, leo2, pff, phf, satallax, spass, spass_new, vampire, z3_tptp, remote_e,
- remote_e_sine, remote_e_tofof, remote_iprover, remote_iprover_eq,
+ [e, leo2, dummy_tff1, dummy_thf, satallax, spass, spass_new, vampire, z3_tptp,
+ remote_e, remote_e_sine, remote_e_tofof, remote_iprover, remote_iprover_eq,
remote_leo2, remote_satallax, remote_vampire, remote_z3_tptp, remote_snark,
remote_waldmeister]
val setup = fold add_atp atps
--- a/src/HOL/Tools/ATP/atp_translate.ML Sun Nov 06 18:42:15 2011 +0100
+++ b/src/HOL/Tools/ATP/atp_translate.ML Sun Nov 06 18:42:17 2011 +0100
@@ -1527,12 +1527,15 @@
(("If", true), @{thms if_True if_False True_or_False})]
|> map (apsnd (map zero_var_indexes))
+fun atype_of_type_vars (Simple_Types (_, Polymorphic, _)) = SOME atype_of_types
+ | atype_of_type_vars _ = NONE
+
fun bound_tvars type_enc Ts =
mk_ahorn (formulas_for_types type_enc add_sorts_on_tvar Ts)
#> mk_aquant AForall
(map_filter (fn TVar (x as (s, _), _) =>
SOME ((make_schematic_type_var x, s),
- SOME atype_of_types)
+ atype_of_type_vars type_enc)
| _ => NONE) Ts)
fun eq_formula type_enc atomic_Ts pred_sym tm1 tm2 =
@@ -1852,11 +1855,12 @@
|> type_class_formula type_enc class
fun formula_line_for_arity_clause format type_enc
- ({name, prem_atoms, concl_atom, ...} : arity_clause) =
+ ({name, prem_atoms, concl_atom} : arity_clause) =
Formula (arity_clause_prefix ^ name, Axiom,
mk_ahorn (map (formula_from_arity_atom type_enc) prem_atoms)
(formula_from_arity_atom type_enc concl_atom)
- |> close_formula_universally type_enc,
+ |> mk_aquant AForall
+ (map (rpair (atype_of_type_vars type_enc)) (#3 concl_atom)),
isabelle_info format introN, NONE)
fun formula_line_for_conjecture ctxt format mono type_enc
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_minimize.ML Sun Nov 06 18:42:15 2011 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_minimize.ML Sun Nov 06 18:42:17 2011 +0100
@@ -38,8 +38,8 @@
let val n = length names in
string_of_int n ^ " fact" ^ plural_s n ^
(if n > 0 then
- ": " ^ (names |> map fst
- |> sort_distinct string_ord |> space_implode " ")
+ ": " ^ (names |> map fst |> sort_distinct string_ord
+ |> space_implode " ")
else
"")
end
@@ -70,7 +70,7 @@
val problem =
{state = state, goal = goal, subgoal = i, subgoal_count = n,
facts = facts, smt_filter = NONE}
- val result as {outcome, used_facts, run_time_in_msecs, ...} =
+ val result as {outcome, used_facts, run_time, ...} =
prover params (K (K "")) problem
in
print silent
@@ -81,97 +81,113 @@
"Found proof" ^
(if length used_facts = length facts then ""
else " with " ^ n_facts used_facts) ^
- (case run_time_in_msecs of
- SOME ms =>
- " (" ^ string_from_time (Time.fromMilliseconds ms) ^ ")"
- | NONE => "") ^ ".");
+ " (" ^ string_from_time run_time ^ ").");
result
end
(* minimalization of facts *)
-(* The sublinear algorithm works well in almost all situations, except when the
- external prover cannot return the list of used facts and hence returns all
- facts as used. In that case, the binary algorithm is much more appropriate.
- We can usually detect the situation by looking at the number of used facts
- reported by the prover. *)
-val binary_min_facts =
- Attrib.setup_config_int @{binding sledgehammer_minimize_binary_min_facts}
- (K 20)
-
-fun sublinear_minimize _ [] p = p
- | sublinear_minimize test (x :: xs) (seen, result) =
- case test (xs @ seen) of
- result as {outcome = NONE, used_facts, ...} : prover_result =>
- sublinear_minimize test (filter_used_facts used_facts xs)
- (filter_used_facts used_facts seen, result)
- | _ => sublinear_minimize test xs (x :: seen, result)
-
-fun binary_minimize test xs =
- let
- fun pred xs = #outcome (test xs : prover_result) = NONE
- fun split [] p = p
- | split [h] (l, r) = (h :: l, r)
- | split (h1 :: h2 :: t) (l, r) = split t (h1 :: l, h2 :: r)
- fun min _ _ [] = raise Empty
- | min _ _ [s0] = [s0]
- | min depth sup xs =
- let
-(*
- val _ = warning (replicate_string depth " " ^ "{" ^ (" " ^
- n_facts (map fst sup) ^ " and " ^
- n_facts (map fst xs)))
-*)
- val (l0, r0) = split xs ([], [])
- in
- if pred (sup @ l0) then
- min (depth + 1) sup l0
- else if pred (sup @ r0) then
- min (depth + 1) sup r0
- else
- let
- val l = min (depth + 1) (sup @ r0) l0
- val r = min (depth + 1) (sup @ l) r0
- in l @ r end
- end
-(*
- |> tap (fn _ => warning (replicate_string depth " " ^ "}"))
-*)
- val xs =
- case min 0 [] xs of
- [x] => if pred [] then [] else [x]
- | xs => xs
- in (xs, test xs) end
-
(* Give the external prover some slack. The ATP gets further slack because the
Sledgehammer preprocessing time is included in the estimate below but isn't
part of the timeout. *)
val slack_msecs = 200
+fun new_timeout timeout run_time =
+ Int.min (Time.toMilliseconds timeout,
+ Time.toMilliseconds run_time + slack_msecs)
+ |> Time.fromMilliseconds
+
+(* The linear algorithm usually outperforms the binary algorithm when over 60%
+ of the facts are actually needed. The binary algorithm is much more
+ appropriate for provers that cannot return the list of used facts and hence
+ returns all facts as used. Since we cannot know in advance how many facts are
+ actually needed, we heuristically set the threshold to 10 facts. *)
+val binary_min_facts =
+ Attrib.setup_config_int @{binding sledgehammer_minimize_binary_min_facts}
+ (K 20)
+
+fun linear_minimize test timeout result xs =
+ let
+ fun min _ [] p = p
+ | min timeout (x :: xs) (seen, result) =
+ case test timeout (xs @ seen) of
+ result as {outcome = NONE, used_facts, run_time, ...}
+ : prover_result =>
+ min (new_timeout timeout run_time) (filter_used_facts used_facts xs)
+ (filter_used_facts used_facts seen, result)
+ | _ => min timeout xs (x :: seen, result)
+ in min timeout xs ([], result) end
+
+fun binary_minimize test timeout result xs =
+ let
+ fun min depth (result as {run_time, ...} : prover_result) sup
+ (xs as _ :: _ :: _) =
+ let
+ val (l0, r0) = chop (length xs div 2) xs
+(*
+ val _ = warning (replicate_string depth " " ^ "{ " ^
+ "sup: " ^ n_facts (map fst sup))
+ val _ = warning (replicate_string depth " " ^ " " ^
+ "xs: " ^ n_facts (map fst xs))
+ val _ = warning (replicate_string depth " " ^ " " ^
+ "l0: " ^ n_facts (map fst l0))
+ val _ = warning (replicate_string depth " " ^ " " ^
+ "r0: " ^ n_facts (map fst r0))
+*)
+ val depth = depth + 1
+ val timeout = new_timeout timeout run_time
+ in
+ case test timeout (sup @ l0) of
+ result as {outcome = NONE, used_facts, ...} =>
+ min depth result (filter_used_facts used_facts sup)
+ (filter_used_facts used_facts l0)
+ | _ =>
+ case test timeout (sup @ r0) of
+ result as {outcome = NONE, used_facts, ...} =>
+ min depth result (filter_used_facts used_facts sup)
+ (filter_used_facts used_facts r0)
+ | _ =>
+ let
+ val (sup_r0, (l, result)) = min depth result (sup @ r0) l0
+ val (sup, r0) =
+ (sup, r0) |> pairself (filter_used_facts (map fst sup_r0))
+ val (sup_l, (r, result)) = min depth result (sup @ l) r0
+ val sup = sup |> filter_used_facts (map fst sup_l)
+ in (sup, (l @ r, result)) end
+ end
+(*
+ |> tap (fn _ => warning (replicate_string depth " " ^ "}"))
+*)
+ | min _ result sup xs = (sup, (xs, result))
+ in
+ case snd (min 0 result [] xs) of
+ ([x], result as {run_time, ...}) =>
+ (case test (new_timeout timeout run_time) [] of
+ result as {outcome = NONE, ...} => ([], result)
+ | _ => ([x], result))
+ | p => p
+ end
+
fun minimize_facts prover_name (params as {timeout, ...}) silent i n state
facts =
let
val ctxt = Proof.context_of state
val prover = get_prover ctxt Minimize prover_name
- val msecs = Time.toMilliseconds timeout
val _ = print silent (fn () => "Sledgehammer minimizer: " ^
quote prover_name ^ ".")
- fun do_test timeout = test_facts params silent prover timeout i n state
- val timer = Timer.startRealTimer ()
+ fun test timeout = test_facts params silent prover timeout i n state
in
- (case do_test timeout facts of
- result as {outcome = NONE, used_facts, ...} =>
+ (case test timeout facts of
+ result as {outcome = NONE, used_facts, run_time, ...} =>
let
- val time = Timer.checkRealTimer timer
- val new_timeout =
- Int.min (msecs, Time.toMilliseconds time + slack_msecs)
- |> Time.fromMilliseconds
val facts = filter_used_facts used_facts facts
- val (min_facts, {preplay, message, message_tail, ...}) =
+ val min =
if length facts >= Config.get ctxt binary_min_facts then
- binary_minimize (do_test new_timeout) facts
+ binary_minimize
else
- sublinear_minimize (do_test new_timeout) facts ([], result)
+ linear_minimize
+ val (min_facts, {preplay, message, message_tail, ...}) =
+ min test (new_timeout timeout run_time) result facts
val _ = print silent (fn () => cat_lines
["Minimized to " ^ n_facts (map fst min_facts)] ^
(case length (filter (curry (op =) Chained o snd o fst) min_facts) of
@@ -183,7 +199,8 @@
(preplay,
fn _ => "Timeout: You can increase the time limit using the \
\\"timeout\" option (e.g., \"timeout = " ^
- string_of_int (10 + msecs div 1000) ^ "\").",
+ string_of_int (10 + Time.toMilliseconds timeout div 1000) ^
+ "\").",
""))
| {preplay, message, ...} =>
(NONE, (preplay, prefix "Prover error: " o message, "")))
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML Sun Nov 06 18:42:15 2011 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML Sun Nov 06 18:42:17 2011 +0100
@@ -52,7 +52,7 @@
type prover_result =
{outcome: failure option,
used_facts: (string * locality) list,
- run_time_in_msecs: int option,
+ run_time: Time.time,
preplay: unit -> play,
message: play -> string,
message_tail: string}
@@ -323,7 +323,7 @@
type prover_result =
{outcome: failure option,
used_facts: (string * locality) list,
- run_time_in_msecs: int option,
+ run_time: Time.time,
preplay: unit -> play,
message: play -> string,
message_tail: string}
@@ -797,7 +797,7 @@
| SOME failure =>
([], K (Failed_to_Play Metis), fn _ => string_for_failure failure, "")
in
- {outcome = outcome, used_facts = used_facts, run_time_in_msecs = SOME msecs,
+ {outcome = outcome, used_facts = used_facts, run_time = Time.fromMilliseconds msecs, (*###*)
preplay = preplay, message = message, message_tail = message_tail}
end
@@ -928,8 +928,7 @@
end
else
{outcome = if is_none outcome then NONE else the outcome0,
- used_facts = used_facts,
- run_time_in_msecs = SOME (Time.toMilliseconds time_so_far)}
+ used_facts = used_facts, run_time = time_so_far}
end
in do_slice timeout 1 NONE Time.zeroTime end
@@ -942,7 +941,7 @@
val num_facts = length facts
val facts = facts ~~ (0 upto num_facts - 1)
|> map (smt_weighted_fact ctxt num_facts)
- val {outcome, used_facts, run_time_in_msecs} =
+ val {outcome, used_facts, run_time} =
smt_filter_loop ctxt name params state subgoal smt_filter facts
val (used_facts, used_ths) = used_facts |> ListPair.unzip
val outcome = outcome |> Option.map failure_from_smt_failure
@@ -968,17 +967,14 @@
subgoal, subgoal_count)
in one_line_proof_text one_line_params end,
if verbose then
- "\nSMT solver real CPU time: " ^
- string_from_time (Time.fromMilliseconds
- (the run_time_in_msecs)) ^ "."
+ "\nSMT solver real CPU time: " ^ string_from_time run_time ^ "."
else
"")
| SOME failure =>
(K (Failed_to_Play Metis), fn _ => string_for_failure failure, "")
in
- {outcome = outcome, used_facts = used_facts,
- run_time_in_msecs = run_time_in_msecs, preplay = preplay,
- message = message, message_tail = message_tail}
+ {outcome = outcome, used_facts = used_facts, run_time = run_time,
+ preplay = preplay, message = message, message_tail = message_tail}
end
fun run_metis mode name ({debug, timeout, ...} : params) minimize_command
@@ -994,8 +990,7 @@
case play_one_line_proof debug timeout used_ths state subgoal
[reconstructor] of
play as Played (_, time) =>
- {outcome = NONE, used_facts = used_facts,
- run_time_in_msecs = SOME (Time.toMilliseconds time),
+ {outcome = NONE, used_facts = used_facts, run_time = time,
preplay = K play,
message = fn play =>
let
@@ -1008,7 +1003,7 @@
let
val failure = case play of Failed_to_Play _ => GaveUp | _ => TimedOut
in
- {outcome = SOME failure, used_facts = [], run_time_in_msecs = NONE,
+ {outcome = SOME failure, used_facts = [], run_time = Time.zeroTime,
preplay = K play, message = fn _ => string_for_failure failure,
message_tail = ""}
end
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_run.ML Sun Nov 06 18:42:15 2011 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_run.ML Sun Nov 06 18:42:17 2011 +0100
@@ -75,8 +75,8 @@
fun minimize ctxt mode name (params as {debug, verbose, isar_proof, ...})
({state, subgoal, subgoal_count, facts, ...} : prover_problem)
- (result as {outcome, used_facts, run_time_in_msecs, preplay,
- message, message_tail} : prover_result) =
+ (result as {outcome, used_facts, run_time, preplay, message,
+ message_tail} : prover_result) =
if is_some outcome orelse null used_facts then
result
else
@@ -88,12 +88,11 @@
((true, name), preplay)
else
let
- fun can_min_fast_enough msecs =
- 0.001 * Real.fromInt ((num_facts + 2) * msecs)
+ fun can_min_fast_enough time =
+ 0.001
+ * Real.fromInt ((num_facts + 1) * Time.toMilliseconds 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
+ val prover_fast_enough = can_min_fast_enough run_time
in
if isar_proof then
((prover_fast_enough, name), preplay)
@@ -101,7 +100,7 @@
let val preplay = preplay () in
(case preplay of
Played (reconstructor, timeout) =>
- if can_min_fast_enough (Time.toMilliseconds timeout) then
+ if can_min_fast_enough timeout then
(true, prover_name_for_reconstructor reconstructor
|> the_default name)
else
@@ -135,9 +134,8 @@
|> Output.urgent_message
else
();
- {outcome = NONE, used_facts = used_facts,
- run_time_in_msecs = run_time_in_msecs, preplay = preplay,
- message = message, message_tail = message_tail})
+ {outcome = NONE, used_facts = used_facts, run_time = run_time,
+ preplay = preplay, message = message, message_tail = message_tail})
| NONE => result
end