# HG changeset patch # User blanchet # Date 1287738694 -7200 # Node ID cfaebaa8588f2f41bba2febbdd9242763a0d1d39 # Parent 71cc5aac8b762b2d1e68b21b811709c95e73be94 make Sledgehammer minimizer fully work with SMT diff -r 71cc5aac8b76 -r cfaebaa8588f NEWS --- a/NEWS Fri Oct 22 09:50:18 2010 +0200 +++ b/NEWS Fri Oct 22 11:11:34 2010 +0200 @@ -296,7 +296,7 @@ INCOMPATIBILITY. - Renamed options: sledgehammer [atps = ...] ~> sledgehammer [provers = ...] - sledgehammer [atp = ...] ~> sledgehammer [provers = ...] + sledgehammer [atp = ...] ~> sledgehammer [prover = ...] INCOMPATIBILITY. diff -r 71cc5aac8b76 -r cfaebaa8588f src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML --- a/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML Fri Oct 22 09:50:18 2010 +0200 +++ b/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML Fri Oct 22 11:11:34 2010 +0200 @@ -29,8 +29,8 @@ lemmas: int, max_lems: int, time_isa: int, - time_atp: int, - time_atp_fail: int} + time_prover: int, + time_prover_fail: int} datatype me_data = MeData of { calls: int, @@ -51,10 +51,11 @@ fun make_sh_data (calls,success,nontriv_calls,nontriv_success,lemmas,max_lems,time_isa, - time_atp,time_atp_fail) = + time_prover,time_prover_fail) = ShData{calls=calls, success=success, nontriv_calls=nontriv_calls, nontriv_success=nontriv_success, lemmas=lemmas, max_lems=max_lems, - time_isa=time_isa, time_atp=time_atp, time_atp_fail=time_atp_fail} + time_isa=time_isa, time_prover=time_prover, + time_prover_fail=time_prover_fail} fun make_min_data (succs, ab_ratios) = MinData{succs=succs, ab_ratios=ab_ratios} @@ -71,8 +72,8 @@ fun tuple_of_sh_data (ShData {calls, success, nontriv_calls, nontriv_success, lemmas, max_lems, time_isa, - time_atp, time_atp_fail}) = (calls, success, nontriv_calls, nontriv_success, - lemmas, max_lems, time_isa, time_atp, time_atp_fail) + time_prover, time_prover_fail}) = (calls, success, nontriv_calls, + nontriv_success, lemmas, max_lems, time_isa, time_prover, time_prover_fail) fun tuple_of_min_data (MinData {succs, ab_ratios}) = (succs, ab_ratios) @@ -127,40 +128,40 @@ fun inc_max (n:int) (s,sos,m) = (s+n, sos + n*n, Int.max(m,n)); val inc_sh_calls = map_sh_data - (fn (calls, success, nontriv_calls, nontriv_success, lemmas,max_lems, time_isa, time_atp, time_atp_fail) - => (calls + 1, success, nontriv_calls, nontriv_success, lemmas, max_lems, time_isa, time_atp, time_atp_fail)) + (fn (calls, success, nontriv_calls, nontriv_success, lemmas,max_lems, time_isa, time_prover, time_prover_fail) + => (calls + 1, success, nontriv_calls, nontriv_success, lemmas, max_lems, time_isa, time_prover, time_prover_fail)) val inc_sh_success = map_sh_data - (fn (calls, success, nontriv_calls, nontriv_success, lemmas,max_lems, time_isa, time_atp, time_atp_fail) - => (calls, success + 1, nontriv_calls, nontriv_success, lemmas,max_lems, time_isa, time_atp, time_atp_fail)) + (fn (calls, success, nontriv_calls, nontriv_success, lemmas,max_lems, time_isa, time_prover, time_prover_fail) + => (calls, success + 1, nontriv_calls, nontriv_success, lemmas,max_lems, time_isa, time_prover, time_prover_fail)) val inc_sh_nontriv_calls = map_sh_data - (fn (calls, success, nontriv_calls, nontriv_success, lemmas,max_lems, time_isa, time_atp, time_atp_fail) - => (calls, success, nontriv_calls + 1, nontriv_success, lemmas, max_lems, time_isa, time_atp, time_atp_fail)) + (fn (calls, success, nontriv_calls, nontriv_success, lemmas,max_lems, time_isa, time_prover, time_prover_fail) + => (calls, success, nontriv_calls + 1, nontriv_success, lemmas, max_lems, time_isa, time_prover, time_prover_fail)) val inc_sh_nontriv_success = map_sh_data - (fn (calls, success, nontriv_calls, nontriv_success, lemmas,max_lems, time_isa, time_atp, time_atp_fail) - => (calls, success, nontriv_calls, nontriv_success + 1, lemmas,max_lems, time_isa, time_atp, time_atp_fail)) + (fn (calls, success, nontriv_calls, nontriv_success, lemmas,max_lems, time_isa, time_prover, time_prover_fail) + => (calls, success, nontriv_calls, nontriv_success + 1, lemmas,max_lems, time_isa, time_prover, time_prover_fail)) fun inc_sh_lemmas n = map_sh_data - (fn (calls,success,nontriv_calls, nontriv_success, lemmas,max_lems,time_isa,time_atp,time_atp_fail) - => (calls,success,nontriv_calls, nontriv_success, lemmas+n,max_lems,time_isa,time_atp,time_atp_fail)) + (fn (calls,success,nontriv_calls, nontriv_success, lemmas,max_lems,time_isa,time_prover,time_prover_fail) + => (calls,success,nontriv_calls, nontriv_success, lemmas+n,max_lems,time_isa,time_prover,time_prover_fail)) fun inc_sh_max_lems n = map_sh_data - (fn (calls,success,nontriv_calls, nontriv_success, lemmas,max_lems,time_isa,time_atp,time_atp_fail) - => (calls,success,nontriv_calls, nontriv_success, lemmas,Int.max(max_lems,n),time_isa,time_atp,time_atp_fail)) + (fn (calls,success,nontriv_calls, nontriv_success, lemmas,max_lems,time_isa,time_prover,time_prover_fail) + => (calls,success,nontriv_calls, nontriv_success, lemmas,Int.max(max_lems,n),time_isa,time_prover,time_prover_fail)) fun inc_sh_time_isa t = map_sh_data - (fn (calls,success,nontriv_calls, nontriv_success, lemmas,max_lems,time_isa,time_atp,time_atp_fail) - => (calls,success,nontriv_calls, nontriv_success, lemmas,max_lems,time_isa + t,time_atp,time_atp_fail)) + (fn (calls,success,nontriv_calls, nontriv_success, lemmas,max_lems,time_isa,time_prover,time_prover_fail) + => (calls,success,nontriv_calls, nontriv_success, lemmas,max_lems,time_isa + t,time_prover,time_prover_fail)) -fun inc_sh_time_atp t = map_sh_data - (fn (calls,success,nontriv_calls, nontriv_success, lemmas,max_lems,time_isa,time_atp,time_atp_fail) - => (calls,success,nontriv_calls, nontriv_success, lemmas,max_lems,time_isa,time_atp + t,time_atp_fail)) +fun inc_sh_time_prover t = map_sh_data + (fn (calls,success,nontriv_calls, nontriv_success, lemmas,max_lems,time_isa,time_prover,time_prover_fail) + => (calls,success,nontriv_calls, nontriv_success, lemmas,max_lems,time_isa,time_prover + t,time_prover_fail)) -fun inc_sh_time_atp_fail t = map_sh_data - (fn (calls,success,nontriv_calls, nontriv_success, lemmas,max_lems,time_isa,time_atp,time_atp_fail) - => (calls,success,nontriv_calls, nontriv_success, lemmas,max_lems,time_isa,time_atp,time_atp_fail + t)) +fun inc_sh_time_prover_fail t = map_sh_data + (fn (calls,success,nontriv_calls, nontriv_success, lemmas,max_lems,time_isa,time_prover,time_prover_fail) + => (calls,success,nontriv_calls, nontriv_success, lemmas,max_lems,time_isa,time_prover,time_prover_fail + t)) val inc_min_succs = map_min_data (fn (succs,ab_ratios) => (succs+1, ab_ratios)) @@ -214,7 +215,7 @@ if n > 0 then (Real.fromInt t / 1000.0) / Real.fromInt n else 0.0 fun log_sh_data log - (calls, success, nontriv_calls, nontriv_success, lemmas, max_lems, time_isa, time_atp, time_atp_fail) = + (calls, success, nontriv_calls, nontriv_success, lemmas, max_lems, time_isa, time_prover, time_prover_fail) = (log ("Total number of sledgehammer calls: " ^ str calls); log ("Number of successful sledgehammer calls: " ^ str success); log ("Number of sledgehammer lemmas: " ^ str lemmas); @@ -223,14 +224,14 @@ log ("Total number of nontrivial sledgehammer calls: " ^ str nontriv_calls); log ("Number of successful nontrivial sledgehammer calls: " ^ str nontriv_success); log ("Total time for sledgehammer calls (Isabelle): " ^ str3 (time time_isa)); - log ("Total time for successful sledgehammer calls (ATP): " ^ str3 (time time_atp)); - log ("Total time for failed sledgehammer calls (ATP): " ^ str3 (time time_atp_fail)); + log ("Total time for successful sledgehammer calls (ATP): " ^ str3 (time time_prover)); + log ("Total time for failed sledgehammer calls (ATP): " ^ str3 (time time_prover_fail)); log ("Average time for sledgehammer calls (Isabelle): " ^ str3 (avg_time time_isa calls)); log ("Average time for successful sledgehammer calls (ATP): " ^ - str3 (avg_time time_atp success)); + str3 (avg_time time_prover success)); log ("Average time for failed sledgehammer calls (ATP): " ^ - str3 (avg_time time_atp_fail (calls - success))) + str3 (avg_time time_prover_fail (calls - success))) ) @@ -313,16 +314,16 @@ fun change_data id f = (Unsynchronized.change data (AList.map_entry (op =) id f); ()) -fun get_atp thy args = +fun get_prover thy args = let - fun default_atp_name () = + fun default_prover_name () = hd (#provers (Sledgehammer_Isar.default_params thy [])) handle Empty => error "No ATP available." - fun get_atp name = (name, Sledgehammer.run_atp thy name) + fun get_prover name = (name, Sledgehammer.get_prover thy name) in (case AList.lookup (op =) args proverK of - SOME name => get_atp name - | NONE => get_atp (default_atp_name ())) + SOME name => get_prover name + | NONE => get_prover (default_prover_name ())) end type locality = Sledgehammer_Filter.locality @@ -349,7 +350,11 @@ Sledgehammer_Isar.default_params thy [("timeout", Int.toString timeout ^ " s")] val relevance_override = {add = [], del = [], only = false} - val {default_max_relevant, ...} = ATP_Systems.get_atp thy prover_name + val default_max_relevant = + if member (op =) Sledgehammer.smt_prover_names prover_name then + Sledgehammer.smt_default_max_relevant + else + #default_max_relevant (ATP_Systems.get_atp thy prover_name) val (_, hyp_ts, concl_t) = Sledgehammer_Util.strip_subgoal goal i val axioms = Sledgehammer_Filter.relevant_facts ctxt full_types relevance_thresholds @@ -362,14 +367,14 @@ (case hard_timeout of NONE => I | SOME secs => TimeLimit.timeLimit (Time.fromSeconds secs)) - val ({outcome, message, used_axioms, run_time_in_msecs = time_atp, ...} + val ({outcome, message, used_axioms, run_time_in_msecs = SOME time_prover, ...} : 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_axioms)) - | SOME _ => (message, SH_FAIL (time_isa, time_atp)) + NONE => (message, SH_OK (time_isa, time_prover, used_axioms)) + | SOME _ => (message, SH_FAIL (time_isa, time_prover)) end handle ERROR msg => ("error: " ^ msg, SH_ERROR) | TimeLimit.TimeOut => ("timeout", SH_ERROR) @@ -394,7 +399,7 @@ val triv_str = if trivial then "[T] " else "" val _ = change_data id inc_sh_calls val _ = if trivial then () else change_data id inc_sh_nontriv_calls - val (prover_name, prover) = get_atp (Proof.theory_of st) args + val (prover_name, prover) = get_prover (Proof.theory_of st) args val dir = AList.lookup (op =) args keepK val timeout = Mirabelle.get_int_setting args (prover_timeoutK, 30) val hard_timeout = AList.lookup (op =) args prover_hard_timeoutK @@ -402,7 +407,7 @@ val (msg, result) = run_sh prover_name prover hard_timeout timeout dir st in case result of - SH_OK (time_isa, time_atp, names) => + SH_OK (time_isa, time_prover, names) => let fun get_thms (_, Sledgehammer_Filter.Chained) = NONE | get_thms (name, loc) = @@ -413,15 +418,15 @@ change_data id (inc_sh_lemmas (length names)); change_data id (inc_sh_max_lems (length names)); change_data id (inc_sh_time_isa time_isa); - change_data id (inc_sh_time_atp time_atp); + change_data id (inc_sh_time_prover time_prover); named_thms := SOME (map_filter get_thms names); log (sh_tag id ^ triv_str ^ "succeeded (" ^ string_of_int time_isa ^ "+" ^ - string_of_int time_atp ^ ") [" ^ prover_name ^ "]:\n" ^ msg) + string_of_int time_prover ^ ") [" ^ prover_name ^ "]:\n" ^ msg) end - | SH_FAIL (time_isa, time_atp) => + | SH_FAIL (time_isa, time_prover) => let val _ = change_data id (inc_sh_time_isa time_isa) - val _ = change_data id (inc_sh_time_atp_fail time_atp) + val _ = change_data id (inc_sh_time_prover_fail time_prover) in log (sh_tag id ^ triv_str ^ "failed: " ^ msg) end | SH_ERROR => log (sh_tag id ^ "failed: " ^ msg) end @@ -436,7 +441,7 @@ open Metis_Translate val thy = Proof.theory_of st val n0 = length (these (!named_thms)) - val (prover_name, _) = get_atp thy args + val (prover_name, _) = get_prover thy args val timeout = AList.lookup (op =) args minimize_timeoutK |> Option.map (fst o read_int o explode) diff -r 71cc5aac8b76 -r cfaebaa8588f src/HOL/Tools/Sledgehammer/sledgehammer.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer.ML Fri Oct 22 09:50:18 2010 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer.ML Fri Oct 22 11:11:34 2010 +0200 @@ -42,13 +42,15 @@ type prover_result = {outcome: failure option, - message: string, used_axioms: (string * locality) list, - run_time_in_msecs: int} + run_time_in_msecs: int option, + message: string} type prover = params -> minimize_command -> prover_problem -> prover_result val smtN : string + val smt_prover_names : string list + val smt_default_max_relevant : int val dest_dir : string Config.T val problem_prefix : string Config.T val measure_run_time : bool Config.T @@ -56,11 +58,7 @@ val kill_provers : unit -> unit val running_provers : unit -> unit val messages : int option -> unit - val run_atp : theory -> string -> prover - val is_smt_solver_installed : unit -> bool - val run_smt_solver : - bool -> params -> minimize_command -> prover_problem - -> string * (string * locality) list + val get_prover : theory -> string -> prover val run_sledgehammer : params -> bool -> int -> relevance_override -> (string -> minimize_command) -> Proof.state -> bool * Proof.state @@ -87,12 +85,15 @@ val das_Tool = "Sledgehammer" val smtN = "smt" -val smt_names = [smtN, remote_prefix ^ smtN] +val smt_prover_names = [smtN, remote_prefix ^ smtN] + +val smt_default_max_relevant = 300 (* FUDGE *) +val auto_max_relevant_divisor = 2 (* FUDGE *) fun available_provers thy = let val (remote_provers, local_provers) = - sort_strings (available_atps thy) @ smt_names + sort_strings (available_atps thy) @ smt_prover_names |> List.partition (String.isPrefix remote_prefix) in priority ("Available provers: " ^ commas (local_provers @ remote_provers) ^ @@ -135,7 +136,7 @@ {outcome: failure option, message: string, used_axioms: (string * locality) list, - run_time_in_msecs: int} + run_time_in_msecs: int option} type prover = params -> minimize_command -> prover_problem -> prover_result @@ -180,6 +181,9 @@ fun prepared_axiom ctxt (Unprepared p) = prepare_axiom ctxt p | prepared_axiom _ (Prepared p) = p +fun int_option_add (SOME m) (SOME n) = SOME (m + n) + | int_option_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 @@ -232,7 +236,7 @@ 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 = the_default 0 o Scan.read Symbol.stopper time o explode; + val as_time = Scan.read Symbol.stopper time o explode in (output, as_time t) end; fun run_on probfile = case filter (curry (op =) "" o getenv o fst) (exec :: required_execs) of @@ -250,7 +254,7 @@ prefix ("% " ^ command ^ "\n% " ^ timestamp () ^ "\n") else I) - |>> (if measure_run_time then split_time else rpair 0) + |>> (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 @@ -277,7 +281,8 @@ ? (fn (_, msecs0, _, SOME _) => run true (Time.- (timeout, Timer.checkRealTimer timer)) |> (fn (output, msecs, tstplike_proof, outcome) => - (output, msecs0 + msecs, tstplike_proof, outcome)) + (output, int_option_add msecs0 msecs, + tstplike_proof, outcome)) | result => result) in ((pool, conjecture_shape, axiom_names), result) end else @@ -312,8 +317,8 @@ axiom_names, goal, subgoal) |>> (fn message => message ^ (if verbose then - "\nATP real CPU time: " ^ string_of_int msecs ^ - " ms." + "\nATP real CPU time: " ^ + string_of_int (the msecs) ^ " ms." else "") ^ (if important_message <> "" then @@ -327,12 +332,12 @@ run_time_in_msecs = msecs} end -fun run_atp thy name = atp_fun false name (get_atp thy name) +fun get_atp_as_prover thy name = atp_fun false name (get_atp thy name) fun run_atp_somehow (params as {blocking, debug, max_relevant, timeout, expect, ...}) auto i n minimize_command - (prover_problem as {state, goal, axioms, ...}) + (problem as {state, goal, axioms, ...}) (prover as {default_max_relevant, ...}, atp_name) = let val ctxt = Proof.context_of state @@ -345,7 +350,7 @@ let fun really_go () = atp_fun auto atp_name prover params (minimize_command atp_name) - prover_problem + problem |> (fn {outcome, message, ...} => (if is_some outcome then "none" else "some", message)) val (outcome_code, message) = @@ -383,37 +388,49 @@ end (* FIXME: dummy *) -fun is_smt_solver_installed () = true - -(* FIXME: dummy *) -fun raw_run_smt_solver remote timeout state axioms i = - ("", axioms |> take 5 |> map fst) +fun run_smt_solver remote timeout state axioms i = + {outcome = NONE, used_axioms = axioms |> take 5 |> map fst, + run_time_in_msecs = NONE} -fun run_smt_solver remote ({timeout, ...} : params) minimize_command - ({state, subgoal, axioms, ...} : prover_problem) = - raw_run_smt_solver remote timeout state +fun get_smt_solver_as_prover remote ({timeout, ...} : params) minimize_command + ({state, subgoal, axioms, ...} : prover_problem) = + let + val {outcome, used_axioms, run_time_in_msecs} = + run_smt_solver remote timeout state (map_filter (try dest_Unprepared) axioms) subgoal + val message = + if outcome = NONE then + sendback_line (proof_banner false) + (apply_on_subgoal subgoal (subgoal_count state) ^ + command_call smtN (map fst used_axioms)) + else + "" + in + {outcome = outcome, used_axioms = used_axioms, + run_time_in_msecs = run_time_in_msecs, message = message} + end -fun run_smt_solver_somehow state (params as {timeout, ...}) i n goal axioms +fun get_prover thy name = + if member (op =) smt_prover_names name then + get_smt_solver_as_prover (String.isPrefix remote_prefix) + else + get_atp_as_prover thy name + +fun run_smt_solver_somehow state params minimize_command i n goal axioms (remote, name) = let 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_axioms)) - else - "Error: " ^ failure) - in priority message; success end - -val smt_default_max_relevant = 300 (* FUDGE *) -val auto_max_relevant_divisor = 2 (* FUDGE *) + val problem = + {state = state, goal = goal, subgoal = i, + axioms = axioms |> map Unprepared, only = true} + val {outcome, used_axioms, message, ...} = + get_smt_solver_as_prover remote params minimize_command problem + val _ = + priority (das_Tool ^ ": " ^ desc ^ "\n" ^ + (if outcome = NONE then message + else "An unknown error occurred.")) + in outcome = NONE end fun run_sledgehammer (params as {blocking, provers, full_types, relevance_thresholds, max_relevant, timeout, @@ -433,7 +450,7 @@ val _ = () |> not blocking ? kill_provers val _ = if auto then () else priority "Sledgehammering..." val (smts, atps) = - provers |> List.partition (member (op =) smt_names) + provers |> List.partition (member (op =) smt_prover_names) |>> (take 1 #> map (`(String.isPrefix remote_prefix))) ||> map (`(get_atp thy)) fun run_atps (res as (success, state)) = @@ -451,12 +468,12 @@ relevant_facts ctxt full_types relevance_thresholds max_max_relevant relevance_override chained_ths hyp_ts concl_t - val prover_problem = + val problem = {state = state, goal = goal, subgoal = i, axioms = axioms |> map (Prepared o prepare_axiom ctxt), only = only} val run_atp_somehow = - run_atp_somehow params auto i n minimize_command prover_problem + run_atp_somehow params auto i n minimize_command problem in if auto then fold (fn prover => fn (true, state) => (true, state) @@ -478,7 +495,8 @@ max_relevant relevance_override chained_ths hyp_ts concl_t in - smts |> map (run_smt_solver_somehow state params i n goal axioms) + smts |> map (run_smt_solver_somehow state params minimize_command i + n goal axioms) |> exists I |> rpair state end fun run_atps_and_smt_solvers () = diff -r 71cc5aac8b76 -r cfaebaa8588f src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML Fri Oct 22 09:50:18 2010 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML Fri Oct 22 11:11:34 2010 +0200 @@ -130,6 +130,9 @@ val extend = I fun merge p : T = AList.merge (op =) (K true) p) +(* FIXME: dummy *) +fun is_smt_solver_installed () = true + fun maybe_remote_atp thy name = name |> not (is_atp_installed thy name) ? prefix remote_prefix fun maybe_remote_smt_solver thy = diff -r 71cc5aac8b76 -r cfaebaa8588f src/HOL/Tools/Sledgehammer/sledgehammer_minimize.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_minimize.ML Fri Oct 22 09:50:18 2010 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_minimize.ML Fri Oct 22 11:11:34 2010 +0200 @@ -94,7 +94,7 @@ i (_ : int) state axioms = let val thy = Proof.theory_of state - val prover = run_atp thy prover_name + val prover = get_prover thy prover_name val msecs = Time.toMilliseconds timeout val _ = priority ("Sledgehammer minimize: " ^ quote prover_name ^ ".") val {goal, ...} = Proof.goal state