# HG changeset patch # User blanchet # Date 1291843072 -3600 # Node ID d7b5fd465198fba26b72899cca7c1eb3bc15350c # Parent b4cccce25d9a19e818c95975c1b23185e50a4193 split "Sledgehammer" module into two parts, to resolve forthcoming dependency problems diff -r b4cccce25d9a -r d7b5fd465198 src/HOL/IsaMakefile --- a/src/HOL/IsaMakefile Wed Dec 08 18:07:04 2010 +0100 +++ b/src/HOL/IsaMakefile Wed Dec 08 22:17:52 2010 +0100 @@ -344,12 +344,13 @@ Tools/record.ML \ Tools/semiring_normalizer.ML \ Tools/Sledgehammer/async_manager.ML \ - Tools/Sledgehammer/sledgehammer.ML \ + Tools/Sledgehammer/sledgehammer_atp_reconstruct.ML \ + Tools/Sledgehammer/sledgehammer_atp_translate.ML \ Tools/Sledgehammer/sledgehammer_filter.ML \ Tools/Sledgehammer/sledgehammer_minimize.ML \ Tools/Sledgehammer/sledgehammer_isar.ML \ - Tools/Sledgehammer/sledgehammer_atp_reconstruct.ML \ - Tools/Sledgehammer/sledgehammer_atp_translate.ML \ + Tools/Sledgehammer/sledgehammer_provers.ML \ + Tools/Sledgehammer/sledgehammer_run.ML \ Tools/Sledgehammer/sledgehammer_util.ML \ Tools/smallvalue_generators.ML \ Tools/SMT/smtlib_interface.ML \ diff -r b4cccce25d9a -r d7b5fd465198 src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML --- a/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML Wed Dec 08 18:07:04 2010 +0100 +++ b/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML Wed Dec 08 22:17:52 2010 +0100 @@ -319,7 +319,8 @@ fun default_prover_name () = hd (#provers (Sledgehammer_Isar.default_params ctxt [])) handle Empty => error "No ATP available." - fun get_prover name = (name, Sledgehammer.get_prover ctxt false name) + fun get_prover name = + (name, Sledgehammer_Provers.get_prover ctxt false name) in (case AList.lookup (op =) args proverK of SOME name => get_prover name @@ -344,22 +345,22 @@ val {context = ctxt, facts = chained_ths, goal} = Proof.goal st val thy = ProofContext.theory_of ctxt val i = 1 - fun change_dir (SOME dir) = Config.put Sledgehammer.dest_dir dir + fun change_dir (SOME dir) = Config.put Sledgehammer_Provers.dest_dir dir | change_dir NONE = I val st' = st |> Proof.map_context (change_dir dir - #> Config.put Sledgehammer.measure_run_time true) + #> Config.put Sledgehammer_Provers.measure_run_time true) val params as {full_types, relevance_thresholds, max_relevant, ...} = Sledgehammer_Isar.default_params ctxt [("verbose", "true"), ("timeout", Int.toString timeout)] val default_max_relevant = - Sledgehammer.default_max_relevant_for_prover ctxt prover_name + Sledgehammer_Provers.default_max_relevant_for_prover ctxt prover_name val is_built_in_const = - Sledgehammer.is_built_in_const_for_prover ctxt prover_name + Sledgehammer_Provers.is_built_in_const_for_prover ctxt prover_name val relevance_fudge = - Sledgehammer.relevance_fudge_for_prover ctxt prover_name + Sledgehammer_Provers.relevance_fudge_for_prover ctxt prover_name val relevance_override = {add = [], del = [], only = false} val (_, hyp_ts, concl_t) = Sledgehammer_Util.strip_subgoal goal i val facts = @@ -369,13 +370,13 @@ val problem = {state = st', goal = goal, subgoal = i, subgoal_count = Sledgehammer_Util.subgoal_count st, - facts = facts |> map Sledgehammer.Untranslated} + facts = facts |> map Sledgehammer_Provers.Untranslated} val time_limit = (case hard_timeout of NONE => I | SOME secs => TimeLimit.timeLimit (Time.fromSeconds secs)) val ({outcome, message, used_facts, run_time_in_msecs, ...} - : Sledgehammer.prover_result, + : Sledgehammer_Provers.prover_result, time_isa) = time_limit (Mirabelle.cpu_time (prover params (K ""))) problem val time_prover = run_time_in_msecs |> the_default ~1 diff -r b4cccce25d9a -r d7b5fd465198 src/HOL/Mirabelle/Tools/mirabelle_sledgehammer_filter.ML --- a/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer_filter.ML Wed Dec 08 18:07:04 2010 +0100 +++ b/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer_filter.ML Wed Dec 08 22:17:52 2010 +0100 @@ -109,12 +109,12 @@ val prover = AList.lookup (op =) args "prover" |> the_default default_prover val default_max_relevant = - Sledgehammer.default_max_relevant_for_prover ctxt prover + Sledgehammer_Provers.default_max_relevant_for_prover ctxt prover val is_built_in_const = - Sledgehammer.is_built_in_const_for_prover ctxt default_prover + Sledgehammer_Provers.is_built_in_const_for_prover ctxt default_prover val relevance_fudge = extract_relevance_fudge args - (Sledgehammer.relevance_fudge_for_prover ctxt prover) + (Sledgehammer_Provers.relevance_fudge_for_prover ctxt prover) val relevance_override = {add = [], del = [], only = false} val {relevance_thresholds, full_types, max_relevant, ...} = Sledgehammer_Isar.default_params ctxt args diff -r b4cccce25d9a -r d7b5fd465198 src/HOL/Mirabelle/Tools/sledgehammer_tactic.ML --- a/src/HOL/Mirabelle/Tools/sledgehammer_tactic.ML Wed Dec 08 18:07:04 2010 +0100 +++ b/src/HOL/Mirabelle/Tools/sledgehammer_tactic.ML Wed Dec 08 22:17:52 2010 +0100 @@ -22,12 +22,13 @@ @ [("timeout", Int.toString (Time.toSeconds timeout))]) @ [("overlord", "true")] |> Sledgehammer_Isar.default_params ctxt - val prover = Sledgehammer.get_prover ctxt false name + val prover = Sledgehammer_Provers.get_prover ctxt false name val default_max_relevant = - Sledgehammer.default_max_relevant_for_prover ctxt name + Sledgehammer_Provers.default_max_relevant_for_prover ctxt name val is_built_in_const = - Sledgehammer.is_built_in_const_for_prover ctxt name - val relevance_fudge = Sledgehammer.relevance_fudge_for_prover ctxt name + Sledgehammer_Provers.is_built_in_const_for_prover ctxt name + val relevance_fudge = + Sledgehammer_Provers.relevance_fudge_for_prover ctxt name val relevance_override = {add = [], del = [], only = false} val (_, hyp_ts, concl_t) = Sledgehammer_Util.strip_subgoal goal i val facts = @@ -43,7 +44,7 @@ (prop_of goal)) val problem = {state = Proof.init ctxt, goal = goal, subgoal = i, - subgoal_count = n, facts = map Sledgehammer.Untranslated facts} + subgoal_count = n, facts = map Sledgehammer_Provers.Untranslated facts} in (case prover params (K "") problem of {outcome = NONE, used_facts, ...} => used_facts |> map fst |> SOME diff -r b4cccce25d9a -r d7b5fd465198 src/HOL/Sledgehammer.thy --- a/src/HOL/Sledgehammer.thy Wed Dec 08 18:07:04 2010 +0100 +++ b/src/HOL/Sledgehammer.thy Wed Dec 08 22:17:52 2010 +0100 @@ -13,8 +13,9 @@ "Tools/Sledgehammer/sledgehammer_filter.ML" "Tools/Sledgehammer/sledgehammer_atp_translate.ML" "Tools/Sledgehammer/sledgehammer_atp_reconstruct.ML" - "Tools/Sledgehammer/sledgehammer.ML" + "Tools/Sledgehammer/sledgehammer_provers.ML" "Tools/Sledgehammer/sledgehammer_minimize.ML" + "Tools/Sledgehammer/sledgehammer_run.ML" "Tools/Sledgehammer/sledgehammer_isar.ML" begin diff -r b4cccce25d9a -r d7b5fd465198 src/HOL/Tools/Sledgehammer/sledgehammer.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer.ML Wed Dec 08 18:07:04 2010 +0100 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,730 +0,0 @@ -(* Title: HOL/Tools/Sledgehammer/sledgehammer.ML - Author: Fabian Immler, TU Muenchen - Author: Makarius - Author: Jasmin Blanchette, TU Muenchen - -Sledgehammer's heart. -*) - -signature SLEDGEHAMMER = -sig - type failure = ATP_Proof.failure - type locality = Sledgehammer_Filter.locality - type relevance_fudge = Sledgehammer_Filter.relevance_fudge - type relevance_override = Sledgehammer_Filter.relevance_override - type translated_formula = Sledgehammer_ATP_Translate.translated_formula - type minimize_command = Sledgehammer_ATP_Reconstruct.minimize_command - - type params = - {blocking: bool, - debug: bool, - verbose: bool, - overlord: bool, - provers: string list, - full_types: bool, - explicit_apply: bool, - relevance_thresholds: real * real, - max_relevant: int option, - isar_proof: bool, - isar_shrink_factor: int, - timeout: Time.time, - expect: string} - - datatype fact = - Untranslated of (string * locality) * thm | - Translated of term * ((string * locality) * translated_formula) option - - type prover_problem = - {state: Proof.state, - goal: thm, - subgoal: int, - subgoal_count: int, - facts: fact list} - - type prover_result = - {outcome: failure option, - used_facts: (string * locality) list, - run_time_in_msecs: int option, - message: string} - - type prover = params -> minimize_command -> prover_problem -> prover_result - - val is_prover_available : Proof.context -> string -> bool - val is_prover_installed : Proof.context -> string -> bool - val default_max_relevant_for_prover : Proof.context -> string -> int - val is_built_in_const_for_prover : - Proof.context -> string -> string * typ -> term list -> bool - val relevance_fudge_for_prover : Proof.context -> string -> relevance_fudge - val dest_dir : string Config.T - val problem_prefix : string Config.T - val measure_run_time : bool Config.T - val available_provers : Proof.context -> unit - val kill_provers : unit -> unit - val running_provers : unit -> unit - val messages : int option -> unit - val get_prover : Proof.context -> bool -> string -> prover - val run_sledgehammer : - params -> bool -> int -> relevance_override -> (string -> minimize_command) - -> Proof.state -> bool * Proof.state - val setup : theory -> theory -end; - -structure Sledgehammer : SLEDGEHAMMER = -struct - -open ATP_Problem -open ATP_Proof -open ATP_Systems -open Metis_Translate -open Sledgehammer_Util -open Sledgehammer_Filter -open Sledgehammer_ATP_Translate -open Sledgehammer_ATP_Reconstruct - - -(** The Sledgehammer **) - -(* Identifier to distinguish Sledgehammer from other tools using - "Async_Manager". *) -val das_Tool = "Sledgehammer" - -fun is_smt_prover ctxt name = - let val smts = SMT_Solver.available_solvers_of ctxt in - case try (unprefix remote_prefix) name of - SOME suffix => member (op =) smts suffix andalso - SMT_Solver.is_remotely_available ctxt suffix - | NONE => member (op =) smts name - end - -fun is_prover_available ctxt name = - let val thy = ProofContext.theory_of ctxt in - is_smt_prover ctxt name orelse member (op =) (available_atps thy) name - end - -fun is_prover_installed ctxt name = - let val thy = ProofContext.theory_of ctxt in - if is_smt_prover ctxt name then - String.isPrefix remote_prefix name orelse - SMT_Solver.is_locally_installed ctxt name - else - is_atp_installed thy name - end - -fun available_smt_solvers ctxt = - let val smts = SMT_Solver.available_solvers_of ctxt in - smts @ map (prefix remote_prefix) - (filter (SMT_Solver.is_remotely_available ctxt) smts) - end - -(* FUDGE *) -val auto_max_relevant_divisor = 2 - -fun default_max_relevant_for_prover ctxt name = - let val thy = ProofContext.theory_of ctxt in - if is_smt_prover ctxt name then - SMT_Solver.default_max_relevant ctxt - (perhaps (try (unprefix remote_prefix)) name) - else - #default_max_relevant (get_atp thy name) - end - -(* These are typically simplified away by "Meson.presimplify". Equality is - handled specially via "fequal". *) -val atp_irrelevant_consts = - [@{const_name False}, @{const_name True}, @{const_name If}, @{const_name Let}, - @{const_name HOL.eq}] - -fun is_built_in_const_for_prover ctxt name (s, T) args = - if is_smt_prover ctxt name then SMT_Builtin.is_builtin_ext ctxt (s, T) args - else member (op =) atp_irrelevant_consts s - -(* FUDGE *) -val atp_relevance_fudge = - {worse_irrel_freq = 100.0, - higher_order_irrel_weight = 1.05, - abs_rel_weight = 0.5, - abs_irrel_weight = 2.0, - skolem_irrel_weight = 0.75, - theory_const_rel_weight = 0.5, - theory_const_irrel_weight = 0.25, - intro_bonus = 0.15, - elim_bonus = 0.15, - simp_bonus = 0.15, - local_bonus = 0.55, - assum_bonus = 1.05, - chained_bonus = 1.5, - max_imperfect = 11.5, - max_imperfect_exp = 1.0, - threshold_divisor = 2.0, - ridiculous_threshold = 0.1} - -(* FUDGE (FIXME) *) -val smt_relevance_fudge = - {worse_irrel_freq = #worse_irrel_freq atp_relevance_fudge, - higher_order_irrel_weight = #higher_order_irrel_weight atp_relevance_fudge, - abs_rel_weight = #abs_rel_weight atp_relevance_fudge, - abs_irrel_weight = #abs_irrel_weight atp_relevance_fudge, - skolem_irrel_weight = #skolem_irrel_weight atp_relevance_fudge, - theory_const_rel_weight = #theory_const_rel_weight atp_relevance_fudge, - theory_const_irrel_weight = #theory_const_irrel_weight atp_relevance_fudge, - intro_bonus = #intro_bonus atp_relevance_fudge, - elim_bonus = #elim_bonus atp_relevance_fudge, - simp_bonus = #simp_bonus atp_relevance_fudge, - local_bonus = #local_bonus atp_relevance_fudge, - assum_bonus = #assum_bonus atp_relevance_fudge, - chained_bonus = #chained_bonus atp_relevance_fudge, - max_imperfect = #max_imperfect atp_relevance_fudge, - max_imperfect_exp = #max_imperfect_exp atp_relevance_fudge, - threshold_divisor = #threshold_divisor atp_relevance_fudge, - ridiculous_threshold = #ridiculous_threshold atp_relevance_fudge} - -fun relevance_fudge_for_prover ctxt name = - if is_smt_prover ctxt name then smt_relevance_fudge else atp_relevance_fudge - -fun available_provers ctxt = - let - val thy = ProofContext.theory_of ctxt - val (remote_provers, local_provers) = - sort_strings (available_atps thy) @ - sort_strings (available_smt_solvers ctxt) - |> List.partition (String.isPrefix remote_prefix) - in - Output.urgent_message ("Available provers: " ^ - commas (local_provers @ remote_provers) ^ ".") - end - -fun kill_provers () = Async_Manager.kill_threads das_Tool "provers" -fun running_provers () = Async_Manager.running_threads das_Tool "provers" -val messages = Async_Manager.thread_messages das_Tool "prover" - -(** problems, results, ATPs, etc. **) - -type params = - {blocking: bool, - debug: bool, - verbose: bool, - overlord: bool, - provers: string list, - full_types: bool, - explicit_apply: bool, - relevance_thresholds: real * real, - max_relevant: int option, - isar_proof: bool, - isar_shrink_factor: int, - timeout: Time.time, - expect: string} - -datatype fact = - Untranslated of (string * locality) * thm | - Translated of term * ((string * locality) * translated_formula) option - -type prover_problem = - {state: Proof.state, - goal: thm, - subgoal: int, - subgoal_count: int, - facts: fact list} - -type prover_result = - {outcome: failure option, - message: string, - used_facts: (string * locality) list, - run_time_in_msecs: int option} - -type prover = params -> minimize_command -> prover_problem -> prover_result - -(* configuration attributes *) - -val (dest_dir, dest_dir_setup) = - Attrib.config_string "sledgehammer_dest_dir" (K "") - (* Empty string means create files in Isabelle's temporary files directory. *) - -val (problem_prefix, problem_prefix_setup) = - Attrib.config_string "sledgehammer_problem_prefix" (K "prob") - -val (measure_run_time, measure_run_time_setup) = - Attrib.config_bool "sledgehammer_measure_run_time" (K false) - -fun with_path cleanup after f path = - Exn.capture f path - |> tap (fn _ => cleanup path) - |> Exn.release - |> tap (after path) - -fun prover_description ctxt ({blocking, verbose, ...} : params) name num_facts i - n goal = - quote name ^ - (if verbose then - " with " ^ string_of_int num_facts ^ " fact" ^ plural_s num_facts - else - "") ^ - " on " ^ (if n = 1 then "goal" else "subgoal " ^ string_of_int i) ^ ":" ^ - (if blocking then - "" - else - "\n" ^ Syntax.string_of_term ctxt (Thm.term_of (Thm.cprem_of goal i))) - -fun proof_banner auto = - if auto then "Auto Sledgehammer found a proof" else "Try this command" - -(* generic TPTP-based ATPs *) - -fun dest_Untranslated (Untranslated p) = p - | dest_Untranslated (Translated _) = raise Fail "dest_Untranslated" -fun translated_fact ctxt (Untranslated p) = translate_fact ctxt p - | translated_fact _ (Translated p) = p -fun fact_name (Untranslated ((name, _), _)) = SOME name - | fact_name (Translated (_, p)) = Option.map (fst o fst) p - -fun int_opt_add (SOME m) (SOME n) = SOME (m + n) - | int_opt_add _ _ = NONE - -(* Important messages are important but not so important that users want to see - them each time. *) -val important_message_keep_factor = 0.1 - -fun run_atp auto atp_name - {exec, required_execs, arguments, has_incomplete_mode, proof_delims, - known_failures, explicit_forall, use_conjecture_for_hypotheses, ...} - ({debug, verbose, overlord, full_types, explicit_apply, isar_proof, - isar_shrink_factor, timeout, ...} : params) - minimize_command ({state, goal, subgoal, facts, ...} : prover_problem) = - let - val ctxt = Proof.context_of state - val (_, hyp_ts, concl_t) = strip_subgoal goal subgoal - val facts = - facts |> map (translated_fact ctxt) - val dest_dir = if overlord then getenv "ISABELLE_HOME_USER" - else Config.get ctxt dest_dir - val problem_prefix = Config.get ctxt problem_prefix - val problem_file_name = - Path.basic ((if overlord then "prob_" ^ atp_name - else problem_prefix ^ serial_string ()) - ^ "_" ^ string_of_int subgoal) - val problem_path_name = - 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 measure_run_time = verbose orelse Config.get ctxt measure_run_time - val command = Path.explode (getenv (fst exec) ^ "/" ^ snd exec) - (* write out problem file and call ATP *) - fun command_line complete timeout probfile = - let - val core = File.shell_path command ^ " " ^ arguments complete timeout ^ - " " ^ File.shell_path probfile - in - (if measure_run_time then "TIMEFORMAT='%3R'; { time " ^ core ^ " ; }" - else "exec " ^ core) ^ " 2>&1" - end - fun split_time s = - let - val split = String.tokens (fn c => str c = "\n"); - val (output, t) = s |> split |> split_last |> apfst 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 = Scan.read Symbol.stopper time o raw_explode - in (output, as_time t) end; - fun run_on probfile = - case filter (curry (op =) "" o getenv o fst) (exec :: required_execs) of - (home_var, _) :: _ => - error ("The environment variable " ^ quote home_var ^ " is not set.") - | [] => - if File.exists command then - let - fun run complete timeout = - let - val command = command_line complete timeout probfile - val ((output, msecs), res_code) = - bash_output command - |>> (if overlord then - prefix ("% " ^ command ^ "\n% " ^ timestamp () ^ "\n") - else - I) - |>> (if measure_run_time then split_time else rpair NONE) - val (tstplike_proof, outcome) = - extract_tstplike_proof_and_outcome complete res_code - proof_delims known_failures output - in (output, msecs, tstplike_proof, outcome) end - val readable_names = debug andalso overlord - val (atp_problem, pool, conjecture_offset, fact_names) = - prepare_atp_problem ctxt readable_names explicit_forall full_types - explicit_apply hyp_ts concl_t facts - val ss = tptp_strings_for_atp_problem use_conjecture_for_hypotheses - atp_problem - val _ = File.write_list probfile ss - val conjecture_shape = - conjecture_offset + 1 upto conjecture_offset + length hyp_ts + 1 - |> map single - val run_twice = has_incomplete_mode andalso not auto - val timer = Timer.startRealTimer () - val result = - run false (if run_twice then - Time.fromMilliseconds - (2 * Time.toMilliseconds timeout div 3) - else - timeout) - |> run_twice - ? (fn (_, msecs0, _, SOME _) => - run true (Time.- (timeout, Timer.checkRealTimer timer)) - |> (fn (output, msecs, tstplike_proof, outcome) => - (output, int_opt_add msecs0 msecs, tstplike_proof, - outcome)) - | result => result) - in ((pool, conjecture_shape, fact_names), result) end - else - error ("Bad executable: " ^ Path.implode command ^ ".") - - (* If the problem file has not been exported, remove it; otherwise, export - the proof file too. *) - fun cleanup probfile = - if dest_dir = "" then try File.rm probfile else NONE - fun export probfile (_, (output, _, _, _)) = - if dest_dir = "" then - () - else - File.write (Path.explode (Path.implode probfile ^ "_proof")) output - val ((pool, conjecture_shape, fact_names), - (output, msecs, tstplike_proof, outcome)) = - with_path cleanup export run_on problem_path_name - val (conjecture_shape, fact_names) = - repair_conjecture_shape_and_fact_names output conjecture_shape fact_names - val important_message = - if not auto andalso random () <= important_message_keep_factor then - extract_important_message output - else - "" - val (message, used_facts) = - case outcome of - NONE => - proof_text isar_proof - (pool, debug, isar_shrink_factor, ctxt, conjecture_shape) - (proof_banner auto, full_types, minimize_command, tstplike_proof, - fact_names, goal, subgoal) - |>> (fn message => - message ^ - (if verbose then - "\nATP real CPU time: " ^ - string_from_time (Time.fromMilliseconds (the msecs)) ^ "." - else - "") ^ - (if important_message <> "" then - "\n\nImportant message from Dr. Geoff Sutcliffe:\n" ^ - important_message - else - "")) - | SOME failure => (string_for_failure "ATP" failure, []) - in - {outcome = outcome, message = message, used_facts = used_facts, - run_time_in_msecs = msecs} - 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 = - [(22, CantConnect), - (127, NoPerl), - (2, NoLibwwwPerl)] -val z3_failures = - [(103, MalformedInput), - (110, MalformedInput)] -val unix_failures = - [(139, Crashed)] -val smt_failures = remote_smt_failures @ z3_failures @ unix_failures - -fun failure_from_smt_failure (SMT_Failure.Counterexample _) = Unprovable - | failure_from_smt_failure SMT_Failure.Time_Out = TimedOut - | failure_from_smt_failure (SMT_Failure.Abnormal_Termination code) = - (case AList.lookup (op =) smt_failures code of - SOME failure => failure - | NONE => UnknownError) - | failure_from_smt_failure SMT_Failure.Out_Of_Memory = OutOfResources - | failure_from_smt_failure _ = UnknownError - -(* FUDGE *) -val smt_max_iter = 8 -val smt_iter_fact_divisor = 2 -val smt_iter_min_msecs = 5000 -val smt_iter_timeout_divisor = 2 -val smt_monomorph_limit = 4 - -fun smt_filter_loop ({verbose, timeout, ...} : params) remote state i = - let - val ctxt = Proof.context_of state - fun iter timeout iter_num outcome0 msecs_so_far facts = - let - val timer = Timer.startRealTimer () - val ms = timeout |> Time.toMilliseconds - val iter_timeout = - if iter_num < smt_max_iter then - Int.min (ms, Int.max (smt_iter_min_msecs, - ms div smt_iter_timeout_divisor)) - |> Time.fromMilliseconds - else - timeout - val num_facts = length facts - val _ = - if verbose then - "SMT iteration with " ^ string_of_int num_facts ^ " fact" ^ - plural_s num_facts ^ " for " ^ string_from_time iter_timeout ^ "..." - |> Output.urgent_message - else - () - val {outcome, used_facts, run_time_in_msecs} = - SMT_Solver.smt_filter remote iter_timeout state facts i - val _ = - if verbose andalso is_some outcome then - "SMT outcome: " ^ SMT_Failure.string_of_failure ctxt (the outcome) - |> Output.urgent_message - else - () - val outcome0 = if is_none outcome0 then SOME outcome else outcome0 - val msecs_so_far = int_opt_add run_time_in_msecs msecs_so_far - val too_many_facts_perhaps = - case outcome of - NONE => false - | SOME (SMT_Failure.Counterexample _) => false - | SOME SMT_Failure.Time_Out => iter_timeout <> timeout - | SOME (SMT_Failure.Abnormal_Termination code) => - (if verbose then - "The SMT solver invoked with " ^ string_of_int num_facts ^ - " fact" ^ plural_s num_facts ^ " terminated abnormally with \ - \exit code " ^ string_of_int code ^ "." - |> warning - else - (); - true (* kind of *)) - | SOME SMT_Failure.Out_Of_Memory => true - | SOME _ => true - val timeout = Time.- (timeout, Timer.checkRealTimer timer) - in - if too_many_facts_perhaps andalso iter_num < smt_max_iter andalso - num_facts > 0 andalso Time.> (timeout, Time.zeroTime) then - let val facts = take (num_facts div smt_iter_fact_divisor) facts in - iter timeout (iter_num + 1) outcome0 msecs_so_far facts - end - else - {outcome = if is_none outcome then NONE else the outcome0, - used_facts = used_facts, run_time_in_msecs = msecs_so_far} - end - in iter timeout 1 NONE (SOME 0) end - -(* taken from "Mirabelle" and generalized *) -fun can_apply timeout tac state i = - let - val {context = ctxt, facts, goal} = Proof.goal state - val full_tac = Method.insert_tac facts i THEN tac ctxt i - in - case try (TimeLimit.timeLimit timeout (Seq.pull o full_tac)) goal of - SOME (SOME _) => true - | _ => false - end - -val smt_metis_timeout = seconds 0.5 - -fun can_apply_metis debug state i ths = - can_apply smt_metis_timeout - (Config.put Metis_Tactics.verbose debug - #> (fn ctxt => Metis_Tactics.metis_tac ctxt ths)) state i - -fun run_smt_solver auto name (params as {debug, ...}) minimize_command - ({state, subgoal, subgoal_count, facts, ...} : prover_problem) = - let - val (remote, suffix) = - case try (unprefix remote_prefix) name of - SOME suffix => (true, suffix) - | NONE => (false, name) - val repair_context = - Context.proof_map (SMT_Config.select_solver suffix) - #> Config.put SMT_Config.verbose debug - #> Config.put SMT_Config.monomorph_limit smt_monomorph_limit - val state = state |> Proof.map_context repair_context - val thy = Proof.theory_of state - val get_fact = Option.map (apsnd (Thm.transfer thy)) o try dest_Untranslated - val facts = facts |> map_filter get_fact - val {outcome, used_facts, run_time_in_msecs} = - smt_filter_loop params remote state subgoal facts - val (chained_lemmas, other_lemmas) = split_used_facts (map fst used_facts) - val outcome = outcome |> Option.map failure_from_smt_failure - val message = - case outcome of - NONE => - let - val method = - if can_apply_metis debug state subgoal (map snd used_facts) then - "metis" - else - "smt" - in - try_command_line (proof_banner auto) - (apply_on_subgoal subgoal subgoal_count ^ - command_call method (map fst other_lemmas)) ^ - minimize_line minimize_command - (map fst (other_lemmas @ chained_lemmas)) - end - | SOME failure => string_for_failure "SMT solver" failure - in - {outcome = outcome, used_facts = map fst used_facts, - run_time_in_msecs = run_time_in_msecs, message = message} - end - -fun get_prover ctxt auto name = - let val thy = ProofContext.theory_of ctxt in - if is_smt_prover ctxt name then - run_smt_solver auto name - else if member (op =) (available_atps thy) name then - run_atp auto name (get_atp thy name) - else - error ("No such prover: " ^ name ^ ".") - end - -fun run_prover (params as {blocking, debug, max_relevant, timeout, expect, ...}) - auto minimize_command only - {state, goal, subgoal, subgoal_count, facts} name = - let - val ctxt = Proof.context_of state - val birth_time = Time.now () - val death_time = Time.+ (birth_time, timeout) - val max_relevant = - the_default (default_max_relevant_for_prover ctxt name) max_relevant - val num_facts = length facts |> not only ? Integer.min max_relevant - val desc = - prover_description ctxt params name num_facts subgoal subgoal_count goal - val prover = get_prover ctxt auto name - val problem = - {state = state, goal = goal, subgoal = subgoal, - subgoal_count = subgoal_count, facts = take num_facts facts} - fun go () = - let - fun really_go () = - prover params (minimize_command name) problem - |> (fn {outcome, message, ...} => - (if is_some outcome then "none" else "some", message)) - val (outcome_code, message) = - if debug then - really_go () - else - (really_go () - handle ERROR message => ("unknown", "Error: " ^ message ^ "\n") - | exn => - if Exn.is_interrupt exn then - reraise exn - else - ("unknown", "Internal error:\n" ^ - ML_Compiler.exn_message exn ^ "\n")) - val _ = - if expect = "" orelse outcome_code = expect then - () - else if blocking then - error ("Unexpected outcome: " ^ quote outcome_code ^ ".") - else - warning ("Unexpected outcome: " ^ quote outcome_code ^ "."); - in (outcome_code = "some", message) end - in - if auto then - let val (success, message) = TimeLimit.timeLimit timeout go () in - (success, state |> success ? Proof.goal_message (fn () => - Pretty.chunks [Pretty.str "", Pretty.mark Markup.hilite - (Pretty.str message)])) - end - else if blocking then - let val (success, message) = TimeLimit.timeLimit timeout go () in - List.app Output.urgent_message - (Async_Manager.break_into_chunks [desc ^ "\n" ^ message]); - (success, state) - end - else - (Async_Manager.launch das_Tool birth_time death_time desc (snd o go); - (false, state)) - end - -fun run_sledgehammer (params as {blocking, debug, provers, full_types, - relevance_thresholds, max_relevant, ...}) - auto i (relevance_override as {only, ...}) minimize_command - state = - if null provers then - error "No prover is set." - else case subgoal_count state of - 0 => (Output.urgent_message "No subgoal!"; (false, state)) - | n => - let - val _ = Proof.assert_backward state - val ctxt = Proof.context_of state - val {facts = chained_ths, goal, ...} = Proof.goal state - val (_, hyp_ts, concl_t) = strip_subgoal goal i - val _ = () |> not blocking ? kill_provers - val _ = case find_first (not o is_prover_available ctxt) provers of - SOME name => error ("No such prover: " ^ name ^ ".") - | NONE => () - val _ = if auto then () else Output.urgent_message "Sledgehammering..." - val (smts, atps) = provers |> List.partition (is_smt_prover ctxt) - fun run_provers label full_types relevance_fudge maybe_translate provers - (res as (success, state)) = - if success orelse null provers then - res - else - let - val max_max_relevant = - case max_relevant of - SOME n => n - | NONE => - 0 |> fold (Integer.max o default_max_relevant_for_prover ctxt) - provers - |> auto ? (fn n => n div auto_max_relevant_divisor) - val is_built_in_const = - is_built_in_const_for_prover ctxt (hd provers) - val facts = - relevant_facts ctxt full_types relevance_thresholds - max_max_relevant is_built_in_const relevance_fudge - relevance_override chained_ths hyp_ts concl_t - |> map maybe_translate - val problem = - {state = state, goal = goal, subgoal = i, subgoal_count = n, - facts = facts} - val run_prover = run_prover params auto minimize_command only - in - if debug then - Output.urgent_message (label ^ plural_s (length provers) ^ ": " ^ - (if null facts then - "Found no relevant facts." - else - "Including (up to) " ^ string_of_int (length facts) ^ - " relevant fact" ^ plural_s (length facts) ^ ":\n" ^ - (facts |> map_filter fact_name - |> space_implode " ") ^ ".")) - else - (); - if auto then - fold (fn prover => fn (true, state) => (true, state) - | (false, _) => run_prover problem prover) - provers (false, state) - else - provers |> (if blocking then Par_List.map else map) - (run_prover problem) - |> exists fst |> rpair state - end - val run_atps = - run_provers "ATP" full_types atp_relevance_fudge - (Translated o translate_fact ctxt) atps - val run_smts = - run_provers "SMT solver" true smt_relevance_fudge Untranslated smts - fun run_atps_and_smt_solvers () = - [run_atps, run_smts] |> Par_List.map (fn f => f (false, state) |> K ()) - in - (false, state) - |> (if blocking then run_atps #> not auto ? run_smts - else (fn p => Future.fork (tap run_atps_and_smt_solvers) |> K p)) - end - -val setup = - dest_dir_setup - #> problem_prefix_setup - #> measure_run_time_setup - -end; diff -r b4cccce25d9a -r d7b5fd465198 src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML Wed Dec 08 18:07:04 2010 +0100 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML Wed Dec 08 22:17:52 2010 +0100 @@ -6,7 +6,7 @@ signature SLEDGEHAMMER_ISAR = sig - type params = Sledgehammer.params + type params = Sledgehammer_Provers.params val auto : bool Unsynchronized.ref val provers : string Unsynchronized.ref @@ -21,8 +21,9 @@ open ATP_Systems open Sledgehammer_Util -open Sledgehammer +open Sledgehammer_Provers open Sledgehammer_Minimize +open Sledgehammer_Run val auto = Unsynchronized.ref false diff -r b4cccce25d9a -r d7b5fd465198 src/HOL/Tools/Sledgehammer/sledgehammer_minimize.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_minimize.ML Wed Dec 08 18:07:04 2010 +0100 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_minimize.ML Wed Dec 08 22:17:52 2010 +0100 @@ -8,7 +8,7 @@ signature SLEDGEHAMMER_MINIMIZE = sig type locality = Sledgehammer_Filter.locality - type params = Sledgehammer.params + type params = Sledgehammer_Provers.params val minimize_facts : params -> int -> int -> Proof.state -> ((string * locality) * thm list) list @@ -23,7 +23,7 @@ open ATP_Proof open Sledgehammer_Util open Sledgehammer_Filter -open Sledgehammer +open Sledgehammer_Provers (* wrapper for calling external prover *) diff -r b4cccce25d9a -r d7b5fd465198 src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML Wed Dec 08 22:17:52 2010 +0100 @@ -0,0 +1,648 @@ +(* Title: HOL/Tools/Sledgehammer/sledgehammer_provers.ML + Author: Fabian Immler, TU Muenchen + Author: Makarius + Author: Jasmin Blanchette, TU Muenchen + +Generic prover abstraction for Sledgehammer. +*) + +signature SLEDGEHAMMER_PROVERS = +sig + type failure = ATP_Proof.failure + type locality = Sledgehammer_Filter.locality + type relevance_fudge = Sledgehammer_Filter.relevance_fudge + type translated_formula = Sledgehammer_ATP_Translate.translated_formula + type minimize_command = Sledgehammer_ATP_Reconstruct.minimize_command + + type params = + {blocking: bool, + debug: bool, + verbose: bool, + overlord: bool, + provers: string list, + full_types: bool, + explicit_apply: bool, + relevance_thresholds: real * real, + max_relevant: int option, + isar_proof: bool, + isar_shrink_factor: int, + timeout: Time.time, + expect: string} + + datatype fact = + Untranslated of (string * locality) * thm | + Translated of term * ((string * locality) * translated_formula) option + + type prover_problem = + {state: Proof.state, + goal: thm, + subgoal: int, + subgoal_count: int, + facts: fact list} + + type prover_result = + {outcome: failure option, + used_facts: (string * locality) list, + run_time_in_msecs: int option, + message: string} + + type prover = params -> minimize_command -> prover_problem -> prover_result + + val is_smt_prover : Proof.context -> string -> bool + val is_prover_available : Proof.context -> string -> bool + val is_prover_installed : Proof.context -> string -> bool + val default_max_relevant_for_prover : Proof.context -> string -> int + val is_built_in_const_for_prover : + Proof.context -> string -> string * typ -> term list -> bool + val atp_relevance_fudge : relevance_fudge + val smt_relevance_fudge : relevance_fudge + val relevance_fudge_for_prover : Proof.context -> string -> relevance_fudge + val dest_dir : string Config.T + val problem_prefix : string Config.T + val measure_run_time : bool Config.T + val available_provers : Proof.context -> unit + val kill_provers : unit -> unit + val running_provers : unit -> unit + val messages : int option -> unit + val get_prover : Proof.context -> bool -> string -> prover + val run_prover : + params -> bool -> (string -> minimize_command) -> bool -> prover_problem + -> string -> bool * Proof.state + val setup : theory -> theory +end; + +structure Sledgehammer_Provers : SLEDGEHAMMER_PROVERS = +struct + +open ATP_Problem +open ATP_Proof +open ATP_Systems +open Metis_Translate +open Sledgehammer_Util +open Sledgehammer_Filter +open Sledgehammer_ATP_Translate +open Sledgehammer_ATP_Reconstruct + +(** The Sledgehammer **) + +(* Identifier to distinguish Sledgehammer from other tools using + "Async_Manager". *) +val das_Tool = "Sledgehammer" + +fun is_smt_prover ctxt name = + let val smts = SMT_Solver.available_solvers_of ctxt in + case try (unprefix remote_prefix) name of + SOME suffix => member (op =) smts suffix andalso + SMT_Solver.is_remotely_available ctxt suffix + | NONE => member (op =) smts name + end + +fun is_prover_available ctxt name = + let val thy = ProofContext.theory_of ctxt in + is_smt_prover ctxt name orelse member (op =) (available_atps thy) name + end + +fun is_prover_installed ctxt name = + let val thy = ProofContext.theory_of ctxt in + if is_smt_prover ctxt name then + String.isPrefix remote_prefix name orelse + SMT_Solver.is_locally_installed ctxt name + else + is_atp_installed thy name + end + +fun available_smt_solvers ctxt = + let val smts = SMT_Solver.available_solvers_of ctxt in + smts @ map (prefix remote_prefix) + (filter (SMT_Solver.is_remotely_available ctxt) smts) + end + +fun default_max_relevant_for_prover ctxt name = + let val thy = ProofContext.theory_of ctxt in + if is_smt_prover ctxt name then + SMT_Solver.default_max_relevant ctxt + (perhaps (try (unprefix remote_prefix)) name) + else + #default_max_relevant (get_atp thy name) + end + +(* These are typically simplified away by "Meson.presimplify". Equality is + handled specially via "fequal". *) +val atp_irrelevant_consts = + [@{const_name False}, @{const_name True}, @{const_name If}, @{const_name Let}, + @{const_name HOL.eq}] + +fun is_built_in_const_for_prover ctxt name (s, T) args = + if is_smt_prover ctxt name then SMT_Builtin.is_builtin_ext ctxt (s, T) args + else member (op =) atp_irrelevant_consts s + +(* FUDGE *) +val atp_relevance_fudge = + {worse_irrel_freq = 100.0, + higher_order_irrel_weight = 1.05, + abs_rel_weight = 0.5, + abs_irrel_weight = 2.0, + skolem_irrel_weight = 0.75, + theory_const_rel_weight = 0.5, + theory_const_irrel_weight = 0.25, + intro_bonus = 0.15, + elim_bonus = 0.15, + simp_bonus = 0.15, + local_bonus = 0.55, + assum_bonus = 1.05, + chained_bonus = 1.5, + max_imperfect = 11.5, + max_imperfect_exp = 1.0, + threshold_divisor = 2.0, + ridiculous_threshold = 0.1} + +(* FUDGE (FIXME) *) +val smt_relevance_fudge = + {worse_irrel_freq = #worse_irrel_freq atp_relevance_fudge, + higher_order_irrel_weight = #higher_order_irrel_weight atp_relevance_fudge, + abs_rel_weight = #abs_rel_weight atp_relevance_fudge, + abs_irrel_weight = #abs_irrel_weight atp_relevance_fudge, + skolem_irrel_weight = #skolem_irrel_weight atp_relevance_fudge, + theory_const_rel_weight = #theory_const_rel_weight atp_relevance_fudge, + theory_const_irrel_weight = #theory_const_irrel_weight atp_relevance_fudge, + intro_bonus = #intro_bonus atp_relevance_fudge, + elim_bonus = #elim_bonus atp_relevance_fudge, + simp_bonus = #simp_bonus atp_relevance_fudge, + local_bonus = #local_bonus atp_relevance_fudge, + assum_bonus = #assum_bonus atp_relevance_fudge, + chained_bonus = #chained_bonus atp_relevance_fudge, + max_imperfect = #max_imperfect atp_relevance_fudge, + max_imperfect_exp = #max_imperfect_exp atp_relevance_fudge, + threshold_divisor = #threshold_divisor atp_relevance_fudge, + ridiculous_threshold = #ridiculous_threshold atp_relevance_fudge} + +fun relevance_fudge_for_prover ctxt name = + if is_smt_prover ctxt name then smt_relevance_fudge else atp_relevance_fudge + +fun available_provers ctxt = + let + val thy = ProofContext.theory_of ctxt + val (remote_provers, local_provers) = + sort_strings (available_atps thy) @ + sort_strings (available_smt_solvers ctxt) + |> List.partition (String.isPrefix remote_prefix) + in + Output.urgent_message ("Available provers: " ^ + commas (local_provers @ remote_provers) ^ ".") + end + +fun kill_provers () = Async_Manager.kill_threads das_Tool "provers" +fun running_provers () = Async_Manager.running_threads das_Tool "provers" +val messages = Async_Manager.thread_messages das_Tool "prover" + +(** problems, results, ATPs, etc. **) + +type params = + {blocking: bool, + debug: bool, + verbose: bool, + overlord: bool, + provers: string list, + full_types: bool, + explicit_apply: bool, + relevance_thresholds: real * real, + max_relevant: int option, + isar_proof: bool, + isar_shrink_factor: int, + timeout: Time.time, + expect: string} + +datatype fact = + Untranslated of (string * locality) * thm | + Translated of term * ((string * locality) * translated_formula) option + +type prover_problem = + {state: Proof.state, + goal: thm, + subgoal: int, + subgoal_count: int, + facts: fact list} + +type prover_result = + {outcome: failure option, + message: string, + used_facts: (string * locality) list, + run_time_in_msecs: int option} + +type prover = params -> minimize_command -> prover_problem -> prover_result + +(* configuration attributes *) + +val (dest_dir, dest_dir_setup) = + Attrib.config_string "sledgehammer_dest_dir" (K "") + (* Empty string means create files in Isabelle's temporary files directory. *) + +val (problem_prefix, problem_prefix_setup) = + Attrib.config_string "sledgehammer_problem_prefix" (K "prob") + +val (measure_run_time, measure_run_time_setup) = + Attrib.config_bool "sledgehammer_measure_run_time" (K false) + +fun with_path cleanup after f path = + Exn.capture f path + |> tap (fn _ => cleanup path) + |> Exn.release + |> tap (after path) + +fun prover_description ctxt ({blocking, verbose, ...} : params) name num_facts i + n goal = + quote name ^ + (if verbose then + " with " ^ string_of_int num_facts ^ " fact" ^ plural_s num_facts + else + "") ^ + " on " ^ (if n = 1 then "goal" else "subgoal " ^ string_of_int i) ^ ":" ^ + (if blocking then + "" + else + "\n" ^ Syntax.string_of_term ctxt (Thm.term_of (Thm.cprem_of goal i))) + +fun proof_banner auto = + if auto then "Auto Sledgehammer found a proof" else "Try this command" + +(* generic TPTP-based ATPs *) + +fun dest_Untranslated (Untranslated p) = p + | dest_Untranslated (Translated _) = raise Fail "dest_Untranslated" +fun translated_fact ctxt (Untranslated p) = translate_fact ctxt p + | translated_fact _ (Translated p) = p + +fun int_opt_add (SOME m) (SOME n) = SOME (m + n) + | int_opt_add _ _ = NONE + +(* Important messages are important but not so important that users want to see + them each time. *) +val important_message_keep_factor = 0.1 + +fun run_atp auto atp_name + {exec, required_execs, arguments, has_incomplete_mode, proof_delims, + known_failures, explicit_forall, use_conjecture_for_hypotheses, ...} + ({debug, verbose, overlord, full_types, explicit_apply, isar_proof, + isar_shrink_factor, timeout, ...} : params) + minimize_command ({state, goal, subgoal, facts, ...} : prover_problem) = + let + val ctxt = Proof.context_of state + val (_, hyp_ts, concl_t) = strip_subgoal goal subgoal + val facts = + facts |> map (translated_fact ctxt) + val dest_dir = if overlord then getenv "ISABELLE_HOME_USER" + else Config.get ctxt dest_dir + val problem_prefix = Config.get ctxt problem_prefix + val problem_file_name = + Path.basic ((if overlord then "prob_" ^ atp_name + else problem_prefix ^ serial_string ()) + ^ "_" ^ string_of_int subgoal) + val problem_path_name = + 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 measure_run_time = verbose orelse Config.get ctxt measure_run_time + val command = Path.explode (getenv (fst exec) ^ "/" ^ snd exec) + (* write out problem file and call ATP *) + fun command_line complete timeout probfile = + let + val core = File.shell_path command ^ " " ^ arguments complete timeout ^ + " " ^ File.shell_path probfile + in + (if measure_run_time then "TIMEFORMAT='%3R'; { time " ^ core ^ " ; }" + else "exec " ^ core) ^ " 2>&1" + end + fun split_time s = + let + val split = String.tokens (fn c => str c = "\n"); + val (output, t) = s |> split |> split_last |> apfst 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 = Scan.read Symbol.stopper time o raw_explode + in (output, as_time t) end; + fun run_on probfile = + case filter (curry (op =) "" o getenv o fst) (exec :: required_execs) of + (home_var, _) :: _ => + error ("The environment variable " ^ quote home_var ^ " is not set.") + | [] => + if File.exists command then + let + fun run complete timeout = + let + val command = command_line complete timeout probfile + val ((output, msecs), res_code) = + bash_output command + |>> (if overlord then + prefix ("% " ^ command ^ "\n% " ^ timestamp () ^ "\n") + else + I) + |>> (if measure_run_time then split_time else rpair NONE) + val (tstplike_proof, outcome) = + extract_tstplike_proof_and_outcome complete res_code + proof_delims known_failures output + in (output, msecs, tstplike_proof, outcome) end + val readable_names = debug andalso overlord + val (atp_problem, pool, conjecture_offset, fact_names) = + prepare_atp_problem ctxt readable_names explicit_forall full_types + explicit_apply hyp_ts concl_t facts + val ss = tptp_strings_for_atp_problem use_conjecture_for_hypotheses + atp_problem + val _ = File.write_list probfile ss + val conjecture_shape = + conjecture_offset + 1 upto conjecture_offset + length hyp_ts + 1 + |> map single + val run_twice = has_incomplete_mode andalso not auto + val timer = Timer.startRealTimer () + val result = + run false (if run_twice then + Time.fromMilliseconds + (2 * Time.toMilliseconds timeout div 3) + else + timeout) + |> run_twice + ? (fn (_, msecs0, _, SOME _) => + run true (Time.- (timeout, Timer.checkRealTimer timer)) + |> (fn (output, msecs, tstplike_proof, outcome) => + (output, int_opt_add msecs0 msecs, tstplike_proof, + outcome)) + | result => result) + in ((pool, conjecture_shape, fact_names), result) end + else + error ("Bad executable: " ^ Path.implode command ^ ".") + + (* If the problem file has not been exported, remove it; otherwise, export + the proof file too. *) + fun cleanup probfile = + if dest_dir = "" then try File.rm probfile else NONE + fun export probfile (_, (output, _, _, _)) = + if dest_dir = "" then + () + else + File.write (Path.explode (Path.implode probfile ^ "_proof")) output + val ((pool, conjecture_shape, fact_names), + (output, msecs, tstplike_proof, outcome)) = + with_path cleanup export run_on problem_path_name + val (conjecture_shape, fact_names) = + repair_conjecture_shape_and_fact_names output conjecture_shape fact_names + val important_message = + if not auto andalso random () <= important_message_keep_factor then + extract_important_message output + else + "" + val (message, used_facts) = + case outcome of + NONE => + proof_text isar_proof + (pool, debug, isar_shrink_factor, ctxt, conjecture_shape) + (proof_banner auto, full_types, minimize_command, tstplike_proof, + fact_names, goal, subgoal) + |>> (fn message => + message ^ + (if verbose then + "\nATP real CPU time: " ^ + string_from_time (Time.fromMilliseconds (the msecs)) ^ "." + else + "") ^ + (if important_message <> "" then + "\n\nImportant message from Dr. Geoff Sutcliffe:\n" ^ + important_message + else + "")) + | SOME failure => (string_for_failure "ATP" failure, []) + in + {outcome = outcome, message = message, used_facts = used_facts, + run_time_in_msecs = msecs} + 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 = + [(22, CantConnect), + (127, NoPerl), + (2, NoLibwwwPerl)] +val z3_failures = + [(103, MalformedInput), + (110, MalformedInput)] +val unix_failures = + [(139, Crashed)] +val smt_failures = remote_smt_failures @ z3_failures @ unix_failures + +fun failure_from_smt_failure (SMT_Failure.Counterexample _) = Unprovable + | failure_from_smt_failure SMT_Failure.Time_Out = TimedOut + | failure_from_smt_failure (SMT_Failure.Abnormal_Termination code) = + (case AList.lookup (op =) smt_failures code of + SOME failure => failure + | NONE => UnknownError) + | failure_from_smt_failure SMT_Failure.Out_Of_Memory = OutOfResources + | failure_from_smt_failure _ = UnknownError + +(* FUDGE *) +val smt_max_iter = 8 +val smt_iter_fact_divisor = 2 +val smt_iter_min_msecs = 5000 +val smt_iter_timeout_divisor = 2 +val smt_monomorph_limit = 4 + +fun smt_filter_loop ({verbose, timeout, ...} : params) remote state i = + let + val ctxt = Proof.context_of state + fun iter timeout iter_num outcome0 msecs_so_far facts = + let + val timer = Timer.startRealTimer () + val ms = timeout |> Time.toMilliseconds + val iter_timeout = + if iter_num < smt_max_iter then + Int.min (ms, Int.max (smt_iter_min_msecs, + ms div smt_iter_timeout_divisor)) + |> Time.fromMilliseconds + else + timeout + val num_facts = length facts + val _ = + if verbose then + "SMT iteration with " ^ string_of_int num_facts ^ " fact" ^ + plural_s num_facts ^ " for " ^ string_from_time iter_timeout ^ "..." + |> Output.urgent_message + else + () + val {outcome, used_facts, run_time_in_msecs} = + SMT_Solver.smt_filter remote iter_timeout state facts i + val _ = + if verbose andalso is_some outcome then + "SMT outcome: " ^ SMT_Failure.string_of_failure ctxt (the outcome) + |> Output.urgent_message + else + () + val outcome0 = if is_none outcome0 then SOME outcome else outcome0 + val msecs_so_far = int_opt_add run_time_in_msecs msecs_so_far + val too_many_facts_perhaps = + case outcome of + NONE => false + | SOME (SMT_Failure.Counterexample _) => false + | SOME SMT_Failure.Time_Out => iter_timeout <> timeout + | SOME (SMT_Failure.Abnormal_Termination code) => + (if verbose then + "The SMT solver invoked with " ^ string_of_int num_facts ^ + " fact" ^ plural_s num_facts ^ " terminated abnormally with \ + \exit code " ^ string_of_int code ^ "." + |> warning + else + (); + true (* kind of *)) + | SOME SMT_Failure.Out_Of_Memory => true + | SOME _ => true + val timeout = Time.- (timeout, Timer.checkRealTimer timer) + in + if too_many_facts_perhaps andalso iter_num < smt_max_iter andalso + num_facts > 0 andalso Time.> (timeout, Time.zeroTime) then + let val facts = take (num_facts div smt_iter_fact_divisor) facts in + iter timeout (iter_num + 1) outcome0 msecs_so_far facts + end + else + {outcome = if is_none outcome then NONE else the outcome0, + used_facts = used_facts, run_time_in_msecs = msecs_so_far} + end + in iter timeout 1 NONE (SOME 0) end + +(* taken from "Mirabelle" and generalized *) +fun can_apply timeout tac state i = + let + val {context = ctxt, facts, goal} = Proof.goal state + val full_tac = Method.insert_tac facts i THEN tac ctxt i + in + case try (TimeLimit.timeLimit timeout (Seq.pull o full_tac)) goal of + SOME (SOME _) => true + | _ => false + end + +val smt_metis_timeout = seconds 0.5 + +fun can_apply_metis debug state i ths = + can_apply smt_metis_timeout + (Config.put Metis_Tactics.verbose debug + #> (fn ctxt => Metis_Tactics.metis_tac ctxt ths)) state i + +fun run_smt_solver auto name (params as {debug, ...}) minimize_command + ({state, subgoal, subgoal_count, facts, ...} : prover_problem) = + let + val (remote, suffix) = + case try (unprefix remote_prefix) name of + SOME suffix => (true, suffix) + | NONE => (false, name) + val repair_context = + Context.proof_map (SMT_Config.select_solver suffix) + #> Config.put SMT_Config.verbose debug + #> Config.put SMT_Config.monomorph_limit smt_monomorph_limit + val state = state |> Proof.map_context repair_context + val thy = Proof.theory_of state + val get_fact = Option.map (apsnd (Thm.transfer thy)) o try dest_Untranslated + val facts = facts |> map_filter get_fact + val {outcome, used_facts, run_time_in_msecs} = + smt_filter_loop params remote state subgoal facts + val (chained_lemmas, other_lemmas) = split_used_facts (map fst used_facts) + val outcome = outcome |> Option.map failure_from_smt_failure + val message = + case outcome of + NONE => + let + val method = + if can_apply_metis debug state subgoal (map snd used_facts) then + "metis" + else + "smt" + in + try_command_line (proof_banner auto) + (apply_on_subgoal subgoal subgoal_count ^ + command_call method (map fst other_lemmas)) ^ + minimize_line minimize_command + (map fst (other_lemmas @ chained_lemmas)) + end + | SOME failure => string_for_failure "SMT solver" failure + in + {outcome = outcome, used_facts = map fst used_facts, + run_time_in_msecs = run_time_in_msecs, message = message} + end + +fun get_prover ctxt auto name = + let val thy = ProofContext.theory_of ctxt in + if is_smt_prover ctxt name then + run_smt_solver auto name + else if member (op =) (available_atps thy) name then + run_atp auto name (get_atp thy name) + else + error ("No such prover: " ^ name ^ ".") + end + +fun run_prover (params as {blocking, debug, max_relevant, timeout, expect, ...}) + auto minimize_command only + {state, goal, subgoal, subgoal_count, facts} name = + let + val ctxt = Proof.context_of state + val birth_time = Time.now () + val death_time = Time.+ (birth_time, timeout) + val max_relevant = + the_default (default_max_relevant_for_prover ctxt name) max_relevant + val num_facts = length facts |> not only ? Integer.min max_relevant + val desc = + prover_description ctxt params name num_facts subgoal subgoal_count goal + val prover = get_prover ctxt auto name + val problem = + {state = state, goal = goal, subgoal = subgoal, + subgoal_count = subgoal_count, facts = take num_facts facts} + fun go () = + let + fun really_go () = + prover params (minimize_command name) problem + |> (fn {outcome, message, ...} => + (if is_some outcome then "none" else "some", message)) + val (outcome_code, message) = + if debug then + really_go () + else + (really_go () + handle ERROR message => ("unknown", "Error: " ^ message ^ "\n") + | exn => + if Exn.is_interrupt exn then + reraise exn + else + ("unknown", "Internal error:\n" ^ + ML_Compiler.exn_message exn ^ "\n")) + val _ = + if expect = "" orelse outcome_code = expect then + () + else if blocking then + error ("Unexpected outcome: " ^ quote outcome_code ^ ".") + else + warning ("Unexpected outcome: " ^ quote outcome_code ^ "."); + in (outcome_code = "some", message) end + in + if auto then + let val (success, message) = TimeLimit.timeLimit timeout go () in + (success, state |> success ? Proof.goal_message (fn () => + Pretty.chunks [Pretty.str "", Pretty.mark Markup.hilite + (Pretty.str message)])) + end + else if blocking then + let val (success, message) = TimeLimit.timeLimit timeout go () in + List.app Output.urgent_message + (Async_Manager.break_into_chunks [desc ^ "\n" ^ message]); + (success, state) + end + else + (Async_Manager.launch das_Tool birth_time death_time desc (snd o go); + (false, state)) + end + +val setup = + dest_dir_setup + #> problem_prefix_setup + #> measure_run_time_setup + +end; diff -r b4cccce25d9a -r d7b5fd465198 src/HOL/Tools/Sledgehammer/sledgehammer_run.ML --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_run.ML Wed Dec 08 22:17:52 2010 +0100 @@ -0,0 +1,112 @@ +(* Title: HOL/Tools/Sledgehammer/sledgehammer_run.ML + Author: Fabian Immler, TU Muenchen + Author: Makarius + Author: Jasmin Blanchette, TU Muenchen + +Sledgehammer's heart. +*) + +signature SLEDGEHAMMER_RUN = +sig + type relevance_override = Sledgehammer_Filter.relevance_override + type minimize_command = Sledgehammer_ATP_Reconstruct.minimize_command + type params = Sledgehammer_Provers.params + + val run_sledgehammer : + params -> bool -> int -> relevance_override -> (string -> minimize_command) + -> Proof.state -> bool * Proof.state +end; + +structure Sledgehammer_Run : SLEDGEHAMMER_RUN = +struct + +open Sledgehammer_Util +open Sledgehammer_Filter +open Sledgehammer_ATP_Translate +open Sledgehammer_Provers + +(* FUDGE *) +val auto_max_relevant_divisor = 2 + +fun fact_name (Untranslated ((name, _), _)) = SOME name + | fact_name (Translated (_, p)) = Option.map (fst o fst) p + +fun run_sledgehammer (params as {blocking, debug, provers, full_types, + relevance_thresholds, max_relevant, ...}) + auto i (relevance_override as {only, ...}) minimize_command + state = + if null provers then + error "No prover is set." + else case subgoal_count state of + 0 => (Output.urgent_message "No subgoal!"; (false, state)) + | n => + let + val _ = Proof.assert_backward state + val ctxt = Proof.context_of state + val {facts = chained_ths, goal, ...} = Proof.goal state + val (_, hyp_ts, concl_t) = strip_subgoal goal i + val _ = () |> not blocking ? kill_provers + val _ = case find_first (not o is_prover_available ctxt) provers of + SOME name => error ("No such prover: " ^ name ^ ".") + | NONE => () + val _ = if auto then () else Output.urgent_message "Sledgehammering..." + val (smts, atps) = provers |> List.partition (is_smt_prover ctxt) + fun run_provers label full_types relevance_fudge maybe_translate provers + (res as (success, state)) = + if success orelse null provers then + res + else + let + val max_max_relevant = + case max_relevant of + SOME n => n + | NONE => + 0 |> fold (Integer.max o default_max_relevant_for_prover ctxt) + provers + |> auto ? (fn n => n div auto_max_relevant_divisor) + val is_built_in_const = + is_built_in_const_for_prover ctxt (hd provers) + val facts = + relevant_facts ctxt full_types relevance_thresholds + max_max_relevant is_built_in_const relevance_fudge + relevance_override chained_ths hyp_ts concl_t + |> map maybe_translate + val problem = + {state = state, goal = goal, subgoal = i, subgoal_count = n, + facts = facts} + val run_prover = run_prover params auto minimize_command only + in + if debug then + Output.urgent_message (label ^ plural_s (length provers) ^ ": " ^ + (if null facts then + "Found no relevant facts." + else + "Including (up to) " ^ string_of_int (length facts) ^ + " relevant fact" ^ plural_s (length facts) ^ ":\n" ^ + (facts |> map_filter fact_name + |> space_implode " ") ^ ".")) + else + (); + if auto then + fold (fn prover => fn (true, state) => (true, state) + | (false, _) => run_prover problem prover) + provers (false, state) + else + provers |> (if blocking then Par_List.map else map) + (run_prover problem) + |> exists fst |> rpair state + end + val run_atps = + run_provers "ATP" full_types atp_relevance_fudge + (Translated o translate_fact ctxt) atps + val run_smts = + run_provers "SMT solver" true smt_relevance_fudge Untranslated smts + fun run_atps_and_smt_solvers () = + [run_atps, run_smts] |> Par_List.map (fn f => f (false, state) |> K ()) + in + (false, state) + |> (if blocking then run_atps #> not auto ? run_smts + else (fn p => Future.fork (tap run_atps_and_smt_solvers) |> K p)) + end + +end;