--- 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))
--- 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"
--- 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"
--- 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
--- 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;