added "force_sos" options to control SPASS's and Vampire's use of SOS in experiments + added corresponding Mirabelle options

--- a/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML	Thu May 12 15:29:18 2011 +0200
+++ b/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML	Thu May 12 15:29:18 2011 +0200
@@ -10,6 +10,10 @@
 val keepK = "keep"
 val full_typesK = "full_types"
 val type_sysK = "type_sys"
+val slicingK = "slicing"
+val e_weight_methodK = "e_weight_method"
+val spass_force_sosK = "spass_force_sos"
+val vampire_force_sosK = "vampire_force_sos"
 val max_relevantK = "max_relevant"
 val minimizeK = "minimize"
 val minimize_timeoutK = "minimize_timeout"
@@ -348,7 +352,8 @@
   SH_FAIL of int * int |
   SH_ERROR
 
-fun run_sh prover_name prover type_sys max_relevant hard_timeout timeout dir st =
+fun run_sh prover_name prover type_sys max_relevant slicing e_weight_method spass_force_sos
+      vampire_force_sos hard_timeout timeout dir st =
   let
     val {context = ctxt, facts = chained_ths, goal} = Proof.goal st
     val i = 1
@@ -361,12 +366,19 @@
     val st' =
       st |> Proof.map_context
                 (change_dir dir
+                 #> (Option.map (Config.put ATP_Systems.e_weight_method)
+                       e_weight_method |> the_default I)
+                 #> (Option.map (Config.put ATP_Systems.spass_force_sos)
+                       spass_force_sos |> the_default I)
+                 #> (Option.map (Config.put ATP_Systems.vampire_force_sos)
+                       vampire_force_sos |> the_default I)
                  #> Config.put Sledgehammer_Provers.measure_run_time true)
     val params as {relevance_thresholds, max_relevant, slicing, ...} =
       Sledgehammer_Isar.default_params ctxt
           [("verbose", "true"),
            ("type_sys", type_sys),
            ("max_relevant", max_relevant),
+           ("slicing", slicing),
            ("timeout", string_of_int timeout)]
     val default_max_relevant =
       Sledgehammer_Provers.default_max_relevant_for_prover ctxt slicing
@@ -429,13 +441,20 @@
     val (prover_name, prover) = get_prover (Proof.context_of st) args
     val type_sys = AList.lookup (op =) args type_sysK |> the_default "smart"
     val max_relevant = AList.lookup (op =) args max_relevantK |> the_default "smart"
+    val slicing = AList.lookup (op =) args slicingK |> the_default "true"
+    val e_weight_method = AList.lookup (op =) args e_weight_methodK
+    val spass_force_sos = AList.lookup (op =) args spass_force_sosK
+      |> Option.map (curry (op <>) "false")
+    val vampire_force_sos = AList.lookup (op =) args vampire_force_sosK
+      |> Option.map (curry (op <>) "false")
     val dir = AList.lookup (op =) args keepK
     val timeout = Mirabelle.get_int_setting args (prover_timeoutK, 30)
     (* always use a hard timeout, but give some slack so that the automatic
        minimizer has a chance to do its magic *)
     val hard_timeout = SOME (2 * timeout)
     val (msg, result) =
-      run_sh prover_name prover type_sys max_relevant hard_timeout timeout dir st
+      run_sh prover_name prover type_sys max_relevant slicing e_weight_method spass_force_sos
+        vampire_force_sos hard_timeout timeout dir st
   in
     case result of
       SH_OK (time_isa, time_prover, names) =>

--- a/src/HOL/Tools/ATP/atp_systems.ML	Thu May 12 15:29:18 2011 +0200
+++ b/src/HOL/Tools/ATP/atp_systems.ML	Thu May 12 15:29:18 2011 +0200
@@ -31,6 +31,8 @@
   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_force_sos : bool Config.T
+  val vampire_force_sos : bool Config.T
   val eN : string
   val spassN : string
   val vampireN : string
@@ -230,15 +232,18 @@
 
 (* SPASS *)
 
+val spass_force_sos =
+  Attrib.setup_config_bool @{binding atp_spass_force_sos} (K false)
+
 (* The "-VarWeight=3" option helps the higher-order problems, probably by
    counteracting the presence of "hAPP". *)
 val spass_config : atp_config =
   {exec = ("ISABELLE_ATP", "scripts/spass"),
    required_execs = [("SPASS_HOME", "SPASS"), ("SPASS_HOME", "tptp2dfg")],
-   arguments = fn _ => fn slice => fn timeout => fn _ =>
+   arguments = fn ctxt => fn slice => fn timeout => fn _ =>
      ("-Auto -PGiven=0 -PProblem=0 -Splits=0 -FullRed=0 -DocProof \
       \-VarWeight=3 -TimeLimit=" ^ string_of_int (to_secs 0 timeout))
-     |> slice = 0 ? prefix "-SOS=1 ",
+     |> (slice = 0 orelse Config.get ctxt spass_force_sos) ? prefix "-SOS=1 ",
    proof_delims = [("Here is a proof", "Formulae used in the proof")],
    known_failures =
      known_perl_failures @
@@ -252,24 +257,30 @@
    conj_sym_kind = Axiom, (* FIXME: try out Hypothesis *)
    prem_kind = Conjecture,
    formats = [Fof],
-   best_slices =
+   best_slices = fn ctxt =>
      (* FUDGE *)
-     K [(0.667, (false, (150, ["mangled_preds"]))) (* SOS *),
-        (0.333, (true, (150, ["mangled_preds"]))) (* ~SOS *)]}
+     [(0.667, (false, (150, ["mangled_preds"]))) (* SOS *),
+      (0.333, (true, (150, ["mangled_preds"]))) (* ~SOS *)]
+     |> (if Config.get ctxt spass_force_sos then hd #> apfst (K 1.0) #> single
+         else I)}
 
 val spass = (spassN, spass_config)
 
 
 (* Vampire *)
 
+val vampire_force_sos =
+  Attrib.setup_config_bool @{binding atp_vampire_force_sos} (K false)
+
 val vampire_config : atp_config =
   {exec = ("VAMPIRE_HOME", "vampire"),
    required_execs = [],
-   arguments = fn _ => fn slice => fn timeout => fn _ =>
+   arguments = fn ctxt => fn slice => fn timeout => fn _ =>
      (* This would work too but it's less tested: "--proof tptp " ^ *)
      "--mode casc -t " ^ string_of_int (to_secs 0 timeout) ^
      " --thanks \"Andrei and Krystof\" --input_file"
-     |> slice = 0 ? prefix "--sos on ",
+     |> (slice = 0 orelse Config.get ctxt vampire_force_sos)
+        ? prefix "--sos on ",
    proof_delims =
      [("=========== Refutation ==========",
        "======= End of refutation ======="),
@@ -289,10 +300,12 @@
    conj_sym_kind = Conjecture, (* FIXME: try out Hypothesis *)
    prem_kind = Conjecture,
    formats = [Fof],
-   best_slices =
+   best_slices = fn ctxt =>
      (* FUDGE *)
-     K [(0.667, (false, (450, ["mangled_tags!", "mangled_preds?"]))) (* SOS *),
-        (0.333, (true, (450, ["mangled_tags!", "mangled_preds?"]))) (* ~SOS *)]}
+     [(0.667, (false, (450, ["mangled_tags!", "mangled_preds?"]))) (* SOS *),
+      (0.333, (true, (450, ["mangled_tags!", "mangled_preds?"]))) (* ~SOS *)]
+     |> (if Config.get ctxt vampire_force_sos then hd #> apfst (K 1.0) #> single
+         else I)}
 
 val vampire = (vampireN, vampire_config)