# HG changeset patch # User blanchet # Date 1269009198 -3600 # Node ID 16279c4c7a3332e4e705df96ed627728debf0cf7 # Parent 513074557e0609a3172ea1439931a6aeef4d5f0e move all ATP setup code into ATP_Wrapper diff -r 513074557e06 -r 16279c4c7a33 src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML --- a/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML Fri Mar 19 15:07:44 2010 +0100 +++ b/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML Fri Mar 19 15:33:18 2010 +0100 @@ -307,13 +307,13 @@ ctxt |> change_dir dir |> Config.put ATP_Wrapper.measure_runtime true - val problem = ATP_Wrapper.problem_of_goal (! ATP_Manager.full_types) 1 (ctxt', (facts, goal)); + val problem = ATP_Manager.problem_of_goal (! ATP_Manager.full_types) 1 (ctxt', (facts, goal)); val time_limit = (case hard_timeout of NONE => I | SOME secs => TimeLimit.timeLimit (Time.fromSeconds secs)) - val ({success, message, theorem_names, runtime=time_atp, ...}: ATP_Wrapper.prover_result, + val ({success, message, theorem_names, runtime=time_atp, ...}: ATP_Manager.prover_result, time_isa) = time_limit (Mirabelle.cpu_time (fn t => prover t problem)) timeout in if success then (message, SH_OK (time_isa, time_atp, theorem_names)) diff -r 513074557e06 -r 16279c4c7a33 src/HOL/Sledgehammer.thy --- a/src/HOL/Sledgehammer.thy Fri Mar 19 15:07:44 2010 +0100 +++ b/src/HOL/Sledgehammer.thy Fri Mar 19 15:33:18 2010 +0100 @@ -101,29 +101,10 @@ use "Tools/Sledgehammer/sledgehammer_proof_reconstruct.ML" setup Sledgehammer_Proof_Reconstruct.setup use "Tools/Sledgehammer/sledgehammer_fact_filter.ML" - +use "Tools/ATP_Manager/atp_manager.ML" use "Tools/ATP_Manager/atp_wrapper.ML" setup ATP_Wrapper.setup -use "Tools/ATP_Manager/atp_manager.ML" use "Tools/ATP_Manager/atp_minimal.ML" - -text {* basic provers *} -setup {* ATP_Manager.add_prover ATP_Wrapper.spass *} -setup {* ATP_Manager.add_prover ATP_Wrapper.vampire *} -setup {* ATP_Manager.add_prover ATP_Wrapper.eprover *} - -text {* provers with stuctured output *} -setup {* ATP_Manager.add_prover ATP_Wrapper.vampire_full *} -setup {* ATP_Manager.add_prover ATP_Wrapper.eprover_full *} - -text {* on some problems better results *} -setup {* ATP_Manager.add_prover ATP_Wrapper.spass_no_tc *} - -text {* remote provers via SystemOnTPTP *} -setup {* ATP_Manager.add_prover ATP_Wrapper.remote_vampire *} -setup {* ATP_Manager.add_prover ATP_Wrapper.remote_spass *} -setup {* ATP_Manager.add_prover ATP_Wrapper.remote_eprover *} - use "Tools/Sledgehammer/sledgehammer_isar.ML" diff -r 513074557e06 -r 16279c4c7a33 src/HOL/Tools/ATP_Manager/atp_manager.ML --- a/src/HOL/Tools/ATP_Manager/atp_manager.ML Fri Mar 19 15:07:44 2010 +0100 +++ b/src/HOL/Tools/ATP_Manager/atp_manager.ML Fri Mar 19 15:33:18 2010 +0100 @@ -7,6 +7,23 @@ signature ATP_MANAGER = sig + type problem = + {with_full_types: bool, + subgoal: int, + goal: Proof.context * (thm list * thm), + axiom_clauses: (thm * (string * int)) list option, + filtered_clauses: (thm * (string * int)) list option} + val problem_of_goal: bool -> int -> Proof.context * (thm list * thm) -> problem + type prover_result = + {success: bool, + message: string, + theorem_names: string list, + runtime: int, + proof: string, + internal_thm_names: string Vector.vector, + filtered_clauses: (thm * (string * int)) list} + type prover = int -> problem -> prover_result + val atps: string Unsynchronized.ref val get_atps: unit -> string list val timeout: int Unsynchronized.ref @@ -14,8 +31,8 @@ val kill: unit -> unit val info: unit -> unit val messages: int option -> unit - val add_prover: string * ATP_Wrapper.prover -> theory -> theory - val get_prover: theory -> string -> ATP_Wrapper.prover option + val add_prover: string * prover -> theory -> theory + val get_prover: theory -> string -> prover option val print_provers: theory -> unit val sledgehammer: string list -> Proof.state -> unit end; @@ -23,6 +40,34 @@ structure ATP_Manager : ATP_MANAGER = struct +(** problems, results, and provers **) + +type problem = + {with_full_types: bool, + subgoal: int, + goal: Proof.context * (thm list * thm), + axiom_clauses: (thm * (string * int)) list option, + filtered_clauses: (thm * (string * int)) list option}; + +fun problem_of_goal with_full_types subgoal goal : problem = + {with_full_types = with_full_types, + subgoal = subgoal, + goal = goal, + axiom_clauses = NONE, + filtered_clauses = NONE}; + +type prover_result = + {success: bool, + message: string, + theorem_names: string list, (*relevant theorems*) + runtime: int, (*user time of the ATP, in milliseconds*) + proof: string, + internal_thm_names: string Vector.vector, + filtered_clauses: (thm * (string * int)) list}; + +type prover = int -> problem -> prover_result; + + (** preferences **) val message_store_limit = 20; @@ -228,7 +273,7 @@ structure Provers = Theory_Data ( - type T = (ATP_Wrapper.prover * stamp) Symtab.table; + type T = (prover * stamp) Symtab.table; val empty = Symtab.empty; val extend = I; fun merge data : T = Symtab.merge (eq_snd op =) data @@ -261,7 +306,7 @@ val _ = Toplevel.thread true (fn () => let val _ = register birth_time death_time (Thread.self (), desc); - val problem = ATP_Wrapper.problem_of_goal (! full_types) i (ctxt, (facts, goal)); + val problem = problem_of_goal (! full_types) i (ctxt, (facts, goal)); val message = #message (prover (! timeout) problem) handle Sledgehammer_HOL_Clause.TRIVIAL => (* FIXME !? *) "Empty clause: Try this command: " ^ Markup.markup Markup.sendback "apply metis" diff -r 513074557e06 -r 16279c4c7a33 src/HOL/Tools/ATP_Manager/atp_minimal.ML --- a/src/HOL/Tools/ATP_Manager/atp_minimal.ML Fri Mar 19 15:07:44 2010 +0100 +++ b/src/HOL/Tools/ATP_Manager/atp_minimal.ML Fri Mar 19 15:33:18 2010 +0100 @@ -1,16 +1,19 @@ (* Title: HOL/Tools/ATP_Manager/atp_minimal.ML Author: Philipp Meyer, TU Muenchen -Minimization of theorem list for metis by using an external automated theorem prover +Minimization of theorem list for Metis using automatic theorem provers. *) signature ATP_MINIMAL = sig + type prover = ATP_Manager.prover + type prover_result = ATP_Manager.prover_result type 'a minimize_fun = ('a list -> bool) -> 'a list -> 'a list + val linear_minimize : 'a minimize_fun val binary_minimize : 'a minimize_fun val minimize_theorems : - (string * thm list) minimize_fun -> ATP_Wrapper.prover -> string -> int + (string * thm list) minimize_fun -> prover -> string -> int -> Proof.state -> (string * thm list) list -> (string * thm list) list option * string end; @@ -19,6 +22,7 @@ struct open Sledgehammer_Fact_Preprocessor +open ATP_Manager type 'a minimize_fun = ('a list -> bool) -> 'a list -> 'a list @@ -87,30 +91,29 @@ ("# Cannot determine problem status within resource limit", Timeout), ("Error", Error)] -fun produce_answer (result : ATP_Wrapper.prover_result) = - let - val {success, proof = result_string, internal_thm_names = thm_name_vec, - filtered_clauses = filtered, ...} = result - in - if success then - (Success (Vector.foldr (op ::) [] thm_name_vec, filtered), result_string) - else - let - val failure = failure_strings |> get_first (fn (s, t) => - if String.isSubstring s result_string then SOME (t, result_string) else NONE) - in - (case failure of - SOME res => res - | NONE => (Failure, result_string)) - end - end +fun produce_answer ({success, proof, internal_thm_names, filtered_clauses, ...} + : prover_result) = + if success then + (Success (Vector.foldr (op ::) [] internal_thm_names, filtered_clauses), + proof) + else + let + val failure = failure_strings |> get_first (fn (s, t) => + if String.isSubstring s proof then SOME (t, proof) else NONE) + in + (case failure of + SOME res => res + | NONE => (Failure, proof)) + end (* wrapper for calling external prover *) -fun sh_test_thms prover time_limit subgoalno state filtered name_thms_pairs = +fun sledgehammer_test_theorems prover time_limit subgoalno state filtered + name_thms_pairs = let - val _ = priority ("Testing " ^ string_of_int (length name_thms_pairs) ^ " theorems... ") + val _ = priority ("Testing " ^ string_of_int (length name_thms_pairs) ^ + " theorems... ") val name_thm_pairs = maps (fn (n, ths) => map (pair n) ths) name_thms_pairs val axclauses = cnf_rules_pairs (Proof.theory_of state) name_thm_pairs val {context = ctxt, facts, goal} = Proof.goal state @@ -122,9 +125,7 @@ filtered_clauses = filtered} val (result, proof) = produce_answer (prover time_limit problem) val _ = priority (string_of_result result) - in - (result, proof) - end + in (result, proof) end (* minimalization of thms *) @@ -136,7 +137,7 @@ priority ("Minimize called with " ^ string_of_int (length name_thms_pairs) ^ " theorems, prover: " ^ prover_name ^ ", time limit: " ^ string_of_int time_limit ^ " seconds") - val test_thms_fun = sh_test_thms prover time_limit 1 state + val test_thms_fun = sledgehammer_test_theorems prover time_limit 1 state fun test_thms filtered thms = case test_thms_fun filtered thms of (Success _, _) => true | _ => false in diff -r 513074557e06 -r 16279c4c7a33 src/HOL/Tools/ATP_Manager/atp_wrapper.ML --- a/src/HOL/Tools/ATP_Manager/atp_wrapper.ML Fri Mar 19 15:07:44 2010 +0100 +++ b/src/HOL/Tools/ATP_Manager/atp_wrapper.ML Fri Mar 19 15:33:18 2010 +0100 @@ -6,48 +6,15 @@ signature ATP_WRAPPER = sig - (*hooks for problem files*) - val destdir: string Config.T - val problem_prefix: string Config.T - val measure_runtime: bool Config.T - val setup: theory -> theory + type prover = ATP_Manager.prover - (*prover configuration, problem format, and prover result*) - type prover_config = - {command: Path.T, - arguments: int -> string, - failure_strs: string list, - max_new_clauses: int, - insert_theory_const: bool, - emit_structured_proof: bool} - type problem = - {with_full_types: bool, - subgoal: int, - goal: Proof.context * (thm list * thm), - axiom_clauses: (thm * (string * int)) list option, - filtered_clauses: (thm * (string * int)) list option} - val problem_of_goal: bool -> int -> Proof.context * (thm list * thm) -> problem - type prover_result = - {success: bool, - message: string, - theorem_names: string list, - runtime: int, - proof: string, - internal_thm_names: string Vector.vector, - filtered_clauses: (thm * (string * int)) list} - type prover = int -> problem -> prover_result + (* hooks for problem files *) + val destdir : string Config.T + val problem_prefix : string Config.T + val measure_runtime : bool Config.T - (*common provers*) - val vampire: string * prover - val vampire_full: string * prover - val eprover: string * prover - val eprover_full: string * prover - val spass: string * prover - val spass_no_tc: string * prover - val remote_vampire: string * prover - val remote_eprover: string * prover - val remote_spass: string * prover - val refresh_systems: unit -> unit + val refresh_systems_on_tptp : unit -> unit + val setup : theory -> theory end; structure ATP_Wrapper : ATP_WRAPPER = @@ -56,6 +23,7 @@ open Sledgehammer_HOL_Clause open Sledgehammer_Fact_Filter open Sledgehammer_Proof_Reconstruct +open ATP_Manager (** generic ATP wrapper **) @@ -70,10 +38,8 @@ val (measure_runtime, measure_runtime_setup) = Attrib.config_bool "atp_measure_runtime" false; -val setup = destdir_setup #> problem_prefix_setup #> measure_runtime_setup; - -(* prover configuration, problem format, and prover result *) +(* prover configuration *) type prover_config = {command: Path.T, @@ -83,31 +49,6 @@ insert_theory_const: bool, emit_structured_proof: bool}; -type problem = - {with_full_types: bool, - subgoal: int, - goal: Proof.context * (thm list * thm), - axiom_clauses: (thm * (string * int)) list option, - filtered_clauses: (thm * (string * int)) list option}; - -fun problem_of_goal with_full_types subgoal goal : problem = - {with_full_types = with_full_types, - subgoal = subgoal, - goal = goal, - axiom_clauses = NONE, - filtered_clauses = NONE}; - -type prover_result = - {success: bool, - message: string, - theorem_names: string list, (*relevant theorems*) - runtime: int, (*user time of the ATP, in milliseconds*) - proof: string, - internal_thm_names: string Vector.vector, - filtered_clauses: (thm * (string * int)) list}; - -type prover = int -> problem -> prover_result; - (* basic template *) @@ -316,7 +257,8 @@ else split_lines answer end; -fun refresh_systems () = Synchronized.change systems (fn _ => get_systems ()); +fun refresh_systems_on_tptp () = + Synchronized.change systems (fn _ => get_systems ()); fun get_system prefix = Synchronized.change_result systems (fn systems => (if null systems then get_systems () else systems) @@ -347,4 +289,15 @@ val remote_spass = tptp_prover ("remote_spass", remote_prover_config "SPASS---" "-x" spass_max_new_clauses spass_insert_theory_const); +val provers = + [spass, vampire, eprover, vampire_full, eprover_full, spass_no_tc, + remote_vampire, remote_spass, remote_eprover] +val prover_setup = fold add_prover provers + +val setup = + destdir_setup + #> problem_prefix_setup + #> measure_runtime_setup + #> prover_setup; + end;