src/HOL/Tools/ATP/atp_systems.ML
changeset 44099 5e14f591515e
parent 44096 6e943b3d2767
child 44235 85e9dad3c187
     1.1 --- a/src/HOL/Tools/ATP/atp_systems.ML	Tue Aug 09 17:33:17 2011 +0200
     1.2 +++ b/src/HOL/Tools/ATP/atp_systems.ML	Tue Aug 09 17:33:17 2011 +0200
     1.3 @@ -25,6 +25,7 @@
     1.4       best_slices :
     1.5         Proof.context -> (real * (bool * (int * string * string))) list}
     1.6  
     1.7 +  val force_sos : bool Config.T
     1.8    val e_smartN : string
     1.9    val e_autoN : string
    1.10    val e_fun_weightN : string
    1.11 @@ -36,8 +37,6 @@
    1.12    val e_default_sym_offs_weight : real Config.T
    1.13    val e_sym_offs_weight_base : real Config.T
    1.14    val e_sym_offs_weight_span : real Config.T
    1.15 -  val spass_force_sos : bool Config.T
    1.16 -  val vampire_force_sos : bool Config.T
    1.17    val eN : string
    1.18    val spassN : string
    1.19    val vampireN : string
    1.20 @@ -103,11 +102,11 @@
    1.21  (* named ATPs *)
    1.22  
    1.23  val eN = "e"
    1.24 +val leo2N = "leo2"
    1.25 +val satallaxN = "satallax"
    1.26  val spassN = "spass"
    1.27  val vampireN = "vampire"
    1.28  val z3_atpN = "z3_atp"
    1.29 -val leo2N = "leo2"
    1.30 -val satallaxN = "satallax"
    1.31  val e_sineN = "e_sine"
    1.32  val snarkN = "snark"
    1.33  val e_tofofN = "e_tofof"
    1.34 @@ -128,6 +127,8 @@
    1.35  val sosN = "sos"
    1.36  val no_sosN = "no_sos"
    1.37  
    1.38 +val force_sos = Attrib.setup_config_bool @{binding atp_force_sos} (K false)
    1.39 +
    1.40  
    1.41  (* E *)
    1.42  
    1.43 @@ -228,10 +229,49 @@
    1.44  val e = (eN, e_config)
    1.45  
    1.46  
    1.47 -(* SPASS *)
    1.48 +(* LEO-II *)
    1.49 +
    1.50 +val leo2_config : atp_config =
    1.51 +  {exec = ("LEO2_HOME", "leo"),
    1.52 +   required_execs = [],
    1.53 +   arguments =
    1.54 +     fn _ => fn _ => fn sos => fn timeout => fn _ =>
    1.55 +        "--proofoutput --timeout " ^ string_of_int (to_secs 1 timeout)
    1.56 +        |> sos = sosN ? prefix "--sos ",
    1.57 +   proof_delims = tstp_proof_delims,
    1.58 +   known_failures = [],
    1.59 +   conj_sym_kind = Axiom,
    1.60 +   prem_kind = Hypothesis,
    1.61 +   formats = [THF, FOF],
    1.62 +   best_slices = fn ctxt =>
    1.63 +     (* FUDGE *)
    1.64 +     [(0.667, (false, (150, "simple_higher", sosN))),
    1.65 +      (0.333, (true, (50, "simple_higher", no_sosN)))]
    1.66 +     |> (if Config.get ctxt force_sos then hd #> apfst (K 1.0) #> single
    1.67 +         else I)}
    1.68  
    1.69 -val spass_force_sos =
    1.70 -  Attrib.setup_config_bool @{binding atp_spass_force_sos} (K false)
    1.71 +val leo2 = (leo2N, leo2_config)
    1.72 +
    1.73 +
    1.74 +(* Satallax *)
    1.75 +
    1.76 +val satallax_config : atp_config =
    1.77 +  {exec = ("SATALLAX_HOME", "satallax"),
    1.78 +   required_execs = [],
    1.79 +   arguments =
    1.80 +     fn _ => fn _ => fn _ => fn timeout => fn _ =>
    1.81 +        "-t " ^ string_of_int (to_secs 1 timeout),
    1.82 +   proof_delims = tstp_proof_delims,
    1.83 +   known_failures = [(ProofMissing, "SZS status Theorem")],
    1.84 +   conj_sym_kind = Axiom,
    1.85 +   prem_kind = Hypothesis,
    1.86 +   formats = [THF],
    1.87 +   best_slices = K [(1.0, (true, (100, "simple_higher", "")))] (* FUDGE *)}
    1.88 +
    1.89 +val satallax = (satallaxN, satallax_config)
    1.90 +
    1.91 +
    1.92 +(* SPASS *)
    1.93  
    1.94  (* The "-VarWeight=3" option helps the higher-order problems, probably by
    1.95     counteracting the presence of "hAPP". *)
    1.96 @@ -260,7 +300,7 @@
    1.97       [(0.333, (false, (150, "mangled_tags", sosN))),
    1.98        (0.333, (false, (300, "poly_tags?", sosN))),
    1.99        (0.334, (true, (50, "mangled_tags?", no_sosN)))]
   1.100 -     |> (if Config.get ctxt spass_force_sos then hd #> apfst (K 1.0) #> single
   1.101 +     |> (if Config.get ctxt force_sos then hd #> apfst (K 1.0) #> single
   1.102           else I)}
   1.103  
   1.104  val spass = (spassN, spass_config)
   1.105 @@ -268,9 +308,6 @@
   1.106  
   1.107  (* Vampire *)
   1.108  
   1.109 -val vampire_force_sos =
   1.110 -  Attrib.setup_config_bool @{binding atp_vampire_force_sos} (K false)
   1.111 -
   1.112  val vampire_config : atp_config =
   1.113    {exec = ("VAMPIRE_HOME", "vampire"),
   1.114     required_execs = [],
   1.115 @@ -301,7 +338,7 @@
   1.116       [(0.333, (false, (150, "poly_guards", sosN))),
   1.117        (0.334, (true, (50, "mangled_guards?", no_sosN))),
   1.118        (0.333, (false, (500, "mangled_tags?", sosN)))]
   1.119 -     |> (if Config.get ctxt vampire_force_sos then hd #> apfst (K 1.0) #> single
   1.120 +     |> (if Config.get ctxt force_sos then hd #> apfst (K 1.0) #> single
   1.121           else I)}
   1.122  
   1.123  val vampire = (vampireN, vampire_config)
   1.124 @@ -411,17 +448,17 @@
   1.125  val remote_e =
   1.126    remotify_atp e "EP" ["1.0", "1.1", "1.2"]
   1.127                 (K (750, "mangled_tags?") (* FUDGE *))
   1.128 +val remote_leo2 =
   1.129 +  remotify_atp leo2 "LEO-II" ["1.2.8", "1.2.6"]
   1.130 +               (K (100, "simple_higher") (* FUDGE *))
   1.131 +val remote_satallax =
   1.132 +  remotify_atp satallax "Satallax" ["2.1", "2.0", "2"]
   1.133 +               (K (100, "simple_higher") (* FUDGE *))
   1.134  val remote_vampire =
   1.135    remotify_atp vampire "Vampire" ["0.6", "9.0", "1.0"]
   1.136                 (K (200, "mangled_guards?") (* FUDGE *))
   1.137  val remote_z3_atp =
   1.138    remotify_atp z3_atp "Z3" ["2.18"] (K (250, "mangled_guards?") (* FUDGE *))
   1.139 -val remote_leo2 =
   1.140 -  remote_atp leo2N "LEO-II" ["1.2.6"] [] [] Axiom Hypothesis [THF, FOF]
   1.141 -             (K (100, "simple_higher") (* FUDGE *))
   1.142 -val remote_satallax =
   1.143 -  remote_atp satallaxN "Satallax" ["2.0"] [] [] Axiom Hypothesis [THF]
   1.144 -             (K (64, "simple_higher") (* FUDGE *))
   1.145  val remote_e_sine =
   1.146    remote_atp e_sineN "SInE" ["0.4"] [] (#known_failures e_config) Axiom
   1.147               Conjecture [FOF] (K (500, "mangled_guards?") (* FUDGE *))
   1.148 @@ -461,9 +498,9 @@
   1.149    Synchronized.change systems (fn _ => get_systems ())
   1.150  
   1.151  val atps =
   1.152 -  [e, spass, vampire, z3_atp, remote_e, remote_vampire, remote_z3_atp,
   1.153 -   remote_leo2, remote_satallax, remote_e_sine, remote_snark, remote_e_tofof,
   1.154 -   remote_waldmeister]
   1.155 +  [e, leo2, satallax, spass, vampire, z3_atp, remote_e, remote_leo2,
   1.156 +   remote_satallax, remote_vampire, remote_z3_atp, remote_e_sine, remote_snark,
   1.157 +   remote_e_tofof, remote_waldmeister]
   1.158  val setup = fold add_atp atps
   1.159  
   1.160  end;