# HG changeset patch # User blanchet # Date 1272044209 -7200 # Node ID b90fc0d75bca8c35385952e3bfa733dd2b20a431 # Parent f4d84d84a01a92b7175fe20f2ba494fb51ba5049 cosmetics diff -r f4d84d84a01a -r b90fc0d75bca src/HOL/Tools/ATP_Manager/atp_systems.ML --- a/src/HOL/Tools/ATP_Manager/atp_systems.ML Fri Apr 23 19:26:39 2010 +0200 +++ b/src/HOL/Tools/ATP_Manager/atp_systems.ML Fri Apr 23 19:36:49 2010 +0200 @@ -51,7 +51,7 @@ arguments: Time.time -> string, proof_delims: (string * string) list, known_failures: (failure * string) list, - max_new_clauses: int, + max_axiom_clauses: int, prefers_theory_relevant: bool}; @@ -175,7 +175,8 @@ if File.exists command then write_file full_types explicit_apply probfile clauses |> pair (apfst split_time' (bash_output (command_line probfile))) - else error ("Bad executable: " ^ Path.implode command ^ "."); + else + error ("Bad executable: " ^ Path.implode command ^ "."); (* If the problem file has not been exported, remove it; otherwise, export the proof file too. *) @@ -217,14 +218,14 @@ fun generic_tptp_prover (name, {home, executable, arguments, proof_delims, known_failures, - max_new_clauses, prefers_theory_relevant}) + max_axiom_clauses, prefers_theory_relevant}) (params as {debug, overlord, respect_no_atp, relevance_threshold, convergence, theory_relevant, higher_order, follow_defs, isar_proof, ...}) minimize_command timeout = generic_prover overlord (get_relevant_facts respect_no_atp relevance_threshold convergence - higher_order follow_defs max_new_clauses + higher_order follow_defs max_axiom_clauses (the_default prefers_theory_relevant theory_relevant)) (prepare_clauses higher_order false) (write_tptp_file (debug andalso overlord andalso not isar_proof)) home @@ -236,7 +237,7 @@ (** common provers **) -fun generous_to_secs time = (Time.toMilliseconds time + 999) div 1000 +fun to_generous_secs time = (Time.toMilliseconds time + 999) div 1000 (* Vampire *) @@ -245,15 +246,16 @@ val vampire_config : prover_config = {home = getenv "VAMPIRE_HOME", executable = "vampire", - arguments = (fn timeout => "--output_syntax tptp --mode casc -t " ^ - string_of_int (generous_to_secs timeout)), + arguments = fn timeout => + "--output_syntax tptp --mode casc -t " ^ + string_of_int (to_generous_secs timeout), proof_delims = [("=========== Refutation ==========", "======= End of refutation =======")], known_failures = [(Unprovable, "Satisfiability detected"), (OutOfResources, "CANNOT PROVE"), (OutOfResources, "Refutation not found")], - max_new_clauses = 60, + max_axiom_clauses = 60, prefers_theory_relevant = false} val vampire = tptp_prover "vampire" vampire_config @@ -266,9 +268,9 @@ val e_config : prover_config = {home = getenv "E_HOME", executable = "eproof", - arguments = (fn timeout => "--tstp-in --tstp-out -l5 -xAutoDev \ - \-tAutoDev --silent --cpu-limit=" ^ - string_of_int (generous_to_secs timeout)), + arguments = fn timeout => + "--tstp-in --tstp-out -l5 -xAutoDev -tAutoDev --silent --cpu-limit=" ^ + string_of_int (to_generous_secs timeout), proof_delims = [tstp_proof_delims], known_failures = [(Unprovable, "SZS status: Satisfiable"), @@ -279,7 +281,7 @@ "# Cannot determine problem status within resource limit"), (OutOfResources, "SZS status: ResourceOut"), (OutOfResources, "SZS status ResourceOut")], - max_new_clauses = 100, + max_axiom_clauses = 100, prefers_theory_relevant = false} val e = tptp_prover "e" e_config @@ -288,13 +290,13 @@ fun generic_dfg_prover (name, {home, executable, arguments, proof_delims, known_failures, - max_new_clauses, prefers_theory_relevant}) + max_axiom_clauses, prefers_theory_relevant}) (params as {overlord, respect_no_atp, relevance_threshold, convergence, theory_relevant, higher_order, follow_defs, ...}) minimize_command timeout = generic_prover overlord (get_relevant_facts respect_no_atp relevance_threshold convergence - higher_order follow_defs max_new_clauses + higher_order follow_defs max_axiom_clauses (the_default prefers_theory_relevant theory_relevant)) (prepare_clauses higher_order true) write_dfg_file home executable (arguments timeout) proof_delims known_failures name params @@ -307,15 +309,15 @@ val spass_config : prover_config = {home = getenv "SPASS_HOME", executable = "SPASS", - arguments = (fn timeout => "-Auto -SOS=1 -PGiven=0 -PProblem=0 -Splits=0" ^ - " -FullRed=0 -DocProof -VarWeight=3 -TimeLimit=" ^ - string_of_int (generous_to_secs timeout)), + arguments = fn timeout => + "-Auto -SOS=1 -PGiven=0 -PProblem=0 -Splits=0 -FullRed=0 -DocProof \ + \-VarWeight=3 -TimeLimit=" ^ string_of_int (to_generous_secs timeout), proof_delims = [("Here is a proof", "Formulae used in the proof")], known_failures = [(Unprovable, "SPASS beiseite: Completion found"), (TimedOut, "SPASS beiseite: Ran out of time"), (OutOfResources, "SPASS beiseite: Maximal number of loops exceeded")], - max_new_clauses = 40, + max_axiom_clauses = 40, prefers_theory_relevant = true} val spass = dfg_prover "spass" spass_config @@ -336,7 +338,7 @@ #known_failures spass_config @ [(OldSpass, "unrecognized option `-TPTP'"), (OldSpass, "Unrecognized option TPTP")], - max_new_clauses = #max_new_clauses spass_config, + max_axiom_clauses = #max_axiom_clauses spass_config, prefers_theory_relevant = #prefers_theory_relevant spass_config} val spass_tptp = tptp_prover "spass_tptp" spass_tptp_config @@ -367,17 +369,17 @@ [(TimedOut, "says Timeout"), (MalformedOutput, "Remote script could not extract proof")] -fun remote_prover_config prover_prefix args - ({proof_delims, known_failures, max_new_clauses, +fun remote_prover_config atp_prefix args + ({proof_delims, known_failures, max_axiom_clauses, prefers_theory_relevant, ...} : prover_config) : prover_config = {home = getenv "ISABELLE_ATP_MANAGER", executable = "SystemOnTPTP", - arguments = (fn timeout => - args ^ " -t " ^ string_of_int (generous_to_secs timeout) ^ " -s " ^ - the_system prover_prefix), + arguments = fn timeout => + args ^ " -t " ^ string_of_int (to_generous_secs timeout) ^ " -s " ^ + the_system atp_prefix, proof_delims = insert (op =) tstp_proof_delims proof_delims, known_failures = remote_known_failures @ known_failures, - max_new_clauses = max_new_clauses, + max_axiom_clauses = max_axiom_clauses, prefers_theory_relevant = prefers_theory_relevant} val remote_vampire = diff -r f4d84d84a01a -r b90fc0d75bca src/HOL/Tools/Sledgehammer/sledgehammer_fact_minimizer.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_fact_minimizer.ML Fri Apr 23 19:26:39 2010 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fact_minimizer.ML Fri Apr 23 19:36:49 2010 +0200 @@ -123,9 +123,8 @@ \option (e.g., \"timeout = " ^ string_of_int (10 + msecs div 1000) ^ " s\").") | {message, ...} => (NONE, "ATP error: " ^ message)) - handle Sledgehammer_HOL_Clause.TRIVIAL => - (SOME [], metis_line i n []) - | ERROR msg => (NONE, "Error: " ^ msg) + handle Sledgehammer_HOL_Clause.TRIVIAL => (SOME [], metis_line i n []) + | ERROR msg => (NONE, "Error: " ^ msg) end end;