# HG changeset patch # User blanchet # Date 1269438572 -3600 # Node ID c9565298df9e037093333300ca24515ffccf7b9c # Parent b7f98ff9c7d97969fcfa1607500e48257c68261c added support for Sledgehammer parameters; this change goes hand in hand with f8c738abaed8 diff -r b7f98ff9c7d9 -r c9565298df9e src/HOL/Tools/ATP_Manager/atp_manager.ML --- 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; diff -r b7f98ff9c7d9 -r c9565298df9e src/HOL/Tools/ATP_Manager/atp_minimal.ML --- 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 diff -r b7f98ff9c7d9 -r c9565298df9e src/HOL/Tools/ATP_Manager/atp_wrapper.ML --- 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 =