# HG changeset patch
# User blanchet
# Date 1319886958 -7200
# Node ID e6901aa86a9e0fdea6dc61a0f930d53164d2d835
# Parent  bd03b08161ac6ef14784ec776b10592c53a5502f
always use DFG format to talk to SPASS -- since that's what we'll need to use anyway to benefit from sorts and other extensions

diff -r bd03b08161ac -r e6901aa86a9e src/HOL/Tools/ATP/atp_problem.ML
--- a/src/HOL/Tools/ATP/atp_problem.ML	Sat Oct 29 13:15:58 2011 +0200
+++ b/src/HOL/Tools/ATP/atp_problem.ML	Sat Oct 29 13:15:58 2011 +0200
@@ -459,6 +459,7 @@
 
 fun dfg_lines flavor problem =
   let
+    val sorted = (flavor = DFG_Sorted)
     val format = DFG flavor
     fun ary sym ty =
       "(" ^ sym ^ ", " ^ string_of_int (arity_of_type ty) ^ ")"
@@ -485,19 +486,21 @@
                if is_predicate_type ty then SOME (ary sym ty) else NONE
              | _ => NONE)
       |> commas |> enclose "predicates [" "]."
-    val sorts =
+    fun sorts () =
       filt (fn Decl (_, sym, AType (s, [])) =>
                if s = tptp_type_of_types then SOME sym else NONE
              | _ => NONE)
       |> commas |> enclose "sorts [" "]."
-    val func_sigs =
+    val syms = [func_aries, pred_aries] @ (if sorted then [sorts ()] else [])
+    fun func_sigs () =
       filt (fn Decl (_, sym, ty) =>
                if is_function_type ty then SOME (fun_typ sym ty) else NONE
              | _ => NONE)
-    val pred_sigs =
+    fun pred_sigs () =
       filt (fn Decl (_, sym, ty) =>
                if is_predicate_type ty then SOME (pred_typ sym ty) else NONE
              | _ => NONE)
+    val decls = if sorted then func_sigs () @ pred_sigs () else []
     val axioms = filt (formula (curry (op <>) Conjecture))
     val conjs = filt (formula (curry (op =) Conjecture))
     fun list_of _ [] = []
@@ -509,8 +512,8 @@
     list_of "descriptions"
             ["name({**}).", "author({**}).", "status(unknown).",
              "description({**})."] @
-    list_of "symbols" [func_aries, pred_aries, sorts] @
-    list_of "declarations" (func_sigs @ pred_sigs) @
+    list_of "symbols" syms @
+    list_of "declarations" decls @
     list_of "formulae(axioms)" axioms @
     list_of "formulae(conjectures)" conjs @
     ["end_problem.\n"]
diff -r bd03b08161ac -r e6901aa86a9e src/HOL/Tools/ATP/atp_systems.ML
--- a/src/HOL/Tools/ATP/atp_systems.ML	Sat Oct 29 13:15:58 2011 +0200
+++ b/src/HOL/Tools/ATP/atp_systems.ML	Sat Oct 29 13:15:58 2011 +0200
@@ -322,9 +322,9 @@
    prem_kind = Conjecture,
    best_slices = fn ctxt =>
      (* FUDGE *)
-     [(0.333, (false, (150, FOF, "mono_tags??", sosN))),
-      (0.333, (false, (300, FOF, "poly_tags??", sosN))),
-      (0.334, (true, (50, FOF, "mono_tags??", no_sosN)))]
+     [(0.333, (false, (150, DFG DFG_Unsorted, "mono_tags??", sosN))),
+      (0.333, (false, (300, DFG DFG_Unsorted, "poly_tags??", sosN))),
+      (0.334, (true, (50, DFG DFG_Unsorted, "mono_tags??", no_sosN)))]
      |> (if Config.get ctxt force_sos then hd #> apfst (K 1.0) #> single
          else I)}
 
diff -r bd03b08161ac -r e6901aa86a9e src/HOL/Tools/ATP/atp_translate.ML
--- a/src/HOL/Tools/ATP/atp_translate.ML	Sat Oct 29 13:15:58 2011 +0200
+++ b/src/HOL/Tools/ATP/atp_translate.ML	Sat Oct 29 13:15:58 2011 +0200
@@ -2365,7 +2365,6 @@
           | FOF => I
           | TFF (_, TPTP_Implicit) => I
           | THF (_, TPTP_Implicit, _) => I
-          | DFG DFG_Unsorted => I
           | _ => declare_undeclared_syms_in_atp_problem type_decl_prefix
                                                         implicit_declsN)
     val (problem, pool) = problem |> nice_atp_problem readable_names
diff -r bd03b08161ac -r e6901aa86a9e src/HOL/Tools/ATP/scripts/spass
--- a/src/HOL/Tools/ATP/scripts/spass	Sat Oct 29 13:15:58 2011 +0200
+++ b/src/HOL/Tools/ATP/scripts/spass	Sat Oct 29 13:15:58 2011 +0200
@@ -8,15 +8,11 @@
 options=${@:1:$(($#-1))}
 name=${@:$(($#)):1}
 
-# Try converting the file from TPTP to DFG, but fail gracefully if it is already
-# in DFG format.
-"$SPASS_HOME/tptp2dfg" $name $name.fof.dfg || cp $name $name.fof.dfg
-"$SPASS_HOME/SPASS" -Flotter $name.fof.dfg \
+"$SPASS_HOME/SPASS" -Flotter $name \
     | sed 's/description({$/description({*/' \
     | sed 's/set_ClauseFormulaRelation()\.//' \
-    > $name.cnf.dfg
-rm -f $name.fof.dfg
-cat $name.cnf.dfg
-"$SPASS_HOME/SPASS" $options $name.cnf.dfg \
+    > $name.cnf
+cat $name.cnf
+"$SPASS_HOME/SPASS" $options $name.cnf \
     | sed 's/\(Formulae used in the proof :\).*/\1 N\/A/'
-rm -f $name.cnf.dfg
+rm -f $name.cnf