--- a/src/HOL/Tools/ATP_Manager/atp_systems.ML Tue Jun 22 14:28:22 2010 +0200
+++ b/src/HOL/Tools/ATP_Manager/atp_systems.ML Tue Jun 22 14:48:46 2010 +0200
@@ -115,10 +115,15 @@
(j :: hd shape) :: tl shape
end
-fun generic_prover overlord get_facts prepare write_file home_var executable
- args proof_delims known_failures name
- ({debug, full_types, explicit_apply, isar_proof, isar_shrink_factor,
- ...} : params) minimize_command
+(* generic TPTP-based provers *)
+
+fun generic_tptp_prover
+ (name, {home_var, executable, arguments, proof_delims, known_failures,
+ max_axiom_clauses, prefers_theory_relevant})
+ ({debug, overlord, full_types, explicit_apply, respect_no_atp,
+ relevance_threshold, relevance_convergence, theory_relevant,
+ defs_relevant, isar_proof, isar_shrink_factor, ...} : params)
+ minimize_command timeout
({subgoal, goal, relevance_override, axiom_clauses, filtered_clauses}
: problem) =
let
@@ -129,14 +134,18 @@
val goal_cls = List.concat goal_clss
val the_filtered_clauses =
(case filtered_clauses of
- NONE => get_facts relevance_override goal goal_cls
+ NONE => relevant_facts full_types respect_no_atp relevance_threshold
+ relevance_convergence defs_relevant max_axiom_clauses
+ (the_default prefers_theory_relevant theory_relevant)
+ relevance_override goal goal_cls
| SOME fcls => fcls);
val the_axiom_clauses =
(case axiom_clauses of
NONE => the_filtered_clauses
| SOME axcls => axcls);
val (internal_thm_names, clauses) =
- prepare goal_cls the_axiom_clauses the_filtered_clauses thy
+ prepare_clauses full_types goal_cls the_axiom_clauses the_filtered_clauses
+ thy
(* path to unique problem file *)
val the_dest_dir = if overlord then getenv "ISABELLE_HOME_USER"
@@ -161,10 +170,10 @@
fun command_line probfile =
(if Config.get ctxt measure_runtime then
"TIMEFORMAT='%3U'; { time " ^
- space_implode " " [File.shell_path command, args,
+ space_implode " " [File.shell_path command, arguments timeout,
File.shell_path probfile] ^ " ; } 2>&1"
else
- space_implode " " ["exec", File.shell_path command, args,
+ space_implode " " ["exec", File.shell_path command, arguments timeout,
File.shell_path probfile, "2>&1"]) ^
(if overlord then
" | sed 's/,/, /g' \
@@ -189,7 +198,8 @@
if Config.get ctxt measure_runtime then split_time s else (s, 0)
fun run_on probfile =
if File.exists command then
- write_file full_types explicit_apply probfile clauses
+ write_tptp_file (debug andalso overlord) full_types explicit_apply
+ probfile clauses
|> pair (apfst split_time' (bash_output (command_line probfile)))
else if home = "" then
error ("The environment variable " ^ quote home_var ^ " is not set.")
@@ -233,25 +243,7 @@
proof = proof, internal_thm_names = internal_thm_names,
conjecture_shape = conjecture_shape,
filtered_clauses = the_filtered_clauses}
- end;
-
-
-(* generic TPTP-based provers *)
-
-fun generic_tptp_prover
- (name, {home_var, executable, arguments, proof_delims, known_failures,
- max_axiom_clauses, prefers_theory_relevant})
- (params as {debug, overlord, full_types, respect_no_atp,
- relevance_threshold, relevance_convergence, theory_relevant,
- defs_relevant, ...})
- minimize_command timeout =
- generic_prover overlord
- (relevant_facts full_types respect_no_atp relevance_threshold
- relevance_convergence defs_relevant max_axiom_clauses
- (the_default prefers_theory_relevant theory_relevant))
- (prepare_clauses full_types) (write_tptp_file (debug andalso overlord))
- home_var executable (arguments timeout) proof_delims known_failures name
- params minimize_command
+ end
fun tptp_prover name p = (name, generic_tptp_prover (name, p));