--- a/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML Fri Jan 31 10:34:20 2014 +0100
+++ b/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML Fri Jan 31 12:30:54 2014 +0100
@@ -361,10 +361,10 @@
fun change_data id f = (Unsynchronized.change data (AList.map_entry (op =) id f); ())
-fun get_prover_name ctxt args =
+fun get_prover_name thy args =
let
fun default_prover_name () =
- hd (#provers (Sledgehammer_Commands.default_params ctxt []))
+ hd (#provers (Sledgehammer_Commands.default_params thy []))
handle List.Empty => error "No ATP available."
in
(case AList.lookup (op =) args proverK of
@@ -417,6 +417,7 @@
hard_timeout timeout preplay_timeout sh_minimizeLST
max_new_mono_instancesLST max_mono_itersLST dir pos st =
let
+ val thy = Proof.theory_of st
val {context = ctxt, facts = chained_ths, goal} = Proof.goal st
val i = 1
fun set_file_name (SOME dir) =
@@ -438,7 +439,7 @@
#> (Option.map (Config.put ATP_Systems.force_sos)
force_sos |> the_default I))
val params as {max_facts, ...} =
- Sledgehammer_Commands.default_params ctxt
+ Sledgehammer_Commands.default_params thy
([("verbose", "true"),
("fact_filter", fact_filter),
("type_enc", type_enc),
@@ -452,7 +453,8 @@
|> sh_minimizeLST (*don't confuse the two minimization flags*)
|> max_new_mono_instancesLST
|> max_mono_itersLST)
- val default_max_facts = Sledgehammer_Prover.default_max_facts_of_prover ctxt prover_name
+ val default_max_facts =
+ Sledgehammer_Prover_Minimize.default_max_facts_of_prover ctxt prover_name
val is_appropriate_prop =
Sledgehammer_Prover.is_appropriate_prop_of_prover ctxt prover_name
val (_, hyp_ts, concl_t) = ATP_Util.strip_subgoal goal i ctxt
@@ -510,11 +512,12 @@
fun run_sledgehammer trivial args reconstructor named_thms id
({pre=st, log, pos, ...}: Mirabelle.run_args) =
let
+ val thy = Proof.theory_of st
val ctxt = Proof.context_of st
val triv_str = if trivial then "[T] " else ""
val _ = change_data id inc_sh_calls
val _ = if trivial then () else change_data id inc_sh_nontriv_calls
- val prover_name = get_prover_name ctxt args
+ val prover_name = get_prover_name thy args
val fact_filter = AList.lookup (op =) args fact_filterK |> the_default fact_filter_default
val type_enc = AList.lookup (op =) args type_encK |> the_default type_enc_default
val strict = AList.lookup (op =) args strictK |> the_default strict_default
@@ -580,10 +583,11 @@
fun run_minimize args reconstructor named_thms id
({pre=st, log, ...}: Mirabelle.run_args) =
let
+ val thy = Proof.theory_of st
val ctxt = Proof.context_of st
val {goal, ...} = Proof.goal st
val n0 = length (these (!named_thms))
- val prover_name = get_prover_name ctxt args
+ val prover_name = get_prover_name thy args
val type_enc = AList.lookup (op =) args type_encK |> the_default type_enc_default
val strict = AList.lookup (op =) args strictK |> the_default strict_default
val timeout =
@@ -596,7 +600,7 @@
val max_new_mono_instancesLST =
available_parameter args max_new_mono_instancesK max_new_mono_instancesK
val max_mono_itersLST = available_parameter args max_mono_itersK max_mono_itersK
- val params = Sledgehammer_Commands.default_params ctxt
+ val params = Sledgehammer_Commands.default_params thy
([("provers", prover_name),
("verbose", "true"),
("type_enc", type_enc),
--- a/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer_filter.ML Fri Jan 31 10:34:20 2014 +0100
+++ b/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer_filter.ML Fri Jan 31 12:30:54 2014 +0100
@@ -11,25 +11,18 @@
| NONE => default_value
fun extract_relevance_fudge args
- {local_const_multiplier, worse_irrel_freq, higher_order_irrel_weight,
- abs_rel_weight, abs_irrel_weight, theory_const_rel_weight,
- theory_const_irrel_weight, chained_const_irrel_weight, intro_bonus,
- elim_bonus, simp_bonus, local_bonus, assum_bonus, chained_bonus,
- max_imperfect, max_imperfect_exp, threshold_divisor,
- ridiculous_threshold} =
- {local_const_multiplier =
- get args "local_const_multiplier" local_const_multiplier,
+ {local_const_multiplier, worse_irrel_freq, higher_order_irrel_weight, abs_rel_weight,
+ abs_irrel_weight, theory_const_rel_weight, theory_const_irrel_weight,
+ chained_const_irrel_weight, intro_bonus, elim_bonus, simp_bonus, local_bonus, assum_bonus,
+ chained_bonus, max_imperfect, max_imperfect_exp, threshold_divisor, ridiculous_threshold} =
+ {local_const_multiplier = get args "local_const_multiplier" local_const_multiplier,
worse_irrel_freq = get args "worse_irrel_freq" worse_irrel_freq,
- higher_order_irrel_weight =
- get args "higher_order_irrel_weight" higher_order_irrel_weight,
+ higher_order_irrel_weight = get args "higher_order_irrel_weight" higher_order_irrel_weight,
abs_rel_weight = get args "abs_rel_weight" abs_rel_weight,
abs_irrel_weight = get args "abs_irrel_weight" abs_irrel_weight,
- theory_const_rel_weight =
- get args "theory_const_rel_weight" theory_const_rel_weight,
- theory_const_irrel_weight =
- get args "theory_const_irrel_weight" theory_const_irrel_weight,
- chained_const_irrel_weight =
- get args "chained_const_irrel_weight" chained_const_irrel_weight,
+ theory_const_rel_weight = get args "theory_const_rel_weight" theory_const_rel_weight,
+ theory_const_irrel_weight = get args "theory_const_irrel_weight" theory_const_irrel_weight,
+ chained_const_irrel_weight = get args "chained_const_irrel_weight" chained_const_irrel_weight,
intro_bonus = get args "intro_bonus" intro_bonus,
elim_bonus = get args "elim_bonus" elim_bonus,
simp_bonus = get args "simp_bonus" simp_bonus,
@@ -56,17 +49,17 @@
fun get id c = the_default 0 (AList.lookup (op =) (!c) id)
fun add id c n =
c := (case AList.lookup (op =) (!c) id of
- SOME m => AList.update (op =) (id, m + n) (!c)
- | NONE => (id, n) :: !c)
+ SOME m => AList.update (op =) (id, m + n) (!c)
+ | NONE => (id, n) :: !c)
fun init proof_file _ thy =
let
fun do_line line =
- case line |> space_explode ":" of
+ (case line |> space_explode ":" of
[line_num, offset, proof] =>
SOME (pairself (the o Int.fromString) (line_num, offset),
proof |> space_explode " " |> filter_out (curry (op =) ""))
- | _ => NONE
+ | _ => NONE)
val proofs = File.read (Path.explode proof_file)
val proof_tab =
proofs |> space_explode "\n"
@@ -81,21 +74,18 @@
fun done id ({log, ...} : Mirabelle.done_args) =
if get id num_successes + get id num_failures > 0 then
(log "";
- log ("Number of overall successes: " ^
- string_of_int (get id num_successes));
+ log ("Number of overall successes: " ^ string_of_int (get id num_successes));
log ("Number of overall failures: " ^ string_of_int (get id num_failures));
log ("Overall success rate: " ^
percentage_alt (get id num_successes) (get id num_failures) ^ "%");
log ("Number of found proofs: " ^ string_of_int (get id num_found_proofs));
log ("Number of lost proofs: " ^ string_of_int (get id num_lost_proofs));
log ("Proof found rate: " ^
- percentage_alt (get id num_found_proofs) (get id num_lost_proofs) ^
- "%");
+ percentage_alt (get id num_found_proofs) (get id num_lost_proofs) ^ "%");
log ("Number of found facts: " ^ string_of_int (get id num_found_facts));
log ("Number of lost facts: " ^ string_of_int (get id num_lost_facts));
log ("Fact found rate: " ^
- percentage_alt (get id num_found_facts) (get id num_lost_facts) ^
- "%"))
+ percentage_alt (get id num_found_facts) (get id num_lost_facts) ^ "%"))
else
()
@@ -109,13 +99,12 @@
(case Prooftab.lookup (!proof_table) (line_num, offset) of
SOME proofs =>
let
+ val thy = Proof.theory_of pre
val {context = ctxt, facts = chained_ths, goal} = Proof.goal pre
val prover = AList.lookup (op =) args "prover" |> the_default default_prover
- val params as {max_facts, ...} =
- Sledgehammer_Commands.default_params ctxt args
- val default_max_facts = Sledgehammer_Prover.default_max_facts_of_prover ctxt prover
- val is_appropriate_prop =
- Sledgehammer_Prover.is_appropriate_prop_of_prover ctxt default_prover
+ val params as {max_facts, ...} = Sledgehammer_Commands.default_params thy args
+ val default_max_facts =
+ Sledgehammer_Prover_Minimize.default_max_facts_of_prover ctxt prover
val relevance_fudge =
extract_relevance_fudge args Sledgehammer_MePo.default_relevance_fudge
val subgoal = 1
@@ -127,7 +116,6 @@
Sledgehammer_Fact.nearly_all_facts ctxt ho_atp
Sledgehammer_Fact.no_fact_override reserved css_table chained_ths
hyp_ts concl_t
- |> filter (is_appropriate_prop o prop_of o snd)
|> Sledgehammer_Fact.drop_duplicate_facts
|> Sledgehammer_MePo.mepo_suggested_facts ctxt params
(the_default default_max_facts max_facts) (SOME relevance_fudge) hyp_ts concl_t
@@ -156,8 +144,7 @@
else
let
val found_weight =
- Real.fromInt (fold (fn (n, _) =>
- Integer.add (n * n)) found_facts 0)
+ Real.fromInt (fold (fn (n, _) => Integer.add (n * n)) found_facts 0)
/ Real.fromInt (length found_facts)
|> Math.sqrt |> Real.ceil
in
@@ -178,11 +165,11 @@
fun invoke args =
let
- val (pf_args, other_args) =
- args |> List.partition (curry (op =) proof_fileK o fst)
- val proof_file = case pf_args of
- [] => error "No \"proof_file\" specified"
- | (_, s) :: _ => s
+ val (pf_args, other_args) = args |> List.partition (curry (op =) proof_fileK o fst)
+ val proof_file =
+ (case pf_args of
+ [] => error "No \"proof_file\" specified"
+ | (_, s) :: _ => s)
in Mirabelle.register (init proof_file, action other_args, done) end
end;
--- a/src/HOL/Sledgehammer.thy Fri Jan 31 10:34:20 2014 +0100
+++ b/src/HOL/Sledgehammer.thy Fri Jan 31 12:30:54 2014 +0100
@@ -27,6 +27,8 @@
ML_file "Tools/Sledgehammer/sledgehammer_isar_minimize.ML"
ML_file "Tools/Sledgehammer/sledgehammer_isar.ML"
ML_file "Tools/Sledgehammer/sledgehammer_prover.ML"
+ML_file "Tools/Sledgehammer/sledgehammer_prover_atp.ML"
+ML_file "Tools/Sledgehammer/sledgehammer_prover_smt.ML"
ML_file "Tools/Sledgehammer/sledgehammer_prover_minimize.ML"
ML_file "Tools/Sledgehammer/sledgehammer_mepo.ML"
ML_file "Tools/Sledgehammer/sledgehammer_mash.ML"
--- a/src/HOL/TPTP/mash_eval.ML Fri Jan 31 10:34:20 2014 +0100
+++ b/src/HOL/TPTP/mash_eval.ML Fri Jan 31 12:30:54 2014 +0100
@@ -46,12 +46,12 @@
mepo_file_name mash_isar_file_name mash_prover_file_name
mesh_isar_file_name mesh_prover_file_name report_file_name =
let
+ val thy = Proof_Context.theory_of ctxt
val zeros = [0, 0, 0, 0, 0, 0]
val report_path = report_file_name |> Path.explode
val _ = File.write report_path ""
fun print s = File.append report_path (s ^ "\n")
- val {provers, max_facts, slice, type_enc, lam_trans, timeout, ...} =
- default_params ctxt []
+ val {provers, max_facts, slice, type_enc, lam_trans, timeout, ...} = default_params thy []
val prover = hd provers
val slack_max_facts = generous_max_facts (the max_facts)
val lines_of = Path.explode #> try File.read_lines #> these
--- a/src/HOL/TPTP/sledgehammer_tactics.ML Fri Jan 31 10:34:20 2014 +0100
+++ b/src/HOL/TPTP/sledgehammer_tactics.ML Fri Jan 31 12:30:54 2014 +0100
@@ -21,13 +21,15 @@
open Sledgehammer_Util
open Sledgehammer_Fact
open Sledgehammer_Prover
+open Sledgehammer_Prover_Minimize
open Sledgehammer_MaSh
open Sledgehammer_Commands
fun run_prover override_params fact_override i n ctxt goal =
let
+ val thy = Proof_Context.theory_of ctxt
val mode = Normal
- val params as {provers, max_facts, ...} = default_params ctxt override_params
+ val params as {provers, max_facts, ...} = default_params thy override_params
val name = hd provers
val prover = get_prover ctxt mode name
val default_max_facts = default_max_facts_of_prover ctxt name
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_commands.ML Fri Jan 31 10:34:20 2014 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_commands.ML Fri Jan 31 12:30:54 2014 +0100
@@ -9,7 +9,7 @@
type params = Sledgehammer_Prover.params
val provers : string Unsynchronized.ref
- val default_params : Proof.context -> (string * string) list -> params
+ val default_params : theory -> (string * string) list -> params
end;
structure Sledgehammer_Commands : SLEDGEHAMMER_COMMANDS =
@@ -193,9 +193,9 @@
(* The first ATP of the list is used by Auto Sledgehammer. Because of the low
timeout, it makes sense to put E first. *)
-fun default_provers_param_value mode ctxt =
+fun default_provers_param_value mode thy =
[eN, spassN, z3N, vampireN, e_sineN, yicesN]
- |> map_filter (remotify_prover_if_not_installed ctxt)
+ |> map_filter (remotify_atp_if_not_installed thy)
(* In "try" mode, leave at least one thread to another slow tool (e.g. Nitpick) *)
|> take (Multithreading.max_threads_value () - (if mode = Try then 1 else 0))
|> implode_param
@@ -205,18 +205,14 @@
thy |> Data.map (AList.update (op =) (normalize_raw_param ctxt param))
end
-fun default_raw_params mode ctxt =
- let val thy = Proof_Context.theory_of ctxt in
- Data.get thy
- |> fold (AList.default (op =))
- [("provers", [case !provers of
- "" => default_provers_param_value mode ctxt
- | s => s]),
- ("timeout", let val timeout = Options.default_int @{option sledgehammer_timeout} in
- [if timeout <= 0 then "none"
- else string_of_int timeout]
- end)]
- end
+fun default_raw_params mode thy =
+ Data.get thy
+ |> fold (AList.default (op =))
+ [("provers", [(case !provers of "" => default_provers_param_value mode thy | s => s)]),
+ ("timeout",
+ let val timeout = Options.default_int @{option sledgehammer_timeout} in
+ [if timeout <= 0 then "none" else string_of_int timeout]
+ end)]
fun extract_params mode default_params override_params =
let
@@ -342,15 +338,16 @@
fun hammer_away override_params subcommand opt_i fact_override state =
let
+ val thy = Proof.theory_of state
val ctxt = Proof.context_of state
+
val override_params = override_params |> map (normalize_raw_param ctxt)
val _ = Isabelle_System.mkdir (Path.explode (getenv "ISABELLE_TMP"))
in
if subcommand = runN then
let val i = the_default 1 opt_i in
- run_sledgehammer (get_params Normal ctxt override_params) Normal NONE i
- fact_override (minimize_command override_params i)
- state
+ run_sledgehammer (get_params Normal thy override_params) Normal NONE i fact_override
+ (minimize_command override_params i) state
|> K ()
end
else if subcommand = minN then
@@ -358,8 +355,7 @@
val ctxt = ctxt |> Config.put instantiate_inducts false
val i = the_default 1 opt_i
val params =
- get_params Minimize ctxt (("provers", [default_minimize_prover]) ::
- override_params)
+ get_params Minimize thy (("provers", [default_minimize_prover]) :: override_params)
val goal = prop_of (#goal (Proof.goal state))
val facts = nearly_all_facts ctxt false fact_override Symtab.empty
Termtab.empty [] [] goal
@@ -371,22 +367,21 @@
supported_provers ctxt
else if subcommand = kill_allN then
(kill_provers ();
- kill_learners ctxt (get_params Normal ctxt override_params))
+ kill_learners ctxt (get_params Normal thy override_params))
else if subcommand = running_proversN then
running_provers ()
else if subcommand = unlearnN then
- mash_unlearn ctxt (get_params Normal ctxt override_params)
+ mash_unlearn ctxt (get_params Normal thy override_params)
else if subcommand = learn_isarN orelse subcommand = learn_proverN orelse
subcommand = relearn_isarN orelse subcommand = relearn_proverN then
(if subcommand = relearn_isarN orelse subcommand = relearn_proverN then
- mash_unlearn ctxt (get_params Normal ctxt override_params)
+ mash_unlearn ctxt (get_params Normal thy override_params)
else
();
mash_learn ctxt
(* TODO: Use MaSh mode instead and have the special defaults hardcoded in "get_params" *)
- (get_params Normal ctxt
- ([("timeout",
- [string_of_real default_learn_prover_timeout]),
+ (get_params Normal thy
+ ([("timeout", [string_of_real default_learn_prover_timeout]),
("slice", ["false"])] @
override_params @
[("minimize", ["true"]),
@@ -410,16 +405,12 @@
fun sledgehammer_params_trans params =
Toplevel.theory
- (fold set_default_raw_param params
- #> tap (fn thy =>
- let val ctxt = Proof_Context.init_global thy in
- writeln ("Default parameters for Sledgehammer:\n" ^
- (case rev (default_raw_params Normal ctxt) of
- [] => "none"
- | params =>
- params |> map string_of_raw_param
- |> sort_strings |> cat_lines))
- end))
+ (fold set_default_raw_param params
+ #> tap (fn thy =>
+ writeln ("Default parameters for Sledgehammer:\n" ^
+ (case rev (default_raw_params Normal thy) of
+ [] => "none"
+ | params => params |> map string_of_raw_param |> sort_strings |> cat_lines))))
val parse_query_bang = @{keyword "?"} || @{keyword "!"} || @{keyword "!!"}
val parse_key =
@@ -451,12 +442,12 @@
fun try_sledgehammer auto state =
let
- val ctxt = Proof.context_of state
+ val thy = Proof.theory_of state
val mode = if auto then Auto_Try else Try
val i = 1
in
- run_sledgehammer (get_params mode ctxt []) mode NONE i no_fact_override
- (minimize_command [] i) state
+ run_sledgehammer (get_params mode thy []) mode NONE i no_fact_override (minimize_command [] i)
+ state
end
val _ = Try.tool_setup (sledgehammerN, (40, @{option auto_sledgehammer}, try_sledgehammer))
@@ -466,8 +457,9 @@
(case try Toplevel.proof_of st of
SOME state =>
let
- val [provers_arg, isar_proofs_arg] = args;
+ val thy = Proof.theory_of state
val ctxt = Proof.context_of state
+ val [provers_arg, isar_proofs_arg] = args
val override_params =
((if provers_arg = "" then [] else [("provers", space_explode " " provers_arg)]) @
@@ -478,9 +470,9 @@
("verbose", ["false"]),
("overlord", ["false"])])
|> map (normalize_raw_param ctxt)
- val _ =
- run_sledgehammer (get_params Normal ctxt override_params) Normal (SOME output_result) 1
- no_fact_override (minimize_command override_params 1) state
+
+ val _ = run_sledgehammer (get_params Normal thy override_params) Normal
+ (SOME output_result) 1 no_fact_override (minimize_command override_params 1) state
in () end
| NONE => error "Unknown proof context"))
@@ -489,8 +481,8 @@
val _ = Isabelle_Process.protocol_command "Sledgehammer.provers"
(fn [] =>
let
- val this_ctxt = @{context}
- val provers = space_implode " " (#provers (default_params this_ctxt []))
+ val this_thy = @{theory}
+ val provers = space_implode " " (#provers (default_params this_thy []))
in Output.protocol_message Markup.sledgehammer_provers provers end)
end;
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar_annotate.ML Fri Jan 31 10:34:20 2014 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar_annotate.ML Fri Jan 31 12:30:54 2014 +0100
@@ -130,7 +130,6 @@
(t', subst)
end
-
(* (4) Typing-spot table *)
local
fun key_of_atype (TVar (z, _)) = Ord_List.insert indexname_ord z
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_prover.ML Fri Jan 31 10:34:20 2014 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_prover.ML Fri Jan 31 12:30:54 2014 +0100
@@ -69,49 +69,35 @@
val problem_prefix : string Config.T
val completish : bool Config.T
val atp_full_names : bool Config.T
- val smt_builtins : bool Config.T
- val smt_triggers : bool Config.T
- val smt_weights : bool Config.T
- val smt_weight_min_facts : int Config.T
- val smt_min_weight : int Config.T
- val smt_max_weight : int Config.T
- val smt_max_weight_index : int Config.T
- val smt_weight_curve : (int -> int) Unsynchronized.ref
- val smt_max_slices : int Config.T
- val smt_slice_fact_frac : real Config.T
- val smt_slice_time_frac : real Config.T
- val smt_slice_min_secs : int Config.T
val SledgehammerN : string
val plain_metis : reconstructor
- val select_smt_solver : string -> Proof.context -> Proof.context
+ val overlord_file_location_of_prover : string -> string * string
+ val proof_banner : mode -> string -> string
val extract_reconstructor : params -> reconstructor -> string * (string * string list) list
val is_reconstructor : string -> bool
val is_atp : theory -> string -> bool
- val is_smt_prover : Proof.context -> string -> bool
val is_ho_atp: Proof.context -> string -> bool
val is_unit_equational_atp : Proof.context -> string -> bool
- val is_prover_supported : Proof.context -> string -> bool
- val is_prover_installed : Proof.context -> string -> bool
- val remotify_prover_if_supported_and_not_already_remote :
- Proof.context -> string -> string option
- val remotify_prover_if_not_installed :
- Proof.context -> string -> string option
- val default_max_facts_of_prover : Proof.context -> string -> int
val is_unit_equality : term -> bool
val is_appropriate_prop_of_prover : Proof.context -> string -> term -> bool
- val weight_smt_fact :
- Proof.context -> int -> ((string * stature) * thm) * int
- -> (string * stature) * (int option * thm)
val supported_provers : Proof.context -> unit
val kill_provers : unit -> unit
val running_provers : unit -> unit
val messages : int option -> unit
val is_fact_chained : (('a * stature) * 'b) -> bool
+ val bunch_of_reconstructors : bool -> (bool -> string) -> reconstructor list
val filter_used_facts :
bool -> (''a * stature) list -> ((''a * stature) * 'b) list ->
((''a * stature) * 'b) list
- val isar_proof_reconstructor : Proof.context -> string -> string
- val get_prover : Proof.context -> mode -> string -> prover
+ val play_one_line_proof : mode -> bool -> bool -> Time.time -> ((string * 'a) * thm) list ->
+ Proof.state -> int -> reconstructor -> reconstructor list -> reconstructor * play_outcome
+ val remotify_atp_if_not_installed : theory -> string -> string option
+ val isar_supported_prover_of : theory -> string -> string
+ val choose_minimize_command : theory -> params -> ((string * string list) list -> string -> 'a) ->
+ string -> reconstructor * play_outcome -> 'a
+ val repair_monomorph_context : int option -> int -> int option -> int -> Proof.context ->
+ Proof.context
+ val run_reconstructor : mode -> string -> prover
end;
structure Sledgehammer_Prover : SLEDGEHAMMER_PROVER =
@@ -130,9 +116,6 @@
open Sledgehammer_Isar_Print
open Sledgehammer_Isar
-
-(** The Sledgehammer **)
-
(* Empty string means create files in Isabelle's temporary files directory. *)
val dest_dir = Attrib.setup_config_string @{binding sledgehammer_dest_dir} (K "")
val problem_prefix = Attrib.setup_config_string @{binding sledgehammer_problem_prefix} (K "prob")
@@ -143,12 +126,6 @@
provers (e.g., E). For these reason, short names are enabled by default. *)
val atp_full_names = Attrib.setup_config_bool @{binding sledgehammer_atp_full_names} (K false)
-val smt_builtins = Attrib.setup_config_bool @{binding sledgehammer_smt_builtins} (K true)
-val smt_triggers = Attrib.setup_config_bool @{binding sledgehammer_smt_triggers} (K true)
-val smt_weights = Attrib.setup_config_bool @{binding sledgehammer_smt_weights} (K true)
-val smt_weight_min_facts =
- Attrib.setup_config_int @{binding sledgehammer_smt_weight_min_facts} (K 20)
-
datatype mode = Auto_Try | Try | Normal | MaSh | Auto_Minimize | Minimize
(* Identifier that distinguishes Sledgehammer from other tools that could use
@@ -161,61 +138,28 @@
val is_atp = member (op =) o supported_atps
-val select_smt_solver = Context.proof_map o SMT_Config.select_solver
-
-fun is_smt_prover ctxt = member (op =) (SMT_Solver.available_solvers_of ctxt)
-
fun is_atp_of_format is_format ctxt name =
let val thy = Proof_Context.theory_of ctxt in
- case try (get_atp thy) name of
+ (case try (get_atp thy) name of
SOME config =>
- exists (fn (_, ((_, format, _, _, _), _)) => is_format format)
- (#best_slices (config ()) ctxt)
- | NONE => false
+ exists (fn (_, ((_, format, _, _, _), _)) => is_format format) (#best_slices (config ()) ctxt)
+ | NONE => false)
end
val is_unit_equational_atp = is_atp_of_format (curry (op =) CNF_UEQ)
val is_ho_atp = is_atp_of_format is_format_higher_order
-fun is_prover_supported ctxt =
- let val thy = Proof_Context.theory_of ctxt in
- is_reconstructor orf is_atp thy orf is_smt_prover ctxt
- end
-
-fun is_prover_installed ctxt =
- is_reconstructor orf is_smt_prover ctxt orf
- is_atp_installed (Proof_Context.theory_of ctxt)
-
-fun remotify_prover_if_supported_and_not_already_remote ctxt name =
+fun remotify_atp_if_supported_and_not_already_remote thy name =
if String.isPrefix remote_prefix name then
SOME name
else
let val remote_name = remote_prefix ^ name in
- if is_prover_supported ctxt remote_name then SOME remote_name else NONE
+ if is_atp thy remote_name then SOME remote_name else NONE
end
-fun remotify_prover_if_not_installed ctxt name =
- if is_prover_supported ctxt name andalso is_prover_installed ctxt name then
- SOME name
- else
- remotify_prover_if_supported_and_not_already_remote ctxt name
-
-fun get_slices slice slices =
- (0 upto length slices - 1) ~~ slices |> not slice ? (List.last #> single)
-
-val reconstructor_default_max_facts = 20
-
-fun slice_max_facts (_, ( ((max_facts, _), _, _, _, _), _)) = max_facts
-
-fun default_max_facts_of_prover ctxt name =
- let val thy = Proof_Context.theory_of ctxt in
- if is_reconstructor name then
- reconstructor_default_max_facts
- else if is_atp thy name then
- fold (Integer.max o slice_max_facts) (#best_slices (get_atp thy name ()) ctxt) 0
- else (* is_smt_prover ctxt name *)
- SMT_Solver.default_max_relevant ctxt name
- end
+fun remotify_atp_if_not_installed thy name =
+ if is_atp_installed thy name then SOME name
+ else remotify_atp_if_supported_and_not_already_remote thy name
fun is_if (@{const_name If}, _) = true
| is_if _ = false
@@ -256,9 +200,6 @@
fun running_provers () = Async_Manager.running_threads SledgehammerN "prover"
val messages = Async_Manager.thread_messages SledgehammerN "prover"
-
-(** problems, results, ATPs, etc. **)
-
type params =
{debug : bool,
verbose : bool,
@@ -306,43 +247,13 @@
params -> ((string * string list) list -> string -> minimize_command)
-> prover_problem -> prover_result
-(* FUDGE *)
-val smt_min_weight =
- Attrib.setup_config_int @{binding sledgehammer_smt_min_weight} (K 0)
-val smt_max_weight =
- Attrib.setup_config_int @{binding sledgehammer_smt_max_weight} (K 10)
-val smt_max_weight_index =
- Attrib.setup_config_int @{binding sledgehammer_smt_max_weight_index} (K 200)
-val smt_weight_curve = Unsynchronized.ref (fn x : int => x * x)
-
-fun smt_fact_weight ctxt j num_facts =
- if Config.get ctxt smt_weights andalso
- num_facts >= Config.get ctxt smt_weight_min_facts then
- let
- val min = Config.get ctxt smt_min_weight
- val max = Config.get ctxt smt_max_weight
- val max_index = Config.get ctxt smt_max_weight_index
- val curve = !smt_weight_curve
- in
- SOME (max - (max - min + 1) * curve (Int.max (0, max_index - j - 1))
- div curve max_index)
- end
- else
- NONE
-
-fun weight_smt_fact ctxt num_facts ((info, th), j) =
- let val thy = Proof_Context.theory_of ctxt in
- (info, (smt_fact_weight ctxt j num_facts, th |> Thm.transfer thy))
- end
-
-fun overlord_file_location_of_prover prover =
- (getenv "ISABELLE_HOME_USER", "prob_" ^ prover)
+fun overlord_file_location_of_prover prover = (getenv "ISABELLE_HOME_USER", "prob_" ^ prover)
fun proof_banner mode name =
- case mode of
+ (case mode of
Auto_Try => "Auto Sledgehammer (" ^ quote name ^ ") found a proof"
| Try => "Sledgehammer (" ^ quote name ^ ") found a proof"
- | _ => "Try this"
+ | _ => "Try this")
fun bunch_of_reconstructors needs_full_types lam_trans =
if needs_full_types then
@@ -423,91 +334,17 @@
end
end
-
-(* generic TPTP-based ATPs *)
-
-(* Too general means, positive equality literal with a variable X as one
- operand, when X does not occur properly in the other operand. This rules out
- clearly inconsistent facts such as X = a | X = b, though it by no means
- guarantees soundness. *)
-
-fun get_facts_of_filter _ [(_, facts)] = facts
- | get_facts_of_filter fact_filter factss =
- case AList.lookup (op =) factss fact_filter of
- SOME facts => facts
- | NONE => snd (hd factss)
+val canonical_isar_supported_prover = eN
-(* Unwanted equalities are those between a (bound or schematic) variable that
- does not properly occur in the second operand. *)
-val is_exhaustive_finite =
- let
- fun is_bad_equal (Var z) t =
- not (exists_subterm (fn Var z' => z = z' | _ => false) t)
- | is_bad_equal (Bound j) t = not (loose_bvar1 (t, j))
- | is_bad_equal _ _ = false
- fun do_equals t1 t2 = is_bad_equal t1 t2 orelse is_bad_equal t2 t1
- fun do_formula pos t =
- case (pos, t) of
- (_, @{const Trueprop} $ t1) => do_formula pos t1
- | (true, Const (@{const_name all}, _) $ Abs (_, _, t')) =>
- do_formula pos t'
- | (true, Const (@{const_name All}, _) $ Abs (_, _, t')) =>
- do_formula pos t'
- | (false, Const (@{const_name Ex}, _) $ Abs (_, _, t')) =>
- do_formula pos t'
- | (_, @{const "==>"} $ t1 $ t2) =>
- do_formula (not pos) t1 andalso
- (t2 = @{prop False} orelse do_formula pos t2)
- | (_, @{const HOL.implies} $ t1 $ t2) =>
- do_formula (not pos) t1 andalso
- (t2 = @{const False} orelse do_formula pos t2)
- | (_, @{const Not} $ t1) => do_formula (not pos) t1
- | (true, @{const HOL.disj} $ t1 $ t2) => forall (do_formula pos) [t1, t2]
- | (false, @{const HOL.conj} $ t1 $ t2) => forall (do_formula pos) [t1, t2]
- | (true, Const (@{const_name HOL.eq}, _) $ t1 $ t2) => do_equals t1 t2
- | (true, Const (@{const_name "=="}, _) $ t1 $ t2) => do_equals t1 t2
- | _ => false
- in do_formula true end
-
-fun has_bound_or_var_of_type pred =
- exists_subterm (fn Var (_, T as Type _) => pred T
- | Abs (_, T as Type _, _) => pred T
- | _ => false)
-
-(* Facts are forbidden to contain variables of these types. The typical reason
- is that they lead to unsoundness. Note that "unit" satisfies numerous
- equations like "?x = ()". The resulting clauses will have no type constraint,
- yielding false proofs. Even "bool" leads to many unsound proofs, though only
- for higher-order problems. *)
-
-(* Facts containing variables of type "unit" or "bool" or of the form
- "ALL x. x = A | x = B | x = C" are likely to lead to unsound proofs if types
- are omitted. *)
-fun is_dangerous_prop ctxt =
- transform_elim_prop
- #> (has_bound_or_var_of_type (is_type_surely_finite ctxt) orf
- is_exhaustive_finite)
-
-(* Important messages are important but not so important that users want to see
- them each time. *)
-val atp_important_message_keep_quotient = 25
-
-fun choose_type_enc strictness best_type_enc format =
- the_default best_type_enc
- #> type_enc_of_string strictness
- #> adjust_type_enc format
-
-fun isar_proof_reconstructor ctxt name =
- let val thy = Proof_Context.theory_of ctxt in
- if is_atp thy name then name
- else remotify_prover_if_not_installed ctxt eN |> the_default name
- end
+fun isar_supported_prover_of thy name =
+ if is_atp thy name then name
+ else the_default name (remotify_atp_if_not_installed thy canonical_isar_supported_prover)
(* FIXME: See the analogous logic in the function "maybe_minimize" in
"sledgehammer_prover_minimize.ML". *)
-fun choose_minimize_command ctxt (params as {isar_proofs, ...}) minimize_command name preplay =
+fun choose_minimize_command thy (params as {isar_proofs, ...}) minimize_command name preplay =
let
- val maybe_isar_name = name |> isar_proofs = SOME true ? isar_proof_reconstructor ctxt
+ val maybe_isar_name = name |> isar_proofs = SOME true ? isar_supported_prover_of thy
val (min_name, override_params) =
(case preplay of
(reconstr, Played _) =>
@@ -518,502 +355,15 @@
val max_fact_instances = 10 (* FUDGE *)
-fun repair_monomorph_context max_iters best_max_iters max_new_instances
- best_max_new_instances =
+fun repair_monomorph_context max_iters best_max_iters max_new_instances best_max_new_instances =
Config.put Monomorph.max_rounds (max_iters |> the_default best_max_iters)
#> Config.put Monomorph.max_new_instances
- (max_new_instances |> the_default best_max_new_instances)
+ (max_new_instances |> the_default best_max_new_instances)
#> Config.put Monomorph.max_thm_instances max_fact_instances
-fun suffix_of_mode Auto_Try = "_try"
- | suffix_of_mode Try = "_try"
- | suffix_of_mode Normal = ""
- | suffix_of_mode MaSh = ""
- | suffix_of_mode Auto_Minimize = "_min"
- | suffix_of_mode Minimize = "_min"
-
-(* Give the ATPs some slack before interrupting them the hard way. "z3_tptp" on
- Linux appears to be the only ATP that does not honor its time limit. *)
-val atp_timeout_slack = seconds 1.0
-
-val mono_max_privileged_facts = 10
-
-(* For low values of "max_facts", this fudge value ensures that most slices are
- invoked with a nontrivial amount of facts. *)
-val max_fact_factor_fudge = 5
-
-fun run_atp mode name
- ({exec, arguments, proof_delims, known_failures, prem_role, best_slices, best_max_mono_iters,
- best_max_new_mono_instances, ...} : atp_config)
- (params as {debug, verbose, overlord, type_enc, strict, lam_trans, uncurried_aliases,
- fact_filter, max_facts, max_mono_iters, max_new_mono_instances, isar_proofs, compress_isar,
- try0_isar, slice, timeout, preplay_timeout, ...})
+fun run_reconstructor mode name (params as {debug, verbose, timeout, type_enc, lam_trans, ...})
minimize_command
- ({comment, state, goal, subgoal, subgoal_count, factss, ...} : prover_problem) =
- let
- val thy = Proof.theory_of state
- val ctxt = Proof.context_of state
- val atp_mode =
- if Config.get ctxt completish then Sledgehammer_Completish
- else Sledgehammer
- val (_, hyp_ts, concl_t) = strip_subgoal goal subgoal ctxt
- val (dest_dir, problem_prefix) =
- if overlord then overlord_file_location_of_prover name
- else (Config.get ctxt dest_dir, Config.get ctxt problem_prefix)
- val problem_file_name =
- Path.basic (problem_prefix ^ (if overlord then "" else serial_string ()) ^
- suffix_of_mode mode ^ "_" ^ string_of_int subgoal)
- val prob_path =
- if dest_dir = "" then
- File.tmp_path problem_file_name
- else if File.exists (Path.explode dest_dir) then
- Path.append (Path.explode dest_dir) problem_file_name
- else
- error ("No such directory: " ^ quote dest_dir ^ ".")
- val exec = exec ()
- val command0 =
- case find_first (fn var => getenv var <> "") (fst exec) of
- SOME var =>
- let
- val pref = getenv var ^ "/"
- val paths = map (Path.explode o prefix pref) (snd exec)
- in
- case find_first File.exists paths of
- SOME path => path
- | NONE => error ("Bad executable: " ^ Path.print (hd paths) ^ ".")
- end
- | NONE => error ("The environment variable " ^ quote (List.last (fst exec)) ^
- " is not set.")
- fun split_time s =
- let
- val split = String.tokens (fn c => str c = "\n")
- val (output, t) =
- s |> split |> (try split_last #> the_default ([], "0"))
- |>> cat_lines
- fun as_num f = f >> (fst o read_int)
- val num = as_num (Scan.many1 Symbol.is_ascii_digit)
- val digit = Scan.one Symbol.is_ascii_digit
- val num3 = as_num (digit ::: digit ::: (digit >> single))
- val time = num --| Scan.$$ "." -- num3 >> (fn (a, b) => a * 1000 + b)
- val as_time =
- raw_explode #> Scan.read Symbol.stopper time #> the_default 0
- in (output, as_time t |> Time.fromMilliseconds) end
- fun run () =
- let
- (* If slicing is disabled, we expand the last slice to fill the entire
- time available. *)
- val all_slices = best_slices ctxt
- val actual_slices = get_slices slice all_slices
- fun max_facts_of_slices f slices = fold (Integer.max o slice_max_facts o f) slices 0
- val num_actual_slices = length actual_slices
- val max_fact_factor =
- Real.fromInt (case max_facts of
- NONE => max_facts_of_slices I all_slices
- | SOME max => max)
- / Real.fromInt (max_facts_of_slices snd actual_slices)
- fun monomorphize_facts facts =
- let
- val ctxt =
- ctxt
- |> repair_monomorph_context max_mono_iters
- best_max_mono_iters max_new_mono_instances
- best_max_new_mono_instances
- (* pseudo-theorem involving the same constants as the subgoal *)
- val subgoal_th =
- Logic.list_implies (hyp_ts, concl_t) |> Skip_Proof.make_thm thy
- val rths =
- facts |> chop mono_max_privileged_facts
- |>> map (pair 1 o snd)
- ||> map (pair 2 o snd)
- |> op @
- |> cons (0, subgoal_th)
- in
- Monomorph.monomorph atp_schematic_consts_of ctxt rths
- |> tl |> curry ListPair.zip (map fst facts)
- |> maps (fn (name, rths) =>
- map (pair name o zero_var_indexes o snd) rths)
- end
- fun run_slice time_left (cache_key, cache_value)
- (slice, (time_frac,
- (key as ((best_max_facts, best_fact_filter), format,
- best_type_enc, best_lam_trans,
- best_uncurried_aliases),
- extra))) =
- let
- val effective_fact_filter =
- fact_filter |> the_default best_fact_filter
- val facts = get_facts_of_filter effective_fact_filter factss
- val num_facts =
- Real.ceil (max_fact_factor * Real.fromInt best_max_facts) +
- max_fact_factor_fudge
- |> Integer.min (length facts)
- val strictness = if strict then Strict else Non_Strict
- val type_enc =
- type_enc |> choose_type_enc strictness best_type_enc format
- val sound = is_type_enc_sound type_enc
- val real_ms = Real.fromInt o Time.toMilliseconds
- val slice_timeout =
- (real_ms time_left
- |> (if slice < num_actual_slices - 1 then
- curry Real.min (time_frac * real_ms timeout)
- else
- I))
- * 0.001
- |> seconds
- val generous_slice_timeout =
- if mode = MaSh then one_day else Time.+ (slice_timeout, atp_timeout_slack)
- val _ =
- if debug then
- quote name ^ " slice #" ^ string_of_int (slice + 1) ^
- " with " ^ string_of_int num_facts ^ " fact" ^
- plural_s num_facts ^ " for " ^ string_of_time slice_timeout ^ "..."
- |> Output.urgent_message
- else
- ()
- val readable_names = not (Config.get ctxt atp_full_names)
- val lam_trans =
- case lam_trans of
- SOME s => s
- | NONE => best_lam_trans
- val uncurried_aliases =
- case uncurried_aliases of
- SOME b => b
- | NONE => best_uncurried_aliases
- val value as (atp_problem, _, fact_names, _, _) =
- if cache_key = SOME key then
- cache_value
- else
- facts
- |> not sound
- ? filter_out (is_dangerous_prop ctxt o prop_of o snd)
- |> take num_facts
- |> not (is_type_enc_polymorphic type_enc) ? monomorphize_facts
- |> map (apsnd prop_of)
- |> prepare_atp_problem ctxt format prem_role type_enc atp_mode
- lam_trans uncurried_aliases
- readable_names true hyp_ts concl_t
- fun sel_weights () = atp_problem_selection_weights atp_problem
- fun ord_info () = atp_problem_term_order_info atp_problem
- val ord = effective_term_order ctxt name
- val full_proof = isar_proofs |> the_default (mode = Minimize)
- val args =
- arguments ctxt full_proof extra slice_timeout (File.shell_path prob_path)
- (ord, ord_info, sel_weights)
- val command =
- "(exec 2>&1; " ^ File.shell_path command0 ^ " " ^ args ^ " " ^ ")"
- |> enclose "TIMEFORMAT='%3R'; { time " " ; }"
- val _ =
- atp_problem
- |> lines_of_atp_problem format ord ord_info
- |> cons ("% " ^ command ^ "\n" ^ (if comment = "" then "" else "% " ^ comment ^ "\n"))
- |> File.write_list prob_path
- val ((output, run_time), (atp_proof, outcome)) =
- TimeLimit.timeLimit generous_slice_timeout Isabelle_System.bash_output command
- |>> (if overlord then prefix ("% " ^ command ^ "\n% " ^ timestamp () ^ "\n") else I)
- |> fst |> split_time
- |> (fn accum as (output, _) =>
- (accum,
- extract_tstplike_proof_and_outcome verbose proof_delims known_failures output
- |>> atp_proof_of_tstplike_proof atp_problem
- handle UNRECOGNIZED_ATP_PROOF () => ([], SOME ProofIncomplete)))
- handle TimeLimit.TimeOut => (("", slice_timeout), ([], SOME TimedOut))
- val outcome =
- (case outcome of
- NONE =>
- (case used_facts_in_unsound_atp_proof ctxt fact_names atp_proof
- |> Option.map (sort string_ord) of
- SOME facts =>
- let val failure = UnsoundProof (is_type_enc_sound type_enc, facts) in
- if debug then (warning (string_of_atp_failure failure); NONE) else SOME failure
- end
- | NONE => NONE)
- | _ => outcome)
- in
- ((SOME key, value), (output, run_time, facts, atp_proof, outcome))
- end
- val timer = Timer.startRealTimer ()
- fun maybe_run_slice slice
- (result as (cache, (_, run_time0, _, _, SOME _))) =
- let
- val time_left = Time.- (timeout, Timer.checkRealTimer timer)
- in
- if Time.<= (time_left, Time.zeroTime) then
- result
- else
- run_slice time_left cache slice
- |> (fn (cache, (output, run_time, used_from, atp_proof, outcome)) =>
- (cache, (output, Time.+ (run_time0, run_time), used_from, atp_proof, outcome)))
- end
- | maybe_run_slice _ result = result
- in
- ((NONE, ([], Symtab.empty, Vector.fromList [], [], Symtab.empty)),
- ("", Time.zeroTime, [], [], SOME InternalError))
- |> fold maybe_run_slice actual_slices
- end
- (* If the problem file has not been exported, remove it; otherwise, export
- the proof file too. *)
- fun clean_up () =
- if dest_dir = "" then (try File.rm prob_path; ()) else ()
- fun export (_, (output, _, _, _, _)) =
- if dest_dir = "" then ()
- else File.write (Path.explode (Path.implode prob_path ^ "_proof")) output
- val ((_, (_, pool, fact_names, lifted, sym_tab)),
- (output, run_time, used_from, atp_proof, outcome)) =
- with_cleanup clean_up run () |> tap export
- val important_message =
- if mode = Normal andalso random_range 0 (atp_important_message_keep_quotient - 1) = 0
- then
- extract_important_message output
- else
- ""
- val (used_facts, preplay, message, message_tail) =
- (case outcome of
- NONE =>
- let
- val used_facts = used_facts_in_atp_proof ctxt fact_names atp_proof
- val needs_full_types = is_typed_helper_used_in_atp_proof atp_proof
- val reconstrs =
- bunch_of_reconstructors needs_full_types (lam_trans_of_atp_proof atp_proof
- o (fn desperate => if desperate then hide_lamsN else default_metis_lam_trans))
- in
- (used_facts,
- Lazy.lazy (fn () =>
- let val used_pairs = used_from |> filter_used_facts false used_facts in
- play_one_line_proof mode debug verbose preplay_timeout used_pairs state subgoal
- (hd reconstrs) reconstrs
- end),
- fn preplay =>
- let
- val _ = if verbose then Output.urgent_message "Generating proof text..." else ()
- fun isar_params () =
- let
- val metis_type_enc =
- if is_typed_helper_used_in_atp_proof atp_proof then full_typesN
- else partial_typesN
- val metis_lam_trans = lam_trans_of_atp_proof atp_proof default_metis_lam_trans
- val atp_proof =
- atp_proof
- |> termify_atp_proof ctxt pool lifted sym_tab
- |> introduce_spass_skolem
- |> factify_atp_proof fact_names hyp_ts concl_t
- in
- (verbose, metis_type_enc, metis_lam_trans, preplay_timeout, compress_isar,
- try0_isar, atp_proof, goal)
- end
- val one_line_params =
- (preplay, proof_banner mode name, used_facts,
- choose_minimize_command ctxt params minimize_command name preplay,
- subgoal, subgoal_count)
- val num_chained = length (#facts (Proof.goal state))
- in
- proof_text ctxt debug isar_proofs isar_params num_chained one_line_params
- end,
- (if verbose then "\nATP real CPU time: " ^ string_of_time run_time ^ "." else "") ^
- (if important_message <> "" then
- "\n\nImportant message from Dr. Geoff Sutcliffe:\n" ^ important_message
- else
- ""))
- end
- | SOME failure =>
- ([], Lazy.value (plain_metis, Play_Failed), fn _ => string_of_atp_failure failure, ""))
- in
- {outcome = outcome, used_facts = used_facts, used_from = used_from, run_time = run_time,
- preplay = preplay, message = message, message_tail = message_tail}
- end
-
-(* "SMT_Failure.Abnormal_Termination" carries the solver's return code. Until
- these are sorted out properly in the SMT module, we have to interpret these
- ourselves. *)
-val remote_smt_failures =
- [(2, NoLibwwwPerl),
- (22, CantConnect)]
-val z3_failures =
- [(101, OutOfResources),
- (103, MalformedInput),
- (110, MalformedInput),
- (112, TimedOut)]
-val unix_failures =
- [(138, Crashed),
- (139, Crashed)]
-val smt_failures = remote_smt_failures @ z3_failures @ unix_failures
-
-fun failure_of_smt_failure (SMT_Failure.Counterexample {is_real_cex, ...}) =
- if is_real_cex then Unprovable else GaveUp
- | failure_of_smt_failure SMT_Failure.Time_Out = TimedOut
- | failure_of_smt_failure (SMT_Failure.Abnormal_Termination code) =
- (case AList.lookup (op =) smt_failures code of
- SOME failure => failure
- | NONE => UnknownError ("Abnormal termination with exit code " ^
- string_of_int code ^ "."))
- | failure_of_smt_failure SMT_Failure.Out_Of_Memory = OutOfResources
- | failure_of_smt_failure (SMT_Failure.Other_Failure s) = UnknownError s
-
-(* FUDGE *)
-val smt_max_slices =
- Attrib.setup_config_int @{binding sledgehammer_smt_max_slices} (K 8)
-val smt_slice_fact_frac =
- Attrib.setup_config_real @{binding sledgehammer_smt_slice_fact_frac}
- (K 0.667)
-val smt_slice_time_frac =
- Attrib.setup_config_real @{binding sledgehammer_smt_slice_time_frac} (K 0.333)
-val smt_slice_min_secs =
- Attrib.setup_config_int @{binding sledgehammer_smt_slice_min_secs} (K 3)
-
-val is_boring_builtin_typ =
- not o exists_subtype (member (op =) [@{typ nat}, @{typ int}, HOLogic.realT])
-
-fun smt_filter_loop name ({debug, overlord, max_mono_iters, max_new_mono_instances, timeout, slice,
- ...} : params) state goal i =
- let
- fun repair_context ctxt =
- ctxt |> select_smt_solver name
- |> Config.put SMT_Config.verbose debug
- |> (if overlord then
- Config.put SMT_Config.debug_files
- (overlord_file_location_of_prover name
- |> (fn (path, name) => path ^ "/" ^ name))
- else
- I)
- |> Config.put SMT_Config.infer_triggers
- (Config.get ctxt smt_triggers)
- |> not (Config.get ctxt smt_builtins)
- ? (SMT_Builtin.filter_builtins is_boring_builtin_typ
- #> Config.put SMT_Config.datatypes false)
- |> repair_monomorph_context max_mono_iters default_max_mono_iters
- max_new_mono_instances default_max_new_mono_instances
- val state = Proof.map_context (repair_context) state
- val ctxt = Proof.context_of state
- val max_slices = if slice then Config.get ctxt smt_max_slices else 1
- fun do_slice timeout slice outcome0 time_so_far
- (weighted_factss as (fact_filter, weighted_facts) :: _) =
- let
- val timer = Timer.startRealTimer ()
- val slice_timeout =
- if slice < max_slices then
- let val ms = Time.toMilliseconds timeout in
- Int.min (ms,
- Int.max (1000 * Config.get ctxt smt_slice_min_secs,
- Real.ceil (Config.get ctxt smt_slice_time_frac
- * Real.fromInt ms)))
- |> Time.fromMilliseconds
- end
- else
- timeout
- val num_facts = length weighted_facts
- val _ =
- if debug then
- quote name ^ " slice " ^ string_of_int slice ^ " with " ^ string_of_int num_facts ^
- " fact" ^ plural_s num_facts ^ " for " ^ string_of_time slice_timeout
- |> Output.urgent_message
- else
- ()
- val birth = Timer.checkRealTimer timer
- val _ =
- if debug then Output.urgent_message "Invoking SMT solver..." else ()
- val (outcome, used_facts) =
- SMT_Solver.smt_filter_preprocess ctxt [] goal weighted_facts i
- |> SMT_Solver.smt_filter_apply slice_timeout
- |> (fn {outcome, used_facts} => (outcome, used_facts))
- handle exn => if Exn.is_interrupt exn then
- reraise exn
- else
- (ML_Compiler.exn_message exn
- |> SMT_Failure.Other_Failure |> SOME, [])
- val death = Timer.checkRealTimer timer
- val outcome0 = if is_none outcome0 then SOME outcome else outcome0
- val time_so_far = Time.+ (time_so_far, Time.- (death, birth))
- val too_many_facts_perhaps =
- case outcome of
- NONE => false
- | SOME (SMT_Failure.Counterexample _) => false
- | SOME SMT_Failure.Time_Out => slice_timeout <> timeout
- | SOME (SMT_Failure.Abnormal_Termination _) => true (* kind of *)
- | SOME SMT_Failure.Out_Of_Memory => true
- | SOME (SMT_Failure.Other_Failure _) => true
- val timeout = Time.- (timeout, Timer.checkRealTimer timer)
- in
- if too_many_facts_perhaps andalso slice < max_slices andalso num_facts > 0 andalso
- Time.> (timeout, Time.zeroTime) then
- let
- val new_num_facts =
- Real.ceil (Config.get ctxt smt_slice_fact_frac * Real.fromInt num_facts)
- val weighted_factss as (new_fact_filter, _) :: _ =
- weighted_factss
- |> (fn (x :: xs) => xs @ [x])
- |> app_hd (apsnd (take new_num_facts))
- val show_filter = fact_filter <> new_fact_filter
- fun num_of_facts fact_filter num_facts =
- string_of_int num_facts ^
- (if show_filter then " " ^ quote fact_filter else "") ^
- " fact" ^ plural_s num_facts
- val _ =
- if debug then
- quote name ^ " invoked with " ^
- num_of_facts fact_filter num_facts ^ ": " ^
- string_of_atp_failure (failure_of_smt_failure (the outcome)) ^
- " Retrying with " ^ num_of_facts new_fact_filter new_num_facts ^
- "..."
- |> Output.urgent_message
- else
- ()
- in
- do_slice timeout (slice + 1) outcome0 time_so_far weighted_factss
- end
- else
- {outcome = if is_none outcome then NONE else the outcome0, used_facts = used_facts,
- used_from = map (apsnd snd) weighted_facts, run_time = time_so_far}
- end
- in
- do_slice timeout 1 NONE Time.zeroTime
- end
-
-fun run_smt_solver mode name (params as {debug, verbose, preplay_timeout, ...}) minimize_command
- ({state, goal, subgoal, subgoal_count, factss, ...} : prover_problem) =
- let
- val ctxt = Proof.context_of state
- fun weight_facts facts =
- let val num_facts = length facts in
- facts ~~ (0 upto num_facts - 1)
- |> map (weight_smt_fact ctxt num_facts)
- end
- val weighted_factss = factss |> map (apsnd weight_facts)
- val {outcome, used_facts = used_pairs, used_from, run_time} =
- smt_filter_loop name params state goal subgoal weighted_factss
- val used_facts = used_pairs |> map fst
- val outcome = outcome |> Option.map failure_of_smt_failure
- val (preplay, message, message_tail) =
- case outcome of
- NONE =>
- (Lazy.lazy (fn () =>
- play_one_line_proof mode debug verbose preplay_timeout used_pairs
- state subgoal SMT
- (bunch_of_reconstructors false (fn desperate =>
- if desperate then liftingN else default_metis_lam_trans))),
- fn preplay =>
- let
- val one_line_params =
- (preplay, proof_banner mode name, used_facts,
- choose_minimize_command ctxt params minimize_command name preplay,
- subgoal, subgoal_count)
- val num_chained = length (#facts (Proof.goal state))
- in
- one_line_proof_text num_chained one_line_params
- end,
- if verbose then "\nSMT solver real CPU time: " ^ string_of_time run_time ^ "." else "")
- | SOME failure =>
- (Lazy.value (plain_metis, Play_Failed),
- fn _ => string_of_atp_failure failure, "")
- in
- {outcome = outcome, used_facts = used_facts, used_from = used_from,
- run_time = run_time, preplay = preplay, message = message,
- message_tail = message_tail}
- end
-
-fun run_reconstructor mode name
- (params as {debug, verbose, timeout, type_enc, lam_trans, ...})
- minimize_command
- ({state, subgoal, subgoal_count, factss = (_, facts) :: _, ...}
- : prover_problem) =
+ ({state, subgoal, subgoal_count, factss = (_, facts) :: _, ...} : prover_problem) =
let
val reconstr =
if name = metisN then
@@ -1052,12 +402,4 @@
end)
end
-fun get_prover ctxt mode name =
- let val thy = Proof_Context.theory_of ctxt in
- if is_reconstructor name then run_reconstructor mode name
- else if is_atp thy name then run_atp mode name (get_atp thy name ())
- else if is_smt_prover ctxt name then run_smt_solver mode name
- else error ("No such prover: " ^ name ^ ".")
- end
-
end;
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_prover_atp.ML Fri Jan 31 12:30:54 2014 +0100
@@ -0,0 +1,394 @@
+(* Title: HOL/Tools/Sledgehammer/sledgehammer_prover_atp.ML
+ Author: Fabian Immler, TU Muenchen
+ Author: Makarius
+ Author: Jasmin Blanchette, TU Muenchen
+
+ATPs as Sledgehammer provers.
+*)
+
+signature SLEDGEHAMMER_PROVER_ATP =
+sig
+ type mode = Sledgehammer_Prover.mode
+ type prover = Sledgehammer_Prover.prover
+
+ val run_atp : mode -> string -> prover
+end;
+
+structure Sledgehammer_Prover_ATP : SLEDGEHAMMER_PROVER_ATP =
+struct
+
+open ATP_Util
+open ATP_Problem
+open ATP_Proof
+open ATP_Problem_Generate
+open ATP_Proof_Reconstruct
+open ATP_Systems
+open Sledgehammer_Util
+open Sledgehammer_Reconstructor
+open Sledgehammer_Isar
+open Sledgehammer_Prover
+
+fun choose_type_enc strictness best_type_enc format =
+ the_default best_type_enc
+ #> type_enc_of_string strictness
+ #> adjust_type_enc format
+
+fun has_bound_or_var_of_type pred =
+ exists_subterm (fn Var (_, T as Type _) => pred T
+ | Abs (_, T as Type _, _) => pred T
+ | _ => false)
+
+(* Unwanted equalities are those between a (bound or schematic) variable that does not properly
+ occur in the second operand. *)
+val is_exhaustive_finite =
+ let
+ fun is_bad_equal (Var z) t =
+ not (exists_subterm (fn Var z' => z = z' | _ => false) t)
+ | is_bad_equal (Bound j) t = not (loose_bvar1 (t, j))
+ | is_bad_equal _ _ = false
+ fun do_equals t1 t2 = is_bad_equal t1 t2 orelse is_bad_equal t2 t1
+ fun do_formula pos t =
+ case (pos, t) of
+ (_, @{const Trueprop} $ t1) => do_formula pos t1
+ | (true, Const (@{const_name all}, _) $ Abs (_, _, t')) =>
+ do_formula pos t'
+ | (true, Const (@{const_name All}, _) $ Abs (_, _, t')) =>
+ do_formula pos t'
+ | (false, Const (@{const_name Ex}, _) $ Abs (_, _, t')) =>
+ do_formula pos t'
+ | (_, @{const "==>"} $ t1 $ t2) =>
+ do_formula (not pos) t1 andalso
+ (t2 = @{prop False} orelse do_formula pos t2)
+ | (_, @{const HOL.implies} $ t1 $ t2) =>
+ do_formula (not pos) t1 andalso
+ (t2 = @{const False} orelse do_formula pos t2)
+ | (_, @{const Not} $ t1) => do_formula (not pos) t1
+ | (true, @{const HOL.disj} $ t1 $ t2) => forall (do_formula pos) [t1, t2]
+ | (false, @{const HOL.conj} $ t1 $ t2) => forall (do_formula pos) [t1, t2]
+ | (true, Const (@{const_name HOL.eq}, _) $ t1 $ t2) => do_equals t1 t2
+ | (true, Const (@{const_name "=="}, _) $ t1 $ t2) => do_equals t1 t2
+ | _ => false
+ in do_formula true end
+
+(* Facts containing variables of finite types such as "unit" or "bool" or of the form
+ "ALL x. x = A | x = B | x = C" are likely to lead to untypable proofs for unsound type
+ encodings. *)
+fun is_dangerous_prop ctxt =
+ transform_elim_prop
+ #> (has_bound_or_var_of_type (is_type_surely_finite ctxt) orf is_exhaustive_finite)
+
+fun get_slices slice slices =
+ (0 upto length slices - 1) ~~ slices |> not slice ? (List.last #> single)
+
+fun get_facts_of_filter _ [(_, facts)] = facts
+ | get_facts_of_filter fact_filter factss =
+ (case AList.lookup (op =) factss fact_filter of
+ SOME facts => facts
+ | NONE => snd (hd factss))
+
+(* For low values of "max_facts", this fudge value ensures that most slices are invoked with a
+ nontrivial amount of facts. *)
+val max_fact_factor_fudge = 5
+
+val mono_max_privileged_facts = 10
+
+fun suffix_of_mode Auto_Try = "_try"
+ | suffix_of_mode Try = "_try"
+ | suffix_of_mode Normal = ""
+ | suffix_of_mode MaSh = ""
+ | suffix_of_mode Auto_Minimize = "_min"
+ | suffix_of_mode Minimize = "_min"
+
+(* Give the ATPs some slack before interrupting them the hard way. "z3_tptp" on Linux appears to be
+ the only ATP that does not honor its time limit. *)
+val atp_timeout_slack = seconds 1.0
+
+(* Important messages are important but not so important that users want to see
+ them each time. *)
+val atp_important_message_keep_quotient = 25
+
+fun run_atp mode name
+ (params as {debug, verbose, overlord, type_enc, strict, lam_trans, uncurried_aliases,
+ fact_filter, max_facts, max_mono_iters, max_new_mono_instances, isar_proofs, compress_isar,
+ try0_isar, slice, timeout, preplay_timeout, ...})
+ minimize_command
+ ({comment, state, goal, subgoal, subgoal_count, factss, ...} : prover_problem) =
+ let
+ val thy = Proof.theory_of state
+ val ctxt = Proof.context_of state
+
+ val {exec, arguments, proof_delims, known_failures, prem_role, best_slices, best_max_mono_iters,
+ best_max_new_mono_instances, ...} = get_atp thy name ()
+
+ val atp_mode = if Config.get ctxt completish then Sledgehammer_Completish else Sledgehammer
+ val (_, hyp_ts, concl_t) = strip_subgoal goal subgoal ctxt
+ val (dest_dir, problem_prefix) =
+ if overlord then overlord_file_location_of_prover name
+ else (Config.get ctxt dest_dir, Config.get ctxt problem_prefix)
+ val problem_file_name =
+ Path.basic (problem_prefix ^ (if overlord then "" else serial_string ()) ^
+ suffix_of_mode mode ^ "_" ^ string_of_int subgoal)
+ val prob_path =
+ if dest_dir = "" then
+ File.tmp_path problem_file_name
+ else if File.exists (Path.explode dest_dir) then
+ Path.append (Path.explode dest_dir) problem_file_name
+ else
+ error ("No such directory: " ^ quote dest_dir ^ ".")
+ val exec = exec ()
+ val command0 =
+ case find_first (fn var => getenv var <> "") (fst exec) of
+ SOME var =>
+ let
+ val pref = getenv var ^ "/"
+ val paths = map (Path.explode o prefix pref) (snd exec)
+ in
+ case find_first File.exists paths of
+ SOME path => path
+ | NONE => error ("Bad executable: " ^ Path.print (hd paths) ^ ".")
+ end
+ | NONE => error ("The environment variable " ^ quote (List.last (fst exec)) ^
+ " is not set.")
+
+ fun split_time s =
+ let
+ val split = String.tokens (fn c => str c = "\n")
+ val (output, t) =
+ s |> split |> (try split_last #> the_default ([], "0"))
+ |>> cat_lines
+ fun as_num f = f >> (fst o read_int)
+ val num = as_num (Scan.many1 Symbol.is_ascii_digit)
+ val digit = Scan.one Symbol.is_ascii_digit
+ val num3 = as_num (digit ::: digit ::: (digit >> single))
+ val time = num --| Scan.$$ "." -- num3 >> (fn (a, b) => a * 1000 + b)
+ val as_time =
+ raw_explode #> Scan.read Symbol.stopper time #> the_default 0
+ in (output, as_time t |> Time.fromMilliseconds) end
+
+ fun run () =
+ let
+ (* If slicing is disabled, we expand the last slice to fill the entire
+ time available. *)
+ val all_slices = best_slices ctxt
+ val actual_slices = get_slices slice all_slices
+ fun max_facts_of_slices f slices = fold (Integer.max o fst o #1 o fst o snd o f) slices 0
+ val num_actual_slices = length actual_slices
+ val max_fact_factor =
+ Real.fromInt (case max_facts of
+ NONE => max_facts_of_slices I all_slices
+ | SOME max => max)
+ / Real.fromInt (max_facts_of_slices snd actual_slices)
+ fun monomorphize_facts facts =
+ let
+ val ctxt =
+ ctxt
+ |> repair_monomorph_context max_mono_iters best_max_mono_iters max_new_mono_instances
+ best_max_new_mono_instances
+ (* pseudo-theorem involving the same constants as the subgoal *)
+ val subgoal_th =
+ Logic.list_implies (hyp_ts, concl_t) |> Skip_Proof.make_thm thy
+ val rths =
+ facts |> chop mono_max_privileged_facts
+ |>> map (pair 1 o snd)
+ ||> map (pair 2 o snd)
+ |> op @
+ |> cons (0, subgoal_th)
+ in
+ Monomorph.monomorph atp_schematic_consts_of ctxt rths
+ |> tl |> curry ListPair.zip (map fst facts)
+ |> maps (fn (name, rths) =>
+ map (pair name o zero_var_indexes o snd) rths)
+ end
+
+ fun run_slice time_left (cache_key, cache_value)
+ (slice, (time_frac,
+ (key as ((best_max_facts, best_fact_filter), format,
+ best_type_enc, best_lam_trans,
+ best_uncurried_aliases),
+ extra))) =
+ let
+ val effective_fact_filter =
+ fact_filter |> the_default best_fact_filter
+ val facts = get_facts_of_filter effective_fact_filter factss
+ val num_facts =
+ Real.ceil (max_fact_factor * Real.fromInt best_max_facts) + max_fact_factor_fudge
+ |> Integer.min (length facts)
+ val strictness = if strict then Strict else Non_Strict
+ val type_enc = type_enc |> choose_type_enc strictness best_type_enc format
+ val sound = is_type_enc_sound type_enc
+ val real_ms = Real.fromInt o Time.toMilliseconds
+ val slice_timeout =
+ (real_ms time_left
+ |> (if slice < num_actual_slices - 1 then
+ curry Real.min (time_frac * real_ms timeout)
+ else
+ I))
+ * 0.001
+ |> seconds
+ val generous_slice_timeout =
+ if mode = MaSh then one_day else Time.+ (slice_timeout, atp_timeout_slack)
+ val _ =
+ if debug then
+ quote name ^ " slice #" ^ string_of_int (slice + 1) ^
+ " with " ^ string_of_int num_facts ^ " fact" ^
+ plural_s num_facts ^ " for " ^ string_of_time slice_timeout ^ "..."
+ |> Output.urgent_message
+ else
+ ()
+ val readable_names = not (Config.get ctxt atp_full_names)
+ val lam_trans =
+ case lam_trans of
+ SOME s => s
+ | NONE => best_lam_trans
+ val uncurried_aliases =
+ case uncurried_aliases of
+ SOME b => b
+ | NONE => best_uncurried_aliases
+ val value as (atp_problem, _, fact_names, _, _) =
+ if cache_key = SOME key then
+ cache_value
+ else
+ facts
+ |> not sound ? filter_out (is_dangerous_prop ctxt o prop_of o snd)
+ |> take num_facts
+ |> not (is_type_enc_polymorphic type_enc) ? monomorphize_facts
+ |> map (apsnd prop_of)
+ |> prepare_atp_problem ctxt format prem_role type_enc atp_mode
+ lam_trans uncurried_aliases
+ readable_names true hyp_ts concl_t
+
+ fun sel_weights () = atp_problem_selection_weights atp_problem
+ fun ord_info () = atp_problem_term_order_info atp_problem
+
+ val ord = effective_term_order ctxt name
+ val full_proof = isar_proofs |> the_default (mode = Minimize)
+ val args =
+ arguments ctxt full_proof extra slice_timeout (File.shell_path prob_path)
+ (ord, ord_info, sel_weights)
+ val command =
+ "(exec 2>&1; " ^ File.shell_path command0 ^ " " ^ args ^ " " ^ ")"
+ |> enclose "TIMEFORMAT='%3R'; { time " " ; }"
+ val _ =
+ atp_problem
+ |> lines_of_atp_problem format ord ord_info
+ |> cons ("% " ^ command ^ "\n" ^ (if comment = "" then "" else "% " ^ comment ^ "\n"))
+ |> File.write_list prob_path
+ val ((output, run_time), (atp_proof, outcome)) =
+ TimeLimit.timeLimit generous_slice_timeout Isabelle_System.bash_output command
+ |>> (if overlord then prefix ("% " ^ command ^ "\n% " ^ timestamp () ^ "\n") else I)
+ |> fst |> split_time
+ |> (fn accum as (output, _) =>
+ (accum,
+ extract_tstplike_proof_and_outcome verbose proof_delims known_failures output
+ |>> atp_proof_of_tstplike_proof atp_problem
+ handle UNRECOGNIZED_ATP_PROOF () => ([], SOME ProofIncomplete)))
+ handle TimeLimit.TimeOut => (("", slice_timeout), ([], SOME TimedOut))
+ val outcome =
+ (case outcome of
+ NONE =>
+ (case used_facts_in_unsound_atp_proof ctxt fact_names atp_proof
+ |> Option.map (sort string_ord) of
+ SOME facts =>
+ let val failure = UnsoundProof (is_type_enc_sound type_enc, facts) in
+ if debug then (warning (string_of_atp_failure failure); NONE) else SOME failure
+ end
+ | NONE => NONE)
+ | _ => outcome)
+ in
+ ((SOME key, value), (output, run_time, facts, atp_proof, outcome))
+ end
+
+ val timer = Timer.startRealTimer ()
+
+ fun maybe_run_slice slice
+ (result as (cache, (_, run_time0, _, _, SOME _))) =
+ let
+ val time_left = Time.- (timeout, Timer.checkRealTimer timer)
+ in
+ if Time.<= (time_left, Time.zeroTime) then
+ result
+ else
+ run_slice time_left cache slice
+ |> (fn (cache, (output, run_time, used_from, atp_proof, outcome)) =>
+ (cache, (output, Time.+ (run_time0, run_time), used_from, atp_proof, outcome)))
+ end
+ | maybe_run_slice _ result = result
+ in
+ ((NONE, ([], Symtab.empty, Vector.fromList [], [], Symtab.empty)),
+ ("", Time.zeroTime, [], [], SOME InternalError))
+ |> fold maybe_run_slice actual_slices
+ end
+
+ (* If the problem file has not been exported, remove it; otherwise, export
+ the proof file too. *)
+ fun clean_up () =
+ if dest_dir = "" then (try File.rm prob_path; ()) else ()
+ fun export (_, (output, _, _, _, _)) =
+ if dest_dir = "" then ()
+ else File.write (Path.explode (Path.implode prob_path ^ "_proof")) output
+ val ((_, (_, pool, fact_names, lifted, sym_tab)),
+ (output, run_time, used_from, atp_proof, outcome)) =
+ with_cleanup clean_up run () |> tap export
+ val important_message =
+ if mode = Normal andalso random_range 0 (atp_important_message_keep_quotient - 1) = 0
+ then
+ extract_important_message output
+ else
+ ""
+
+ val (used_facts, preplay, message, message_tail) =
+ (case outcome of
+ NONE =>
+ let
+ val used_facts = used_facts_in_atp_proof ctxt fact_names atp_proof
+ val needs_full_types = is_typed_helper_used_in_atp_proof atp_proof
+ val reconstrs =
+ bunch_of_reconstructors needs_full_types (lam_trans_of_atp_proof atp_proof
+ o (fn desperate => if desperate then hide_lamsN else default_metis_lam_trans))
+ in
+ (used_facts,
+ Lazy.lazy (fn () =>
+ let val used_pairs = used_from |> filter_used_facts false used_facts in
+ play_one_line_proof mode debug verbose preplay_timeout used_pairs state subgoal
+ (hd reconstrs) reconstrs
+ end),
+ fn preplay =>
+ let
+ val _ = if verbose then Output.urgent_message "Generating proof text..." else ()
+ fun isar_params () =
+ let
+ val metis_type_enc =
+ if is_typed_helper_used_in_atp_proof atp_proof then full_typesN
+ else partial_typesN
+ val metis_lam_trans = lam_trans_of_atp_proof atp_proof default_metis_lam_trans
+ val atp_proof =
+ atp_proof
+ |> termify_atp_proof ctxt pool lifted sym_tab
+ |> introduce_spass_skolem
+ |> factify_atp_proof fact_names hyp_ts concl_t
+ in
+ (verbose, metis_type_enc, metis_lam_trans, preplay_timeout, compress_isar,
+ try0_isar, atp_proof, goal)
+ end
+ val one_line_params =
+ (preplay, proof_banner mode name, used_facts,
+ choose_minimize_command thy params minimize_command name preplay, subgoal,
+ subgoal_count)
+ val num_chained = length (#facts (Proof.goal state))
+ in
+ proof_text ctxt debug isar_proofs isar_params num_chained one_line_params
+ end,
+ (if verbose then "\nATP real CPU time: " ^ string_of_time run_time ^ "." else "") ^
+ (if important_message <> "" then
+ "\n\nImportant message from Dr. Geoff Sutcliffe:\n" ^ important_message
+ else
+ ""))
+ end
+ | SOME failure =>
+ ([], Lazy.value (plain_metis, Play_Failed), fn _ => string_of_atp_failure failure, ""))
+ in
+ {outcome = outcome, used_facts = used_facts, used_from = used_from, run_time = run_time,
+ preplay = preplay, message = message, message_tail = message_tail}
+ end
+
+end;
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_prover_minimize.ML Fri Jan 31 10:34:20 2014 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_prover_minimize.ML Fri Jan 31 12:30:54 2014 +0100
@@ -14,6 +14,11 @@
type params = Sledgehammer_Prover.params
type prover = Sledgehammer_Prover.prover
+ val is_prover_supported : Proof.context -> string -> bool
+ val is_prover_installed : Proof.context -> string -> bool
+ val default_max_facts_of_prover : Proof.context -> string -> int
+ val get_prover : Proof.context -> mode -> string -> prover
+
val binary_min_facts : int Config.T
val auto_minimize_min_facts : int Config.T
val auto_minimize_max_time : real Config.T
@@ -24,6 +29,7 @@
* ((reconstructor * play_outcome) Lazy.lazy * ((reconstructor * play_outcome) -> string)
* string)
val get_minimizing_prover : Proof.context -> mode -> (thm list -> unit) -> string -> prover
+
val run_minimize : params -> (thm list -> unit) -> int -> (Facts.ref * Attrib.src list) list ->
Proof.state -> unit
end;
@@ -40,6 +46,36 @@
open Sledgehammer_Reconstructor
open Sledgehammer_Isar
open Sledgehammer_Prover
+open Sledgehammer_Prover_ATP
+open Sledgehammer_Prover_SMT
+
+fun is_prover_supported ctxt =
+ let val thy = Proof_Context.theory_of ctxt in
+ is_reconstructor orf is_atp thy orf is_smt_prover ctxt
+ end
+
+fun is_prover_installed ctxt =
+ is_reconstructor orf is_smt_prover ctxt orf is_atp_installed (Proof_Context.theory_of ctxt)
+
+val reconstructor_default_max_facts = 20
+
+fun default_max_facts_of_prover ctxt name =
+ let val thy = Proof_Context.theory_of ctxt in
+ if is_reconstructor name then
+ reconstructor_default_max_facts
+ else if is_atp thy name then
+ fold (Integer.max o fst o #1 o fst o snd) (#best_slices (get_atp thy name ()) ctxt) 0
+ else (* is_smt_prover ctxt name *)
+ SMT_Solver.default_max_relevant ctxt name
+ end
+
+fun get_prover ctxt mode name =
+ let val thy = Proof_Context.theory_of ctxt in
+ if is_reconstructor name then run_reconstructor mode name
+ else if is_atp thy name then run_atp mode name
+ else if is_smt_prover ctxt name then run_smt_solver mode name
+ else error ("No such prover: " ^ name ^ ".")
+ end
(* wrapper for calling external prover *)
@@ -234,16 +270,17 @@
timeout = timeout, preplay_timeout = preplay_timeout, expect = expect}
end
-fun maybe_minimize ctxt mode do_learn name
- (params as {verbose, isar_proofs, minimize, ...})
- ({state, goal, subgoal, subgoal_count, ...} : prover_problem)
- (result as {outcome, used_facts, used_from, run_time, preplay, message,
- message_tail} : prover_result) =
+fun maybe_minimize ctxt mode do_learn name (params as {verbose, isar_proofs, minimize, ...})
+ ({state, goal, subgoal, subgoal_count, ...} : prover_problem)
+ (result as {outcome, used_facts, used_from, run_time, preplay, message, message_tail} :
+ prover_result) =
if is_some outcome orelse null used_facts then
result
else
let
+ val thy = Proof_Context.theory_of ctxt
val num_facts = length used_facts
+
val ((perhaps_minimize, (minimize_name, params)), preplay) =
if mode = Normal then
if num_facts >= Config.get ctxt auto_minimize_min_facts then
@@ -261,7 +298,7 @@
if isar_proofs = SOME true then
(* Cheat: Assume the selected ATP is as fast as "metis" for the goal it proved
itself. *)
- (can_min_fast_enough timeout, (isar_proof_reconstructor ctxt name, params))
+ (can_min_fast_enough timeout, (isar_supported_prover_of thy name, params))
else if can_min_fast_enough timeout then
(true, extract_reconstructor params reconstr
||> (fn override_params =>
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_prover_smt.ML Fri Jan 31 12:30:54 2014 +0100
@@ -0,0 +1,268 @@
+(* Title: HOL/Tools/Sledgehammer/sledgehammer_prover_smt.ML
+ Author: Fabian Immler, TU Muenchen
+ Author: Makarius
+ Author: Jasmin Blanchette, TU Muenchen
+
+SMT solvers as Sledgehammer provers.
+*)
+
+signature SLEDGEHAMMER_PROVER_SMT =
+sig
+ type stature = ATP_Problem_Generate.stature
+ type mode = Sledgehammer_Prover.mode
+ type prover = Sledgehammer_Prover.prover
+
+ val smt_builtins : bool Config.T
+ val smt_triggers : bool Config.T
+ val smt_weights : bool Config.T
+ val smt_weight_min_facts : int Config.T
+ val smt_min_weight : int Config.T
+ val smt_max_weight : int Config.T
+ val smt_max_weight_index : int Config.T
+ val smt_weight_curve : (int -> int) Unsynchronized.ref
+ val smt_max_slices : int Config.T
+ val smt_slice_fact_frac : real Config.T
+ val smt_slice_time_frac : real Config.T
+ val smt_slice_min_secs : int Config.T
+
+ val select_smt_solver : string -> Proof.context -> Proof.context
+ val is_smt_prover : Proof.context -> string -> bool
+ val weight_smt_fact : Proof.context -> int -> ((string * stature) * thm) * int
+ -> (string * stature) * (int option * thm)
+ val run_smt_solver : mode -> string -> prover
+end;
+
+structure Sledgehammer_Prover_SMT : SLEDGEHAMMER_PROVER_SMT =
+struct
+
+open ATP_Proof
+open ATP_Util
+open ATP_Systems
+open ATP_Problem_Generate
+open ATP_Proof_Reconstruct
+open Sledgehammer_Util
+open Sledgehammer_Reconstructor
+open Sledgehammer_Isar_Print
+open Sledgehammer_Prover
+
+val smt_builtins = Attrib.setup_config_bool @{binding sledgehammer_smt_builtins} (K true)
+val smt_triggers = Attrib.setup_config_bool @{binding sledgehammer_smt_triggers} (K true)
+val smt_weights = Attrib.setup_config_bool @{binding sledgehammer_smt_weights} (K true)
+val smt_weight_min_facts =
+ Attrib.setup_config_int @{binding sledgehammer_smt_weight_min_facts} (K 20)
+
+val select_smt_solver = Context.proof_map o SMT_Config.select_solver
+
+fun is_smt_prover ctxt = member (op =) (SMT_Solver.available_solvers_of ctxt)
+
+(* FUDGE *)
+val smt_min_weight =
+ Attrib.setup_config_int @{binding sledgehammer_smt_min_weight} (K 0)
+val smt_max_weight =
+ Attrib.setup_config_int @{binding sledgehammer_smt_max_weight} (K 10)
+val smt_max_weight_index =
+ Attrib.setup_config_int @{binding sledgehammer_smt_max_weight_index} (K 200)
+val smt_weight_curve = Unsynchronized.ref (fn x : int => x * x)
+
+fun smt_fact_weight ctxt j num_facts =
+ if Config.get ctxt smt_weights andalso
+ num_facts >= Config.get ctxt smt_weight_min_facts then
+ let
+ val min = Config.get ctxt smt_min_weight
+ val max = Config.get ctxt smt_max_weight
+ val max_index = Config.get ctxt smt_max_weight_index
+ val curve = !smt_weight_curve
+ in
+ SOME (max - (max - min + 1) * curve (Int.max (0, max_index - j - 1))
+ div curve max_index)
+ end
+ else
+ NONE
+
+fun weight_smt_fact ctxt num_facts ((info, th), j) =
+ let val thy = Proof_Context.theory_of ctxt in
+ (info, (smt_fact_weight ctxt j num_facts, th |> Thm.transfer thy))
+ end
+
+(* "SMT_Failure.Abnormal_Termination" carries the solver's return code. Until these are sorted out
+ properly in the SMT module, we must interpret these here. *)
+val z3_failures =
+ [(101, OutOfResources),
+ (103, MalformedInput),
+ (110, MalformedInput),
+ (112, TimedOut)]
+val unix_failures =
+ [(138, Crashed),
+ (139, Crashed)]
+val smt_failures = z3_failures @ unix_failures
+
+fun failure_of_smt_failure (SMT_Failure.Counterexample {is_real_cex, ...}) =
+ if is_real_cex then Unprovable else GaveUp
+ | failure_of_smt_failure SMT_Failure.Time_Out = TimedOut
+ | failure_of_smt_failure (SMT_Failure.Abnormal_Termination code) =
+ (case AList.lookup (op =) smt_failures code of
+ SOME failure => failure
+ | NONE => UnknownError ("Abnormal termination with exit code " ^ string_of_int code ^ "."))
+ | failure_of_smt_failure SMT_Failure.Out_Of_Memory = OutOfResources
+ | failure_of_smt_failure (SMT_Failure.Other_Failure s) = UnknownError s
+
+(* FUDGE *)
+val smt_max_slices = Attrib.setup_config_int @{binding sledgehammer_smt_max_slices} (K 8)
+val smt_slice_fact_frac =
+ Attrib.setup_config_real @{binding sledgehammer_smt_slice_fact_frac} (K 0.667)
+val smt_slice_time_frac =
+ Attrib.setup_config_real @{binding sledgehammer_smt_slice_time_frac} (K 0.333)
+val smt_slice_min_secs = Attrib.setup_config_int @{binding sledgehammer_smt_slice_min_secs} (K 3)
+
+val is_boring_builtin_typ =
+ not o exists_subtype (member (op =) [@{typ nat}, @{typ int}, HOLogic.realT])
+
+fun smt_filter_loop name ({debug, overlord, max_mono_iters, max_new_mono_instances, timeout, slice,
+ ...} : params) state goal i =
+ let
+ fun repair_context ctxt =
+ ctxt |> select_smt_solver name
+ |> Config.put SMT_Config.verbose debug
+ |> (if overlord then
+ Config.put SMT_Config.debug_files
+ (overlord_file_location_of_prover name |> (fn (path, name) => path ^ "/" ^ name))
+ else
+ I)
+ |> Config.put SMT_Config.infer_triggers (Config.get ctxt smt_triggers)
+ |> not (Config.get ctxt smt_builtins)
+ ? (SMT_Builtin.filter_builtins is_boring_builtin_typ
+ #> Config.put SMT_Config.datatypes false)
+ |> repair_monomorph_context max_mono_iters default_max_mono_iters max_new_mono_instances
+ default_max_new_mono_instances
+
+ val state = Proof.map_context (repair_context) state
+ val ctxt = Proof.context_of state
+ val max_slices = if slice then Config.get ctxt smt_max_slices else 1
+
+ fun do_slice timeout slice outcome0 time_so_far
+ (weighted_factss as (fact_filter, weighted_facts) :: _) =
+ let
+ val timer = Timer.startRealTimer ()
+ val slice_timeout =
+ if slice < max_slices then
+ let val ms = Time.toMilliseconds timeout in
+ Int.min (ms, Int.max (1000 * Config.get ctxt smt_slice_min_secs,
+ Real.ceil (Config.get ctxt smt_slice_time_frac * Real.fromInt ms)))
+ |> Time.fromMilliseconds
+ end
+ else
+ timeout
+ val num_facts = length weighted_facts
+ val _ =
+ if debug then
+ quote name ^ " slice " ^ string_of_int slice ^ " with " ^ string_of_int num_facts ^
+ " fact" ^ plural_s num_facts ^ " for " ^ string_of_time slice_timeout
+ |> Output.urgent_message
+ else
+ ()
+ val birth = Timer.checkRealTimer timer
+ val _ = if debug then Output.urgent_message "Invoking SMT solver..." else ()
+
+ val (outcome, used_facts) =
+ SMT_Solver.smt_filter_preprocess ctxt [] goal weighted_facts i
+ |> SMT_Solver.smt_filter_apply slice_timeout
+ |> (fn {outcome, used_facts} => (outcome, used_facts))
+ handle exn =>
+ if Exn.is_interrupt exn then reraise exn
+ else (ML_Compiler.exn_message exn |> SMT_Failure.Other_Failure |> SOME, [])
+
+ val death = Timer.checkRealTimer timer
+ val outcome0 = if is_none outcome0 then SOME outcome else outcome0
+ val time_so_far = Time.+ (time_so_far, Time.- (death, birth))
+
+ val too_many_facts_perhaps =
+ (case outcome of
+ NONE => false
+ | SOME (SMT_Failure.Counterexample _) => false
+ | SOME SMT_Failure.Time_Out => slice_timeout <> timeout
+ | SOME (SMT_Failure.Abnormal_Termination _) => true (* kind of *)
+ | SOME SMT_Failure.Out_Of_Memory => true
+ | SOME (SMT_Failure.Other_Failure _) => true)
+
+ val timeout = Time.- (timeout, Timer.checkRealTimer timer)
+ in
+ if too_many_facts_perhaps andalso slice < max_slices andalso num_facts > 0 andalso
+ Time.> (timeout, Time.zeroTime) then
+ let
+ val new_num_facts =
+ Real.ceil (Config.get ctxt smt_slice_fact_frac * Real.fromInt num_facts)
+ val weighted_factss as (new_fact_filter, _) :: _ =
+ weighted_factss
+ |> (fn (x :: xs) => xs @ [x])
+ |> app_hd (apsnd (take new_num_facts))
+ val show_filter = fact_filter <> new_fact_filter
+
+ fun num_of_facts fact_filter num_facts =
+ string_of_int num_facts ^ (if show_filter then " " ^ quote fact_filter else "") ^
+ " fact" ^ plural_s num_facts
+
+ val _ =
+ if debug then
+ quote name ^ " invoked with " ^
+ num_of_facts fact_filter num_facts ^ ": " ^
+ string_of_atp_failure (failure_of_smt_failure (the outcome)) ^
+ " Retrying with " ^ num_of_facts new_fact_filter new_num_facts ^
+ "..."
+ |> Output.urgent_message
+ else
+ ()
+ in
+ do_slice timeout (slice + 1) outcome0 time_so_far weighted_factss
+ end
+ else
+ {outcome = if is_none outcome then NONE else the outcome0, used_facts = used_facts,
+ used_from = map (apsnd snd) weighted_facts, run_time = time_so_far}
+ end
+ in
+ do_slice timeout 1 NONE Time.zeroTime
+ end
+
+fun run_smt_solver mode name (params as {debug, verbose, preplay_timeout, ...}) minimize_command
+ ({state, goal, subgoal, subgoal_count, factss, ...} : prover_problem) =
+ let
+ val thy = Proof.theory_of state
+ val ctxt = Proof.context_of state
+
+ fun weight_facts facts =
+ let val num_facts = length facts in
+ map (weight_smt_fact ctxt num_facts) (facts ~~ (0 upto num_facts - 1))
+ end
+
+ val weighted_factss = factss |> map (apsnd weight_facts)
+ val {outcome, used_facts = used_pairs, used_from, run_time} =
+ smt_filter_loop name params state goal subgoal weighted_factss
+ val used_facts = used_pairs |> map fst
+ val outcome = outcome |> Option.map failure_of_smt_failure
+
+ val (preplay, message, message_tail) =
+ (case outcome of
+ NONE =>
+ (Lazy.lazy (fn () =>
+ play_one_line_proof mode debug verbose preplay_timeout used_pairs state subgoal SMT
+ (bunch_of_reconstructors false (fn desperate =>
+ if desperate then liftingN else default_metis_lam_trans))),
+ fn preplay =>
+ let
+ val one_line_params =
+ (preplay, proof_banner mode name, used_facts,
+ choose_minimize_command thy params minimize_command name preplay, subgoal,
+ subgoal_count)
+ val num_chained = length (#facts (Proof.goal state))
+ in
+ one_line_proof_text num_chained one_line_params
+ end,
+ if verbose then "\nSMT solver real CPU time: " ^ string_of_time run_time ^ "." else "")
+ | SOME failure =>
+ (Lazy.value (plain_metis, Play_Failed), fn _ => string_of_atp_failure failure, ""))
+ in
+ {outcome = outcome, used_facts = used_facts, used_from = used_from,
+ run_time = run_time, preplay = preplay, message = message,
+ message_tail = message_tail}
+ end
+
+end;