--- a/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML Fri Dec 17 18:38:33 2010 +0100
+++ b/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML Fri Dec 17 21:32:06 2010 +0100
@@ -577,6 +577,7 @@
fun invoke args =
let
+ val _ = Sledgehammer_Run.show_facts_in_proofs := true
val _ = Sledgehammer_Isar.full_types := AList.defined (op =) args full_typesK
in Mirabelle.register (init, sledgehammer_action args, done) end
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_minimize.ML Fri Dec 17 18:38:33 2010 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_minimize.ML Fri Dec 17 21:32:06 2010 +0100
@@ -10,9 +10,7 @@
type locality = Sledgehammer_Filter.locality
type params = Sledgehammer_Provers.params
- val filter_used_facts :
- (string * locality) list -> ((string * locality) * thm list) list
- -> ((string * locality) * thm list) list
+ val filter_used_facts : ''a list -> (''a * 'b) list -> (''a * 'b) list
val minimize_facts :
params -> bool -> int -> int -> Proof.state
-> ((string * locality) * thm list) list
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML Fri Dec 17 18:38:33 2010 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML Fri Dec 17 21:32:06 2010 +0100
@@ -53,6 +53,12 @@
type prover = params -> minimize_command -> prover_problem -> prover_result
(* for experimentation purposes -- do not use in production code *)
+ val smt_weights : bool Unsynchronized.ref
+ val smt_weight_min_facts : int Unsynchronized.ref
+ val smt_min_weight : int Unsynchronized.ref
+ val smt_max_weight : int Unsynchronized.ref
+ val smt_max_weight_index : int Unsynchronized.ref
+ val smt_weight_curve : (int -> int) Unsynchronized.ref
val smt_max_iters : int Unsynchronized.ref
val smt_iter_fact_frac : real Unsynchronized.ref
val smt_iter_time_frac : real Unsynchronized.ref
@@ -73,9 +79,13 @@
val dest_dir : string Config.T
val problem_prefix : string Config.T
val measure_run_time : bool Config.T
+ val weight_smt_fact :
+ theory -> int -> ((string * locality) * thm) * int
+ -> (string * locality) * (int option * thm)
val untranslated_fact : prover_fact -> (string * locality) * thm
val smt_weighted_fact :
- prover_fact -> (string * locality) * (int option * thm)
+ theory -> int -> prover_fact * int
+ -> (string * locality) * (int option * thm)
val available_provers : Proof.context -> unit
val kill_provers : unit -> unit
val running_provers : unit -> unit
@@ -277,7 +287,26 @@
fun proof_banner auto =
if auto then "Auto Sledgehammer found a proof" else "Try this command"
-(* generic TPTP-based ATPs *)
+val smt_weights = Unsynchronized.ref true
+val smt_weight_min_facts = Unsynchronized.ref 20
+
+(* FUDGE *)
+val smt_min_weight = Unsynchronized.ref 0
+val smt_max_weight = Unsynchronized.ref 10
+val smt_max_weight_index = Unsynchronized.ref 200
+val smt_weight_curve = Unsynchronized.ref (fn x : int => x * x)
+
+fun smt_fact_weight j num_facts =
+ if !smt_weights andalso num_facts >= !smt_weight_min_facts then
+ SOME (!smt_max_weight
+ - (!smt_max_weight - !smt_min_weight + 1)
+ * !smt_weight_curve (Int.max (0, !smt_max_weight_index - j - 1))
+ div !smt_weight_curve (!smt_max_weight_index))
+ else
+ NONE
+
+fun weight_smt_fact thy num_facts ((info, th), j) =
+ (info, (smt_fact_weight j num_facts, th |> Thm.transfer thy))
fun untranslated_fact (Untranslated_Fact p) = p
| untranslated_fact (ATP_Translated_Fact (_, p)) = p
@@ -285,8 +314,11 @@
fun atp_translated_fact _ (ATP_Translated_Fact p) = p
| atp_translated_fact ctxt fact =
translate_atp_fact ctxt (untranslated_fact fact)
-fun smt_weighted_fact (SMT_Weighted_Fact p) = p
- | smt_weighted_fact fact = untranslated_fact fact |> apsnd (pair NONE)
+fun smt_weighted_fact _ _ (SMT_Weighted_Fact p, _) = p
+ | smt_weighted_fact thy num_facts (fact, j) =
+ (untranslated_fact fact, j) |> weight_smt_fact thy num_facts
+
+(* generic TPTP-based ATPs *)
fun int_opt_add (SOME m) (SOME n) = SOME (m + n)
| int_opt_add _ _ = NONE
@@ -602,7 +634,10 @@
: prover_problem) =
let
val ctxt = Proof.context_of state
- val facts = facts |> map smt_weighted_fact
+ val thy = Proof.theory_of state
+ val num_facts = length facts
+ val facts = facts ~~ (0 upto num_facts - 1)
+ |> map (smt_weighted_fact thy num_facts)
val {outcome, used_facts, run_time_in_msecs} =
smt_filter_loop name params state subgoal smt_head facts
val (chained_lemmas, other_lemmas) = split_used_facts (map fst used_facts)
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_run.ML Fri Dec 17 18:38:33 2010 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_run.ML Fri Dec 17 21:32:06 2010 +0100
@@ -13,12 +13,7 @@
type params = Sledgehammer_Provers.params
(* for experimentation purposes -- do not use in production code *)
- val smt_weights : bool Unsynchronized.ref
- val smt_weight_min_facts : int Unsynchronized.ref
- val smt_min_weight : int Unsynchronized.ref
- val smt_max_weight : int Unsynchronized.ref
- val smt_max_weight_index : int Unsynchronized.ref
- val smt_weight_curve : (int -> int) Unsynchronized.ref
+ val show_facts_in_proofs : bool Unsynchronized.ref
val run_sledgehammer :
params -> bool -> int -> relevance_override -> (string -> minimize_command)
@@ -47,6 +42,8 @@
else
"\n" ^ Syntax.string_of_term ctxt (Thm.term_of (Thm.cprem_of goal i)))
+val show_facts_in_proofs = Unsynchronized.ref false
+
val implicit_minimization_threshold = 50
fun run_prover (params as {debug, blocking, max_relevant, timeout, expect, ...})
@@ -66,22 +63,38 @@
{state = state, goal = goal, subgoal = subgoal,
subgoal_count = subgoal_count, facts = take num_facts facts,
smt_head = smt_head}
+ fun really_go () =
+ prover params (minimize_command name) problem
+ |> (fn {outcome, used_facts, message, ...} =>
+ if is_some outcome then
+ ("none", message)
+ else
+ let
+ val (used_facts, message) =
+ if length used_facts >= implicit_minimization_threshold then
+ minimize_facts params true subgoal subgoal_count state
+ (filter_used_facts used_facts
+ (map (apsnd single o untranslated_fact) facts))
+ |>> Option.map (map fst)
+ else
+ (SOME used_facts, message)
+ val _ =
+ case (debug orelse !show_facts_in_proofs, used_facts) of
+ (true, SOME (used_facts as _ :: _)) =>
+ facts ~~ (0 upto length facts - 1)
+ |> map (fn (fact, j) =>
+ fact |> untranslated_fact |> apsnd (K j))
+ |> filter_used_facts used_facts
+ |> map (fn ((name, _), j) => name ^ "@" ^ string_of_int j)
+ |> commas
+ |> enclose ("Fact" ^ plural_s num_facts ^ " in " ^
+ quote name ^ " proof (of " ^
+ string_of_int num_facts ^ "): ") "."
+ |> Output.urgent_message
+ | _ => ()
+ in ("some", message) end)
fun go () =
let
- fun really_go () =
- prover params (minimize_command name) problem
- |> (fn {outcome, used_facts, message, ...} =>
- if is_some outcome then
- ("none", message)
- else
- ("some",
- if length used_facts >= implicit_minimization_threshold then
- minimize_facts params true subgoal subgoal_count state
- (filter_used_facts used_facts
- (map (apsnd single o untranslated_fact) facts))
- |> snd
- else
- message))
val (outcome_code, message) =
if debug then
really_go ()
@@ -124,27 +137,6 @@
(false, state))
end
-val smt_weights = Unsynchronized.ref true
-val smt_weight_min_facts = Unsynchronized.ref 20
-
-(* FUDGE *)
-val smt_min_weight = Unsynchronized.ref 0
-val smt_max_weight = Unsynchronized.ref 10
-val smt_max_weight_index = Unsynchronized.ref 200
-val smt_weight_curve = Unsynchronized.ref (fn x : int => x * x)
-
-fun smt_fact_weight j num_facts =
- if !smt_weights andalso num_facts >= !smt_weight_min_facts then
- SOME (!smt_max_weight
- - (!smt_max_weight - !smt_min_weight + 1)
- * !smt_weight_curve (Int.max (0, !smt_max_weight_index - j - 1))
- div !smt_weight_curve (!smt_max_weight_index))
- else
- NONE
-
-fun weight_smt_fact thy num_facts (fact, j) =
- fact |> apsnd (pair (smt_fact_weight j num_facts) o Thm.transfer thy)
-
fun class_of_smt_solver ctxt name =
ctxt |> select_smt_solver name
|> SMT_Config.solver_class_of |> SMT_Utils.string_of_class
@@ -154,6 +146,9 @@
| smart_par_list_map f [x] = [f x]
| smart_par_list_map f xs = Par_List.map f xs
+fun dest_SMT_Weighted_Fact (SMT_Weighted_Fact p) = p
+ | dest_SMT_Weighted_Fact _ = raise Fail "dest_SMT_Weighted_Fact"
+
(* FUDGE *)
val auto_max_relevant_divisor = 2
@@ -181,32 +176,29 @@
| NONE => ()
val _ = if auto then () else Output.urgent_message "Sledgehammering..."
val (smts, atps) = provers |> List.partition (is_smt_prover ctxt)
- fun run_provers get_facts translate maybe_smt_head provers
- (res as (success, state)) =
- if success orelse null provers then
- res
- else
- let
- val facts = get_facts ()
- val num_facts = length facts
- val facts = facts ~~ (0 upto num_facts - 1)
- |> map (translate num_facts)
- val problem =
- {state = state, goal = goal, subgoal = i, subgoal_count = n,
- facts = facts,
- smt_head = maybe_smt_head (map smt_weighted_fact facts) i}
- val run_prover = run_prover params auto minimize_command only
- in
- if auto then
- fold (fn prover => fn (true, state) => (true, state)
- | (false, _) => run_prover problem prover)
- provers (false, state)
- else
- provers
- |> (if blocking then smart_par_list_map else map)
- (run_prover problem)
- |> exists fst |> rpair state
- end
+ fun run_provers state get_facts translate maybe_smt_head provers =
+ let
+ val facts = get_facts ()
+ val num_facts = length facts
+ val facts = facts ~~ (0 upto num_facts - 1)
+ |> map (translate num_facts)
+ val problem =
+ {state = state, goal = goal, subgoal = i, subgoal_count = n,
+ facts = facts,
+ smt_head = maybe_smt_head
+ (fn () => map_filter (try dest_SMT_Weighted_Fact) facts) i}
+ val run_prover = run_prover params auto minimize_command only
+ in
+ if auto then
+ fold (fn prover => fn (true, state) => (true, state)
+ | (false, _) => run_prover problem prover)
+ provers (false, state)
+ else
+ provers
+ |> (if blocking then smart_par_list_map else map)
+ (run_prover problem)
+ |> exists fst |> rpair state
+ end
fun get_facts label no_dangerous_types relevance_fudge provers =
let
val max_max_relevant =
@@ -235,24 +227,27 @@
else
())
end
- val run_atps =
- run_provers
- (get_facts "ATP" no_dangerous_types atp_relevance_fudge o K atps)
- (ATP_Translated_Fact oo K (translate_atp_fact ctxt o fst))
- (K (K NONE)) atps
+ fun run_atps (accum as (success, _)) =
+ if success orelse null atps then
+ accum
+ else
+ run_provers state
+ (get_facts "ATP" no_dangerous_types atp_relevance_fudge o K atps)
+ (ATP_Translated_Fact oo K (translate_atp_fact ctxt o fst))
+ (K (K NONE)) atps
fun run_smts (accum as (success, _)) =
if success orelse null smts then
accum
else
let
val facts = get_facts "SMT solver" true smt_relevance_fudge smts
- val translate = SMT_Weighted_Fact oo weight_smt_fact thy
- val maybe_smt_head = try o SMT_Solver.smt_filter_head state
+ val weight = SMT_Weighted_Fact oo weight_smt_fact thy
+ fun smt_head facts =
+ try (SMT_Solver.smt_filter_head state (facts ()))
in
smts |> map (`(class_of_smt_solver ctxt))
|> AList.group (op =)
- |> map (fn (_, smts) => run_provers (K facts) translate
- maybe_smt_head smts accum)
+ |> map (run_provers state (K facts) weight smt_head o snd)
|> exists fst |> rpair state
end
fun run_atps_and_smt_solvers () =