1.1 --- a/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML	Tue Aug 09 17:33:17 2011 +0200
     1.2 +++ b/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML	Tue Aug 09 17:33:17 2011 +0200
     1.3 @@ -13,8 +13,7 @@
     1.4  val slicingK = "slicing"
     1.5  val lambda_translationK = "lambda_translation"
     1.6  val e_weight_methodK = "e_weight_method"
     1.7 -val spass_force_sosK = "spass_force_sos"
     1.8 -val vampire_force_sosK = "vampire_force_sos"
     1.9 +val force_sosK = "force_sos"
    1.10  val max_relevantK = "max_relevant"
    1.11  val minimizeK = "minimize"
    1.12  val minimize_timeoutK = "minimize_timeout"
    1.13 @@ -354,8 +353,8 @@
    1.14    SH_ERROR
    1.15  
    1.16  fun run_sh prover_name prover type_enc sound max_relevant slicing
    1.17 -        lambda_translation e_weight_method spass_force_sos vampire_force_sos
    1.18 -        hard_timeout timeout dir pos st =
    1.19 +        lambda_translation e_weight_method force_sos hard_timeout timeout dir
    1.20 +        pos st =
    1.21    let
    1.22      val {context = ctxt, facts = chained_ths, goal} = Proof.goal st
    1.23      val i = 1
    1.24 @@ -375,10 +374,8 @@
    1.25                         lambda_translation |> the_default I)
    1.26                   #> (Option.map (Config.put ATP_Systems.e_weight_method)
    1.27                         e_weight_method |> the_default I)
    1.28 -                 #> (Option.map (Config.put ATP_Systems.spass_force_sos)
    1.29 -                       spass_force_sos |> the_default I)
    1.30 -                 #> (Option.map (Config.put ATP_Systems.vampire_force_sos)
    1.31 -                       vampire_force_sos |> the_default I)
    1.32 +                 #> (Option.map (Config.put ATP_Systems.force_sos)
    1.33 +                       force_sos |> the_default I)
    1.34                   #> Config.put Sledgehammer_Provers.measure_run_time true)
    1.35      val params as {relevance_thresholds, max_relevant, slicing, ...} =
    1.36        Sledgehammer_Isar.default_params ctxt
    1.37 @@ -466,9 +463,7 @@
    1.38      val slicing = AList.lookup (op =) args slicingK |> the_default "true"
    1.39      val lambda_translation = AList.lookup (op =) args lambda_translationK
    1.40      val e_weight_method = AList.lookup (op =) args e_weight_methodK
    1.41 -    val spass_force_sos = AList.lookup (op =) args spass_force_sosK
    1.42 -      |> Option.map (curry (op <>) "false")
    1.43 -    val vampire_force_sos = AList.lookup (op =) args vampire_force_sosK
    1.44 +    val force_sos = AList.lookup (op =) args force_sosK
    1.45        |> Option.map (curry (op <>) "false")
    1.46      val dir = AList.lookup (op =) args keepK
    1.47      val timeout = Mirabelle.get_int_setting args (prover_timeoutK, 30)
    1.48 @@ -477,8 +472,8 @@
    1.49      val hard_timeout = SOME (2 * timeout)
    1.50      val (msg, result) =
    1.51        run_sh prover_name prover type_enc sound max_relevant slicing
    1.52 -        lambda_translation e_weight_method spass_force_sos vampire_force_sos
    1.53 -        hard_timeout timeout dir pos st
    1.54 +        lambda_translation e_weight_method force_sos hard_timeout timeout dir
    1.55 +        pos st
    1.56    in
    1.57      case result of
    1.58        SH_OK (time_isa, time_prover, names) =>

     2.1 --- a/src/HOL/Tools/ATP/atp_systems.ML	Tue Aug 09 17:33:17 2011 +0200
     2.2 +++ b/src/HOL/Tools/ATP/atp_systems.ML	Tue Aug 09 17:33:17 2011 +0200
     2.3 @@ -25,6 +25,7 @@
     2.4       best_slices :
     2.5         Proof.context -> (real * (bool * (int * string * string))) list}
     2.6  
     2.7 +  val force_sos : bool Config.T
     2.8    val e_smartN : string
     2.9    val e_autoN : string
    2.10    val e_fun_weightN : string
    2.11 @@ -36,8 +37,6 @@
    2.12    val e_default_sym_offs_weight : real Config.T
    2.13    val e_sym_offs_weight_base : real Config.T
    2.14    val e_sym_offs_weight_span : real Config.T
    2.15 -  val spass_force_sos : bool Config.T
    2.16 -  val vampire_force_sos : bool Config.T
    2.17    val eN : string
    2.18    val spassN : string
    2.19    val vampireN : string
    2.20 @@ -103,11 +102,11 @@
    2.21  (* named ATPs *)
    2.22  
    2.23  val eN = "e"
    2.24 +val leo2N = "leo2"
    2.25 +val satallaxN = "satallax"
    2.26  val spassN = "spass"
    2.27  val vampireN = "vampire"
    2.28  val z3_atpN = "z3_atp"
    2.29 -val leo2N = "leo2"
    2.30 -val satallaxN = "satallax"
    2.31  val e_sineN = "e_sine"
    2.32  val snarkN = "snark"
    2.33  val e_tofofN = "e_tofof"
    2.34 @@ -128,6 +127,8 @@
    2.35  val sosN = "sos"
    2.36  val no_sosN = "no_sos"
    2.37  
    2.38 +val force_sos = Attrib.setup_config_bool @{binding atp_force_sos} (K false)
    2.39 +
    2.40  
    2.41  (* E *)
    2.42  
    2.43 @@ -228,11 +229,50 @@
    2.44  val e = (eN, e_config)
    2.45  
    2.46  
    2.47 +(* LEO-II *)
    2.48 +
    2.49 +val leo2_config : atp_config =
    2.50 +  {exec = ("LEO2_HOME", "leo"),
    2.51 +   required_execs = [],
    2.52 +   arguments =
    2.53 +     fn _ => fn _ => fn sos => fn timeout => fn _ =>
    2.54 +        "--proofoutput --timeout " ^ string_of_int (to_secs 1 timeout)
    2.55 +        |> sos = sosN ? prefix "--sos ",
    2.56 +   proof_delims = tstp_proof_delims,
    2.57 +   known_failures = [],
    2.58 +   conj_sym_kind = Axiom,
    2.59 +   prem_kind = Hypothesis,
    2.60 +   formats = [THF, FOF],
    2.61 +   best_slices = fn ctxt =>
    2.62 +     (* FUDGE *)
    2.63 +     [(0.667, (false, (150, "simple_higher", sosN))),
    2.64 +      (0.333, (true, (50, "simple_higher", no_sosN)))]
    2.65 +     |> (if Config.get ctxt force_sos then hd #> apfst (K 1.0) #> single
    2.66 +         else I)}
    2.67 +
    2.68 +val leo2 = (leo2N, leo2_config)
    2.69 +
    2.70 +
    2.71 +(* Satallax *)
    2.72 +
    2.73 +val satallax_config : atp_config =
    2.74 +  {exec = ("SATALLAX_HOME", "satallax"),
    2.75 +   required_execs = [],
    2.76 +   arguments =
    2.77 +     fn _ => fn _ => fn _ => fn timeout => fn _ =>
    2.78 +        "-t " ^ string_of_int (to_secs 1 timeout),
    2.79 +   proof_delims = tstp_proof_delims,
    2.80 +   known_failures = [(ProofMissing, "SZS status Theorem")],
    2.81 +   conj_sym_kind = Axiom,
    2.82 +   prem_kind = Hypothesis,
    2.83 +   formats = [THF],
    2.84 +   best_slices = K [(1.0, (true, (100, "simple_higher", "")))] (* FUDGE *)}
    2.85 +
    2.86 +val satallax = (satallaxN, satallax_config)
    2.87 +
    2.88 +
    2.89  (* SPASS *)
    2.90  
    2.91 -val spass_force_sos =
    2.92 -  Attrib.setup_config_bool @{binding atp_spass_force_sos} (K false)
    2.93 -
    2.94  (* The "-VarWeight=3" option helps the higher-order problems, probably by
    2.95     counteracting the presence of "hAPP". *)
    2.96  val spass_config : atp_config =
    2.97 @@ -260,7 +300,7 @@
    2.98       [(0.333, (false, (150, "mangled_tags", sosN))),
    2.99        (0.333, (false, (300, "poly_tags?", sosN))),
   2.100        (0.334, (true, (50, "mangled_tags?", no_sosN)))]
   2.101 -     |> (if Config.get ctxt spass_force_sos then hd #> apfst (K 1.0) #> single
   2.102 +     |> (if Config.get ctxt force_sos then hd #> apfst (K 1.0) #> single
   2.103           else I)}
   2.104  
   2.105  val spass = (spassN, spass_config)
   2.106 @@ -268,9 +308,6 @@
   2.107  
   2.108  (* Vampire *)
   2.109  
   2.110 -val vampire_force_sos =
   2.111 -  Attrib.setup_config_bool @{binding atp_vampire_force_sos} (K false)
   2.112 -
   2.113  val vampire_config : atp_config =
   2.114    {exec = ("VAMPIRE_HOME", "vampire"),
   2.115     required_execs = [],
   2.116 @@ -301,7 +338,7 @@
   2.117       [(0.333, (false, (150, "poly_guards", sosN))),
   2.118        (0.334, (true, (50, "mangled_guards?", no_sosN))),
   2.119        (0.333, (false, (500, "mangled_tags?", sosN)))]
   2.120 -     |> (if Config.get ctxt vampire_force_sos then hd #> apfst (K 1.0) #> single
   2.121 +     |> (if Config.get ctxt force_sos then hd #> apfst (K 1.0) #> single
   2.122           else I)}
   2.123  
   2.124  val vampire = (vampireN, vampire_config)
   2.125 @@ -411,17 +448,17 @@
   2.126  val remote_e =
   2.127    remotify_atp e "EP" ["1.0", "1.1", "1.2"]
   2.128                 (K (750, "mangled_tags?") (* FUDGE *))
   2.129 +val remote_leo2 =
   2.130 +  remotify_atp leo2 "LEO-II" ["1.2.8", "1.2.6"]
   2.131 +               (K (100, "simple_higher") (* FUDGE *))
   2.132 +val remote_satallax =
   2.133 +  remotify_atp satallax "Satallax" ["2.1", "2.0", "2"]
   2.134 +               (K (100, "simple_higher") (* FUDGE *))
   2.135  val remote_vampire =
   2.136    remotify_atp vampire "Vampire" ["0.6", "9.0", "1.0"]
   2.137                 (K (200, "mangled_guards?") (* FUDGE *))
   2.138  val remote_z3_atp =
   2.139    remotify_atp z3_atp "Z3" ["2.18"] (K (250, "mangled_guards?") (* FUDGE *))
   2.140 -val remote_leo2 =
   2.141 -  remote_atp leo2N "LEO-II" ["1.2.6"] [] [] Axiom Hypothesis [THF, FOF]
   2.142 -             (K (100, "simple_higher") (* FUDGE *))
   2.143 -val remote_satallax =
   2.144 -  remote_atp satallaxN "Satallax" ["2.0"] [] [] Axiom Hypothesis [THF]
   2.145 -             (K (64, "simple_higher") (* FUDGE *))
   2.146  val remote_e_sine =
   2.147    remote_atp e_sineN "SInE" ["0.4"] [] (#known_failures e_config) Axiom
   2.148               Conjecture [FOF] (K (500, "mangled_guards?") (* FUDGE *))
   2.149 @@ -461,9 +498,9 @@
   2.150    Synchronized.change systems (fn _ => get_systems ())
   2.151  
   2.152  val atps =
   2.153 -  [e, spass, vampire, z3_atp, remote_e, remote_vampire, remote_z3_atp,
   2.154 -   remote_leo2, remote_satallax, remote_e_sine, remote_snark, remote_e_tofof,
   2.155 -   remote_waldmeister]
   2.156 +  [e, leo2, satallax, spass, vampire, z3_atp, remote_e, remote_leo2,
   2.157 +   remote_satallax, remote_vampire, remote_z3_atp, remote_e_sine, remote_snark,
   2.158 +   remote_e_tofof, remote_waldmeister]
   2.159  val setup = fold add_atp atps
   2.160  
   2.161  end;