src/HOL/Tools/ATP_Manager/atp_wrapper.ML

--- a/src/HOL/Tools/ATP_Manager/atp_wrapper.ML	Tue Apr 20 17:41:00 2010 +0200
+++ b/src/HOL/Tools/ATP_Manager/atp_wrapper.ML	Wed Apr 21 11:03:35 2010 +0200
@@ -166,16 +166,16 @@
 fun generic_tptp_prover
         (name, {command, arguments, failure_strs, max_new_clauses,
                 prefers_theory_relevant, supports_isar_proofs})
-        (params as {overlord, respect_no_atp, relevance_threshold, convergence,
-                    theory_relevant, higher_order, follow_defs, isar_proof,
-                    modulus, sorts, ...})
+        (params as {debug, overlord, respect_no_atp, relevance_threshold,
+                    convergence, theory_relevant, higher_order, follow_defs,
+                    isar_proof, modulus, sorts, ...})
         timeout =
   generic_prover overlord
       (get_relevant_facts respect_no_atp relevance_threshold convergence
                           higher_order follow_defs max_new_clauses
                           (the_default prefers_theory_relevant theory_relevant))
       (prepare_clauses higher_order false)
-      (write_tptp_file (overlord andalso not isar_proof)) command
+      (write_tptp_file (debug andalso overlord andalso not isar_proof)) command
       (arguments timeout) failure_strs
       (proof_text (supports_isar_proofs andalso isar_proof) false modulus sorts)
       name params
@@ -236,7 +236,7 @@
       (arguments timeout) failure_strs (metis_proof_text false false)
       name params
 
-fun dfg_prover (name, p) = (name, generic_dfg_prover (name, p));
+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". *)
@@ -251,8 +251,21 @@
   max_new_clauses = 40,
   prefers_theory_relevant = true,
   supports_isar_proofs = false}
-val spass = dfg_prover ("spass", spass_config)
+val spass = dfg_prover "spass" spass_config
+
+(* SPASS 3.7 supports both the DFG and the TPTP syntax, whereas SPASS 3.0
+   supports only the DFG syntax. As soon as all Isabelle repository/snapshot
+   users have upgraded to 3.7, we can kill "spass" (and all DFG support in
+   Sledgehammer) and rename "spass_tptp" "spass". *)
 
+val spass_tptp_config =
+  {command = #command spass_config,
+   arguments = prefix "-TPTP " o #arguments spass_config,
+   failure_strs = #failure_strs spass_config,
+   max_new_clauses = #max_new_clauses spass_config,
+   prefers_theory_relevant = #prefers_theory_relevant spass_config,
+   supports_isar_proofs = #supports_isar_proofs spass_config}
+val spass_tptp = tptp_prover "spass_tptp" spass_tptp_config
 
 (* remote prover invocation via SystemOnTPTP *)
 
@@ -304,7 +317,8 @@
 val remote_spass =
   tptp_prover "remote_spass" (remote_prover_config "SPASS---" "-x" spass_config)
 
-val provers = [spass, vampire, e, remote_vampire, remote_spass, remote_e]
+val provers = [spass, spass_tptp, vampire, e, remote_vampire, remote_spass,
+               remote_e]
 val prover_setup = fold add_prover provers
 
 val setup =