# HG changeset patch
# User blanchet
# Date 1335395106 -7200
# Node ID 024cf0f7fb6de29059acd14d9882a93b52d8ba1a
# Parent  ccb1d4874f63df08a7d8926aa320d25145f048ca
further tweaking for Satallax, so that TPTP problems before parsing and after generation are as similar as possible/practical

diff -r ccb1d4874f63 -r 024cf0f7fb6d src/HOL/TPTP/atp_problem_import.ML
--- a/src/HOL/TPTP/atp_problem_import.ML	Thu Apr 26 00:33:47 2012 +0200
+++ b/src/HOL/TPTP/atp_problem_import.ML	Thu Apr 26 01:05:06 2012 +0200
@@ -21,6 +21,9 @@
 open ATP_Problem
 open ATP_Proof
 
+val debug = false
+val overlord = false
+
 
 (** TPTP parsing **)
 
@@ -70,10 +73,8 @@
        ("batch_size", "10"),
        ("falsify", if null conjs then "false" else "true"),
        ("verbose", "true"),
-(*
-       ("debug", "true"),
-       ("overlord", "true"),
-*)
+       ("debug", if debug then "true" else "false"),
+       ("overlord", if overlord then "true" else "false"),
        ("show_consts", "true"),
        ("format", "1"),
        ("max_potential", "0"),
@@ -138,11 +139,8 @@
 
 fun atp_tac ctxt timeout prover =
   Sledgehammer_Tactics.sledgehammer_as_oracle_tac ctxt
-      [
-(*
-       ("debug", "true"),
-       ("overlord", "true"),
-*)
+      [("debug", if debug then "true" else "false"),
+       ("overlord", if overlord then "true" else "false"),
        ("provers", prover),
        ("timeout", string_of_int timeout)]
       {add = [], del = [], only = true} i
@@ -152,6 +150,8 @@
     fun slice timeout prover =
       SOLVE_TIMEOUT timeout prover (atp_tac ctxt timeout prover)
   in
+    slice timeout ATP_Systems.satallaxN
+    ORELSE
     slice (timeout div 10) ATP_Systems.spassN
     ORELSE
     slice (timeout div 10) z3N
@@ -163,8 +163,6 @@
     slice (timeout div 10) cvc3N
     ORELSE
     slice (timeout div 10) ATP_Systems.leo2N
-    ORELSE
-    slice timeout ATP_Systems.satallaxN
   end
 
 fun auto_etc_tac ctxt timeout =
@@ -185,9 +183,9 @@
   ORELSE
   SOLVE_TIMEOUT timeout "fastforce" (fast_force_tac ctxt i)
 
-fun make_conj assms conjs =
-  (rev assms, case conjs of conj :: _ => conj | [] => @{prop False})
-  |> Logic.list_implies
+fun make_conj (defs, nondefs) conjs =
+  Logic.list_implies (rev defs @ rev nondefs,
+                      case conjs of conj :: _ => conj | [] => @{prop False})
 
 fun print_szs_from_success conjs success =
   writeln ("% SZS status " ^
@@ -198,8 +196,8 @@
 
 fun sledgehammer_tptp_file timeout file_name =
   let
-    val (conjs, (defs, nondefs), ctxt) = read_tptp_file @{theory} file_name
-    val conj = make_conj (defs @ nondefs) conjs
+    val (conjs, assms, ctxt) = read_tptp_file @{theory} file_name
+    val conj = make_conj assms conjs
   in
     can_tac ctxt (sledgehammer_tac ctxt timeout) conj
     |> print_szs_from_success conjs
@@ -207,8 +205,8 @@
 
 fun isabelle_tptp_file timeout file_name =
   let
-    val (conjs, (defs, nondefs), ctxt) = read_tptp_file @{theory} file_name
-    val conj = make_conj (defs @ nondefs) conjs
+    val (conjs, assms, ctxt) = read_tptp_file @{theory} file_name
+    val conj = make_conj assms conjs
   in
     (can_tac ctxt (sledgehammer_tac ctxt (timeout div 2)) conj orelse
      can_tac ctxt (auto_etc_tac ctxt (timeout div 2)) conj orelse
diff -r ccb1d4874f63 -r 024cf0f7fb6d src/HOL/Tools/ATP/atp_problem_generate.ML
--- a/src/HOL/Tools/ATP/atp_problem_generate.ML	Thu Apr 26 00:33:47 2012 +0200
+++ b/src/HOL/Tools/ATP/atp_problem_generate.ML	Thu Apr 26 01:05:06 2012 +0200
@@ -1257,8 +1257,15 @@
      atomic_types = atomic_Ts}
   end
 
+(* Satallax prefers "=" to "<=>" *)
+fun is_format_eq_as_iff FOF = true
+  | is_format_eq_as_iff (TFF _) = true
+  | is_format_eq_as_iff (DFG _) = true
+  | is_format_eq_as_iff _ = false
+
 fun make_fact ctxt format type_enc eq_as_iff ((name, stature), t) =
-  case t |> make_formula ctxt type_enc (eq_as_iff andalso format <> CNF) name
+  case t |> make_formula ctxt type_enc
+                         (eq_as_iff andalso is_format_eq_as_iff format) name
                          stature Axiom of
     formula as {iformula = AAtom (IConst ((s, _), _, _)), ...} =>
     if s = tptp_true then NONE else SOME formula
@@ -1274,7 +1281,8 @@
 fun make_conjecture ctxt format type_enc =
   map (fn ((name, stature), (kind, t)) =>
           t |> kind = Conjecture ? s_not
-            |> make_formula ctxt type_enc (format <> CNF) name stature kind)
+            |> make_formula ctxt type_enc (is_format_eq_as_iff format) name
+                            stature kind)
 
 (** Finite and infinite type inference **)