update SPASS slices
authorblanchet
Fri Feb 10 16:33:58 2012 +0100 (2012-02-10)
changeset 46449312b49fba357
parent 46448 f1201fac7398
child 46450 7560930b2e06
update SPASS slices
src/HOL/Tools/ATP/atp_systems.ML
     1.1 --- a/src/HOL/Tools/ATP/atp_systems.ML	Fri Feb 10 09:47:59 2012 +0100
     1.2 +++ b/src/HOL/Tools/ATP/atp_systems.ML	Fri Feb 10 16:33:58 2012 +0100
     1.3 @@ -246,12 +246,9 @@
     1.4       let val method = effective_e_weight_method ctxt in
     1.5         (* FUDGE *)
     1.6         if method = e_smartN then
     1.7 -         [(0.333, (true, ((500, FOF, "mono_tags??", combsN, false),
     1.8 -                          e_fun_weightN))),
     1.9 -          (0.334, (true, ((50, FOF, "mono_guards??", combsN, false),
    1.10 -                          e_fun_weightN))),
    1.11 -          (0.333, (true, ((1000, FOF, "mono_tags??", combsN, false),
    1.12 -                          e_sym_offset_weightN)))]
    1.13 +         [(0.333, (true, ((500, FOF, "mono_tags??", combsN, false), e_fun_weightN))),
    1.14 +          (0.334, (true, ((50, FOF, "mono_guards??", combsN, false), e_fun_weightN))),
    1.15 +          (0.333, (true, ((1000, FOF, "mono_tags??", combsN, false), e_sym_offset_weightN)))]
    1.16         else
    1.17           [(1.0, (true, ((500, FOF, "mono_tags??", combsN, false), method)))]
    1.18       end}
    1.19 @@ -278,10 +275,8 @@
    1.20     prem_kind = Hypothesis,
    1.21     best_slices = fn ctxt =>
    1.22       (* FUDGE *)
    1.23 -     [(0.667, (false, ((150, leo2_thf0, "mono_native_higher", liftingN, false),
    1.24 -                       sosN))),
    1.25 -      (0.333, (true, ((50, leo2_thf0, "mono_native_higher", liftingN, false),
    1.26 -                      no_sosN)))]
    1.27 +     [(0.667, (false, ((150, leo2_thf0, "mono_native_higher", liftingN, false), sosN))),
    1.28 +      (0.333, (true, ((50, leo2_thf0, "mono_native_higher", liftingN, false), no_sosN)))]
    1.29       |> (if Config.get ctxt force_sos then hd #> apfst (K 1.0) #> single
    1.30           else I)}
    1.31  
    1.32 @@ -305,8 +300,7 @@
    1.33     prem_kind = Hypothesis,
    1.34     best_slices =
    1.35       (* FUDGE *)
    1.36 -     K [(1.0, (true, ((100, satallax_thf0, "mono_native_higher", keep_lamsN,
    1.37 -                       false), "")))]}
    1.38 +     K [(1.0, (true, ((100, satallax_thf0, "mono_native_higher", keep_lamsN, false), "")))]}
    1.39  
    1.40  val satallax = (satallaxN, satallax_config)
    1.41  
    1.42 @@ -336,23 +330,23 @@
    1.43     prem_kind = Conjecture,
    1.44     best_slices = fn ctxt =>
    1.45       (* FUDGE *)
    1.46 -     [(0.333, (false, ((150, DFG DFG_Unsorted, "mono_tags??", liftingN, false),
    1.47 -                       sosN))),
    1.48 -      (0.333, (false, ((300, DFG DFG_Unsorted, "poly_tags??", liftingN, false),
    1.49 -                       sosN))),
    1.50 -      (0.334, (false, ((50, DFG DFG_Unsorted, "mono_tags??", liftingN, false),
    1.51 -                       no_sosN)))]
    1.52 -     |> (if Config.get ctxt force_sos then hd #> apfst (K 1.0) #> single
    1.53 -         else I)}
    1.54 +     [(0.333, (false, ((150, DFG DFG_Unsorted, "mono_tags??", liftingN, false), sosN))),
    1.55 +      (0.333, (false, ((300, DFG DFG_Unsorted, "poly_tags??", liftingN, false), sosN))),
    1.56 +      (0.334, (false, ((50, DFG DFG_Unsorted, "mono_tags??", liftingN, false), no_sosN)))]
    1.57 +     |> (if Config.get ctxt force_sos then hd #> apfst (K 1.0) #> single else I)}
    1.58  
    1.59  val spass = (spassN, spass_config)
    1.60  
    1.61 +val spass_new_H2 = "-Heuristic=2"
    1.62 +val spass_new_H2_SOS = "-Heuristic=2 -SOS"
    1.63 +val spass_new_Red2 = "-RFRew=2 -RBRew=2 -RTaut=2"
    1.64 +val spass_new_Sorts0 = "-Sorts=0"
    1.65 +
    1.66  (* Experimental *)
    1.67  val spass_new_config : atp_config =
    1.68    {exec = ("SPASS_NEW_HOME", "SPASS"),
    1.69     required_execs = [],
    1.70     arguments = fn _ => fn _ => fn extra_options => fn timeout => fn _ =>
    1.71 -     (* TODO: add: -FPDFGProof -FPFCR *)
    1.72       ("-Isabelle=1 -TimeLimit=" ^ string_of_int (to_secs 1 timeout))
    1.73       |> extra_options <> "" ? prefix (extra_options ^ " "),
    1.74     proof_delims = #proof_delims spass_config,
    1.75 @@ -361,16 +355,23 @@
    1.76     prem_kind = #prem_kind spass_config,
    1.77     best_slices = fn _ =>
    1.78       (* FUDGE *)
    1.79 -     [(0.25, (true, ((150, DFG DFG_Sorted, "mono_native", combsN, true),
    1.80 -                     "-Heuristic=1"))),
    1.81 -      (0.20, (true, ((500, DFG DFG_Sorted, "mono_native", liftingN, true),
    1.82 -                     "-Heuristic=2 -SOS"))),
    1.83 -      (0.20, (true, ((50, DFG DFG_Sorted, "mono_native", liftingN, true),
    1.84 -                     "-Heuristic=2"))),
    1.85 -      (0.20, (true, ((250, DFG DFG_Sorted, "mono_native", combs_and_liftingN,
    1.86 -                      true), "-Heuristic=2"))),
    1.87 -      (0.15, (true, ((100, DFG DFG_Sorted, "mono_native", combs_and_liftingN,
    1.88 -                      true), "-Heuristic=2")))]}
    1.89 +(*
    1.90 +     [(0.25, (true, ((150, DFG DFG_Sorted, "mono_native", combsN, true), spass_new_H1))),
    1.91 +      (0.20, (false, ((500, DFG DFG_Sorted, "mono_native", liftingN, true), spass_new_H2_SOS))),
    1.92 +      (0.20, (true, ((50, DFG DFG_Sorted, "mono_native", liftingN, true), spass_new_H2))),
    1.93 +      (0.20, (true, ((250, DFG DFG_Sorted, "mono_native", combs_and_liftingN, true), spass_new_H2))),
    1.94 +      (0.15, (true, ((100, DFG DFG_Sorted, "mono_native", combs_and_liftingN, true), spass_new_H2)))]
    1.95 +*)
    1.96 +     [(0.1, (true, ((50, DFG DFG_Sorted, "mono_native", liftingN, true), spass_new_H2))),
    1.97 +      (0.1, (true, ((150, DFG DFG_Sorted, "mono_native", combsN, true), spass_new_Sorts0))),
    1.98 +      (0.1, (true, ((250, DFG DFG_Sorted, "mono_native", combs_and_liftingN, true), spass_new_H2))),
    1.99 +      (0.1, (false, ((500, DFG DFG_Sorted, "mono_native", liftingN, true), spass_new_H2_SOS))),
   1.100 +      (0.1, (true, ((600, DFG DFG_Sorted, "mono_native", combs_and_liftingN, true), spass_new_Red2))),
   1.101 +      (0.1, (true, ((150, DFG DFG_Sorted, "poly_guards??", combsN, false), spass_new_H2))),
   1.102 +      (0.1, (false, ((300, DFG DFG_Sorted, "mono_native", combsN, true), spass_new_H2_SOS))),
   1.103 +      (0.1, (true, ((100, DFG DFG_Sorted, "mono_native", combs_and_liftingN, true), spass_new_H2))),
   1.104 +      (0.1, (true, ((50, DFG DFG_Sorted, "mono_native", combsN, true), spass_new_Sorts0))),
   1.105 +      (0.1, (true, ((100, DFG DFG_Sorted, "poly_guards??", liftingN, false), spass_new_Red2)))]}
   1.106  
   1.107  val spass_new = (spass_newN, spass_new_config)
   1.108  
   1.109 @@ -410,19 +411,13 @@
   1.110     best_slices = fn ctxt =>
   1.111       (* FUDGE *)
   1.112       (if is_old_vampire_version () then
   1.113 -        [(0.333, (false, ((150, FOF, "poly_guards??", combs_or_liftingN, false),
   1.114 -                          sosN))),
   1.115 -         (0.333, (false, ((500, FOF, "mono_tags??", combs_or_liftingN, false),
   1.116 -                          sosN))),
   1.117 -         (0.334, (true, ((50, FOF, "mono_guards??", combs_or_liftingN, false),
   1.118 -                         no_sosN)))]
   1.119 +        [(0.333, (false, ((150, FOF, "poly_guards??", combs_or_liftingN, false), sosN))),
   1.120 +         (0.333, (false, ((500, FOF, "mono_tags??", combs_or_liftingN, false), sosN))),
   1.121 +         (0.334, (true, ((50, FOF, "mono_guards??", combs_or_liftingN, false), no_sosN)))]
   1.122        else
   1.123 -        [(0.333, (false, ((150, vampire_tff0, "poly_guards??",
   1.124 -                           combs_or_liftingN, false), sosN))),
   1.125 -         (0.333, (false, ((500, vampire_tff0, "mono_native", combs_or_liftingN,
   1.126 -                           false), sosN))),
   1.127 -         (0.334, (true, ((50, vampire_tff0, "mono_native", combs_or_liftingN,
   1.128 -                          false), no_sosN)))])
   1.129 +        [(0.333, (false, ((150, vampire_tff0, "poly_guards??", combs_or_liftingN, false), sosN))),
   1.130 +         (0.333, (false, ((500, vampire_tff0, "mono_native", combs_or_liftingN, false), sosN))),
   1.131 +         (0.334, (true, ((50, vampire_tff0, "mono_native", combs_or_liftingN, false), no_sosN)))])
   1.132       |> (if Config.get ctxt force_sos then hd #> apfst (K 1.0) #> single
   1.133           else I)}
   1.134