added support for Sledgehammer parameters;
this change goes hand in hand with f8c738abaed8
--- a/src/HOL/Tools/ATP_Manager/atp_manager.ML Wed Mar 24 14:43:35 2010 +0100
+++ b/src/HOL/Tools/ATP_Manager/atp_manager.ML Wed Mar 24 14:49:32 2010 +0100
@@ -1,71 +1,92 @@
(* Title: HOL/Tools/ATP_Manager/atp_manager.ML
Author: Fabian Immler, TU Muenchen
Author: Makarius
+ Author: Jasmin Blanchette, TU Muenchen
Central manager component for ATP threads.
*)
signature ATP_MANAGER =
sig
+ type relevance_override = Sledgehammer_Fact_Filter.relevance_override
+ type params =
+ {debug: bool,
+ verbose: bool,
+ atps: string list,
+ full_types: bool,
+ relevance_threshold: real,
+ higher_order: bool option,
+ respect_no_atp: bool,
+ follow_defs: bool,
+ isar_proof: bool,
+ timeout: Time.time,
+ minimize_timeout: Time.time}
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
+ {subgoal: int,
+ goal: Proof.context * (thm list * thm),
+ relevance_override: relevance_override,
+ axiom_clauses: (thm * (string * int)) list option,
+ filtered_clauses: (thm * (string * int)) list option}
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
+ {success: bool,
+ message: string,
+ relevant_thm_names: string list,
+ atp_run_time_in_msecs: int,
+ proof: string,
+ internal_thm_names: string Vector.vector,
+ filtered_clauses: (thm * (string * int)) list}
+ type prover = params -> Time.time -> problem -> prover_result
val atps: string Unsynchronized.ref
- val get_atps: unit -> string list
val timeout: int Unsynchronized.ref
val full_types: bool Unsynchronized.ref
- val kill: unit -> unit
- val info: unit -> unit
+ val kill_atps: unit -> unit
+ val running_atps: unit -> unit
val messages: int option -> unit
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
+ val available_atps: theory -> unit
+ val sledgehammer: params -> int -> relevance_override -> Proof.state -> unit
end;
structure ATP_Manager : ATP_MANAGER =
struct
-(** problems, results, and provers **)
+type relevance_override = Sledgehammer_Fact_Filter.relevance_override
+
+(** parameters, problems, results, and provers **)
+
+(* TODO: "theory_const", "blacklist_filter", "convergence" *)
+type params =
+ {debug: bool,
+ verbose: bool,
+ atps: string list,
+ full_types: bool,
+ relevance_threshold: real,
+ higher_order: bool option,
+ respect_no_atp: bool,
+ follow_defs: bool,
+ isar_proof: bool,
+ timeout: Time.time,
+ minimize_timeout: Time.time}
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};
+ {subgoal: int,
+ goal: Proof.context * (thm list * thm),
+ relevance_override: relevance_override,
+ axiom_clauses: (thm * (string * int)) list option,
+ filtered_clauses: (thm * (string * int)) list option};
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};
+ {success: bool,
+ message: string,
+ relevant_thm_names: string list,
+ atp_run_time_in_msecs: int,
+ proof: string,
+ internal_thm_names: string Vector.vector,
+ filtered_clauses: (thm * (string * int)) list};
-type prover = int -> problem -> prover_result;
+type prover = params -> Time.time -> problem -> prover_result;
(** preferences **)
@@ -74,8 +95,6 @@
val message_display_limit = 5;
val atps = Unsynchronized.ref "e spass remote_vampire";
-fun get_atps () = String.tokens (Symbol.is_ascii_blank o String.str) (! atps);
-
val timeout = Unsynchronized.ref 60;
val full_types = Unsynchronized.ref false;
@@ -218,9 +237,9 @@
(** user commands **)
-(* kill *)
+(* kill ATPs *)
-fun kill () = Synchronized.change global_state
+fun kill_atps () = Synchronized.change global_state
(fn {manager, timeout_heap, active, cancelling, messages, store} =>
let
val killing = map (fn (th, (_, _, desc)) => (th, (Time.now (), desc))) active;
@@ -228,11 +247,11 @@
in state' end);
-(* info *)
+(* running_atps *)
fun seconds time = string_of_int (Time.toSeconds time) ^ "s";
-fun info () =
+fun running_atps () =
let
val {active, cancelling, ...} = Synchronized.value global_state;
@@ -287,44 +306,51 @@
fun get_prover thy name =
Option.map #1 (Symtab.lookup (Provers.get thy) name);
-fun print_provers thy = Pretty.writeln
- (Pretty.strs ("external provers:" :: sort_strings (Symtab.keys (Provers.get thy))));
+fun available_atps thy = Pretty.writeln
+ (Pretty.strs ("ATPs:" :: sort_strings (Symtab.keys (Provers.get thy))));
(* start prover thread *)
-fun start_prover name birth_time death_time i proof_state =
+fun start_prover (params as {timeout, ...}) birth_time death_time i
+ relevance_override proof_state name =
(case get_prover (Proof.theory_of proof_state) name of
- NONE => warning ("Unknown external prover: " ^ quote name)
+ NONE => warning ("Unknown ATP: " ^ quote name)
| SOME prover =>
let
val {context = ctxt, facts, goal} = Proof.goal proof_state;
val desc =
- "external prover " ^ quote name ^ " for subgoal " ^ string_of_int i ^ ":\n" ^
+ "ATP " ^ quote name ^ " for subgoal " ^ string_of_int i ^ ":\n" ^
Syntax.string_of_term ctxt (Thm.term_of (Thm.cprem_of goal i));
val _ = Toplevel.thread true (fn () =>
let
val _ = register birth_time death_time (Thread.self (), desc);
- val problem = problem_of_goal (! full_types) i (ctxt, (facts, goal));
- val message = #message (prover (! timeout) problem)
+ val problem =
+ {subgoal = i, goal = (ctxt, (facts, goal)),
+ relevance_override = relevance_override, axiom_clauses = NONE,
+ filtered_clauses = NONE}
+ val message = #message (prover params timeout problem)
handle Sledgehammer_HOL_Clause.TRIVIAL => (* FIXME !? *)
- "Empty clause: Try this command: " ^ Markup.markup Markup.sendback "apply metis"
+ "Try this command: " ^
+ Markup.markup Markup.sendback "by metis" ^ "."
| ERROR msg => ("Error: " ^ msg);
val _ = unregister message (Thread.self ());
in () end);
in () end);
-(* sledghammer for first subgoal *)
+(* Sledgehammer the given subgoal *)
-fun sledgehammer names proof_state =
+fun sledgehammer (params as {atps, timeout, ...}) i relevance_override
+ proof_state =
let
- val provers = if null names then get_atps () else names;
- val birth_time = Time.now ();
- val death_time = Time.+ (birth_time, Time.fromSeconds (! timeout));
- val _ = kill (); (*RACE wrt. other invocations of sledgehammer*)
- val _ = List.app (fn name => start_prover name birth_time death_time 1 proof_state) provers;
- in () end;
+ val birth_time = Time.now ()
+ val death_time = Time.+ (birth_time, timeout)
+ val _ = kill_atps () (* RACE w.r.t. other invocations of Sledgehammer *)
+ val _ = priority "Sledgehammering..."
+ val _ = List.app (start_prover params birth_time death_time i
+ relevance_override proof_state) atps
+ in () end
end;
--- a/src/HOL/Tools/ATP_Manager/atp_minimal.ML Wed Mar 24 14:43:35 2010 +0100
+++ b/src/HOL/Tools/ATP_Manager/atp_minimal.ML Wed Mar 24 14:49:32 2010 +0100
@@ -6,6 +6,7 @@
signature ATP_MINIMAL =
sig
+ type params = ATP_Manager.params
type prover = ATP_Manager.prover
type prover_result = ATP_Manager.prover_result
type 'a minimize_fun = ('a list -> bool) -> 'a list -> 'a list
@@ -13,7 +14,7 @@
val linear_minimize : 'a minimize_fun
val binary_minimize : 'a minimize_fun
val minimize_theorems :
- (string * thm list) minimize_fun -> prover -> string -> int
+ params -> (string * thm list) minimize_fun -> prover -> string
-> Proof.state -> (string * thm list) list
-> (string * thm list) list option * string
end;
@@ -109,8 +110,8 @@
(* wrapper for calling external prover *)
-fun sledgehammer_test_theorems prover time_limit subgoalno state filtered
- name_thms_pairs =
+fun sledgehammer_test_theorems (params as {full_types, ...} : params) prover
+ timeout subgoalno state filtered name_thms_pairs =
let
val _ = priority ("Testing " ^ string_of_int (length name_thms_pairs) ^
" theorems... ")
@@ -118,26 +119,26 @@
val axclauses = cnf_rules_pairs (Proof.theory_of state) name_thm_pairs
val {context = ctxt, facts, goal} = Proof.goal state
val problem =
- {with_full_types = ! ATP_Manager.full_types,
- subgoal = subgoalno,
- goal = (ctxt, (facts, goal)),
- axiom_clauses = SOME axclauses,
- filtered_clauses = filtered}
- val (result, proof) = produce_answer (prover time_limit problem)
+ {subgoal = subgoalno, goal = (ctxt, (facts, goal)),
+ relevance_override = {add = [], del = [], only = false},
+ axiom_clauses = SOME axclauses, filtered_clauses = filtered}
+ val (result, proof) = produce_answer (prover params timeout problem)
val _ = priority (string_of_result result)
in (result, proof) end
(* minimalization of thms *)
-fun minimize_theorems gen_min prover prover_name time_limit state
- name_thms_pairs =
+fun minimize_theorems (params as {minimize_timeout, ...}) gen_min prover
+ prover_name state name_thms_pairs =
let
+ val msecs = Time.toMilliseconds minimize_timeout
val _ =
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 = sledgehammer_test_theorems prover time_limit 1 state
+ " theorems, ATP: " ^ prover_name ^
+ ", time limit: " ^ string_of_int msecs ^ " ms")
+ val test_thms_fun =
+ sledgehammer_test_theorems params prover minimize_timeout 1 state
fun test_thms filtered thms =
case test_thms_fun filtered thms of (Success _, _) => true | _ => false
in
@@ -157,18 +158,22 @@
val _ = priority (cat_lines
["Minimal " ^ string_of_int (length min_thms) ^ " theorems"])
in
- (SOME min_thms, "Try this command: " ^
- Markup.markup Markup.sendback ("apply (metis " ^ space_implode " " min_names ^ ")"))
+ (SOME min_thms,
+ "Try this command: " ^
+ Markup.markup Markup.sendback
+ ("by (metis " ^ space_implode " " min_names ^ ")")
+ ^ ".")
end
| (Timeout, _) =>
(NONE, "Timeout: You may need to increase the time limit of " ^
- string_of_int time_limit ^ " seconds. Call atp_minimize [time=...] ")
+ string_of_int msecs ^ " ms. Invoke \"atp_minimize [time=...]\".")
| (Error, msg) =>
(NONE, "Error in prover: " ^ msg)
| (Failure, _) =>
(NONE, "Failure: No proof with the theorems supplied"))
handle Sledgehammer_HOL_Clause.TRIVIAL =>
- (SOME [], "Trivial: Try this command: " ^ Markup.markup Markup.sendback "apply metis")
+ (SOME [], "Trivial: Try this command: " ^
+ Markup.markup Markup.sendback "by metis" ^ ".")
| ERROR msg => (NONE, "Error: " ^ msg)
end
--- a/src/HOL/Tools/ATP_Manager/atp_wrapper.ML Wed Mar 24 14:43:35 2010 +0100
+++ b/src/HOL/Tools/ATP_Manager/atp_wrapper.ML Wed Mar 24 14:49:32 2010 +0100
@@ -20,6 +20,7 @@
structure ATP_Wrapper : ATP_WRAPPER =
struct
+open Sledgehammer_Fact_Preprocessor
open Sledgehammer_HOL_Clause
open Sledgehammer_Fact_Filter
open Sledgehammer_Proof_Reconstruct
@@ -43,11 +44,11 @@
type prover_config =
{command: Path.T,
- arguments: int -> string,
+ arguments: Time.time -> string,
failure_strs: string list,
max_new_clauses: int,
- insert_theory_const: bool,
- emit_structured_proof: bool};
+ add_theory_const: bool,
+ supports_isar_proofs: bool};
(* basic template *)
@@ -64,24 +65,25 @@
else SOME "Ill-formed ATP output"
| (failure :: _) => SOME failure
-fun external_prover relevance_filter prepare write cmd args failure_strs
- produce_answer name ({with_full_types, subgoal, goal, axiom_clauses,
- filtered_clauses}: problem) =
+fun generic_prover get_facts prepare write cmd args failure_strs produce_answer
+ name ({full_types, ...} : params)
+ ({subgoal, goal, relevance_override, axiom_clauses, filtered_clauses}
+ : problem) =
let
(* get clauses and prepare them for writing *)
val (ctxt, (chain_ths, th)) = goal;
val thy = ProofContext.theory_of ctxt;
val chain_ths = map (Thm.put_name_hint chained_hint) chain_ths;
- val goal_cls = #1 (Sledgehammer_Fact_Preprocessor.neg_conjecture_clauses ctxt th subgoal);
+ val goal_cls = #1 (neg_conjecture_clauses ctxt th subgoal);
val the_filtered_clauses =
(case filtered_clauses of
- NONE => relevance_filter goal goal_cls
+ NONE => get_facts relevance_override goal goal_cls
| SOME fcls => fcls);
val the_axiom_clauses =
(case axiom_clauses of
NONE => the_filtered_clauses
| SOME axcls => axcls);
- val (thm_names, clauses) =
+ val (internal_thm_names, clauses) =
prepare goal_cls chain_ths the_axiom_clauses the_filtered_clauses thy;
(* path to unique problem file *)
@@ -121,7 +123,7 @@
if Config.get ctxt measure_runtime then split_time s else (s, 0)
fun run_on probfile =
if File.exists cmd then
- write with_full_types probfile clauses
+ write full_types probfile clauses
|> pair (apfst split_time' (bash_output (cmd_line probfile)))
else error ("Bad executable: " ^ Path.implode cmd);
@@ -131,21 +133,24 @@
if destdir' = "" then ()
else File.write (Path.explode (Path.implode probfile ^ "_proof")) proof;
- val (((proof, time), rc), conj_pos) =
+ val (((proof, atp_run_time_in_msecs), rc), conj_pos) =
with_path cleanup export run_on (prob_pathname subgoal);
(* check for success and print out some information on failure *)
val failure = find_failure failure_strs proof;
val success = rc = 0 andalso is_none failure;
- val (message, real_thm_names) =
+ val (message, relevant_thm_names) =
if is_some failure then ("External prover failed.", [])
else if rc <> 0 then ("External prover failed: " ^ proof, [])
- else apfst (fn s => "Try this command: " ^ s)
- (produce_answer name (proof, thm_names, conj_pos, ctxt, th, subgoal));
+ else
+ (produce_answer name (proof, internal_thm_names, conj_pos, ctxt, th,
+ subgoal));
in
{success = success, message = message,
- theorem_names = real_thm_names, runtime = time, proof = proof,
- internal_thm_names = thm_names, filtered_clauses = the_filtered_clauses}
+ relevant_thm_names = relevant_thm_names,
+ atp_run_time_in_msecs = atp_run_time_in_msecs, proof = proof,
+ internal_thm_names = internal_thm_names,
+ filtered_clauses = the_filtered_clauses}
end;
@@ -153,96 +158,87 @@
fun generic_tptp_prover
(name, {command, arguments, failure_strs, max_new_clauses,
- insert_theory_const, emit_structured_proof}) timeout =
- external_prover (get_relevant_facts max_new_clauses insert_theory_const)
- (prepare_clauses false) write_tptp_file command (arguments timeout)
- failure_strs
- (if emit_structured_proof then structured_isar_proof
- else metis_lemma_list false) name;
+ add_theory_const, supports_isar_proofs})
+ (params as {relevance_threshold, higher_order, follow_defs, isar_proof,
+ ...}) timeout =
+ generic_prover
+ (get_relevant_facts relevance_threshold higher_order follow_defs
+ max_new_clauses add_theory_const)
+ (prepare_clauses higher_order false) write_tptp_file command
+ (arguments timeout) failure_strs
+ (if supports_isar_proofs andalso isar_proof then structured_isar_proof
+ else metis_lemma_list false) name params;
-fun tptp_prover (name, p) = (name, generic_tptp_prover (name, p));
+fun tptp_prover name p = (name, generic_tptp_prover (name, p));
(** common provers **)
(* Vampire *)
-(*NB: Vampire does not work without explicit timelimit*)
-
-val vampire_failure_strs =
- ["Satisfiability detected", "Refutation not found", "CANNOT PROVE"];
-val vampire_max_new_clauses = 60;
-val vampire_insert_theory_const = false;
+(* NB: Vampire does not work without explicit time limit. *)
-fun vampire_prover_config isar : prover_config =
- {command = Path.explode "$VAMPIRE_HOME/vampire",
- arguments = (fn timeout => "--output_syntax tptp --mode casc" ^
- " -t " ^ string_of_int timeout),
- failure_strs = vampire_failure_strs,
- max_new_clauses = vampire_max_new_clauses,
- insert_theory_const = vampire_insert_theory_const,
- emit_structured_proof = isar};
-
-val vampire = tptp_prover ("vampire", vampire_prover_config false);
-val vampire_isar = tptp_prover ("vampire_isar", vampire_prover_config true);
+val vampire_config : prover_config =
+ {command = Path.explode "$VAMPIRE_HOME/vampire",
+ arguments = (fn timeout => "--output_syntax tptp --mode casc -t " ^
+ string_of_int (Time.toSeconds timeout)),
+ failure_strs =
+ ["Satisfiability detected", "Refutation not found", "CANNOT PROVE"],
+ max_new_clauses = 60,
+ add_theory_const = false,
+ supports_isar_proofs = true}
+val vampire = tptp_prover "vampire" vampire_config
(* E prover *)
-val eprover_failure_strs =
- ["SZS status: Satisfiable", "SZS status Satisfiable",
- "SZS status: ResourceOut", "SZS status ResourceOut",
- "# Cannot determine problem status"];
-val eprover_max_new_clauses = 100;
-val eprover_insert_theory_const = false;
-
-fun eprover_config isar : prover_config =
- {command = Path.explode "$E_HOME/eproof",
- arguments = (fn timeout => "--tstp-in --tstp-out -l5 -xAutoDev -tAutoDev" ^
- " --silent --cpu-limit=" ^ string_of_int timeout),
- failure_strs = eprover_failure_strs,
- max_new_clauses = eprover_max_new_clauses,
- insert_theory_const = eprover_insert_theory_const,
- emit_structured_proof = isar};
-
-val eprover = tptp_prover ("e", eprover_config false);
-val eprover_isar = tptp_prover ("e_isar", eprover_config true);
+val e_config : prover_config =
+ {command = Path.explode "$E_HOME/eproof",
+ arguments = (fn timeout => "--tstp-in --tstp-out -l5 -xAutoDev \
+ \-tAutoDev --silent --cpu-limit=" ^
+ string_of_int (Time.toSeconds timeout)),
+ failure_strs =
+ ["SZS status: Satisfiable", "SZS status Satisfiable",
+ "SZS status: ResourceOut", "SZS status ResourceOut",
+ "# Cannot determine problem status"],
+ max_new_clauses = 100,
+ add_theory_const = false,
+ supports_isar_proofs = true}
+val e = tptp_prover "e" e_config
(* SPASS *)
-val spass_failure_strs =
- ["SPASS beiseite: Completion found.", "SPASS beiseite: Ran out of time.",
- "SPASS beiseite: Maximal number of loops exceeded."];
-val spass_max_new_clauses = 40;
-val spass_insert_theory_const = true;
-
-fun spass_config insert_theory_const: prover_config =
- {command = Path.explode "$SPASS_HOME/SPASS",
- arguments = (fn timeout => "-Auto -SOS=1 -PGiven=0 -PProblem=0 -Splits=0" ^
- " -FullRed=0 -DocProof -TimeLimit=" ^ string_of_int timeout),
- failure_strs = spass_failure_strs,
- max_new_clauses = spass_max_new_clauses,
- insert_theory_const = insert_theory_const,
- emit_structured_proof = false};
-
fun generic_dfg_prover
(name, ({command, arguments, failure_strs, max_new_clauses,
- insert_theory_const, ...} : prover_config)) timeout =
- external_prover
- (get_relevant_facts max_new_clauses insert_theory_const)
- (prepare_clauses true)
- write_dfg_file
- command
- (arguments timeout)
- failure_strs
- (metis_lemma_list true)
- name;
+ add_theory_const, ...} : prover_config))
+ (params as {relevance_threshold, higher_order, follow_defs, ...})
+ timeout =
+ generic_prover
+ (get_relevant_facts relevance_threshold higher_order follow_defs
+ max_new_clauses add_theory_const)
+ (prepare_clauses higher_order true) write_dfg_file command
+ (arguments timeout) failure_strs (metis_lemma_list true) name params;
fun dfg_prover (name, p) = (name, generic_dfg_prover (name, p));
-val spass = dfg_prover ("spass", spass_config spass_insert_theory_const);
-val spass_no_tc = dfg_prover ("spass_no_tc", spass_config false);
+fun spass_config_for add_theory_const : prover_config =
+ {command = Path.explode "$SPASS_HOME/SPASS",
+ arguments = (fn timeout => "-Auto -SOS=1 -PGiven=0 -PProblem=0 -Splits=0" ^
+ " -FullRed=0 -DocProof -TimeLimit=" ^
+ string_of_int (Time.toSeconds timeout)),
+ failure_strs =
+ ["SPASS beiseite: Completion found.", "SPASS beiseite: Ran out of time.",
+ "SPASS beiseite: Maximal number of loops exceeded."],
+ max_new_clauses = 40,
+ add_theory_const = add_theory_const,
+ supports_isar_proofs = false};
+
+val spass_config = spass_config_for true
+val spass = dfg_prover ("spass", spass_config)
+
+val spass_no_tc_config = spass_config_for false
+val spass_no_tc = dfg_prover ("spass_no_tc", spass_no_tc_config)
(* remote prover invocation via SystemOnTPTP *)
@@ -251,10 +247,12 @@
fun get_systems () =
let
- val (answer, rc) = bash_output ("\"$ISABELLE_ATP_MANAGER/SystemOnTPTP\" -w")
+ val (answer, rc) = bash_output "\"$ISABELLE_ATP_MANAGER/SystemOnTPTP\" -w"
in
- if rc <> 0 then error ("Failed to get available systems at SystemOnTPTP:\n" ^ answer)
- else split_lines answer
+ if rc <> 0 then
+ error ("Failed to get available systems at SystemOnTPTP:\n" ^ answer)
+ else
+ split_lines answer
end;
fun refresh_systems_on_tptp () =
@@ -271,27 +269,34 @@
val remote_failure_strs = ["Remote-script could not extract proof"];
-fun remote_prover_config prover_prefix args max_new insert_tc: prover_config =
- {command = Path.explode "$ISABELLE_ATP_MANAGER/SystemOnTPTP",
- arguments = (fn timeout =>
- args ^ " -t " ^ string_of_int timeout ^ " -s " ^ the_system prover_prefix),
- failure_strs = remote_failure_strs,
- max_new_clauses = max_new,
- insert_theory_const = insert_tc,
- emit_structured_proof = false};
+fun remote_prover_config prover_prefix args max_new_clauses add_theory_const
+ : prover_config =
+ {command = Path.explode "$ISABELLE_ATP_MANAGER/SystemOnTPTP",
+ arguments = (fn timeout =>
+ args ^ " -t " ^ string_of_int (Time.toSeconds timeout) ^ " -s " ^
+ the_system prover_prefix),
+ failure_strs = remote_failure_strs,
+ max_new_clauses = max_new_clauses,
+ add_theory_const = add_theory_const,
+ supports_isar_proofs = false}
-val remote_vampire = tptp_prover ("remote_vampire", remote_prover_config
- "Vampire---9" "" vampire_max_new_clauses vampire_insert_theory_const);
+val remote_vampire =
+ tptp_prover "remote_vampire"
+ (remote_prover_config "Vampire---9" ""
+ (#max_new_clauses vampire_config) (#add_theory_const vampire_config))
-val remote_eprover = tptp_prover ("remote_e", remote_prover_config
- "EP---" "" eprover_max_new_clauses eprover_insert_theory_const);
+val remote_e =
+ tptp_prover "remote_e"
+ (remote_prover_config "EP---" ""
+ (#max_new_clauses e_config) (#add_theory_const e_config))
-val remote_spass = tptp_prover ("remote_spass", remote_prover_config
- "SPASS---" "-x" spass_max_new_clauses spass_insert_theory_const);
+val remote_spass =
+ tptp_prover "remote_spass"
+ (remote_prover_config "SPASS---" "-x"
+ (#max_new_clauses spass_config) (#add_theory_const spass_config))
val provers =
- [spass, vampire, eprover, vampire_isar, eprover_isar, spass_no_tc,
- remote_vampire, remote_spass, remote_eprover]
+ [spass, vampire, e, spass_no_tc, remote_vampire, remote_spass, remote_e]
val prover_setup = fold add_prover provers
val setup =