1.1 --- a/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML Fri Mar 19 15:07:44 2010 +0100
1.2 +++ b/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML Fri Mar 19 15:33:18 2010 +0100
1.3 @@ -307,13 +307,13 @@
1.4 ctxt
1.5 |> change_dir dir
1.6 |> Config.put ATP_Wrapper.measure_runtime true
1.7 - val problem = ATP_Wrapper.problem_of_goal (! ATP_Manager.full_types) 1 (ctxt', (facts, goal));
1.8 + val problem = ATP_Manager.problem_of_goal (! ATP_Manager.full_types) 1 (ctxt', (facts, goal));
1.9
1.10 val time_limit =
1.11 (case hard_timeout of
1.12 NONE => I
1.13 | SOME secs => TimeLimit.timeLimit (Time.fromSeconds secs))
1.14 - val ({success, message, theorem_names, runtime=time_atp, ...}: ATP_Wrapper.prover_result,
1.15 + val ({success, message, theorem_names, runtime=time_atp, ...}: ATP_Manager.prover_result,
1.16 time_isa) = time_limit (Mirabelle.cpu_time (fn t => prover t problem)) timeout
1.17 in
1.18 if success then (message, SH_OK (time_isa, time_atp, theorem_names))
2.1 --- a/src/HOL/Sledgehammer.thy Fri Mar 19 15:07:44 2010 +0100
2.2 +++ b/src/HOL/Sledgehammer.thy Fri Mar 19 15:33:18 2010 +0100
2.3 @@ -101,29 +101,10 @@
2.4 use "Tools/Sledgehammer/sledgehammer_proof_reconstruct.ML"
2.5 setup Sledgehammer_Proof_Reconstruct.setup
2.6 use "Tools/Sledgehammer/sledgehammer_fact_filter.ML"
2.7 -
2.8 +use "Tools/ATP_Manager/atp_manager.ML"
2.9 use "Tools/ATP_Manager/atp_wrapper.ML"
2.10 setup ATP_Wrapper.setup
2.11 -use "Tools/ATP_Manager/atp_manager.ML"
2.12 use "Tools/ATP_Manager/atp_minimal.ML"
2.13 -
2.14 -text {* basic provers *}
2.15 -setup {* ATP_Manager.add_prover ATP_Wrapper.spass *}
2.16 -setup {* ATP_Manager.add_prover ATP_Wrapper.vampire *}
2.17 -setup {* ATP_Manager.add_prover ATP_Wrapper.eprover *}
2.18 -
2.19 -text {* provers with stuctured output *}
2.20 -setup {* ATP_Manager.add_prover ATP_Wrapper.vampire_full *}
2.21 -setup {* ATP_Manager.add_prover ATP_Wrapper.eprover_full *}
2.22 -
2.23 -text {* on some problems better results *}
2.24 -setup {* ATP_Manager.add_prover ATP_Wrapper.spass_no_tc *}
2.25 -
2.26 -text {* remote provers via SystemOnTPTP *}
2.27 -setup {* ATP_Manager.add_prover ATP_Wrapper.remote_vampire *}
2.28 -setup {* ATP_Manager.add_prover ATP_Wrapper.remote_spass *}
2.29 -setup {* ATP_Manager.add_prover ATP_Wrapper.remote_eprover *}
2.30 -
2.31 use "Tools/Sledgehammer/sledgehammer_isar.ML"
2.32
2.33
3.1 --- a/src/HOL/Tools/ATP_Manager/atp_manager.ML Fri Mar 19 15:07:44 2010 +0100
3.2 +++ b/src/HOL/Tools/ATP_Manager/atp_manager.ML Fri Mar 19 15:33:18 2010 +0100
3.3 @@ -7,6 +7,23 @@
3.4
3.5 signature ATP_MANAGER =
3.6 sig
3.7 + type problem =
3.8 + {with_full_types: bool,
3.9 + subgoal: int,
3.10 + goal: Proof.context * (thm list * thm),
3.11 + axiom_clauses: (thm * (string * int)) list option,
3.12 + filtered_clauses: (thm * (string * int)) list option}
3.13 + val problem_of_goal: bool -> int -> Proof.context * (thm list * thm) -> problem
3.14 + type prover_result =
3.15 + {success: bool,
3.16 + message: string,
3.17 + theorem_names: string list,
3.18 + runtime: int,
3.19 + proof: string,
3.20 + internal_thm_names: string Vector.vector,
3.21 + filtered_clauses: (thm * (string * int)) list}
3.22 + type prover = int -> problem -> prover_result
3.23 +
3.24 val atps: string Unsynchronized.ref
3.25 val get_atps: unit -> string list
3.26 val timeout: int Unsynchronized.ref
3.27 @@ -14,8 +31,8 @@
3.28 val kill: unit -> unit
3.29 val info: unit -> unit
3.30 val messages: int option -> unit
3.31 - val add_prover: string * ATP_Wrapper.prover -> theory -> theory
3.32 - val get_prover: theory -> string -> ATP_Wrapper.prover option
3.33 + val add_prover: string * prover -> theory -> theory
3.34 + val get_prover: theory -> string -> prover option
3.35 val print_provers: theory -> unit
3.36 val sledgehammer: string list -> Proof.state -> unit
3.37 end;
3.38 @@ -23,6 +40,34 @@
3.39 structure ATP_Manager : ATP_MANAGER =
3.40 struct
3.41
3.42 +(** problems, results, and provers **)
3.43 +
3.44 +type problem =
3.45 + {with_full_types: bool,
3.46 + subgoal: int,
3.47 + goal: Proof.context * (thm list * thm),
3.48 + axiom_clauses: (thm * (string * int)) list option,
3.49 + filtered_clauses: (thm * (string * int)) list option};
3.50 +
3.51 +fun problem_of_goal with_full_types subgoal goal : problem =
3.52 + {with_full_types = with_full_types,
3.53 + subgoal = subgoal,
3.54 + goal = goal,
3.55 + axiom_clauses = NONE,
3.56 + filtered_clauses = NONE};
3.57 +
3.58 +type prover_result =
3.59 + {success: bool,
3.60 + message: string,
3.61 + theorem_names: string list, (*relevant theorems*)
3.62 + runtime: int, (*user time of the ATP, in milliseconds*)
3.63 + proof: string,
3.64 + internal_thm_names: string Vector.vector,
3.65 + filtered_clauses: (thm * (string * int)) list};
3.66 +
3.67 +type prover = int -> problem -> prover_result;
3.68 +
3.69 +
3.70 (** preferences **)
3.71
3.72 val message_store_limit = 20;
3.73 @@ -228,7 +273,7 @@
3.74
3.75 structure Provers = Theory_Data
3.76 (
3.77 - type T = (ATP_Wrapper.prover * stamp) Symtab.table;
3.78 + type T = (prover * stamp) Symtab.table;
3.79 val empty = Symtab.empty;
3.80 val extend = I;
3.81 fun merge data : T = Symtab.merge (eq_snd op =) data
3.82 @@ -261,7 +306,7 @@
3.83 val _ = Toplevel.thread true (fn () =>
3.84 let
3.85 val _ = register birth_time death_time (Thread.self (), desc);
3.86 - val problem = ATP_Wrapper.problem_of_goal (! full_types) i (ctxt, (facts, goal));
3.87 + val problem = problem_of_goal (! full_types) i (ctxt, (facts, goal));
3.88 val message = #message (prover (! timeout) problem)
3.89 handle Sledgehammer_HOL_Clause.TRIVIAL => (* FIXME !? *)
3.90 "Empty clause: Try this command: " ^ Markup.markup Markup.sendback "apply metis"
4.1 --- a/src/HOL/Tools/ATP_Manager/atp_minimal.ML Fri Mar 19 15:07:44 2010 +0100
4.2 +++ b/src/HOL/Tools/ATP_Manager/atp_minimal.ML Fri Mar 19 15:33:18 2010 +0100
4.3 @@ -1,16 +1,19 @@
4.4 (* Title: HOL/Tools/ATP_Manager/atp_minimal.ML
4.5 Author: Philipp Meyer, TU Muenchen
4.6
4.7 -Minimization of theorem list for metis by using an external automated theorem prover
4.8 +Minimization of theorem list for Metis using automatic theorem provers.
4.9 *)
4.10
4.11 signature ATP_MINIMAL =
4.12 sig
4.13 + type prover = ATP_Manager.prover
4.14 + type prover_result = ATP_Manager.prover_result
4.15 type 'a minimize_fun = ('a list -> bool) -> 'a list -> 'a list
4.16 +
4.17 val linear_minimize : 'a minimize_fun
4.18 val binary_minimize : 'a minimize_fun
4.19 val minimize_theorems :
4.20 - (string * thm list) minimize_fun -> ATP_Wrapper.prover -> string -> int
4.21 + (string * thm list) minimize_fun -> prover -> string -> int
4.22 -> Proof.state -> (string * thm list) list
4.23 -> (string * thm list) list option * string
4.24 end;
4.25 @@ -19,6 +22,7 @@
4.26 struct
4.27
4.28 open Sledgehammer_Fact_Preprocessor
4.29 +open ATP_Manager
4.30
4.31 type 'a minimize_fun = ('a list -> bool) -> 'a list -> 'a list
4.32
4.33 @@ -87,30 +91,29 @@
4.34 ("# Cannot determine problem status within resource limit", Timeout),
4.35 ("Error", Error)]
4.36
4.37 -fun produce_answer (result : ATP_Wrapper.prover_result) =
4.38 - let
4.39 - val {success, proof = result_string, internal_thm_names = thm_name_vec,
4.40 - filtered_clauses = filtered, ...} = result
4.41 - in
4.42 - if success then
4.43 - (Success (Vector.foldr (op ::) [] thm_name_vec, filtered), result_string)
4.44 - else
4.45 - let
4.46 - val failure = failure_strings |> get_first (fn (s, t) =>
4.47 - if String.isSubstring s result_string then SOME (t, result_string) else NONE)
4.48 - in
4.49 - (case failure of
4.50 - SOME res => res
4.51 - | NONE => (Failure, result_string))
4.52 - end
4.53 - end
4.54 +fun produce_answer ({success, proof, internal_thm_names, filtered_clauses, ...}
4.55 + : prover_result) =
4.56 + if success then
4.57 + (Success (Vector.foldr (op ::) [] internal_thm_names, filtered_clauses),
4.58 + proof)
4.59 + else
4.60 + let
4.61 + val failure = failure_strings |> get_first (fn (s, t) =>
4.62 + if String.isSubstring s proof then SOME (t, proof) else NONE)
4.63 + in
4.64 + (case failure of
4.65 + SOME res => res
4.66 + | NONE => (Failure, proof))
4.67 + end
4.68
4.69
4.70 (* wrapper for calling external prover *)
4.71
4.72 -fun sh_test_thms prover time_limit subgoalno state filtered name_thms_pairs =
4.73 +fun sledgehammer_test_theorems prover time_limit subgoalno state filtered
4.74 + name_thms_pairs =
4.75 let
4.76 - val _ = priority ("Testing " ^ string_of_int (length name_thms_pairs) ^ " theorems... ")
4.77 + val _ = priority ("Testing " ^ string_of_int (length name_thms_pairs) ^
4.78 + " theorems... ")
4.79 val name_thm_pairs = maps (fn (n, ths) => map (pair n) ths) name_thms_pairs
4.80 val axclauses = cnf_rules_pairs (Proof.theory_of state) name_thm_pairs
4.81 val {context = ctxt, facts, goal} = Proof.goal state
4.82 @@ -122,9 +125,7 @@
4.83 filtered_clauses = filtered}
4.84 val (result, proof) = produce_answer (prover time_limit problem)
4.85 val _ = priority (string_of_result result)
4.86 - in
4.87 - (result, proof)
4.88 - end
4.89 + in (result, proof) end
4.90
4.91
4.92 (* minimalization of thms *)
4.93 @@ -136,7 +137,7 @@
4.94 priority ("Minimize called with " ^ string_of_int (length name_thms_pairs) ^
4.95 " theorems, prover: " ^ prover_name ^
4.96 ", time limit: " ^ string_of_int time_limit ^ " seconds")
4.97 - val test_thms_fun = sh_test_thms prover time_limit 1 state
4.98 + val test_thms_fun = sledgehammer_test_theorems prover time_limit 1 state
4.99 fun test_thms filtered thms =
4.100 case test_thms_fun filtered thms of (Success _, _) => true | _ => false
4.101 in
5.1 --- a/src/HOL/Tools/ATP_Manager/atp_wrapper.ML Fri Mar 19 15:07:44 2010 +0100
5.2 +++ b/src/HOL/Tools/ATP_Manager/atp_wrapper.ML Fri Mar 19 15:33:18 2010 +0100
5.3 @@ -6,48 +6,15 @@
5.4
5.5 signature ATP_WRAPPER =
5.6 sig
5.7 - (*hooks for problem files*)
5.8 - val destdir: string Config.T
5.9 - val problem_prefix: string Config.T
5.10 - val measure_runtime: bool Config.T
5.11 - val setup: theory -> theory
5.12 + type prover = ATP_Manager.prover
5.13
5.14 - (*prover configuration, problem format, and prover result*)
5.15 - type prover_config =
5.16 - {command: Path.T,
5.17 - arguments: int -> string,
5.18 - failure_strs: string list,
5.19 - max_new_clauses: int,
5.20 - insert_theory_const: bool,
5.21 - emit_structured_proof: bool}
5.22 - type problem =
5.23 - {with_full_types: bool,
5.24 - subgoal: int,
5.25 - goal: Proof.context * (thm list * thm),
5.26 - axiom_clauses: (thm * (string * int)) list option,
5.27 - filtered_clauses: (thm * (string * int)) list option}
5.28 - val problem_of_goal: bool -> int -> Proof.context * (thm list * thm) -> problem
5.29 - type prover_result =
5.30 - {success: bool,
5.31 - message: string,
5.32 - theorem_names: string list,
5.33 - runtime: int,
5.34 - proof: string,
5.35 - internal_thm_names: string Vector.vector,
5.36 - filtered_clauses: (thm * (string * int)) list}
5.37 - type prover = int -> problem -> prover_result
5.38 + (* hooks for problem files *)
5.39 + val destdir : string Config.T
5.40 + val problem_prefix : string Config.T
5.41 + val measure_runtime : bool Config.T
5.42
5.43 - (*common provers*)
5.44 - val vampire: string * prover
5.45 - val vampire_full: string * prover
5.46 - val eprover: string * prover
5.47 - val eprover_full: string * prover
5.48 - val spass: string * prover
5.49 - val spass_no_tc: string * prover
5.50 - val remote_vampire: string * prover
5.51 - val remote_eprover: string * prover
5.52 - val remote_spass: string * prover
5.53 - val refresh_systems: unit -> unit
5.54 + val refresh_systems_on_tptp : unit -> unit
5.55 + val setup : theory -> theory
5.56 end;
5.57
5.58 structure ATP_Wrapper : ATP_WRAPPER =
5.59 @@ -56,6 +23,7 @@
5.60 open Sledgehammer_HOL_Clause
5.61 open Sledgehammer_Fact_Filter
5.62 open Sledgehammer_Proof_Reconstruct
5.63 +open ATP_Manager
5.64
5.65 (** generic ATP wrapper **)
5.66
5.67 @@ -70,10 +38,8 @@
5.68 val (measure_runtime, measure_runtime_setup) =
5.69 Attrib.config_bool "atp_measure_runtime" false;
5.70
5.71 -val setup = destdir_setup #> problem_prefix_setup #> measure_runtime_setup;
5.72
5.73 -
5.74 -(* prover configuration, problem format, and prover result *)
5.75 +(* prover configuration *)
5.76
5.77 type prover_config =
5.78 {command: Path.T,
5.79 @@ -83,31 +49,6 @@
5.80 insert_theory_const: bool,
5.81 emit_structured_proof: bool};
5.82
5.83 -type problem =
5.84 - {with_full_types: bool,
5.85 - subgoal: int,
5.86 - goal: Proof.context * (thm list * thm),
5.87 - axiom_clauses: (thm * (string * int)) list option,
5.88 - filtered_clauses: (thm * (string * int)) list option};
5.89 -
5.90 -fun problem_of_goal with_full_types subgoal goal : problem =
5.91 - {with_full_types = with_full_types,
5.92 - subgoal = subgoal,
5.93 - goal = goal,
5.94 - axiom_clauses = NONE,
5.95 - filtered_clauses = NONE};
5.96 -
5.97 -type prover_result =
5.98 - {success: bool,
5.99 - message: string,
5.100 - theorem_names: string list, (*relevant theorems*)
5.101 - runtime: int, (*user time of the ATP, in milliseconds*)
5.102 - proof: string,
5.103 - internal_thm_names: string Vector.vector,
5.104 - filtered_clauses: (thm * (string * int)) list};
5.105 -
5.106 -type prover = int -> problem -> prover_result;
5.107 -
5.108
5.109 (* basic template *)
5.110
5.111 @@ -316,7 +257,8 @@
5.112 else split_lines answer
5.113 end;
5.114
5.115 -fun refresh_systems () = Synchronized.change systems (fn _ => get_systems ());
5.116 +fun refresh_systems_on_tptp () =
5.117 + Synchronized.change systems (fn _ => get_systems ());
5.118
5.119 fun get_system prefix = Synchronized.change_result systems (fn systems =>
5.120 (if null systems then get_systems () else systems)
5.121 @@ -347,4 +289,15 @@
5.122 val remote_spass = tptp_prover ("remote_spass", remote_prover_config
5.123 "SPASS---" "-x" spass_max_new_clauses spass_insert_theory_const);
5.124
5.125 +val provers =
5.126 + [spass, vampire, eprover, vampire_full, eprover_full, spass_no_tc,
5.127 + remote_vampire, remote_spass, remote_eprover]
5.128 +val prover_setup = fold add_prover provers
5.129 +
5.130 +val setup =
5.131 + destdir_setup
5.132 + #> problem_prefix_setup
5.133 + #> measure_runtime_setup
5.134 + #> prover_setup;
5.135 +
5.136 end;