# HG changeset patch
# User boehmes
# Date 1254653962 -7200
# Node ID 159309603edcf6ceda21813a50eb61b828f8d3b8
# Parent  5f1805c6ef2a64a2b8f75ade396f380864e5bb44
recovered support for Spass: re-enabled writing problems in DFG format

diff -r 5f1805c6ef2a -r 159309603edc src/HOL/Tools/ATP_Manager/atp_wrapper.ML
--- a/src/HOL/Tools/ATP_Manager/atp_wrapper.ML	Sun Oct 04 11:45:41 2009 +0200
+++ b/src/HOL/Tools/ATP_Manager/atp_wrapper.ML	Sun Oct 04 12:59:22 2009 +0200
@@ -263,8 +263,32 @@
   insert_theory_const = insert_theory_const,
   emit_structured_proof = false }
 
-val spass = tptp_prover ("spass", spass_config spass_insert_theory_const)
-val spass_no_tc = tptp_prover ("spass_no_tc", spass_config false)
+fun gen_dfg_prover (name, prover_config) problem timeout =
+  let
+    val Prover_Config {max_new_clauses, insert_theory_const,
+      emit_structured_proof, command, arguments} = prover_config
+    val ATP_Problem {with_full_types, subgoal, goal, axiom_clauses,
+      filtered_clauses} = problem
+  in
+    external_prover
+      (ResAtp.get_relevant max_new_clauses insert_theory_const)
+      (ResAtp.prepare_clauses true)
+      (ResHolClause.dfg_write_file with_full_types)
+      command
+      (arguments timeout)
+      ResReconstruct.find_failure
+      (ResReconstruct.lemma_list true)
+      axiom_clauses
+      filtered_clauses
+      name
+      subgoal
+      goal
+  end
+
+fun dfg_prover (name, config) = (name, gen_dfg_prover (name, config))
+
+val spass = dfg_prover ("spass", spass_config spass_insert_theory_const)
+val spass_no_tc = dfg_prover ("spass_no_tc", spass_config false)
 
 
 (* remote prover invocation via SystemOnTPTP *)