# HG changeset patch
# User blanchet
# Date 1327940338 -3600
# Node ID b3e53dd6f10a301b0bbf07ede2bfbf547e6ac33f
# Parent  9ac0c64ad8e75f20c46a7bb19cc320f8ad3023db
new SPASS setup

diff -r 9ac0c64ad8e7 -r b3e53dd6f10a src/HOL/Tools/ATP/atp_problem_generate.ML
--- a/src/HOL/Tools/ATP/atp_problem_generate.ML	Mon Jan 30 17:15:59 2012 +0100
+++ b/src/HOL/Tools/ATP/atp_problem_generate.ML	Mon Jan 30 17:18:58 2012 +0100
@@ -2433,8 +2433,8 @@
 
 (* Forcing explicit applications is expensive for polymorphic encodings, because
    it takes only one existential variable ranging over "'a => 'b" to ruin
-   everything. Hence we do it only if there are few facts (is normally the case
-   for "metis" and the minimizer. *)
+   everything. Hence we do it only if there are few facts (which is normally the
+   case for "metis" and the minimizer). *)
 val explicit_apply_threshold = 50
 
 fun prepare_atp_problem ctxt format conj_sym_kind prem_kind type_enc exporter
@@ -2443,11 +2443,11 @@
     val thy = Proof_Context.theory_of ctxt
     val type_enc = type_enc |> adjust_type_enc format
     val explicit_apply =
-      if polymorphism_of_type_enc type_enc <> Polymorphic orelse
-         length facts <= explicit_apply_threshold then
+      if polymorphism_of_type_enc type_enc = Polymorphic andalso
+         length facts >= explicit_apply_threshold then
+        SOME false
+      else
         NONE
-      else
-        SOME false
     val lam_trans =
       if lam_trans = keep_lamsN andalso
          not (is_type_enc_higher_order type_enc) then
diff -r 9ac0c64ad8e7 -r b3e53dd6f10a src/HOL/Tools/ATP/atp_systems.ML
--- a/src/HOL/Tools/ATP/atp_systems.ML	Mon Jan 30 17:15:59 2012 +0100
+++ b/src/HOL/Tools/ATP/atp_systems.ML	Mon Jan 30 17:18:58 2012 +0100
@@ -348,9 +348,12 @@
 
 (* Experimental *)
 val spass_new_config : atp_config =
-  {exec = ("SPASS_HOME", "SPASS"),
+  {exec = ("ISABELLE_ATP", "scripts/spass_new"),
    required_execs = [],
-   arguments = #arguments spass_config,
+   arguments = fn _ => fn _ => fn sos => fn timeout => fn _ =>
+     (* -Splits=0 -FullRed=0 -VarWeight=3? *)
+     ("-Auto -LR=1 -Isabelle=1 -TimeLimit=" ^ string_of_int (to_secs 1 timeout))
+     |> sos = sosN ? prefix "-SOS=1 ",
    proof_delims = #proof_delims spass_config,
    known_failures = #known_failures spass_config,
    conj_sym_kind = #conj_sym_kind spass_config,
@@ -358,11 +361,11 @@
    best_slices = fn ctxt =>
      (* FUDGE *)
      [(0.333, (false, (150, DFG DFG_Sorted, "mono_simple", liftingN,
-                       sosN))) (*,
-      (0.333, (false, (300, DFG DFG_Sorted, "poly_tags??", liftingN,
-                       sosN))),
+                       no_sosN))),
+      (0.333, (false, (300, DFG DFG_Sorted, "mono_simple", liftingN,
+                       no_sosN))),
       (0.334, (true, (50, DFG DFG_Sorted, "mono_simple", liftingN,
-                      no_sosN)))*)]
+                      no_sosN)))]
      |> (if Config.get ctxt force_sos then hd #> apfst (K 1.0) #> single
          else I)}
 
diff -r 9ac0c64ad8e7 -r b3e53dd6f10a src/HOL/Tools/ATP/scripts/spass_new
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Tools/ATP/scripts/spass_new	Mon Jan 30 17:18:58 2012 +0100
@@ -0,0 +1,14 @@
+#!/usr/bin/env bash
+#
+# Wrapper for SPASS 3.8 that also outputs the clause-to-formula relation
+#
+# Author: Jasmin Blanchette, TU Muenchen
+
+options=${@:1:$(($#-1))}
+name=${@:$(($#)):1}
+
+rm -f $name.prf
+"$SPASS_NEW_HOME/SPASS" -FPDFGProof -FPFCR $options $name \
+    | sed 's/\(Formulae used in the proof :\).*/\1 N\/A/'
+cat $name.prf
+#rm -f $name.cnf