# HG changeset patch
# User blanchet
# Date 1328794527 -3600
# Node ID db6d2a89a21fa5940b5fa62bbc1819a54cd916ac
# Parent  c862760145716e13387782d29979849f57fe42b1
new SPASS slices

diff -r c86276014571 -r db6d2a89a21f src/HOL/Tools/ATP/atp_systems.ML
--- a/src/HOL/Tools/ATP/atp_systems.ML	Thu Feb 09 14:04:17 2012 +0100
+++ b/src/HOL/Tools/ATP/atp_systems.ML	Thu Feb 09 14:35:27 2012 +0100
@@ -37,7 +37,6 @@
   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
@@ -314,8 +313,6 @@
 
 (* 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,28 +347,30 @@
 
 val spass = (spassN, spass_config)
 
-val spass_new_slice_1 = (300, DFG DFG_Sorted, "mono_native", combsN, true)
-val spass_new_slice_2 = (50, DFG DFG_Sorted, "mono_native", combsN, true)
-val spass_new_slice_3 = (150, DFG DFG_Sorted, "mono_native", liftingN, true)
-
 (* Experimental *)
 val spass_new_config : atp_config =
   {exec = ("SPASS_NEW_HOME", "SPASS"),
    required_execs = [],
-   arguments = fn _ => fn _ => fn incomplete => fn timeout => fn _ =>
+   arguments = fn _ => fn _ => fn extra_options => fn timeout => fn _ =>
      (* TODO: add: -FPDFGProof -FPFCR *)
      ("-Isabelle=1 -TimeLimit=" ^ string_of_int (to_secs 1 timeout))
-     (* TODO: not used yet *)
-     |> incomplete = spass_incompleteN ? prefix "-Splits=0 -FullRed=0 ",
+     |> extra_options <> "" ? prefix (extra_options ^ " "),
    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 _ =>
      (* FUDGE *)
-     [(0.300, (true, (spass_new_slice_1, ""))),
-      (0.333, (true, (spass_new_slice_2, ""))),
-      (0.333, (true, (spass_new_slice_3, "")))]}
+     [(0.25, (true, ((150, DFG DFG_Sorted, "mono_native", combsN, true),
+                     "-Heuristic=1"))),
+      (0.20, (true, ((500, DFG DFG_Sorted, "mono_native", liftingN, true),
+                     "-Heuristic=2 -SOS"))),
+      (0.20, (true, ((50, DFG DFG_Sorted, "mono_native", liftingN, true),
+                     "-Heuristic=2"))),
+      (0.20, (true, ((250, DFG DFG_Sorted, "mono_native", combs_and_liftingN,
+                      true), "-Heuristic=2"))),
+      (0.15, (true, ((100, DFG DFG_Sorted, "mono_native", combs_and_liftingN,
+                      true), "-Heuristic=2")))]}
 
 val spass_new = (spass_newN, spass_new_config)