# HG changeset patch # User blanchet # Date 1291843073 -3600 # Node ID 0afdf5cde8743541ccdeb4bc270a3017eb5efdc4 # Parent b98fe4de1ecdb25cd49524ab58425c7b4f4854be implicitly call the minimizer for SMT solvers that don't return an unsat core diff -r b98fe4de1ecd -r 0afdf5cde874 src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML --- a/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML Wed Dec 08 22:17:52 2010 +0100 +++ b/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML Wed Dec 08 22:17:53 2010 +0100 @@ -457,7 +457,7 @@ ("provers", prover_name), ("timeout", Int.toString timeout)] val minimize = - Sledgehammer_Minimize.minimize_facts params 1 + Sledgehammer_Minimize.minimize_facts params true 1 (Sledgehammer_Util.subgoal_count st) val _ = log separator in diff -r b98fe4de1ecd -r 0afdf5cde874 src/HOL/Tools/Sledgehammer/sledgehammer_atp_translate.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_atp_translate.ML Wed Dec 08 22:17:52 2010 +0100 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_atp_translate.ML Wed Dec 08 22:17:53 2010 +0100 @@ -15,10 +15,10 @@ val conjecture_prefix : string val translate_atp_fact : Proof.context -> (string * 'a) * thm - -> term * ((string * 'a) * translated_formula) option + -> translated_formula option * ((string * 'a) * thm) val prepare_atp_problem : Proof.context -> bool -> bool -> bool -> bool -> term list -> term - -> (term * ((string * 'a) * translated_formula) option) list + -> (translated_formula option * ((string * 'a) * thm)) list -> string problem * string Symtab.table * int * (string * 'a) list vector end; @@ -194,10 +194,10 @@ ctypes_sorts = ctypes_sorts} end -fun make_fact ctxt presimp ((name, loc), th) = +fun make_fact ctxt presimp ((name, _), th) = case make_formula ctxt presimp name Axiom (prop_of th) of {combformula = AAtom (CombConst (("c_True", _), _, _)), ...} => NONE - | formula => SOME ((name, loc), formula) + | formula => SOME formula fun make_conjecture ctxt ts = let val last = length ts - 1 in map2 (fn j => make_formula ctxt true (Int.toString j) @@ -244,16 +244,20 @@ |> maps (fn (ss, ths) => if exists is_needed ss then map baptize ths else [])) @ (if is_FO then [] else map baptize mandatory_helpers) - |> map_filter (Option.map snd o make_fact ctxt false) + |> map_filter (make_fact ctxt false) end -fun translate_atp_fact ctxt (ax as (_, th)) = - (prop_of th, make_fact ctxt true ax) +fun translate_atp_fact ctxt = `(make_fact ctxt true) -fun translate_formulas ctxt full_types hyp_ts concl_t facts = +fun translate_formulas ctxt full_types hyp_ts concl_t rich_facts = let val thy = ProofContext.theory_of ctxt - val (fact_ts, translated_facts) = ListPair.unzip facts + val fact_ts = map (prop_of o snd o snd) rich_facts + val (facts, fact_names) = + rich_facts + |> map_filter (fn (NONE, _) => NONE + | (SOME fact, (name, _)) => SOME (fact, name)) + |> ListPair.unzip (* Remove existing facts from the conjecture, as this can dramatically boost an ATP's performance (for some reason). *) val hyp_ts = hyp_ts |> filter_out (member (op aconv) fact_ts) @@ -264,7 +268,6 @@ val tycons = type_consts_of_terms thy (goal_t :: fact_ts) (* TFrees in the conjecture; TVars in the facts *) val conjectures = make_conjecture ctxt (hyp_ts @ [concl_t]) - val (fact_names, facts) = ListPair.unzip (map_filter I translated_facts) val helper_facts = get_helper_facts ctxt is_FO full_types conjectures facts val (supers', arity_clauses) = make_arity_clauses thy tycons supers val class_rel_clauses = make_class_rel_clauses thy subs supers' diff -r b98fe4de1ecd -r 0afdf5cde874 src/HOL/Tools/Sledgehammer/sledgehammer_minimize.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_minimize.ML Wed Dec 08 22:17:52 2010 +0100 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_minimize.ML Wed Dec 08 22:17:53 2010 +0100 @@ -10,8 +10,12 @@ type locality = Sledgehammer_Filter.locality type params = Sledgehammer_Provers.params + val filter_used_facts : + (string * locality) list -> ((string * locality) * thm list) list + -> ((string * locality) * thm list) list val minimize_facts : - params -> int -> int -> Proof.state -> ((string * locality) * thm list) list + params -> bool -> int -> int -> Proof.state + -> ((string * locality) * thm list) list -> ((string * locality) * thm list) list option * string val run_minimize : params -> int -> (Facts.ref * Attrib.src list) list -> Proof.state -> unit @@ -42,12 +46,13 @@ "") end +fun print silent f = if silent then () else Output.urgent_message (f ()) + fun test_facts ({debug, overlord, provers, full_types, isar_proof, - isar_shrink_factor, ...} : params) (prover : prover) + isar_shrink_factor, ...} : params) silent (prover : prover) explicit_apply timeout i n state facts = let - val _ = - Output.urgent_message ("Testing " ^ n_facts (map fst facts) ^ "...") + val _ = print silent (fn () => "Testing " ^ n_facts (map fst facts) ^ "...") val params = {blocking = true, debug = debug, verbose = false, overlord = overlord, provers = provers, full_types = full_types, @@ -62,12 +67,12 @@ facts = facts} val result as {outcome, used_facts, ...} = prover params (K "") problem in - Output.urgent_message - (case outcome of - SOME failure => string_for_failure failure - | NONE => - if length used_facts = length facts then "Found proof." - else "Found proof with " ^ n_facts used_facts ^ "."); + print silent + (fn () => case outcome of + SOME failure => string_for_failure failure + | NONE => + if length used_facts = length facts then "Found proof." + else "Found proof with " ^ n_facts used_facts ^ "."); result end @@ -121,15 +126,15 @@ part of the timeout. *) val fudge_msecs = 1000 -fun minimize_facts {provers = [], ...} _ _ _ _ = error "No prover is set." - | minimize_facts (params as {provers = prover_name :: _, timeout, ...}) i n - state facts = +fun minimize_facts {provers = [], ...} _ _ _ _ _ = error "No prover is set." + | minimize_facts (params as {provers = prover_name :: _, timeout, ...}) silent + i n state facts = let val thy = Proof.theory_of state val ctxt = Proof.context_of state val prover = get_prover ctxt false prover_name val msecs = Time.toMilliseconds timeout - val _ = Output.urgent_message ("Sledgehammer minimize: " ^ + val _ = print silent (fn () => "Sledgehammer minimize: " ^ quote prover_name ^ ".") val {goal, ...} = Proof.goal state val (_, hyp_ts, concl_t) = strip_subgoal goal i @@ -137,7 +142,7 @@ not (forall (Meson.is_fol_term thy) (concl_t :: hyp_ts @ maps (map prop_of o snd) facts)) fun do_test timeout = - test_facts params prover explicit_apply timeout i n state + test_facts params silent prover explicit_apply timeout i n state val timer = Timer.startRealTimer () in (case do_test timeout facts of @@ -154,7 +159,7 @@ else sublinear_minimize (do_test new_timeout) facts ([], result) val n = length min_thms - val _ = Output.urgent_message (cat_lines + val _ = print silent (fn () => cat_lines ["Minimized: " ^ string_of_int n ^ " fact" ^ plural_s n] ^ (case length (filter (curry (op =) Chained o snd o fst) min_thms) of 0 => "" @@ -180,13 +185,14 @@ val reserved = reserved_isar_keyword_table () val chained_ths = #facts (Proof.goal state) val facts = - maps (map (apsnd single) o fact_from_ref ctxt reserved chained_ths) refs + refs + |> maps (map (apsnd single) o fact_from_ref ctxt reserved chained_ths) in case subgoal_count state of 0 => Output.urgent_message "No subgoal!" | n => (kill_provers (); - Output.urgent_message (#2 (minimize_facts params i n state facts))) + Output.urgent_message (#2 (minimize_facts params false i n state facts))) end end; diff -r b98fe4de1ecd -r 0afdf5cde874 src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML Wed Dec 08 22:17:52 2010 +0100 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML Wed Dec 08 22:17:53 2010 +0100 @@ -32,7 +32,7 @@ datatype prover_fact = Untranslated_Fact of (string * locality) * thm | ATP_Translated_Fact of - term * ((string * locality) * translated_formula) option + translated_formula option * ((string * locality) * thm) type prover_problem = {state: Proof.state, @@ -62,6 +62,7 @@ val dest_dir : string Config.T val problem_prefix : string Config.T val measure_run_time : bool Config.T + val untranslated_fact : prover_fact -> (string * locality) * thm val available_provers : Proof.context -> unit val kill_provers : unit -> unit val running_provers : unit -> unit @@ -213,8 +214,7 @@ datatype prover_fact = Untranslated_Fact of (string * locality) * thm | - ATP_Translated_Fact of - term * ((string * locality) * translated_formula) option + ATP_Translated_Fact of translated_formula option * ((string * locality) * thm) type prover_problem = {state: Proof.state, @@ -254,11 +254,10 @@ (* generic TPTP-based ATPs *) -fun dest_Untranslated_Fact (Untranslated_Fact p) = p - | dest_Untranslated_Fact (ATP_Translated_Fact _) = - raise Fail "dest_Untranslated_Fact" +fun untranslated_fact (Untranslated_Fact p) = p + | untranslated_fact (ATP_Translated_Fact (_, p)) = p fun atp_translated_fact ctxt (Untranslated_Fact p) = translate_atp_fact ctxt p - | atp_translated_fact _ (ATP_Translated_Fact p) = p + | atp_translated_fact _ (ATP_Translated_Fact q) = q fun int_opt_add (SOME m) (SOME n) = SOME (m + n) | int_opt_add _ _ = NONE @@ -276,8 +275,7 @@ let val ctxt = Proof.context_of state val (_, hyp_ts, concl_t) = strip_subgoal goal subgoal - val facts = - facts |> map (atp_translated_fact ctxt) + val facts = facts |> map (atp_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 @@ -530,9 +528,7 @@ #> 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_Fact - val facts = facts |> map_filter get_fact + val facts = facts |> map (apsnd (Thm.transfer thy) o untranslated_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) diff -r b98fe4de1ecd -r 0afdf5cde874 src/HOL/Tools/Sledgehammer/sledgehammer_run.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_run.ML Wed Dec 08 22:17:52 2010 +0100 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_run.ML Wed Dec 08 22:17:53 2010 +0100 @@ -24,6 +24,7 @@ open Sledgehammer_Filter open Sledgehammer_ATP_Translate open Sledgehammer_Provers +open Sledgehammer_Minimize fun prover_description ctxt ({blocking, verbose, ...} : params) name num_facts i n goal = @@ -38,6 +39,8 @@ else "\n" ^ Syntax.string_of_term ctxt (Thm.term_of (Thm.cprem_of goal i))) +val implicit_minimization_threshold = 50 + fun run_prover (params as {blocking, debug, max_relevant, timeout, expect, ...}) auto minimize_command only {state, goal, subgoal, subgoal_count, facts} name = @@ -58,8 +61,18 @@ let fun really_go () = prover params (minimize_command name) problem - |> (fn {outcome, message, ...} => - (if is_some outcome then "none" else "some", message)) + |> (fn {outcome, used_facts, message, ...} => + if is_some outcome then + ("none", message) + else + ("some", + if length used_facts >= implicit_minimization_threshold then + minimize_facts params true subgoal subgoal_count state + (filter_used_facts used_facts + (map (apsnd single o untranslated_fact) facts)) + |> snd + else + message)) val (outcome_code, message) = if debug then really_go () @@ -84,8 +97,8 @@ 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)])) + 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 @@ -101,9 +114,6 @@ (* FUDGE *) val auto_max_relevant_divisor = 2 -fun fact_name (Untranslated_Fact ((name, _), _)) = SOME name - | fact_name (ATP_Translated_Fact (_, 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 @@ -156,7 +166,7 @@ else "Including (up to) " ^ string_of_int (length facts) ^ " relevant fact" ^ plural_s (length facts) ^ ":\n" ^ - (facts |> map_filter fact_name + (facts |> map (fst o fst o untranslated_fact) |> space_implode " ") ^ ".")) else ();