--- a/src/HOL/Tools/ATP_Manager/atp_systems.ML Tue Jun 22 13:17:59 2010 +0200
+++ b/src/HOL/Tools/ATP_Manager/atp_systems.ML Tue Jun 22 14:28:22 2010 +0200
@@ -110,7 +110,7 @@
fun shape_of_clauses _ [] = []
| shape_of_clauses j ([] :: clauses) = [] :: shape_of_clauses j clauses
- | shape_of_clauses j ((lit :: lits) :: clauses) =
+ | shape_of_clauses j ((_ :: lits) :: clauses) =
let val shape = shape_of_clauses (j + 1) (lits :: clauses) in
(j :: hd shape) :: tl shape
end
@@ -123,7 +123,7 @@
: problem) =
let
(* get clauses and prepare them for writing *)
- val (ctxt, (chained_ths, th)) = goal;
+ val (ctxt, (_, th)) = goal;
val thy = ProofContext.theory_of ctxt;
val goal_clss = #1 (neg_conjecture_clauses ctxt th subgoal)
val goal_cls = List.concat goal_clss
@@ -136,7 +136,7 @@
NONE => the_filtered_clauses
| SOME axcls => axcls);
val (internal_thm_names, clauses) =
- prepare goal_cls chained_ths the_axiom_clauses the_filtered_clauses thy;
+ prepare 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"
@@ -243,16 +243,15 @@
max_axiom_clauses, prefers_theory_relevant})
(params as {debug, overlord, full_types, respect_no_atp,
relevance_threshold, relevance_convergence, theory_relevant,
- defs_relevant, isar_proof, ...})
+ 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 false full_types)
- (write_tptp_file (debug andalso overlord)) home_var
- executable (arguments timeout) proof_delims known_failures name params
- minimize_command
+ (prepare_clauses full_types) (write_tptp_file (debug andalso overlord))
+ home_var executable (arguments timeout) proof_delims known_failures name
+ params minimize_command
fun tptp_prover name p = (name, generic_tptp_prover (name, p));
@@ -313,31 +312,14 @@
(* SPASS *)
-fun generic_dfg_prover
- (name, {home_var, executable, arguments, proof_delims, known_failures,
- max_axiom_clauses, prefers_theory_relevant})
- (params as {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 true full_types) write_dfg_file home_var executable
- (arguments timeout) proof_delims known_failures name params
- minimize_command
-
-fun dfg_prover name p = (name, generic_dfg_prover (name, p))
-
(* The "-VarWeight=3" option helps the higher-order problems, probably by
counteracting the presence of "hAPP". *)
-fun generic_spass_config dfg : prover_config =
+val spass_config : prover_config =
{home_var = "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 (to_generous_secs timeout)
- |> not dfg ? prefix "-TPTP ",
+ "-TPTP -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 =
[(IncompleteUnprovable, "SPASS beiseite: Completion found"),
@@ -349,10 +331,6 @@
(OldSpass, "Unrecognized option TPTP")],
max_axiom_clauses = 40,
prefers_theory_relevant = true}
-val spass_dfg_config = generic_spass_config true
-val spass_dfg = dfg_prover "spass_dfg" spass_dfg_config
-
-val spass_config = generic_spass_config false
val spass = tptp_prover "spass" spass_config
(* remote prover invocation via SystemOnTPTP *)
@@ -414,8 +392,7 @@
space_implode " " [maybe_remote e e_config, maybe_remote spass spass_config,
remotify (fst vampire)]
-val provers =
- [spass, spass_dfg, vampire, e, remote_vampire, remote_spass, remote_e]
+val provers = [spass, vampire, e, remote_vampire, remote_spass, remote_e]
val prover_setup = fold add_prover provers
val setup =