# HG changeset patch
# User blanchet
# Date 1328017161 -3600
# Node ID 7e049e9f5c8b7e4dbf00bf6a497b08071eda9072
# Parent  de5dd84717c1ea34d6f0f16180255ed3474c3f3b
new SPASS setup

diff -r de5dd84717c1 -r 7e049e9f5c8b src/HOL/Tools/ATP/atp_problem.ML
--- a/src/HOL/Tools/ATP/atp_problem.ML	Tue Jan 31 12:43:48 2012 +0100
+++ b/src/HOL/Tools/ATP/atp_problem.ML	Tue Jan 31 14:39:21 2012 +0100
@@ -439,7 +439,7 @@
       if top_level then
         case extract_isabelle_info info of
           SOME s' => if s' = simpN then s ^ ":lr"
-                     else if s' = eqN then s ^ ":lr" (* not yet ":lt" *)
+                     else if s' = eqN then s ^ ":lt"
                      else s
         | NONE => s
       else
diff -r de5dd84717c1 -r 7e049e9f5c8b src/HOL/Tools/ATP/atp_problem_generate.ML
--- a/src/HOL/Tools/ATP/atp_problem_generate.ML	Tue Jan 31 12:43:48 2012 +0100
+++ b/src/HOL/Tools/ATP/atp_problem_generate.ML	Tue Jan 31 14:39:21 2012 +0100
@@ -1186,8 +1186,7 @@
             |>> map2 (fn (name, (kind, _)) => fn t => (name, (kind, t))) facts
     val lam_facts =
       map2 (fn t => fn j =>
-               ((lam_fact_prefix ^ Int.toString j, (Global, General)),
-                (Axiom, t)))
+               ((lam_fact_prefix ^ Int.toString j, (Global, Eq)), (Axiom, t)))
            lambda_ts (1 upto length lambda_ts)
   in (facts, lam_facts) end
 
diff -r de5dd84717c1 -r 7e049e9f5c8b src/HOL/Tools/ATP/atp_systems.ML
--- a/src/HOL/Tools/ATP/atp_systems.ML	Tue Jan 31 12:43:48 2012 +0100
+++ b/src/HOL/Tools/ATP/atp_systems.ML	Tue Jan 31 14:39:21 2012 +0100
@@ -37,6 +37,7 @@
   val e_default_sym_offs_weight : real Config.T
   val e_sym_offs_weight_base : real Config.T
   val e_sym_offs_weight_span : real Config.T
+  val spass_incompleteN : string
   val eN : string
   val e_sineN : string
   val e_tofofN : string
@@ -312,6 +313,8 @@
 
 (* SPASS *)
 
+val spass_incompleteN = "incomplete"
+
 (* The "-VarWeight=3" option helps the higher-order problems, probably by
    counteracting the presence of explicit application operators. *)
 val spass_config : atp_config =
@@ -350,24 +353,21 @@
 val spass_new_config : atp_config =
   {exec = ("ISABELLE_ATP", "scripts/spass_new"),
    required_execs = [],
-   arguments = fn _ => fn _ => fn sos => fn timeout => fn _ =>
-     (* -Splits=0 -FullRed=0 -VarWeight=3? *)
+   arguments = fn _ => fn _ => fn incomplete => fn timeout => fn _ =>
      ("-Auto -LR=1 -Isabelle=1 -TimeLimit=" ^ string_of_int (to_secs 1 timeout))
-     |> sos = sosN ? prefix "-SOS=1 ",
+     |> incomplete = spass_incompleteN ? prefix "-Splits=0 -FullRed=0 ",
    proof_delims = #proof_delims spass_config,
    known_failures = #known_failures spass_config,
    conj_sym_kind = #conj_sym_kind spass_config,
    prem_kind = #prem_kind spass_config,
    best_slices = fn ctxt =>
      (* FUDGE *)
-     [(0.333, (false, (150, DFG DFG_Sorted, "mono_simple", liftingN,
-                       no_sosN))),
+     [(0.333, (false, (150, DFG DFG_Sorted, "poly_tags??", combs_and_liftingN,
+                       ""))),
       (0.333, (false, (300, DFG DFG_Sorted, "mono_simple", liftingN,
-                       no_sosN))),
-      (0.334, (true, (50, DFG DFG_Sorted, "mono_simple", liftingN,
-                      no_sosN)))]
-     |> (if Config.get ctxt force_sos then hd #> apfst (K 1.0) #> single
-         else I)}
+                       spass_incompleteN))),
+      (0.334, (false, (50, DFG DFG_Sorted, "mono_simple", combs_and_liftingN,
+                       "")))]}
 
 val spass_new = (spass_newN, spass_new_config)