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