# HG changeset patch # User blanchet # Date 1306767638 -7200 # Node ID 59284a13abc46efb01963b8f82c2197d3bab4c15 # Parent 99985426c0bb9bd5eaa121f3bd209d1c8d69f91c support "metis" and "metisFT" as provers in the architecture, so they can be used for minimizing diff -r 99985426c0bb -r 59284a13abc4 src/HOL/Tools/ATP/atp_proof.ML --- a/src/HOL/Tools/ATP/atp_proof.ML Mon May 30 15:30:05 2011 +0100 +++ b/src/HOL/Tools/ATP/atp_proof.ML Mon May 30 17:00:38 2011 +0200 @@ -16,7 +16,7 @@ datatype failure = Unprovable | - IncompleteUnprovable | + GaveUp | ProofMissing | ProofIncomplete | UnsoundProof of bool * string list | @@ -73,7 +73,7 @@ datatype failure = Unprovable | - IncompleteUnprovable | + GaveUp | ProofMissing | ProofIncomplete | UnsoundProof of bool * string list | @@ -146,7 +146,7 @@ " " fun string_for_failure Unprovable = "The problem is unprovable." - | string_for_failure IncompleteUnprovable = "The prover gave up." + | string_for_failure GaveUp = "The prover gave up." | string_for_failure ProofMissing = "The prover claims the conjecture is a theorem but did not provide a proof." | string_for_failure ProofIncomplete = @@ -231,7 +231,7 @@ extract_known_failure known_failures output) of (_, SOME ProofIncomplete) => ("", SOME ProofIncomplete) | ("", SOME failure) => - ("", SOME (if failure = IncompleteUnprovable andalso complete then Unprovable + ("", SOME (if failure = GaveUp andalso complete then Unprovable else failure)) | ("", NONE) => ("", SOME (if res_code = 0 andalso output = "" then ProofMissing diff -r 99985426c0bb -r 59284a13abc4 src/HOL/Tools/ATP/atp_systems.ML --- a/src/HOL/Tools/ATP/atp_systems.ML Mon May 30 15:30:05 2011 +0100 +++ b/src/HOL/Tools/ATP/atp_systems.ML Mon May 30 17:00:38 2011 +0200 @@ -256,7 +256,7 @@ proof_delims = [("Here is a proof", "Formulae used in the proof")], known_failures = known_perl_failures @ - [(IncompleteUnprovable, "SPASS beiseite: Completion found"), + [(GaveUp, "SPASS beiseite: Completion found"), (TimedOut, "SPASS beiseite: Ran out of time"), (OutOfResources, "SPASS beiseite: Maximal number of loops exceeded"), (MalformedInput, "Undefined symbol"), @@ -296,9 +296,9 @@ ("% SZS output start Refutation", "% SZS output end Refutation"), ("% SZS output start Proof", "% SZS output end Proof")], known_failures = - [(Unprovable, "UNPROVABLE"), - (IncompleteUnprovable, "CANNOT PROVE"), - (IncompleteUnprovable, "SZS status GaveUp"), + [(GaveUp, "UNPROVABLE"), + (GaveUp, "CANNOT PROVE"), + (GaveUp, "SZS status GaveUp"), (ProofIncomplete, "predicate_definition_introduction,[]"), (TimedOut, "SZS status Timeout"), (Unprovable, "Satisfiability detected"), @@ -329,8 +329,8 @@ proof_delims = [], known_failures = [(Unprovable, "\nsat"), - (IncompleteUnprovable, "\nunknown"), - (IncompleteUnprovable, "SZS status Satisfiable"), + (GaveUp, "\nunknown"), + (GaveUp, "SZS status Satisfiable"), (ProofMissing, "\nunsat"), (ProofMissing, "SZS status Unsatisfiable")], conj_sym_kind = Hypothesis, @@ -388,10 +388,10 @@ known_failures = known_failures @ known_perl_failures @ [(Unprovable, "says Satisfiable"), (Unprovable, "says CounterSatisfiable"), + (GaveUp, "says Unknown"), + (GaveUp, "says GaveUp"), (ProofMissing, "says Theorem"), (ProofMissing, "says Unsatisfiable"), - (IncompleteUnprovable, "says Unknown"), - (IncompleteUnprovable, "says GaveUp"), (TimedOut, "says Timeout"), (Inappropriate, "says Inappropriate")], conj_sym_kind = conj_sym_kind, diff -r 99985426c0bb -r 59284a13abc4 src/HOL/Tools/Metis/metis_tactics.ML --- a/src/HOL/Tools/Metis/metis_tactics.ML Mon May 30 15:30:05 2011 +0100 +++ b/src/HOL/Tools/Metis/metis_tactics.ML Mon May 30 17:00:38 2011 +0200 @@ -9,6 +9,9 @@ signature METIS_TACTICS = sig + val metisN : string + val metisF_N : string + val metisFT_N : string val trace : bool Config.T val verbose : bool Config.T val type_lits : bool Config.T @@ -26,6 +29,14 @@ open Metis_Translate open Metis_Reconstruct +fun method_binding_for_mode HO = @{binding metis} + | method_binding_for_mode FO = @{binding metisF} + | method_binding_for_mode FT = @{binding metisFT} + +val metisN = Binding.qualified_name_of (method_binding_for_mode HO) +val metisF_N = Binding.qualified_name_of (method_binding_for_mode FO) +val metisFT_N = Binding.qualified_name_of (method_binding_for_mode FT) + val type_lits = Attrib.setup_config_bool @{binding metis_type_lits} (K true) val new_skolemizer = Attrib.setup_config_bool @{binding metis_new_skolemizer} (K false) @@ -53,10 +64,6 @@ models = []} val resolution_params = {active = active_params, waiting = waiting_params} -fun method_binding_for_mode HO = @{binding metis} - | method_binding_for_mode FO = @{binding metisF} - | method_binding_for_mode FT = @{binding metisFT} - (* Main function to start Metis proof and reconstruction *) fun FOL_SOLVE (mode :: fallback_modes) ctxt cls ths0 = let val thy = Proof_Context.theory_of ctxt @@ -136,7 +143,8 @@ | mode :: _ => (verbose_warning ctxt ("Falling back on " ^ - quote (Binding.str_of (method_binding_for_mode mode)) ^ "..."); + quote (Binding.qualified_name_of + (method_binding_for_mode mode)) ^ "..."); FOL_SOLVE fallback_modes ctxt cls ths0) val neg_clausify = diff -r 99985426c0bb -r 59284a13abc4 src/HOL/Tools/Sledgehammer/sledgehammer_atp_reconstruct.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_atp_reconstruct.ML Mon May 30 15:30:05 2011 +0100 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_atp_reconstruct.ML Mon May 30 17:00:38 2011 +0200 @@ -17,14 +17,14 @@ MetisFT | SMT of string - datatype preplay = - Preplayed of reconstructor * Time.time | + datatype play = + Played of reconstructor * Time.time | Trust_Playable of reconstructor * Time.time option| - Failed_to_Preplay + Failed_to_Play type minimize_command = string list -> string type one_line_params = - preplay * string * (string * locality) list * minimize_command * int * int + play * string * (string * locality) list * minimize_command * int * int type isar_params = bool * bool * int * type_system * string Symtab.table * int list list * int * (string * locality) list vector * int Symtab.table * string proof @@ -62,14 +62,14 @@ MetisFT | SMT of string -datatype preplay = - Preplayed of reconstructor * Time.time | +datatype play = + Played of reconstructor * Time.time | Trust_Playable of reconstructor * Time.time option | - Failed_to_Preplay + Failed_to_Play type minimize_command = string list -> string type one_line_params = - preplay * string * (string * locality) list * minimize_command * int * int + play * string * (string * locality) list * minimize_command * int * int type isar_params = bool * bool * int * type_system * string Symtab.table * int list list * int * (string * locality) list vector * int Symtab.table * string proof * thm @@ -288,7 +288,7 @@ val (chained, extra) = split_used_facts used_facts val (reconstructor, ext_time) = case preplay of - Preplayed (reconstructor, time) => + Played (reconstructor, time) => (SOME reconstructor, (SOME (false, time))) | Trust_Playable (reconstructor, time) => (SOME reconstructor, @@ -296,7 +296,7 @@ NONE => NONE | SOME time => if time = Time.zeroTime then NONE else SOME (true, time)) - | Failed_to_Preplay => (NONE, NONE) + | Failed_to_Play => (NONE, NONE) val try_line = case reconstructor of SOME r => ([], map fst extra) @@ -1076,7 +1076,7 @@ fun proof_text ctxt isar_proof isar_params (one_line_params as (preplay, _, _, _, _, _)) = - (if isar_proof orelse preplay = Failed_to_Preplay then + (if isar_proof orelse preplay = Failed_to_Play then isar_proof_text ctxt isar_params else one_line_proof_text) one_line_params diff -r 99985426c0bb -r 59284a13abc4 src/HOL/Tools/Sledgehammer/sledgehammer_minimize.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_minimize.ML Mon May 30 15:30:05 2011 +0100 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_minimize.ML Mon May 30 17:00:38 2011 +0200 @@ -75,13 +75,19 @@ val problem = {state = state, goal = goal, subgoal = i, subgoal_count = n, facts = facts, smt_filter = NONE} - val result as {outcome, used_facts, ...} = prover params (K "") problem + val result as {outcome, used_facts, run_time_in_msecs, ...} = + prover params (K "") problem in 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 ^ "."); + | NONE => "Found proof" ^ + (if length used_facts = length facts then "" + else " with " ^ n_facts used_facts) ^ + (case run_time_in_msecs of + SOME ms => + " (" ^ string_from_time (Time.fromMilliseconds ms) ^ ")" + | NONE => "") ^ "."); result end diff -r 99985426c0bb -r 59284a13abc4 src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML Mon May 30 15:30:05 2011 +0100 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML Mon May 30 17:00:38 2011 +0200 @@ -73,6 +73,8 @@ val smt_slice_min_secs : int Config.T val das_tool : string val select_smt_solver : string -> Proof.context -> Proof.context + val is_metis_prover : string -> bool + val is_atp : theory -> string -> bool val is_smt_prover : Proof.context -> string -> bool val is_unit_equational_atp : Proof.context -> string -> bool val is_prover_supported : Proof.context -> string -> bool @@ -123,6 +125,11 @@ "Async_Manager". *) val das_tool = "Sledgehammer" +val metis_prover_names = [Metis_Tactics.metisN, Metis_Tactics.metisFT_N] + +val is_metis_prover = member (op =) metis_prover_names +val is_atp = member (op =) o supported_atps + val select_smt_solver = Context.proof_map o SMT_Config.select_solver @@ -138,22 +145,27 @@ fun is_prover_supported ctxt name = let val thy = Proof_Context.theory_of ctxt in - is_smt_prover ctxt name orelse member (op =) (supported_atps thy) name + is_metis_prover name orelse is_atp thy name orelse is_smt_prover ctxt name end fun is_prover_installed ctxt = - is_smt_prover ctxt orf is_atp_installed (Proof_Context.theory_of ctxt) + is_metis_prover orf is_smt_prover ctxt orf + is_atp_installed (Proof_Context.theory_of ctxt) fun get_slices slicing slices = (0 upto length slices - 1) ~~ slices |> not slicing ? (List.last #> single) +val metis_default_max_relevant = 20 + fun default_max_relevant_for_prover ctxt slicing name = let val thy = Proof_Context.theory_of ctxt in - if is_smt_prover ctxt name then - SMT_Solver.default_max_relevant ctxt name - else + if is_metis_prover name then + metis_default_max_relevant + else if is_atp thy name then fold (Integer.max o fst o snd o snd o snd) (get_slices slicing (#best_slices (get_atp thy name) ctxt)) 0 + else (* is_smt_prover ctxt name *) + SMT_Solver.default_max_relevant ctxt name end (* These are either simplified away by "Meson.presimplify" (most of the time) or @@ -250,6 +262,7 @@ let val thy = Proof_Context.theory_of ctxt val (remote_provers, local_provers) = + metis_prover_names @ sort_strings (supported_atps thy) @ sort_strings (SMT_Solver.available_solvers_of ctxt) |> List.partition (String.isPrefix remote_prefix) @@ -399,22 +412,21 @@ fun filter_used_facts used = filter (member (op =) used o fst) -fun preplay_one_line_proof debug timeout ths state i reconstructors = +fun play_one_line_proof debug timeout ths state i reconstructors = let - fun preplay [] [] = Failed_to_Preplay - | preplay (timed_out :: _) [] = Trust_Playable (timed_out, SOME timeout) - | preplay timed_out (reconstructor :: reconstructors) = + fun play [] [] = Failed_to_Play + | play (timed_out :: _) [] = Trust_Playable (timed_out, SOME timeout) + | play timed_out (reconstructor :: reconstructors) = let val timer = Timer.startRealTimer () in case timed_reconstructor reconstructor debug timeout ths state i of - SOME (SOME _) => - Preplayed (reconstructor, Timer.checkRealTimer timer) - | _ => preplay timed_out reconstructors + SOME (SOME _) => Played (reconstructor, Timer.checkRealTimer timer) + | _ => play timed_out reconstructors end handle TimeLimit.TimeOut => - preplay (reconstructor :: timed_out) reconstructors + play (reconstructor :: timed_out) reconstructors in if timeout = Time.zeroTime then Trust_Playable (hd reconstructors, NONE) - else preplay [] reconstructors + else play [] reconstructors end @@ -676,8 +688,7 @@ UnsoundProof (is_type_sys_virtually_sound type_sys, facts |> sort string_ord)) | SOME Unprovable => - if null blacklist then outcome - else SOME IncompleteUnprovable + if null blacklist then outcome else SOME GaveUp | _ => outcome in ((pool, conjecture_shape, facts_offset, fact_names, @@ -763,8 +774,8 @@ |> filter_used_facts used_facts |> map snd val preplay = - preplay_one_line_proof debug preplay_timeout used_ths state subgoal - reconstructors + play_one_line_proof debug preplay_timeout used_ths state subgoal + reconstructors val full_types = uses_typed_helpers typed_helpers atp_proof val isar_params = (debug, full_types, isar_shrink_factor, type_sys, pool, @@ -814,7 +825,7 @@ remote_smt_failures @ z3_wrapper_failures @ z3_failures @ unix_failures fun failure_from_smt_failure (SMT_Failure.Counterexample {is_real_cex, ...}) = - if is_real_cex then Unprovable else IncompleteUnprovable + if is_real_cex then Unprovable else GaveUp | 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 @@ -953,9 +964,9 @@ if name = SMT_Solver.solver_name_of ctxt then "" else "smt_solver = " ^ maybe_quote name val preplay = - case preplay_one_line_proof debug preplay_timeout used_ths state - subgoal [Metis, MetisFT] of - p as Preplayed _ => p + case play_one_line_proof debug preplay_timeout used_ths state + subgoal [Metis, MetisFT] of + p as Played _ => p | _ => Trust_Playable (SMT (smt_settings ()), NONE) val one_line_params = (preplay, proof_banner mode blocking name, used_facts, @@ -975,12 +986,41 @@ run_time_in_msecs = run_time_in_msecs, message = message} end +fun run_metis mode name ({debug, blocking, timeout, ...} : params) + minimize_command + ({state, subgoal, subgoal_count, facts, ...} : prover_problem) = + let + val reconstructor = if name = Metis_Tactics.metisN then Metis + else if name = Metis_Tactics.metisFT_N then MetisFT + else raise Fail ("unknown Metis version: " ^ quote name) + val (used_facts, used_ths) = + facts |> map untranslated_fact |> ListPair.unzip + in + case play_one_line_proof debug timeout used_ths state subgoal + [reconstructor] of + play as Played (_, time) => + let + val one_line_params = + (play, proof_banner mode blocking name, used_facts, + minimize_command, subgoal, subgoal_count) + in + {outcome = NONE, used_facts = used_facts, + run_time_in_msecs = SOME (Time.toMilliseconds time), + message = one_line_proof_text one_line_params} + end + | play => + {outcome = SOME (if play = Failed_to_Play then GaveUp else TimedOut), + used_facts = [], run_time_in_msecs = NONE, message = ""} + end + fun get_prover ctxt mode name = let val thy = Proof_Context.theory_of ctxt in - if is_smt_prover ctxt name then + if is_metis_prover name then + run_metis mode name + else if is_atp thy name then + run_atp mode name (get_atp thy name) + else if is_smt_prover ctxt name then run_smt_solver mode name - else if member (op =) (supported_atps thy) name then - run_atp mode name (get_atp thy name) else error ("No such prover: " ^ name ^ ".") end