# HG changeset patch # User blanchet # Date 1287733818 -7200 # Node ID 71cc5aac8b762b2d1e68b21b811709c95e73be94 # Parent 5ef6747aa6194d1fdba957f9db9dde254fb7f820 generalization of the Sledgehammer minimizer, to make it possible to handle SMT solvers as well diff -r 5ef6747aa619 -r 71cc5aac8b76 src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML --- a/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML Thu Oct 21 16:25:40 2010 +0200 +++ b/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML Fri Oct 22 09:50:18 2010 +0200 @@ -357,19 +357,18 @@ relevance_override chained_ths hyp_ts concl_t val problem = {state = st', goal = goal, subgoal = i, - axioms = map (Sledgehammer_Translate.prepare_axiom ctxt) axioms, - only = true} + axioms = axioms |> map Sledgehammer.Unprepared, only = true} val time_limit = (case hard_timeout of NONE => I | SOME secs => TimeLimit.timeLimit (Time.fromSeconds secs)) - val ({outcome, message, used_thm_names, - atp_run_time_in_msecs = time_atp, ...} : Sledgehammer.atp_result, + val ({outcome, message, used_axioms, run_time_in_msecs = time_atp, ...} + : Sledgehammer.prover_result, time_isa) = time_limit (Mirabelle.cpu_time (prover params (K ""))) problem in case outcome of - NONE => (message, SH_OK (time_isa, time_atp, used_thm_names)) + NONE => (message, SH_OK (time_isa, time_atp, used_axioms)) | SOME _ => (message, SH_FAIL (time_isa, time_atp)) end handle ERROR msg => ("error: " ^ msg, SH_ERROR) @@ -445,7 +444,7 @@ val params = Sledgehammer_Isar.default_params thy [("provers", prover_name), ("timeout", Int.toString timeout ^ " s")] val minimize = - Sledgehammer_Minimize.minimize_theorems params 1 (subgoal_count st) + Sledgehammer_Minimize.minimize_facts params 1 (subgoal_count st) val _ = log separator in case minimize st (these (!named_thms)) of diff -r 5ef6747aa619 -r 71cc5aac8b76 src/HOL/Tools/Sledgehammer/sledgehammer.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer.ML Thu Oct 21 16:25:40 2010 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer.ML Fri Oct 22 09:50:18 2010 +0200 @@ -29,25 +29,24 @@ timeout: Time.time, expect: string} - type atp_problem = + datatype axiom = + Unprepared of (string * locality) * thm | + Prepared of term * ((string * locality) * fol_formula) option + + type prover_problem = {state: Proof.state, goal: thm, subgoal: int, - axioms: (term * ((string * locality) * fol_formula) option) list, + axioms: axiom list, only: bool} - type atp_result = + type prover_result = {outcome: failure option, message: string, - pool: string Symtab.table, - used_thm_names: (string * locality) list, - atp_run_time_in_msecs: int, - output: string, - tstplike_proof: string, - axiom_names: (string * locality) list vector, - conjecture_shape: int list list} + used_axioms: (string * locality) list, + run_time_in_msecs: int} - type atp = params -> minimize_command -> atp_problem -> atp_result + type prover = params -> minimize_command -> prover_problem -> prover_result val smtN : string val dest_dir : string Config.T @@ -57,10 +56,11 @@ val kill_provers : unit -> unit val running_provers : unit -> unit val messages : int option -> unit - val run_atp : theory -> string -> atp + val run_atp : theory -> string -> prover + val is_smt_solver_installed : unit -> bool val run_smt_solver : - Proof.context -> bool -> Time.time -> ('a * thm) list -> string * 'a list - val is_smt_solver_installed : unit -> bool + bool -> params -> minimize_command -> prover_problem + -> string * (string * locality) list val run_sledgehammer : params -> bool -> int -> relevance_override -> (string -> minimize_command) -> Proof.state -> bool * Proof.state @@ -120,25 +120,24 @@ timeout: Time.time, expect: string} -type atp_problem = +datatype axiom = + Unprepared of (string * locality) * thm | + Prepared of term * ((string * locality) * fol_formula) option + +type prover_problem = {state: Proof.state, goal: thm, subgoal: int, - axioms: (term * ((string * locality) * fol_formula) option) list, + axioms: axiom list, only: bool} -type atp_result = +type prover_result = {outcome: failure option, message: string, - pool: string Symtab.table, - used_thm_names: (string * locality) list, - atp_run_time_in_msecs: int, - output: string, - tstplike_proof: string, - axiom_names: (string * locality) list vector, - conjecture_shape: int list list} + used_axioms: (string * locality) list, + run_time_in_msecs: int} -type atp = params -> minimize_command -> atp_problem -> atp_result +type prover = params -> minimize_command -> prover_problem -> prover_result (* configuration attributes *) @@ -176,6 +175,11 @@ (* generic TPTP-based ATPs *) +fun dest_Unprepared (Unprepared p) = p + | dest_Unprepared (Prepared _) = raise Fail "dest_Unprepared" +fun prepared_axiom ctxt (Unprepared p) = prepare_axiom ctxt p + | prepared_axiom _ (Prepared p) = p + (* Important messages are important but not so important that users want to see them each time. *) val important_message_keep_factor = 0.1 @@ -186,24 +190,26 @@ use_conjecture_for_hypotheses} ({debug, verbose, overlord, full_types, explicit_apply, max_relevant, isar_proof, isar_shrink_factor, timeout, ...} : params) - minimize_command ({state, goal, subgoal, axioms, only} : atp_problem) = + minimize_command + ({state, goal, subgoal, axioms, only} : prover_problem) = let val ctxt = Proof.context_of state val (_, hyp_ts, concl_t) = strip_subgoal goal subgoal - val axioms = axioms |> not only - ? take (the_default default_max_relevant max_relevant) + val axioms = + axioms |> not only ? take (the_default default_max_relevant max_relevant) + |> map (prepared_axiom 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 atp_problem_file_name = + val problem_file_name = Path.basic ((if overlord then "prob_" ^ atp_name else problem_prefix ^ serial_string ()) ^ "_" ^ string_of_int subgoal) - val atp_problem_path_name = + val problem_path_name = if dest_dir = "" then - File.tmp_path atp_problem_file_name + File.tmp_path problem_file_name else if File.exists (Path.explode dest_dir) then - Path.append (Path.explode dest_dir) atp_problem_file_name + 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 @@ -288,7 +294,7 @@ File.write (Path.explode (Path.implode probfile ^ "_proof")) output val ((pool, conjecture_shape, axiom_names), (output, msecs, tstplike_proof, outcome)) = - with_path cleanup export run_on atp_problem_path_name + with_path cleanup export run_on problem_path_name val (conjecture_shape, axiom_names) = repair_conjecture_shape_and_axiom_names output conjecture_shape axiom_names @@ -297,7 +303,7 @@ extract_important_message output else "" - val (message, used_thm_names) = + val (message, used_axioms) = case outcome of NONE => proof_text isar_proof @@ -317,10 +323,8 @@ "")) | SOME failure => (string_for_failure failure, []) in - {outcome = outcome, message = message, pool = pool, - used_thm_names = used_thm_names, atp_run_time_in_msecs = msecs, - output = output, tstplike_proof = tstplike_proof, - axiom_names = axiom_names, conjecture_shape = conjecture_shape} + {outcome = outcome, message = message, used_axioms = used_axioms, + run_time_in_msecs = msecs} end fun run_atp thy name = atp_fun false name (get_atp thy name) @@ -328,8 +332,8 @@ fun run_atp_somehow (params as {blocking, debug, max_relevant, timeout, expect, ...}) auto i n minimize_command - (atp_problem as {state, goal, axioms, ...}) - (atp as {default_max_relevant, ...}, atp_name) = + (prover_problem as {state, goal, axioms, ...}) + (prover as {default_max_relevant, ...}, atp_name) = let val ctxt = Proof.context_of state val birth_time = Time.now () @@ -340,8 +344,8 @@ fun go () = let fun really_go () = - atp_fun auto atp_name atp params (minimize_command atp_name) - atp_problem + atp_fun auto atp_name prover params (minimize_command atp_name) + prover_problem |> (fn {outcome, message, ...} => (if is_some outcome then "none" else "some", message)) val (outcome_code, message) = @@ -379,25 +383,31 @@ end (* FIXME: dummy *) -fun run_smt_solver ctxt remote timeout axioms = - ("", axioms |> take 5 |> map fst) - -(* FIXME: dummy *) fun is_smt_solver_installed () = true -fun run_smt_solver_somehow ctxt (params as {timeout, ...}) i n goal axioms +(* FIXME: dummy *) +fun raw_run_smt_solver remote timeout state axioms i = + ("", axioms |> take 5 |> map fst) + +fun run_smt_solver remote ({timeout, ...} : params) minimize_command + ({state, subgoal, axioms, ...} : prover_problem) = + raw_run_smt_solver remote timeout state + (map_filter (try dest_Unprepared) axioms) subgoal + +fun run_smt_solver_somehow state (params as {timeout, ...}) i n goal axioms (remote, name) = let - val desc = - prover_description ctxt params name (length axioms) i n goal - val (failure, used_thm_names) = run_smt_solver ctxt remote timeout axioms + val ctxt = Proof.context_of state + val desc = prover_description ctxt params name (length axioms) i n goal + val (failure, used_axioms) = + raw_run_smt_solver remote timeout state axioms i val success = (failure = "") val message = das_Tool ^ ": " ^ desc ^ "\n" ^ (if success then sendback_line (proof_banner false) (apply_on_subgoal i n ^ - command_call "smt" (map fst used_thm_names)) + command_call "smt" (map fst used_axioms)) else "Error: " ^ failure) in priority message; success end @@ -441,15 +451,16 @@ relevant_facts ctxt full_types relevance_thresholds max_max_relevant relevance_override chained_ths hyp_ts concl_t - val atp_problem = + val prover_problem = {state = state, goal = goal, subgoal = i, - axioms = map (prepare_axiom ctxt) axioms, only = only} + axioms = axioms |> map (Prepared o prepare_axiom ctxt), + only = only} val run_atp_somehow = - run_atp_somehow params auto i n minimize_command atp_problem + run_atp_somehow params auto i n minimize_command prover_problem in if auto then - fold (fn atp => fn (true, state) => (true, state) - | (false, _) => run_atp_somehow atp) + fold (fn prover => fn (true, state) => (true, state) + | (false, _) => run_atp_somehow prover) atps (false, state) else atps |> (if blocking then Par_List.map else map) run_atp_somehow @@ -467,7 +478,7 @@ max_relevant relevance_override chained_ths hyp_ts concl_t in - smts |> map (run_smt_solver_somehow ctxt params i n goal axioms) + smts |> map (run_smt_solver_somehow state params i n goal axioms) |> exists I |> rpair state end fun run_atps_and_smt_solvers () = diff -r 5ef6747aa619 -r 71cc5aac8b76 src/HOL/Tools/Sledgehammer/sledgehammer_minimize.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_minimize.ML Thu Oct 21 16:25:40 2010 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_minimize.ML Fri Oct 22 09:50:18 2010 +0200 @@ -2,7 +2,7 @@ Author: Philipp Meyer, TU Muenchen Author: Jasmin Blanchette, TU Muenchen -Minimization of theorem list for Metis using automatic theorem provers. +Minimization of fact list for Metis using ATPs. *) signature SLEDGEHAMMER_MINIMIZE = @@ -10,7 +10,7 @@ type locality = Sledgehammer_Filter.locality type params = Sledgehammer.params - val minimize_theorems : + val minimize_facts : params -> int -> int -> Proof.state -> ((string * locality) * thm list) list -> ((string * locality) * thm list) list option * string val run_minimize : @@ -24,7 +24,6 @@ open Sledgehammer_Util open Sledgehammer_Filter open Sledgehammer_Translate -open Sledgehammer_Reconstruct open Sledgehammer (* wrapper for calling external prover *) @@ -34,9 +33,9 @@ | string_for_failure Interrupted = "Interrupted." | string_for_failure _ = "Unknown error." -fun n_theorems names = +fun n_facts names = let val n = length names in - string_of_int n ^ " theorem" ^ plural_s n ^ + string_of_int n ^ " fact" ^ plural_s n ^ (if n > 0 then ": " ^ (names |> map fst |> sort_distinct string_ord |> space_implode " ") @@ -44,45 +43,45 @@ "") end -fun test_theorems ({debug, verbose, overlord, provers, full_types, isar_proof, - isar_shrink_factor, ...} : params) - (atp : atp) explicit_apply timeout subgoal state axioms = +fun test_facts ({debug, verbose, overlord, provers, full_types, isar_proof, + isar_shrink_factor, ...} : params) (prover : prover) + explicit_apply timeout subgoal state axioms = let val _ = - priority ("Testing " ^ n_theorems (map fst axioms) ^ "...") + priority ("Testing " ^ n_facts (map fst axioms) ^ "...") val params = {blocking = true, debug = debug, verbose = verbose, overlord = overlord, provers = provers, full_types = full_types, explicit_apply = explicit_apply, relevance_thresholds = (1.01, 1.01), - max_relevant = SOME 65536 (* a large number *), isar_proof = isar_proof, + max_relevant = NONE, isar_proof = isar_proof, isar_shrink_factor = isar_shrink_factor, timeout = timeout, expect = ""} - val axioms = maps (fn (n, ths) => map (pair n) ths) axioms + val axioms = + axioms |> maps (fn (n, ths) => ths |> map (Unprepared o pair n)) val {context = ctxt, goal, ...} = Proof.goal state - val atp_problem = - {state = state, goal = goal, subgoal = subgoal, - axioms = map (prepare_axiom ctxt) axioms, only = true} - val result as {outcome, used_thm_names, ...} = atp params (K "") atp_problem + val prover_problem = + {state = state, goal = goal, subgoal = subgoal, axioms = axioms, + only = true} + val result as {outcome, used_axioms, ...} = + prover params (K "") prover_problem in priority (case outcome of - NONE => - if length used_thm_names = length axioms then - "Found proof." - else - "Found proof with " ^ n_theorems used_thm_names ^ "." - | SOME failure => string_for_failure failure); + SOME failure => string_for_failure failure + | NONE => + if length used_axioms = length axioms then "Found proof." + else "Found proof with " ^ n_facts used_axioms ^ "."); result end (* minimalization of thms *) -fun filter_used_facts used = filter (member (op =) used o fst) +fun filter_used_axioms used = filter (member (op =) used o fst) fun sublinear_minimize _ [] p = p | sublinear_minimize test (x :: xs) (seen, result) = case test (xs @ seen) of - result as {outcome = NONE, used_thm_names, ...} : atp_result => - sublinear_minimize test (filter_used_facts used_thm_names xs) - (filter_used_facts used_thm_names seen, result) + result as {outcome = NONE, used_axioms, ...} : prover_result => + sublinear_minimize test (filter_used_axioms used_axioms xs) + (filter_used_axioms used_axioms seen, result) | _ => sublinear_minimize test xs (x :: seen, result) (* Give the ATP some slack. The ATP gets further slack because the Sledgehammer @@ -90,48 +89,40 @@ timeout. *) val fudge_msecs = 1000 -fun minimize_theorems {provers = [], ...} _ _ _ _ = error "No prover is set." - | minimize_theorems (params as {debug, provers = prover :: _, full_types, - isar_proof, isar_shrink_factor, timeout, ...}) - i (_ : int) state axioms = +fun minimize_facts {provers = [], ...} _ _ _ _ = error "No prover is set." + | minimize_facts (params as {provers = prover_name :: _, timeout, ...}) + i (_ : int) state axioms = let val thy = Proof.theory_of state - val atp = run_atp thy prover + val prover = run_atp thy prover_name val msecs = Time.toMilliseconds timeout - val _ = priority ("Sledgehammer minimize: prover " ^ quote prover ^ ".") - val {context = ctxt, goal, ...} = Proof.goal state + val _ = priority ("Sledgehammer minimize: " ^ quote prover_name ^ ".") + val {goal, ...} = Proof.goal state val (_, hyp_ts, concl_t) = strip_subgoal goal i val explicit_apply = not (forall (Meson.is_fol_term thy) (concl_t :: hyp_ts @ maps (map prop_of o snd) axioms)) fun do_test timeout = - test_theorems params atp explicit_apply timeout i state + test_facts params prover explicit_apply timeout i state val timer = Timer.startRealTimer () in (case do_test timeout axioms of - result as {outcome = NONE, pool, used_thm_names, - conjecture_shape, ...} => + result as {outcome = NONE, used_axioms, ...} => let val time = Timer.checkRealTimer timer val new_timeout = Int.min (msecs, Time.toMilliseconds time + fudge_msecs) |> Time.fromMilliseconds - val (min_thms, {tstplike_proof, axiom_names, ...}) = + val (min_thms, {message, ...}) = sublinear_minimize (do_test new_timeout) - (filter_used_facts used_thm_names axioms) ([], result) + (filter_used_axioms used_axioms axioms) ([], result) val n = length min_thms val _ = priority (cat_lines - ["Minimized: " ^ string_of_int n ^ " theorem" ^ plural_s n] ^ + ["Minimized: " ^ string_of_int n ^ " fact" ^ plural_s n] ^ (case length (filter (curry (op =) Chained o snd o fst) min_thms) of 0 => "" | n => " (including " ^ Int.toString n ^ " chained)") ^ ".") - in - (SOME min_thms, - proof_text isar_proof - (pool, debug, isar_shrink_factor, ctxt, conjecture_shape) - ("Minimized command", full_types, K "", tstplike_proof, - axiom_names, goal, i) |> fst) - end + in (SOME min_thms, message) end | {outcome = SOME TimedOut, ...} => (NONE, "Timeout: You can increase the time limit using the \"timeout\" \ \option (e.g., \"timeout = " ^ @@ -159,7 +150,7 @@ 0 => priority "No subgoal!" | n => (kill_provers (); - priority (#2 (minimize_theorems params i n state axioms))) + priority (#2 (minimize_facts params i n state axioms))) end end;